X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=d3d6e28aebcbb4377d9ad343774b89b16b4ba601;hb=aa0c24992572f26d8e78ae34b60c7e151167cf49;hp=a7d43bb45f75461cda893201a49459bc458f0dda;hpb=2dde94202f728a388eabd91018d71c0bce0708cb;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index a7d43bb45..d3d6e28ae 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -53,9 +53,9 @@ let fresh_num_instance = else (fun () -> 0) -let choice_of_uri uri = - let term = CicUtil.term_of_uri uri in - (uri, (fun _ _ _ -> term)) +let choice_of_uri suri = + let term = CicUtil.term_of_uri (UriManager.uri_of_string suri) in + (suri, (fun _ _ _ -> term)) let grammar = Grammar.gcreate cic_lexer @@ -312,22 +312,33 @@ EXTEND | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; - tactic_where: [ - [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] - ]; tactic_term: [ [ t = term -> t ] ]; ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; - ident_list1: [ - [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] - ]; reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl | [ IDENT "whd" ] -> `Whd | [ IDENT "normalize" ] -> `Normalize ] ]; + pattern_spec: [ + [ "in"; + hyp_paths = + LIST0 + [ id = IDENT ; + path = OPT [SYMBOL ":" ; path = term -> path ] -> + (id,match path with Some p -> p | None -> CicAst.UserInput) ] + SEP SYMBOL ";"; + goal_path = OPT [ SYMBOL <:unicode>; term = term -> term ] -> + (hyp_paths, goal_path) ] + ]; + direction: [ + [ IDENT "left" -> `Left + | SYMBOL ">" -> `Left + | IDENT "right" -> `Right + | SYMBOL "<" -> `Right ] + ]; tactic: [ [ [ IDENT "absurd" ]; t = tactic_term -> TacticAst.Absurd (loc, t) @@ -338,8 +349,7 @@ EXTEND | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> TacticAst.Auto (loc,num) | [ IDENT "change" ]; - t1 = tactic_term; "with"; t2 = tactic_term; - where = tactic_where -> + t1 = tactic_term; "with"; t2 = tactic_term; where = pattern_spec -> TacticAst.Change (loc, t1, t2, where) (* TODO Change_pattern *) | [ IDENT "contradiction" ] -> @@ -347,12 +357,11 @@ EXTEND | [ IDENT "cut" ]; t = tactic_term -> TacticAst.Cut (loc, t) - | [ IDENT "decompose" ]; - principles = ident_list1; where = IDENT -> - TacticAst.Decompose (loc, where, principles) + | [ IDENT "decompose" ]; where = term -> + TacticAst.Decompose (loc, where) | [ IDENT "discriminate" ]; - hyp = IDENT -> - TacticAst.Discriminate (loc, hyp) + t = tactic_term -> + TacticAst.Discriminate (loc, t) | [ IDENT "elimType" ]; t = tactic_term -> TacticAst.ElimType (loc, t) | [ IDENT "elim" ]; @@ -369,8 +378,8 @@ EXTEND | [ IDENT "fourier" ] -> TacticAst.Fourier loc | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) - | [ IDENT "injection" ]; ident = IDENT -> - TacticAst.Injection (loc, ident) + | [ IDENT "injection" ]; t = term -> + TacticAst.Injection (loc, t) | [ IDENT "intros" ]; num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> @@ -383,28 +392,21 @@ EXTEND where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) | kind = reduction_kind; - pat = OPT [ - "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] -> - pat - ]; - terms = LIST0 term SEP SYMBOL "," -> - (match (pat, terms) with - | None, [] -> TacticAst.Reduce (loc, kind, None) - | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal)) - | Some pat, [] -> fail loc "Missing term [list]" - | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat))) - | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term -> - TacticAst.ReduceAt (loc, kind, where, pat) + p = OPT [ pattern_spec ] -> + let p = match p with None -> [], None | Some p -> p in + TacticAst.Reduce (loc, kind, p) + | IDENT "generalize"; t = tactic_term; p = OPT [ pattern_spec ] -> + let p = match p with None -> [], None | Some p -> p in + TacticAst.Generalize (loc,t,p) | [ IDENT "reflexivity" ] -> TacticAst.Reflexivity loc | [ IDENT "replace" ]; t1 = tactic_term; "with"; t2 = tactic_term -> TacticAst.Replace (loc, t1, t2) - | [ IDENT "rewrite" ; IDENT "left" ] ; t = term -> - TacticAst.Rewrite (loc,`Left, t, None) - | [ IDENT "rewrite" ; IDENT "right" ] ; t = term -> - TacticAst.Rewrite (loc,`Right, t, None) - (* TODO Replace_pattern *) + | IDENT "rewrite" ; d = direction; t = term ; + p = OPT [ pattern_spec ] -> + let p = match p with None -> [], None | Some p -> p in + TacticAst.Rewrite (loc, d, t, p) | [ IDENT "right" ] -> TacticAst.Right loc | [ IDENT "ring" ] -> TacticAst.Ring loc | [ IDENT "split" ] -> TacticAst.Split loc @@ -413,6 +415,11 @@ EXTEND | [ IDENT "transitivity" ]; t = tactic_term -> TacticAst.Transitivity (loc, t) + | [ IDENT "fwd" ]; t = term -> + TacticAst.FwdSimpl (loc, t) + | [ IDENT "lapply" ]; what = tactic_term; + to_what = OPT [ "to" ; t = tactic_term -> t ] -> + TacticAst.LApply (loc, to_what, what) ] ]; tactical: @@ -553,12 +560,12 @@ EXTEND [ IDENT "set" ]; n = QSTRING; v = QSTRING -> TacticAst.Set (loc, n, v) | [ IDENT "qed" ] -> TacticAst.Qed loc - | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; + | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - TacticAst.Theorem (loc, flavour, name, typ, body) - | flavour = theorem_flavour; name = OPT IDENT; + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body) + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs -> let name,ty = @@ -568,19 +575,19 @@ EXTEND | _ -> assert false in let body = CicAst.Ident (name,None) in - TacticAst.Theorem(loc, `Definition, Some name, ty, - Some (CicAst.LetRec (ind_kind, defs, body))) + TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty, + Some (CicAst.LetRec (ind_kind, defs, body)))) | [ IDENT "inductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in - TacticAst.Inductive (loc, params, ind_types) + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) | [ IDENT "coinductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) ind_types in - TacticAst.Inductive (loc, params, ind_types) + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) | [ IDENT "coercion" ] ; name = IDENT -> TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) | [ IDENT "coercion" ] ; name = URI -> @@ -588,7 +595,7 @@ EXTEND | [ IDENT "alias" ]; spec = alias_spec -> TacticAst.Alias (loc, spec) | [ IDENT "record" ]; (params,name,ty,fields) = record_spec -> - TacticAst.Record (loc, params,name,ty,fields) + TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) ]]; executable: [ @@ -612,7 +619,7 @@ EXTEND ] ]; statements: [ - [ l = LIST0 [ statement ] -> l + [ l = LIST0 statement ; EOI -> l ] ]; END @@ -679,8 +686,8 @@ module EnvironmentP3 = alias: [ (* return a pair from an alias *) [ IDENT "alias"; choice = - [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI -> - (Id id, choice_of_uri uri) + [ IDENT "id"; id = IDENT; SYMBOL "="; suri = URI -> + (Id id, choice_of_uri suri) | IDENT "symbol"; symbol = QSTRING; PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; SYMBOL "="; dsc = QSTRING ->