From: Andrea Asperti Date: Fri, 22 Oct 2004 12:16:22 +0000 (+0000) Subject: - ported to typed explicit subst X-Git-Tag: V_0_0_10~45 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16e2e2496f35a96c59e909133ff69767d37298aa;p=helm.git - ported to typed explicit subst - beta expansion in the case of Appl commented, waiting for a better solution --- diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index cebbb9e8f..63abdfb01 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -59,6 +59,7 @@ let type_of_aux' metasenv subst context term = (CicMetaSubst.ppmetasenv metasenv subst) msg))) *) let rec deref subst = + let snd (_,a,_) = a in function Cic.Meta(n,l) as t -> (try @@ -241,6 +242,9 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = let module S = CicSubstitution in let t1 = deref subst t1 in let t2 = deref subst t2 in + if R.are_convertible ~subst ~metasenv context t1 t2 then + subst, metasenv + else match (t1, t2) with (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> let _,subst,metasenv = @@ -346,14 +350,14 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str in (* Unifying the types may have already instantiated n. Let's check *) try - let (_, oldt) = CicUtil.lookup_subst n subst in + let (_, oldt,_) = CicUtil.lookup_subst 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 CicUtil.Subst_not_found _ -> - let (_, context, _) = CicUtil.lookup_meta n metasenv in - let subst = (n, (context, t'')) :: subst in + let (_, context, ty) = CicUtil.lookup_meta n metasenv in + let subst = (n, (context, t'',ty)) :: subst in let metasenv = List.filter (fun (m,_,_) -> not (n = m)) metasenv in subst, metasenv @@ -421,6 +425,8 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str beta_reduce (Cic.Appl(he''::tl')) | t -> t in (match l1,l2 with +(* andrea : this was too powerful. It works very bad with f_equal and + similar terms, try and see C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j -> (try List.fold_left2 @@ -430,7 +436,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str with (Invalid_argument msg) -> raise (UnificationFailure msg)) | C.Meta (i,l)::args, _ -> (try - let (_,t) = CicUtil.lookup_subst i subst in + let (_,t,_) = CicUtil.lookup_subst i subst in let lifted = S.lift_meta l t in let reduced = beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst @@ -444,7 +450,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str (C.Meta (i,l)) beta_expanded) | _, C.Meta (i,l)::args -> (try - let (_,t) = CicUtil.lookup_subst i subst in + let (_,t,_) = CicUtil.lookup_subst i subst in let lifted = S.lift_meta l t in let reduced = beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst @@ -456,6 +462,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str test_equality_only metasenv subst context t1 args in fo_unif_subst test_equality_only subst context metasenv (C.Meta (i,l)) beta_expanded) +*) | _,_ -> let lr1 = List.rev l1 in let lr2 = List.rev l2 in diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 9956b3043..9d26fd3df 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -35,7 +35,7 @@ exception AssertFailure of string;; (* withouth first unwinding it. *) val fo_unif : Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> - CicMetaSubst.substitution * Cic.metasenv + Cic.substitution * Cic.metasenv (* fo_unif_subst metasenv subst context t1 t2 *) (* unifies [t1] and [t2] in a context [context] *) @@ -51,7 +51,7 @@ val fo_unif : (*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la cosa all'apply_subst!!!*) val fo_unif_subst : - CicMetaSubst.substitution -> + Cic.substitution -> Cic.context -> Cic.metasenv -> Cic.term -> Cic.term -> - CicMetaSubst.substitution * Cic.metasenv + Cic.substitution * Cic.metasenv