From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 1 Oct 2009 09:36:12 +0000 (+0000)
Subject: added sortification for (? args), untested code
X-Git-Tag: make_still_working~3405
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1f30bba33513dc8257a7c89e64038c096fa21072;p=helm.git

added sortification for (? args), untested code
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index e56832fd5..d48dfaf46 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -274,6 +274,14 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
            let subst = subst_entry :: subst in
            let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
            metasenv, subst, m, j 
+    | NCic.Appl (NCic.Meta _ as hd :: args) as t -> 
+           let metasenv, subst, lambda_Mj =
+             lambda_intros rdb metasenv subst context t args
+           in
+           let metasenv,subst= unify true metasenv subst context hd lambda_Mj in
+           let t = NCicReduction.whd ~subst context t in
+           let _result = sortify metasenv subst t in       
+           (* untested, maybe dead, code *) assert false;
     | t -> 
          if could_reduce t then raise (Uncertain(lazy "not a sort"))
          else raise (UnificationFailure(lazy "not a sort"))
@@ -289,15 +297,6 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
   in
   let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in
   (* instantiation *)
-  
-  (* sortification:
-      - Meta sort === t -> check t is sort or sortify
-        - add tag `IsSort and set cc=[] to n and its pile
-        - se gli ancestor non sono sorte o meta... bum...
-          - cambiare in-place menv
-          - geneare meta fresh sorta e dall'alto al basso
-      - Meta _ === Meta sort -> sortify n (i.e. add `IsSort)
-       *)
   pp (lazy(string_of_int n ^ " := 111 = "^ 
     NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t =