X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=a879ccf94ff1f380d011e71927250df3e3c46f3d;hb=287dfa9d6e5213d4c578f5b3485fc52a86ce7934;hp=bfc535a3c35f59b204ccd8d7706d7df3fb15d8af;hpb=17c5ad881e737bd2cba2e157f346a618fce87204;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index bfc535a3c..a879ccf94 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 @@ -69,6 +69,7 @@ let alias_spec = Grammar.Entry.create grammar "alias_spec" let macro = Grammar.Entry.create grammar "macro" let script = Grammar.Entry.create grammar "script" let statement = Grammar.Entry.create grammar "statement" +let statements = Grammar.Entry.create grammar "statements" let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) @@ -116,7 +117,7 @@ let mk_binder_ast binder typ vars body = vars body EXTEND - GLOBAL: term term0 statement; + GLOBAL: term term0 statement statements; int: [ [ num = NUM -> try @@ -170,14 +171,16 @@ EXTEND (head, vars) ] ]; + arg: [ + [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; PAREN ")" -> names,ty + | name = IDENT -> [name],CicAst.Implicit + ] + ]; let_defs:[ [ defs = LIST1 [ name = IDENT; - args = LIST1 [ - PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; - ty = term; PAREN ")" -> - (names, ty) - ]; + args = LIST1 [arg = arg -> arg]; index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; ty = OPT [ SYMBOL ":" ; t = term -> t ]; SYMBOL <:unicode> (* ≝ *); @@ -226,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 ] ]; @@ -278,6 +283,7 @@ EXTEND | n = substituted_name -> return_term loc n | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ()))) | IMPLICIT -> return_term loc CicAst.Implicit + | PLACEHOLDER -> return_term loc CicAst.UserInput | m = META; substs = [ PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> @@ -292,7 +298,7 @@ EXTEND return_term loc (CicAst.Meta (index, substs)) | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; "match"; t = term; - indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; + indty_ident = OPT ["in" ; id = IDENT -> id ]; "with"; PAREN "["; patterns = LIST0 [ @@ -308,103 +314,159 @@ 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 ] + tactic_term_list1: [ + [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl - | [ IDENT "whd" ] -> `Whd ] + | [ 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: [ + [ 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: [ + [ 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 = tactic_where -> - 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" ]; - principles = ident_list1; where = IDENT -> - TacticAst.Decompose (loc, where, principles) - | [ IDENT "discriminate" ]; - hyp = IDENT -> - TacticAst.Discriminate (loc, hyp) - | [ IDENT "elimType" ]; t = tactic_term -> - TacticAst.ElimType (loc, t) - | [ IDENT "elim" ]; - t1 = tactic_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 -> + TacticAst.Discriminate (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 "elimType"; t = tactic_term -> + TacticAst.ElimType (loc, t) + | 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" ]; ident = IDENT -> - TacticAst.Injection (loc, ident) - | [ IDENT "intros" ]; - num = OPT [ num = int -> num ]; - idents = OPT ident_list0 -> + | 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 "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, None, []) - | [ IDENT "left" ] -> TacticAst.Left loc - | [ "let" | "Let" ]; - t = tactic_term; "in"; where = IDENT -> + | 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; - 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))) - | [ IDENT "reflexivity" ] -> + | kind = reduction_kind; p = pattern_spec -> + TacticAst.Reduce (loc, kind, 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 "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) ] ]; @@ -415,7 +477,7 @@ EXTEND ] | "then" NONA [ tac = tactical; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> (TacticAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA @@ -430,8 +492,6 @@ EXTEND TacticAst.Tries (loc, tacs) | IDENT "try"; tac = NEXT -> TacticAst.Try (loc, tac) - | IDENT "fail" -> TacticAst.Fail loc - | IDENT "id" -> TacticAst.IdTac loc | PAREN "("; tac = tactical; PAREN ")" -> tac | tac = tactic -> TacticAst.Tactic (loc, tac) ] @@ -445,9 +505,7 @@ EXTEND ] ]; inductive_spec: [ [ - fst_name = IDENT; params = LIST0 [ - PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; - typ = term; PAREN ")" -> (names, typ) ]; + fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; @@ -467,15 +525,30 @@ EXTEND let ind_types = fst_ind_type :: tl_ind_types in (params, ind_types) ] ]; - - macro: [[ - [ IDENT "abort" ] -> TacticAst.Abort loc - | [ IDENT "quit" ] -> TacticAst.Quit loc + + record_spec: [ [ + name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + SYMBOL ":"; typ = term; SYMBOL <:unicode>; PAREN "{" ; + fields = LIST0 [ + name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) + ] SEP SYMBOL ";"; PAREN "}" -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + (params,name,typ,fields) + ] ]; + + macro: [ + [ [ IDENT "quit" ] -> TacticAst.Quit loc +(* | [ IDENT "abort" ] -> TacticAst.Abort loc *) | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) - | [ IDENT "undo" ]; steps = OPT NUM -> +(* | [ IDENT "undo" ]; steps = OPT NUM -> TacticAst.Undo (loc, int_opt steps) | [ IDENT "redo" ]; steps = OPT NUM -> - TacticAst.Redo (loc, int_opt steps) + TacticAst.Redo (loc, int_opt steps) *) | [ IDENT "check" ]; t = term -> TacticAst.Check (loc, t) | [ IDENT "hint" ] -> TacticAst.Hint loc @@ -490,7 +563,8 @@ EXTEND | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> TacticAst.WHint (loc,t) | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) - ]]; + ] + ]; alias_spec: [ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> @@ -529,41 +603,46 @@ 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 = 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) + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs -> let name,ty = match defs with | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty - | ((Cic.Name name,None),_,_) :: _ -> - fail loc ("No type given for " ^ name) + | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit | _ -> 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 -> TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) | [ IDENT "alias" ]; spec = alias_spec -> TacticAst.Alias (loc, spec) + | [ IDENT "record" ]; (params,name,ty,fields) = record_spec -> + TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) ]]; executable: [ @@ -586,6 +665,10 @@ EXTEND | com = comment -> TacticAst.Comment (loc, com) ] ]; + statements: [ + [ l = LIST0 statement ; EOI -> l + ] + ]; END let exc_located_wrapper f = @@ -601,6 +684,9 @@ let parse_term stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) let parse_statement stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) +let parse_statements stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream)) + (**/**) @@ -647,8 +733,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 ->