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 "assumption" ->
- GrafiteAst.Assumption loc
- | IDENT "auto"; params =
+ | 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 = auto_params ->
GrafiteAst.Auto (loc,params)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
let to_spec id = GrafiteAst.Ident id in
GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
- | IDENT "discriminate"; t = tactic_term ->
- GrafiteAst.Discriminate (loc, t)
+ | IDENT "destruct"; t = tactic_term ->
+ GrafiteAst.Destruct (loc, t)
| IDENT "elim"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.Elim (loc, what, using, num, idents)
| IDENT "goal"; n = int ->
GrafiteAst.Goal (loc, n)
| IDENT "id" -> GrafiteAst.IdTac loc
- | IDENT "injection"; t = tactic_term ->
- GrafiteAst.Injection (loc, t)
| IDENT "intro"; ident = OPT IDENT ->
let idents = match ident with None -> [] | Some id -> [id] in
GrafiteAst.Intros (loc, Some 1, idents)
GrafiteAst.Ring loc
| IDENT "split" ->
GrafiteAst.Split loc
+ | IDENT "subst" ->
+ GrafiteAst.Subst loc
| IDENT "symmetry" ->
GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
(* Produzioni Aggiunte *)
| IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
GrafiteAst.Assume (loc, id, t)
- | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']->
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
GrafiteAst.Suppose (loc, t, id, t1)
| IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
cont=by_continuation ->
(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)
| IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
GrafiteAst.Case(loc,id,params)
- | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
- | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
+ | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
+ | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
+ cont=rewriting_step_continuation ->
GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
]
+];
+ auto_params: [
+ [ params =
+ LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+ string_of_int v | v = IDENT -> v ] -> i,v ] ->
+ params
+ ]
+];
+ auto_params': [
+ [ LPAREN; params = auto_params; RPAREN -> params
+ | -> []
+ ]
];
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 : [
- [ IDENT "done" -> None
- | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
- | -> Some Cic.Anonymous
+ [ IDENT "done" -> true
+ | -> false
]
];
atomic_tactical:
| IDENT "solve";
SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
GrafiteAst.Solve (loc, tacs)
+ | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
| LPAREN; tac = SELF; RPAREN -> tac
| tac = tactic -> GrafiteAst.Tactic (loc, tac)
]
]
];
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 ;
- coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ;
- ty = term -> (name,ty,coercion)
+ coercion = [
+ SYMBOL ":" -> false,0
+ | SYMBOL ":"; SYMBOL ">" -> true,0
+ | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
+ ];
+ ty = term ->
+ let b,n = coercion in
+ (name,ty,b,n)
] SEP SYMBOL ";"; SYMBOL "}" ->
let params =
List.fold_right
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
+ | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
+ let prefix = match prefix with None -> "" | Some prefix -> prefix in
+ GrafiteAst.Inline (loc,suri,prefix)
| [ 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
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ->
- GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
+ | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+ let arity = match arity with None -> 0 | Some x -> x in
+ GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| 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 ->
projects / helm.git / blobdiff