val comments_buffer:comments_buffer_t
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
  }
val comments_buffer:comments_buffer_t
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 }
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
Ast.Mkcomments_buffer_t Ast.pos Prims.list Prims.string FStar.Pervasives.Native.tuple3 FStar.All.op_Bar_Greater FStar.List.map Prims.unit FStar.ST.op_Colon_Equals FStar.Heap.trivial_preorder FStar.Pervasives.Native.tuple2 FStar.List.partition Prims.op_LessThanOrEqual Ast.__proj__Mkpos__item__line Prims.bool Options.debug_print_string FStar.Printf.sprintf FStar.ST.op_Bang FStar.Pervasives.all_post_h FStar.Monotonic.Heap.heap Prims.l_and FStar.Monotonic.Heap.sel Prims.Nil Prims.l_Forall Prims.l_imp FStar.Monotonic.Heap.contains FStar.Monotonic.Heap.modifies FStar.Set.singleton Prims.nat FStar.Monotonic.Heap.addr_of FStar.Monotonic.Heap.equal_dom Prims.eq2 FStar.Pervasives.result FStar.List.Tot.Base.rev Prims.l_True FStar.Pervasives.V Prims.exn FStar.Pervasives.E FStar.Pervasives.Err Prims.Cons FStar.Pervasives.Native.Mktuple3 FStar.String.substring Prims.op_Subtraction FStar.String.length Ast.comments_buffer_t FStar.ST.ref FStar.ST.alloc FStar.ST.mref
(*
   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);
}
val comments_buffer:comments_buffer_t
Ast.comments_buffer_t