From 9945374a5594c068883fa6c775f17b640fcac64d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 Jun 2004 10:59:17 +0000 Subject: [PATCH] - new implementation of the apply case in fo_unif using beta expansion - infinite loop fix while unifying terms in an invalid metasenv --- helm/ocaml/cic_unification/.depend | 6 +- helm/ocaml/cic_unification/cicMetaSubst.ml | 5 +- helm/ocaml/cic_unification/cicMetaSubst.mli | 1 + helm/ocaml/cic_unification/cicRefine.ml | 16 +-- helm/ocaml/cic_unification/cicUnification.ml | 108 +++++++++++-------- 5 files changed, 80 insertions(+), 56 deletions(-) diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index b91986315..c71893c83 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -3,10 +3,12 @@ cicMkImplicit.cmo: cicMkImplicit.cmi cicMkImplicit.cmx: cicMkImplicit.cmi cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi -cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi -cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi freshNamesGenerator.cmo: freshNamesGenerator.cmi freshNamesGenerator.cmx: freshNamesGenerator.cmi +cicUnification.cmo: cicMetaSubst.cmi freshNamesGenerator.cmi \ + cicUnification.cmi +cicUnification.cmx: cicMetaSubst.cmx freshNamesGenerator.cmx \ + cicUnification.cmi cicRefine.cmo: cicMetaSubst.cmi cicMkImplicit.cmi cicUnification.cmi \ freshNamesGenerator.cmi cicRefine.cmi cicRefine.cmx: cicMetaSubst.cmx cicMkImplicit.cmx cicUnification.cmx \ diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 512c65d98..d5262f44b 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -25,6 +25,7 @@ open Printf + exception MetaSubstFailure of string exception Uncertain of string exception AssertFailure of string @@ -239,6 +240,7 @@ let are_convertible subst context t1 t2 = CicReduction.are_convertible context t1 t2 let tempi_type_of_aux_subst = ref 0.0;; +let tempi_subst = ref 0.0;; let tempi_type_of_aux = ref 0.0;; let type_of_aux' metasenv subst context term = @@ -261,7 +263,8 @@ let res = in let time3 = Unix.gettimeofday () in tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; - tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; + tempi_subst := !tempi_subst +. time2 -. time1 ; + tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ; res (**** DELIFT ****) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 4f055f1f8..546a71dea 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -52,6 +52,7 @@ val type_of_aux': Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term val tempi_type_of_aux : float ref +val tempi_subst : float ref val tempi_type_of_aux_subst : float ref (*** delifting ***) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index e8ea0769d..7bd3de5c2 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -452,6 +452,7 @@ and type_of_aux' metasenv context t = | ((uri,t) as subst)::tl -> let typeofvar = CicSubstitution.subst_vars substs (type_of_variable uri) in +(* CSC: why was this code here? it is wrong (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise @@ -463,16 +464,19 @@ and type_of_aux' metasenv context t = (RefineFailure ("Unkown variable definition " ^ UriManager.string_of_uri uri)) ) ; +*) let typeoft,metasubst',metasenv' = type_of_aux metasubst metasenv context t in - try - let metasubst'',metasenv'' = + let metasubst'',metasenv'' = + try fo_unif_subst metasubst' context metasenv' typeoft typeofvar - in - check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl - with _ -> - raise (RefineFailure "Wrong Explicit Named Substitution") + with _ -> + raise (RefineFailure + ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ + " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar)) + in + check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl in check_exp_named_subst_aux metasubst metasenv [] diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 8a1f4c43e..81e794c8c 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -43,11 +43,11 @@ let type_of_aux' metasenv subst context term = (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv metasenv subst) msg))) -let rec eta_expand test_equality_only metasenv subst context t arg = - let module T = CicTypeChecker in +let rec beta_expand test_equality_only metasenv subst context t arg = let module S = CicSubstitution in let module C = Cic in let rec aux metasenv subst n context t' = +(*prerr_endline ("1 ciclo di beta_expand arg=" ^ CicMetaSubst.ppterm subst arg ^ " ; term=" ^ CicMetaSubst.ppterm subst t') ;*) try let subst,metasenv = fo_unif_subst test_equality_only subst context metasenv arg t' @@ -156,7 +156,7 @@ let rec eta_expand test_equality_only metasenv subst context t arg = subst,metasenv,(uri,t')::l) ens (subst,metasenv,[]) in let argty = - T.type_of_aux' metasenv context arg + type_of_aux' metasenv subst context arg in let fresh_name = FreshNamesGenerator.mk_fresh_name @@ -165,10 +165,10 @@ let rec eta_expand test_equality_only metasenv subst context t arg = let subst,metasenv,t' = aux metasenv subst 0 context t in subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] -and eta_expand_many test_equality_only metasenv subst context t = +and beta_expand_many test_equality_only metasenv subst context t = List.fold_left (fun (subst,metasenv,t) arg -> - eta_expand test_equality_only metasenv subst context t arg + beta_expand test_equality_only metasenv subst context t arg ) (subst,metasenv,t) (* NUOVA UNIFICAZIONE *) @@ -204,7 +204,7 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = (try let subst,metasenv = fo_unif_subst - test_equality_only subst context metasenv t1' t2' + test_equality_only subst context metasenv t1' t2' in true,subst,metasenv with @@ -236,53 +236,64 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = let fo_unif_subst_ordered test_equality_only subst context metasenv m1 m2 = fo_unif_subst test_equality_only subst context metasenv - (lower m1 m2) (upper m1 m2) + (lower m1 m2) (upper m1 m2) in - let subst'',metasenv' = + begin try let oldt = (List.assoc n subst) in let lifted_oldt = S.lift_meta l oldt in fo_unif_subst_ordered - test_equality_only subst context metasenv t lifted_oldt + test_equality_only subst context metasenv t lifted_oldt with Not_found -> - let t',metasenv',subst' = - try - CicMetaSubst.delift n subst context metasenv l t - with - (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg) - | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) - in - let t'' = - match t' with - C.Sort (C.Type u) when not test_equality_only -> - let u' = CicUniv.fresh () in - let s = C.Sort (C.Type u') in - ignore (CicUniv.add_ge (upper u u') (lower u u')) ; - s - | _ -> t' - in - (n, t'')::subst', metasenv' - in - let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in - (try - let tyt = - type_of_aux' metasenv' subst'' context t - in - fo_unif_subst - test_equality_only - subst'' context metasenv' tyt (S.lift_meta l meta_type) - with AssertFailure _ -> - (* TODO huge hack!!!! - * we keep on unifying/refining in the hope that the problem will be - * eventually solved. In the meantime we're breaking a big invariant: - * the terms that we are unifying are no longer well typed in the - * current context (in the worst case we could even diverge) - *) + (* First of all we unify the type of the meta with the type of the term *) + let subst,metasenv = + let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in + (try + let tyt = + type_of_aux' metasenv subst context t + in + fo_unif_subst + test_equality_only + subst context metasenv tyt (S.lift_meta l meta_type) + with AssertFailure _ -> + (* TODO huge hack!!!! + * we keep on unifying/refining in the hope that the problem will be + * eventually solved. In the meantime we're breaking a big invariant: + * the terms that we are unifying are no longer well typed in the + * current context (in the worst case we could even diverge) + *) (* prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN."; prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; *) - (subst'', metasenv')) + (subst, metasenv)) + in + let t',metasenv,subst = + try + CicMetaSubst.delift n subst context metasenv l t + with + (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg) + | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) + in + let t'' = + match t' with + C.Sort (C.Type u) when not test_equality_only -> + let u' = CicUniv.fresh () in + let s = C.Sort (C.Type u') in + ignore (CicUniv.add_ge (upper u u') (lower u u')) ; + s + | _ -> t' + in + (* Unifying the types may have already instantiated n. Let's check *) + try + let oldt = (List.assoc n subst) in + let lifted_oldt = S.lift_meta l oldt in + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt + with + Not_found -> + (n,t'')::subst, metasenv + end | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> if UriManager.eq uri1 uri2 then @@ -333,21 +344,24 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; | (C.Appl l1, C.Appl l2) -> let subst,metasenv,t1',t2' = match l1,l2 with + C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j -> + subst,metasenv,t1,t2 (* In the first two cases when we reach the next begin ... end section useless work is done since, by construction, the list of arguments will be equal. *) - C.Meta (i,l)::args, _ -> + | C.Meta (i,l)::args, _ -> let subst,metasenv,t2' = - eta_expand_many test_equality_only metasenv subst context t2 args + beta_expand_many test_equality_only metasenv subst context t2 args in subst,metasenv,t1,t2' | _, C.Meta (i,l)::args -> let subst,metasenv,t1' = - eta_expand_many test_equality_only metasenv subst context t1 args + beta_expand_many test_equality_only metasenv subst context t1 args in subst,metasenv,t1',t2 - | _,_ -> subst,metasenv,t1,t2 + | _,_ -> + subst,metasenv,t1,t2 in begin match t1',t2' with -- 2.39.2