let range = pos * pos
let range =
pos * pos
Ast.fst.checked
prims.fst.checked Options.fsti.checked Hashtable.fsti.checked FStar.UInt.fsti.checked FStar.String.fsti.checked FStar.ST.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Ast.fst
FStar.Pervasives.Native.tuple2 Ast.pos
(*
   Copyright 2019 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Ast
(* The source abstract syntax for the 3d frontend to EverParse *)

open FStar.All

let reserved_prefix = "___"

//redefining either because we need to serialize to Json
[@@ PpxDerivingYoJson ]
type either a b =
  | Inl of a
  | Inr of b

/// pos: Source locations
type pos = {
  filename: string;
  line:int;
  col:int
}

noeq
type comments_buffer_t = {
  push: string & pos & pos -> ML unit;
  flush: unit -> ML (list string);
  flush_until: pos -> ML (list string);
}

#push-options "--warn_error -272" //top-level effect; ok
let comments_buffer : comments_buffer_t =
  let buffer : ref (list (string & pos & pos)) = FStar.ST.alloc [] in
  let buffer_comment (c, s, p) =
    let c = String.substring c 2 (String.length c - 2) in
    buffer := (c, s, p) :: !buffer
  in
  let flush_comments () =
    let cs = !buffer in
    buffer := [];
    (List.rev cs) |> List.map (fun (c, _, _) -> c)
  in
  let flush_until pos : ML (list string) =
    let cs = !buffer in
    let preceding, following =
      List.partition (fun (c, _, end_pos) ->
        Options.debug_print_string
          (Printf.sprintf "Requesting comments until line %d,\nAt line %d we have comment (*%s*)\n"
            pos.line
            end_pos.line
            c);
          end_pos.line <= pos.line) cs
    in
    buffer := following;
    preceding |> List.map (fun (c, _, _) -> c)
  in
  {
    push = buffer_comment;
    flush = flush_comments;
    flush_until = flush_until
  }
#pop-options

let string_of_pos p =
  Printf.sprintf "%s:(%d,%d)" p.filename p.line p.col
val range : Type0
Type0