open Printf
exception RefineFailure of string;;
-
-exception Impossible of int;;
-exception NotRefinable of string;;
exception Uncertain of string;;
-exception WrongUriToConstant of string;;
-exception WrongUriToVariable of string;;
-exception ListTooShort;;
-exception WrongUriToMutualInductiveDefinitions of string;;
-exception RelToHiddenHypothesis;;
-exception WrongArgumentNumber;;
-
-let fdebug = ref 0;;
-let debug t context =
- let rec debug_aux t i =
- let module C = Cic in
- let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
- in
- if !fdebug = 0 then
- raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
- (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
-;;
+exception AssertFailure of string;;
let debug_print = prerr_endline
+let fo_unif_subst subst context metasenv t1 t2 =
+ try
+ CicUnification.fo_unif_subst subst context metasenv t1 t2
+ with
+ (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+ | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
let rec split l n =
match (l,n) with
(l,0) -> ([], l)
| (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
- | (_,_) -> raise ListTooShort
+ | (_,_) -> raise (AssertFailure "split: list too short")
;;
let rec type_of_constant uri =
match CicEnvironment.get_cooked_obj uri with
C.Constant (_,_,ty,_) -> ty
| C.CurrentProof (_,_,_,ty,_) -> ty
- | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
and type_of_variable uri =
let module C = Cic in
let module U = UriManager in
match CicEnvironment.get_cooked_obj uri with
C.Variable (_,_,ty,_) -> ty
- | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown variable definition " ^ UriManager.string_of_uri uri))
and type_of_mutual_inductive_defs uri i =
let module C = Cic in
C.InductiveDefinition (dl,_,_) ->
let (_,_,arity,_) = List.nth dl i in
arity
- | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
and type_of_mutual_inductive_constr uri i j =
let module C = Cic in
let (_,_,_,cl) = List.nth dl i in
let (_,ty) = List.nth cl (j-1) in
ty
- | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
let module C = Cic in
- let module R = CicMetaSubst in
- let module Un = CicUnification in
- match R.whd subst context expectedtype with
+ (* let module R = CicMetaSubst in *)
+ let module R = CicReduction in
+ match R.whd ~subst context expectedtype with
C.MutInd (_,_,_) ->
(n,context,actualtype, [term]), subst, metasenv
| C.Appl (C.MutInd (_,_,_)::tl) ->
| C.Prod (name,so,de) ->
(* we expect that the actual type of the branch has the due
number of Prod *)
- (match R.whd subst context actualtype with
+ (match R.whd ~subst context actualtype with
C.Prod (name',so',de') ->
let subst, metasenv =
- Un.fo_unif_subst subst context metasenv so so' in
+ fo_unif_subst subst context metasenv so so' in
let term' =
(match CicSubstitution.lift 1 term with
C.Appl l -> C.Appl (l@[C.Rel 1])
(* we should also check that the name variable is anonymous in
the actual type de' ?? *)
check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
- | _ -> raise WrongArgumentNumber)
- | _ -> raise (NotRefinable "Prod or MutInd expected")
+ | _ -> raise (AssertFailure "Wrong number of arguments"))
+ | _ -> 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
- let module Un = CicUnification in
- function
+ match t with
+(* function *)
C.Rel n ->
(try
match List.nth context (n - 1) with
| Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
| Some (_,C.Def (bo,None)) ->
type_of_aux subst metasenv context (S.lift n bo)
- | None -> raise RelToHiddenHypothesis
+ | None -> raise (RefineFailure "Rel to hidden hypothesis")
with
- _ -> raise (NotRefinable "Not a close term")
+ _ -> raise (RefineFailure "Not a close term")
)
| C.Var (uri,exp_named_subst) ->
- incr fdebug ;
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
let ty =
CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
in
- decr fdebug ;
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'
- | C.Sort s ->
- C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
- subst,metasenv
- | C.Implicit -> raise (Impossible 21)
+ (try
+ let (canonical_context, term) = CicUtil.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 CicUtil.Subst_not_found _ ->
+ 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
+ if not (CicUniv.add_gt t' t ) then
+ assert false (* t' is fresh! an error in CicUniv *)
+ else
+ C.Sort (C.Type t'),subst,metasenv
+ (* TASSI: CONSTRAINT *)
+ | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
+ | C.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) ->
let _,subst',metasenv' =
type_of_aux subst metasenv context ty in
in
(try
let subst''',metasenv''' =
- Un.fo_unif_subst subst'' context metasenv'' inferredty ty
+ fo_unif_subst subst'' context metasenv'' inferredty ty
in
ty,subst''',metasenv'''
with
- _ -> raise (NotRefinable "Cast"))
+ _ -> raise (RefineFailure "Cast"))
| C.Prod (name,s,t) ->
let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
let sort2,subst'',metasenv'' =
type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
in
- sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
- subst'',metasenv''
+ sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
| C.Lambda (n,s,t) ->
let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
+ (match CicReduction.whd ~subst:subst' context sort1 with
+ C.Meta _
+ | C.Sort _ -> ()
+ | _ ->
+ raise (RefineFailure (sprintf
+ "Not well-typed lambda-abstraction: the source %s should be a type;
+ instead it is a term of type %s" (CicPp.ppterm s)
+ (CicPp.ppterm sort1)))
+ ) ;
let type2,subst'',metasenv'' =
type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
in
- let sort2,subst''',metasenv''' =
- type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
- in
- (* only to check if the product is well-typed *)
- let _ =
- sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
- in
- C.Prod (n,s,type2),subst''',metasenv'''
+ C.Prod (n,s,type2),subst'',metasenv''
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
let ty,subst',metasenv' = type_of_aux subst metasenv context s 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
) tl ([],subst',metasenv')
in
eat_prods subst'' metasenv'' context hetype tlbody_and_type
- | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
+ | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
- incr fdebug ;
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
let cty =
CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
in
- decr fdebug ;
cty,subst',metasenv'
| C.MutInd (uri,i,exp_named_subst) ->
- incr fdebug ;
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
let cty =
CicSubstitution.subst_vars exp_named_subst
(type_of_mutual_inductive_defs uri i)
in
- decr fdebug ;
cty,subst',metasenv'
| C.MutConstruct (uri,i,j,exp_named_subst) ->
let subst',metasenv' =
List.nth l i , expl_params, parsno
| _ ->
raise
- (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
+ (RefineFailure
+ ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
let rec count_prod t =
- match CicMetaSubst.whd subst context t with
+ match CicReduction.whd ~subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0 in
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)
let _, subst, metasenv =
type_of_aux subst metasenv context expected_type
in
- let actual_type = CicMetaSubst.whd subst context actual_type in
+ let actual_type = CicReduction.whd ~subst context actual_type in
let subst,metasenv =
- Un.fo_unif_subst subst context metasenv expected_type actual_type
+ fo_unif_subst subst context metasenv expected_type actual_type
in
(* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
let (_,outtypeinstances,subst,metasenv) =
The easy case is when the outype is specified, that amount
to a trivial check. Otherwise, we should guess a type from
its instances *)
+
(* easy case *)
let _, subst, metasenv =
type_of_aux subst metasenv context
type_of_aux subst metasenv context appl
in
*)
- CicMetaSubst.whd subst context appl
+ (* DEBUG
+ let prova1 = CicMetaSubst.whd subst context appl in
+ let prova2 = CicReduction.whd ~subst context appl in
+ if not (prova1 = prova2) then
+ begin
+ prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
+ prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
+ end;
+ *)
+ (* CicMetaSubst.whd subst context appl *)
+ CicReduction.whd ~subst context appl
in
- Un.fo_unif_subst subst context metasenv instance instance')
+ fo_unif_subst subst context metasenv instance instance')
(subst,metasenv) outtypeinstances in
- CicMetaSubst.whd subst
+ CicReduction.whd ~subst
context (C.Appl(outtype::right_args@[term])),subst,metasenv
| C.Fix (i,fl) ->
let subst,metasenv,types =
let ty_of_bo,subst,metasenv =
type_of_aux subst metasenv context' bo
in
- Un.fo_unif_subst subst context' metasenv
- ty_of_bo (CicMetaSubst.lift subst len ty)
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty)
) (subst,metasenv) fl in
let (_,_,ty,_) = List.nth fl i in
ty,subst,metasenv
let ty_of_bo,subst,metasenv =
type_of_aux subst metasenv context' bo
in
- Un.fo_unif_subst subst context' metasenv
- ty_of_bo (CicMetaSubst.lift subst len ty)
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty)
) (subst,metasenv) fl in
let (_,ty,_) = List.nth fl i in
C.Def ((S.lift_meta l (S.lift i t)),
Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
in
- aux 1 canonical_context
+ aux 1 canonical_context
in
+ try
List.fold_left2
(fun (subst,metasenv) t ct ->
match (t,ct) with
subst,metasenv
| Some t,Some (_,C.Def (ct,_)) ->
(try
- CicUnification.fo_unif_subst subst context metasenv t ct
- with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct))))
+ fo_unif_subst subst context metasenv t ct
+ with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
| Some t,Some (_,C.Decl ct) ->
let inferredty,subst',metasenv' =
type_of_aux subst metasenv context t
in
(try
- CicUnification.fo_unif_subst
+ fo_unif_subst
subst' context metasenv' inferredty ct
- with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct))))
+ with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
| None, Some _ ->
- raise (NotRefinable (sprintf
+ raise (RefineFailure (sprintf
"Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
(CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
(CicMetaSubst.ppcontext subst canonical_context)))
) (subst,metasenv) l lifted_canonical_context
+ with
+ Invalid_argument _ ->
+ raise
+ (RefineFailure
+ (sprintf
+ "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
+ (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+ (CicMetaSubst.ppcontext subst canonical_context)))
and check_exp_named_subst metasubst metasenv context =
let rec check_exp_named_subst_aux metasubst metasenv substs =
| ((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
- (NotRefinable
+ (RefineFailure
"A variable with a body can not be explicit substituted")
| Cic.Variable (_,None,_,_) -> ()
- | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+ | _ ->
+ 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'' =
- CicUnification.fo_unif_subst
- metasubst' context metasenv' typeoft typeofvar
- in
- check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
- with _ ->
- raise (NotRefinable "Wrong Explicit Named Substitution")
+ let metasubst'',metasenv'' =
+ try
+ fo_unif_subst metasubst' context metasenv' typeoft typeofvar
+ 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 []
and sort_of_prod subst metasenv context (name,s) (t1, t2) =
let module C = Cic in
- let t1'' = CicMetaSubst.whd subst context t1 in
- let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
+ let context_for_t2 = (Some (name,C.Decl s))::context in
+ let t1'' = CicReduction.whd ~subst context t1 in
+ let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
- C.Sort s2
- | (C.Sort s1, C.Sort s2) ->
- (*CSC manca la gestione degli universi!!! *)
- C.Sort C.Type
- | (C.Meta _,_) | (_,C.Meta _) ->
+ C.Sort s2,subst,metasenv
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+ let t' = CicUniv.fresh() in
+ if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
+ assert false ; (* not possible, error in CicUniv *)
+ C.Sort (C.Type t'),subst,metasenv
+ | (C.Sort _,C.Sort (C.Type t1)) ->
+ (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+ C.Sort (C.Type t1),subst,metasenv
+ | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
+ | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
(* TODO how can we force the meta to become a sort? If we don't we
* brake the invariant that refine produce only well typed terms *)
(* TODO if we check the non meta term and if it is a sort then we are
* 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 *)
- (C.Sort C.Type)
-(* t2'' *)
+ let (metasenv,idx) =
+ CicMkImplicit.mk_implicit_sort metasenv subst in
+ let (subst, metasenv) =
+ fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
+ in
+ t2'',subst,metasenv
| (_,_) ->
- raise (NotRefinable (sprintf
- "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
+ raise (RefineFailure (sprintf
+ "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
(CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
(CicPp.ppterm t2'')))
and eat_prods subst metasenv context hetype tlbody_and_type =
+ let rec mk_prod metasenv context =
+ function
+ [] ->
+ 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 subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let meta = Cic.Meta (idx,irl) in
+ let name =
+ (* The name must be fresh for context. *)
+ (* Nevertheless, argty is well-typed only in context. *)
+ (* Thus I generate a name (name_hint) in context and *)
+ (* then I generate a name --- using the hint name_hint *)
+ (* --- that is fresh in (context'@context). *)
+ let name_hint =
+ (* Cic.Name "pippo" *)
+ 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
+ (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+ FreshNamesGenerator.mk_fresh_name
+ [] context name_hint (Cic.Sort Cic.Prop)
+ in
+ let metasenv,target =
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+ in
+ metasenv,Cic.Prod (name,meta,target)
+ in
+ let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+ let (subst, metasenv) =
+ fo_unif_subst subst context metasenv hetype hetype'
+ in
+ let rec eat_prods metasenv subst context hetype =
+ function
+ [] -> metasenv,subst,hetype
+ | (hete, hety)::tl ->
+ (match hetype with
+ Cic.Prod (n,s,t) ->
+ let subst,metasenv =
+ fo_unif_subst subst context metasenv hety s
+(*
+ try
+ fo_unif_subst subst context metasenv hety s
+ with _ ->
+ prerr_endline("senza subst fallisce");
+ let hety = CicMetaSubst.apply_subst subst hety in
+ let s = CicMetaSubst.apply_subst subst s in
+ prerr_endline ("unifico = " ^(CicPp.ppterm hety));
+ prerr_endline ("con = " ^(CicPp.ppterm s));
+ fo_unif_subst subst context metasenv hety s *)
+ in
+ (* DEBUG
+ let t1 = CicMetaSubst.subst subst hete t in
+ let t2 = CicSubstitution.subst hete t in
+ prerr_endline ("con subst = " ^(CicPp.ppterm t1));
+ prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
+ prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
+ (CicMetaSubst.ppmetasenv metasenv subst));
+ prerr_endline("++++++++++subst prima di eat_prods:\n" ^
+ (CicMetaSubst.ppsubst subst));
+ *)
+ eat_prods metasenv subst context
+ (* (CicMetaSubst.subst subst hete t) tl *)
+ (CicSubstitution.subst hete t) tl
+ | _ -> assert false
+ )
+ in
+ let metasenv,subst,t =
+ eat_prods metasenv subst context hetype' tlbody_and_type
+ in
+ t,subst,metasenv
+(*
let rec aux context' args (resty,subst,metasenv) =
function
[] -> resty,subst,metasenv
| Some t -> Some (CicMetaSubst.lift subst 1 t)
) args in
let argty' = CicMetaSubst.lift subst (List.length args) argty in
- let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in
+ let name =
+ (* The name must be fresh for (context'@context). *)
+ (* Nevertheless, argty is well-typed only in context. *)
+ (* Thus I generate a name (name_hint) in context and *)
+ (* 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)
+ (CicMetaSubst.apply_subst_context subst context)
+ Cic.Anonymous
+ (CicMetaSubst.apply_subst subst argty)
+ in
+ (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+ FreshNamesGenerator.mk_fresh_name
+ [] (context'@context) name_hint (Cic.Sort Cic.Prop)
+ in
+ let context'' = Some (name, Cic.Decl argty') :: context' in
let (metasenv, idx) =
- CicMkImplicit.mk_implicit metasenv (context'' @ context) in
+ CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
let irl =
(Some (Cic.Rel 1))::args' @
(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
context)
in
let newmeta = Cic.Meta (idx, irl) in
- let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
+ let prod = Cic.Prod (name, argty, newmeta) in
let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
let (subst, metasenv) =
- CicUnification.fo_unif_subst subst context metasenv resty prod
+ fo_unif_subst subst context metasenv resty prod
in
aux context'' (Some arg :: args)
(CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
in
aux [] [] (hetype,subst,metasenv) tlbody_and_type
-
- in
+*)
+ in
let ty,subst',metasenv' =
type_of_aux [] metasenv context t
in
- (CicMetaSubst.apply_subst subst' t,
- CicMetaSubst.apply_subst subst' ty,
- CicMetaSubst.apply_subst_metasenv subst' metasenv')
+ let substituted_t = CicMetaSubst.apply_subst subst' t in
+ let substituted_ty = CicMetaSubst.apply_subst subst' ty in
+(* Andrea: ho rimesso qui l'applicazione della subst al
+metasenv dopo che ho droppato l'invariante che il metsaenv
+e' sempre istanziato *)
+ let substituted_metasenv =
+ CicMetaSubst.apply_subst_metasenv subst' metasenv' in
+ (* metasenv' *)
+(* substituted_t,substituted_ty,substituted_metasenv *)
+(* ANDREA: spostare tutta questa robaccia da un altra parte *)
+ let cleaned_t =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+ let cleaned_ty =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+ let cleaned_metasenv =
+ List.map
+ (function (n,context,ty) ->
+ let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
+ let context' =
+ List.map
+ (function
+ None -> None
+ | Some (n, Cic.Decl t) ->
+ Some (n,
+ Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
+ | Some (n, Cic.Def (bo,ty)) ->
+ let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
+ let ty' =
+ match ty with
+ None -> None
+ | Some ty ->
+ Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ in
+ Some (n, Cic.Def (bo',ty'))
+ ) context
+ in
+ (n,context',ty')
+ ) substituted_metasenv
+ in
+ (cleaned_t,cleaned_ty,cleaned_metasenv)
;;
-(* DEBUGGING ONLY *)
+
+
+(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
try
- let (t,ty,m) = type_of_aux' metasenv context term in
- debug_print
- ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
-(*
+ let (t,ty,m) =
+ type_of_aux' metasenv context term in
+ debug_print
+ ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
debug_print
- ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
-*)
+ ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
(t,ty,m)
with
- | CicUnification.AssertFailure msg as e ->
- debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
- debug_print msg;
+ | RefineFailure msg as e ->
+ debug_print ("@@@ REFINE FAILED: " ^ msg);
raise e
- | CicUnification.UnificationFailure msg as e ->
- debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
- debug_print msg;
+ | Uncertain msg as e ->
+ debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
raise e
- | e ->
- debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
- raise e
-;;
-
+;; *)
projects / helm.git / blobdiff