From e874af2d785b2b383ae8444fdd32bb5344fb914f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 17:01:50 +0000 Subject: [PATCH] - refine's type_of no longer return a substitution --- helm/ocaml/cic_unification/cicMetaSubst.ml | 8 ++++++++ helm/ocaml/cic_unification/cicMetaSubst.mli | 1 + helm/ocaml/cic_unification/cicRefine.ml | 21 +++++++-------------- helm/ocaml/cic_unification/cicRefine.mli | 3 +-- 4 files changed, 17 insertions(+), 16 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index a28b853be..ba8ae7d98 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -475,6 +475,14 @@ let rec apply_subst_context subst context = | None -> None :: context) context [] +let apply_subst_metasenv subst metasenv = + List.map + (fun (n, context, ty) -> + (n, apply_subst_context subst context, apply_subst subst ty)) + (List.filter + (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst)) + metasenv) + let ppterm subst term = CicPp.ppterm (apply_subst subst term) let ppcontext ?(sep = "\n") subst context = diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index fd770215a..730afcd10 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -54,6 +54,7 @@ val apply_subst_reducing : (int * int) option -> substitution -> Cic.term -> Cic.term val apply_subst_context : substitution -> Cic.context -> Cic.context +val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv (** {2 Pretty printers} *) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 3fc0dcf5a..a6506d5ca 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -460,13 +460,8 @@ 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 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.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 than Coq manual!!! *) @@ -519,24 +514,22 @@ and type_of_aux' metasenv context t = (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); (* - debug_print - ("@@@ REFINE SUCCESSFUL (subst):\n" ^ CicMetaSubst.ppsubst s); debug_print ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s); *) - (t,ty,s,m) + (t,ty,m) with | CicUnification.AssertFailure msg as e -> debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index ce97e8ab7..28a34f5ff 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -32,7 +32,6 @@ exception WrongUriToMutualInductiveDefinitions of string (* type_of_aux' metasenv context term *) (* refines [term] and returns the refined form of [term], *) (* its type, the computed substitution and the new metasenv. *) -(* The substitution returned is already unwinded *) val type_of_aux': Cic.metasenv -> Cic.context -> Cic.term -> - Cic.term * Cic.term * CicMetaSubst.substitution * Cic.metasenv + Cic.term * Cic.term * Cic.metasenv -- 2.39.2