X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=378931c1471829b0a62bd5349b0db4d351458acf;hb=6beda5aa100b617b75d88a5a519b5022c99208a0;hp=10a841e2eae14e01db81a03147ca3ace7ebb8bfe;hpb=3990759a81db3ce45bf4ec56e1985e532151f6e0;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 10a841e2e..378931c14 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -30,6 +30,8 @@ let set_callback f = out := f module Ast = CicNotationPt +exception NoInclusionPerformed of string (* full path *) + type 'a localized_option = LSome of 'a | LNone of GrafiteAst.loc @@ -41,6 +43,7 @@ type ast_statement = GrafiteAst.statement type statement = + ?never_include:bool -> include_paths:string list -> LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option @@ -75,7 +78,6 @@ EXTEND ]; reduction_kind: [ [ IDENT "normalize" -> `Normalize - | IDENT "reduce" -> `Reduce | IDENT "simplify" -> `Simpl | IDENT "unfold"; t = OPT tactic_term -> `Unfold t | IDENT "whd" -> `Whd ] @@ -156,9 +158,10 @@ EXTEND GrafiteAst.ClearBody (loc,id) | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Change (loc, what, t) - | IDENT "compose"; t1 = tactic_term; t2 = tactic_term; - specs = intros_spec -> - GrafiteAst.Compose (loc, t1, t2, specs) + | 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" -> @@ -169,8 +172,8 @@ EXTEND let idents = match idents with None -> [] | Some idents -> idents in GrafiteAst.Decompose (loc, idents) | IDENT "demodulate" -> GrafiteAst.Demodulate loc - | IDENT "destruct"; t = tactic_term -> - GrafiteAst.Destruct (loc, t) + | 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 -> @@ -245,8 +248,6 @@ EXTEND GrafiteAst.Ring loc | IDENT "split" -> GrafiteAst.Split loc - | IDENT "subst" -> - GrafiteAst.Subst loc | IDENT "symmetry" -> GrafiteAst.Symmetry loc | IDENT "transitivity"; t = tactic_term -> @@ -290,11 +291,28 @@ EXTEND | 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 ] ; 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) + | 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: [ @@ -441,7 +459,8 @@ EXTEND in let prefix = match prefix with None -> "" | Some prefix -> prefix in GrafiteAst.Inline (loc,style,suri,prefix) - | [ IDENT "hint" ] -> GrafiteAst.Hint loc + | [ 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 -> @@ -620,9 +639,13 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI ; arity = OPT int -> + | 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 - GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity) + 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 -> @@ -666,17 +689,18 @@ EXTEND ]; statement: [ [ ex = executable -> - fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) + fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) | com = comment -> - fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) + fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> - fun ~include_paths status -> - let buri, fullpath = - DependenciesParser.baseuri_of_script ~include_paths fname + fun ?(never_include=false) ~include_paths status -> + let _root, buri, fullpath, _rrelpath = + Librarian.baseuri_of_script ~include_paths fname in let status = - LexiconEngine.eval_command status - (LexiconAst.Include (iloc,buri,mode,fullpath)) + if never_include then raise (NoInclusionPerformed fullpath) + else LexiconEngine.eval_command status + (LexiconAst.Include (iloc,buri,mode,fullpath)) in !out fname; status, @@ -685,7 +709,7 @@ EXTEND (loc,GrafiteAst.Command (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> - fun ~include_paths status -> + fun ?(never_include=false) ~include_paths status -> let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file @@ -707,3 +731,4 @@ let exc_located_wrapper f = let parse_statement lexbuf = exc_located_wrapper (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf))) +