let macro = Grammar.Entry.create grammar "macro"
let script = Grammar.Entry.create grammar "script"
let statement = Grammar.Entry.create grammar "statement"
+let statements = Grammar.Entry.create grammar "statements"
let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
vars body
EXTEND
- GLOBAL: term term0 statement;
+ GLOBAL: term term0 statement statements;
int: [
[ num = NUM ->
try
]
];
subst: [
- [ subst = OPT [
- SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
- PAREN "[";
- substs = LIST1 [
- i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
- ] SEP SYMBOL ";";
- PAREN "]" ->
- substs
- ] -> subst
+ [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
+ PAREN "[";
+ substs = LIST1 [
+ i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
+ ] SEP SYMBOL ";";
+ PAREN "]" ->
+ substs
]
];
substituted_name: [ (* a subs.name is an explicit substitution subject *)
- [ s = IDENT; subst = subst -> CicAst.Ident (s, subst)
- | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst)
+ [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst)
+ | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst)
]
];
name: [ (* as substituted_name with no explicit substitution *)
(head, vars)
]
];
+ arg: [
+ [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+ SYMBOL ":"; ty = term; PAREN ")" -> names,ty
+ | name = IDENT -> [name],CicAst.Implicit
+ ]
+ ];
let_defs:[
[ defs = LIST1 [
name = IDENT;
- args = LIST1 [
- PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
- ty = term; PAREN ")" ->
- (names, ty)
- ];
+ args = LIST1 [arg = arg -> arg];
index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
ty = OPT [ SYMBOL ":" ; t = term -> t ];
SYMBOL <:unicode<def>> (* ≝ *);
b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
let binder = mk_binder_ast b typ vars body in
return_term loc binder
+ | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ let binder = mk_binder_ast b typ vars body in
+ return_term loc binder
| t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
in
CicAst.Appl (aux t1 @ [t2])
]
- | "binder" RIGHTA
- [
- b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
- let binder = mk_binder_ast b typ vars body in
- return_term loc binder
- ]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort
| n = substituted_name -> return_term loc n
| i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
| IMPLICIT -> return_term loc CicAst.Implicit
+ | PLACEHOLDER -> return_term loc CicAst.UserInput
| m = META;
substs = [
PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
return_term loc (CicAst.Meta (index, substs))
| outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
"match"; t = term;
- indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
+ indty_ident = OPT ["in" ; id = IDENT -> id ];
"with";
PAREN "[";
patterns = LIST0 [
reduction_kind: [
[ [ IDENT "reduce" ] -> `Reduce
| [ IDENT "simplify" ] -> `Simpl
- | [ IDENT "whd" ] -> `Whd ]
+ | [ IDENT "whd" ] -> `Whd
+ | [ IDENT "normalize" ] -> `Normalize ]
];
tactic: [
[ [ IDENT "absurd" ]; t = tactic_term ->
TacticAst.Apply (loc, t)
| [ IDENT "assumption" ] ->
TacticAst.Assumption loc
- | [ IDENT "auto" ] -> TacticAst.Auto loc
+ | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] ->
+ TacticAst.Auto (loc,num)
| [ IDENT "change" ];
t1 = tactic_term; "with"; t2 = tactic_term;
where = tactic_where ->
| [ IDENT "fourier" ] ->
TacticAst.Fourier loc
| IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n)
- | [ IDENT "hint" ] -> TacticAst.Hint loc
| [ IDENT "injection" ]; ident = IDENT ->
TacticAst.Injection (loc, ident)
| [ IDENT "intros" ];
let idents = match idents with None -> [] | Some idents -> idents in
TacticAst.Intros (loc, num, idents)
| [ IDENT "intro" ] ->
- TacticAst.Intros (loc, None, [])
+ TacticAst.Intros (loc, Some 1, [])
| [ IDENT "left" ] -> TacticAst.Left loc
- | [ "let" | "Let" ];
- t = tactic_term; "in"; where = IDENT ->
+ | [ IDENT "letin" ];
+ where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
TacticAst.LetIn (loc, t, where)
| kind = reduction_kind;
pat = OPT [
(match (pat, terms) with
| None, [] -> TacticAst.Reduce (loc, kind, None)
| None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
- | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+ | Some pat, [] -> fail loc "Missing term [list]"
| Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+ | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term ->
+ TacticAst.ReduceAt (loc, kind, where, pat)
| [ IDENT "reflexivity" ] ->
TacticAst.Reflexivity loc
| [ IDENT "replace" ];
t1 = tactic_term; "with"; t2 = tactic_term ->
TacticAst.Replace (loc, t1, t2)
- (* TODO Rewrite *)
+ | [ IDENT "rewrite" ; IDENT "left" ] ; t = term ->
+ TacticAst.Rewrite (loc,`Left, t, None)
+ | [ IDENT "rewrite" ; IDENT "right" ] ; t = term ->
+ TacticAst.Rewrite (loc,`Right, t, None)
(* TODO Replace_pattern *)
| [ IDENT "right" ] -> TacticAst.Right loc
| [ IDENT "ring" ] -> TacticAst.Ring loc
| [ IDENT "transitivity" ];
t = tactic_term ->
TacticAst.Transitivity (loc, t)
+ | [ IDENT "fwd" ]; name = IDENT ->
+ TacticAst.FwdSimpl (loc, name)
+ | [ IDENT "lapply" ]; t = term ->
+ TacticAst.LApply (loc, t, [])
]
];
tactical:
]
];
inductive_spec: [ [
- fst_name = IDENT; params = LIST0 [
- PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
- typ = term; PAREN ")" -> (names, typ) ];
+ 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";
let ind_types = fst_ind_type :: tl_ind_types in
(params, ind_types)
] ];
-
- macro: [[
- [ IDENT "abort" ] -> TacticAst.Abort loc
- | [ IDENT "quit" ] -> TacticAst.Quit loc
+
+ 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 ->
+(* | [ IDENT "undo" ]; steps = OPT NUM ->
TacticAst.Undo (loc, int_opt steps)
| [ IDENT "redo" ]; steps = OPT NUM ->
- TacticAst.Redo (loc, int_opt steps)
+ 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 ->
[ IDENT "set" ]; n = QSTRING; v = QSTRING ->
TacticAst.Set (loc, n, v)
| [ IDENT "qed" ] -> TacticAst.Qed loc
- | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+ | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
- TacticAst.Theorem (loc, flavour, name, typ, 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),_,_) :: _ ->
- fail loc ("No type given for " ^ name)
+ | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
| _ -> assert false
in
let body = CicAst.Ident (name,None) in
- TacticAst.Theorem(loc, `Definition, Some name, ty,
- Some (CicAst.LetRec (ind_kind, defs, body)))
+ 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.Inductive (loc, params, ind_types)
+ 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.Inductive (loc, params, ind_types)
+ 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))
]];
- statement: [
+ 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
+ ]
+ ];
END
let exc_located_wrapper f =
exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
let parse_statement stream =
exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statements stream =
+ exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
+
(**/**)
projects / helm.git / blobdiff