X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=7b3e4179c47b77f65d2939d5fead0e2bea3914f9;hb=a864255e782859e2b3b7da08297f5d3fe2ee710d;hp=b64d8f4bb8b2236793b5be72d911e038e946b227;hpb=f42507bf45ea6b50adbae7ba8117905cc9631101;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index b64d8f4bb..7b3e4179c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -26,36 +26,24 @@ 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 = @@ -65,7 +53,9 @@ 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 @@ -73,7 +63,10 @@ and type_of_variable uri = 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 @@ -83,7 +76,10 @@ and type_of_mutual_inductive_defs uri i = 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 @@ -94,7 +90,10 @@ and type_of_mutual_inductive_constr uri i j = 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 *) @@ -108,9 +107,9 @@ and type_of_mutual_inductive_constr uri i j = 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) -> @@ -119,10 +118,10 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | 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]) @@ -130,16 +129,16 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (* 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 @@ -147,29 +146,42 @@ and type_of_aux' metasenv context t = | 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 @@ -178,11 +190,11 @@ and type_of_aux' metasenv context t = 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'' = @@ -191,17 +203,19 @@ and type_of_aux' metasenv context t = 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 _,subst'''',metasenv'''' = - 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 @@ -211,7 +225,7 @@ and type_of_aux' metasenv context t = (* 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 @@ -223,25 +237,21 @@ and type_of_aux' metasenv context t = ) 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' = @@ -259,21 +269,22 @@ and type_of_aux' metasenv context t = 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) @@ -286,9 +297,9 @@ and type_of_aux' metasenv context t = 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) = @@ -314,6 +325,7 @@ and type_of_aux' metasenv context t = 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 @@ -336,11 +348,21 @@ and type_of_aux' metasenv context t = 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 = @@ -358,8 +380,8 @@ and type_of_aux' metasenv context t = 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 @@ -379,8 +401,8 @@ and type_of_aux' metasenv context t = 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 @@ -409,8 +431,9 @@ and type_of_aux' metasenv context t = 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 @@ -418,22 +441,30 @@ and type_of_aux' metasenv context t = 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 = @@ -442,39 +473,52 @@ and type_of_aux' metasenv context t = | ((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,subst,metasenv - | (C.Sort s1, C.Sort s2) -> - (*CSC manca la gestione degli universi!!! *) - C.Sort C.Type,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 @@ -483,19 +527,99 @@ and type_of_aux' metasenv context t = * 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 metasenv [] in + CicMkImplicit.mk_implicit_sort metasenv subst in let (subst, metasenv) = - CicUnification.fo_unif_subst subst context metasenv - (C.Meta (idx,[])) t2'' + 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 @@ -526,7 +650,7 @@ and type_of_aux' metasenv context t = 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 @@ -536,22 +660,27 @@ and type_of_aux' metasenv context t = 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 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' - 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 = @@ -581,32 +710,26 @@ and type_of_aux' metasenv context t = (n,context',ty') ) substituted_metasenv in - (cleaned_t,cleaned_ty,cleaned_metasenv) - + (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 -;; - +;; *)