let default_precedence = 50
let default_associativity = Gramext.NonA
+type by_continuation =
+ BYC_done
+ | BYC_weproved of CicNotationPt.term * string * 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: [
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
reduction_kind: [
- [ IDENT "demodulate" -> `Demodulate
- | IDENT "normalize" -> `Normalize
+ [ IDENT "normalize" -> `Normalize
| IDENT "reduce" -> `Reduce
| IDENT "simplify" -> `Simpl
| IDENT "unfold"; t = OPT tactic_term -> `Unfold t
GrafiteAst.ApplyS (loc, t)
| IDENT "assumption" ->
GrafiteAst.Assumption loc
- | IDENT "auto";
- depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
- width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
- paramodulation = OPT [ IDENT "paramodulation" ];
- full = OPT [ IDENT "full" ] -> (* ALB *)
- GrafiteAst.Auto (loc,depth,width,paramodulation,full)
- | IDENT "clear"; id = IDENT ->
- GrafiteAst.Clear (loc,id)
+ | IDENT "auto"; params =
+ LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+ string_of_int v | v = IDENT -> v ] -> i,v ] ->
+ GrafiteAst.Auto (loc,params)
+ | IDENT "clear"; ids = LIST1 IDENT ->
+ GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
- (num, idents) = intros_spec ->
+ | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
+ idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
let types = match types with None -> [] | Some types -> types in
+ let idents = match idents with None -> [] | Some idents -> idents in
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 "elim"; what = tactic_term; using = using;
GrafiteAst.Fold (loc, kind, t, p)
| IDENT "fourier" ->
GrafiteAst.Fourier loc
- | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
+ | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.FwdSimpl (loc, hyp, idents)
| IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
| IDENT "inversion"; t = tactic_term ->
GrafiteAst.Inversion (loc, t)
| IDENT "lapply";
+ linear = OPT [ IDENT "linear" ];
depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
what = tactic_term;
to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
ident = OPT [ "as" ; ident = IDENT -> ident ] ->
- let to_what = match to_what with None -> [] | Some to_what -> to_what in
- GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ let linear = match linear with None -> false | Some _ -> true in
+ let to_what = match to_what with None -> [] | Some to_what -> to_what in
+ GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
| IDENT "left" -> GrafiteAst.Left loc
| IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
GrafiteAst.LetIn (loc, t, where)
GrafiteAst.Ring loc
| IDENT "split" ->
GrafiteAst.Split loc
+ | IDENT "subst" ->
+ GrafiteAst.Subst loc
| IDENT "symmetry" ->
GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
GrafiteAst.Transitivity (loc, t)
+ (* 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']->
+ GrafiteAst.Suppose (loc, t, id, t1)
+ | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
+ cont=by_continuation ->
+ let t' = match t with LNone _ -> None | LSome t -> Some t in
+ (match cont with
+ BYC_done -> GrafiteAst.Bydone (loc, t')
+ | BYC_weproved (ty,id,t1) ->
+ GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
+ | BYC_letsuchthat (id1,t1,id2,t2) ->
+ (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error
+ "tactic_term expected here"))
+ | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+ | BYC_wehaveand (id1,t1,id2,t2) ->
+ (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (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']->
+ 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 "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.Byinduction(loc, t, id)
+ | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
+ GrafiteAst.Thesisbecomes(loc, t)
+ | 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 ->
+ GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+ ]
+];
+ 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 "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)
]
- ];
+];
+ rewriting_step_continuation : [
+ [ IDENT "done" -> None
+ | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
+ | -> Some Cic.Anonymous
+ ]
+];
atomic_tactical:
[ "sequence" LEFTA
[ t1 = SELF; SYMBOL ";"; t2 = SELF ->
| 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)
]
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 "quit" ] -> GrafiteAst.Quit loc
-(* | [ IDENT "abort" ] -> GrafiteAst.Abort loc *)
-(* | [ IDENT "undo" ]; steps = OPT NUMBER ->
- GrafiteAst.Undo (loc, int_opt steps)
- | [ IDENT "redo" ]; steps = OPT NUMBER ->
- GrafiteAst.Redo (loc, int_opt steps) *)
- | [ IDENT "check" ]; t = term ->
+ [ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WElim (loc, t)
| [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
GrafiteAst.WHint (loc,t)
- | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
]
];
alias_spec: [
IDENT "set"; n = QSTRING; v = QSTRING ->
GrafiteAst.Set (loc, n, v)
| IDENT "drop" -> GrafiteAst.Drop loc
+ | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
| IDENT "qed" -> GrafiteAst.Qed loc
| IDENT "variant" ; name = IDENT; SYMBOL ":";
typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
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 ->
fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
fun ~include_paths status ->
- let path = DependenciesParser.baseuri_of_script ~include_paths fname in
+ let buri, fullpath =
+ DependenciesParser.baseuri_of_script ~include_paths fname
+ in
let status =
- LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode))
+ LexiconEngine.eval_command status
+ (LexiconAst.Include (iloc,buri,mode,fullpath))
in
status,
LSome
(GrafiteAst.Executable
(loc,GrafiteAst.Command
- (loc,GrafiteAst.Include (iloc,path))))
+ (loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
fun ~include_paths status ->
let status = LexiconEngine.eval_command status scom in
projects / helm.git / blobdiff