X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=060d2bd1f767c9767fdd1c6cb99b65d22f8bca9e;hb=aef0ab661736f065a2a41a09df6e79fd4e626cd7;hp=979c9637ede5591125cf64dfa4786d08299a2648;hpb=cf7fbeee5c21b86f70281f42cd09ee699e0c62b7;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 979c9637e..060d2bd1f 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,7 +35,6 @@ exception WrongUriToVariable of string;; exception ListTooShort;; exception WrongUriToMutualInductiveDefinitions of string;; exception RelToHiddenHypothesis;; -exception MetasenvInconsistency;; exception WrongArgumentNumber;; let fdebug = ref 0;; @@ -109,7 +110,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt let module C = Cic in let module R = CicMetaSubst in let module Un = CicUnification in - match R.whd metasenv subst context expectedtype with + match R.whd subst context expectedtype with C.MutInd (_,_,_) -> (n,context,actualtype, [term]), subst, metasenv | C.Appl (C.MutInd (_,_,_)::tl) -> @@ -118,7 +119,7 @@ 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 metasenv 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 @@ -162,9 +163,9 @@ and type_of_aux' metasenv context t = | 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' + CicSubstitution.lift_meta l ty, subst', metasenv' | C.Sort s -> C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) subst,metasenv @@ -187,7 +188,8 @@ and type_of_aux' metasenv context t = 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) + sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2), + subst'',metasenv'' | C.Lambda (n,s,t) -> let sort1,subst',metasenv' = type_of_aux subst metasenv context s in let type2,subst'',metasenv'' = @@ -197,10 +199,10 @@ and type_of_aux' metasenv context t = 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'''' = + 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 @@ -260,7 +262,7 @@ and type_of_aux' metasenv context t = raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in let rec count_prod t = - match CicMetaSubst.whd metasenv subst context t with + match CicMetaSubst.whd subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in let no_args = count_prod arity in @@ -285,7 +287,7 @@ and type_of_aux' metasenv context t = let _, subst, metasenv = type_of_aux subst metasenv context expected_type in - let actual_type = CicMetaSubst.whd metasenv subst context actual_type 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 in @@ -335,11 +337,11 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context appl in *) - CicMetaSubst.whd metasenv subst context appl + CicMetaSubst.whd subst context appl in Un.fo_unif_subst subst context metasenv instance instance') (subst,metasenv) outtypeinstances in - CicMetaSubst.whd metasenv subst + CicMetaSubst.whd subst context (C.Appl(outtype::right_args@[term])),subst,metasenv | C.Fix (i,fl) -> let subst,metasenv,types = @@ -358,9 +360,8 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context' bo in Un.fo_unif_subst subst context' metasenv - ty_of_bo (CicMetaSubst.lift metasenv subst len ty) + 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) -> @@ -380,7 +381,7 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context' bo in Un.fo_unif_subst subst context' metasenv - ty_of_bo (CicMetaSubst.lift metasenv subst len ty) + ty_of_bo (CicMetaSubst.lift subst len ty) ) (subst,metasenv) fl in let (_,ty,_) = List.nth fl i in @@ -389,7 +390,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 @@ -402,7 +405,10 @@ 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 @@ -414,7 +420,7 @@ and type_of_aux' metasenv context t = | Some t,Some (_,C.Def (ct,_)) -> (try CicUnification.fo_unif_subst subst context metasenv t ct - with _ -> raise MetasenvInconsistency) + 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)))) | Some t,Some (_,C.Decl ct) -> let inferredty,subst',metasenv' = type_of_aux subst metasenv context t @@ -422,9 +428,12 @@ and type_of_aux' metasenv context t = (try CicUnification.fo_unif_subst subst' context metasenv' inferredty ct - with _ -> raise MetasenvInconsistency) - | _, _ -> - raise MetasenvInconsistency + 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)))) + | 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 = @@ -458,81 +467,80 @@ and type_of_aux' metasenv context t = 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' = CicMetaSubst.unwind_subst metasenv subst in - let t1' = CicMetaSubst.apply_subst subst' t1 in - let t2' = CicMetaSubst.apply_subst subst' t2 in - let t1'' = CicMetaSubst.whd metasenv subst' context t1' in - let t2'' = - CicMetaSubst.whd metasenv subst' ((Some (name,C.Decl s))::context) t2' - in + let t1'' = CicMetaSubst.whd subst context t1 in + let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) 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' + 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,subst',metasenv' + C.Sort C.Type | (C.Meta _,_) | (_,C.Meta _) -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - C.Meta (idx, irl), subst, metasenv' + (* 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'' *) | (_,_) -> 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 = - function - [] -> hetype,subst,metasenv - | (hete, hety)::tl -> - (match (CicMetaSubst.whd metasenv subst context hetype) with - Cic.Prod (n,s,t) -> - let subst',metasenv' = - CicUnification.fo_unif_subst subst context metasenv s hety - 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") - ) + and eat_prods subst metasenv context hetype tlbody_and_type = + 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 context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in + let (metasenv, idx) = + CicMkImplicit.mk_implicit 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 (_, subst, metasenv) = type_of_aux subst metasenv context prod in + let (subst, metasenv) = + CicUnification.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'' = CicMetaSubst.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'' - in - CicMetaSubst.apply_subst subst'' t, - CicMetaSubst.apply_subst subst'' ty, - subst'', metasenv''' + (CicMetaSubst.apply_subst subst' t, + CicMetaSubst.apply_subst subst' ty, + CicMetaSubst.apply_subst_metasenv subst' metasenv') ;; (* DEBUGGING ONLY *) let type_of_aux' metasenv context term = try - let (t,ty,s,m) = type_of_aux' metasenv context term in + let (t,ty,m) = type_of_aux' metasenv context term in + debug_print + ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); (* - List.iter - (function (i,t) -> - debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ; - List.iter - (function (i,_,t) -> - debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ; -*) debug_print - ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ; - (t,ty,s,m) + ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s); +*) + (t,ty,m) with | CicUnification.AssertFailure msg as e -> debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; @@ -543,12 +551,6 @@ let type_of_aux' metasenv context term = debug_print msg; raise e | e -> -(* - List.iter - (function (i,_,t) -> - debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) - metasenv ; -*) debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; raise e ;;