refinedc_parser.expected

open Earley_core
open Earley
open Extra
[@@@ocaml.text " {3 Combinators and utilities} "]
type 'a quot_elt =
  | Quot_plain of string 
  | Quot_anti of 'a 
type 'a quoted = 'a quot_elt list
let well_bracketed : char -> char -> 'a grammar -> 'a quoted grammar =
  fun c_op ->
    fun c_cl ->
      fun anti_gr ->
        let fn buf pos =
          let elts = ref [] in
          let str = Buffer.create 20 in
          let flush_plain () =
            elts := ((Quot_plain (Buffer.contents str)) :: (!elts));
            Buffer.clear str in
          let flush_anti () =
            let text = Buffer.contents str in
            let anti =
              let parse = Earley.parse_string anti_gr Blanks.default in
              try parse text with | Earley.Parse_error (_, _) -> assert false in
            elts := ((Quot_anti anti) :: (!elts)); Buffer.clear str in
          let rec loop state buf pos =
            let (c, next_buf, next_pos) = Input.read buf pos in
            match (c, state) with
            | ('\255', _) -> Earley.give_up ()
            | ('\\', _) ->
                let c = Input.get next_buf next_pos in
                (if not (List.mem c ['\255'; '"'; '\\'])
                 then Earley.give_up ();
                 loop state next_buf next_pos)
            | (_, `Init i) when c = c_op ->
                (Buffer.add_char str c;
                 loop (`Init (i + 1)) next_buf next_pos)
            | (_, `Init 1) when c = c_cl ->
                (flush_plain (); (next_buf, next_pos))
            | (_, `Init i) when c = c_cl ->
                (Buffer.add_char str c;
                 loop (`Init (i - 1)) next_buf next_pos)
            | ('!', `Init i) -> loop (`Bang i) next_buf next_pos
            | ('{', `Bang i) ->
                (flush_plain (); loop (`Anti (1, i)) next_buf next_pos)
            | (_, `Bang i) ->
                (Buffer.add_char str '!'; loop (`Init i) buf pos)
            | ('{', `Anti (k, i)) ->
                (Buffer.add_char str c;
                 loop (`Anti ((k + 1), i)) next_buf next_pos)
            | ('}', `Anti (1, i)) ->
                (flush_anti (); loop (`Init i) next_buf next_pos)
            | ('}', `Anti (k, i)) ->
                (Buffer.add_char str '}';
                 loop (`Anti ((k - 1), i)) next_buf next_pos)
            | (_, _) -> (Buffer.add_char str c; loop state next_buf next_pos) in
          let (buf, pos) = loop (`Init 1) buf (pos + 1) in
          ((List.rev (!elts)), buf, pos) in
        let name = Printf.sprintf "<%cwell-bracketed%c>" c_op c_cl in
        Earley.black_box fn (Charset.singleton c_op) false name[@@ocaml.doc
                                                                 " [well_bracketed c_op c_cl anti_gr] is a grammar accepting strings starting\n    with character [c_op], and ending with character [c_cl]. Moreover, strings\n    with non-well-bracketed occurences of characters [c_op] / [c_cl] and ['{']\n    / ['}'] are rejected. A sequence of the form [\"!{text}\"] is interpreted as\n    an antiquotation. Its contents (here, [\"text\"]) is parsed using [anti_gr],\n    an it should itself be well-bracketed in terms of ['{'] / ['}']. Note that\n    the produced semantic value is a list of elements that can be either plain\n    text (using the [Quot_plain(s)] constructor) or an anti-quotation (using a\n    [Quot_anti(e)] constructor). "]
[@@@ocaml.text " {3 Annotations AST} "]
type ident = string
type pattern = ident list
type coq_term = type_expr quoted
and iris_term = type_expr quoted
and coq_expr =
  | Coq_ident of string 
  | Coq_all of coq_term 
and constr =
  | Constr_Iris of iris_term 
  | Constr_exist of string * coq_expr option * constr 
  | Constr_own of string * ptr_kind * type_expr 
  | Constr_Coq of coq_expr 
and ptr_kind =
  | Own 
  | Shr 
  | Frac of coq_expr 
and type_expr =
  | Ty_refine of coq_expr * type_expr 
  | Ty_ptr of ptr_kind * type_expr 
  | Ty_dots 
  | Ty_exists of pattern * coq_expr option * type_expr 
  | Ty_constr of type_expr * constr 
  | Ty_params of ident * type_expr_arg list 
  | Ty_Coq of coq_expr 
and type_expr_arg =
  | Ty_arg_expr of type_expr 
  | Ty_arg_lambda of pattern * coq_expr option * type_expr_arg 
type annot_arg = (int * int * coq_expr)
[@@@ocaml.text " {3 Main grammar defintions} "]
let ident : ident Earley.grammar =
  let cs_first = Charset.from_string "A-Za-z_" in
  let cs = Charset.from_string "A-Za-z_0-9" in
  let fn buf pos =
    let nb = ref 1 in
    while Charset.mem cs (Input.get buf (pos + (!nb))) do incr nb done;
    ((String.sub (Input.line buf) pos (!nb)), buf, (pos + (!nb))) in
  Earley.black_box fn cs_first false "<ident>"[@@ocaml.doc
                                                " Identifier token (regexp [\"[A-Za-z_]+\"]). "]
let integer : int Earley.grammar =
  let cs = Charset.from_string "0-9" in
  let fn buf pos =
    let nb = ref 1 in
    while Charset.mem cs (Input.get buf (pos + (!nb))) do incr nb done;
    ((int_of_string (String.sub (Input.line buf) pos (!nb))), buf,
      (pos + (!nb))) in
  Earley.black_box fn cs false "<integer>"[@@ocaml.doc
                                            " Integer token (regexp [\"[0-9]+\"]). "]
let pattern = Earley_core.Earley.declare_grammar "pattern"
let _ =
  Earley_core.Earley.set_grammar pattern
    (Earley_core.Earley.alternatives
       (List.cons
          (Earley_core.Earley.fsequence_ignore
             (Earley_core.Earley.string "(" "(")
             (Earley_core.Earley.fsequence ident
                (Earley_core.Earley.fsequence
                   (Earley_core.Earley.apply (fun f -> f [])
                      (Earley_core.Earley.fixpoint1' (fun l -> l)
                         (Earley_core.Earley.fsequence_ignore
                            (Earley_core.Earley.string "," ",")
                            (Earley_core.Earley.fsequence ident
                               (Earley_core.Earley.empty
                                  (fun _default_0 -> _default_0))))
                         (fun x -> fun f -> fun l -> f (List.cons x l))))
                   (Earley_core.Earley.fsequence_ignore
                      (Earley_core.Earley.string ")" ")")
                      (Earley_core.Earley.empty (fun xs -> fun x -> x :: xs))))))
          (List.cons
             (Earley_core.Earley.fsequence_ignore
                (Earley_core.Earley.string "(" "(")
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string ")" ")")
                   (Earley_core.Earley.empty [])))
             (List.cons
                (Earley_core.Earley.fsequence ident
                   (Earley_core.Earley.empty (fun x -> [x]))) []))))
let coq_term = Earley_core.Earley.declare_grammar "coq_term"
let iris_term = Earley_core.Earley.declare_grammar "iris_term"
let coq_expr = Earley_core.Earley.declare_grammar "coq_expr"
let constr = Earley_core.Earley.declare_grammar "constr"
let ptr_type = Earley_core.Earley.declare_grammar "ptr_type"
let (type_expr, type_expr__set__grammar) =
  Earley_core.Earley.grammar_prio "type_expr"
let type_expr_arg = Earley_core.Earley.declare_grammar "type_expr_arg"
let type_args = Earley_core.Earley.declare_grammar "type_args"
let _ =
  Earley_core.Earley.set_grammar coq_term
    (well_bracketed '{' '}' (type_expr `Full))
let _ =
  Earley_core.Earley.set_grammar iris_term
    (well_bracketed '[' ']' (type_expr `Full))
let _ =
  Earley_core.Earley.set_grammar coq_expr
    (Earley_core.Earley.alternatives
       (List.cons
          (Earley_core.Earley.fsequence coq_term
             (Earley_core.Earley.empty (fun s -> Coq_all s)))
          (List.cons
             (Earley_core.Earley.fsequence ident
                (Earley_core.Earley.empty (fun x -> Coq_ident x))) [])))
let _ =
  Earley_core.Earley.set_grammar constr
    (Earley_core.Earley.alternatives
       (List.cons
          (Earley_core.Earley.fsequence coq_expr
             (Earley_core.Earley.empty (fun c -> Constr_Coq c)))
          (List.cons
             (Earley_core.Earley.fsequence iris_term
                (Earley_core.Earley.empty (fun s -> Constr_Iris s)))
             (List.cons
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string "\226\136\131" "\226\136\131")
                   (Earley_core.Earley.fsequence ident
                      (Earley_core.Earley.fsequence
                         (Earley_core.Earley.option None
                            (Earley_core.Earley.apply (fun x -> Some x)
                               (Earley_core.Earley.fsequence_ignore
                                  (Earley_core.Earley.string ":" ":")
                                  (Earley_core.Earley.fsequence coq_expr
                                     (Earley_core.Earley.empty
                                        (fun _default_0 -> _default_0))))))
                         (Earley_core.Earley.fsequence_ignore
                            (Earley_core.Earley.string "." ".")
                            (Earley_core.Earley.fsequence constr
                               (Earley_core.Earley.empty
                                  (fun c ->
                                     fun a -> fun x -> Constr_exist (x, a, c))))))))
                (List.cons
                   (Earley_core.Earley.fsequence ident
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string "@" "@")
                         (Earley_core.Earley.fsequence ptr_type
                            (Earley_core.Earley.empty
                               (fun ((k, ty) as _default_0) ->
                                  fun x -> Constr_own (x, k, ty)))))) [])))))
let _ =
  Earley_core.Earley.set_grammar ptr_type
    (Earley_core.Earley.alternatives
       (List.cons
          (Earley_core.Earley.fsequence_ignore
             (Earley_core.Earley.string "&frac<" "&frac<")
             (Earley_core.Earley.fsequence coq_expr
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string "," ",")
                   (Earley_core.Earley.fsequence (type_expr `Full)
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string ">" ">")
                         (Earley_core.Earley.empty
                            (fun ty -> fun e -> ((Frac e), ty))))))))
          (List.cons
             (Earley_core.Earley.fsequence_ignore
                (Earley_core.Earley.string "&own<" "&own<")
                (Earley_core.Earley.fsequence (type_expr `Full)
                   (Earley_core.Earley.fsequence_ignore
                      (Earley_core.Earley.string ">" ">")
                      (Earley_core.Earley.empty (fun ty -> (Own, ty))))))
             (List.cons
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string "&shr<" "&shr<")
                   (Earley_core.Earley.fsequence (type_expr `Full)
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string ">" ">")
                         (Earley_core.Earley.empty (fun ty -> (Shr, ty))))))
                []))))
let _ =
  type_expr__set__grammar
    ((List.cons
        ((fun (p : [ `Atom  | `Cstr  | `Full ]) -> p >= `Atom),
          (Earley_core.Earley.fsequence_ignore
             (Earley_core.Earley.string "(" "(")
             (Earley_core.Earley.fsequence (type_expr `Full)
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string ")" ")")
                   (Earley_core.Earley.empty (fun ty -> ty))))))
        (List.cons
           ((fun (p : [ `Atom  | `Cstr  | `Full ]) -> p >= `Atom),
             (Earley_core.Earley.fsequence coq_expr
                (Earley_core.Earley.fsequence
                   (Earley_core.Earley.option None
                      (Earley_core.Earley.apply (fun x -> Some x)
                         (Earley_core.Earley.fsequence_ignore
                            (Earley_core.Earley.string "@" "@")
                            (Earley_core.Earley.fsequence (type_expr `Atom)
                               (Earley_core.Earley.empty
                                  (fun _default_0 -> _default_0))))))
                   (Earley_core.Earley.empty
                      (fun ty ->
                         fun c ->
                           match (c, ty) with
                           | (Coq_ident x, None) -> Ty_params (x, [])
                           | (_, None) -> Ty_Coq c
                           | (_, Some ty) -> Ty_refine (c, ty))))))
           (List.cons
              ((fun (p : [ `Atom  | `Cstr  | `Full ]) -> p >= `Atom),
                (Earley_core.Earley.fsequence ptr_type
                   (Earley_core.Earley.empty
                      (fun ((k, ty) as _default_0) -> Ty_ptr (k, ty)))))
              (List.cons
                 ((fun (p : [ `Atom  | `Cstr  | `Full ]) -> p >= `Atom),
                   (Earley_core.Earley.fsequence ident
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string "<" "<")
                         (Earley_core.Earley.fsequence type_args
                            (Earley_core.Earley.fsequence_ignore
                               (Earley_core.Earley.string ">" ">")
                               (Earley_core.Earley.empty
                                  (fun tys -> fun id -> Ty_params (id, tys))))))))
                 (List.cons
                    ((fun (p : [ `Atom  | `Cstr  | `Full ]) -> p >= `Atom),
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string "..." "...")
                         (Earley_core.Earley.empty Ty_dots)))
                    (List.cons
                       ((fun (p : [ `Atom  | `Cstr  | `Full ]) -> p >= `Full),
                         (Earley_core.Earley.fsequence_ignore
                            (Earley_core.Earley.string "\226\136\131"
                               "\226\136\131")
                            (Earley_core.Earley.fsequence pattern
                               (Earley_core.Earley.fsequence
                                  (Earley_core.Earley.option None
                                     (Earley_core.Earley.apply
                                        (fun x -> Some x)
                                        (Earley_core.Earley.fsequence_ignore
                                           (Earley_core.Earley.string ":" ":")
                                           (Earley_core.Earley.fsequence
                                              coq_expr
                                              (Earley_core.Earley.empty
                                                 (fun _default_0 ->
                                                    _default_0))))))
                                  (Earley_core.Earley.fsequence_ignore
                                     (Earley_core.Earley.string "." ".")
                                     (Earley_core.Earley.fsequence
                                        (type_expr `Full)
                                        (Earley_core.Earley.empty
                                           (fun ty ->
                                              fun a ->
                                                fun p -> Ty_exists (p, a, ty)))))))))
                       (List.cons
                          ((fun (p : [ `Atom  | `Cstr  | `Full ]) ->
                              p >= `Cstr),
                            (Earley_core.Earley.fsequence (type_expr `Cstr)
                               (Earley_core.Earley.fsequence_ignore
                                  (Earley_core.Earley.string "&" "&")
                                  (Earley_core.Earley.fsequence constr
                                     (Earley_core.Earley.empty
                                        (fun c -> fun ty -> Ty_constr (ty, c)))))))
                          []))))))),
      (fun (p : [ `Atom  | `Cstr  | `Full ]) -> []))
let _ =
  Earley_core.Earley.set_grammar type_expr_arg
    (Earley_core.Earley.alternatives
       (List.cons
          (Earley_core.Earley.fsequence_ignore
             (Earley_core.Earley.string "\206\187" "\206\187")
             (Earley_core.Earley.fsequence pattern
                (Earley_core.Earley.fsequence
                   (Earley_core.Earley.option None
                      (Earley_core.Earley.apply (fun x -> Some x)
                         (Earley_core.Earley.fsequence_ignore
                            (Earley_core.Earley.string ":" ":")
                            (Earley_core.Earley.fsequence coq_expr
                               (Earley_core.Earley.empty
                                  (fun _default_0 -> _default_0))))))
                   (Earley_core.Earley.fsequence_ignore
                      (Earley_core.Earley.string "." ".")
                      (Earley_core.Earley.fsequence type_expr_arg
                         (Earley_core.Earley.empty
                            (fun tya ->
                               fun a -> fun p -> Ty_arg_lambda (p, a, tya))))))))
          (List.cons
             (Earley_core.Earley.fsequence (type_expr `Full)
                (Earley_core.Earley.empty (fun ty -> Ty_arg_expr ty))) [])))
let _ =
  Earley_core.Earley.set_grammar type_args
    (Earley_core.Earley.alternatives
       (List.cons
          (Earley_core.Earley.fsequence type_expr_arg
             (Earley_core.Earley.fsequence
                (Earley_core.Earley.apply (fun f -> f [])
                   (Earley_core.Earley.fixpoint' (fun l -> l)
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string "," ",")
                         (Earley_core.Earley.fsequence type_expr_arg
                            (Earley_core.Earley.empty
                               (fun _default_0 -> _default_0))))
                      (fun x -> fun f -> fun l -> f (List.cons x l))))
                (Earley_core.Earley.empty (fun es -> fun e -> e :: es))))
          (List.cons
             (Earley_core.Earley.fsequence_ignore
                (Earley_core.Earley.empty ()) (Earley_core.Earley.empty []))
             [])))
[@@@ocaml.text
  " Arbitrary (\"well-bracketed\") string delimited by ['{'] and ['}']. "]
[@@@ocaml.text
  " Arbitrary (\"well-bracketed\") string delimited by ['['] and [']']. "]
let type_expr = type_expr `Full
[@@@ocaml.text " {3 Entry points} "]
[@@@ocaml.text " {4 Annotations on type definitions} "]
let annot_parameter = Earley_core.Earley.declare_grammar "annot_parameter"
let _ =
  Earley_core.Earley.set_grammar annot_parameter
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence_ignore
          (Earley_core.Earley.string ":" ":")
          (Earley_core.Earley.fsequence coq_expr
             (Earley_core.Earley.empty (fun s -> fun id -> (id, s))))) : 
    (ident * coq_expr) Earley.grammar)
let annot_refine = Earley_core.Earley.declare_grammar "annot_refine"
let _ =
  Earley_core.Earley.set_grammar annot_refine
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence_ignore
          (Earley_core.Earley.string ":" ":")
          (Earley_core.Earley.fsequence coq_expr
             (Earley_core.Earley.empty (fun s -> fun id -> (id, s))))) : 
    (ident * coq_expr) Earley.grammar)
let annot_ptr_type = Earley_core.Earley.declare_grammar "annot_ptr_type"
let _ =
  Earley_core.Earley.set_grammar annot_ptr_type
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence_ignore
          (Earley_core.Earley.string ":" ":")
          (Earley_core.Earley.fsequence type_expr
             (Earley_core.Earley.empty (fun ty -> fun id -> (id, ty))))) : 
    (ident * type_expr) Earley.grammar)
let annot_type = Earley_core.Earley.declare_grammar "annot_type"
let _ =
  Earley_core.Earley.set_grammar annot_type (ident : ident Earley.grammar)
[@@@ocaml.text " {4 Annotations on structs} "]
let annot_size = Earley_core.Earley.declare_grammar "annot_size"
let _ =
  Earley_core.Earley.set_grammar annot_size
    (coq_expr : coq_expr Earley.grammar)
let annot_exist = Earley_core.Earley.declare_grammar "annot_exist"
let _ =
  Earley_core.Earley.set_grammar annot_exist
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence_ignore
          (Earley_core.Earley.string ":" ":")
          (Earley_core.Earley.fsequence coq_expr
             (Earley_core.Earley.empty (fun s -> fun id -> (id, s))))) : 
    (ident * coq_expr) Earley.grammar)
let annot_constr = Earley_core.Earley.declare_grammar "annot_constr"
let _ =
  Earley_core.Earley.set_grammar annot_constr
    (constr : constr Earley.grammar)
[@@@ocaml.text " {4 Annotations on tagged unions} "]
type tag_spec = (string * (string * coq_expr) list)
let tagged_union : coq_expr Earley.grammar = coq_expr
let union_tag = Earley_core.Earley.declare_grammar "union_tag"
let _ =
  Earley_core.Earley.set_grammar union_tag
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence
          (Earley_core.Earley.apply (fun f -> f [])
             (Earley_core.Earley.fixpoint' (fun l -> l)
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string "(" "(")
                   (Earley_core.Earley.fsequence ident
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string ":" ":")
                         (Earley_core.Earley.fsequence coq_expr
                            (Earley_core.Earley.fsequence_ignore
                               (Earley_core.Earley.string ")" ")")
                               (Earley_core.Earley.empty
                                  (fun _default_0 ->
                                     fun _default_1 ->
                                       (_default_1, _default_0))))))))
                (fun x -> fun f -> fun l -> f (List.cons x l))))
          (Earley_core.Earley.empty (fun l -> fun c -> (c, l)))) : tag_spec
                                                                    Earley.grammar)
[@@@ocaml.text " {4 Annotations on fields} "]
let annot_field = Earley_core.Earley.declare_grammar "annot_field"
let _ =
  Earley_core.Earley.set_grammar annot_field
    (type_expr : type_expr Earley.grammar)
[@@@ocaml.text " {4 Annotations on global variables} "]
let annot_global = Earley_core.Earley.declare_grammar "annot_global"
let _ =
  Earley_core.Earley.set_grammar annot_global
    (type_expr : type_expr Earley.grammar)
[@@@ocaml.text " {4 Annotations on functions} "]
let annot_arg = Earley_core.Earley.declare_grammar "annot_arg"
let _ =
  Earley_core.Earley.set_grammar annot_arg
    (type_expr : type_expr Earley.grammar)
let annot_requires = Earley_core.Earley.declare_grammar "annot_requires"
let _ =
  Earley_core.Earley.set_grammar annot_requires
    (constr : constr Earley.grammar)
let annot_returns = Earley_core.Earley.declare_grammar "annot_returns"
let _ =
  Earley_core.Earley.set_grammar annot_returns
    (type_expr : type_expr Earley.grammar)
let annot_ensures = Earley_core.Earley.declare_grammar "annot_ensures"
let _ =
  Earley_core.Earley.set_grammar annot_ensures
    (constr : constr Earley.grammar)
let annot_args = Earley_core.Earley.declare_grammar "annot_args"
let _ =
  Earley_core.Earley.set_grammar annot_args
    (Earley_core.Earley.fsequence integer
       (Earley_core.Earley.fsequence_ignore
          (Earley_core.Earley.string ":" ":")
          (Earley_core.Earley.fsequence integer
             (Earley_core.Earley.fsequence coq_expr
                (Earley_core.Earley.empty
                   (fun _default_0 ->
                      fun _default_1 ->
                        fun _default_2 ->
                          (_default_2, _default_1, _default_0)))))) : 
    annot_arg Earley.grammar)
type manual_proof = (string * string * string)
let annot_manual = Earley_core.Earley.declare_grammar "annot_manual"
let _ =
  Earley_core.Earley.set_grammar annot_manual
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence
          (Earley_core.Earley.apply (fun f -> f [])
             (Earley_core.Earley.fixpoint' (fun l -> l)
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string "." ".")
                   (Earley_core.Earley.fsequence ident
                      (Earley_core.Earley.empty
                         (fun _default_0 -> _default_0))))
                (fun x -> fun f -> fun l -> f (List.cons x l))))
          (Earley_core.Earley.fsequence_ignore
             (Earley_core.Earley.string ":" ":")
             (Earley_core.Earley.fsequence ident
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string "," ",")
                   (Earley_core.Earley.fsequence ident
                      (Earley_core.Earley.empty
                         (fun thm ->
                            fun file ->
                              fun fs ->
                                fun f ->
                                  ((String.concat "." (f :: fs)), file, thm)))))))) : 
    manual_proof Earley.grammar)
[@@@ocaml.text " {4 Annotations on statement expressions (ExprS)} "]
[@@@ocaml.text " {4 Annotations on blocks} "]
let annot_inv_var = Earley_core.Earley.declare_grammar "annot_inv_var"
let _ =
  Earley_core.Earley.set_grammar annot_inv_var
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence_ignore
          (Earley_core.Earley.string ":" ":")
          (Earley_core.Earley.fsequence type_expr
             (Earley_core.Earley.empty (fun ty -> fun id -> (id, ty))))) : 
    (ident * type_expr) Earley.grammar)
[@@@ocaml.text " {4 Type definition (in comments)} "]
type typedef = (string * (string * coq_expr option) list * type_expr)
let typedef_arg = Earley_core.Earley.declare_grammar "typedef_arg"
let _ =
  Earley_core.Earley.set_grammar typedef_arg
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence
          (Earley_core.Earley.option None
             (Earley_core.Earley.apply (fun x -> Some x)
                (Earley_core.Earley.fsequence_ignore
                   (Earley_core.Earley.string ":" ":")
                   (Earley_core.Earley.fsequence coq_expr
                      (Earley_core.Earley.empty
                         (fun _default_0 -> _default_0))))))
          (Earley_core.Earley.empty
             (fun _default_0 -> fun _default_1 -> (_default_1, _default_0)))))
let typedef_args = Earley_core.Earley.declare_grammar "typedef_args"
let _ =
  Earley_core.Earley.set_grammar typedef_args
    (Earley_core.Earley.alternatives
       (List.cons
          (Earley_core.Earley.fsequence typedef_arg
             (Earley_core.Earley.fsequence
                (Earley_core.Earley.apply (fun f -> f [])
                   (Earley_core.Earley.fixpoint' (fun l -> l)
                      (Earley_core.Earley.fsequence_ignore
                         (Earley_core.Earley.string "," ",")
                         (Earley_core.Earley.fsequence typedef_arg
                            (Earley_core.Earley.empty
                               (fun _default_0 -> _default_0))))
                      (fun x -> fun f -> fun l -> f (List.cons x l))))
                (Earley_core.Earley.empty
                   (fun args -> fun arg -> arg :: args))))
          (List.cons
             (Earley_core.Earley.fsequence_ignore
                (Earley_core.Earley.empty ()) (Earley_core.Earley.empty []))
             [])))
let typedef = Earley_core.Earley.declare_grammar "typedef"
let _ =
  Earley_core.Earley.set_grammar typedef
    (Earley_core.Earley.fsequence ident
       (Earley_core.Earley.fsequence
          (Earley_core.Earley.option []
             (Earley_core.Earley.fsequence_ignore
                (Earley_core.Earley.string "<" "<")
                (Earley_core.Earley.fsequence typedef_args
                   (Earley_core.Earley.fsequence_ignore
                      (Earley_core.Earley.string ">" ">")
                      (Earley_core.Earley.empty
                         (fun _default_0 -> _default_0))))))
          (Earley_core.Earley.fsequence_ignore
             (Earley_core.Earley.string "\226\137\148" "\226\137\148")
             (Earley_core.Earley.fsequence type_expr
                (Earley_core.Earley.empty
                   (fun ty -> fun args -> fun id -> (id, args, ty)))))) : 
    typedef Earley.grammar)
[@@@ocaml.text " {3 Parsing of attributes} "]
type annot =
  | Annot_parameters of (ident * coq_expr) list 
  | Annot_refined_by of (ident * coq_expr) list 
  | Annot_ptr_type of (ident * type_expr) 
  | Annot_size of coq_expr 
  | Annot_exist of (ident * coq_expr) list 
  | Annot_constraint of constr list 
  | Annot_immovable 
  | Annot_tagged_union of coq_expr 
  | Annot_union_tag of tag_spec 
  | Annot_field of type_expr 
  | Annot_global of type_expr 
  | Annot_args of type_expr list 
  | Annot_requires of constr list 
  | Annot_returns of type_expr 
  | Annot_ensures of constr list 
  | Annot_annot of string 
  | Annot_inv_vars of (ident * type_expr) list 
  | Annot_annot_args of annot_arg list 
  | Annot_tactics of string list 
  | Annot_trust_me 
  | Annot_skip 
  | Annot_manual of manual_proof 
  | Annot_block 
  | Annot_full_block 
let annot_lemmas : string list -> string list =
  List.map (Printf.sprintf "all: try by apply: %s; solve_goal.")
let rc_locs : Location.Pool.t = Location.Pool.make ()
exception Invalid_annot of Location.t * string 
let invalid_annot : type a. Location.t -> string -> a =
  fun loc -> fun msg -> raise (Invalid_annot (loc, msg))
let invalid_annot_no_pos : type a. string -> a =
  fun msg -> invalid_annot (Location.none rc_locs) msg
type rc_attr =
  {
  rc_attr_id: string Location.located ;
  rc_attr_args: string Location.located list }
let parse_attr : rc_attr -> annot =
  fun attr ->
    let { rc_attr_id = id; rc_attr_args = args } = attr in
    let error msg =
      invalid_annot id.loc (Printf.sprintf "Annotation [%s] %s." id.elt msg) in
    let parse : type a. a grammar -> string Location.located -> a =
      fun gr ->
        fun s ->
          let parse_string = Earley.parse_string gr Blanks.default in
          try parse_string s.elt
          with
          | Earley.Parse_error (buf, pos) ->
              let msg =
                let i = Input.utf8_col_num buf pos in
                Printf.sprintf "No parse in annotation at position %i." i in
              invalid_annot s.loc msg in
    let single_arg : type a. a grammar -> (a -> annot) -> annot =
      fun gr ->
        fun c ->
          match args with
          | s::[] -> c (parse gr s)
          | _ -> error "should have exactly one argument" in
    let many_args : type a. a grammar -> (a list -> annot) -> annot =
      fun gr ->
        fun c ->
          match args with
          | [] -> error "should have at least one argument"
          | _ -> c (List.map (parse gr) args) in
    let raw_single_arg : (string -> annot) -> annot =
      fun c ->
        match args with
        | s::[] -> c s.elt
        | _ -> error "should have exactly one argument" in
    let raw_many_args : (string list -> annot) -> annot =
      fun c ->
        match args with
        | [] -> error "should have at least one argument"
        | _ -> c (List.map (fun a -> let open Location in a.elt) args) in
    let no_args : annot -> annot =
      fun c ->
        match args with | [] -> c | _ -> error "should not have arguments" in
    match id.elt with
    | "parameters" -> many_args annot_parameter (fun l -> Annot_parameters l)
    | "refined_by" -> many_args annot_refine (fun l -> Annot_refined_by l)
    | "ptr_type" -> single_arg annot_ptr_type (fun e -> Annot_ptr_type e)
    | "size" -> single_arg annot_size (fun e -> Annot_size e)
    | "exists" -> many_args annot_exist (fun l -> Annot_exist l)
    | "constraints" -> many_args annot_constr (fun l -> Annot_constraint l)
    | "immovable" -> no_args Annot_immovable
    | "tagged_union" ->
        single_arg tagged_union (fun e -> Annot_tagged_union e)
    | "union_tag" -> single_arg union_tag (fun t -> Annot_union_tag t)
    | "field" -> single_arg annot_field (fun e -> Annot_field e)
    | "global" -> single_arg annot_global (fun e -> Annot_global e)
    | "args" -> many_args annot_arg (fun l -> Annot_args l)
    | "requires" -> many_args annot_requires (fun l -> Annot_requires l)
    | "returns" -> single_arg annot_returns (fun e -> Annot_returns e)
    | "ensures" -> many_args annot_ensures (fun l -> Annot_ensures l)
    | "annot" -> raw_single_arg (fun e -> Annot_annot e)
    | "inv_vars" -> many_args annot_inv_var (fun l -> Annot_inv_vars l)
    | "annot_args" -> many_args annot_args (fun l -> Annot_annot_args l)
    | "tactics" -> raw_many_args (fun l -> Annot_tactics l)
    | "lemmas" -> raw_many_args (fun l -> Annot_tactics (annot_lemmas l))
    | "trust_me" -> no_args Annot_trust_me
    | "skip" -> no_args Annot_skip
    | "manual_proof" -> single_arg annot_manual (fun e -> Annot_manual e)
    | "block" -> no_args Annot_block
    | "full_block" -> no_args Annot_full_block
    | _ -> error "undefined"
[@@@ocaml.text " {3 High level parsing of attributes} "]
type proof_kind =
  | Proof_normal 
  | Proof_skipped 
  | Proof_trusted 
  | Proof_manual of manual_proof 
type function_annot =
  {
  fa_parameters: (ident * coq_expr) list ;
  fa_args: type_expr list ;
  fa_returns: type_expr ;
  fa_exists: (ident * coq_expr) list ;
  fa_requires: constr list ;
  fa_ensures: constr list ;
  fa_tactics: string list ;
  fa_proof_kind: proof_kind }
let function_annot : rc_attr list -> function_annot =
  fun attrs ->
    let parameters = ref [] in
    let args = ref [] in
    let exists = ref [] in
    let returns = ref None in
    let requires = ref [] in
    let ensures = ref [] in
    let tactics = ref [] in
    let proof = ref Proof_normal in
    let nb_attrs = ref 0 in
    let handle_attr ({ rc_attr_id = id;_} as attr) =
      let error msg =
        invalid_annot id.loc
          (Printf.sprintf "Annotation [%s] %s." id.elt msg) in
      incr nb_attrs;
      (match ((parse_attr attr), (!returns)) with
       | (_, _) when (!proof) = Proof_skipped ->
           error "a skipped function should not have other annotations"
       | (Annot_skip, _) ->
           (if (!proof) <> Proof_normal
            then error "proof mode already specified";
            if (!nb_attrs) <> 1 then error "other annotations are given";
            proof := Proof_skipped)
       | (Annot_trust_me, _) ->
           (if (!proof) <> Proof_normal
            then error "proof mode already specified";
            proof := Proof_trusted)
       | (Annot_manual cfg, _) ->
           (if (!proof) <> Proof_normal
            then error "proof mode already specified";
            proof := (Proof_manual cfg))
       | (Annot_parameters l, _) -> parameters := ((!parameters) @ l)
       | (Annot_args l, _) -> args := ((!args) @ l)
       | (Annot_returns ty, None) -> returns := (Some ty)
       | (Annot_returns _, _) -> error "already specified"
       | (Annot_requires l, _) -> requires := ((!requires) @ l)
       | (Annot_ensures l, _) -> ensures := ((!ensures) @ l)
       | (Annot_exist l, _) -> exists := ((!exists) @ l)
       | (Annot_annot_args _, _) -> ()
       | (Annot_tactics l, _) -> tactics := ((!tactics) @ l)
       | (_, _) -> error "is invalid for a function") in
    List.iter handle_attr attrs;
    if (!nb_attrs) = 0 then proof := Proof_skipped;
    {
      fa_parameters = (!parameters);
      fa_args = (!args);
      fa_returns = (Option.get (Ty_params ("void", [])) (!returns));
      fa_exists = (!exists);
      fa_requires = (!requires);
      fa_ensures = (!ensures);
      fa_tactics = (!tactics);
      fa_proof_kind = (!proof)
    }
let function_annot_args : rc_attr list -> annot_arg list =
  fun attrs ->
    let annot_args = ref [] in
    let handle_attr ({ rc_attr_id = id;_} as attr) =
      if id.elt <> "annot_args"
      then ()
      else
        (match parse_attr attr with
         | Annot_annot_args l -> annot_args := ((!annot_args) @ l)
         | _ -> assert false) in
    List.iter handle_attr attrs; !annot_args
type member_annot =
  | MA_none 
  | MA_field of type_expr 
  | MA_utag of tag_spec 
let member_annot : rc_attr list -> member_annot =
  fun attrs ->
    let annot = ref MA_none in
    let handle_attr ({ rc_attr_id = id;_} as attr) =
      let error msg =
        invalid_annot id.loc
          (Printf.sprintf "Annotation [%s] %s." id.elt msg) in
      match ((parse_attr attr), (!annot)) with
      | (Annot_field ty, MA_none) -> annot := (MA_field ty)
      | (Annot_field _, _) -> error "already specified"
      | (Annot_union_tag s, MA_none) -> annot := (MA_utag s)
      | (Annot_union_tag _, _) -> error "already specified"
      | (_, _) -> error "is invalid for a field" in
    List.iter handle_attr attrs; !annot
type expr_annot = string option
let expr_annot : rc_attr list -> expr_annot =
  fun attrs ->
    let error msg =
      invalid_annot_no_pos (Printf.sprintf "Expression annotation %s." msg) in
    match attrs with
    | [] -> None
    | _::_::_ -> error "carries more than one attributes"
    | attr::[] ->
        (match parse_attr attr with
         | Annot_annot s -> Some s
         | _ -> error "is invalid (wrong kind)")
type basic_struct_annot =
  {
  st_parameters: (ident * coq_expr) list ;
  st_refined_by: (ident * coq_expr) list ;
  st_exists: (ident * coq_expr) list ;
  st_constrs: constr list ;
  st_size: coq_expr option ;
  st_ptr_type: (ident * type_expr) option ;
  st_immovable: bool }
let default_basic_struct_annot : basic_struct_annot =
  {
    st_parameters = [];
    st_refined_by = [];
    st_exists = [];
    st_constrs = [];
    st_size = None;
    st_ptr_type = None;
    st_immovable = false
  }
type struct_annot =
  | SA_union 
  | SA_basic of basic_struct_annot 
  | SA_tagged_u of coq_expr 
let struct_annot : rc_attr list -> struct_annot =
  fun attrs ->
    let parameters = ref [] in
    let refined_by = ref [] in
    let exists = ref [] in
    let constrs = ref [] in
    let size = ref None in
    let ptr = ref None in
    let immovable = ref false in
    let tagged_union = ref None in
    let handle_attr ({ rc_attr_id = id;_} as attr) =
      let error msg =
        invalid_annot id.loc
          (Printf.sprintf "Annotation [%s] %s." id.elt msg) in
      let check_and_set r v =
        if (!r) <> None then error "already specified"; r := (Some v) in
      match ((parse_attr attr), (!tagged_union)) with
      | (Annot_tagged_union e, None) -> tagged_union := (Some e)
      | (Annot_tagged_union e, Some _) -> error "already specified"
      | (Annot_parameters l, None) -> parameters := ((!parameters) @ l)
      | (Annot_refined_by l, None) -> refined_by := ((!refined_by) @ l)
      | (Annot_exist l, None) -> exists := ((!exists) @ l)
      | (Annot_constraint l, None) -> constrs := ((!constrs) @ l)
      | (Annot_size s, None) -> check_and_set size s
      | (Annot_ptr_type e, None) -> check_and_set ptr e
      | (Annot_immovable, None) ->
          (if !immovable then error "already specified"; immovable := true)
      | (Annot_parameters _, _)|(Annot_refined_by _, _)|(Annot_exist _, _)
        |(Annot_constraint _, _)|(Annot_size _, _)|(Annot_ptr_type _, _)
        |(Annot_immovable, _) -> error "is invalid for tagged unions"
      | (_, _) -> error "is invalid for a struct or a tagged union" in
    List.iter handle_attr attrs;
    (match !tagged_union with
     | Some e -> SA_tagged_u e
     | None ->
         let basic_annot =
           {
             st_parameters = (!parameters);
             st_refined_by = (!refined_by);
             st_exists = (!exists);
             st_constrs = (!constrs);
             st_size = (!size);
             st_ptr_type = (!ptr);
             st_immovable = (!immovable)
           } in
         SA_basic basic_annot)
type loop_annot =
  {
  la_exists: (ident * coq_expr) list ;
  la_constrs: constr list ;
  la_inv_vars: (ident * type_expr) list ;
  la_full: bool }
let no_loop_annot : loop_annot =
  { la_exists = []; la_constrs = []; la_inv_vars = []; la_full = true }
let loop_annot : rc_attr list -> loop_annot =
  fun attrs ->
    let exists = ref [] in
    let constrs = ref [] in
    let vars = ref [] in
    let full_block = ref None in
    let handle_attr ({ rc_attr_id = id;_} as attr) =
      let error msg =
        invalid_annot id.loc
          (Printf.sprintf "Annotation [%s] %s." id.elt msg) in
      let set_full_block b =
        match !full_block with
        | Some _ -> error "mode already specified"
        | None -> full_block := (Some b) in
      match parse_attr attr with
      | Annot_exist l -> exists := ((!exists) @ l)
      | Annot_constraint l -> constrs := ((!constrs) @ l)
      | Annot_inv_vars l -> vars := ((!vars) @ l)
      | Annot_block -> set_full_block false
      | Annot_full_block -> set_full_block true
      | _ -> error "is invalid (wrong kind)" in
    List.iter handle_attr attrs;
    (let la_full =
       match !full_block with | Some b -> b | None -> no_loop_annot.la_full in
     {
       la_exists = (!exists);
       la_constrs = (!constrs);
       la_inv_vars = (!vars);
       la_full
     })
type global_annot =
  {
  ga_parameters: (ident * coq_expr) list ;
  ga_type: type_expr }
let global_annot : rc_attr list -> global_annot option =
  fun attrs ->
    let typ = ref None in
    let parameters = ref [] in
    let handle_attr ({ rc_attr_id = id;_} as attr) =
      let error msg =
        invalid_annot id.loc
          (Printf.sprintf "Annotation [%s] %s." id.elt msg) in
      match ((parse_attr attr), (!typ)) with
      | (Annot_global e, None) -> typ := (Some e)
      | (Annot_parameters l, _) -> parameters := ((!parameters) @ l)
      | (Annot_global _, _) -> error "already specified"
      | (_, _) -> error "is invalid for a global" in
    List.iter handle_attr attrs;
    (match !typ with
     | Some ty -> Some { ga_parameters = (!parameters); ga_type = ty }
     | None -> None)