X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=7b515472d2ef386385855a7d78abbf6543513618;hb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;hp=d00f7de7cfa065215969c7e49e55f7ccc989b20f;hpb=8a219d1957a19d666a929e9a674a5fddee10066b;p=helm.git diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index d00f7de7c..7b515472d 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -35,7 +35,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 = @@ -115,9 +116,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 ] ]; @@ -135,6 +142,9 @@ EXTEND GrafiteAst.Assumption loc | IDENT "auto"; params = auto_params -> GrafiteAst.Auto (loc,params) + | IDENT "cases"; what = tactic_term; + (num, idents) = intros_spec -> + GrafiteAst.Cases (loc, what, idents) | IDENT "clear"; ids = LIST1 IDENT -> GrafiteAst.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> @@ -147,18 +157,20 @@ 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 IDENT -> 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) @@ -182,8 +194,6 @@ EXTEND 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 @@ -210,7 +220,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 @@ -218,7 +229,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" -> @@ -244,12 +256,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 -> @@ -259,6 +271,8 @@ EXTEND | 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 -> @@ -268,8 +282,8 @@ EXTEND | 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 -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation -> - GrafiteAst.RewritingStep(loc, Some termine, 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 ] ; 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) @@ -299,9 +313,8 @@ EXTEND ] ]; 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: @@ -320,9 +333,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"; @@ -334,7 +347,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: @@ -348,12 +361,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: [ @@ -412,9 +424,15 @@ EXTEND 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 "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" ] -> GrafiteAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> GrafiteAst.WMatch (loc,t) @@ -555,6 +573,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),_,_) :: _ -> @@ -569,8 +592,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)) @@ -610,9 +639,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) ] ]; @@ -644,7 +675,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 ]