diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-19 17:35:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-19 17:35:03 +0000 |
| commit | 1abd56dea147493178a582569f50c9c6f03c6008 (patch) | |
| tree | 940ad7cdc5bef6de02ea76d7b7bd450920313798 | |
| parent | 4f17ea4dcc68bb4619dbf2b8578333288f145fe5 (diff) | |
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
79 files changed, 411 insertions, 316 deletions
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml index 5c6e845a3..70182d128 100644 --- a/contrib/correctness/pmlize.ml +++ b/contrib/correctness/pmlize.ml @@ -30,7 +30,7 @@ open Pmonad let has_proof_part ren env c = let sign = Pcicenv.trad_sign_of ren env in let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in - is_matching (Coqlib.build_coq_sig_pattern ()) (Reductionops.nf_betaiota ty) + Hipattern.is_matching_sigma (Reductionops.nf_betaiota ty) (* main part: translation of imperative programs into functional ones. * diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index e3028ffb0..b272f6d04 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -105,19 +105,22 @@ let z = IndRef (coq_constant ["ZArith";"fast_integer"] "Z", 0) let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0) let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0) +let mkmeta n = Nameops.make_ident "X" (Some n) +let mkPMeta n = PMeta (Some (mkmeta n)) + (* ["(well_founded nat lt)"] *) let wf_nat_pattern = PApp (PRef well_founded, [| PRef nat; PRef lt |]) (* ["((well_founded Z (Zwf ?1))"] *) let wf_z_pattern = let zwf = ConstRef (coq_constant ["ZArith";"Zwf"] "Zwf") in - PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |]) + PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| mkPMeta 1 |]) |]) (* ["(and ?1 ?2)"] *) let and_pattern = - PApp (PRef and_, [| PMeta (Some 1); PMeta (Some 2) |]) + PApp (PRef and_, [| mkPMeta 1; mkPMeta 2 |]) (* ["(eq ?1 ?2 ?3)"] *) let eq_pattern = - PApp (PRef eq, [| PMeta (Some 1); PMeta (Some 2); PMeta (Some 3) |]) + PApp (PRef eq, [| mkPMeta 1; mkPMeta 2; mkPMeta 3 |]) (* loop_ids: remove loop<i> hypotheses from the context, and rewrite * using Variant<i> hypotheses when needed. *) diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index eb64b7eb2..f70af8c9f 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -17,6 +17,7 @@ open Term open Termops open Pattern open Matching +open Hipattern open Environ open Pmisc @@ -193,16 +194,12 @@ let id_from_name = function Name id -> id | Anonymous -> (id_of_string "X") (* v_of_constr : traduit un type CCI en un type ML *) -let dest_sig c = match matches (Coqlib.build_coq_sig_pattern ()) c with - | [_,a; _,p] -> (a,p) - | _ -> assert false - (* TODO: faire un test plus serieux sur le type des objets Coq *) let rec is_pure_cci c = match kind_of_term c with | Cast (c,_) -> is_pure_cci c | Prod(_,_,c') -> is_pure_cci c' | Rel _ | Ind _ | Const _ -> true (* heu... *) - | App _ -> not (is_matching (Coqlib.build_coq_sig_pattern ()) c) + | App _ -> not (is_matching_sigma c) | _ -> Util.error "CCI term not acceptable in programs" let rec v_of_constr c = match kind_of_term c with @@ -222,8 +219,8 @@ let rec v_of_constr c = match kind_of_term c with failwith "v_of_constr: TODO" and c_of_constr c = - if is_matching (Coqlib.build_coq_sig_pattern ()) c then - let (a,q) = dest_sig c in + if is_matching_sigma c then + let (a,q) = match_sigma c in (result_id, v_of_constr a), Peffect.bottom, [], Some (anonymous q) else (result_id, v_of_constr c), Peffect.bottom, [], None diff --git a/contrib/correctness/putil.mli b/contrib/correctness/putil.mli index fa5596034..57315efaf 100644 --- a/contrib/correctness/putil.mli +++ b/contrib/correctness/putil.mli @@ -52,8 +52,6 @@ val type_c_subst : (identifier * identifier) list -> type_c -> type_c val type_v_rsubst : (identifier * constr) list -> type_v -> type_v val type_c_rsubst : (identifier * constr) list -> type_c -> type_c -val dest_sig : constr -> constr * constr - val make_arrow : ('a ml_type_v binder) list -> 'a ml_type_c -> 'a ml_type_v val is_mutable_in_env : local_env -> identifier -> bool diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml index e5af703d2..f30d5382d 100644 --- a/contrib/correctness/pwp.ml +++ b/contrib/correctness/pwp.ml @@ -135,7 +135,7 @@ let normalize_boolean ren env b = Expression c -> let c' = Term.applist (constant "annot_bool",[c]) in let ty = type_of_expression ren env c' in - let (_,q') = dest_sig ty in + let (_,q') = Hipattern.match_sigma ty in let q' = Some { a_value = q'; a_name = Name (bool_name()) } in { desc = Expression c'; pre = b.pre; post = q'; loc = b.loc; diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 4ac1e0e9a..74fbd7f6b 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -147,7 +147,7 @@ let field g = let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in let typ = match Hipattern.match_with_equation (pf_concl g) with - | Some (eq,t::args) when eq = Coqlib.build_coq_eq_data.Coqlib.eq () -> t + | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t | _ -> error "The statement is not built from Leibniz' equality" in let th = VConstr (lookup typ) in (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ()) diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index aaf195a43..810603e45 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -40,7 +40,7 @@ type kind_of_formula= |Evaluable of evaluable_global_reference*constr |False -type counter = bool -> int +type counter = bool -> metavariable let constant path str ()=Coqlib.gen_constant "User" ["Init";path] str @@ -167,7 +167,7 @@ type right_pattern = Rand | Ror | Rforall - | Rexists of int*constr + | Rexists of metavariable*constr | Rarrow | Revaluable of evaluable_global_reference @@ -189,7 +189,7 @@ type left_pattern= Lfalse | Land of inductive | Lor of inductive - | Lforall of int*constr + | Lforall of metavariable*constr | Lexists | Levaluable of evaluable_global_reference | LA of constr*left_arrow_pattern @@ -202,6 +202,8 @@ type left_formula={id:global_reference; exception Is_atom of constr +let meta_succ m = m+1 + let build_left_entry nam typ internal gl metagen= try let pattern= @@ -211,7 +213,7 @@ let build_left_entry nam typ internal gl metagen= | And(i,_) -> Land i | Or(i,_) -> Lor i | Exists (_,_,_,_) -> Lexists - | Forall (d,_) -> let m=1+(metagen false) in Lforall(m,d) + | Forall (d,_) -> let m=meta_succ(metagen false) in Lforall(m,d) | Evaluable (egc,_) ->Levaluable egc | Arrow (a,b) ->LA (a, match kind_of_formula a with @@ -243,7 +245,7 @@ let build_right_entry typ gl metagen= | And(_,_) -> Rand | Or(_,_) -> Ror | Exists (_,d,_,_) -> - let m=1+(metagen false) in Rexists(m,d) + let m=meta_succ(metagen false) in Rexists(m,d) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow | Evaluable (egc,_)->Revaluable egc in diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli index 1e23d7c0b..89bd6d25f 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -32,7 +32,7 @@ type kind_of_formula= |Evaluable of Names.evaluable_global_reference * Term.constr |False -type counter = bool -> int +type counter = bool -> metavariable val construct_nhyps : inductive -> int array @@ -49,7 +49,7 @@ type right_pattern = Rand | Ror | Rforall - | Rexists of int*constr + | Rexists of metavariable*constr | Rarrow | Revaluable of Names.evaluable_global_reference @@ -71,7 +71,7 @@ type left_pattern= Lfalse | Land of inductive | Lor of inductive - | Lforall of int*constr + | Lforall of metavariable*constr | Lexists | Levaluable of Names.evaluable_global_reference | LA of constr*left_arrow_pattern diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml index 5c0148d1f..e5ac4134f 100644 --- a/contrib/first-order/unify.ml +++ b/contrib/first-order/unify.ml @@ -15,6 +15,7 @@ open Tacmach open Term open Names open Termops +open Pattern open Reductionops exception UFAIL of constr*constr diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli index 281e94063..90d3cb3f9 100644 --- a/contrib/first-order/unify.mli +++ b/contrib/first-order/unify.mli @@ -15,9 +15,9 @@ type instance= Real of constr*int (* instance*valeur heuristique*) | Phantom of constr (* domaine de quantification *) -val unif_atoms : int -> constr -> constr -> constr -> instance option +val unif_atoms : metavariable -> constr -> constr -> constr -> instance option -val give_right_instances : int -> constr -> (bool * constr) list -> +val give_right_instances : metavariable -> constr -> (bool * constr) list -> Sequent.t -> (constr*int) list option val give_left_instances : Formula.left_formula list-> Sequent.t -> diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 03070ac92..3139db208 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -284,7 +284,7 @@ open Coqlib let coq_sym_eqT = lazy (build_coq_sym_eqT ()) let coq_False = lazy (build_coq_False ()) let coq_not = lazy (build_coq_not ()) -let coq_eq = lazy (build_coq_eq_data.eq ()) +let coq_eq = lazy (build_coq_eq ()) (* Rdefinitions *) let constant_real = constant ["Reals";"Rdefinitions"] diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 4a8ccef81..eb03d3427 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -57,7 +57,7 @@ let resetexist ()= evarcpt := 0 let mknewmeta ()= begin metacpt := !metacpt+1; - mkMeta !metacpt + mkMeta (!metacpt) end let resetmeta () = metacpt := 0 @@ -86,7 +86,7 @@ let constant dir s = (* fin const\_omega.ml *) let mkEq typ c1 c2 = - mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) + mkApp (build_coq_eq(),[| typ; c1; c2|]) let mkRefl typ c1 = mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 3eb6e7993..a391abf33 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -69,8 +69,8 @@ let rec get_subterm (depth:int) (path: int list) (constr:constr) = transform constr terms into abstract syntax trees. The second argument is the substitution, a list of pairs linking an integer and a constr term. *) -let rec map_subst (env :env) (subst:(int * Term.constr) list) = function - | CMeta (_,i) -> +let rec map_subst (env :env) (subst:patvar_map) = function + | CPatVar (_,(_,i)) -> let constr = List.assoc i subst in extern_constr false env constr | x -> map_constr_expr_with_binders (map_subst env) (fun _ x -> x) subst x;; @@ -173,7 +173,7 @@ let dad_rule_names () = List.map (function (s,_) -> s) !dad_rule_list;; (* this function is inspired from matches_core in pattern.ml *) -let constrain ((n : int),(pat : constr_pattern)) sigma = +let constrain ((n : patvar),(pat : constr_pattern)) sigma = if List.mem_assoc n sigma then if pat = (List.assoc n sigma) then sigma else failwith "internal" @@ -248,7 +248,7 @@ let rec sort_list = function [] -> [] | a::l -> add_in_list_sorting a (sort_list l);; -let mk_dad_meta n = CMeta (zz,n);; +let mk_dad_meta n = CPatVar (zz,(true,Nameops.make_ident "DAD" (Some n)));; let mk_rewrite lr ast = let b = in_gen rawwit_bool lr in let cb = in_gen rawwit_constr_with_bindings ((*Ctast.ct_to_ast*) ast,NoBindings) in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 31d59cab2..a011416f1 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -197,13 +197,18 @@ let tac_qualid_to_ct_ID ref = let loc_qualid_to_ct_ID ref = CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref))) +let int_of_meta n = int_of_string (string_of_id n) +let is_int_meta n = try let _ = int_of_meta n in true with _ -> false + let qualid_or_meta_to_ct_ID = function | AN qid -> tac_qualid_to_ct_ID qid - | MetaNum (_,n) -> CT_metac (CT_int n) + | MetaNum (_,n) when is_int_meta n -> CT_metac (CT_int (int_of_meta n)) + | MetaNum _ -> xlate_error "TODO: ident meta" let ident_or_meta_to_ct_ID = function | AN id -> xlate_ident id - | MetaNum (_,n) -> CT_metac (CT_int n) + | MetaNum (_,n) when is_int_meta n -> CT_metac (CT_int (int_of_meta n)) + | MetaNum _ -> xlate_error "TODO: ident meta" let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l) @@ -347,7 +352,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CCast (_, e, t) -> CT_coerce_TYPED_FORMULA_to_FORMULA (CT_typed_formula(xlate_formula e, xlate_formula t)) - | CMeta (_, i) -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int i)) + | CPatVar (_, (_,i)) when is_int_meta i -> + CT_coerce_ID_to_FORMULA(CT_metac (CT_int (int_of_meta i))) + | CPatVar (_, _) -> xlate_error "TODO: meta as ident" + | CEvar (_, _) -> xlate_error "TODO: evars" | CCoFix (_, (_, id), lm::lmi) -> let strip_mutcorec (fid, arf, ardef) = CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 501206c88..3791716e0 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -326,7 +326,6 @@ let coq_not_gt = lazy (constant ["Arith";"Compare_dec"] "not_gt") (* Logic *) open Coqlib -let build_coq_eq = build_coq_eq_data.eq let coq_eq_ind_r = lazy (constant ["Init"; "Logic"] "eq_ind_r") let coq_dec_or = lazy (logic_constant ["Decidable"] "dec_or") diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 270f09587..db8ce1cb6 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -192,6 +192,9 @@ let decomp_term c = kind_of_term (strip_outer_cast c) ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive type [typ] *) +let coerce_meta_out id = int_of_string (string_of_id id) +let coerce_meta_in n = id_of_string (string_of_int n) + let compute_lhs typ i nargsi = match kind_of_term typ with | Ind(sp,0) -> @@ -204,15 +207,16 @@ let compute_lhs typ i nargsi = let compute_rhs bodyi index_of_f = let rec aux c = - match decomp_term c with + match kind_of_term c with | App (j, args) when j = mkRel (index_of_f) (* recursive call *) -> - let i = destRel (array_last args) in mkMeta i + let i = destRel (array_last args) in + PMeta (Some (coerce_meta_in i)) | App (f,args) -> - mkApp (f, Array.map aux args) + PApp (pattern_of_constr f, Array.map aux args) | Cast (c,t) -> aux c - | _ -> c + | _ -> pattern_of_constr c in - pattern_of_constr (aux bodyi) + aux bodyi (*s Now the function [compute_ivs] itself *) @@ -392,7 +396,8 @@ let quote_terms ivs lc gl = | (lhs, rhs)::tail -> begin try let s1 = matches rhs c in - let s2 = List.map (fun (i,c_i) -> (i,aux c_i)) s1 in + let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1 + in Termops.subst_meta s2 lhs with PatternMatchingFailure -> auxl tail end diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 75f8e7abc..d23986def 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -105,7 +105,7 @@ let idopt_of_name = function let extern_evar loc n = warning "Existential variable turned into meta-variable during externalization"; - CMeta (loc,n) + CPatVar (loc,(false,make_ident "META" (Some n))) let raw_string_of_ref = function | ConstRef kn -> @@ -193,7 +193,8 @@ let extern_app loc inctx impl f args = not !print_implicits_explicit_args & List.exists is_status_implicit impl then - CAppExpl (loc, f, args) + if args = [] (* maybe caused by a hidden coercion *) then CRef f + else CAppExpl (loc, f, args) else explicitize loc inctx impl (CRef f) args @@ -222,7 +223,7 @@ let rec extern inctx scopes vars r = | REvar (loc,n) -> extern_evar loc n - | RMeta (loc,n) -> if !print_meta_as_hole then CHole loc else CMeta (loc,n) + | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n) | RApp (loc,f,args) -> let (f,args) = @@ -411,7 +412,7 @@ let rec extern_pattern tenv vars env = function | PMeta None -> CHole loc - | PMeta (Some n) -> CMeta (loc,n) + | PMeta (Some n) -> CPatVar (loc,(false,n)) | PApp (f,args) -> let (f,args) = @@ -430,7 +431,7 @@ let rec extern_pattern tenv vars env = function let args = List.map (extern_pattern tenv vars env) args in (* [-n] is the trick to embed a so patten into a regular application *) (* see constrintern.ml and g_constr.ml4 *) - explicitize loc false [] (CMeta (loc,-n)) args + explicitize loc false [] (CPatVar (loc,(true,n))) args | PProd (Anonymous,t,c) -> (* Anonymous product are never factorized *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 13864febc..8831b054b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -94,9 +94,10 @@ let explain_internalisation_error = function | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po -let error_unbound_metanum loc n = +let error_unbound_patvar loc n = user_err_loc - (loc,"glob_qualid_or_metanum", str "?" ++ int n ++ str " is unbound") + (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ + str " is unbound") (**********************************************************************) (* Dump of globalization (to be used by coqdoc) *) @@ -470,15 +471,17 @@ let internalise isarity sigma env allow_soapp lvar c = Array.of_list (List.map (intern false env) cl)) | CHole loc -> RHole (loc, QuestionMark) - | CMeta (loc, n) when allow_soapp = None or !interning_grammar -> - RMeta (loc, n) - | CMeta (loc, n) when n >=0 -> + | CPatVar (loc, n) when allow_soapp = None or !interning_grammar -> + RPatVar (loc, n) + | CPatVar (loc, (false,n as x)) -> if List.mem n (out_some allow_soapp) then - RMeta (loc, n) + RPatVar (loc, x) else - error_unbound_metanum loc n - | CMeta (loc, _) -> + error_unbound_patvar loc n + | CPatVar (loc, _) -> raise (InternalisationError (loc,NegativeMetavariable)) + | CEvar (loc, n) -> + REvar (loc, n) | CSort (loc, s) -> RSort(loc,s) | CCast (loc, c1, c2) -> diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b135caf50..c052dadab 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -19,6 +19,7 @@ open Rawterm open Pattern open Coqast open Topconstr +open Termops (*i*) (*s Translation from front abstract syntax of term to untyped terms (rawconstr) @@ -43,7 +44,7 @@ type ltac_env = (* Interprets global names, including syntactic defs and section variables *) val interp_rawconstr : evar_map -> env -> constr_expr -> rawconstr val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> - int list option -> ltac_sign -> constr_expr -> rawconstr + patvar list option -> ltac_sign -> constr_expr -> rawconstr (*s Composing the translation with typing *) val interp_constr : evar_map -> env -> constr_expr -> constr @@ -69,22 +70,22 @@ val type_judgment_of_rawconstr : (* Interprets a constr according to two lists of instantiations (variables and metas), possibly casting it*) val interp_constr_gen : - evar_map -> env -> ltac_env -> (int * constr) list -> constr_expr -> + evar_map -> env -> ltac_env -> patvar_map -> constr_expr -> constr option -> constr (* Interprets a constr according to two lists of instantiations (variables and metas), possibly casting it, and turning unresolved evar into metas*) val interp_openconstr_gen : evar_map -> env -> ltac_env -> - (int * constr) list -> constr_expr -> constr option -> evar_map * constr + patvar_map -> constr_expr -> constr option -> evar_map * constr (* Interprets constr patterns according to a list of instantiations (variables)*) -val interp_constrpattern_gen : - evar_map -> env -> ltac_env -> constr_expr -> int list * constr_pattern +val interp_constrpattern_gen : evar_map -> env -> ltac_env -> constr_expr -> + patvar list * constr_pattern val interp_constrpattern : - evar_map -> env -> constr_expr -> int list * constr_pattern + evar_map -> env -> constr_expr -> patvar list * constr_pattern val interp_reference : ltac_sign -> reference -> rawconstr diff --git a/interp/genarg.ml b/interp/genarg.ml index e1df0ab72..833da9e78 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -13,6 +13,7 @@ open Names open Nametab open Rawterm open Topconstr +open Term type argument_type = (* Basic types *) @@ -39,7 +40,7 @@ type argument_type = | ExtraArgType of string type 'a or_var = ArgArg of 'a | ArgVar of identifier located -type 'a or_metanum = AN of 'a | MetaNum of int located +type 'a or_metanum = AN of 'a | MetaNum of patvar located type 'a and_short_name = 'a * identifier located option type rawconstr_and_expr = rawconstr * constr_expr option diff --git a/interp/genarg.mli b/interp/genarg.mli index 88865f022..8aa82ecb2 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -14,9 +14,10 @@ open Term open Libnames open Rawterm open Topconstr +open Term type 'a or_var = ArgArg of 'a | ArgVar of identifier located -type 'a or_metanum = AN of 'a | MetaNum of int located +type 'a or_metanum = AN of 'a | MetaNum of patvar located type 'a and_short_name = 'a * identifier located option (* In globalize tactics, we need to keep the initial constr_expr to recompute*) diff --git a/interp/reserve.ml b/interp/reserve.ml index deb696733..f6f9fe60d 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -56,7 +56,7 @@ let rec unloc = function | RHole (_,x) -> RHole (dummy_loc,x) | RRef (_,x) -> RRef (dummy_loc,x) | REvar (_,x) -> REvar (dummy_loc,x) - | RMeta (_,x) -> RMeta (dummy_loc,x) + | RPatVar (_,x) -> RPatVar (dummy_loc,x) | RDynamic (_,x) -> RDynamic (dummy_loc,x) let anonymize_if_reserved na t = match na with diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 7f53f7eb2..c8f79b8c5 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -33,7 +33,7 @@ type aconstr = | AOrderedCase of case_style * aconstr option * aconstr * aconstr array | ASort of rawsort | AHole of hole_kind - | AMeta of int + | APatVar of patvar | ACast of aconstr * aconstr let name_app f e = function @@ -59,7 +59,7 @@ let map_aconstr_with_binders_loc loc g f e = function | ACast (c,t) -> RCast (loc,f e c,f e t) | ASort x -> RSort (loc,x) | AHole x -> RHole (loc,x) - | AMeta n -> RMeta (loc,n) + | APatVar n -> RPatVar (loc,(false,n)) | ARef x -> RRef (loc,x) let rec subst_pat subst pat = @@ -122,7 +122,7 @@ let rec subst_aconstr subst raw = if ro' == ro && r' == r && ra' == ra then raw else AOrderedCase (b,ro',r',ra') - | AMeta _ | ASort _ -> raw + | APatVar _ | ASort _ -> raw | AHole (ImplicitArg (ref,i)) -> let ref' = subst_global subst ref in @@ -162,7 +162,7 @@ let aconstr_of_rawconstr vars a = | RSort (_,s) -> ASort s | RHole (_,w) -> AHole w | RRef (_,r) -> ARef r - | RMeta (_,n) -> AMeta n + | RPatVar (_,(_,n)) -> APatVar n | RDynamic _ | RRec _ | REvar _ -> error "Fixpoints, cofixpoints, existential variables and pattern-matching not \ allowed in abbreviatable expressions" @@ -198,7 +198,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1 | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma | RRef (_,r1), ARef r2 when r1 = r2 -> sigma - | RMeta (_,n1), AMeta n2 when n1=n2 -> sigma + | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 -> List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2 | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) -> @@ -217,7 +217,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | RCast(_,c1,t1), ACast(c2,t2) -> match_ alp metas (match_ alp metas sigma c1 c2) t1 t2 | RSort (_,s1), ASort s2 when s1 = s2 -> sigma - | RMeta _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, AHole _ when not(Options.do_translate()) -> sigma | RHole _, AHole _ -> sigma | (RDynamic _ | RRec _ | REvar _), _ @@ -285,7 +285,8 @@ type constr_expr = | COrderedCase of loc * case_style * constr_expr option * constr_expr * constr_expr list | CHole of loc - | CMeta of loc * int + | CPatVar of loc * (bool * patvar) + | CEvar of loc * existential_key | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr | CNotation of loc * notation * constr_expr list @@ -321,7 +322,8 @@ let constr_loc = function | CCases (loc,_,_,_) -> loc | COrderedCase (loc,_,_,_,_) -> loc | CHole loc -> loc - | CMeta (loc,_) -> loc + | CPatVar (loc,_) -> loc + | CEvar (loc,_) -> loc | CSort (loc,_) -> loc | CCast (loc,_,_) -> loc | CNotation (loc,_,_) -> loc @@ -354,7 +356,7 @@ let rec occur_var_constr_expr id = function | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l | CDelimiters (loc,_,a) -> occur_var_constr_expr id a - | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ -> false + | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false | CCases (loc,_,_,_) | COrderedCase (loc,_,_,_,_) | CFix (loc,_,_) @@ -396,7 +398,8 @@ let map_constr_expr_with_binders f g e = function | CCast (loc,a,b) -> CCast (loc,f e a,f e b) | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l) | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) - | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x + | CHole _ | CEvar _ | CPatVar _ | CSort _ + | CNumeral _ | CDynamic _ | CRef _ as x -> x | CCases (loc,po,a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 5c452b870..8f0f5fb75 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -34,7 +34,7 @@ type aconstr = | AOrderedCase of case_style * aconstr option * aconstr * aconstr array | ASort of rawsort | AHole of hole_kind - | AMeta of int + | APatVar of patvar | ACast of aconstr * aconstr val map_aconstr_with_binders_loc : loc -> @@ -83,7 +83,8 @@ type constr_expr = | COrderedCase of loc * case_style * constr_expr option * constr_expr * constr_expr list | CHole of loc - | CMeta of loc * int + | CPatVar of loc * (bool * patvar) + | CEvar of loc * existential_key | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr | CNotation of loc * notation * constr_expr list diff --git a/kernel/term.ml b/kernel/term.ml index bb2247523..f53f28bbb 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -19,6 +19,7 @@ open Esubst (* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *) type existential_key = int +type metavariable = int (* This defines Cases annotations *) type pattern_source = DefaultPat of int | RegularPat @@ -71,7 +72,7 @@ type ('constr, 'types) pcofixpoint = type ('constr, 'types) kind_of_term = | Rel of int | Var of identifier - | Meta of int + | Meta of metavariable | Evar of 'constr pexistential | Sort of sorts | Cast of 'constr * 'types @@ -120,7 +121,7 @@ type cofixpoint = int * rec_declaration let comp_term t1 t2 = match t1, t2 with | Rel n1, Rel n2 -> n1 = n2 - | Meta m1, Meta m2 -> m1 = m2 + | Meta m1, Meta m2 -> m1 == m2 | Var id1, Var id2 -> id1 == id2 | Sort s1, Sort s2 -> s1 == s2 | Cast (c1,t1), Cast (c2,t2) -> c1 == c2 & t1 == t2 @@ -150,7 +151,8 @@ let comp_term t1 t2 = let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t = match t with - | Rel _ | Meta _ -> t + | Rel _ -> t + | Meta x -> Meta x | Var x -> Var (sh_id x) | Sort s -> Sort (sh_sort s) | Cast (c,t) -> Cast (sh_rec c, sh_rec t) diff --git a/kernel/term.mli b/kernel/term.mli index 2c8e9be3f..5f3807605 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -35,6 +35,9 @@ val family_of_sort : sorts -> sorts_family (*s Existential variables *) type existential_key = int +(*s Existential variables *) +type metavariable = int + (*s Case annotation *) type pattern_source = DefaultPat of int | RegularPat type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle @@ -84,8 +87,8 @@ val mkRel : int -> constr (* Constructs a Variable *) val mkVar : identifier -> constr -(* Constructs an metavariable named "?n" *) -val mkMeta : int -> constr +(* Constructs an patvar named "?n" *) +val mkMeta : metavariable -> constr (* Constructs an existential variable *) type existential = existential_key * constr array @@ -187,7 +190,7 @@ type ('constr, 'types) pcofixpoint = type ('constr, 'types) kind_of_term = | Rel of int | Var of identifier - | Meta of int + | Meta of metavariable | Evar of 'constr pexistential | Sort of sorts | Cast of 'constr * 'types @@ -246,7 +249,7 @@ val is_small : sorts -> bool val destRel : constr -> int (* Destructs an existential variable *) -val destMeta : constr -> int +val destMeta : constr -> metavariable (* Destructs a variable *) val destVar : constr -> identifier diff --git a/lib/util.ml b/lib/util.ml index fb71357ba..32ebb30ad 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -543,8 +543,6 @@ type ('a,'b) union = Inl of 'a | Inr of 'b module Intset = Set.Make(struct type t = int let compare = compare end) -let intset_exists p s = Intset.fold (fun x b -> (p x) || b) s false - module Intmap = Map.Make(struct type t = int let compare = compare end) let intmap_in_dom x m = diff --git a/lib/util.mli b/lib/util.mli index 5dac6d30e..349a32366 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -165,8 +165,6 @@ type ('a,'b) union = Inl of 'a | Inr of 'b module Intset : Set.S with type elt = int -val intset_exists : (int -> bool) -> Intset.t -> bool - module Intmap : Map.S with type key = int val intmap_in_dom : int -> 'a Intmap.t -> bool diff --git a/library/nameops.ml b/library/nameops.ml index 04dfd287f..cb1c90e50 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -209,3 +209,6 @@ let default_library = Names.initial_dir (* = ["Top"] *) let coq_root = id_of_string "Coq" let default_root_prefix = make_dirpath [] +(* Metavariables *) +let pr_meta = Pp.int +let string_of_meta = string_of_int diff --git a/library/nameops.mli b/library/nameops.mli index 9e70f0a17..4bb05bd8a 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -49,3 +49,7 @@ val coq_root : module_ident (* This is the default root prefix for developments which doesn't mention a root *) val default_root_prefix : dir_path + +(* Metavariables *) +val pr_meta : Term.metavariable -> Pp.std_ppcmds +val string_of_meta : Term.metavariable -> string diff --git a/parsing/ast.ml b/parsing/ast.ml index 1b68f69bf..869f55bb0 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -466,7 +466,7 @@ let rec pat_of_ast env ast = (Pslam(os,pb), env') | Node(loc,op,_) when isMeta op -> user_err_loc(loc,"Ast.pat_of_ast", - (str"no metavariable in operator position.")) + (str"no patvar in operator position.")) | Node(_,op,args) -> let (pargs, env') = patl_of_astl env args in (Pnode(op,pargs), env') @@ -550,7 +550,7 @@ let rec val_of_ast env = function | Slam(_,os,b) -> Pslam(os, val_of_ast env b) | Node(loc,op,_) when isMeta op -> user_err_loc(loc,"Ast.val_of_ast", - (str"no metavariable in operator position.")) + (str"no patvar in operator position.")) | Node(_,op,args) -> Pnode(op, vall_of_astl env args) | Dynamic(loc,_) -> invalid_arg_loc(loc,"val_of_ast: dynamic") diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index c3b5d98f8..83f4cad58 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -281,7 +281,8 @@ let subst_constr_expr a loc subs = | CCast (_,a,b) -> CCast (loc,subst a,subst b) | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l) | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) - | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x + | CHole _ | CEvar _ | CPatVar _ | CSort _ + | CNumeral _ | CDynamic _ | CRef _ as x -> x | CCases (_,po,a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index b2da272a3..367fd5e0e 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -173,7 +173,7 @@ GEXTEND Gram COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) ] | "0" RIGHTA [ "?" -> CHole loc - | "?"; n = Prim.natural -> CMeta (loc, n) + | "?"; n = Prim.natural -> CPatVar (loc, (false,Pattern.patvar_of_int n)) | bll = binders; c = constr -> abstract_constr loc c bll (* Hack to parse syntax "(n)" as a natural number *) | "("; test_int_rparen; n = bigint; ")" -> @@ -195,8 +195,8 @@ GEXTEND Gram | "("; lc1 = lconstr; ")" -> lc1 | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" -> (match lc1 with - | CMeta (loc2,n) -> - CApp (loc,CMeta (loc2, -n), List.map (fun c -> c, None) cl) + | CPatVar (loc2,(false,n)) -> + CApp (loc,CPatVar (loc2, (true,n)), List.map (fun c -> c, None) cl) | _ -> Util.error "Second-order pattern-matching expects a head metavariable") | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" -> diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index ffc7d403c..a0bd0fb5e 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -179,7 +179,7 @@ GEXTEND Gram | s=sort -> CSort(loc,s) | n=INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n)) | IDENT "_" -> CHole loc - | "?"; n=Prim.natural -> CMeta(loc,n) ] ] + | "?"; n=Prim.natural -> CPatVar(loc,(false,Pattern.patvar_of_int n)) ] ] ; fix_constr: [ [ kw=fix_kw; dcl=fix_decl -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index f5309fa39..5c74f4ef6 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -230,7 +230,7 @@ GEXTEND Gram | n = integer -> Integer n | id = METAIDENT -> MetaIdArg (loc,id) | "?" -> ConstrMayEval (ConstrTerm (CHole loc)) - | "?"; n = natural -> ConstrMayEval (ConstrTerm (CMeta (loc,n))) + | "?"; n = natural -> ConstrMayEval (ConstrTerm (CPatVar (loc,(false,Pattern.patvar_of_int n)))) | "'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 945009ae9..b364bb874 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -136,7 +136,7 @@ GEXTEND Gram tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) | r = reference -> Reference r - | "?"; n = natural -> ConstrMayEval (ConstrTerm (CMeta (loc,n))) + | "?"; n = natural -> ConstrMayEval (ConstrTerm (CPatVar (loc,(false,Pattern.patvar_of_int n)))) | "()" -> TacVoid ] ] ; input_fun: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 862bbd3dd..62f2300a7 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -82,15 +82,15 @@ GEXTEND Gram [ [ a0 = autoarg_depth; l = autoarg_adding; a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ] ; - (* Either an hypothesis or a ltac ref (variable or pattern metavariable) *) + (* Either an hypothesis or a ltac ref (variable or pattern patvar) *) id_or_ltac_ref: [ [ id = base_ident -> Genarg.AN id - | "?"; n = natural -> Genarg.MetaNum (loc,n) ] ] + | "?"; n = natural -> Genarg.MetaNum (loc,Pattern.patvar_of_int n) ] ] ; - (* Either a global ref or a ltac ref (variable or pattern metavariable) *) + (* Either a global ref or a ltac ref (variable or pattern patvar) *) global_or_ltac_ref: [ [ qid = global -> AN qid - | "?"; n = natural -> MetaNum (loc,n) ] ] + | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index f5a0f851e..fb6e213a4 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -95,15 +95,15 @@ GEXTEND Gram [ [ a0 = autoarg_depth; l = autoarg_adding; a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ] ; - (* Either an hypothesis or a ltac ref (variable or pattern metavariable) *) + (* Either an hypothesis or a ltac ref (variable or pattern patvar) *) id_or_ltac_ref: [ [ id = base_ident -> AN id - | "?"; n = natural -> MetaNum (loc,n) ] ] + | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ] ; - (* Either a global ref or a ltac ref (variable or pattern metavariable) *) + (* Either a global ref or a ltac ref (variable or pattern patvar) *) global_or_ltac_ref: [ [ qid = global -> AN qid - | "?"; n = natural -> MetaNum (loc,n) ] ] + | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index d716e773b..72a693012 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -20,6 +20,7 @@ open Coqast open Ppextend open Topconstr open Term +open Pattern (*i*) let latom = 0 @@ -275,7 +276,8 @@ let rec pr inherited a = | COrderedCase (_,_,_,_,_) -> anomaly "malformed if or destructuring let" | CHole _ -> str "?", latom - | CMeta (_,p) -> str "?" ++ int p, latom + | CEvar (_,n) -> str "?" ++ int n, latom + | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_sort s, latom | CCast (_,a,b) -> hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 7b1ccb511..8e6d63c2d 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -18,6 +18,7 @@ open Rawterm open Topconstr open Genarg open Libnames +open Pattern let pr_red_expr = Ppconstr.pr_red_expr let pr_may_eval = Ppconstr.pr_may_eval @@ -84,7 +85,7 @@ let pr_arg pr x = spc () ++ pr x let pr_or_metanum pr = function | AN x -> pr x - | MetaNum (_,n) -> str "?" ++ int n + | MetaNum (_,n) -> str "?" ++ pr_patvar n let pr_or_var pr = function | ArgArg x -> pr x diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index f79148911..495e2eaff 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -147,7 +147,7 @@ let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) let mlexpr_of_or_metanum f = function | Genarg.AN a -> <:expr< Genarg.AN $f a$ >> | Genarg.MetaNum (_,n) -> - <:expr< Genarg.MetaNum $dloc$ $mlexpr_of_int n$ >> + <:expr< Genarg.MetaNum $dloc$ $mlexpr_of_ident n$ >> let mlexpr_of_or_metaid f = function | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> @@ -204,7 +204,8 @@ let rec mlexpr_of_constr = function | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >> - | Topconstr.CMeta (loc,n) -> <:expr< Topconstr.CMeta $dloc$ $mlexpr_of_int n$ >> + | Topconstr.CPatVar (loc,n) -> + <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> | _ -> failwith "mlexpr_of_constr: TODO" let mlexpr_of_occ_constr = diff --git a/parsing/termast.ml b/parsing/termast.ml index e9892758b..9f09c14be 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -190,7 +190,7 @@ let rec ast_of_raw = function | RRef (_,ref) -> ast_of_ref ref | RVar (_,id) -> ast_of_ident id | REvar (_,n) -> ast_of_existential_ref n - | RMeta (_,n) -> ope("META",[num n]) + | RPatVar (_,(_,n)) -> ope("META",[ast_of_ident n]) | RApp (_,f,args) -> let (f,args) = skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in @@ -379,7 +379,7 @@ let rec ast_of_pattern tenv env = function | _ -> ast_of_app [] astf astargs) | PSoApp (n,args) -> - ope("SOAPP",(ope ("META",[num n])):: + ope("SOAPP",(ope ("META",[ast_of_ident n])):: (List.map (ast_of_pattern tenv env) args)) | PLetIn (na,b,c) -> @@ -420,7 +420,7 @@ let rec ast_of_pattern tenv env = function | RProp Pos -> ope("SET",[]) | RType _ -> ope("TYPE",[])) - | PMeta (Some n) -> ope("META",[num n]) + | PMeta (Some n) -> ope("META",[ast_of_ident n]) | PMeta None -> ope("ISEVAR",[]) | PFix f -> ast_of_raw (Detyping.detype tenv [] env (mkFix f)) | PCoFix c -> ast_of_raw (Detyping.detype tenv [] env (mkCoFix c)) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index bd38d5c86..c24748970 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -261,7 +261,7 @@ type tomatch_status = type tomatch_stack = tomatch_status list -(* Warning: PrLetIn takes a parallel substitution as argument *) +(* Warning: PrLetIn takes a parallel bindings as argument *) type predicate_signature = | PrLetIn of (constr list * constr option) * predicate_signature @@ -600,7 +600,7 @@ let occur_rawconstr id = (array_exists occur tyl) or (not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv) | RCast (loc,c,t) -> (occur c) or (occur t) - | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) -> false + | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -1025,7 +1025,7 @@ let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0 let substnl_predicate sigma = map_predicate (substnl sigma) -(* This is parallel substitution *) +(* This is parallel bindings *) let subst_predicate (args,copt) pred = let sigma = match copt with | None -> List.rev args @@ -1144,7 +1144,7 @@ let specialize_predicate tomatchs deps cs = function let argsi = Array.to_list cs.cs_concl_realargs in let copti = option_app (fun _ -> build_dependent_constructor cs) copt in (* The substituends argsi, copti are all defined in gamma, x1...xn *) - (* We *need _parallel_ substitution to get gamma, x1...xn |- pred'' *) + (* We *need _parallel_ bindings to get gamma, x1...xn |- pred'' *) let pred'' = subst_predicate (argsi, copti) pred' in (* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *) let pred''' = liftn_predicate n (n+1) pred'' in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2599e2958..58d461e57 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -27,12 +27,12 @@ open Esubst * in normal form and neutral (i.e. not a lambda, a construct or a * (co)fix, because they may produce redexes by applying them, * or putting them in a case) - * LAM(x,a,b,S) is the term [S]([x:a]b). the substitution is propagated + * LAM(x,a,b,S) is the term [S]([x:a]b). the bindings is propagated * only when the abstraction is applied, and then we use the rule * ([S]([x:a]b) c) --> [S.c]b * This corresponds to the usual strategy of weak reduction * FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under - * the substitution S, and then applied to args. Here again, + * the bindings S, and then applied to args. Here again, * weak reduction. * CONSTR(c,args) is the constructor [c] applied to [args]. * @@ -67,8 +67,8 @@ let rec shift_value n = function CONSTR (c, List.map (shift_value n) args) -(* Contracts a fixpoint: given a fixpoint and a substitution, - * returns the corresponding fixpoint body, and the substitution in which +(* Contracts a fixpoint: given a fixpoint and a bindings, + * returns the corresponding fixpoint body, and the bindings in which * it should be evaluated: its first variables are the fixpoint bodies * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1})) * -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti) @@ -204,7 +204,7 @@ let rec norm_head info env t stack = | LetIn (x, b, t, c) -> (* zeta means letin are contracted; delta without zeta means we *) - (* allow substitution but leave let's in place *) + (* allow bindings but leave let's in place *) let zeta = red_set (info_flags info) fZETA in let env' = if zeta diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b4af4821d..b9751dbc7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -204,7 +204,9 @@ let rec detype tenv avoid env t = with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in RVar (dummy_loc, id_of_string s)) - | Meta n -> RMeta (dummy_loc, n) + | Meta n -> + (* Meta in constr are not user-parsable and are mapped to Evar *) + REvar (dummy_loc, n) | Var id -> (try let _ = Global.lookup_named id in RRef (dummy_loc, VarRef id) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 9d65430ed..13ed8e8f6 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -366,7 +366,7 @@ let evar_define isevars (ev,argsv) rhs = then error_occur_check empty_env (evars_of isevars) ev rhs; let args = Array.to_list argsv in let evd = ise_map isevars ev in - (* the substitution to invert *) + (* the bindings to invert *) let worklist = make_subst (evar_env evd) args in let body = real_clean isevars ev worklist rhs in ise_define isevars ev body; diff --git a/pretyping/matching.ml b/pretyping/matching.ml index caecbf455..b42365679 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -45,7 +45,7 @@ open Pattern exception PatternMatchingFailure -let constrain ((n : int),(m : constr)) sigma = +let constrain (n,m) sigma = if List.mem_assoc n sigma then if eq_constr m (List.assoc n sigma) then sigma else raise PatternMatchingFailure @@ -169,11 +169,13 @@ let authorized_occ nocc mres = if nocc = 0 then mres else raise (NextOccurrence nocc) +let special_meta = (-1) + (* Tries to match a subterm of [c] with [pat] *) let rec sub_match nocc pat c = match kind_of_term c with | Cast (c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1] in (lm,mkCast (List.hd lc, c2)) @@ -181,7 +183,7 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in (lm,mkCast (List.hd lc, c2))) | Lambda (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1;c2] in (lm,mkLambda (x,List.hd lc,List.nth lc 1)) @@ -189,7 +191,7 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in (lm,mkLambda (x,List.hd lc,List.nth lc 1))) | Prod (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1;c2] in (lm,mkProd (x,List.hd lc,List.nth lc 1)) @@ -197,7 +199,7 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in (lm,mkProd (x,List.hd lc,List.nth lc 1))) | LetIn (x,c1,t2,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)) @@ -205,7 +207,7 @@ let rec sub_match nocc pat c = let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))) | App (c1,lc) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in (lm,mkApp (List.hd le, Array.of_list (List.tl le))) @@ -213,7 +215,7 @@ let rec sub_match nocc pat c = let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in (lm,mkApp (List.hd le, Array.of_list (List.tl le)))) | Case (ci,hd,c1,lc) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with + (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) @@ -222,7 +224,7 @@ let rec sub_match nocc pat c = (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))) | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with + (try authorized_occ nocc ((matches pat c),mkMeta special_meta) with | PatternMatchingFailure -> raise (NextOccurrence nocc) | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 5a789b442..32c2906b6 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -13,38 +13,37 @@ open Names open Term open Environ open Pattern +open Termops (*i*) (*s This modules implements pattern-matching on terms *) exception PatternMatchingFailure +val special_meta : metavariable + (* [matches pat c] matches [c] against [pat] and returns the resulting assignment of metavariables; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) -val matches : - constr_pattern -> constr -> (int * constr) list +val matches : constr_pattern -> constr -> patvar_map (* [is_matching pat c] just tells if [c] matches against [pat] *) -val is_matching : - constr_pattern -> constr -> bool +val is_matching : constr_pattern -> constr -> bool (* [matches_conv env sigma] matches up to conversion in environment [(env,sigma)] when constants in pattern are concerned; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) -val matches_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> (int * constr) list +val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (* To skip to the next occurrence *) exception NextOccurrence of int (* Tries to match a subterm of [c] with [pat] *) -val sub_match : - int -> constr_pattern -> constr -> ((int * constr) list * constr) +val sub_match : int -> constr_pattern -> constr -> patvar_map * constr (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] up to conversion for constants in patterns *) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 9dafda587..5ad06a6e5 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -18,18 +18,26 @@ open Environ open Nametab open Pp +(* Metavariables *) + +type patvar_map = (patvar * constr) list +let patvar_of_int n = Names.id_of_string (string_of_int n) +let pr_patvar = pr_id + +(* Patterns *) + type constr_pattern = | PRef of global_reference | PVar of identifier | PEvar of existential_key | PRel of int | PApp of constr_pattern * constr_pattern array - | PSoApp of int * constr_pattern list + | PSoApp of patvar * constr_pattern list | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern | PSort of rawsort - | PMeta of int option + | PMeta of patvar option | PCase of case_style * constr_pattern option * constr_pattern * constr_pattern array | PFix of fixpoint @@ -151,7 +159,7 @@ let head_of_constr_reference c = match kind_of_term c with let rec pattern_of_constr t = match kind_of_term t with | Rel n -> PRel n - | Meta n -> PMeta (Some n) + | Meta n -> PMeta (Some (id_of_string (string_of_int n))) | Var id -> PVar id | Sort (Prop c) -> PSort (RProp c) | Sort (Type _) -> PSort (RType None) @@ -197,13 +205,13 @@ let rec pat_of_raw metas vars = function | RVar (_,id) -> (try PRel (list_index (Name id) vars) with Not_found -> PVar id) - | RMeta (_,n) -> + | RPatVar (_,(false,n)) -> metas := n::!metas; PMeta (Some n) | RRef (_,r) -> PRef r (* Hack pour ne pas réécrire une interprétation complète des patterns*) - | RApp (_, RMeta (_,n), cl) when n<0 -> - PSoApp (- n, List.map (pat_of_raw metas vars) cl) + | RApp (_, RPatVar (_,(true,n)), cl) -> + PSoApp (n, List.map (pat_of_raw metas vars) cl) | RApp (_,c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 11821a6a8..535ca8c01 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -9,26 +9,36 @@ (*i $Id$ i*) (*i*) +open Pp open Names open Sign open Term open Environ open Libnames open Nametab +open Rawterm (*i*) +(* Pattern variables *) + +type patvar_map = (patvar * constr) list +val patvar_of_int : int -> patvar +val pr_patvar : patvar -> std_ppcmds + +(* Patterns *) + type constr_pattern = | PRef of global_reference | PVar of identifier | PEvar of existential_key | PRel of int | PApp of constr_pattern * constr_pattern array - | PSoApp of int * constr_pattern list + | PSoApp of patvar * constr_pattern list | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of Rawterm.rawsort - | PMeta of int option + | PSort of rawsort + | PMeta of patvar option | PCase of case_style * constr_pattern option * constr_pattern * constr_pattern array | PFix of fixpoint @@ -71,7 +81,8 @@ val pattern_of_constr : constr -> constr_pattern a pattern; variables bound in [l] are replaced by the pattern to which they are bound *) -val pattern_of_rawconstr : Rawterm.rawconstr -> int list * constr_pattern +val pattern_of_rawconstr : rawconstr -> + patvar list * constr_pattern val instantiate_pattern : (identifier * constr_pattern) list -> constr_pattern -> constr_pattern diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e4714468a..f94c14e71 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,6 +28,7 @@ open Pretype_errors open Rawterm open Evarconv open Coercion +open Pattern open Dyn @@ -151,7 +152,13 @@ let evar_type_case isevars env ct pt lft p c = in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) *) -let pretype_id loc env lvar id = +let strip_meta id = (* For Grammar v7 compatibility *) + let s = string_of_id id in + if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1)) + else id + +let pretype_id loc env lvar id = + let id = strip_meta id in (* May happen in tactics defined by Grammar *) try List.assoc id lvar with Not_found -> @@ -217,7 +224,8 @@ let rec pretype tycon env isevars lvar lmeta = function let j = (Retyping.get_judgment_of env (evars_of isevars) c) in inh_conv_coerce_to_tycon loc env isevars j tycon - | RMeta (loc,n) -> + | RPatVar (loc,(someta,n)) -> + assert (not someta); let j = try List.assoc n lmeta @@ -225,7 +233,7 @@ let rec pretype tycon env isevars lvar lmeta = function Not_found -> user_err_loc (loc,"pretype", - str "Metavariable " ++ int n ++ str " is unbound") + str "Metavariable " ++ pr_patvar n ++ str " is unbound") in inh_conv_coerce_to_tycon loc env isevars j tycon | RHole (loc,k) -> @@ -618,7 +626,7 @@ let ise_infer_type_gen fail_evar sigma env lvar lmeta c = check_evars fail_evar env sigma isevars tj.utj_val; (evars_of isevars, tj) -type meta_map = (int * unsafe_judgment) list +type meta_map = (patvar * unsafe_judgment) list type var_map = (identifier * unsafe_judgment) list let understand_judgment sigma env c = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index dadc8b94c..e6dc58896 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -18,7 +18,7 @@ open Rawterm open Evarutil (*i*) -type meta_map = (int * unsafe_judgment) list +type meta_map = (patvar * unsafe_judgment) list type var_map = (identifier * unsafe_judgment) list (* constr with holes *) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 0dcf90188..3e13cd861 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -31,6 +31,8 @@ let pattern_loc = function PatVar(loc,_) -> loc | PatCstr(loc,_,_,_) -> loc +type patvar = identifier + type rawsort = RProp of Term.contents | RType of Univ.universe option type fix_kind = RFix of (int array * int) | RCoFix of int @@ -39,14 +41,14 @@ type binder_kind = BProd | BLambda | BLetIn type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier -type 'a explicit_substitution = (loc * quantified_hypothesis * 'a) list +type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list -type 'a substitution = +type 'a bindings = | ImplicitBindings of 'a list - | ExplicitBindings of 'a explicit_substitution + | ExplicitBindings of 'a explicit_bindings | NoBindings -type 'a with_bindings = 'a * 'a substitution +type 'a with_bindings = 'a * 'a bindings type hole_kind = | ImplicitArg of global_reference * int @@ -60,7 +62,7 @@ type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) | REvar of loc * existential_key - | RMeta of loc * int + | RPatVar of loc * (bool * patvar) (* Used for patterns only *) | RApp of loc * rawconstr * rawconstr list | RLambda of loc * name * rawconstr * rawconstr | RProd of loc * name * rawconstr * rawconstr @@ -101,7 +103,7 @@ let loc = function | RHole (loc,_) -> loc | RRef (loc,_) -> loc | REvar (loc,_) -> loc - | RMeta (loc,_) -> loc + | RPatVar (loc,_) -> loc | RDynamic (loc,_) -> loc let map_rawconstr f = function @@ -117,7 +119,7 @@ let map_rawconstr f = function ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv) | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv) | RCast (loc,c,t) -> RCast (loc,f c,f t) - | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) as x -> x + | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x (* let name_app f e = function @@ -155,7 +157,7 @@ let map_rawconstr_with_binders_loc loc g f e = function | RHole (_,x) -> RHole (loc,x) | RRef (_,x) -> RRef (loc,x) | REvar (_,x) -> REvar (loc,x) - | RMeta (_,x) -> RMeta (loc,x) + | RPatVar (_,x) -> RPatVar (loc,x) | RDynamic (_,x) -> RDynamic (loc,x) *) @@ -177,7 +179,7 @@ let rec subst_raw subst raw = | RVar _ -> raw | REvar _ -> raw - | RMeta _ -> raw + | RPatVar _ -> raw | RApp (loc,r,rl) -> let r' = subst_raw subst r @@ -247,7 +249,7 @@ let loc_of_rawconstr = function | RRef (loc,_) -> loc | RVar (loc,_) -> loc | REvar (loc,_) -> loc - | RMeta (loc,_) -> loc + | RPatVar (loc,_) -> loc | RApp (loc,_,_) -> loc | RLambda (loc,_,_,_) -> loc | RProd (loc,_,_,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 293667aed..fbd01db9a 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -29,6 +29,8 @@ type cases_pattern = val pattern_loc : cases_pattern -> loc +type patvar = identifier + type rawsort = RProp of Term.contents | RType of Univ.universe option type fix_kind = RFix of (int array * int) | RCoFix of int @@ -37,14 +39,14 @@ type binder_kind = BProd | BLambda | BLetIn type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier -type 'a explicit_substitution = (loc * quantified_hypothesis * 'a) list +type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list -type 'a substitution = +type 'a bindings = | ImplicitBindings of 'a list - | ExplicitBindings of 'a explicit_substitution + | ExplicitBindings of 'a explicit_bindings | NoBindings -type 'a with_bindings = 'a * 'a substitution +type 'a with_bindings = 'a * 'a bindings type hole_kind = | ImplicitArg of global_reference * int @@ -58,7 +60,7 @@ type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) | REvar of loc * existential_key - | RMeta of loc * int + | RPatVar of loc * (bool * patvar) (* Used for patterns only *) | RApp of loc * rawconstr * rawconstr list | RLambda of loc * name * rawconstr * rawconstr | RProd of loc * name * rawconstr * rawconstr diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b2d60176d..9b51abff3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -76,7 +76,7 @@ let rec strong_prodspine redfun c = | _ -> x (*************************************) -(*** Reduction using substitutions ***) +(*** Reduction using bindingss ***) (*************************************) (* This signature is very similar to Closure.RedFlagsSig except there diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 5cf0bfd91..d2f260b7b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -192,9 +192,9 @@ val is_fconv : conv_pb -> env -> evar_map -> constr -> constr -> bool (*s Special-Purpose Reduction Functions *) -val whd_meta : (int * constr) list -> constr -> constr -val plain_instance : (int * constr) list -> constr -> constr -val instance : (int * constr) list -> constr -> constr +val whd_meta : (metavariable * constr) list -> constr -> constr +val plain_instance : (metavariable * constr) list -> constr -> constr +val instance : (metavariable * constr) list -> constr -> constr (*s Obsolete Reduction Functions *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index aa5d27d20..43218ca72 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -18,8 +18,6 @@ open Typeops open Declarations open Instantiate -type metamap = (int * constr) list - let outsort env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with | Sort s -> s diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index cec8c5f9d..d7c1c516e 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -13,6 +13,8 @@ open Names open Term open Evd open Environ +open Pattern +open Termops (*i*) (* This family of functions assumes its constr argument is known to be @@ -21,8 +23,6 @@ open Environ either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too. *) -type metamap = (int * constr) list - val get_type_of : env -> evar_map -> constr -> constr val get_sort_of : env -> evar_map -> types -> sorts val get_sort_family_of : env -> evar_map -> types -> sorts_family diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7dc78cbe6..13fefd306 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -623,7 +623,7 @@ let contextually (locs,c) f env sigma t = errorlabstrm "contextually" (str "Too few occurences"); t' -(* linear substitution (following pretty-printer) of the value of name in c. +(* linear bindings (following pretty-printer) of the value of name in c. * n is the number of the next occurence of name. * ol is the occurence list to find. *) let rec substlin env name n ol c = diff --git a/pretyping/termops.ml b/pretyping/termops.ml index a41631bd2..080ed4374 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -18,6 +18,8 @@ open Environ open Libnames open Nametab +(* Sorts and sort family *) + let print_sort = function | Prop Pos -> (str "Set") | Prop Null -> (str "Prop") @@ -399,9 +401,11 @@ let dependent m t = let pop t = lift (-1) t (***************************) -(* substitution functions *) +(* bindings functions *) (***************************) +type metamap = (metavariable * constr) list + let rec subst_meta bl c = match kind_of_term c with | Meta i -> (try List.assoc i bl with Not_found -> c) @@ -473,7 +477,7 @@ let replace_term = replace_term_gen eq_constr (* Substitute only a list of locations locs, the empty list is interpreted as substitute all, if 0 is in the list then no - substitution is done. The list may contain only negative occurrences + bindings is done. The list may contain only negative occurrences that will not be substituted. *) let subst_term_occ_gen locs occ c t = @@ -697,9 +701,15 @@ let occur_id env nenv id0 c = with Occur -> true | Not_found -> false (* Case when a global is not in the env *) +let is_section_variable id = + try let _ = Declare.find_section_variable id in true with Not_found -> false + let next_name_not_occuring env name l env_names t = let rec next id = - if List.mem id l or occur_id env env_names id t then next (lift_ident id) + if List.mem id l or occur_id env env_names id t or + (* To be consistent with intro mechanism *) + (Declare.is_global id & not (is_section_variable id)) + then next (lift_ident id) else id in match name with diff --git a/pretyping/termops.mli b/pretyping/termops.mli index cd5d7def0..216a090c4 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -86,12 +86,13 @@ val occur_term : constr -> constr -> bool val free_rels : constr -> Intset.t (* Substitution of metavariables *) -val subst_meta : (int * constr) list -> constr -> constr +type metamap = (metavariable * constr) list +val subst_meta : metamap -> constr -> constr (* [pop c] lifts by -1 the positive indexes in [c] *) val pop : constr -> constr -(* substitution of an arbitrary large term. Uses equality modulo +(* bindings of an arbitrary large term. Uses equality modulo reduction of let *) val dependent : constr -> constr -> bool val subst_term_gen : diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0ac1f4ecb..eb91ade44 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -26,6 +26,7 @@ open Reductionops open Tacmach open Evar_refiner open Rawterm +open Pattern open Tacexpr (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, @@ -52,9 +53,9 @@ let abstract_list_all env sigma typ c l = raise (RefinerError (CannotGeneralize typ)) (* Generator of metavariables *) -let meta_ctr = ref 0;; - -let new_meta () = incr meta_ctr;!meta_ctr;; +let new_meta = + let meta_ctr = ref 0 in + fun () -> incr meta_ctr; !meta_ctr (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) @@ -71,10 +72,24 @@ let exist_to_meta sigma (emap, c) = | _ -> map_constr replace c in (!metamap, replace c) +module Metaset = Intset + +module Metamap = Intmap + +let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false + +let metamap_in_dom x m = + try let _ = Metamap.find x m in true with Not_found -> false + +let metamap_to_list m = + Metamap.fold (fun n v l -> (n,v)::l) m [] + +let metamap_inv m b = + Metamap.fold (fun n v l -> if v = b then n::l else l) m [] type 'a freelisted = { rebus : 'a; - freemetas : Intset.t } + freemetas : Metaset.t } (* collects all metavar occurences, in left-to-right order, preserving * repetitions and all. *) @@ -90,10 +105,10 @@ let collect_metas c = let metavars_of c = let rec collrec acc c = match kind_of_term c with - | Meta mv -> Intset.add mv acc + | Meta mv -> Metaset.add mv acc | _ -> fold_constr collrec acc c in - collrec Intset.empty c + collrec Metaset.empty c let mk_freelisted c = { rebus = c; freemetas = metavars_of c } @@ -108,8 +123,8 @@ type clbinding = type 'a clausenv = { templval : constr freelisted; templtyp : constr freelisted; - namenv : identifier Intmap.t; - env : clbinding Intmap.t; + namenv : identifier Metamap.t; + env : clbinding Metamap.t; hook : 'a } type wc = named_context sigma @@ -122,9 +137,9 @@ type wc = named_context sigma let mentions clenv mv0 = let rec menrec mv1 = try - (match Intmap.find mv1 clenv.env with + (match Metamap.find mv1 clenv.env with | Clval (b,_) -> - Intset.mem mv0 b.freemetas || intset_exists menrec b.freemetas + Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas | Cltyp _ -> false) with Not_found -> false @@ -141,8 +156,8 @@ let mk_clenv wc cty = let cty_fls = mk_freelisted cty in { templval = mk_freelisted (mkMeta mv); templtyp = cty_fls; - namenv = Intmap.empty; - env = Intmap.add mv (Cltyp cty_fls) Intmap.empty ; + namenv = Metamap.empty; + env = Metamap.add mv (Cltyp cty_fls) Metamap.empty ; hook = wc } let clenv_environments bound c = @@ -158,23 +173,23 @@ let clenv_environments bound c = match na with | Anonymous -> ne | Name id -> - if intmap_in_dom mv ne then begin - warning ("Cannot put metavar "^(string_of_int mv)^ + if metamap_in_dom mv ne then begin + warning ("Cannot put metavar "^(string_of_meta mv)^ " in name-environment twice"); ne end else - Intmap.add mv id ne + Metamap.add mv id ne else ne in - let e' = Intmap.add mv (Cltyp (mk_freelisted c1)) e in + let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) c2) else c2) | (n, LetIn (na,b,_,c)) -> clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c) | (n, _) -> (ne, e, List.rev metas, c) in - clrec (Intmap.empty,Intmap.empty,[]) bound c + clrec (Metamap.empty,Metamap.empty,[]) bound c let mk_clenv_from_n wc n (c,cty) = let (namenv,env,args,concl) = clenv_environments n cty in @@ -196,7 +211,7 @@ let subst_clenv f sub clenv = { templval = map_fl (subst_mps sub) clenv.templval; templtyp = map_fl (subst_mps sub) clenv.templtyp; namenv = clenv.namenv; - env = Intmap.map (map_clb (subst_mps sub)) clenv.env; + env = Metamap.map (map_clb (subst_mps sub)) clenv.env; hook = f sub clenv.hook } let connect_clenv wc clenv = { clenv with hook = wc } @@ -229,15 +244,15 @@ let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t) let clenv_assign mv rhs clenv = let rhs_fls = mk_freelisted rhs in - if intset_exists (mentions clenv mv) rhs_fls.freemetas then + if meta_exists (mentions clenv mv) rhs_fls.freemetas then error "clenv__assign: circularity in unification"; try - (match Intmap.find mv clenv.env with + (match Metamap.find mv clenv.env with | Clval (fls,ty) -> if not (eq_constr fls.rebus rhs) then try (* Streams are lazy, force evaluation of id to catch Not_found*) - let id = Intmap.find mv clenv.namenv in + let id = Metamap.find mv clenv.namenv in errorlabstrm "clenv_assign" (str "An incompatible instantiation has already been found for " ++ pr_id id) @@ -249,7 +264,7 @@ let clenv_assign mv rhs clenv = { templval = clenv.templval; templtyp = clenv.templtyp; namenv = clenv.namenv; - env = Intmap.add mv (Clval (rhs_fls,bty)) clenv.env; + env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env; hook = clenv.hook }) with Not_found -> error "clenv_assign" @@ -257,11 +272,11 @@ let clenv_assign mv rhs clenv = let clenv_val_of clenv mv = let rec valrec mv = try - (match Intmap.find mv clenv.env with + (match Metamap.find mv clenv.env with | Cltyp _ -> mkMeta mv | Clval(b,_) -> instance (List.map (fun mv' -> (mv',valrec mv')) - (Intset.elements b.freemetas)) b.rebus) + (Metaset.elements b.freemetas)) b.rebus) with Not_found -> mkMeta mv in @@ -270,7 +285,7 @@ let clenv_val_of clenv mv = let clenv_instance clenv b = let c_sigma = List.map - (fun mv -> (mv,clenv_val_of clenv mv)) (Intset.elements b.freemetas) + (fun mv -> (mv,clenv_val_of clenv mv)) (Metaset.elements b.freemetas) in instance c_sigma b.rebus @@ -295,7 +310,7 @@ let clenv_cast_meta clenv = match kind_of_term (strip_outer_cast u) with | Meta mv -> (try - match Intmap.find mv clenv.env with + match Metamap.find mv clenv.env with | Cltyp b -> let b' = clenv_instance clenv b in if occur_meta b' then u else mkCast (mkMeta mv, b') @@ -319,24 +334,24 @@ let clenv_cast_meta clenv = let clenv_pose (na,mv,cty) clenv = { templval = clenv.templval; templtyp = clenv.templtyp; - env = Intmap.add mv (Cltyp (mk_freelisted cty)) clenv.env; + env = Metamap.add mv (Cltyp (mk_freelisted cty)) clenv.env; namenv = (match na with | Anonymous -> clenv.namenv - | Name id -> Intmap.add mv id clenv.namenv); + | Name id -> Metamap.add mv id clenv.namenv); hook = clenv.hook } let clenv_defined clenv mv = - match Intmap.find mv clenv.env with + match Metamap.find mv clenv.env with | Clval _ -> true | Cltyp _ -> false let clenv_value clenv mv = - match Intmap.find mv clenv.env with + match Metamap.find mv clenv.env with | Clval(b,_) -> b | Cltyp _ -> failwith "clenv_value" let clenv_type clenv mv = - match Intmap.find mv clenv.env with + match Metamap.find mv clenv.env with | Cltyp b -> b | Clval(_,b) -> b @@ -369,7 +384,7 @@ let clenv_type_of ce c = (function | (n,Clval(_,typ)) -> (n,typ.rebus) | (n,Cltyp typ) -> (n,typ.rebus)) - (intmap_to_list ce.env) + (metamap_to_list ce.env) in Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c @@ -854,15 +869,15 @@ let clenv_bchain mv subclenv clenv = List.fold_left (fun ne (mv,id) -> if clenv_defined subclenv mv then ne - else if intmap_in_dom mv ne then begin - warning ("Cannot put metavar "^(string_of_int mv)^ + else if metamap_in_dom mv ne then begin + warning ("Cannot put metavar "^(string_of_meta mv)^ " in name-environment twice"); ne end else - Intmap.add mv id ne) - clenv.namenv (intmap_to_list subclenv.namenv); - env = List.fold_left (fun m (n,v) -> Intmap.add n v m) - clenv.env (intmap_to_list subclenv.env); + Metamap.add mv id ne) + clenv.namenv (metamap_to_list subclenv.namenv); + env = List.fold_left (fun m (n,v) -> Metamap.add n v m) + clenv.env (metamap_to_list subclenv.env); hook = clenv.hook } in (* unify the type of the template of [subclenv] with the type of [mv] *) @@ -916,7 +931,7 @@ let clenv_refine_cast kONT clenv gls = * the metavar mv. The list is unordered. *) let clenv_metavars clenv mv = - match Intmap.find mv clenv.env with + match Metamap.find mv clenv.env with | Clval(_,b) -> b.freemetas | Cltyp b -> b.freemetas @@ -933,7 +948,7 @@ let clenv_template_metavars clenv = clenv.templval.freemetas let dependent_metas clenv mvs conclmetas = List.fold_right (fun mv deps -> - Intset.union deps (clenv_metavars clenv mv)) + Metaset.union deps (clenv_metavars clenv mv)) mvs conclmetas let clenv_dependent hyps_only clenv = @@ -941,7 +956,7 @@ let clenv_dependent hyps_only clenv = let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in let deps = dependent_metas clenv mvs ctyp_mvs in List.filter - (fun mv -> Intset.mem mv deps && not (hyps_only && Intset.mem mv ctyp_mvs)) + (fun mv -> Metaset.mem mv deps && not (hyps_only && Metaset.mem mv ctyp_mvs)) mvs let clenv_missing c = clenv_dependent true c @@ -956,7 +971,7 @@ let clenv_independent clenv = let mvs = collect_metas (clenv_instance_template clenv) in let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in let deps = dependent_metas clenv mvs ctyp_mvs in - List.filter (fun mv -> not (Intset.mem mv deps)) mvs + List.filter (fun mv -> not (Metaset.mem mv deps)) mvs let w_coerce wc c ctyp target = let j = make_judge c ctyp in @@ -990,7 +1005,7 @@ let clenv_constrain_missing_args mlist clause = clenv_constrain_dep_args true clause mlist let clenv_lookup_name clenv id = - match intmap_inv clenv.namenv id with + match metamap_inv clenv.namenv id with | [] -> errorlabstrm "clenv_lookup_name" (str"No such bound variable " ++ pr_id id) @@ -1136,16 +1151,18 @@ open Printer let pr_clenv clenv = let pr_name mv = try - let id = Intmap.find mv clenv.namenv in + let id = Metamap.find mv clenv.namenv in (str"[" ++ pr_id id ++ str"]") with Not_found -> (mt ()) in let pr_meta_binding = function | (mv,Cltyp b) -> - hov 0 (int mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ()) + hov 0 + (pr_meta mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ()) | (mv,Clval(b,_)) -> - hov 0 (int mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ()) + hov 0 + (pr_meta mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ()) in (str"TEMPL: " ++ prterm clenv.templval.rebus ++ str" : " ++ prterm clenv.templtyp.rebus ++ fnl () ++ - (prlist pr_meta_binding (intmap_to_list clenv.env))) + (prlist pr_meta_binding (metamap_to_list clenv.env))) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 3e39fc3e6..3babd9224 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -17,19 +17,22 @@ open Proof_type (*i*) (* [new_meta] is a generator of unique meta variables *) -val new_meta : unit -> int +val new_meta : unit -> metavariable (* [exist_to_meta] generates new metavariables for each existential and performs the replacement in the given constr *) val exist_to_meta : - Evd.evar_map -> Pretyping.open_constr -> - ((int * types) list * constr) + Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr) (* The Type of Constructions clausale environments. *) +module Metaset : Set.S with type elt = metavariable + +module Metamap : Map.S with type key = metavariable + type 'a freelisted = { rebus : 'a; - freemetas : Intset.t } + freemetas : Metaset.t } type clbinding = | Cltyp of constr freelisted @@ -38,8 +41,8 @@ type clbinding = type 'a clausenv = { templval : constr freelisted; templtyp : constr freelisted; - namenv : identifier Intmap.t; - env : clbinding Intmap.t; + namenv : identifier Metamap.t; + env : clbinding Metamap.t; hook : 'a } type wc = named_context sigma (* for a better reading of the following *) @@ -53,7 +56,7 @@ type wc = named_context sigma (* for a better reading of the following *) * [hook] is the pointer to the current walking context, for * integrating existential vars and metavars. *) -val collect_metas : constr -> int list +val collect_metas : constr -> metavariable list val mk_clenv : 'a -> constr -> 'a clausenv val mk_clenv_from : 'a -> constr * constr -> 'a clausenv val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv @@ -67,46 +70,46 @@ val subst_clenv : (substitution -> 'a -> 'a) -> val connect_clenv : wc -> 'a clausenv -> wc clausenv val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv -val clenv_assign : int -> constr -> 'a clausenv -> 'a clausenv +val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv val clenv_instance_term : wc clausenv -> constr -> constr -val clenv_pose : name * int * constr -> 'a clausenv -> 'a clausenv +val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv val clenv_template : 'a clausenv -> constr freelisted val clenv_template_type : 'a clausenv -> constr freelisted -val clenv_instance_type : wc clausenv -> int -> constr +val clenv_instance_type : wc clausenv -> metavariable -> constr val clenv_instance_template : wc clausenv -> constr val clenv_instance_template_type : wc clausenv -> constr val clenv_type_of : wc clausenv -> constr -> constr -val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv -val clenv_bchain : int -> 'a clausenv -> wc clausenv -> wc clausenv +val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv +val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv (* Unification with clenv *) type arg_bindings = (int * constr) list val unify_0 : Reductionops.conv_pb -> wc -> constr -> constr - -> (int * constr) list * (constr * constr) list + -> Termops.metamap * (constr * constr) list val clenv_unify : bool -> Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv val clenv_match_args : - constr Rawterm.explicit_substitution -> wc clausenv -> wc clausenv + constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv (* Bindings *) -val clenv_independent : wc clausenv -> int list -val clenv_missing : 'a clausenv -> int list +val clenv_independent : wc clausenv -> metavariable list +val clenv_missing : 'a clausenv -> metavariable list val clenv_constrain_missing_args : (* Used in user contrib Lannion *) constr list -> wc clausenv -> wc clausenv (* val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv *) -val clenv_lookup_name : 'a clausenv -> identifier -> int +val clenv_lookup_name : 'a clausenv -> identifier -> metavariable val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv val make_clenv_binding_apply : - wc -> int -> constr * constr -> types Rawterm.substitution -> wc clausenv + wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv val make_clenv_binding : - wc -> constr * constr -> types Rawterm.substitution -> wc clausenv + wc -> constr * constr -> types Rawterm.bindings -> wc clausenv (* Tactics *) val unify : constr -> tactic diff --git a/proofs/refiner.ml b/proofs/refiner.ml index c49c0780c..dad31af9c 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -276,7 +276,9 @@ let extract_open_proof sigma pf = let next_meta = let meta_cnt = ref 0 in let rec f () = - incr meta_cnt; if in_dom sigma !meta_cnt then f () else !meta_cnt + incr meta_cnt; + if in_dom sigma !meta_cnt then f () + else !meta_cnt in f in let open_obligations = ref [] in diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 6ea71c4db..01ffae0d4 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -172,7 +172,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate val weak_undo_pftreestate : pftreestate -> pftreestate val mk_pftreestate : goal -> pftreestate -val extract_open_pftreestate : pftreestate -> constr * (int * types) list +val extract_open_pftreestate : pftreestate -> constr * Termops.metamap val extract_pftreestate : pftreestate -> constr val first_unproven : pftreestate -> pftreestate val last_unproven : pftreestate -> pftreestate diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index bdc8f3367..3461987c4 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -145,11 +145,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacRename of identifier located * identifier located (* Constructors *) - | TacLeft of 'constr substitution - | TacRight of 'constr substitution - | TacSplit of bool * 'constr substitution + | TacLeft of 'constr bindings + | TacRight of 'constr bindings + | TacSplit of bool * 'constr bindings | TacAnyConstructor of 'tac option - | TacConstructor of int or_metaid * 'constr substitution + | TacConstructor of int or_metaid * 'constr bindings (* Conversion *) | TacReduce of ('constr,'cst) red_expr_gen * 'id raw_hyp_location list diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 828b6b146..73916c6bb 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -104,7 +104,7 @@ val weak_undo_pftreestate : pftreestate -> pftreestate val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate val solve_pftreestate : tactic -> pftreestate -> pftreestate val mk_pftreestate : goal -> pftreestate -val extract_open_pftreestate : pftreestate -> constr * (int * types) list +val extract_open_pftreestate : pftreestate -> constr * Termops.metamap val extract_pftreestate : pftreestate -> constr val first_unproven : pftreestate -> pftreestate val last_unproven : pftreestate -> pftreestate diff --git a/tactics/auto.ml b/tactics/auto.ml index 8788f7208..638f6d727 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -414,7 +414,7 @@ let add_extern name pri (patmetas,pat) tacast dbname = match (list_subtract tacmetas patmetas) with | i::_ -> errorlabstrm "add_extern" - (str "The meta-variable ?" ++ int i ++ str" is not bound") + (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound") | [] -> Lib.add_anonymous_leaf (inAutoHint(dbname, [make_extern name pri pat tacast])) diff --git a/tactics/auto.mli b/tactics/auto.mli index 5fe5ebb86..a8d8cf1df 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -118,10 +118,11 @@ val make_extern : -> constr_label * pri_auto_tactic val set_extern_interp : - ((int * constr) list -> Tacexpr.glob_tactic_expr -> tactic) -> unit + (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit val set_extern_intern_tac : - (int list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) -> unit + (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) + -> unit val set_extern_subst_tactic : (Names.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 9bef1f269..2205ed8ac 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -78,10 +78,10 @@ val h_rename : identifier -> identifier -> tactic (* val h_any_constructor : tactic -> tactic *) -val h_constructor : int -> constr substitution -> tactic -val h_left : constr substitution -> tactic -val h_right : constr substitution -> tactic -val h_split : constr substitution -> tactic +val h_constructor : int -> constr bindings -> tactic +val h_left : constr bindings -> tactic +val h_right : constr bindings -> tactic +val h_split : constr bindings -> tactic val h_one_constructor : int -> tactic val h_simplest_left : tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index 233c149cb..f76729fa2 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -45,7 +45,7 @@ let collect_meta_variables c = let check_no_metas clenv ccl = if occur_meta ccl then - let metas = List.map (fun n -> Intmap.find n clenv.namenv) + let metas = List.map (fun n -> Metamap.find n clenv.namenv) (collect_meta_variables ccl) in errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ @@ -53,19 +53,6 @@ let check_no_metas clenv ccl = prlist_with_sep pr_coma pr_id metas (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *)) -let dest_match_eq gls eqn = - try - pf_matches gls (Coqlib.build_coq_eq_pattern ()) eqn - with PatternMatchingFailure -> - (try - pf_matches gls (Coqlib.build_coq_eqT_pattern ()) eqn - with PatternMatchingFailure -> - (try - pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn - with PatternMatchingFailure -> - errorlabstrm "dest_match_eq" - (str "no primitive equality here"))) - let var_occurs_in_pf gl id = let env = pf_env gl in occur_var env id (pf_concl gl) or @@ -220,12 +207,7 @@ let split_dep_and_nodep hyps gl = if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) - -let dest_nf_eq gls t = - match dest_match_eq gls t with - | [(1,x);(2,y);(3,z)] -> - (x,pf_whd_betadeltaiota gls y, pf_whd_betadeltaiota gls z) - | _ -> error "dest_nf_eq: should be an equality" +open Coqlib let generalizeRewriteIntros tac depids id gls = let dids = dependent_hyps id depids (pf_env gls) in @@ -247,7 +229,7 @@ let projectAndApply thin id depids gls = let subst_hyp_RL id = tclTRY(hypSubst_RL id None) in let subst_hyp gls = let orient_rule id = - let (t,t1,t2) = dest_nf_eq gls (pf_get_hyp_typ gls id) in + let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in match (kind_of_term t1, kind_of_term t2) with | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1 @@ -257,7 +239,7 @@ let projectAndApply thin id depids gls = in onLastHyp orient_rule gls in - let (t,t1,t2) = dest_nf_eq gls (pf_get_hyp_typ gls id) in + let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in match (thin, kind_of_term t1, kind_of_term t2) with | (true, Var id1, _) -> generalizeRewriteIntros diff --git a/tactics/refine.ml b/tactics/refine.ml index 1a360f9ba..cb2809cd3 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -60,8 +60,6 @@ open Tactics open Tacticals open Printer -type metamap = (int * constr) list - type term_with_holes = TH of constr * metamap * sg_proofs and sg_proofs = (term_with_holes option) list @@ -81,14 +79,14 @@ and pp_sg sg = (* compute_metamap : constr -> 'a evar_map -> term_with_holes * réalise le 2. ci-dessus * - * Pour cela, on renvoie une metamap qui indique pour chaque meta-variable + * Pour cela, on renvoie une meta_map qui indique pour chaque meta-variable * si elle correspond à un but (None) ou si elle réduite à son tour * par un terme de preuve incomplet (Some c). * * On a donc l'INVARIANT suivant : le terme c rendu est "de niveau 1" - * -- i.e. à plat -- et la metamap contient autant d'éléments qu'il y + * -- i.e. à plat -- et la meta_map contient autant d'éléments qu'il y * a de meta-variables dans c. On suppose de plus que l'ordre dans la - * metamap correspond à celui des buts qui seront engendrés par le refine. + * meta_map correspond à celui des buts qui seront engendrés par le refine. *) let replace_by_meta env gmm = function diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3f3b4e019..ea7765cd6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -91,7 +91,7 @@ let catch_error loc tac g = (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = { lfun : (identifier * value) list; - lmatch : (int * constr) list; + lmatch : patvar_map; debug : debug_info } let check_is_value = function @@ -260,7 +260,7 @@ type glob_sign = { (* ltac variables and the subset of vars introduced by Intro/Let/... *) ltacrecvars : (identifier * ltac_constant) list; (* ltac recursive names *) - metavars : int list; + metavars : patvar list; (* metavariables introduced by patterns *) gsigma : Evd.evar_map; genv : Environ.env } @@ -345,7 +345,7 @@ let intern_lochyp ist (_loc,_ as locid) = (loc,intern_hyp ist locid) let error_unbound_metanum loc n = user_err_loc - (loc,"intern_qualid_or_metanum", str "?" ++ int n ++ str " is unbound") + (loc,"intern_qualid_or_metanum", str "?" ++ pr_patvar n ++ str " is unbound") let intern_metanum sign loc n = if List.mem n sign.metavars then n else error_unbound_metanum loc n @@ -440,10 +440,16 @@ let intern_clause_pattern ist (l,occl) = | [] -> [] in (l,check occl) + (* TODO: catch ltac vars *) let intern_induction_arg ist = function | ElimOnConstr c -> ElimOnConstr (intern_constr ist c) | ElimOnAnonHyp n as x -> x - | ElimOnIdent (_loc,id) as x -> ElimOnIdent (loc,id) + | ElimOnIdent (_loc,id) as x -> + if !strict_check then + (* If in a defined tactic, no intros-until *) + ElimOnConstr (intern_constr ist (CRef (Ident (loc,id)))) + else + ElimOnIdent (loc,id) (* Globalizes a reduction expression *) let intern_evaluable_or_metanum ist = function @@ -1181,7 +1187,7 @@ let interp_may_eval f ist gl = function (try let ic = f ist gl c and ctxt = constr_of_VConstr_context (List.assoc s ist.lfun) in - subst_meta [-1,ic] ctxt + subst_meta [special_meta,ic] ctxt with | Not_found -> user_err_loc (loc, "interp_may_eval", @@ -1221,7 +1227,8 @@ let interp_induction_arg ist gl = function | ElimOnAnonHyp n as x -> x | ElimOnIdent (loc,id) -> if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) - else ElimOnConstr (pf_interp_constr ist gl (RVar (loc,id),None)) + else ElimOnConstr + (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id))))) let interp_binding ist gl (loc,b,c) = (loc,interp_quantified_hypothesis ist gl b,pf_interp_constr ist gl c) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index e36c89377..ddd5175da 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -36,7 +36,7 @@ type value = (* Signature for interpretation: val\_interp and interpretation functions *) and interp_sign = { lfun : (identifier * value) list; - lmatch : (int * constr) list; + lmatch : Pattern.patvar_map; debug : debug_info } (* Gives the identifier corresponding to an Identifier [tactic_arg] *) @@ -70,7 +70,7 @@ val add_tacdef : type glob_sign = { ltacvars : identifier list * identifier list; ltacrecvars : (identifier * Nametab.ltac_constant) list; - metavars : int list; + metavars : Rawterm.patvar list; gsigma : Evd.evar_map; genv : Environ.env } @@ -99,7 +99,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Tacred.red_expr (* Interprets tactic expressions *) -val interp_tac_gen : (identifier * value) list -> (int * constr) list -> +val interp_tac_gen : (identifier * value) list -> Pattern.patvar_map -> debug_info -> raw_tactic_expr -> tactic (* Initial call for interpretation *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index a32eaf54f..3a42dc227 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -66,7 +66,7 @@ type clause = identifier option val nth_clause : int -> goal sigma -> clause val clause_type : clause -> goal sigma -> constr -val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list +val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool val allHyps : goal sigma -> identifier list diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 3a2ac7b22..0cdf1c086 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -31,7 +31,7 @@ open Rawterm (*s General functions. *) val type_clenv_binding : named_context sigma -> - constr * constr -> constr substitution -> constr + constr * constr -> constr bindings -> constr val string_of_inductive : constr -> string val head_constr : constr -> constr list @@ -163,12 +163,12 @@ val general_elim : constr with_bindings -> constr with_bindings -> val default_elim : constr with_bindings -> tactic val simplest_elim : constr -> tactic val elim : constr with_bindings -> constr with_bindings option -> tactic -val general_elim_in : identifier -> constr * constr substitution -> - constr * constr substitution -> tactic +val general_elim_in : identifier -> constr * constr bindings -> + constr * constr bindings -> tactic val old_induct : quantified_hypothesis -> tactic -val general_elim_in : identifier -> constr * constr substitution -> - constr * constr substitution -> tactic +val general_elim_in : identifier -> constr * constr bindings -> + constr * constr bindings -> tactic val new_induct : constr induction_arg -> constr with_bindings option -> identifier list list -> tactic @@ -200,14 +200,14 @@ val dorE : bool -> clause ->tactic (*s Introduction tactics. *) val constructor_tac : int option -> int -> - constr substitution -> tactic -val one_constructor : int -> constr substitution -> tactic + constr bindings -> tactic +val one_constructor : int -> constr bindings -> tactic val any_constructor : tactic option -> tactic -val left : constr substitution -> tactic +val left : constr bindings -> tactic val simplest_left : tactic -val right : constr substitution -> tactic +val right : constr bindings -> tactic val simplest_right : tactic -val split : constr substitution -> tactic +val split : constr bindings -> tactic val simplest_split : tactic (*s Logical connective tactics. *) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index dd5268720..5a03b0841 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -23,26 +23,26 @@ open Tactics open Util let is_empty ist = - if (is_empty_type (List.assoc 1 ist.lmatch)) then + if (is_empty_type (List.assoc (id_of_string "1") ist.lmatch)) then <:tactic<Idtac>> else <:tactic<Fail>> let is_unit ist = - if (is_unit_type (List.assoc 1 ist.lmatch)) then + if (is_unit_type (List.assoc (id_of_string "1") ist.lmatch)) then <:tactic<Idtac>> else <:tactic<Fail>> let is_conj ist = - let ind=(List.assoc 1 ist.lmatch) in + let ind=(List.assoc (id_of_string "1") ist.lmatch) in if (is_conjunction ind) && (is_nodep_ind ind) then <:tactic<Idtac>> else <:tactic<Fail>> let is_disj ist = - if (is_disjunction (List.assoc 1 ist.lmatch)) then + if (is_disjunction (List.assoc (id_of_string "1") ist.lmatch)) then <:tactic<Idtac>> else <:tactic<Fail>> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index bc77424c5..8cbc8312e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -90,7 +90,8 @@ let show_proof () = msgnl (str"LOC: " ++ prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ str"Subgoals" ++ fnl () ++ - prlist (fun (mv,ty) -> int mv ++ str" -> " ++ prtype ty ++ fnl ()) + prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ + prtype ty ++ fnl ()) meta_types ++ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm)) diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 1ba590cee..92feaa7de 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -8,6 +8,7 @@ (* $Id$ *) +(*i*) open Ast open Util open Pp @@ -19,6 +20,8 @@ open Coqast open Ppextend open Topconstr open Term +open Pattern +(*i*) let sep = fun _ -> brk(1,0) let sep_p = fun _ -> str"." @@ -288,7 +291,7 @@ let rec check_same_type ty1 ty2 = check_same_type a1 a2; List.iter2 check_same_type bl1 bl2 | CHole _, CHole _ -> () - | CMeta(_,i1), CMeta(_,i2) when i1=i2 -> () + | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () | CSort(_,s1), CSort(_,s2) when s1=s2 -> () | CCast(_,a1,b1), CCast(_,a2,b2) -> check_same_type a1 a2; @@ -498,7 +501,8 @@ let rec pr inherited a = str "end"), latom | CHole _ -> str "_", latom - | CMeta (_,p) -> str "?" ++ int p, latom + | CEvar (_,n) -> str "?" ++ int n, latom + | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_sort s, latom | CCast (_,a,b) -> hv 0 (pr (lcast,L) a ++ cut () ++ str ":" ++ pr (-lcast,E) b), lcast |