| _ -> raise (AssertFailure "Prod or MutInd expected")
and type_of_aux' metasenv context t =
- let rec type_of_aux subst metasenv context =
+ let rec type_of_aux subst metasenv context t =
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
- function
+ match t with
+(* function *)
C.Rel n ->
(try
match List.nth context (n - 1) with
in
ty,subst',metasenv'
| C.Meta (n,l) ->
- let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- let subst',metasenv' =
- check_metasenv_consistency n subst metasenv context canonical_context l
- in
- CicSubstitution.lift_meta l ty, subst', metasenv'
+ (try
+ let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in
+ let subst,metasenv =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
+ with CicMetaSubst.SubstNotFound _ ->
+ let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
+ let subst,metasenv =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ CicSubstitution.lift_meta l ty, subst, metasenv)
(* TASSI: CONSTRAINT *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
CicSubstitution.subst s inferredty,subst',metasenv'
- | C.Appl (he::tl) when List.length tl > 0 ->
+ | C.Appl (he::((_::_) as tl)) ->
let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
let tlbody_and_type,subst'',metasenv'' =
List.fold_right
let no_args = count_prod arity in
(* now, create a "generic" MutInd *)
let metasenv,left_args =
- CicMkImplicit.n_fresh_metas metasenv context no_left_params in
+ CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
let metasenv,right_args =
let no_right_params = no_args - no_left_params in
if no_right_params < 0 then assert false
- else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
+ else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
let metasenv,exp_named_subst =
- CicMkImplicit.fresh_subst metasenv context expl_params in
+ CicMkImplicit.fresh_subst metasenv subst context expl_params in
let expected_type =
if no_args = 0 then
C.MutInd (uri,i,exp_named_subst)
| ((uri,t) as subst)::tl ->
let typeofvar =
CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: why was this code here? it is wrong
(match CicEnvironment.get_cooked_obj ~trust:false uri with
Cic.Variable (_,Some bo,_,_) ->
raise
(RefineFailure
("Unkown variable definition " ^ UriManager.string_of_uri uri))
) ;
+*)
let typeoft,metasubst',metasenv' =
type_of_aux metasubst metasenv context t
in
- try
- let metasubst'',metasenv'' =
+ let metasubst'',metasenv'' =
+ try
fo_unif_subst metasubst' context metasenv' typeoft typeofvar
- in
- check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
- with _ ->
- raise (RefineFailure "Wrong Explicit Named Substitution")
+ with _ ->
+ raise (RefineFailure
+ ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
+ " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
+ in
+ check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
in
check_exp_named_subst_aux metasubst metasenv []
* likely to know the exact value of the result e.g. if the rhs is a
* Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
- CicMkImplicit.mk_implicit_sort metasenv in
+ CicMkImplicit.mk_implicit_sort metasenv subst in
let (subst, metasenv) =
fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
in
let rec mk_prod metasenv context =
function
[] ->
- let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+ let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
metasenv,Cic.Meta (idx, irl)
| (_,argty)::tl ->
- let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+ let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
(* then I generate a name --- using the hint name_hint *)
(* --- that is fresh in (context'@context). *)
let name_hint =
- FreshNamesGenerator.mk_fresh_name
- (CicMetaSubst.apply_subst_metasenv subst metasenv)
+ FreshNamesGenerator.mk_fresh_name metasenv
+(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
(CicMetaSubst.apply_subst_context subst context)
Cic.Anonymous
(CicMetaSubst.apply_subst subst argty)
in
let substituted_t = CicMetaSubst.apply_subst subst' t in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
- let substituted_metasenv =
- CicMetaSubst.apply_subst_metasenv subst' metasenv'
+ let substituted_metasenv = metasenv'
+(* CicMetaSubst.apply_subst_metasenv subst' metasenv' *)
in
let cleaned_t =
FreshNamesGenerator.clean_dummy_dependent_types substituted_t in