From ece6204d9ccb8e37f5050ba4ee5c3d43669bf6ef Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 1 Mar 2004 14:53:49 +0000 Subject: Généralisation du type ltac Identifier en IntroPattern; prise en compte des IntroPattern au parsing, à l'interprétation, à la traduction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/genarg.ml | 34 ++++++++++-- interp/genarg.mli | 25 +++++++-- parsing/argextend.ml4 | 3 + parsing/g_ltac.ml4 | 2 + parsing/g_ltacnew.ml4 | 5 +- parsing/g_tactic.ml4 | 3 +- parsing/g_tacticnew.ml4 | 2 +- parsing/pcoq.ml4 | 2 + parsing/pcoq.mli | 1 + parsing/pptactic.ml | 18 +++--- parsing/q_coqast.ml4 | 9 +-- tactics/tacinterp.ml | 140 +++++++++++++++++++++++++++-------------------- tactics/tacinterp.mli | 2 +- translate/pptacticnew.ml | 15 +---- 14 files changed, 160 insertions(+), 101 deletions(-) diff --git a/interp/genarg.ml b/interp/genarg.ml index 80248f7e5..4ef21df45 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -8,8 +8,10 @@ (* $Id$ *) +open Pp open Util open Names +open Nameops open Nametab open Rawterm open Topconstr @@ -22,6 +24,7 @@ type argument_type = | IntOrVarArgType | StringArgType | PreIdentArgType + | IntroPatternArgType | IdentArgType | RefArgType (* Specific types *) @@ -61,6 +64,25 @@ let create_arg s = let exists_argtype s = List.mem s !dyntab +type intro_pattern_expr = + | IntroOrAndPattern of case_intro_pattern_expr + | IntroWildcard + | IntroIdentifier of identifier +and case_intro_pattern_expr = intro_pattern_expr list list + +let rec pr_intro_pattern = function + | IntroOrAndPattern pll -> pr_case_intro_pattern pll + | IntroWildcard -> str "_" + | IntroIdentifier id -> pr_id id + +and pr_case_intro_pattern = function + | [_::_ as pl] -> + str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" + | pll -> + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) + ++ str "]" + type open_constr = Evd.evar_map * Term.constr type open_constr_expr = constr_expr type open_rawconstr = rawconstr_and_expr @@ -81,14 +103,18 @@ let rawwit_string = StringArgType let globwit_string = StringArgType let wit_string = StringArgType -let rawwit_ident = IdentArgType -let globwit_ident = IdentArgType -let wit_ident = IdentArgType - let rawwit_pre_ident = PreIdentArgType let globwit_pre_ident = PreIdentArgType let wit_pre_ident = PreIdentArgType +let rawwit_intro_pattern = IntroPatternArgType +let globwit_intro_pattern = IntroPatternArgType +let wit_intro_pattern = IntroPatternArgType + +let rawwit_ident = IdentArgType +let globwit_ident = IdentArgType +let wit_ident = IdentArgType + let rawwit_ref = RefArgType let globwit_ref = RefArgType let wit_ref = RefArgType diff --git a/interp/genarg.mli b/interp/genarg.mli index 23e1b5377..18f1e33fb 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -28,6 +28,15 @@ type open_constr = Evd.evar_map * Term.constr type open_constr_expr = constr_expr type open_rawconstr = rawconstr_and_expr +type intro_pattern_expr = + | IntroOrAndPattern of case_intro_pattern_expr + | IntroWildcard + | IntroIdentifier of identifier +and case_intro_pattern_expr = intro_pattern_expr list list + +val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds +val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds + (* The route of a generic argument, from parsing to evaluation parsing in_raw out_raw @@ -52,8 +61,9 @@ BoolArgType bool bool IntArgType int int IntOrVarArgType int or_var int StringArgType string (parsed w/ "") string -IdentArgType identifier identifier PreIdentArgType string (parsed w/o "") string +IdentArgType identifier identifier +IntroPatternArgType intro_pattern_expr intro_pattern_expr RefArgType reference global_reference ConstrArgType constr_expr constr ConstrMayEvalArgType constr_expr may_eval constr @@ -85,14 +95,18 @@ val rawwit_string : (string,'co,'ta) abstract_argument_type val globwit_string : (string,'co,'ta) abstract_argument_type val wit_string : (string,'co,'ta) abstract_argument_type -val rawwit_ident : (identifier,'co,'ta) abstract_argument_type -val globwit_ident : (identifier,'co,'ta) abstract_argument_type -val wit_ident : (identifier,'co,'ta) abstract_argument_type - val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type val globwit_pre_ident : (string,'co,'ta) abstract_argument_type val wit_pre_ident : (string,'co,'ta) abstract_argument_type +val rawwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type +val globwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type +val wit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type + +val rawwit_ident : (identifier,'co,'ta) abstract_argument_type +val globwit_ident : (identifier,'co,'ta) abstract_argument_type +val wit_ident : (identifier,'co,'ta) abstract_argument_type + val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type val wit_ref : (global_reference,constr,'ta) abstract_argument_type @@ -198,6 +212,7 @@ type argument_type = | IntOrVarArgType | StringArgType | PreIdentArgType + | IntroPatternArgType | IdentArgType | RefArgType (* Specific types *) diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 44a54a0cf..6ed6c51e4 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -23,6 +23,7 @@ let rec make_rawwit loc = function | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >> | StringArgType -> <:expr< Genarg.rawwit_string >> | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >> + | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >> | IdentArgType -> <:expr< Genarg.rawwit_ident >> | RefArgType -> <:expr< Genarg.rawwit_ref >> | SortArgType -> <:expr< Genarg.rawwit_sort >> @@ -47,6 +48,7 @@ let rec make_globwit loc = function | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >> | StringArgType -> <:expr< Genarg.globwit_string >> | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >> + | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >> | IdentArgType -> <:expr< Genarg.globwit_ident >> | RefArgType -> <:expr< Genarg.globwit_ref >> | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >> @@ -71,6 +73,7 @@ let rec make_wit loc = function | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> | StringArgType -> <:expr< Genarg.wit_string >> | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> + | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> | IdentArgType -> <:expr< Genarg.wit_ident >> | RefArgType -> <:expr< Genarg.wit_ref >> | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 1e57506df..bd60dc672 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -188,6 +188,7 @@ GEXTEND Gram | IDENT "Check"; c = Constr.constr -> ConstrMayEval (ConstrTypeOf c) | IDENT "FreshId"; s = OPT STRING -> TacFreshId s + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat | r = reference -> Reference r | ta = tactic_arg0 -> ta ] ] ; @@ -199,6 +200,7 @@ GEXTEND Gram | IDENT "Check"; c = Constr.constr -> ConstrMayEval (ConstrTypeOf c) | IDENT "FreshId"; s = OPT STRING -> TacFreshId s + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat | r = reference; la = LIST1 tactic_arg0 -> TacCall (loc,r,la) | r = reference -> Reference r | ta = tactic_arg0 -> ta ] ] diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index c57e7761d..35f8e642e 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -115,8 +115,10 @@ GEXTEND Gram s = [ s = STRING -> s | -> ""] -> TacFail (n,s) | st = simple_tactic -> TacAtom (loc,st) | a = may_eval_arg -> TacArg(a) - | IDENT"constr"; ":"; c = Constr.constr -> + | IDENT "constr"; ":"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c)) + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> + TacArg(IntroPattern ipat) | r = reference; la = LIST1 tactic_arg -> TacArg(TacCall (loc,r,la)) | r = reference -> TacArg (Reference r) ] @@ -127,6 +129,7 @@ GEXTEND Gram (* Tactic arguments *) tactic_arg: [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat | a = may_eval_arg -> a | a = tactic_atom -> a | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index e9a5ed777..73718c629 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -64,7 +64,8 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if !Options.v7 then GEXTEND Gram GLOBAL: simple_tactic constrarg bindings constr_with_bindings - quantified_hypothesis red_expr int_or_var castedopenconstr; + quantified_hypothesis red_expr int_or_var castedopenconstr + simple_intropattern; int_or_var: [ [ n = integer -> Genarg.ArgArg n diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 4cdf0bc35..721697c9a 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -130,7 +130,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if not !Options.v7 then GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis - bindings red_expr int_or_var castedopenconstr; + bindings red_expr int_or_var castedopenconstr simple_intropattern; int_or_var: [ [ n = integer -> Genarg.ArgArg n diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 296c66b07..5aad710c7 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -379,6 +379,8 @@ module Tactic = make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis" let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var" let red_expr = make_gen_entry utactic rawwit_red_expr "red_expr" + let simple_intropattern = + make_gen_entry utactic rawwit_intro_pattern "simple_intropattern" (* Main entries for ltac *) let tactic_arg = Gram.Entry.create "tactic:tactic_arg" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index c245f9fd5..68977fb3d 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -162,6 +162,7 @@ module Tactic : val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e + val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e val tactic_arg : raw_tactic_arg Gram.Entry.e val tactic : raw_tactic_expr Gram.Entry.e val tactic_eoi : raw_tactic_expr Gram.Entry.e diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3a6cfab0e..9c27cb65b 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -140,16 +140,6 @@ let pr_with_constr prc = function | None -> mt () | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) -let rec pr_intro_pattern = function - | IntroOrAndPattern pll -> pr_case_intro_pattern pll - | IntroWildcard -> str "_" - | IntroIdentifier id -> pr_id id - -and pr_case_intro_pattern pll = - str "[" ++ - hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) - ++ str "]" - let pr_with_names = function | [] -> mt () | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids) @@ -265,6 +255,8 @@ let rec pr_raw_generic prc prlc prtac prref x = | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x) | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x) + | IntroPatternArgType -> pr_arg pr_intro_pattern + (out_gen rawwit_intro_pattern x) | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen rawwit_ident x)) | RefArgType -> pr_arg prref (out_gen rawwit_ref x) | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x) @@ -310,6 +302,8 @@ let rec pr_glob_generic prc prlc prtac x = | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen globwit_int_or_var x) | StringArgType -> spc () ++ str "\"" ++ str (out_gen globwit_string x) ++ str "\"" | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x) + | IntroPatternArgType -> + pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x) | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen globwit_ident x)) | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x) | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x) @@ -356,6 +350,8 @@ let rec pr_generic prc prlc prtac x = | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x) | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\"" | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x) + | IntroPatternArgType -> + pr_arg pr_intro_pattern (out_gen wit_intro_pattern x) | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen wit_ident x)) | RefArgType -> pr_arg pr_global (out_gen wit_ref x) | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x)) @@ -692,7 +688,7 @@ and pr6 = function and pr_tacarg0 = function | TacDynamic (_,t) -> str ("") | MetaIdArg (_,s) -> str ("$" ^ s) - | Identifier id -> pr_id id + | IntroPattern ipat -> pr_intro_pattern ipat | TacVoid -> str "()" | Reference r -> pr_ref r | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 8df84e573..87eb0784f 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -133,10 +133,10 @@ let mlexpr_of_reference = function | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> let mlexpr_of_intro_pattern = function - | Tacexpr.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO" - | Tacexpr.IntroWildcard -> <:expr< Tacexpr.IntroWildcard >> - | Tacexpr.IntroIdentifier id -> - <:expr< Tacexpr.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> + | Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO" + | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> + | Genarg.IntroIdentifier id -> + <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) @@ -250,6 +250,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> | Genarg.RefArgType -> <:expr< Genarg.RefArgType >> | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> + | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >> | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >> | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index fe96fa44d..a0d791a58 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -69,10 +69,10 @@ type value = | VFun of (identifier*value) list * identifier option list * glob_tactic_expr | VVoid | VInteger of int - | VIdentifier of identifier (* idents which are not bound, as in "Intro H" *) - (* but which may be bound later, as in "tac" in*) - (* "Intro H; tac" *) - | VConstr of constr (* includes idents known bound and references *) + | VIntroPattern of intro_pattern_expr (* includes idents which are not *) + (* bound as in "Intro H" but which may be bound *) + (* later, as in "tac" in "Intro H; tac" *) + | VConstr of constr (* includes idents known bound and references *) | VConstr_context of constr | VRec of value ref @@ -114,7 +114,7 @@ let constr_of_VConstr_context = function let pr_value env = function | VVoid -> str "()" | VInteger n -> int n - | VIdentifier id -> pr_id id + | VIntroPattern ipat -> pr_intro_pattern ipat | VConstr c -> Printer.prterm_env env c | VConstr_context c -> Printer.prterm_env env c | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "" @@ -205,7 +205,6 @@ let coerce_to_reference env = function | VConstr c -> (try reference_of_constr c with Not_found -> invalid_arg_loc (loc, "Not a reference")) -(* | VIdentifier id -> VarRef id*) | v -> errorlabstrm "coerce_to_reference" (str "The value" ++ spc () ++ pr_value env v ++ str "cannot be coerced to a reference") @@ -220,7 +219,6 @@ let coerce_to_evaluable_ref env c = let ev = match c with | VConstr c when isConst c -> EvalConstRef (destConst c) | VConstr c when isVar c -> EvalVarRef (destVar c) -(* | VIdentifier id -> EvalVarRef id*) | _ -> error_not_evaluable (pr_value env c) in if not (Tacred.is_evaluable env ev) then @@ -352,7 +350,7 @@ let find_hyp id sign = (* be fresh in which case it is binding later on *) let intern_ident l ist id = (* We use identifier both for variables and new names; thus nothing to do *) - if find_ident id ist then () else l:=(id::fst !l,id::snd !l); + if not (find_ident id ist) then l:=(id::fst !l,id::snd !l); id let intern_name l ist = function @@ -442,7 +440,8 @@ let intern_reference strict ist = function ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> (match r with - | Ident (loc,id) when not strict -> Identifier id + | Ident (loc,id) when not strict -> + IntroPattern (IntroIdentifier id) | _ -> let (loc,qid) = qualid_of_reference r in error_global_not_found_loc loc qid))) @@ -795,7 +794,9 @@ and intern_tactic_fun ist (var,body) = and intern_tacarg strict ist = function | TacVoid -> TacVoid | Reference r -> intern_reference strict ist r - | Identifier id -> anomaly "Not used only in raw_tactic_expr" + | IntroPattern ipat -> + let lf = ref([],[]) in (*How to know what names the intropattern binds?*) + IntroPattern (intern_intro_pattern lf ist ipat) | Integer n -> Integer n | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) | MetaIdArg (loc,s) -> @@ -840,6 +841,11 @@ and intern_genarg ist x = in_gen globwit_string (out_gen rawwit_string x) | PreIdentArgType -> in_gen globwit_pre_ident (out_gen rawwit_pre_ident x) + | IntroPatternArgType -> + let lf = ref ([],[]) in + (* how to know which names are bound by the intropattern *) + in_gen globwit_intro_pattern + (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x)) | IdentArgType -> in_gen globwit_ident (snd (intern_hyp ist (dummy_loc,out_gen rawwit_ident x))) | RefArgType -> @@ -962,7 +968,8 @@ let apply_matching pat csr = (* Tries to match one hypothesis pattern with a list of hypotheses *) let apply_one_mhyp_context ist env gl lmatch (hypname,pat) (lhyps,nocc) = let get_id_couple id = function - | Name idpat -> [idpat,VIdentifier id] +(* | Name idpat -> [idpat,VIdentifier id]*) + | Name idpat -> [idpat,VConstr (mkVar id)] | Anonymous -> [] in let rec apply_one_mhyp_context_rec nocc = function | (id,hyp)::tl as hyps -> @@ -1009,31 +1016,43 @@ let set_debug pos = debug := pos let get_debug () = !debug (* Interprets an identifier which must be fresh *) -let eval_ident ist id = +let interp_ident ist id = try match List.assoc id ist.lfun with - | VIdentifier id -> id + | VIntroPattern (IntroIdentifier id) -> id | VConstr c as v when isVar c -> (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *) (* c is then expected not to belong to the proof context *) - (* would be checkable if env were known from eval_ident *) + (* would be checkable if env were known from interp_ident *) destVar c - | _ -> user_err_loc(loc,"eval_ident", str "An ltac name (" ++ pr_id id ++ + | _ -> user_err_loc(loc,"interp_ident", str "An ltac name (" ++ pr_id id ++ str ") should have been bound to an identifier") with Not_found -> id -let eval_integer lfun (loc,id) = +let interp_intro_pattern_var ist id = + try match List.assoc id ist.lfun with + | VIntroPattern ipat -> ipat + | VConstr c as v when isVar c -> + (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *) + (* c is then expected not to belong to the proof context *) + (* would be checkable if env were known from interp_ident *) + IntroIdentifier (destVar c) + | _ -> user_err_loc(loc,"interp_ident", str "An ltac name (" ++ pr_id id ++ + str ") should have been bound to an introduction pattern") + with Not_found -> IntroIdentifier id + +let interp_int lfun (loc,id) = try match List.assoc id lfun with | VInteger n -> n - | _ -> user_err_loc(loc,"eval_integer",str "should be bound to an integer") - with Not_found -> user_err_loc (loc,"eval_integer",str "Unbound variable") + | _ -> user_err_loc(loc,"interp_int",str "should be bound to an integer") + with Not_found -> user_err_loc (loc,"interp_int",str "Unbound variable") let interp_int_or_var ist = function - | ArgVar locid -> eval_integer ist.lfun locid + | ArgVar locid -> interp_int ist.lfun locid | ArgArg n -> n let constr_of_value env = function | VConstr csr -> csr - | VIdentifier id -> constr_of_id env id + | VIntroPattern (IntroIdentifier id) -> constr_of_id env id | _ -> raise Not_found let is_variable env id = @@ -1041,7 +1060,7 @@ let is_variable env id = let variable_of_value env = function | VConstr c as v when isVar c -> destVar c - | VIdentifier id' when is_variable env id' -> id' + | VIntroPattern (IntroIdentifier id) when is_variable env id -> id | _ -> raise Not_found (* Extract a variable from a value, if any *) @@ -1069,9 +1088,9 @@ let interp_var ist gl (loc,id) = (* Interprets an existing hypothesis (i.e. a declared variable) *) let interp_hyp = interp_var -let eval_name ist = function +let interp_name ist = function | Anonymous -> Anonymous - | Name id -> Name (eval_ident ist id) + | Name id -> Name (interp_ident ist id) let interp_clause_pattern ist gl (l,occl) = let rec check acc = function @@ -1083,20 +1102,7 @@ let interp_clause_pattern ist gl (l,occl) = | [] -> [] in (l,check [] occl) -let interp_pure_qualid is_applied env (loc,qid) = - try VConstr (constr_of_reference (find_reference env qid)) - with Not_found -> - let (dir,id) = repr_qualid qid in - if not is_applied & dir = empty_dirpath then VIdentifier id - else user_err_loc (loc,"interp_pure_qualid",str "Unknown reference") - (* Interprets a qualified name *) -let eval_ref ist env = function - | Qualid locqid -> interp_pure_qualid false env locqid - | Ident (loc,id) -> - try unrec (List.assoc id ist.lfun) - with Not_found -> interp_pure_qualid false env (loc,make_short_qualid id) - let interp_reference ist env = function | ArgArg (_,r) -> r | ArgVar (loc,id) -> coerce_to_reference env (unrec (List.assoc id ist.lfun)) @@ -1129,8 +1135,6 @@ let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } = onconcl=b; concl_occs=occs } -let eval_opt_ident ist = option_app (eval_ident ist) - (* Interpretation of constructions *) (* Extract the constr list from lfun *) @@ -1139,14 +1143,23 @@ let rec constr_list_aux env = function let (l1,l2) = constr_list_aux env tl in (try ((id,constr_of_value env v)::l1,l2) with Not_found -> - (l1,(id,match v with VIdentifier id0 -> Some id0 | _ -> None)::l2)) + let ido = match v with + | VIntroPattern (IntroIdentifier id0) -> Some id0 + | _ -> None in + (l1,(id,ido)::l2)) | [] -> ([],[]) let constr_list ist env = constr_list_aux env ist.lfun -(* Extract the identifier list from lfun *) +(*Extract the identifier list from lfun: join all branches (what to do else?)*) +let rec intropattern_ids = function + | IntroIdentifier id -> [id] + | IntroOrAndPattern ll -> + List.flatten (List.map intropattern_ids (List.flatten ll)) + | IntroWildcard -> [] + let rec extract_ids = function - | (id,VIdentifier id')::tl -> id'::extract_ids tl + | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl | _::tl -> extract_ids tl | [] -> [] @@ -1246,7 +1259,7 @@ let interp_constr_may_eval ist gl c = let rec interp_intro_pattern ist = function | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist l) | IntroWildcard -> IntroWildcard - | IntroIdentifier id -> IntroIdentifier (eval_ident ist id) + | IntroIdentifier id -> interp_intro_pattern_var ist id and interp_case_intro_pattern ist = List.map (List.map (interp_intro_pattern ist)) @@ -1258,7 +1271,7 @@ let interp_quantified_hypothesis ist gl = function | NamedHyp id -> try match List.assoc id ist.lfun with | VInteger n -> AnonHyp n - | VIdentifier id -> NamedHyp id +(* | VIdentifier id -> NamedHyp id Why ?*) | v -> NamedHyp (variable_of_value (pf_env gl) v) with Not_found -> NamedHyp id @@ -1337,7 +1350,7 @@ and interp_tacarg ist gl = function | TacVoid -> VVoid | Reference r -> interp_ltac_reference false ist gl r | Integer n -> VInteger n - | Identifier id -> VIdentifier id + | IntroPattern ipat -> VIntroPattern ipat | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c) | MetaIdArg (loc,id) -> assert false | TacCall (loc,f,l) -> @@ -1347,7 +1360,8 @@ and interp_tacarg ist gl = function interp_app ist gl fv largs loc | TacFreshId idopt -> let s = match idopt with None -> "H" | Some s -> s in - VIdentifier (Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl) + let id = Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl in + VIntroPattern (IntroIdentifier id) | Tacexp t -> val_interp ist gl t | TacDynamic(_,t) -> let tg = (tag t) in @@ -1553,8 +1567,11 @@ and interp_genarg ist goal x = in_gen wit_string (out_gen globwit_string x) | PreIdentArgType -> in_gen wit_pre_ident (out_gen globwit_pre_ident x) + | IntroPatternArgType -> + in_gen wit_intro_pattern + (interp_intro_pattern ist (out_gen globwit_intro_pattern x)) | IdentArgType -> - in_gen wit_ident (eval_ident ist (out_gen globwit_ident x)) + in_gen wit_ident (interp_ident ist (out_gen globwit_ident x)) | RefArgType -> in_gen wit_ref (pf_interp_reference ist goal (out_gen globwit_ref x)) | SortArgType -> @@ -1640,7 +1657,7 @@ and interp_atomic ist gl = function | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist gl hyp) | TacIntroMove (ido,ido') -> - h_intro_move (option_app (eval_ident ist) ido) + h_intro_move (option_app (interp_ident ist) ido) (option_app (interp_hyp ist gl) ido') | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) @@ -1651,24 +1668,24 @@ and interp_atomic ist gl = function | TacElimType c -> h_elim_type (pf_interp_constr ist gl c) | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb) | TacCaseType c -> h_case_type (pf_interp_constr ist gl c) - | TacFix (idopt,n) -> h_fix (eval_opt_ident ist idopt) n + | TacFix (idopt,n) -> h_fix (option_app (interp_ident ist) idopt) n | TacMutualFix (id,n,l) -> - let f (id,n,c) = (eval_ident ist id,n,pf_interp_constr ist gl c) in - h_mutual_fix (eval_ident ist id) n (List.map f l) - | TacCofix idopt -> h_cofix (eval_opt_ident ist idopt) + let f (id,n,c) = (interp_ident ist id,n,pf_interp_constr ist gl c) in + h_mutual_fix (interp_ident ist id) n (List.map f l) + | TacCofix idopt -> h_cofix (option_app (interp_ident ist) idopt) | TacMutualCofix (id,l) -> - let f (id,c) = (eval_ident ist id,pf_interp_constr ist gl c) in - h_mutual_cofix (eval_ident ist id) (List.map f l) + let f (id,c) = (interp_ident ist id,pf_interp_constr ist gl c) in + h_mutual_cofix (interp_ident ist id) (List.map f l) | TacCut c -> h_cut (pf_interp_constr ist gl c) | TacTrueCut (na,c) -> - h_true_cut (eval_name ist na) (pf_interp_constr ist gl c) + h_true_cut (interp_name ist na) (pf_interp_constr ist gl c) | TacForward (b,na,c) -> - h_forward b (eval_name ist na) (pf_interp_constr ist gl c) + h_forward b (interp_name ist na) (pf_interp_constr ist gl c) | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) | TacLetTac (na,c,clp) -> let clp = interp_clause ist gl clp in - h_let_tac (eval_name ist na) (pf_interp_constr ist gl c) clp + h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c) (clause_app (interp_hyp_location ist gl) ido) @@ -1713,7 +1730,7 @@ and interp_atomic ist gl = function | TacMove (dep,id1,id2) -> h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2) | TacRename (id1,id2) -> - h_rename (interp_hyp ist gl id1) (eval_ident ist (snd id2)) + h_rename (interp_hyp ist gl id1) (interp_ident ist (snd id2)) (* Constructors *) | TacLeft bl -> h_left (interp_bindings ist gl bl) @@ -1761,7 +1778,10 @@ and interp_atomic ist gl = function | IntOrVarArgType -> VInteger (interp_int_or_var ist (out_gen globwit_int_or_var x)) | PreIdentArgType -> - VIdentifier (id_of_string (out_gen globwit_pre_ident x)) + VIntroPattern + (IntroIdentifier (id_of_string (out_gen globwit_pre_ident x))) + | IntroPatternArgType -> + VIntroPattern (out_gen globwit_intro_pattern x) | IdentArgType -> VConstr (mkVar (interp_hyp ist gl (dummy_loc,out_gen globwit_ident x))) @@ -2020,7 +2040,7 @@ and subst_tacarg subst = function | MetaIdArg (_loc,_) -> assert false | TacCall (_loc,f,l) -> TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) - | (TacVoid | Identifier _ | Integer _ | TacFreshId _) as x -> x + | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x | Tacexp t -> Tacexp (subst_tactic subst t) | TacDynamic(_,t) as x -> (match tag t with @@ -2046,6 +2066,8 @@ and subst_genarg subst (x:glob_generic_argument) = | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x) | StringArgType -> in_gen globwit_string (out_gen globwit_string x) | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x) + | IntroPatternArgType -> + in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x) | IdentArgType -> in_gen globwit_ident (out_gen globwit_ident x) | RefArgType -> in_gen globwit_ref (subst_global_reference subst diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 1a80e9811..49af044c5 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -28,7 +28,7 @@ type value = | VFun of (identifier * value) list * identifier option list * glob_tactic_expr | VVoid | VInteger of int - | VIdentifier of identifier + | VIntroPattern of intro_pattern_expr | VConstr of constr | VConstr_context of constr | VRec of value ref diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index d663c942a..5704d853b 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -207,19 +207,6 @@ let pr_with_constr prc = function | None -> mt () | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) -let rec pr_intro_pattern = function - | IntroOrAndPattern pll -> pr_case_intro_pattern pll - | IntroWildcard -> str "_" - | IntroIdentifier id -> pr_id id - -and pr_case_intro_pattern = function - | [_::_ as pl] -> - str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" - | pll -> - str "[" ++ - hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) - ++ str "]" - let pr_with_names = function | [] -> mt () | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids) @@ -765,7 +752,7 @@ and pr_tacarg env = function | TacDynamic (loc,t) -> pr_with_comments loc (str ("")) | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s)) - | Identifier id -> pr_id id + | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat | TacVoid -> str "()" | Reference r -> pr_ref r | ConstrMayEval c -> -- cgit v1.2.3