X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=9a4340f9fb4b692a9c797e63de88875f57c5ff6f;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=9a88a2cbef3e792ad49d154cfc06fc0ef89efd11;hpb=90c15accf8c385a3dc44aa5f6df13f707514e2cd;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 9a88a2cbe..9a4340f9f 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -181,7 +181,7 @@ EXTEND [ defs = LIST1 [ name = IDENT; args = LIST1 [arg = arg -> arg]; - index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; + index_name = OPT [ "on"; idx = IDENT -> idx ]; ty = OPT [ SYMBOL ":" ; t = term -> t ]; SYMBOL <:unicode> (* ≝ *); t1 = term -> @@ -229,10 +229,12 @@ EXTEND ]]; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; binder_vars: [ - [ vars = LIST1 IDENT SEP SYMBOL ","; + [ vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]]; typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) - | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ","; - typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ) + | PAREN "("; + vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]]; + typ = OPT [ SYMBOL ":"; t = term -> t ]; + PAREN ")" -> (vars, typ) ] ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; @@ -316,135 +318,191 @@ EXTEND ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; + tactic_term_list1: [ + [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] + ]; reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl | [ IDENT "whd" ] -> `Whd | [ IDENT "normalize" ] -> `Normalize ] ]; + sequent_pattern_spec : [ + [ 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 ] -> + let goal_path = + match goal_path with + None -> CicAst.UserInput + | Some goal_path -> goal_path + in + hyp_paths,goal_path + ] + ]; 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) ] + [ res = OPT [ + "in"; + wanted_and_sps = + [ "match" ; wanted = term ; + sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> + Some wanted,sps + | sps = sequent_pattern_spec -> + None,Some sps + ] -> + let wanted,hyp_paths,goal_path = + match wanted_and_sps with + wanted,None -> wanted, [], CicAst.UserInput + | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path + in + wanted, hyp_paths, goal_path ] -> + match res with + None -> None,[],CicAst.UserInput + | Some ps -> ps] ]; direction: [ - [ IDENT "left" -> `Left - | SYMBOL ">" -> `Left - | IDENT "right" -> `Right - | SYMBOL "<" -> `Right ] + [ SYMBOL ">" -> `LeftToRight + | SYMBOL "<" -> `RightToLeft ] ]; tactic: [ - [ [ IDENT "absurd" ]; t = tactic_term -> + [ IDENT "absurd"; t = tactic_term -> TacticAst.Absurd (loc, t) - | [ IDENT "apply" ]; t = tactic_term -> + | IDENT "apply"; t = tactic_term -> TacticAst.Apply (loc, t) - | [ IDENT "assumption" ] -> + | IDENT "assumption" -> TacticAst.Assumption loc - | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> - TacticAst.Auto (loc,num) - | [ IDENT "change" ]; - t1 = tactic_term; "with"; t2 = tactic_term; where = pattern_spec -> - TacticAst.Change (loc, t1, t2, where) - (* TODO Change_pattern *) - | [ IDENT "contradiction" ] -> + | IDENT "auto"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; + width = OPT [ IDENT "width"; SYMBOL "="; i = NUM -> int_of_string i ] -> + TacticAst.Auto (loc,depth,width) + | IDENT "clear"; id = IDENT -> + TacticAst.Clear (loc,id) + | IDENT "clearbody"; id = IDENT -> + TacticAst.ClearBody (loc,id) + | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> + TacticAst.Change (loc, what, t) + | IDENT "compare"; t = tactic_term -> + TacticAst.Compare (loc,t) + | IDENT "constructor"; n = NUM -> + TacticAst.Constructor (loc,int_of_string n) + | IDENT "contradiction" -> TacticAst.Contradiction loc - | [ IDENT "cut" ]; - t = tactic_term -> - TacticAst.Cut (loc, t) - | [ IDENT "decompose" ]; where = term -> + | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> + TacticAst.Cut (loc, ident, t) + | IDENT "decide"; IDENT "equality" -> + TacticAst.DecideEquality loc + | IDENT "decompose"; where = tactic_term -> TacticAst.Decompose (loc, where) - | [ IDENT "discriminate" ]; - t = tactic_term -> + | IDENT "discriminate"; t = tactic_term -> TacticAst.Discriminate (loc, t) - | [ IDENT "elimType" ]; t = tactic_term -> - TacticAst.ElimType (loc, t) - | [ IDENT "elim" ]; - t1 = tactic_term; - using = OPT [ "using"; using = tactic_term -> using ] -> - TacticAst.Elim (loc, t1, using) - | [ IDENT "exact" ]; t = tactic_term -> + | IDENT "elim"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.Elim (loc, what, using, num, idents) + | IDENT "elimType"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.ElimType (loc, what, using, num, idents) + | IDENT "exact"; t = tactic_term -> TacticAst.Exact (loc, t) - | [ IDENT "exists" ] -> + | IDENT "exists" -> TacticAst.Exists loc - | [ IDENT "fold" ]; - kind = reduction_kind; t = tactic_term -> - TacticAst.Fold (loc, kind, t) - | [ IDENT "fourier" ] -> + | IDENT "fail" -> TacticAst.Fail loc + | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise + (Parse_error + (loc,"the pattern cannot specify the term to replace, only its paths in the hypotheses and in the conclusion")) + else + TacticAst.Fold (loc, kind, t, p) + | IDENT "fourier" -> TacticAst.Fourier loc - | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) - | [ IDENT "injection" ]; t = term -> + | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.FwdSimpl (loc, hyp, idents) + | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> + TacticAst.Generalize (loc,p,id) + | IDENT "goal"; n = NUM -> + TacticAst.Goal (loc, int_of_string n) + | IDENT "id" -> TacticAst.IdTac loc + | IDENT "injection"; t = tactic_term -> TacticAst.Injection (loc, t) - | [ IDENT "intros" ]; - num = OPT [ num = int -> num ]; - idents = OPT ident_list0 -> + | IDENT "intro"; ident = OPT IDENT -> + let idents = match ident with None -> [] | Some id -> [id] in + TacticAst.Intros (loc, Some 1, idents) + | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> let idents = match idents with None -> [] | Some idents -> idents in TacticAst.Intros (loc, num, idents) - | [ IDENT "intro" ] -> - TacticAst.Intros (loc, Some 1, []) - | [ IDENT "left" ] -> TacticAst.Left loc - | [ IDENT "letin" ]; - where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> + | IDENT "lapply"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; + what = tactic_term; + to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; + ident = OPT [ "using" ; ident = IDENT -> ident ] -> + let to_what = match to_what with None -> [] | Some to_what -> to_what in + TacticAst.LApply (loc, depth, to_what, what, ident) + | IDENT "left" -> TacticAst.Left loc + | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) - | kind = reduction_kind; - p = OPT [ pattern_spec ] -> - let p = match p with None -> [], None | Some p -> p in + | kind = reduction_kind; p = pattern_spec -> 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" ] -> + | IDENT "reflexivity" -> TacticAst.Reflexivity loc - | [ IDENT "replace" ]; - t1 = tactic_term; "with"; t2 = tactic_term -> - TacticAst.Replace (loc, t1, t2) - | 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 - | [ IDENT "symmetry" ] -> + | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> + TacticAst.Replace (loc, p, t) + | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise + (Parse_error + (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")) + else + TacticAst.Rewrite (loc, d, t, p) + | IDENT "right" -> + TacticAst.Right loc + | IDENT "ring" -> + TacticAst.Ring loc + | IDENT "split" -> + TacticAst.Split loc + | IDENT "symmetry" -> TacticAst.Symmetry loc - | [ IDENT "transitivity" ]; - t = tactic_term -> + | 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: [ "sequence" LEFTA [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> - TacticAst.Seq (loc, tacticals) + match tacticals with + [] -> assert false + | [tac] -> tac + | l -> TacticAst.Seq (loc, l) ] | "then" NONA - [ tac = tactical; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> + [ tac = tactical; SYMBOL ";"; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> (TacticAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA - [ [ IDENT "do" ]; count = int; tac = tactical -> + [ IDENT "do"; count = int; tac = tactical -> TacticAst.Do (loc, count, tac) - | [ IDENT "repeat" ]; tac = tactical -> + | IDENT "repeat"; tac = tactical -> TacticAst.Repeat (loc, tac) ] | "simple" NONA - [ IDENT "tries"; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> - TacticAst.Tries (loc, tacs) + [ IDENT "first"; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> + TacticAst.First (loc, tacs) | IDENT "try"; tac = NEXT -> TacticAst.Try (loc, tac) - | IDENT "fail" -> TacticAst.Fail loc - | IDENT "id" -> TacticAst.IdTac loc + | IDENT "solve"; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> + TacticAst.Solve (loc, tacs) | PAREN "("; tac = tactical; PAREN ")" -> tac | tac = tactic -> TacticAst.Tactic (loc, tac) ] @@ -527,12 +585,9 @@ EXTEND let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in let rex = Str.regexp ("^"^ident^"$") in if Str.string_match rex id 0 then - let rex = Str.regexp - ("^\\(cic:/\\|theory:/\\)"^ident^ - "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^ - "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$") - in - if Str.string_match rex uri 0 then + if (try ignore (UriManager.uri_of_string uri); true + with UriManager.IllFormedUri _ -> false) + then TacticAst.Ident_alias (id, uri) else raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri)) @@ -556,8 +611,9 @@ EXTEND ]; command: [[ - [ IDENT "set" ]; n = QSTRING; v = QSTRING -> + [ IDENT "set" ]; n = QSTRING; v = QSTRING -> TacticAst.Set (loc, n, v) + | [ IDENT "drop" ] -> TacticAst.Drop loc | [ IDENT "qed" ] -> TacticAst.Qed loc | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> @@ -587,14 +643,19 @@ EXTEND ind_types in TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) - | [ IDENT "coercion" ] ; name = IDENT -> + | IDENT "coercion" ; name = IDENT -> TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) - | [ IDENT "coercion" ] ; name = URI -> + | IDENT "coercion" ; name = URI -> TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) - | [ IDENT "alias" ]; spec = alias_spec -> + | IDENT "alias" ; spec = alias_spec -> TacticAst.Alias (loc, spec) - | [ IDENT "record" ]; (params,name,ty,fields) = record_spec -> + | IDENT "record" ; (params,name,ty,fields) = record_spec -> TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) + | IDENT "include" ; path = QSTRING -> + TacticAst.Include (loc,path) + | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> + let uris = List.map UriManager.uri_of_string uris in + TacticAst.Default (loc,what,uris) ]]; executable: [ @@ -670,7 +731,8 @@ module EnvironmentP3 = s :: acc) env [] in - String.concat "\n" (List.sort compare aliases) + String.concat "\n" (List.sort compare aliases) ^ + (if aliases = [] then "" else "\n") EXTEND GLOBAL: aliases;