type by_continuation =
BYC_done
- | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option
+ | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
| BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
| BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
EXTEND
GLOBAL: term statement;
- arg: [
- [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
- SYMBOL ":"; ty = term; RPAREN -> names,ty
- | name = IDENT -> [name],Ast.Implicit
- ]
- ];
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
- | IDENT "applyS"; t = tactic_term ->
- GrafiteAst.ApplyS (loc, t)
+ | IDENT "applyS"; t = tactic_term ; params =
+ LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+ string_of_int v | v = IDENT -> v ] -> i,v ] ->
+ GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
GrafiteAst.Assumption loc
| IDENT "auto"; params =
(floc,CicNotationParser.Parse_error
"tactic_term expected here"))
| LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
- | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
GrafiteAst.We_need_to_prove (loc, t, id, t1)
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
]
];
by_continuation: [
- [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,id,t1)
+ [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
+ | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
+ IDENT "done" -> BYC_weproved (ty,None,t1)
| IDENT "done" -> BYC_done
| "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
- IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ;
- RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
- | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;
- "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
- BYC_wehaveand (id1,t1,id2,t2)
+ IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
+ | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
+ BYC_wehaveand (id1,t1,id2,t2)
]
];
rewriting_step_continuation : [
]
];
inductive_spec: [ [
- fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
+ fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
fst_constructors = LIST0 constructor SEP SYMBOL "|";
tl = OPT [ "with";
] ];
record_spec: [ [
- name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+ name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
fields = LIST0 [
name = IDENT ;
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
+ | [ IDENT "inline"]; suri = QSTRING ->
+ GrafiteAst.Inline (loc,suri)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WMatch (loc,t)
defs = CicNotationParser.let_defs ->
let name,ty =
match defs with
- | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
- | ((Ast.Ident (name, None), None),_,_) :: _ ->
+ | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
+ let ty =
+ List.fold_right
+ (fun var ty -> Ast.Binder (`Pi,var,ty)
+ ) params ty
+ in
+ name,ty
+ | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
name, Ast.Implicit
| _ -> assert false
in
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
let uris = List.map UriManager.uri_of_string uris in
GrafiteAst.Default (loc,what,uris)
+ | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
+ refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
+ refl = tactic_term -> refl ] ;
+ sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
+ sym = tactic_term -> sym ] ;
+ trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
+ trans = tactic_term -> trans ] ;
+ "as" ; id = IDENT ->
+ GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
]];
lexicon_command: [ [
IDENT "alias" ; spec = alias_spec ->