+ theorem_flavour: [
+ [ [ IDENT "definition" ] -> `Definition
+ | [ IDENT "fact" ] -> `Fact
+ | [ IDENT "lemma" ] -> `Lemma
+ | [ IDENT "remark" ] -> `Remark
+ | [ IDENT "theorem" ] -> `Theorem
+ ]
+ ];
+ inductive_spec: [ [
+ fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
+ SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
+ fst_constructors = LIST0 constructor SEP SYMBOL "|";
+ tl = OPT [ "with";
+ types = LIST1 [
+ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
+ OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
+ (name, true, typ, constructors) ] SEP "with" -> types
+ ] ->
+ let params =
+ List.fold_right
+ (fun (names, typ) acc ->
+ (List.map (fun name -> (name, typ)) names) @ acc)
+ params []
+ in
+ let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
+ let tl_ind_types = match tl with None -> [] | Some types -> types in
+ let ind_types = fst_ind_type :: tl_ind_types in
+ (params, ind_types)
+ ] ];
+
+ record_spec: [ [
+ name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+ SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; PAREN "{" ;
+ fields = LIST0 [
+ name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty)
+ ] SEP SYMBOL ";"; PAREN "}" ->
+ let params =
+ List.fold_right
+ (fun (names, typ) acc ->
+ (List.map (fun name -> (name, typ)) names) @ acc)
+ params []
+ in
+ (params,name,typ,fields)
+ ] ];
+
+ macro: [
+ [ [ IDENT "quit" ] -> TacticAst.Quit loc
+(* | [ IDENT "abort" ] -> TacticAst.Abort loc *)
+ | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
+(* | [ IDENT "undo" ]; steps = OPT NUM ->
+ TacticAst.Undo (loc, int_opt steps)
+ | [ IDENT "redo" ]; steps = OPT NUM ->
+ TacticAst.Redo (loc, int_opt steps) *)
+ | [ IDENT "check" ]; t = term ->
+ TacticAst.Check (loc, t)
+ | [ IDENT "hint" ] -> TacticAst.Hint loc
+ | [ IDENT "whelp"; "match" ] ; t = term ->
+ TacticAst.WMatch (loc,t)
+ | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
+ TacticAst.WInstance (loc,t)
+ | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT ->
+ TacticAst.WLocate (loc,id)
+ | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
+ TacticAst.WElim (loc, t)
+ | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
+ TacticAst.WHint (loc,t)
+ | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
+ ]
+ ];
+
+ alias_spec: [
+ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
+ let alpha = "[a-zA-Z]" in
+ let num = "[0-9]+" in
+ let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
+ let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
+ let rex = Str.regexp ("^"^ident^"$") in
+ if Str.string_match rex id 0 then
+ let rex = Str.regexp
+ ("^\\(cic:/\\|theory:/\\)"^ident^
+ "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^
+ "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$")
+ in
+ if Str.string_match rex uri 0 then
+ TacticAst.Ident_alias (id, uri)
+ else
+ raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri))
+ else
+ raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id))
+ | IDENT "symbol"; symbol = QSTRING;
+ instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
+ SYMBOL "="; dsc = QSTRING ->
+ let instance =
+ match instance with Some i -> int_of_string i | None -> 0
+ in
+ TacticAst.Symbol_alias (symbol, instance, dsc)
+ | IDENT "num";
+ instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
+ SYMBOL "="; dsc = QSTRING ->
+ let instance =
+ match instance with Some i -> int_of_string i | None -> 0
+ in
+ TacticAst.Number_alias (instance, dsc)
+ ]
+ ];
+
+ command: [[
+ [ IDENT "set" ]; n = QSTRING; v = QSTRING ->
+ TacticAst.Set (loc, n, v)
+ | [ IDENT "qed" ] -> TacticAst.Qed loc
+ | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))
+ | flavour = theorem_flavour; name = IDENT;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body))
+ | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
+ defs = let_defs ->
+ let name,ty =
+ match defs with
+ | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
+ | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
+ | _ -> assert false
+ in
+ let body = CicAst.Ident (name,None) in
+ TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty,
+ Some (CicAst.LetRec (ind_kind, defs, body))))
+
+ | [ IDENT "inductive" ]; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
+ | [ IDENT "coinductive" ]; spec = inductive_spec ->
+ let (params, ind_types) = spec in
+ let ind_types = (* set inductive flags to false (coinductive) *)
+ List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
+ ind_types
+ in
+ TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
+ | [ IDENT "coercion" ] ; name = IDENT ->
+ TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
+ | [ IDENT "coercion" ] ; name = URI ->
+ TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
+ | [ IDENT "alias" ]; spec = alias_spec ->
+ TacticAst.Alias (loc, spec)
+ | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
+ TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields))
+ ]];
+
+ executable: [
+ [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
+ | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
+ | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)
+ ]
+ ];
+
+ comment: [
+ [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
+ TacticAst.Code (loc, ex)
+ | str = NOTE ->
+ TacticAst.Note (loc, str)
+ ]
+ ];
+
+ statement: [
+ [ ex = executable -> TacticAst.Executable (loc,ex)
+ | com = comment -> TacticAst.Comment (loc, com)
+ ]
+ ];
+ statements: [
+ [ l = LIST0 [ statement ] -> l
+ ]
+ ];