From 04ca589d65bcef6bd46cf4d277a748a12e09234b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 27 Jan 2004 17:30:09 +0000 Subject: [PATCH] - occur check test anticipated to the delift phase - uses CicUtil.lookup_meta --- helm/ocaml/cic_unification/cicMetaSubst.ml | 91 +++++++++++--------- helm/ocaml/cic_unification/cicMetaSubst.mli | 12 +-- helm/ocaml/cic_unification/cicRefine.ml | 28 +++--- helm/ocaml/cic_unification/cicRefine.mli | 1 - helm/ocaml/cic_unification/cicUnification.ml | 11 ++- 5 files changed, 75 insertions(+), 68 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index f8a73f2f5..a3b27c3e7 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -3,7 +3,8 @@ open Printf exception AssertFailure of string exception MetaSubstFailure of string -exception RelToHiddenHypothesis + +exception RelToHiddenHypothesis (* TODO remove this exception *) let debug_print = prerr_endline @@ -16,17 +17,19 @@ let ppsubst subst = subst) (**** DELIFT ****) - -(* the delift function takes in input an ordered list of optional terms *) -(* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with *) -(* rel(k). Typically, the list of optional terms is the explicit substitution *) -(* that is applied to a metavariable occurrence and the result of the delift *) -(* function is a term the implicit variable can be substituted with to make *) -(* the term [t] unifiable with the metavariable occurrence. *) -(* In general, the problem is undecidable if we consider equivalence in place *) -(* of alpha convertibility. Our implementation, though, is even weaker than *) -(* alpha convertibility, since it replace the term [tk] if and only if [tk] *) -(* is a Rel (missing all the other cases). Does this matter in practice? *) +(* the delift function takes in input a metavariable index, an ordered list of + * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some + * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit + * substitution that is applied to a metavariable occurrence and the result of + * the delift function is a term the implicit variable can be substituted with + * to make the term [t] unifiable with the metavariable occurrence. In general, + * the problem is undecidable if we consider equivalence in place of alpha + * convertibility. Our implementation, though, is even weaker than alpha + * convertibility, since it replace the term [tk] if and only if [tk] is a Rel + * (missing all the other cases). Does this matter in practice? + * The metavariable index is the index of the metavariable that must not occur + * in the term (for occur check). + *) exception NotInTheList;; @@ -60,7 +63,7 @@ let restrict to_be_restricted = ;; (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *) -let delift context metasenv l t = +let delift n subst context metasenv l t = let module S = CicSubstitution in let to_be_restricted = ref [] in let rec deliftaux k = @@ -96,21 +99,30 @@ let delift context metasenv l t = in C.Var (uri,exp_named_subst') | C.Meta (i, l1) as t -> - let rec deliftl j = - function - [] -> [] - | None::tl -> None::(deliftl (j+1) tl) - | (Some t)::tl -> - let l1' = (deliftl (j+1) tl) in - try - Some (deliftaux k t)::l1' - with - RelToHiddenHypothesis - | NotInTheList -> - to_be_restricted := (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l') + if i = n then + raise (MetaSubstFailure (sprintf + "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" + i (CicPp.ppterm t))) + else + (try + deliftaux k (S.lift_meta l (List.assoc i subst)) + with Not_found -> + let rec deliftl j = + function + [] -> [] + | None::tl -> None::(deliftl (j+1) tl) + | (Some t)::tl -> + let l1' = (deliftl (j+1) tl) in + try + Some (deliftaux k t)::l1' + with + RelToHiddenHypothesis + | NotInTheList + | MetaSubstFailure _ -> + to_be_restricted := (i,j)::!to_be_restricted ; None::l1' + in + let l' = deliftl 1 l1 in + C.Meta(i,l')) | C.Sort _ as t -> t | C.Implicit as t -> t | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) @@ -201,15 +213,12 @@ let rec unwind metasenv subst unwinded t = let t = List.assoc i subst in let t',metasenv' = um_aux metasenv t in let _,metasenv'' = - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=i) metasenv - in - delift canonical_context metasenv' l t' + let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in + delift i subst canonical_context metasenv' l t' in unwinded := (i,t')::!unwinded ; S.lift_meta l t', metasenv' - with - Not_found -> + with Not_found -> (* not constrained variable, i.e. free in subst*) let l',metasenv' = List.fold_right @@ -459,9 +468,7 @@ let ppmetasenv ?(sep = "\n") subst metasenv = let unwind_subst metasenv subst = List.fold_left (fun (unwinded,metasenv) (i,_) -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=i) metasenv - in + let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in let identity_relocation_list = CicMkImplicit.identity_relocation_list_for_metavariable canonical_context in @@ -474,7 +481,9 @@ let unwind_subst metasenv subst = (* From now on we recreate a kernel abstraction where substitutions are part of * the calculus *) -let whd subst context term = +let whd metasenv subst context term = + (* TODO unwind's result is thrown away :-( *) + let (subst, _) = unwind_subst metasenv subst in let term = apply_subst subst term in let context = apply_subst_context subst context in try @@ -483,12 +492,16 @@ let whd subst context term = raise (MetaSubstFailure ("Weak head reduction failure: " ^ Printexc.to_string e)) -let are_convertible subst context t1 t2 = +let are_convertible metasenv subst context t1 t2 = + (* TODO unwind's result is thrown away :-( *) + let (subst, _) = unwind_subst metasenv subst in let context = apply_subst_context subst context in let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in CicReduction.are_convertible context t1 t2 let type_of_aux' metasenv subst context term = + (* TODO unwind's result is thrown away :-( *) + let (subst, _) = unwind_subst metasenv subst in let term = apply_subst subst term in let context = apply_subst_context subst context in let metasenv = diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 5f29b9bdf..986a595ce 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -26,14 +26,14 @@ exception AssertFailure of string exception MetaSubstFailure of string -val delift : - Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> - Cic.term * Cic.metasenv - (* The entry (i,t) in a substitution means that *) (* (META i) have been instantiated with t. *) type substitution = (int * Cic.term) list +val delift : + int -> substitution -> Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> + Cic.term * Cic.metasenv + (* unwind_subst metasenv subst *) (* unwinds [subst] w.r.t. itself. *) (* It can restrict some metavariable in the [metasenv] *) @@ -69,10 +69,10 @@ val ppsubst: substitution -> string * From now on we recreate a kernel abstraction where substitutions are part of * the calculus *) -val whd: substitution -> Cic.context -> Cic.term -> Cic.term +val whd: Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term val are_convertible: - substitution -> Cic.context -> Cic.term -> Cic.term -> + Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term -> bool val type_of_aux': diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index e3086c801..54fde9a45 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -35,7 +35,6 @@ exception WrongUriToMutualInductiveDefinitions of string;; exception RelToHiddenHypothesis;; exception MetasenvInconsistency;; exception MutCaseFixAndCofixRefineNotImplemented;; -exception FreeMetaFound of int;; exception WrongArgumentNumber;; let fdebug = ref 0;; @@ -111,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 subst context expectedtype with + match R.whd metasenv subst context expectedtype with C.MutInd (_,_,_) -> (n,context,actualtype, [term]), subst, metasenv | C.Appl (C.MutInd (_,_,_)::tl) -> @@ -120,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 subst context actualtype with + (match R.whd metasenv subst context actualtype with C.Prod (name',so',de') -> let subst, metasenv = Un.fo_unif_subst subst context metasenv so so' in @@ -162,12 +161,7 @@ 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 @@ -267,7 +261,7 @@ and type_of_aux' metasenv context t = raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in let rec count_prod t = - match CicMetaSubst.whd subst context t with + match CicMetaSubst.whd metasenv subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in let no_args = count_prod arity in @@ -292,7 +286,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 subst context actual_type in + let actual_type = CicMetaSubst.whd metasenv subst context actual_type in let subst,metasenv = Un.fo_unif_subst subst context metasenv expected_type actual_type in @@ -342,11 +336,11 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context appl in *) - CicMetaSubst.whd subst context appl + CicMetaSubst.whd metasenv subst context appl in Un.fo_unif_subst subst context metasenv instance instance') (subst,metasenv) outtypeinstances in - CicMetaSubst.whd subst + CicMetaSubst.whd metasenv subst context (C.Appl(outtype::right_args@[term])),subst,metasenv | C.Fix _ | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented @@ -427,8 +421,10 @@ and type_of_aux' metasenv context t = 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.whd metasenv subst' context t1' in + let t2'' = + CicMetaSubst.whd metasenv 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!!! *) @@ -452,7 +448,7 @@ and type_of_aux' metasenv context t = function [] -> hetype,subst,metasenv | (hete, hety)::tl -> - (match (CicMetaSubst.whd subst context hetype) with + (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 diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index 2d4c0214a..12a4bb98b 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -29,7 +29,6 @@ exception WrongUriToConstant of string exception WrongUriToVariable of string exception WrongUriToMutualInductiveDefinitions of string exception MutCaseFixAndCofixRefineNotImplemented;; -exception FreeMetaFound of int;; (* type_of_aux' metasenv context term *) (* refines [term] and returns the refined form of [term], *) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index e0ec5cb44..704eecb46 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -66,7 +66,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = (* First possibility: restriction *) (* Second possibility: unification *) (* Third possibility: convertibility *) - R.are_convertible subst context t1' t2' + R.are_convertible metasenv subst context t1' t2' ) true ln lm in if ok then @@ -85,11 +85,10 @@ let rec fo_unif_subst subst context metasenv t1 t2 = let lifted_oldt = S.lift_meta l oldt in fo_unif_subst subst context metasenv lifted_oldt t with Not_found -> - let t',metasenv' = CicMetaSubst.delift context metasenv l t in + let t',metasenv' = CicMetaSubst.delift n subst context metasenv l t in (n, t')::subst, metasenv' in - let (_,_,meta_type) = - List.find (function (m,_,_) -> m=n) metasenv' in + let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in let tyt = type_of_aux' metasenv' subst' context t in fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) @@ -165,14 +164,14 @@ let rec fo_unif_subst subst context metasenv t1 t2 = | (C.MutConstruct _, _) | (_, C.MutConstruct _) | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) | (_, C.CoFix _) -> - if R.are_convertible subst context t1 t2 then + if R.are_convertible metasenv subst context t1 t2 then subst, metasenv else raise (UnificationFailure (sprintf "Can't unify %s with %s because they are not convertible" (CicPp.ppterm t1) (CicPp.ppterm t2))) | (_,_) -> - if R.are_convertible subst context t1 t2 then + if R.are_convertible metasenv subst context t1 t2 then subst, metasenv else raise (UnificationFailure (sprintf -- 2.39.2