X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=50a373e49bf8b8389d0aad6836d2459c17f59a30;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=ccff1fab1d3560cd46e2f2a4d3927259418ae747;hpb=f68f452173a5077c58f93587faad65fcced77223;p=helm.git diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index ccff1fab1..50a373e49 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -25,7 +25,8 @@ (* $Id$ *) -open Printf +let out = ref ignore +let set_callback f = out := f module Ast = CicNotationPt @@ -35,7 +36,8 @@ type 'a localized_option = type ast_statement = (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, + CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement type statement = @@ -53,23 +55,26 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) let default_precedence = 50 let default_associativity = Gramext.NonA +type by_continuation = + BYC_done + | 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 ] ]; + new_name: [ + [ id = IDENT -> Some id + | SYMBOL "_" -> None ] + ]; + ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ]; tactic_term_list1: [ [ 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 @@ -116,9 +121,15 @@ EXTEND | SYMBOL "<" -> `RightToLeft ] ]; int: [ [ num = NUMBER -> int_of_string num ] ]; + intros_names: [ + [ idents = OPT ident_list0 -> + match idents with None -> [] | Some idents -> idents + ] + ]; intros_spec: [ - [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in + [ OPT [ IDENT "names" ]; + num = OPT [ num = int -> num ]; + idents = intros_names -> num, idents ] ]; @@ -128,40 +139,50 @@ EXTEND 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.Auto (loc,params) + GrafiteAst.ApplyS (loc, t, params) + | IDENT "assumption" -> + GrafiteAst.Assumption loc + | IDENT "autobatch"; params = auto_params -> + GrafiteAst.AutoBatch (loc,params) + | IDENT "cases"; what = tactic_term; + specs = intros_spec -> + GrafiteAst.Cases (loc, what, specs) | 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.Change (loc, what, t) + | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = + OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec -> + let times = match times with None -> 1 | Some i -> i in + GrafiteAst.Compose (loc, t1, t2, times, specs) | IDENT "constructor"; n = int -> GrafiteAst.Constructor (loc, n) | IDENT "contradiction" -> 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 = OPT IDENT; - idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> - let types = match types with None -> [] | Some types -> types in + | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] -> 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 "discriminate"; t = tactic_term -> - GrafiteAst.Discriminate (loc, t) - | IDENT "elim"; what = tactic_term; using = using; - (num, idents) = intros_spec -> - GrafiteAst.Elim (loc, what, using, num, idents) + GrafiteAst.Decompose (loc, idents) + | IDENT "demodulate" -> GrafiteAst.Demodulate loc + | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] -> + GrafiteAst.Destruct (loc, xts) + | IDENT "elim"; what = tactic_term; using = using; + pattern = OPT pattern_spec; + (num, idents) = intros_spec -> + let pattern = match pattern with + | None -> None, [], Some Ast.UserInput + | Some pattern -> pattern + in + GrafiteAst.Elim (loc, what, using, pattern, (num, idents)) | IDENT "elimType"; what = tactic_term; using = using; (num, idents) = intros_spec -> - GrafiteAst.ElimType (loc, what, using, num, idents) + GrafiteAst.ElimType (loc, what, using, (num, idents)) | IDENT "exact"; t = tactic_term -> GrafiteAst.Exact (loc, t) | IDENT "exists" -> @@ -177,21 +198,17 @@ EXTEND GrafiteAst.Fold (loc, kind, t, p) | IDENT "fourier" -> GrafiteAst.Fourier loc - | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> + | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> 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] -> GrafiteAst.Generalize (loc,p,id) - | 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) - | IDENT "intros"; (num, idents) = intros_spec -> - GrafiteAst.Intros (loc, num, idents) + let idents = match ident with None -> [] | Some id -> [Some id] in + GrafiteAst.Intros (loc, (Some 1, idents)) + | IDENT "intros"; specs = intros_spec -> + GrafiteAst.Intros (loc, specs) | IDENT "inversion"; t = tactic_term -> GrafiteAst.Inversion (loc, t) | IDENT "lapply"; @@ -212,7 +229,8 @@ EXTEND GrafiteAst.Reflexivity loc | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Replace (loc, p, t) - | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> + | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec; + xnames = OPT [ "as"; n = ident_list0 -> n ] -> let (pt,_,_) = p in if pt <> None then raise @@ -220,7 +238,8 @@ EXTEND (CicNotationParser.Parse_error "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) else - GrafiteAst.Rewrite (loc, d, t, p) + let n = match xnames with None -> [] | Some names -> names in + GrafiteAst.Rewrite (loc, d, t, p, n) | IDENT "right" -> GrafiteAst.Right loc | IDENT "ring" -> @@ -231,8 +250,97 @@ EXTEND 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 ; 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 "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + GrafiteAst.We_proceed_by_cases_on (loc, t, 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) + | 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 + | IDENT "proof" -> `Proof] ; + 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 + | IDENT "proof" -> `Proof] ; + 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,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) ] - ]; +]; + rewriting_step_continuation : [ + [ IDENT "done" -> true + | -> false + ] +]; atomic_tactical: [ "sequence" LEFTA [ t1 = SELF; SYMBOL ";"; t2 = SELF -> @@ -249,9 +357,9 @@ EXTEND (GrafiteAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA - [ IDENT "do"; count = int; tac = SELF; IDENT "end" -> + [ IDENT "do"; count = int; tac = SELF -> GrafiteAst.Do (loc, count, tac) - | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac) + | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac) ] | "simple" NONA [ IDENT "first"; @@ -261,8 +369,9 @@ EXTEND | 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) + | tac = tactic -> tac ] ]; punctuation_tactical: @@ -276,12 +385,11 @@ EXTEND | SYMBOL "." -> GrafiteAst.Dot loc ] ]; - tactical: + non_punctuation_tactical: [ "simple" NONA [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals) | IDENT "unfocus" -> GrafiteAst.Unfocus loc | IDENT "skip" -> GrafiteAst.Skip loc - | tac = atomic_tactical LEVEL "loops" -> tac ] ]; theorem_flavour: [ @@ -293,7 +401,7 @@ EXTEND ] ]; 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>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; @@ -315,12 +423,18 @@ EXTEND ] ]; record_spec: [ [ - name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ; SYMBOL ":"; typ = term; SYMBOL <:unicode>; 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 @@ -332,15 +446,21 @@ EXTEND ] ]; 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 "inline"]; + style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; + suri = QSTRING; prefix = OPT QSTRING -> + let style = match style with + | None -> GrafiteAst.Declarative + | Some depth -> GrafiteAst.Procedural depth + in + let prefix = match prefix with None -> "" | Some prefix -> prefix in + GrafiteAst.Inline (loc,style,suri,prefix) + | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> + if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true) + | IDENT "auto"; params = auto_params -> + GrafiteAst.AutoInteractive (loc,params) | [ IDENT "whelp"; "match" ] ; t = term -> GrafiteAst.WMatch (loc,t) | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> @@ -351,7 +471,6 @@ EXTEND GrafiteAst.WElim (loc, t) | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> GrafiteAst.WHint (loc,t) - | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name) ] ]; alias_spec: [ @@ -368,10 +487,10 @@ EXTEND LexiconAst.Ident_alias (id, uri) else raise - (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri))) + (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri))) else raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( - sprintf "Not a valid identifier: %s" id))) + Printf.sprintf "Not a valid identifier: %s" id))) | IDENT "symbol"; symbol = QSTRING; instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; SYMBOL "="; dsc = QSTRING -> @@ -409,11 +528,11 @@ EXTEND IDENT "for"; p2 = [ blob = UNPARSED_AST -> - add_raw_attribute ~text:(sprintf "@{%s}" blob) + add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob) (CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string blob)) | blob = UNPARSED_META -> - add_raw_attribute ~text:(sprintf "${%s}" blob) + add_raw_attribute ~text:(Printf.sprintf "${%s}" blob) (CicNotationParser.parse_level2_meta (Ulexing.from_utf8_string blob)) ] -> @@ -463,6 +582,7 @@ EXTEND 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> ; newname = IDENT -> @@ -480,16 +600,33 @@ EXTEND GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = CicNotationParser.let_defs -> + (* In case of mutual definitions here we produce just + the syntax tree for the first one. The others will be + generated from the completely specified term just before + insertion in the environment. We use the flavour + `MutualDefinition to rememer this. *) 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 let body = Ast.Ident (name,None) in - GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty, - Some (Ast.LetRec (ind_kind, defs, body)))) + let flavour = + if List.length defs = 1 then + `Definition + else + `MutualDefinition + in + GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty, + Some (Ast.LetRec (ind_kind, defs, body)))) | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) @@ -500,13 +637,27 @@ EXTEND 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 ; + saturations = OPT int; composites = OPT (IDENT "nocomposites") -> + let arity = match arity with None -> 0 | Some x -> x in + let saturations = match saturations with None -> 0 | Some x -> x in + let composites = match composites with None -> true | Some _ -> false in + GrafiteAst.Coercion + (loc, UriManager.uri_of_string suri, composites, arity, saturations) | 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 -> @@ -519,9 +670,11 @@ EXTEND ]]; executable: [ [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) - | tac = tactical; punct = punctuation_tactical -> - GrafiteAst.Tactical (loc, tac, Some punct) - | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None) + | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical -> + GrafiteAst.Tactic (loc, Some tac, punct) + | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct) + | tac = non_punctuation_tactical; punct = punctuation_tactical -> + GrafiteAst.NonPunctuationTactical (loc, tac, punct) | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) ] ]; @@ -539,18 +692,22 @@ EXTEND 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 + !out fname; 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 + let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file ]