diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/nativenorm.ml | 28 | ||||
-rw-r--r-- | pretyping/unification.ml | 9 | ||||
-rw-r--r-- | pretyping/unification.mli | 3 | ||||
-rw-r--r-- | pretyping/vnorm.ml | 20 |
4 files changed, 39 insertions, 21 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 7666ce0eb..4b8e0e096 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -312,10 +312,10 @@ and nf_atom_type env sigma atom = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env + hnf_prod_applist_assum env nparamdecls (Inductiveops.type_of_inductive env ind) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma ind mip params p pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in @@ -372,20 +372,24 @@ and nf_atom_type env sigma atom = and nf_predicate env sigma ind mip params v pT = - match kind_of_value v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in - let name,dom,codom = - try decompose_prod env pT with - DestKO -> - CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") - in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> false, nf_type env sigma v + end + | _ -> + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in let name = Name (Id.of_string "c") in @@ -395,7 +399,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_type env sigma v + | _ -> false, nf_type env sigma v and nf_evar env sigma evk ty args = let evi = try Evd.find sigma evk with Not_found -> assert false in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a8a4003dc..5cf6e4b26 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -398,8 +398,13 @@ let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with modulo_betaiota = false; } -let default_no_delta_unify_flags () = - let flags = default_no_delta_core_unify_flags () in { +let default_no_delta_unify_flags ts = + let flags = default_no_delta_core_unify_flags () in + let flags = { flags with + modulo_conv_on_closed_terms = Some ts; + modulo_delta_types = ts + } in + { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = flags; diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 16ce5c93d..e2e261ae7 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Constr open EConstr open Environ @@ -40,7 +41,7 @@ val default_core_unify_flags : unit -> core_unify_flags val default_no_delta_core_unify_flags : unit -> core_unify_flags val default_unify_flags : unit -> unify_flags -val default_no_delta_unify_flags : unit -> unify_flags +val default_no_delta_unify_flags : transparent_state -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index a1ba4a6a9..14c9f49b1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -266,7 +266,6 @@ and nf_stk ?from:(from=0) env sigma c t stk = let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma ind mib mip u params dep p in @@ -288,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> assert false + end + | _ -> + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in let name = Name (Id.of_string "c") in @@ -306,7 +314,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_val env sigma v crazy_type + | _ -> false, nf_val env sigma v crazy_type and nf_args env sigma vargs ?from:(f=0) t = let t = ref t in |