X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=17144a85244a40cea868499ac3ce36c1fb535059;hb=7dbc6d6fe71f6967f5ad31528a629dc89e6d8160;hp=2d37892217407440aac8957ee8c9029ff1bc9613;hpb=77d56df4d446307199a9d4e03478260c6c63baf8;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 2d3789221..17144a852 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/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 @@ -64,7 +65,11 @@ EXTEND GLOBAL: term statement; 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 ] ]; @@ -140,11 +145,11 @@ EXTEND GrafiteAst.ApplyS (loc, t, params) | IDENT "assumption" -> GrafiteAst.Assumption loc - | IDENT "auto"; params = auto_params -> - GrafiteAst.Auto (loc,params) + | IDENT "autobatch"; params = auto_params -> + GrafiteAst.AutoBatch (loc,params) | IDENT "cases"; what = tactic_term; - (num, idents) = intros_spec -> - GrafiteAst.Cases (loc, what, idents) + specs = intros_spec -> + GrafiteAst.Cases (loc, what, specs) | IDENT "clear"; ids = LIST1 IDENT -> GrafiteAst.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> @@ -157,21 +162,23 @@ EXTEND 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) + GrafiteAst.Decompose (loc, idents) | IDENT "demodulate" -> GrafiteAst.Demodulate loc | 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 "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" -> @@ -187,19 +194,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 "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"; @@ -256,12 +261,12 @@ EXTEND | BYC_weproved (ty,id,t1) -> GrafiteAst.By_term_we_proved(loc, t', ty, id, t1) | BYC_letsuchthat (id1,t1,id2,t2) -> - (match t with + (* (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)) + | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*) | BYC_wehaveand (id1,t1,id2,t2) -> (match t with LNone floc -> @@ -333,9 +338,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"; @@ -347,7 +352,7 @@ EXTEND 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: @@ -361,12 +366,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: [ @@ -435,6 +439,8 @@ EXTEND let prefix = match prefix with None -> "" | Some prefix -> prefix in GrafiteAst.Inline (loc,style,suri,prefix) | [ IDENT "hint" ] -> GrafiteAst.Hint loc + | IDENT "auto"; params = auto_params -> + GrafiteAst.AutoInteractive (loc,params) | [ IDENT "whelp"; "match" ] ; t = term -> GrafiteAst.WMatch (loc,t) | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> @@ -461,10 +467,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 -> @@ -502,11 +508,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)) ] -> @@ -574,6 +580,11 @@ 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 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ -> @@ -588,8 +599,14 @@ EXTEND | _ -> 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)) @@ -629,9 +646,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) ] ]; @@ -649,13 +668,14 @@ EXTEND fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ~include_paths status -> - let buri, fullpath = + let buri, fullpath = DependenciesParser.baseuri_of_script ~include_paths fname in let status = LexiconEngine.eval_command status (LexiconAst.Include (iloc,buri,mode,fullpath)) in + !out fname; status, LSome (GrafiteAst.Executable @@ -663,7 +683,7 @@ EXTEND (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 ]