X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=b3525d3182bcec3737d02c2883cd7402d1acf730;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=ba79ce92232f4cce5866786b6d6b8ea4e4b3133e;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index ba79ce922..b3525d318 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -23,27 +23,27 @@ * http://cs.unibo.it/helm/. *) -exception Impossible of int;; -exception NotRefinable of string;; +open Printf + +exception RefineFailure of string;; exception Uncertain of string;; -exception WrongUriToConstant of string;; -exception WrongUriToVariable of string;; -exception WrongUriToMutualInductiveDefinitions of string;; -exception RelToHiddenHypothesis;; -exception MetasenvInconsistency;; -exception MutCaseFixAndCofixRefineNotImplemented;; -exception FreeMetaFound of int;; +exception AssertFailure of string;; -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*) +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 (AssertFailure "split: list too short") ;; let rec type_of_constant uri = @@ -53,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 @@ -61,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 @@ -71,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 @@ -82,15 +90,52 @@ 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 *) + +(* the check_branch function checks if a branch of a case is refinable. + It returns a pair (outype_instance,args), a subst and a metasenv. + outype_instance is the expected result of applying the case outtype + to args. + The problem is that outype is in general unknown, and we should + try to synthesize it from the above information, that is in general + a second order unification problem. *) + +and check_branch n context metasenv subst left_args_no actualtype term expectedtype = + let module C = Cic in + let module R = CicMetaSubst in + match R.whd subst context expectedtype with + C.MutInd (_,_,_) -> + (n,context,actualtype, [term]), subst, metasenv + | C.Appl (C.MutInd (_,_,_)::tl) -> + let (_,arguments) = split tl left_args_no in + (n,context,actualtype, arguments@[term]), subst, metasenv + | 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 + C.Prod (name',so',de') -> + let subst, metasenv = + 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]) + | t -> C.Appl [t ; C.Rel 1]) in + (* 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 (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 module C = Cic in let module S = CicSubstitution in let module U = UriManager in - let module Un = CicUnification in function C.Rel n -> (try @@ -98,49 +143,47 @@ and type_of_aux' metasenv context t = Some (_,C.Decl t) -> S.lift n t,subst,metasenv | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv | Some (_,C.Def (bo,None)) -> - prerr_endline "##### DA INVESTIGARE E CAPIRE" ; 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) = - try - List.find (function (m,_,_) -> n = m) metasenv - with - Not_found -> raise (FreeMetaFound n) - in + let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let subst',metasenv' = - check_metasenv_consistency subst metasenv context canonical_context l + 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) + 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 let inferredty,subst'',metasenv'' = - type_of_aux subst' metasenv' context ty + type_of_aux subst' metasenv' context te 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'' = @@ -149,17 +192,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 CicMetaSubst.whd 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 @@ -181,25 +226,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' = @@ -209,14 +250,149 @@ and type_of_aux' metasenv context t = (type_of_mutual_inductive_constr uri i j) in cty,subst',metasenv' - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented + | C.MutCase (uri, i, outtype, term, pl) -> + (* first, get the inductive type (and noparams) in the environment *) + let (_,b,arity,constructors), expl_params, no_left_params = + match CicEnvironment.get_cooked_obj ~trust:true uri with + C.InductiveDefinition (l,expl_params,parsno) -> + List.nth l i , expl_params, parsno + | _ -> + raise + (RefineFailure + ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in + let rec count_prod t = + match CicMetaSubst.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 + 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 + let metasenv,exp_named_subst = + CicMkImplicit.fresh_subst metasenv context expl_params in + let expected_type = + if no_args = 0 then + C.MutInd (uri,i,exp_named_subst) + else + C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args)) + in + (* check consistency with the actual type of term *) + let actual_type,subst,metasenv = + type_of_aux subst metasenv context term in + let _, subst, metasenv = + type_of_aux subst metasenv context expected_type + in + let actual_type = CicMetaSubst.whd subst context actual_type in + let subst,metasenv = + 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) = + List.fold_left + (fun (j,outtypeinstances,subst,metasenv) p -> + let constructor = + if left_args = [] then + (C.MutConstruct (uri,i,j,exp_named_subst)) + else + (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args)) + in + let actual_type,subst,metasenv = + type_of_aux subst metasenv context p in + let expected_type, subst, metasenv = + type_of_aux subst metasenv context constructor in + let outtypeinstance,subst,metasenv = + check_branch + 0 context metasenv subst + no_left_params actual_type constructor expected_type in + (j+1,outtypeinstance::outtypeinstances,subst,metasenv)) + (1,[],subst,metasenv) pl in + (* we are left to check that the outype matches his instances. + 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 + (C.Appl ((outtype :: right_args) @ [term])) + in + let (subst,metasenv) = + List.fold_left + (fun (subst,metasenv) (constructor_args_no,context,instance,args) -> + let instance' = + let appl = + let outtype' = + CicSubstitution.lift constructor_args_no outtype + in + C.Appl (outtype'::args) + in +(* + (* if appl is not well typed then the type_of below solves the + * problem *) + let (_, subst, metasenv) = + type_of_aux subst metasenv context appl + in +*) + CicMetaSubst.whd subst context appl + in + fo_unif_subst subst context metasenv instance instance') + (subst,metasenv) outtypeinstances in + CicMetaSubst.whd subst + context (C.Appl(outtype::right_args@[term])),subst,metasenv + | C.Fix (i,fl) -> + let subst,metasenv,types = + List.fold_left + (fun (subst,metasenv,types) (n,_,ty,_) -> + let _,subst',metasenv' = type_of_aux subst metasenv context ty in + subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types + ) (subst,metasenv,[]) fl + in + let len = List.length types in + let context' = types@context in + let subst,metasenv = + List.fold_left + (fun (subst,metasenv) (name,x,ty,bo) -> + let ty_of_bo,subst,metasenv = + type_of_aux subst metasenv context' bo + in + fo_unif_subst subst context' metasenv + ty_of_bo (CicMetaSubst.lift subst len ty) + ) (subst,metasenv) fl in + let (_,_,ty,_) = List.nth fl i in + ty,subst,metasenv + | C.CoFix (i,fl) -> + let subst,metasenv,types = + List.fold_left + (fun (subst,metasenv,types) (n,ty,_) -> + let _,subst',metasenv' = type_of_aux subst metasenv context ty in + subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types + ) (subst,metasenv,[]) fl + in + let len = List.length types in + let context' = types@context in + let subst,metasenv = + List.fold_left + (fun (subst,metasenv) (name,ty,bo) -> + let ty_of_bo,subst,metasenv = + type_of_aux subst metasenv context' bo + in + fo_unif_subst subst context' metasenv + ty_of_bo (CicMetaSubst.lift subst len ty) + ) (subst,metasenv) fl in + + let (_,ty,_) = List.nth fl i in + ty,subst,metasenv (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) - and check_metasenv_consistency subst metasenv context canonical_context l = + and check_metasenv_consistency + metano subst metasenv context canonical_context l + = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in @@ -229,27 +405,45 @@ and type_of_aux' metasenv context t = | (Some (n,C.Def (t,None)))::tl -> (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (_,C.Def (_,Some _)))::_ -> assert false + | (Some (n,C.Def (t,Some ty)))::tl -> + (Some (n, + 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 in + try List.fold_left2 (fun (subst,metasenv) t ct -> match (t,ct) with - _,None -> subst,metasenv + _,None -> + subst,metasenv | Some t,Some (_,C.Def (ct,_)) -> (try - CicUnification.fo_unif_subst subst context metasenv t ct - with _ -> raise MetasenvInconsistency) + 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 subst context metasenv inferredty ct - with _ -> raise MetasenvInconsistency) - | _, _ -> raise MetasenvInconsistency + fo_unif_subst + subst' context metasenv' inferredty 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 (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 = @@ -261,108 +455,229 @@ and type_of_aux' metasenv context t = (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 + 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") + raise (RefineFailure "Wrong Explicit Named Substitution") in check_exp_named_subst_aux metasubst metasenv [] and sort_of_prod subst metasenv context (name,s) (t1, t2) = let module C = Cic in - (* ti could be a metavariable in the domain of the substitution *) - let subst',metasenv' = CicUnification.unwind_subst metasenv subst in - let t1' = CicUnification.apply_subst subst' t1 in - let t2' = CicUnification.apply_subst subst' t2 in - let t1'' = CicReduction.whd context t1' in - let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in + let context_for_t2 = (Some (name,C.Decl s))::context in + let t1'' = CicMetaSubst.whd subst context t1 in + let t2'' = CicMetaSubst.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 from 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.Meta _,_) - | (_,C.Meta _) -> - raise - (Uncertain - ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^ - CicPp.ppterm t2'')) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) + 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 *) + let (metasenv,idx) = + CicMkImplicit.mk_implicit_sort metasenv in + let (subst, metasenv) = + fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' + in + t2'',subst,metasenv | (_,_) -> - raise - (NotRefinable - ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2'')) + 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 = + and eat_prods subst metasenv context hetype tlbody_and_type = + let rec mk_prod metasenv context = function - [] -> hetype,subst,metasenv - | (hete, hety)::tl -> - (match (CicReduction.whd context hetype) with - Cic.Prod (n,s,t) -> - let subst',metasenv' = - try - CicUnification.fo_unif_subst subst context metasenv s hety - with _ -> - raise (NotRefinable "Appl: wrong parameter-type") - in - CicReduction.fdebug := -1 ; - eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl - | Cic.Meta _ as t -> - raise - (Uncertain - ("Prod expected, " ^ CicPp.ppterm t ^ " found")) - | _ -> raise (NotRefinable "Appl: wrong Prod-type") - ) + [] -> + let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv 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 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 = + 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 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 + in + eat_prods metasenv subst context + (CicMetaSubst.subst 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 + | (arg,argty)::tl -> + let args' = + List.map + (function + None -> assert false + | Some t -> Some (CicMetaSubst.lift subst 1 t) + ) args in + let argty' = CicMetaSubst.lift subst (List.length args) argty 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_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 (name, argty, newmeta) in + let (_, subst, metasenv) = type_of_aux subst metasenv context prod in + let (subst, metasenv) = + 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 let ty,subst',metasenv' = type_of_aux [] metasenv context t in - let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in - (* we get rid of the metavariables that have been instantiated *) - let metasenv''' = - List.filter - (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'')) - metasenv'' + 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 - CicUnification.apply_subst subst'' t, - CicUnification.apply_subst subst'' ty, - subst'', metasenv''' + 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 *) let type_of_aux' metasenv context term = try - let (t,ty,s,m) = - type_of_aux' metasenv context term - in - List.iter - (function (i,t) -> - prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ; - List.iter - (function (i,_,t) -> - prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ; - prerr_endline - ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ; - (t,ty,s,m) + 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); +*) + (t,ty,m) with - e -> - List.iter - (function (i,_,t) -> - prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) - metasenv ; - prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; - raise e + | RefineFailure msg as e -> + debug_print ("@@@ REFINE FAILED: " ^ msg); + raise e + | Uncertain msg as e -> + debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); + raise e ;;