From 335186953e826833ed43b33cac98884d3f99a228 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:37:10 +0000 Subject: [PATCH] - removed metasenv argument from kernel proxies invocations - lift_meta over defs with an explicit type implemented - reimplemented eat_prods (open bug: when an application has more than one argument and its type is a meta then the outtype is a Meta whose context is not general enough. To be implemented) --- helm/ocaml/cic_unification/cicRefine.ml | 116 ++++++++++++------------ 1 file changed, 57 insertions(+), 59 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 979c9637e..3fc0dcf5a 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -109,7 +109,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 +118,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 @@ -164,7 +164,7 @@ and type_of_aux' metasenv context t = 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 @@ -260,7 +260,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 +285,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 +335,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 +358,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 +379,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 @@ -402,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 @@ -459,79 +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 metasenv subst' context t1' 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 metasenv subst' ((Some (name,C.Decl s))::context) 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' + C.Meta (idx, irl), subst, metasenv | (_,_) -> 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 = - 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 = + (* 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 + 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 -> @@ -543,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 ;; -- 2.39.2