From 08e552969f366bd18b5bb7515bbc514576a9b395 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 28 Oct 2009 16:29:46 +0000 Subject: [PATCH] Ad-hoc management of ? vs out_scope in instantiate. The library passes again, but there seems to be still more work to do in instantiate. --- .../components/ng_refiner/nCicUnification.ml | 29 +++++++++++++++---- 1 file changed, 24 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 936d1ec8d..71b790a26 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -307,11 +307,30 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = let t = NCic.Sort (NCic.Type u) in move_to_subst n attrs cc t ty metasenv subst else (raise exc) - | _, _, NCic.Meta(m,lcm), _ when List.mem_assoc m subst -> - (* deref needed for locked metas, maybe should be done outside *) - let _,_,bo,_ = NCicUtils.lookup_subst m subst in - let bo = NCicSubstitution.subst_meta lcm bo in - instantiate rdb test_eq_only metasenv subst context n lc bo swap + | kind, ty, NCic.Meta(m,lcm), _ when List.mem_assoc m subst -> + let at,ccm,bo,tym = NCicUtils.lookup_subst m subst in + if NCicMetaSubst.is_out_scope_tag at then + begin + (* Case meta vs out-scope *) + pp(lazy("4.1")); + let ty_t, ccm, kindm = + NCicSubstitution.subst_meta lcm tym, ccm, + NCicUntrusted.kind_of_meta at in + let lty = NCicSubstitution.subst_meta lc ty in + pp (lazy ("On the types: " ^ + ppterm ~metasenv ~subst ~context lty ^ + (if test_eq_only then " === " else "=<=") ^ + ppterm ~metasenv ~subst ~context ty_t)); + let metasenv, subst = + unify rdb test_eq_only metasenv subst context ty_t lty in + (*CSC: here I should call kindfy, but it fails since the second + meta in in the susbt, not the metasenv! *) + (* let metasenv,t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in *) + delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst + end + else + let bo = NCicSubstitution.subst_meta lcm bo in + instantiate rdb test_eq_only metasenv subst context n lc bo swap | kind, (NCic.Implicit (`Typeof _) as bot), NCic.Meta(m,lcm), _ -> pp(lazy("5")); let attrsm, ccm, tym = NCicUtils.lookup_meta m metasenv in -- 2.39.2