From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- pretyping/cases.ml | 39 +++---- pretyping/classops.ml | 7 +- pretyping/clenv.ml | 45 ++++++- pretyping/clenv.mli | 32 +++-- pretyping/coercion.ml | 144 ++++++++++++----------- pretyping/evarconv.ml | 152 +++++++++++++++++------- pretyping/evarconv.mli | 4 +- pretyping/evarutil.ml | 140 ++++++++++++++++------ pretyping/evarutil.mli | 10 +- pretyping/evd.ml | 43 ++++--- pretyping/evd.mli | 6 +- pretyping/inductiveops.ml | 8 +- pretyping/inductiveops.mli | 4 +- pretyping/matching.ml | 4 +- pretyping/pretype_errors.ml | 6 +- pretyping/pretype_errors.mli | 5 +- pretyping/pretyping.ml | 69 ++++------- pretyping/pretyping.mli | 3 +- pretyping/rawterm.ml | 4 +- pretyping/rawterm.mli | 13 ++- pretyping/recordops.ml | 8 +- pretyping/recordops.mli | 4 +- pretyping/reductionops.ml | 31 +++-- pretyping/reductionops.mli | 10 +- pretyping/retyping.ml | 52 +++++---- pretyping/retyping.mli | 5 +- pretyping/termops.ml | 15 ++- pretyping/termops.mli | 10 +- pretyping/typing.ml | 21 ++-- pretyping/unification.ml | 183 +++++++++++++++++------------ pretyping/vnorm.ml | 271 +++++++++++++++++++++++++++++++++++++++++++ pretyping/vnorm.mli | 18 +++ 32 files changed, 971 insertions(+), 395 deletions(-) create mode 100644 pretyping/vnorm.ml create mode 100644 pretyping/vnorm.mli (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b0fe83a3..58dda021 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *) open Util open Names @@ -336,8 +336,8 @@ let inh_coerce_to_ind isevars env ty tyi = un inductif cela doit être égal *) let _ = e_cumul env isevars expected_typ ty in () -let unify_tomatch_with_patterns isevars env typ tm = - match find_row_ind tm with +let unify_tomatch_with_patterns isevars env loc typ pats = + match find_row_ind pats with | None -> NotInd (None,typ) | Some (_,(ind,_)) -> inh_coerce_to_ind isevars env typ ind; @@ -345,29 +345,26 @@ let unify_tomatch_with_patterns isevars env typ tm = with Not_found -> NotInd (None,typ) let find_tomatch_tycon isevars env loc = function - (* Try first if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,_,_),_ - (* Otherwise try to get constraints from (the 1st) constructor in clauses *) - | None, Some (_,(ind,_)) -> - mk_tycon (inductive_template isevars env loc ind) - | None, None -> - empty_tycon - -let coerce_row typing_fun isevars env cstropt (tomatch,(_,indopt)) = + (* Try if some 'in I ...' is present and can be used as a constraint *) + | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind) + | None -> empty_tycon + +let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) = let loc = Some (loc_of_rawconstr tomatch) in - let tycon = find_tomatch_tycon isevars env loc (indopt,cstropt) in + let tycon = find_tomatch_tycon isevars env loc indopt in let j = typing_fun tycon env tomatch in let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in - let t = + let t = try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) - with Not_found -> NotInd (None,typ) in + with Not_found -> + unify_tomatch_with_patterns isevars env loc typ pats in (j.uj_val,t) let coerce_to_indtype typing_fun isevars env matx tomatchl = let pats = List.map (fun r -> r.patterns) matx in let matx' = match matrix_transpose pats with - | [] -> List.map (fun _ -> None) tomatchl (* no patterns at all *) - | m -> List.map find_row_ind m in + | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *) + | m -> m in List.map2 (coerce_row typing_fun isevars env) matx' tomatchl (************************************************************************) @@ -500,12 +497,12 @@ let rec adjust_local_defs loc = function | [], [] -> [] | _ -> raise NotAdjustable -let check_and_adjust_constructor ind cstrs = function +let check_and_adjust_constructor env ind cstrs = function | PatVar _ as pat -> pat | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in - if ind' = ind then + if Closure.mind_equiv env ind' ind then (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in @@ -1132,7 +1129,7 @@ let first_clause_irrefutable env = function | eqn::mat -> List.for_all (irrefutable env) eqn.patterns | _ -> false -let group_equations pb mind current cstrs mat = +let group_equations pb ind current cstrs mat = let mat = if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in let brs = Array.create (Array.length cstrs) [] in @@ -1142,7 +1139,7 @@ let group_equations pb mind current cstrs mat = (fun eqn () -> let rest = remove_current_pattern eqn in let pat = current_pattern eqn in - match check_and_adjust_constructor mind cstrs pat with + match check_and_adjust_constructor pb.env ind cstrs pat with | PatVar (_,name) -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b6cce031..bbad005c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: classops.ml 8642 2006-03-17 10:09:02Z notin $ *) +(* $Id: classops.ml 9257 2006-10-21 17:28:28Z herbelin $ *) open Util open Pp @@ -154,7 +154,8 @@ let lookup_pattern_path_between (s,t) = coe.coe_value in match kind_of_term c with - | Construct sp -> (sp, coe.coe_param) + | Construct cstr -> + (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1) | _ -> raise Not_found) l (* find_class_type : constr -> cl_typ * int *) @@ -207,7 +208,7 @@ let class_of env sigma t = let inductive_class_of ind = fst (class_info (CL_IND ind)) -let class_args_of c = snd (decompose_app c) +let class_args_of c = snd (find_class_type c) let string_of_class = function | CL_FUN -> "Funclass" diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 6113ec2d..abe31e06 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 8752 2006-04-27 19:37:33Z herbelin $ *) +(* $Id: clenv.ml 9279 2006-10-25 15:51:24Z herbelin $ *) open Pp open Util @@ -74,6 +74,26 @@ let clenv_get_type_of ce c = (meta_list ce.env) in Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c +exception NotExtensibleClause + +let clenv_push_prod cl = + let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in + let rec clrec typ = match kind_of_term typ with + | Cast (t,_,_) -> clrec t + | Prod (na,t,u) -> + let mv = new_meta () in + let dep = dependent (mkRel 1) u in + let na' = if dep then na else Anonymous in + let e' = meta_declare mv t ~name:na' cl.env in + let concl = if dep then subst1 (mkMeta mv) u else u in + let def = applist (cl.templval.rebus,[mkMeta mv]) in + { templval = mk_freelisted def; + templtyp = mk_freelisted concl; + env = e'; + templenv = cl.templenv } + | _ -> raise NotExtensibleClause + in clrec typ + let clenv_environments evd bound c = let rec clrec (e,metas) n c = match n, kind_of_term c with @@ -258,7 +278,20 @@ let connect_clenv gls clenv = * resolution can cause unification of already-existing metavars, and * of the fresh ones which get created. This operation is a composite * of operations which pose new metavars, perform unification on - * terms, and make bindings. *) + * terms, and make bindings. + + Otherwise said, from + + [clenv] = [env;sigma;metas |- c:T] + [clenv'] = [env';sigma';metas' |- d:U] + [mv] = [mi] of type [Ti] in [metas] + + then, if the unification of [Ti] and [U] produces map [rho], the + chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for + [rho'] being [rho;mi:=d]. + + In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma]. +*) let clenv_fchain mv clenv nextclenv = (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) let clenv' = @@ -412,18 +445,18 @@ let clenv_constrain_missing_args mlist clause = (****************************************************************) (* Clausal environment for an application *) -let make_clenv_binding_gen n gls (c,t) = function +let make_clenv_binding_gen hyps_only n gls (c,t) = function | ImplicitBindings largs -> let clause = mk_clenv_from_n gls n (c,t) in - clenv_constrain_dep_args (n <> None) clause largs + clenv_constrain_dep_args hyps_only clause largs | ExplicitBindings lbind -> let clause = mk_clenv_rename_from_n gls n (c,t) in clenv_match_args lbind clause | NoBindings -> mk_clenv_from_n gls n (c,t) -let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc -let make_clenv_binding = make_clenv_binding_gen None +let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls +let make_clenv_binding = make_clenv_binding_gen false None (****************************************************************) (* Pretty-print *) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index f585dfea..b5433cac 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: clenv.mli 7659 2005-12-17 21:07:17Z herbelin $ i*) +(*i $Id: clenv.mli 9277 2006-10-25 13:02:22Z herbelin $ i*) (*i*) open Util @@ -17,6 +17,7 @@ open Environ open Evd open Evarutil open Mod_subst +open Rawterm (*i*) (***************************************************************) @@ -93,24 +94,41 @@ val clenv_missing : clausenv -> metavariable list (* defines metas corresponding to the name of the bindings *) val clenv_match_args : - constr Rawterm.explicit_bindings -> clausenv -> clausenv + constr explicit_bindings -> clausenv -> clausenv val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv (* start with a clenv to refine with a given term with bindings *) -(* 1- the arity of the lemma is fixed *) +(* the arity of the lemma is fixed *) +(* the optional int tells how many prods of the lemma have to be used *) +(* use all of them if None *) val make_clenv_binding_apply : - evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings -> + evar_info sigma -> int option -> constr * constr -> constr bindings -> clausenv val make_clenv_binding : - evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv - -(* other stuff *) + evar_info sigma -> constr * constr -> constr bindings -> clausenv + +(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where + [lmetas] is a list of metas to be applied to a proof of [t] so that + it produces the unification pattern [ccl]; [sigma'] is [sigma] + extended with [lmetas]; if [n] is defined, it limits the size of + the list even if [ccl] is still a product; otherwise, it stops when + [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x] + and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and + [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] + and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) val clenv_environments : evar_defs -> int option -> types -> evar_defs * constr list * types + +(* [clenv_environments_evars env sigma n t] does the same but returns + a list of Evar's defined in [env] and extends [sigma] accordingly *) val clenv_environments_evars : env -> evar_defs -> int option -> types -> evar_defs * constr list * types +(* if the clause is a product, add an extra meta for this product *) +exception NotExtensibleClause +val clenv_push_prod : clausenv -> clausenv + (***************************************************************) (* Pretty-print *) val pr_clenv : clausenv -> Pp.std_ppcmds diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index d0ee913f..cc74b0ad 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: coercion.ml 9257 2006-10-21 17:28:28Z herbelin $ *) open Util open Names @@ -20,6 +20,7 @@ open Evarutil open Evarconv open Retyping open Evd +open Termops module type S = sig (*s Coercions. *) @@ -66,7 +67,14 @@ module Default = struct (* Typing operations dealing with coercions *) exception NoCoercion - let class_of1 env sigma t = class_of env sigma (nf_evar sigma t) + let whd_app_evar sigma t = + match kind_of_term t with + | App (f,l) -> mkApp (whd_evar sigma f,l) + | _ -> whd_evar sigma t + + let class_of1 env isevars t = + let sigma = evars_of isevars in + class_of env sigma (whd_app_evar sigma t) (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = @@ -84,7 +92,6 @@ module Default = struct apply_rec [] funj.uj_type argl (* appliquer le chemin de coercions de patterns p *) - let apply_pattern_coercion loc pat p = List.fold_left (fun pat (co,n) -> @@ -100,7 +107,6 @@ module Default = struct apply_pattern_coercion loc pat p (* appliquer le chemin de coercions p à hj *) - let apply_coercion env p hj typ_cl = try fst (List.fold_left @@ -120,22 +126,23 @@ module Default = struct let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (isevars,j) - | Evar ev when not (is_defined_evar isevars ev) -> + | Evar ev -> let (isevars',t) = define_evar_as_arrow isevars ev in (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in + let t,i1 = class_of1 env isevars j.uj_type in let p = lookup_path_to_fun_from i1 in (isevars,apply_coercion env p j t) with Not_found -> (isevars,j)) let inh_tosort_force loc env isevars j = try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in + let t,i1 = class_of1 env isevars j.uj_type in let p = lookup_path_to_sort_from i1 in let j1 = apply_coercion env p j t in - (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) + let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in + (isevars,type_judgment env j2) with Not_found -> error_not_a_type_loc loc env (evars_of isevars) j @@ -154,8 +161,8 @@ module Default = struct let inh_coerce_to_fail env isevars c1 v t = let v', t' = try - let t1,i1 = class_of1 env (evars_of isevars) c1 in - let t2,i2 = class_of1 env (evars_of isevars) t in + let t1,i1 = class_of1 env isevars c1 in + let t2,i2 = class_of1 env isevars t in let p = lookup_path_between (i2,i1) in match v with Some v -> @@ -166,64 +173,68 @@ module Default = struct in try (the_conv_x_leq env t' c1 isevars, v', t') with Reduction.NotConvertible -> raise NoCoercion - open Pp + let rec inh_conv_coerce_to_fail loc env isevars v t c1 = try (the_conv_x_leq env t c1 isevars, v, t) with Reduction.NotConvertible -> - (try - inh_coerce_to_fail env isevars c1 v t - with NoCoercion -> - (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), - kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with - | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in - let (evd',b) = - match v' with - Some v' -> - (match kind_of_term v' with - | Lambda (x,v1,v2) -> - (try the_conv_x env v1 u1 isevars, Some (x, v1, v2) (* leq v1 u1? *) - with Reduction.NotConvertible -> (isevars, None)) - | _ -> (isevars, None)) - | None -> (isevars, None) - in - (match b with - Some (x, v1, v2) -> - let env1 = push_rel (x,None,v1) env in - let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' - (Some v2) t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', - mkProd (x, v1, t2')) - | None -> - (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) - (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *) - (* has type (name:u1)u2 (with v' recursively obtained) *) - let name = (match name with - | Anonymous -> Name (id_of_string "x") - | _ -> name) in - let env1 = push_rel (name,None,u1) env in - let (evd', v1', t1') = - inh_conv_coerce_to_fail loc env1 isevars - (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) - in - let (evd'', v2', t2') = - let v2 = - match v with - Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' - | None -> None - and evd', t2 = - match v1' with - Some v1' -> evd', subst1 v1' t2 - | None -> - let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in - evd', subst1 ev t2 - in - inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 - in - (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2', - mkProd (name, u1, t2'))) - | _ -> raise NoCoercion)) - + try inh_coerce_to_fail env isevars c1 v t + with NoCoercion -> + match + kind_of_term (whd_betadeltaiota env (evars_of isevars) t), + kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) + with + | Prod (_,t1,t2), Prod (name,u1,u2) -> + let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in + let (evd',b) = + match v' with + | Some v' -> + (match kind_of_term v' with + | Lambda (x,v1,v2) -> + (* sous-typage non contravariant: pas de "leq v1 u1" *) + (try the_conv_x env v1 u1 isevars, Some (x, v1, v2) + with Reduction.NotConvertible -> (isevars, None)) + | _ -> (isevars, None)) + | None -> (isevars, None) + in + (match b with + | Some (x, v1, v2) -> + let env1 = push_rel (x,None,v1) env in + let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' + (Some v2) t2 u2 in + (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', + mkProd (x, v1, t2')) + | None -> + (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) + (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *) + (* has type (name:u1)u2 (with v' recursively obtained) *) + let name = match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name + in + let env1 = push_rel (name,None,u1) env in + let (evd', v1', t1') = + inh_conv_coerce_to_fail loc env1 isevars + (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) + in + let (evd'', v2', t2') = + let v2 = + match v with + | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1' + | None -> None + and evd', t2 = + match v1' with + | Some v1' -> evd', subst_term v1' t2 + | None -> + let evd', ev = + new_evar evd' env ~src:(loc, InternalHole) t1' in + evd', subst_term ev t2 + in + inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 + in + (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2', + mkProd (name, u1, t2'))) + | _ -> raise NoCoercion + (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to loc env isevars cj (n, t) = match n with @@ -236,8 +247,7 @@ module Default = struct error_actual_type_loc loc env sigma cj t in let val' = match val' with Some v -> v | None -> assert(false) in - let nf = nf_isevar evd' in - (evd',{ uj_val = nf val'; uj_type = nf t }) + (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> (isevars, cj) let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 458f5bd3..3c4a23ec 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,14 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 8793 2006-05-05 17:41:41Z barras $ *) +(* $Id: evarconv.ml 9141 2006-09-15 10:07:01Z herbelin $ *) +open Pp open Util open Names open Term open Closure open Reduction open Reductionops +open Termops open Environ open Typing open Classops @@ -83,7 +85,7 @@ let evar_apprec env isevars stack c = | Evar (n,_ as ev) when Evd.is_defined sigma n -> aux (Evd.existential_value sigma ev, stack) | _ -> (t, list_of_stack stack) - in aux (c, append_stack (Array.of_list stack) empty_stack) + in aux (c, append_stack_list stack empty_stack) let apprec_nohdbeta env isevars c = let (t,stack as s) = Reductionops.whd_stack c in @@ -126,7 +128,6 @@ let check_conv_record (t1,l1) (t2,l2) = with _ -> raise Not_found - (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) @@ -190,12 +191,7 @@ let rec evar_conv_x env isevars pbty term1 term2 = else let (t1,l1) = apprec_nohdbeta env isevars term1 in let (t2,l2) = apprec_nohdbeta env isevars term2 in - if (head_is_embedded_evar isevars t1 & not(is_eliminator t2)) - or (head_is_embedded_evar isevars t2 & not(is_eliminator t1)) - then - (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true) - else - evar_eqappr_x env isevars pbty (t1,l1) (t2,l2) + evar_eqappr_x env isevars pbty (t1,l1) (t2,l2) and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) @@ -229,7 +225,20 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, MaybeFlexible flex2 -> let f1 i = - if List.length l1 <= List.length l2 then + if + is_unification_pattern_evar ev1 l1 & + not (occur_evar (fst ev1) (applist (term2,l2))) + then + (* Miller-Pfenning's patterns unification *) + (* Preserve generality (except that CCI has no eta-conversion) *) + let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in + let t2 = solve_pattern_eqn env l1 t2 in + solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2) + else if + List.length l1 <= List.length l2 + then + (* Try first-order unification *) + (* (heuristic that gives acceptable results in practice) *) let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in ise_and i @@ -248,7 +257,20 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Flexible ev2 -> let f1 i = - if List.length l2 <= List.length l1 then + if + is_unification_pattern_evar ev2 l2 & + not (occur_evar (fst ev2) (applist (term1,l1))) + then + (* Miller-Pfenning's patterns unification *) + (* Preserve generality (except that CCI has no eta-conversion) *) + let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in + let t1 = solve_pattern_eqn env l2 t1 in + solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1) + else if + List.length l2 <= List.length l1 + then + (* Try first-order unification *) + (* (heuristic that gives acceptable results in practice) *) let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in ise_and i (* First compare extra args for better failure message *) @@ -273,8 +295,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (try conv_record env i (try check_conv_record appr1 appr2 with Not_found -> check_conv_record appr2 appr1) -(* TODO: remove this _ !!! *) - with _ -> (i,false)) + with Not_found -> (i,false)) and f4 i = (* heuristic: unfold second argument first, exception made if the first argument is a beta-redex (expand a constant @@ -295,38 +316,39 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_try isevars [f2; f3; f4] | Flexible ev1, Rigid _ -> - if (List.length l1 <= List.length l2) then - let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - ise_and isevars - (* First compare extra args for better failure message *) - [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2); - (fun i -> - (* Then instantiate evar unless already done by unifying args *) - let t2 = applist(term2,deb2) in - if is_defined_evar i ev1 then - evar_conv_x env i pbty (mkEvar ev1) t2 - else - solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))] - else (isevars,false) + if + is_unification_pattern_evar ev1 l1 & + not (occur_evar (fst ev1) (applist (term2,l2))) + then + (* Miller-Pfenning's patterns unification *) + (* Preserve generality (except that CCI has no eta-conversion) *) + let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in + let t2 = solve_pattern_eqn env l1 t2 in + solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2) + else + (* Postpone the use of an heuristic *) + add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars, + true + | Rigid _, Flexible ev2 -> - if List.length l2 <= List.length l1 then - let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - ise_and isevars - (* First compare extra args for better failure message *) - [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2); - (fun i -> - (* Then instantiate evar unless already done by unifying args *) - let t1 = applist(term1,deb1) in - if is_defined_evar i ev2 then - evar_conv_x env i pbty t1 (mkEvar ev2) - else - solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))] - else (isevars,false) + if + is_unification_pattern_evar ev2 l2 & + not (occur_evar (fst ev2) (applist (term1,l1))) + then + (* Miller-Pfenning's patterns unification *) + (* Preserve generality (except that CCI has no eta-conversion) *) + let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in + let t1 = solve_pattern_eqn env l2 t1 in + solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1) + else + (* Postpone the use of an heuristic *) + add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars, + true | MaybeFlexible flex1, Rigid _ -> let f3 i = (try conv_record env i (check_conv_record appr1 appr2) - with _ -> (i,false)) + with Not_found -> (i,false)) and f4 i = match eval_flexible_term env flex1 with | Some v1 -> @@ -337,8 +359,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Rigid _ , MaybeFlexible flex2 -> let f3 i = - (try (conv_record env i (check_conv_record appr2 appr1)) - with _ -> (i,false)) + (try conv_record env i (check_conv_record appr2 appr1) + with Not_found -> (i,false)) and f4 i = match eval_flexible_term env flex2 with | Some v2 -> @@ -468,7 +490,51 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = params1 params); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1); (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))] - + +let first_order_unification env isevars pbty (term1,l1) (term2,l2) = + match kind_of_term term1, kind_of_term term2 with + | Evar ev1,_ when List.length l1 <= List.length l2 -> + let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in + ise_and isevars + (* First compare extra args for better failure message *) + [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1); + (fun i -> + (* Then instantiate evar unless already done by unifying args *) + let t2 = applist(term2,deb2) in + if is_defined_evar i ev1 then + evar_conv_x env i pbty t2 (mkEvar ev1) + else + solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))] + | _,Evar ev2 when List.length l2 <= List.length l1 -> + let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in + ise_and isevars + (* First compare extra args for better failure message *) + [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2); + (fun i -> + (* Then instantiate evar unless already done by unifying args *) + let t1 = applist(term1,deb1) in + if is_defined_evar i ev2 then + evar_conv_x env i pbty t1 (mkEvar ev2) + else + solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))] + | _ -> + (* Some head evar have been instantiated *) + evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2)) + +let consider_remaining_unif_problems env isevars = + let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in + List.fold_left + (fun (isevars,b as p) (pbty,t1,t2) -> + (* Pas le bon env pour le problème... *) + if b then first_order_unification env isevars pbty + (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1)) + (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2)) + else p) + (isevars,true) + pbs + +(* Main entry points *) + let the_conv_x env t1 t2 isevars = match evar_conv_x env isevars CONV t1 t2 with (evd',true) -> evd' diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index a6f5b489..f92a6fdb 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarconv.mli 6109 2004-09-15 16:50:56Z barras $ i*) +(*i $Id: evarconv.mli 9141 2006-09-15 10:07:01Z herbelin $ i*) (*i*) open Term @@ -33,3 +33,5 @@ val evar_eqappr_x : conv_pb -> constr * constr list -> constr * constr list -> evar_defs * bool (*i*) + +val consider_remaining_unif_problems : env -> evar_defs -> evar_defs * bool diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 506cd03f..307c9886 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 8759 2006-04-28 12:24:14Z herbelin $ *) +(* $Id: evarutil.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Util open Pp @@ -21,13 +21,6 @@ open Evd open Reductionops open Pretype_errors - -let rec filter_unique = function - | [] -> [] - | x::l -> - if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l) - else x::filter_unique l - (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) @@ -63,9 +56,9 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar let tj_nf_evar = Pretype_errors.tj_nf_evar let nf_evar_info evc info = - { evar_concl = Reductionops.nf_evar evc info.evar_concl; - evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; - evar_body = info.evar_body} + { info with + evar_concl = Reductionops.nf_evar evc info.evar_concl; + evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps} let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty @@ -310,29 +303,45 @@ let is_defined_equation env evd (ev,inst) rhs = * ?3 <-- ?1 no pb: env of ?3 is larger than ?1's * ?1 <-- (list ?2) pb: ?2 may depend on x, but not ?1. * What we do is that ?2 is defined by a new evar ?4 whose context will be - * a prefix of ?2's env, included in ?1's env. *) + * a prefix of ?2's env, included in ?1's env. + + Concretely, the assumptions are "env |- ev : T" and "Gamma |- + ev[hyps:=args]" for some Gamma whose de Bruijn context has length k. + We create "env' |- ev' : T" for some env' <= env and define ev:=ev' +*) -let do_restrict_hyps evd ev args = +let do_restrict_hyps env k evd ev args = let args = Array.to_list args in let evi = Evd.find (evars_of !evd) ev in - let env = evar_env evi in let hyps = evar_context evi in - let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in + let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in (* No care is taken in case the evar type uses vars filtered out! - Is it important ? *) - let nc = - let env = - Sign.fold_named_context push_named sign ~init:(reset_context env) in - e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in + Assuming that the restriction comes from a well-typed Flex/Flex + unification problem (see real_clean), the type of the evar cannot + depend on variables that are not in the scope of the other evar, + since this other evar has the same type (up to unification). + Since moreover, the evar contexts uses names only, the + restriction raise no de Bruijn reallocation problem *) + let env' = + Sign.fold_named_context push_named hyps' ~init:(reset_context env) in + let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in evd := Evd.evar_define ev nc !evd; let (evn,_) = destEvar nc in mkEvar(evn,Array.of_list ncargs) - -let need_restriction isevars args = not (array_for_all closed0 args) +let need_restriction k args = not (array_for_all (closedn k) args) (* We try to instantiate the evar assuming the body won't depend - * on arguments that are not Rels or Vars, or appearing several times. + * on arguments that are not Rels or Vars, or appearing several times + (i.e. we tackle only Miller-Pfenning patterns unification) + + 1) Let a unification problem "env |- ev[hyps:=args] = rhs" + 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs" + where only Rel's and Var's are relevant in subst + 3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope + + Note: we don't assume rhs in normal form, it may fail while it would + have succeeded after some reductions *) (* Note: error_not_clean should not be an error: it simply means that the * conversion test that lead to the faulty call to [real_clean] should return @@ -341,36 +350,52 @@ let need_restriction isevars args = not (array_for_all closed0 args) let real_clean env isevars ev evi args rhs = let evd = ref isevars in - let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in + let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in let rec subs rigid k t = match kind_of_term t with | Rel i -> if i<=k then t - else (try List.assoc (mkRel (i-k)) subst with Not_found -> t) + else + (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *) + (try List.assoc (mkRel (i-k)) subst + with Not_found -> if rigid then raise Exit else t) | Evar (ev,args) -> if Evd.is_defined_evar !evd (ev,args) then subs rigid k (existential_value (evars_of !evd) (ev,args)) else + (* Flex/Flex problem: restriction to a common scope *) let args' = Array.map (subs false k) args in - if need_restriction !evd args' then - do_restrict_hyps evd ev args' + if need_restriction k args' then + do_restrict_hyps (reset_context env) k evd ev args' else mkEvar (ev,args') | Var id -> + (* Flex/Var problem: unifiable as a pattern iff Var in scope of ev *) (try List.assoc t subst with Not_found -> if not rigid + (* I don't understand this line: vars from evar_context evi + are private (especially some of them are freshly + generated in push_rel_context_to_named_context). They + have a priori nothing to do with the vars in env. I + remove the test [HH 25/8/06] + or List.exists (fun (id',_,_) -> id=id') (evar_context evi) + *) then t - else - error_not_clean env (evars_of !evd) ev rhs - (evar_source ev !evd)) - | _ -> map_constr_with_binders succ (subs rigid) k t + else raise Exit) + + | _ -> + (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *) + map_constr_with_binders succ (subs rigid) k t in - let body = subs true 0 (nf_evar (evars_of isevars) rhs) in - if not (closed0 body) - then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd); + let rhs = nf_evar (evars_of isevars) rhs in + let rhs = whd_beta rhs (* heuristic *) in + let body = + try subs true 0 rhs + with Exit -> + error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in (!evd,body) (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated @@ -464,6 +489,34 @@ let head_evar = in hrec +(* Check if an applied evar "?X[args] l" is a Miller's pattern; note + that we don't care whether args itself contains Rel's or even Rel's + distinct from the ones in l *) + +let is_unification_pattern_evar (_,args) l = + let l' = Array.to_list args @ l in + List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l' + +let is_unification_pattern f l = + match kind_of_term f with + | Meta _ -> array_for_all isRel l & array_distinct l + | Evar ev -> is_unification_pattern_evar ev (Array.to_list l) + | _ -> false + +(* From a unification problem "?X l1 = term1 l2" such that l1 is made + of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *) + +let solve_pattern_eqn env l1 c = + let c' = List.fold_right (fun a c -> + let c' = subst_term (lift 1 a) (lift 1 c) in + match kind_of_term a with + (* Rem: if [a] links to a let-in, do as if it were an assumption *) + | Rel n -> let (na,_,t) = lookup_rel n env in mkLambda (na,lift n t,c') + | Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c' + | _ -> assert false) + l1 c in + whd_eta c' + (* This code (i.e. solve_pb, etc.) takes a unification * problem, and tries to solve it. If it solves it, then it removes * all the conversion problems, and re-runs conversion on each one, in @@ -550,11 +603,28 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in List.fold_left (fun (isevars,b as p) (pbty,t1,t2) -> - if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true) + if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true) pbs with e when precatchable_exception e -> (isevars,false) + +(* [check_evars] fails if some unresolved evar remains *) +(* it assumes that the defined existentials have already been substituted *) + +let check_evars env initial_sigma isevars c = + let sigma = evars_of isevars in + let c = nf_evar sigma c in + let rec proc_rec c = + match kind_of_term c with + | Evar (ev,args) -> + assert (Evd.mem sigma ev); + if not (Evd.mem initial_sigma ev) then + let (loc,k) = evar_source ev isevars in + error_unsolvable_implicit loc env sigma k + | _ -> iter_constr proc_rec c + in proc_rec c + (* Operations on value/type constraints *) type type_constraint_type = (int * int) option * constr diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7429cd16..3ac05481 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 8695 2006-04-10 16:33:52Z msozeau $ i*) +(*i $Id: evarutil.mli 9141 2006-09-15 10:07:01Z herbelin $ i*) (*i*) open Util @@ -78,10 +78,18 @@ val solve_simple_eqn : -> env -> evar_defs -> conv_pb * existential * constr -> evar_defs * bool +(* [check_evars env initial_sigma extended_sigma c] fails if some + new unresolved evar remains in [c] *) +val check_evars : env -> evar_map -> evar_defs -> constr -> unit + val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts +val is_unification_pattern_evar : existential -> constr list -> bool +val is_unification_pattern : constr -> constr array -> bool +val solve_pattern_eqn : env -> constr list -> constr -> constr + (***********************************************************) (* Value/Type constraints *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 33f88ebd..030983e1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml 8759 2006-04-28 12:24:14Z herbelin $ *) +(* $Id: evd.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Pp open Util @@ -30,7 +30,8 @@ type evar_body = type evar_info = { evar_concl : constr; evar_hyps : named_context_val; - evar_body : evar_body} + evar_body : evar_body; + evar_extra : Dyn.t option} let evar_context evi = named_context_of_val evi.evar_hyps @@ -46,7 +47,11 @@ type evar_map1 = evar_info Evarmap.t let empty = Evarmap.empty -let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc [] +let to_list evc = (* Workaround for change in Map.fold behavior *) + let l = ref [] in + Evarmap.iter (fun ev x -> l:=(ev,x)::!l) evc; + !l + let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc [] let find evc k = Evarmap.find k evc let remove evc k = Evarmap.remove k evc @@ -60,9 +65,8 @@ let define evd ev body = try find evd ev with Not_found -> error "Evd.define: cannot define undeclared evar" in let newinfo = - { evar_concl = oldinfo.evar_concl; - evar_hyps = oldinfo.evar_hyps; - evar_body = Evar_defined body} in + { oldinfo with + evar_body = Evar_defined body } in match oldinfo.evar_body with | Evar_empty -> Evarmap.add ev newinfo evd | _ -> anomaly "Evd.define: cannot define an isevar twice" @@ -377,14 +381,7 @@ let create_evar_defs sigma = let evars_of d = d.evars let evars_reset_evd evd d = {d with evars = evd} let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} -let add_conv_pb pb d = -(* let (pbty,c1,c2) = pb in - pperrnl - (Termops.print_constr c1 ++ - (if pbty=Reduction.CUMUL then str " <="++ spc() - else str" =="++spc()) ++ - Termops.print_constr c2);*) - {d with conv_pbs = pb::d.conv_pbs} +let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source ev d = try List.assoc ev d.history with Not_found -> (dummy_loc, InternalHole) @@ -396,7 +393,10 @@ let evar_define sp body isevars = let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd = { evd with evars = add evd.evars evn - {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty}; + {evar_hyps=hyps; + evar_concl=ty; + evar_body=Evar_empty; + evar_extra=None}; history = (evn,src)::evd.history } let is_defined_evar isevars (n,_) = is_defined isevars.evars n @@ -548,14 +548,21 @@ let pr_evar_map sigma = h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) (to_list sigma)) +let pr_constraints pbs = + h 0 + (prlist_with_sep pr_fnl (fun (pbty,t1,t2) -> + print_constr t1 ++ spc() ++ + str (match pbty with + | Reduction.CONV -> "==" + | Reduction.CUMUL -> "<=") ++ + spc() ++ print_constr t2) pbs) + let pr_evar_defs evd = let pp_evm = if evd.evars = empty then mt() else str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in - let n = List.length evd.conv_pbs in let cstrs = - if n=0 then mt() else - str"=> " ++ int n ++ str" constraints" ++ fnl() ++ fnl() in + str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in let pp_met = if evd.metas = Metamap.empty then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd.metas in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index cbc96b04..876c34d2 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 8759 2006-04-28 12:24:14Z herbelin $ i*) +(*i $Id: evd.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) (*i*) open Util @@ -32,7 +32,8 @@ type evar_body = type evar_info = { evar_concl : constr; evar_hyps : Environ.named_context_val; - evar_body : evar_body} + evar_body : evar_body; + evar_extra : Dyn.t option} val eq_evar_info : evar_info -> evar_info -> bool val evar_context : evar_info -> named_context @@ -94,6 +95,7 @@ type 'a freelisted = { rebus : 'a; freemetas : Metaset.t } +val metavars_of : constr -> Metaset.t val mk_freelisted : constr -> constr freelisted val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index e0cdeeee..14136f61 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: inductiveops.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -23,7 +23,7 @@ open Reductionops let type_of_inductive env ind = let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif + Inductive.type_of_inductive env specif (* Return type as quoted by the user *) let type_of_constructor env cstr = @@ -126,6 +126,10 @@ let inductive_nargs env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mib.mind_nparams, mip.mind_nrealargs +let allowed_sorts env (kn,i as ind) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_kelim + (* Annotation for cases *) let make_case_info env ind style pats_source = let (mib,mip) = Inductive.lookup_mind_specif env ind in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index dcd86716..d49b64d9 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductiveops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) +(*i $Id: inductiveops.mli 9194 2006-10-01 09:25:19Z herbelin $ i*) open Names open Term @@ -66,6 +66,8 @@ val constructor_nrealhyps : env -> constructor -> int val get_full_arity_sign : env -> inductive -> rel_context +val allowed_sorts : env -> inductive -> sorts_family list + (* Extract information from an inductive family *) type constructor_summary = { diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 12c1ea33..65ce2ef4 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: matching.ml 8827 2006-05-17 15:15:34Z jforest $ *) +(* $Id: matching.ml 9280 2006-10-25 21:37:37Z herbelin $ *) (*i*) open Util @@ -119,6 +119,8 @@ let matches_core convert allow_partial_app pat c = | PSort (RType _), Sort (Type _) -> sigma + | PApp (p, [||]), _ -> sorec stk sigma p t + | PApp (PApp (h, a1), a2), _ -> sorec stk sigma (PApp(h,Array.append a1 a2)) t diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index f5a81659..59cdad04 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretype_errors.ml 8752 2006-04-27 19:37:33Z herbelin $ *) +(* $Id: pretype_errors.ml 9217 2006-10-05 17:31:23Z notin $ *) open Util open Stdpp @@ -27,6 +27,7 @@ type pretype_error = | NotClean of existential_key * constr * Evd.hole_kind | UnsolvableImplicit of Evd.hole_kind | CannotUnify of constr * constr + | CannotUnifyLocal of Environ.env * constr * constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr @@ -157,6 +158,9 @@ let error_unsolvable_implicit loc env sigma e = let error_cannot_unify env sigma (m,n) = raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) +let error_cannot_unify_local env sigma (e,m,n,sn) = + raise (PretypeError (env_ise sigma env,CannotUnifyLocal (e,m,n,sn))) + let error_cannot_coerce env sigma (m,n) = raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 3c78d48d..137ef639 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretype_errors.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) +(*i $Id: pretype_errors.mli 9217 2006-10-05 17:31:23Z notin $ i*) (*i*) open Pp @@ -29,6 +29,7 @@ type pretype_error = | NotClean of existential_key * constr * Evd.hole_kind | UnsolvableImplicit of Evd.hole_kind | CannotUnify of constr * constr + | CannotUnifyLocal of Environ.env * constr * constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr @@ -96,6 +97,8 @@ val error_unsolvable_implicit : val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b +val error_cannot_unify_local : env -> Evd.evar_map -> Environ.env * constr * constr * constr -> 'b + (*s Ml Case errors *) val error_cant_find_case_type_loc : diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e3cfe974..0b00c82c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 8992 2006-06-27 21:29:18Z herbelin $ *) +(* $Id: pretyping.ml 9338 2006-11-03 13:09:53Z herbelin $ *) open Pp open Util @@ -245,6 +245,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ccl' = mkLambda (Anonymous, ind, ccl) in {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} + let evar_kind_of_term sigma c = + kind_of_term (whd_evar (Evd.evars_of sigma) c) + (*************************************************************************) (* Main pretyping function *) @@ -375,10 +378,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct | Prod (na,c1,c2) -> let hj = pretype (mk_tycon c1) env isevars lvar c in let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in - let typ' = nf_isevar !isevars typ in apply_rec env (n+1) - { uj_val = nf_isevar !isevars value; - uj_type = typ' } + { uj_val = value; + uj_type = typ } rest | _ -> let hj = pretype empty_tycon env isevars lvar c in @@ -386,15 +388,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct (join_loc floc argloc) env (evars_of !isevars) resj [hj] in - let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in + let resj = apply_rec env 1 fj args in let resj = - match kind_of_term resj.uj_val with - | App (f,args) when isInd f -> - let sigma = evars_of !isevars in - let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in - let s = snd (splay_arity env sigma t) in - on_judgment_type (set_inductive_level env s) resj - (* Rem: no need to send sigma: no head evar, it's an arity *) + match evar_kind_of_term !isevars resj.uj_val with + | App (f,args) -> + let f = whd_evar (Evd.evars_of !isevars) f in + begin match kind_of_term f with + | Ind _ (* | Const _ *) -> + let sigma = evars_of !isevars in + let c = mkApp (f,Array.map (whd_evar sigma) args) in + let t = Retyping.get_type_of env sigma c in + make_judge c t + | _ -> resj end | _ -> resj in inh_conv_coerce_to_tycon loc env isevars resj tycon @@ -455,7 +460,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | Some p -> let env_p = push_rels psign env in let pj = pretype_type empty_valcon env_p isevars lvar p in - let ccl = nf_evar (evars_of !isevars) pj.utj_val in + let ccl = nf_isevar !isevars pj.utj_val in let psign = make_arity_signature env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = @@ -475,7 +480,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let tycon = lift_tycon cs.cs_nargs tycon in let fj = pretype tycon env_f isevars lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let ccl = nf_evar (evars_of !isevars) fj.uj_type in + let ccl = nf_isevar !isevars fj.uj_type in let ccl = if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl @@ -632,35 +637,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env isevars lvar c).utj_val in nf_evar (evars_of !isevars) c' - (* [check_evars] fails if some unresolved evar remains *) - (* it assumes that the defined existentials have already been substituted - (should be done in unsafe_infer and unsafe_infer_type) *) - - let check_evars env initial_sigma isevars c = - let sigma = evars_of !isevars in - let rec proc_rec c = - match kind_of_term c with - | Evar (ev,args) -> - assert (Evd.mem sigma ev); - if not (Evd.mem initial_sigma ev) then - let (loc,k) = evar_source ev !isevars in - error_unsolvable_implicit loc env sigma k - | _ -> iter_constr proc_rec c - in - proc_rec c(*; - let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in - if pbs <> [] then begin - pperrnl - (str"TYPING OF "++Termops.print_constr_env env c++fnl()++ - prlist_with_sep fnl - (fun (pb,c1,c2) -> - Termops.print_constr c1 ++ - (if pb=Reduction.CUMUL then str " <="++ spc() - else str" =="++spc()) ++ - Termops.print_constr c2) - pbs ++ fnl()) - end*) - (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... @@ -669,7 +645,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let isevars = ref (create_evar_defs sigma) in let j = pretype empty_tycon env isevars ([],[]) c in - let j = j_nf_evar (evars_of !isevars) j in + let isevars,_ = consider_remaining_unif_problems env !isevars in + let j = j_nf_evar (evars_of isevars) j in check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j @@ -686,8 +663,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let isevars = ref (Evd.create_evar_defs sigma) in let c = pretype_gen isevars env lvar kind c in + let isevars,_ = consider_remaining_unif_problems env !isevars in + let c = nf_evar (evars_of isevars) c in if fail_evar then check_evars env sigma isevars c; - !isevars, c + isevars, c (** Entry points of the high-level type synthesis algorithm *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7bb8c374..b1ed20c2 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretyping.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) +(*i $Id: pretyping.mli 9141 2006-09-15 10:07:01Z herbelin $ i*) (*i*) open Names @@ -78,7 +78,6 @@ sig (* Idem but do not fail on unresolved evars *) val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment - (*i*) (* Internal of Pretyping... *) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index ece536d1..00dd034d 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml 8969 2006-06-22 12:51:04Z msozeau $ *) +(* $Id: rawterm.ml 9226 2006-10-09 16:11:01Z herbelin $ *) (*i*) open Util @@ -26,7 +26,7 @@ type cases_pattern = | PatVar of loc * name | PatCstr of loc * constructor * cases_pattern list * name -let pattern_loc = function +let cases_pattern_loc = function PatVar(loc,_) -> loc | PatCstr(loc,_,_,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 89b13ff0..6c2276d7 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rawterm.mli 8969 2006-06-22 12:51:04Z msozeau $ i*) +(*i $Id: rawterm.mli 9226 2006-10-09 16:11:01Z herbelin $ i*) (*i*) open Util @@ -17,7 +17,8 @@ open Libnames open Nametab (*i*) -(* Untyped intermediate terms, after ASTs and before constr. *) +(**********************************************************************) +(* The kind of patterns that occurs in "match ... with ... end" *) (* locs here refers to the ident's location, not whole pat *) (* the last argument of PatCstr is a possible alias ident for the pattern *) @@ -25,7 +26,13 @@ type cases_pattern = | PatVar of loc * name | PatCstr of loc * constructor * cases_pattern list * name -val pattern_loc : cases_pattern -> loc +val cases_pattern_loc : cases_pattern -> loc + +(**********************************************************************) +(* Untyped intermediate terms, after constr_expr and before constr *) +(* Resolution of names, insertion of implicit arguments placeholder, *) +(* and notations are done, but coercions, inference of implicit *) +(* arguments and pattern-matching compilation are not *) type patvar = identifier diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 74df5eea..5bbaa207 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml 9032 2006-07-07 16:30:34Z herbelin $ *) +(* $Id: recordops.ml 9166 2006-09-23 11:20:06Z herbelin $ *) open Util open Pp @@ -20,6 +20,7 @@ open Libobject open Library open Classops open Mod_subst +open Reductionops (*s A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) @@ -78,7 +79,7 @@ let (inStruc,outStruc) = discharge_function = discharge_structure; export_function = (function x -> Some x) } -let declare_structure (s,c,_,kl,pl) = +let declare_structure (s,c,kl,pl) = Lib.add_anonymous_leaf (inStruc (s,c,kl,pl)) let lookup_structure indsp = Indmap.find indsp !structure_table @@ -197,7 +198,8 @@ let check_and_decompose_canonical_structure ref = let vc = match Environ.constant_opt_value env sp with | Some vc -> vc | None -> error_not_structure ref in - let f,args = match kind_of_term (snd (decompose_lam vc)) with + let body = snd (splay_lambda (Global.env()) Evd.empty vc) in + let f,args = match kind_of_term body with | App (f,args) -> f,args | _ -> error_not_structure ref in let indsp = match kind_of_term f with diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 91bc2ba1..0a05aef6 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli 9032 2006-07-07 16:30:34Z herbelin $ i*) +(*i $Id: recordops.mli 9082 2006-08-24 17:03:28Z herbelin $ i*) (*i*) open Names @@ -22,7 +22,7 @@ open Library constructor (the name of which defaults to Build_S) *) val declare_structure : - inductive * identifier * int * bool list * constant option list -> unit + inductive * identifier * bool list * constant option list -> unit (* [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 82cc1b7d..19f515d0 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: reductionops.ml 9106 2006-09-01 11:18:17Z herbelin $ *) open Pp open Util @@ -37,11 +37,12 @@ type 'a stack_member = and 'a stack = 'a stack_member list let empty_stack = [] -let append_stack_list = function +let append_stack_list l s = + match (l,s) with | ([],s) -> s | (l1, Zapp l :: s) -> Zapp (l1@l) :: s | (l1, s) -> Zapp l1 :: s -let append_stack v s = append_stack_list (Array.to_list v, s) +let append_stack v s = append_stack_list (Array.to_list v) s (* Collapse the shifts in the stack *) let zshift n s = @@ -227,6 +228,7 @@ open RedFlags (* Local *) let beta = mkflags [fbeta] +let eta = mkflags [feta] let evar = mkflags [fevar] let betaevar = mkflags [fevar; fbeta] let betaiota = mkflags [fiota; fbeta] @@ -251,7 +253,7 @@ let rec stacklam recfun env t stack = | _ -> recfun (substl env t, stack) let beta_applist (c,l) = - stacklam app_stack [] c (append_stack (Array.of_list l) empty_stack) + stacklam app_stack [] c (append_stack_list l empty_stack) (* Iota reduction tools *) @@ -261,7 +263,7 @@ type 'a miota_args = { mci : case_info; (* special info to re-build pattern *) mcargs : 'a list; (* the constructor's arguments *) mlf : 'a array } (* the branch code vector *) - + let reducible_mind_case c = match kind_of_term c with | Construct _ | CoFix _ -> true | _ -> false @@ -505,6 +507,10 @@ let whd_betadeltaiota_nolet_stack env sigma x = let whd_betadeltaiota_nolet env sigma x = app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack)) +(* 3. Eta reduction Functions *) + +let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack)) + (****************************************************************************) (* Reduction Functions *) (****************************************************************************) @@ -641,7 +647,7 @@ let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq let whd_meta metamap c = match kind_of_term c with | Meta p -> (try List.assoc p metamap with Not_found -> c) | _ -> c - + (* Try to replace all metas. Does not replace metas in the metas' values * Differs from (strong whd_meta). *) let plain_instance s c = @@ -668,7 +674,7 @@ let plain_instance s c = | _ -> map_constr irec u in if s = [] then c else irec c - + (* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *) let instance s c = if s = [] then c else local_strong whd_betaiota (plain_instance s c) @@ -746,7 +752,7 @@ let splay_arity env sigma c = | _ -> error "not an arity" let sort_of_arity env c = snd (splay_arity env Evd.empty c) - + let decomp_n_prod env sigma n = let rec decrec env m ln c = if m = 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with @@ -764,7 +770,12 @@ let decomp_sort env sigma t = | Sort s -> s | _ -> raise NotASort -(* One step of approximation *) +let is_sort env sigma arity = + try let _ = decomp_sort env sigma arity in true + with NotASort -> false + +(* reduction to head-normal-form allowing delta/zeta only in argument + of case/fix (heuristic used by evar_conv) *) let rec apprec env sigma s = let (t, stack as s) = whd_betaiota_state s in @@ -782,8 +793,6 @@ let rec apprec env sigma s = | NotReducible -> s) | _ -> s -let hnf env sigma c = apprec env sigma (c, empty_stack) - (* A reduction function like whd_betaiota but which keeps casts * and does not reduce redexes containing existential variables. * Used in Correctness. diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 78afd22b..1e9b3b5b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reductionops.mli 8812 2006-05-13 11:46:02Z herbelin $ i*) +(*i $Id: reductionops.mli 9106 2006-09-01 11:18:17Z herbelin $ i*) (*i*) open Names @@ -37,6 +37,7 @@ and 'a stack = 'a stack_member list val empty_stack : 'a stack val append_stack : 'a array -> 'a stack -> 'a stack +val append_stack_list : 'a list -> 'a stack -> 'a stack val decomp_stack : 'a stack -> ('a * 'a stack) option val list_of_stack : 'a stack -> 'a list @@ -140,6 +141,7 @@ val whd_betadeltaiotaeta_stack : stack_reduction_function val whd_betadeltaiotaeta_state : state_reduction_function val whd_betadeltaiotaeta : reduction_function +val whd_eta : constr -> constr @@ -162,6 +164,7 @@ val decomp_n_prod : val splay_prod_assum : env -> evar_map -> constr -> Sign.rel_context * constr val decomp_sort : env -> evar_map -> types -> sorts +val is_sort : env -> evar_map -> types -> bool type 'a miota_args = { mP : constr; (* the result type *) @@ -206,11 +209,8 @@ 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 *) +(*s Heuristic for Conversion with Evar *) -(*i -val hnf : env -> 'a evar_map -> constr -> constr * constr list -i*) val apprec : state_reduction_function (*s Meta-related reduction functions *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 428a7306..ecead438 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: retyping.ml 9314 2006-10-29 20:11:08Z herbelin $ *) open Util open Term @@ -17,6 +17,7 @@ open Reductionops open Environ open Typeops open Declarations +open Termops let rec subst_type env sigma typ = function | [] -> typ @@ -38,6 +39,11 @@ let sort_of_atomic_type env sigma ft args = | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args)) in concl_of_arity env ft +let type_of_var env id = + try let (_,_,ty) = lookup_named id env in ty + with Not_found -> + anomaly ("type_of: variable "^(string_of_id id)^" unbound") + let typeur sigma metamap = let rec type_of env cstr= match kind_of_term cstr with @@ -47,18 +53,11 @@ let typeur sigma metamap = | Rel n -> let (_,_,ty) = lookup_rel n env in lift n ty - | Var id -> - (try - let (_,_,ty) = lookup_named id env in - body_of_type ty - with Not_found -> - anomaly ("type_of: variable "^(string_of_id id)^" unbound")) - | Const c -> - let cb = lookup_constant c env in - body_of_type cb.const_type + | Var id -> type_of_var env id + | Const cst -> Typeops.type_of_constant env cst | Evar ev -> Evd.existential_type sigma ev - | Ind ind -> body_of_type (type_of_inductive env ind) - | Construct cstr -> body_of_type (type_of_constructor env cstr) + | Ind ind -> type_of_inductive env ind + | Construct cstr -> type_of_constructor env cstr | Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) @@ -73,8 +72,8 @@ let typeur sigma metamap = subst1 b (type_of (push_rel (name,Some b,c1) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when isInd f -> - let t = type_of_inductive_knowing_parameters env (destInd f) args in + | App(f,args) when isGlobalRef f -> + let t = type_of_global_reference_knowing_parameters env f args in strip_outer_cast (subst_type env sigma t (Array.to_list args)) | App(f,args) -> strip_outer_cast @@ -97,8 +96,8 @@ let typeur sigma metamap = | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) - | App(f,args) when isInd f -> - let t = type_of_inductive_knowing_parameters env (destInd f) args in + | App(f,args) when isGlobalRef f -> + let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> @@ -117,18 +116,27 @@ let typeur sigma metamap = anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) - and type_of_inductive_knowing_parameters env ind args = - let (_,mip) = lookup_mind_specif env ind in + and type_of_global_reference_knowing_parameters env c args = let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in - Inductive.type_of_inductive_knowing_parameters env mip argtyps + match kind_of_term c with + | Ind ind -> + let (_,mip) = lookup_mind_specif env ind in + Inductive.type_of_inductive_knowing_parameters env mip argtyps + | Const cst -> + let t = constant_type env cst in + Typeops.type_of_constant_knowing_parameters env t argtyps + | Var id -> type_of_var env id + | Construct cstr -> type_of_constructor env cstr + | _ -> assert false - in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters + in type_of, sort_of, sort_family_of, + type_of_global_reference_knowing_parameters let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c -let type_of_inductive_knowing_parameters env sigma ind args = - let _,_,_,f = typeur sigma [] in f env ind args +let type_of_global_reference_knowing_parameters env sigma c args = + let _,_,_,f = typeur sigma [] in f env c args let get_type_of_with_meta env sigma metamap = let f,_,_,_ = typeur sigma metamap in f env diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 923123c5..733cb4b1 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: retyping.mli 8871 2006-05-28 16:46:48Z herbelin $ i*) +(*i $Id: retyping.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) (*i*) open Names @@ -34,5 +34,6 @@ val get_assumption_of : env -> evar_map -> constr -> types (* Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment -val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> +val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> constr array -> types + diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 823da969..9b8764f2 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: termops.ml 9314 2006-10-29 20:11:08Z herbelin $ *) open Pp open Util @@ -855,7 +855,12 @@ let next_global_ident_away allow_secvar id avoid = else next_global_ident_from allow_secvar (lift_ident id) avoid -(* Nouvelle version de renommage des variables (DEC 98) *) +let isGlobalRef c = + match kind_of_term c with + | Const _ | Ind _ | Construct _ | Var _ -> true + | _ -> false + +(* nouvelle version de renommage des variables (DEC 98) *) (* This is the algorithm to display distinct bound variables - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste @@ -1020,3 +1025,9 @@ let rec rename_bound_var env l c = | Cast (c,k,t) -> mkCast (rename_bound_var env l c, k,t) | x -> c +(* Combinators on judgments *) + +let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type } +let on_judgment_value f j = { j with uj_val = f j.uj_val } +let on_judgment_type f j = { j with uj_type = f j.uj_type } + diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 49de4838..e406b148 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) +(*i $Id: termops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) open Util open Pp @@ -203,3 +203,11 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t (* Test if an identifier is the basename of a global reference *) val is_section_variable : identifier -> bool + +val isGlobalRef : constr -> bool + +(* Combinators on judgments *) + +val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment +val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment +val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 78902a7d..63fdd6d5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typing.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -53,7 +53,7 @@ let rec execute env evd cstr = j_nf_evar (evars_of evd) (judge_of_variable env id) | Const c -> - make_judge cstr (nf_evar (evars_of evd) (constant_type env c)) + make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c)) | Ind ind -> make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind)) @@ -90,12 +90,17 @@ let rec execute env evd cstr = | App (f,args) -> let jl = execute_array env evd args in let j = - if isInd f then - (* Sort-polymorphism of inductive types *) - judge_of_inductive_knowing_parameters env (destInd f) - (jv_nf_evar (evars_of evd) jl) - else - execute env evd f + match kind_of_term f with + | Ind ind -> + (* Sort-polymorphism of inductive types *) + judge_of_inductive_knowing_parameters env ind + (jv_nf_evar (evars_of evd) jl) + | Const cst -> + (* Sort-polymorphism of inductive types *) + judge_of_constant_knowing_parameters env cst + (jv_nf_evar (evars_of evd) jl) + | _ -> + execute env evd f in fst (judge_of_apply env j jl) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e4bde925..fabe24ef 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 8759 2006-04-28 12:24:14Z herbelin $ *) +(* $Id: unification.ml 9217 2006-10-05 17:31:23Z notin $ *) open Pp open Util @@ -47,6 +47,16 @@ let abstract_list_all env sigma typ c l = with UserError _ -> raise (PretypeError (env,CannotGeneralize typ)) +(**) + +let solve_pattern_eqn_array env f l c (metasubst,evarsubst) = + match kind_of_term f with + | Meta k -> + (k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst + | Evar ev -> + (* Currently unused: incompatible with eauto/eassumption backtracking *) + metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst + | _ -> assert false (*******************************) @@ -70,58 +80,77 @@ let sort_eqns = unify_r2l let unify_0 env sigma cv_pb mod_delta m n = let trivial_unify pb substn m n = - if (not(occur_meta m)) && (if mod_delta then is_fconv pb env sigma m n else eq_constr m n) then substn + if (not(occur_meta m)) && + (if mod_delta then is_fconv pb env sigma m n else eq_constr m n) + then substn else error_cannot_unify env sigma (m,n) in - let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n = - let cM = Evarutil.whd_castappevar sigma m - and cN = Evarutil.whd_castappevar sigma n in - match (kind_of_term cM,kind_of_term cN) with - | Meta k1, Meta k2 -> - if k1 < k2 then (k1,cN)::metasubst,evarsubst - else if k1 = k2 then substn - else (k2,cM)::metasubst,evarsubst - | Meta k, _ -> (k,cN)::metasubst,evarsubst - | _, Meta k -> (k,cM)::metasubst,evarsubst - | Evar _, _ -> metasubst,((cM,cN)::evarsubst) - | _, Evar _ -> metasubst,((cN,cM)::evarsubst) - - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> - unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> - unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2 - | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN - | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c) - - | App (f1,l1), App (f2,l2) -> - let len1 = Array.length l1 - and len2 = Array.length l2 in - let (f1,l1,f2,l2) = - if len1 = len2 then (f1,l1,f2,l2) - else if len1 < len2 then - let extras,restl2 = array_chop (len2-len1) l2 in - (f1, l1, appvect (f2,extras), restl2) - else - let extras,restl1 = array_chop (len1-len2) l1 in - (appvect (f1,extras), restl1, f2, l2) in - (try - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV substn f1 f2) l1 l2 - with ex when precatchable_exception ex -> - trivial_unify pb substn cM cN) - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2 - - | _ -> trivial_unify pb substn cM cN - + let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn = + let cM = Evarutil.whd_castappevar sigma curm + and cN = Evarutil.whd_castappevar sigma curn in + match (kind_of_term cM,kind_of_term cN) with + | Meta k1, Meta k2 -> + if k1 < k2 + then (k1,cN)::metasubst,evarsubst + else if k1 = k2 then substn else (k2,cM)::metasubst,evarsubst + | Meta k, _ -> + (* Here we check that [cN] does not contain any local variables *) + if (closedn (nb_rel env) cN) + then (k,cN)::metasubst,evarsubst + else error_cannot_unify_local curenv sigma (curenv,m,n,cN) + | _, Meta k -> + (* Here we check that [cM] does not contain any local variables *) + if (closedn (nb_rel env) cM) + then (k,cM)::metasubst,evarsubst + else error_cannot_unify_local curenv sigma (curenv,m,n,cM) + | Evar _, _ -> metasubst,((cM,cN)::evarsubst) + | _, Evar _ -> metasubst,((cN,cM)::evarsubst) + | Lambda (na,t1,c1), Lambda (_,t2,c2) -> + unirec_rec (push_rel_assum (na,t1) curenv) CONV + (unirec_rec curenv CONV substn t1 t2) c1 c2 + | Prod (na,t1,c1), Prod (_,t2,c2) -> + unirec_rec (push_rel_assum (na,t1) curenv) pb + (unirec_rec curenv CONV substn t1 t2) c1 c2 + | LetIn (_,b,_,c), _ -> unirec_rec curenv pb substn (subst1 b c) cN + | _, LetIn (_,b,_,c) -> unirec_rec curenv pb substn cM (subst1 b c) + + | App (f1,l1), App (f2,l2) -> + if + isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) + then + solve_pattern_eqn_array curenv f1 l1 cN substn + else if + isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) + then + solve_pattern_eqn_array curenv f2 l2 cM substn + else + let len1 = Array.length l1 + and len2 = Array.length l2 in + let (f1,l1,f2,l2) = + if len1 = len2 then (f1,l1,f2,l2) + else if len1 < len2 then + let extras,restl2 = array_chop (len2-len1) l2 in + (f1, l1, appvect (f2,extras), restl2) + else + let extras,restl1 = array_chop (len1-len2) l1 in + (appvect (f1,extras), restl1, f2, l2) in + (try + array_fold_left2 (unirec_rec curenv CONV) + (unirec_rec curenv CONV substn f1 f2) l1 l2 + with ex when precatchable_exception ex -> + trivial_unify pb substn cM cN) + | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> + array_fold_left2 (unirec_rec curenv CONV) + (unirec_rec curenv CONV + (unirec_rec curenv CONV substn p1 p2) c1 c2) cl1 cl2 + | _ -> trivial_unify pb substn cM cN in - if (not(occur_meta m)) && - (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n) - then - ([],[]) - else - let (mc,ec) = unirec_rec cv_pb ([],[]) m n in - ((*sort_eqns*) mc, (*sort_eqns*) ec) + if (not(occur_meta m)) && + (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n) + then + ([],[]) + else + let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in + ((*sort_eqns*) mc, (*sort_eqns*) ec) (* Unification @@ -442,30 +471,30 @@ let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd = let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd = let hd1,l1 = whd_stack ty1 in let hd2,l2 = whd_stack ty2 in - match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with - (* Pattern case *) - | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) - when List.length l1 = List.length l2 -> - (try - w_typed_unify env cv_pb mod_delta ty1 ty2 evd - with ex when precatchable_exception ex -> - try - w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound c) as e -> raise e - | ex when precatchable_exception ex -> - error "Cannot solve a second-order unification problem") - - (* Second order case *) - | (Meta _, true, _, _ | _, _, Meta _, true) -> - (try - w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound c) as e -> raise e - | ex when precatchable_exception ex -> - try - w_typed_unify env cv_pb mod_delta ty1 ty2 evd - with ex when precatchable_exception ex -> - error "Cannot solve a second-order unification problem") - - (* General case: try first order *) - | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd + match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with + (* Pattern case *) + | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) + when List.length l1 = List.length l2 -> + (try + w_typed_unify env cv_pb mod_delta ty1 ty2 evd + with ex when precatchable_exception ex -> + try + w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd + with PretypeError (env,NoOccurrenceFound c) as e -> raise e + | ex when precatchable_exception ex -> + error "Cannot solve a second-order unification problem") + + (* Second order case *) + | (Meta _, true, _, _ | _, _, Meta _, true) -> + (try + w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd + with PretypeError (env,NoOccurrenceFound c) as e -> raise e + | ex when precatchable_exception ex -> + try + w_typed_unify env cv_pb mod_delta ty1 ty2 evd + with ex when precatchable_exception ex -> + error "Cannot solve a second-order unification problem") + + (* General case: try first order *) + | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml new file mode 100644 index 00000000..55f798de --- /dev/null +++ b/pretyping/vnorm.ml @@ -0,0 +1,271 @@ +open Names +open Declarations +open Term +open Environ +open Inductive +open Reduction +open Vm + +(*******************************************) +(* Calcul de la forme normal d'un terme *) +(*******************************************) + +let crazy_type = mkSet + +let decompose_prod env t = + let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + if name = Anonymous then (Name (id_of_string "x"),dom,codom) + else res + +exception Find_at of int + +(* rend le numero du constructeur correspondant au tag [tag], + [cst] = true si c'est un constructeur constant *) + +let invert_tag cst tag reloc_tbl = + try + for j = 0 to Array.length reloc_tbl - 1 do + let tagj,arity = reloc_tbl.(j) in + if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then + raise (Find_at j) + else () + done;raise Not_found + with Find_at j -> (j+1) + (* Argggg, ces constructeurs de ... qui commencent a 1*) + +let find_rectype_a env c = + let (t, l) = + let t = whd_betadeltaiota env c in + try destApp t with _ -> (t,[||]) in + match kind_of_term t with + | Ind ind -> (ind, l) + | _ -> raise Not_found + +(* Instantiate inductives and parameters in constructor type *) +let build_type_constructor mind mib params ctyp = + let si = ind_subst mind mib in + let ctyp1 = substl si ctyp in + let nparams = Array.length params in + if nparams = 0 then ctyp1 + else + let _,ctyp2 = decompose_prod_n nparams ctyp1 in + let sp = List.rev (Array.to_list params) in substl sp ctyp2 + +let construct_of_constr_const env tag typ = + let ind,params = find_rectype env typ in + let (_,mip) = lookup_mind_specif env ind in + let i = invert_tag true tag mip.mind_reloc_tbl in + applistc (mkConstruct(ind,i)) params + +let construct_of_constr_block env tag typ = + let (mind,_ as ind), allargs = find_rectype_a env typ in + let (mib,mip) = lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let i = invert_tag false tag mip.mind_reloc_tbl in + let params = Array.sub allargs 0 nparams in + let specif = mip.mind_nf_lc in + let ctyp = build_type_constructor mind mib params specif.(i-1) in + (mkApp(mkConstruct(ind,i), params), ctyp) + +let constr_type_of_idkey env idkey = + match idkey with + | ConstKey cst -> + mkConst cst, Typeops.type_of_constant env cst + | VarKey id -> + let (_,_,ty) = lookup_named id env in + mkVar id, ty + | RelKey i -> + let n = (nb_rel env - i) in + let (_,_,ty) = lookup_rel n env in + mkRel n, lift n ty + +let type_of_ind env ind = + type_of_inductive env (Inductive.lookup_mind_specif env ind) + +let build_branches_type env (mind,_ as _ind) mib mip params dep p = + let rtbl = mip.mind_reloc_tbl in + (* [build_one_branch i cty] construit le type de la ieme branche (commence + a 0) et les lambda correspondant aux realargs *) + let build_one_branch i cty = + let typi = build_type_constructor mind mib params cty in + let decl,indapp = Term.decompose_prod typi in + let ind,cargs = find_rectype_a env indapp in + let nparams = Array.length params in + let carity = snd (rtbl.(i)) in + let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in + let codom = + let papp = mkApp(p,crealargs) in + if dep then + let cstr = ith_constructor_of_inductive ind (i+1) in + let relargs = Array.init carity (fun i -> mkRel (carity-i)) in + let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in + mkApp(papp,[|dep_cstr|]) + else papp + in + decl, codom + in Array.mapi build_one_branch mip.mind_nf_lc + +let build_case_type dep p realargs c = + if dep then mkApp(mkApp(p, realargs), [|c|]) + else mkApp(p, realargs) + +(* La fonction de normalisation *) + +let rec nf_val env v t = nf_whd env (whd_val v) t + +and nf_vtype env v = nf_val env v crazy_type + +and nf_whd env whd typ = + match whd with + | Vsort s -> mkSort s + | Vprod p -> + let dom = nf_vtype env (dom p) in + let name = Name (id_of_string "x") in + let vc = body_of_vfun (nb_rel env) (codom p) in + let codom = nf_vtype (push_rel (name,None,dom) env) vc in + mkProd(name,dom,codom) + | Vfun f -> nf_fun env f typ + | Vfix(f,None) -> nf_fix env f + | Vfix(f,Some vargs) -> fst (nf_fix_app env f vargs) + | Vcofix(cf,_,None) -> nf_cofix env cf + | Vcofix(cf,_,Some vargs) -> + let cfd = nf_cofix env cf in + let i,(_,ta,_) = destCoFix cfd in + let t = ta.(i) in + let _, args = nf_args env vargs t in + mkApp(cfd,args) + | Vconstr_const n -> construct_of_constr_const env n typ + | Vconstr_block b -> + let capp,ctyp = construct_of_constr_block env (btag b) typ in + let args = nf_bargs env b ctyp in + mkApp(capp,args) + | Vatom_stk(Aid idkey, stk) -> + let c,typ = constr_type_of_idkey env idkey in + nf_stk env c typ stk + | Vatom_stk(Aiddef(idkey,v), stk) -> + nf_whd env (whd_stack v stk) typ + | Vatom_stk(Aind ind, stk) -> + nf_stk env (mkInd ind) (type_of_ind env ind) stk + +and nf_stk env c t stk = + match stk with + | [] -> c + | Zapp vargs :: stk -> + let t, args = nf_args env vargs t in + nf_stk env (mkApp(c,args)) t stk + | Zfix (f,vargs) :: stk -> + let fa, typ = nf_fix_app env f vargs in + let _,_,codom = decompose_prod env typ in + nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk + | Zswitch sw :: stk -> + let (mind,_ as ind),allargs = find_rectype_a env t in + let (mib,mip) = Inductive.lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let params,realargs = Util.array_chop nparams allargs in + let pT = + hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in + let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in + (* Calcul du type des branches *) + let btypes = build_branches_type env ind mib mip params dep p in + (* calcul des branches *) + let bsw = branch_of_switch (nb_rel env) sw in + let mkbranch i (n,v) = + let decl,codom = btypes.(i) in + let env = + List.fold_right + (fun (name,t) env -> push_rel (name,None,t) env) decl env in + let b = nf_val env v codom in + compose_lam decl b + in + let branchs = Array.mapi mkbranch bsw in + let tcase = build_case_type dep p realargs c in + let ci = case_info sw in + nf_stk env (mkCase(ci, p, c, branchs)) tcase stk + +and nf_predicate env ind mip params v pT = + match whd_val v, kind_of_term pT with + | Vfun f, Prod _ -> + let k = nb_rel env in + let vb = body_of_vfun k f in + let name,dom,codom = decompose_prod env pT in + let dep,body = + nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in + dep, mkLambda(name,dom,body) + | Vfun f, _ -> + let k = nb_rel env in + let vb = body_of_vfun k f in + let name = Name (id_of_string "c") in + let n = mip.mind_nrealargs in + let rargs = Array.init n (fun i -> mkRel (n-i)) in + let dom = mkApp(mkApp(mkInd ind,params),rargs) in + let body = nf_vtype (push_rel (name,None,dom) env) vb in + true, mkLambda(name,dom,body) + | _, _ -> false, nf_val env v crazy_type + +and nf_args env vargs t = + let t = ref t in + let len = nargs vargs in + let args = + Array.init len + (fun i -> + let _,dom,codom = decompose_prod env !t in + let c = nf_val env (arg vargs i) dom in + t := subst1 c codom; c) in + !t,args + +and nf_bargs env b t = + let t = ref t in + let len = bsize b in + let args = + Array.init len + (fun i -> + let _,dom,codom = decompose_prod env !t in + let c = nf_val env (bfield b i) dom in + t := subst1 c codom; c) in + args + +and nf_fun env f typ = + let k = nb_rel env in + let vb = body_of_vfun k f in + let name,dom,codom = decompose_prod env typ in + let body = nf_val (push_rel (name,None,dom) env) vb codom in + mkLambda(name,dom,body) + +and nf_fix env f = + let init = current_fix f in + let rec_args = rec_args f in + let k = nb_rel env in + let vb, vt = reduce_fix k f in + let ndef = Array.length vt in + let ft = Array.map (fun v -> nf_val env v crazy_type) vt in + let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in + let env = push_rec_types (name,ft,ft) env in + let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in + mkFix ((rec_args,init),(name,ft,fb)) + +and nf_fix_app env f vargs = + let fd = nf_fix env f in + let (_,i),(_,ta,_) = destFix fd in + let t = ta.(i) in + let t, args = nf_args env vargs t in + mkApp(fd,args),t + +and nf_cofix env cf = + let init = current_cofix cf in + let k = nb_rel env in + let vb,vt = reduce_cofix k cf in + let ndef = Array.length vt in + let cft = Array.map (fun v -> nf_val env v crazy_type) vt in + let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in + let env = push_rec_types (name,cft,cft) env in + let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in + mkCoFix (init,(name,cft,cfb)) + +let cbv_vm env c t = + let transp = transp_values () in + if not transp then set_transp_values true; + let v = Vconv.val_of_constr env c in + let c = nf_val env v t in + if not transp then set_transp_values false; + c + diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli new file mode 100644 index 00000000..2ea94bfb --- /dev/null +++ b/pretyping/vnorm.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> types -> constr + -- cgit v1.2.3