X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=3fc0dcf5a4003585b10f17e19240fc0932c04994;hb=2f4e2076f4b53f0c3e277bff67268cb80bfae967;hp=9434f523235931389762cd1f3252f61308f9e69c;hpb=99744ac02b9f208f6668d7efc9b21a8e3818cc39;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 9434f5232..3fc0dcf5a 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +open Printf + exception Impossible of int;; exception NotRefinable of string;; exception Uncertain of string;; @@ -32,8 +34,6 @@ exception ListTooShort;; exception WrongUriToMutualInductiveDefinitions of string;; exception RelToHiddenHypothesis;; exception MetasenvInconsistency;; -exception MutCaseFixAndCofixRefineNotImplemented;; -exception FreeMetaFound of int;; exception WrongArgumentNumber;; let fdebug = ref 0;; @@ -160,16 +160,11 @@ and type_of_aux' metasenv context t = 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 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 @@ -178,7 +173,7 @@ and type_of_aux' metasenv context t = 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''' = @@ -346,8 +341,49 @@ and type_of_aux' metasenv context t = (subst,metasenv) outtypeinstances in CicMetaSubst.whd subst context (C.Appl(outtype::right_args@[term])),subst,metasenv - | C.Fix _ - | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented + | 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 + Un.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 + Un.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 - @@ -365,7 +401,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 @@ -422,82 +461,81 @@ 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 subst' context t1' in - let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) t2' in + let t1' = CicMetaSubst.apply_subst subst t1 in + let t2' = CicMetaSubst.apply_subst subst 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,subst,metasenv | (C.Sort s1, C.Sort s2) -> (*CSC manca la gestione degli universi!!! *) - C.Sort C.Type,subst',metasenv' + C.Sort C.Type,subst,metasenv | (C.Meta _,_) | (_,C.Meta _) -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in + (* 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 in - C.Meta (idx, irl), subst, metasenv' -(* - raise - (Uncertain - ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^ - CicPp.ppterm t2'')) -*) + C.Meta (idx, irl), subst, metasenv | (_,_) -> - raise - (NotRefinable - ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2'')) + raise (NotRefinable (sprintf + "Two types were expected, found %s of type %s and %s of type %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 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 + in + (CicMetaSubst.subst subst arg newmeta, subst, metasenv)) + (hetype, subst, metasenv) tlbody_and_type - and eat_prods subst metasenv context hetype = - function - [] -> hetype,subst,metasenv - | (hete, hety)::tl -> - (match (CicMetaSubst.whd 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") - ) 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''' = + let metasenv'' = List.filter - (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'')) - metasenv'' + (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, + subst', metasenv'' ;; (* DEBUGGING ONLY *) let type_of_aux' metasenv context term = try let (t,ty,s,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) ; + ("@@@ REFINE SUCCESSFUL (subst):\n" ^ CicMetaSubst.ppsubst s); + debug_print + ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s); +*) (t,ty,s,m) with | CicUnification.AssertFailure msg as e -> @@ -509,12 +547,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 ;;