From fed8f1a2c4d10e8b6411ae471d0f85636d2f13a9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Jul 2009 16:30:26 +0000 Subject: [PATCH] Very serious bug fixed in unification, but the fix is very ugly. Explanation: we have reduced the case ? x1 .. xn to the case ?[x1,...,xn] by mean of lambda-abstractions. However, these need to be typed. The way we used to type them was with non-dependent types. Thus they failed in almost all dependent cases (like rewrite). This fix seems to work and uses a few lines of code, but it requires a call to the unifier which is VEEERY bad. Debugging prints still to be removed. --- .../components/ng_refiner/nCicRefiner.ml | 2 + .../components/ng_refiner/nCicUnification.ml | 76 ++++++++++++++----- .../components/ng_refiner/nCicUnification.mli | 7 ++ 3 files changed, 66 insertions(+), 19 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 8872cbc9b..2b648d857 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -745,4 +745,6 @@ let typeof_obj uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr) ;; +NCicUnification.set_refiner_typeof typeof;; + (* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 13ddac96d..71203b3a5 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -15,6 +15,11 @@ exception UnificationFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +let refiner_typeof = + ref (fun _ ?localise _ _ _ _ _ -> ignore localise; assert false);; +let set_refiner_typeof f = refiner_typeof := f +;; + let (===) x y = Pervasives.compare x y = 0 ;; let uncert_exc metasenv subst context t1 t2 = @@ -80,7 +85,12 @@ module Ref = NReference;; let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; -let outside () = indent := String.sub !indent 0 (String.length !indent -1);; +let outside () = + try + indent := String.sub !indent 0 (String.length !indent -1) + with + Invalid_argument _ -> indent := "??"; () +;; let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) @@ -89,8 +99,8 @@ let pp s = let ppcontext = NCicPp.ppcontext;; let ppmetasenv = NCicPp.ppmetasenv;; -(*let ppcontext ~metasenv ~subst context = "...";; -let ppmetasenv ~subst metasenv = "...";;*) +let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "...";; +let ppmetasenv ~subst:_subst _metasenv = "...";; let pp _ = ();; @@ -121,24 +131,51 @@ let is_locked n subst = with NCicUtils.Subst_not_found _ -> false ;; +let rec mk_irl = + function + 0 -> [] + | n -> NCic.Rel n :: mk_irl (n-1) +;; -let rec lambda_intros metasenv subst context t args = +let rec lambda_intros rdb metasenv subst context t args = let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in - let argsty = List.map (NCicTypeChecker.typeof ~metasenv ~subst context) args in - let rec mk_lambda context n = function - | [] -> + let argsty = + List.map + (fun arg -> arg, NCicTypeChecker.typeof ~metasenv ~subst context arg) args in + let context_of_args = context in + let mk_appl = function [] -> assert false | [t] -> t | l -> NCic.Appl l in + let rec mk_lambda metasenv subst context n processed_args = function + | [] -> let metasenv, _, bo, _ = NCicMetaSubst.mk_meta metasenv context (`WithType (NCicSubstitution.lift n tty)) in - metasenv, bo - | ty::tail -> + metasenv, subst, bo + | (arg,ty)::tail -> let name = "HBeta"^string_of_int n in - let ty = NCicSubstitution.lift n ty in - let metasenv, bo = mk_lambda ((name,NCic.Decl ty)::context) (n+1) tail in - metasenv, NCic.Lambda (name, ty, bo) + let metasenv,_,instance,_ = + NCicMetaSubst.mk_meta metasenv context_of_args `Term in + let meta_applied = mk_appl (instance::List.rev processed_args) in +let metasenv,subst,_,_ = + !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None +in +prerr_endline ("########################## LI1: " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args meta_applied ^ " vs " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty); +prerr_endline (NCicPp.ppcontext ~metasenv ~subst context_of_args); +prerr_endline (NCicPp.ppmetasenv metasenv ~subst); + let metasenv,subst = + unify rdb true metasenv subst context_of_args meta_applied ty in +prerr_endline "UNIFY FINITA"; + let telescopic_ty = NCicSubstitution.lift n instance in + let telescopic_ty = + mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in +prerr_endline ("########################## LI: " ^ NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty); + let metasenv, subst, bo = + mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1) + (arg::processed_args) tail + in + metasenv, subst, NCic.Lambda (name, telescopic_ty, bo) in - mk_lambda context 0 argsty + mk_lambda metasenv subst context 0 [] argsty and instantiate rdb test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = @@ -314,9 +351,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = | NCic.Appl (NCic.Meta (i,l)::args) when not (NCicMetaSubst.flexible subst args) -> - let metasenv, lambda_Mj = - lambda_intros metasenv subst context t1 args + let metasenv, subst, lambda_Mj = + lambda_intros rdb metasenv subst context t1 args in +prerr_endline ("XXXXXXXXX " ^ NCicPp.ppterm ~metasenv ~subst ~context lambda_Mj); unify rdb test_eq_only metasenv subst context (C.Meta (i,l)) lambda_Mj, i @@ -395,8 +433,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = not (NCicMetaSubst.flexible subst args) -> (* we verify that none of the args is a Meta, since beta expanding w.r.t a metavariable makes no sense *) - let metasenv, lambda_Mj = - lambda_intros metasenv subst context t1 args + let metasenv, subst, lambda_Mj = + lambda_intros rdb metasenv subst context t1 args in let metasenv, subst = unify rdb test_eq_only metasenv subst context @@ -414,8 +452,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = | _, NCic.Appl (NCic.Meta (i,l)::args) when not(NCicMetaSubst.flexible subst args) -> - let metasenv, lambda_Mj = - lambda_intros metasenv subst context t2 args + let metasenv, subst, lambda_Mj = + lambda_intros rdb metasenv subst context t2 args in let metasenv, subst = unify rdb test_eq_only metasenv subst context diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index a6ddfaeed..47a59d4f2 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -15,6 +15,13 @@ exception UnificationFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +val set_refiner_typeof: + (NRstatus.status -> + ?localise:(NCic.term -> Stdpp.location) -> + NCic.metasenv -> NCic.substitution -> NCic.context -> + NCic.term -> NCic.term option -> (* term, expected type *) + NCic.metasenv * NCic.substitution * NCic.term * NCic.term) -> unit + val unify : #NRstatus.status -> ?test_eq_only:bool -> (* default: false *) -- 2.39.2