X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=06398da9a5e3dafa1fa3e89545d8e65f3d5d5f38;hb=da11c92be86c24285ef1a4d0ddfe1e074a6b322a;hp=a6506d5cacb057c13c0f7de4813364c813922d68;hpb=e874af2d785b2b383ae8444fdd32bb5344fb914f;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index a6506d5ca..06398da9a 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -25,6 +25,8 @@ open Printf +exception RefineFailure of string;; + exception Impossible of int;; exception NotRefinable of string;; exception Uncertain of string;; @@ -33,23 +35,18 @@ exception WrongUriToVariable of string;; exception ListTooShort;; exception WrongUriToMutualInductiveDefinitions of string;; exception RelToHiddenHypothesis;; -exception MetasenvInconsistency;; 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*) -;; - 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) @@ -121,7 +118,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (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]) @@ -151,24 +148,22 @@ and type_of_aux' metasenv context t = _ -> raise (NotRefinable "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 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) + | C.Implicit _ -> raise (Impossible 21) | C.Cast (te,ty) -> let _,subst',metasenv' = type_of_aux subst metasenv context ty in @@ -177,7 +172,7 @@ 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 @@ -190,17 +185,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 (NotRefinable (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 @@ -224,23 +221,19 @@ and type_of_aux' metasenv context t = eat_prods subst'' metasenv'' context hetype tlbody_and_type | C.Appl _ -> raise (NotRefinable "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' = @@ -287,7 +280,7 @@ and type_of_aux' metasenv context t = in let actual_type = CicMetaSubst.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) = @@ -337,7 +330,7 @@ and type_of_aux' metasenv context t = *) CicMetaSubst.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 context (C.Appl(outtype::right_args@[term])),subst,metasenv @@ -357,7 +350,7 @@ 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 + 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 @@ -378,7 +371,7 @@ 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 + fo_unif_subst subst context' metasenv ty_of_bo (CicMetaSubst.lift subst len ty) ) (subst,metasenv) fl in @@ -388,7 +381,9 @@ and type_of_aux' metasenv context t = (* 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 @@ -415,18 +410,21 @@ 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 MetasenvInconsistency) + fo_unif_subst subst context metasenv t ct + with e -> raise (NotRefinable (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 CicUnification.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 MetasenvInconsistency) - | _, _ -> - raise MetasenvInconsistency + with e -> 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. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + | None, Some _ -> + raise (NotRefinable (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 and check_exp_named_subst metasubst metasenv context = @@ -449,8 +447,7 @@ and type_of_aux' 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 _ -> @@ -460,8 +457,9 @@ and type_of_aux' metasenv context t = and sort_of_prod subst metasenv context (name,s) (t1, t2) = let module C = Cic 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 ((Some (name,C.Decl s))::context) t2 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 than Coq manual!!! *) @@ -469,54 +467,177 @@ and type_of_aux' metasenv context t = | (C.Sort s1, C.Sort s2) -> (*CSC manca la gestione degli universi!!! *) C.Sort C.Type,subst,metasenv - | (C.Meta _,_) | (_,C.Meta _) -> + | (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 metasenv context in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context + 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 - C.Meta (idx, irl), subst, metasenv + t2'',subst,metasenv | (_,_) -> raise (NotRefinable (sprintf - "Two types were expected, found %s of type %s and %s of type %s" + "Two types 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 = - (* TODO to be reviewed *) - List.fold_left - (fun (resty, subst, metasenv) (arg, argty) -> - let context' = Some (Cic.Anonymous, Cic.Decl argty) :: context in - let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context' in + let rec mk_prod metasenv context = + function + [] -> + 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 newmeta = Cic.Meta (idx, irl) in - let prod = Cic.Prod (Cic.Anonymous, 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 + CicMkImplicit.identity_relocation_list_for_metavariable context in - (CicMetaSubst.subst subst arg newmeta, subst, metasenv)) - (hetype, subst, metasenv) tlbody_and_type + 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) = + CicUnification.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) -> + (try + let subst,metasenv = + CicUnification.fo_unif_subst subst context metasenv s hety + in + eat_prods metasenv subst context + (CicMetaSubst.subst subst hete t) tl + with + e -> raise (RefineFailure ("XXX " ^ Printexc.to_string e))) + | _ -> 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 - (* 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 - (CicMetaSubst.apply_subst subst' t, - CicMetaSubst.apply_subst subst' ty, - CicMetaSubst.apply_subst_metasenv 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 *) @@ -535,10 +656,6 @@ let type_of_aux' metasenv context term = debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; debug_print msg; raise e - | CicUnification.UnificationFailure msg as e -> - debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:"; - debug_print msg; - raise e | e -> debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; raise e