From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 30 Sep 2009 20:19:38 +0000 (+0000)
Subject: rewritten instantiate code
X-Git-Tag: make_still_working~3409
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7b112b0cd39c5ab0db5c28636c0a7f7e36b4d6e2;p=helm.git

rewritten instantiate code
---

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index bdd0adfe0..496648f55 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -463,7 +463,7 @@ let mk_meta ?(attrs=[]) metasenv context ty =
     menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
   | `Sort ->
     let ty = NCic.Implicit (`Typeof n) in
-    mk_meta (tyof attrs) n metasenv [] (`WithType ty)
+    mk_meta (`IsSort::tyof attrs) n metasenv [] (`WithType ty)
   | `Type ->
     let metasenv, _, ty, _ = 
       mk_meta (tyof attrs) (newmeta ()) metasenv context `Sort in
diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index a84ce0f4f..e3112f3f2 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -316,6 +316,40 @@ let look_for_hint hdb metasenv subst context t1 t2 =
   rc
 ;;
 
+let pp_hint t p =
+  let context, t = 
+     let rec aux ctx = function
+       | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
+       | t -> ctx, t
+     in
+      aux [] t
+  in
+  let recproblems, concl = 
+    let rec aux ctx = function
+      | NCic.LetIn (name,ty,bo,rest) -> aux ((name, NCic.Def(bo,ty))::ctx) rest
+      | t -> ctx, t
+    in
+      aux [] t
+  in
+  let buff = Buffer.create 100 in
+  let fmt = Format.formatter_of_buffer buff in
+(*
+  F.fprintf "@[<hov>"
+   F.fprintf "@[<hov>"
+(*    pp_ctx [] context *)
+   F.fprintf "@]"
+  F.fprintf "@;"
+   F.fprintf "@[<hov>"
+(*    pp_ctx context recproblems *)
+   F.fprintf "@]"
+  F.fprintf "\vdash@;";
+    NCicPp.ppterm ~fmt ~context:(recproblems@context) ~subst:[] ~metasenv:[];
+  F.fprintf "@]"
+  F.fprintf formatter "@?";
+  prerr_endline (Buffer.contents buff);
+*)
+()
+;;
 
 let generate_dot_file status fmt =
   let module Pp = GraphvizPp.Dot in
@@ -344,18 +378,20 @@ let generate_dot_file status fmt =
                (NCicPp.ppterm 
                 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
             in
-            let hint =  "???" (*
+            let shint =  "???" (*
               string_of_int precedence ^ "..." ^
               Str.global_substitute (Str.regexp "\n") (fun _ -> "")
                (NCicPp.ppterm 
                 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*)
             in
             nodes := (mangle l,l) :: (mangle r,r) :: !nodes;
-            edges := (mangle l, mangle r, hint) :: !edges)
+            edges := (mangle l, mangle r, shint, precedence, hint) :: !edges)
         (HintSet.elements dataset);
     );
   List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
-  List.iter (fun x, y, l -> 
+  List.iter (fun x, y, l, _, _ -> 
       Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
   !edges;
+  edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges;
+  List.iter (fun x, y, _, p, l -> pp_hint l p) !edges;
 ;;
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 09b1f3d2e..8e3cf216e 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -200,98 +200,115 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
     if swap then unify rdb test_eq_only m s c t2 t1 
     else unify rdb test_eq_only m s c t1 t2
   in
-  let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
+  let has_tag = List.exists in
+  let tags, _, ty = NCicUtils.lookup_meta n metasenv in
+  (* on the types *)
   let metasenv, subst, t = 
     match ty with 
-    | NCic.Implicit (`Typeof _) ->
-       (match NCicReduction.whd ~subst context t with
-          NCic.Sort _ -> metasenv,subst,t
-        | NCic.Meta (i,_) when
-           let _,_,ty = NCicUtils.lookup_meta i metasenv in
-            (match ty with
-                NCic.Implicit (`Typeof _) -> true
-              | _ -> false)
-           -> metasenv,subst,t
-        | NCic.Meta (i,_) ->
-           let rec remove_and_hope i =
-            let _,ctx,ty = NCicUtils.lookup_meta i metasenv in
-            match ty with
-               NCic.Implicit _ -> List.filter (fun i',_ -> i <> i') metasenv
-             | _ ->
-               match NCicReduction.whd ~subst ctx ty with
-                  NCic.Meta (j,_) ->
-                   let metasenv = remove_and_hope j in
-                    List.filter (fun i',_ -> i <> i') metasenv
-                | _ -> assert false (* NON POSSO RESTRINGERE *)
-           in
-           let metasenv = remove_and_hope i in
-           let metasenv =
-            (i,([],[],NCic.Implicit (`Typeof i)))::
-             List.filter (fun i',_ -> i <> i') metasenv
-           in
-            metasenv,subst,t
-        | NCic.Appl (NCic.Meta _::_) ->
-           raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
-        | t when could_reduce t -> 
-           raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
-        | _ ->
-           raise (UnificationFailure (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
+    | NCic.Implicit (`Typeof _) -> 
+         pp(lazy("meta with no type"));
+         assert(has_tag ((=)`IsSort) tags); 
+         metasenv, subst, t
     | _ ->
-       pp (lazy (
-               "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
-          ppcontext ~metasenv ~subst context ^ 
-          ppmetasenv ~subst metasenv));
        let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
          with 
          | NCicTypeChecker.AssertFailure msg -> 
-           (pp (lazy "fine typeof (fallimento)");
-           let ft = fix_sorts swap exc_to_be t in
-           if ft == t then 
-             (prerr_endline ( ("ILLTYPED: " ^ 
-                NCicPp.ppterm ~metasenv ~subst ~context t
-            ^ "\nBECAUSE:" ^ Lazy.force msg ^ 
-            ppcontext ~metasenv ~subst context ^ 
-            ppmetasenv ~subst metasenv
-            ));
-                     assert false)
-           else
-            try 
-              pp (lazy ("typeof: " ^ 
-                NCicPp.ppterm ~metasenv ~subst ~context ft));
-              ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-            with NCicTypeChecker.AssertFailure _ -> 
-              assert false)
+              pp(lazy("we try to fix the sort\n"^Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst
+              metasenv));
+              let ft = fix_sorts swap exc_to_be t in
+              pp(lazy("unable to fix the sort"));
+              if ft == t then begin
+                raise (UnificationFailure (lazy ("unable to fix sorts of: "^
+                  NCicPp.ppterm ~metasenv ~subst ~context t)))
+              end;
+              (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
+               with NCicTypeChecker.AssertFailure _ -> 
+                 raise (UnificationFailure (lazy 
+                   ("fix sorts generated an ill-typed: "^
+                   NCicPp.ppterm ~metasenv ~subst ~context t))))
          | NCicTypeChecker.TypeCheckerFailure msg ->
               prerr_endline (Lazy.force msg);
-       prerr_endline (
-               "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
-          ppcontext ~metasenv ~subst context ^ 
-          ppmetasenv ~subst metasenv);
-              pp msg; assert false
+              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+              prerr_endline (ppcontext ~metasenv ~subst context); 
+              prerr_endline (ppmetasenv ~subst metasenv);
+              assert false
        in
-       let lty = NCicSubstitution.subst_meta lc ty in
        match ty_t with
-       | NCic.Implicit _ -> 
-           raise (UnificationFailure 
-             (lazy "trying to unify a term with a type"))
-       | ty_t -> 
+       | NCic.Implicit (`Typeof _) -> 
+           raise (UnificationFailure(lazy "trying to unify a term with a type"))
+       | _ -> 
+          let lty = NCicSubstitution.subst_meta lc ty in
           pp (lazy ("On the types: " ^
-           NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
-           NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
-            ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
+              NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ 
+              NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
           let metasenv,subst = 
-           try
-            unify test_eq_only metasenv subst context lty ty_t
+           try unify test_eq_only metasenv subst context lty ty_t
            with NCicEnvironment.BadConstraint _ as exc ->
             let ty_t = fix_sorts swap exc_to_be ty_t in 
              try unify test_eq_only metasenv subst context lty ty_t
-             with _ -> raise exc in
-          metasenv, subst, t
+             with 
+             | NCicEnvironment.BadConstraint _ 
+             | UnificationFailure _ -> raise exc 
+          in
+           metasenv, subst, t
+  in 
+  (* viral sortification *)
+  let is_sort metasenv subst context t = 
+    match NCicReduction.whd ~subst context t with
+    | NCic.Meta (i,_) ->
+         let tags, _, _ = NCicUtils.lookup_meta i metasenv in
+         has_tag ((=) `IsSort) tags
+    | NCic.Sort _ -> true
+    | _ -> false
   in
-         pp (lazy(string_of_int n ^ " := 111 = "^
-           NCicPp.ppterm ~metasenv ~subst ~context t));
+  let rec sortify metasenv subst = function
+    | NCic.Implicit (`Typeof _) 
+    | NCic.Sort _ as t -> metasenv, subst, t, 0
+    | NCic.Meta (i,_) as t -> 
+         let tags, context, ty = NCicUtils.lookup_meta i metasenv in
+         if has_tag ((=) `IsSort) tags then metasenv, subst, t, i
+         else
+           let ty = NCicReduction.whd ~subst context ty in
+           let metasenv, subst, ty, _ = sortify metasenv subst ty in
+           let metasenv, j, m, _ = 
+             NCicMetaSubst.mk_meta metasenv [] (`WithType ty)
+           in
+           pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
+           let metasenv,subst = unify test_eq_only metasenv subst context t m in
+           let j = if swap then i else j in
+           let tags, context, ty = NCicUtils.lookup_meta j metasenv in
+           let tags = `IsSort :: tags in
+           let metasenv = List.filter (fun x,_ -> x <> j) metasenv in
+           let metasenv = (j,(tags,context,ty)) ::metasenv in 
+           metasenv, subst, m, j 
+    | t -> 
+         if could_reduce t then raise (Uncertain(lazy "not a sort"))
+         else raise (UnificationFailure(lazy "not a sort"))
+  in
+  let metasenv, subst, _, n = 
+    if has_tag ((=) `IsSort) tags then
+      let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t)
+      in m,s,x,n
+    else if is_sort metasenv subst context t then
+      sortify metasenv subst (NCic.Meta (n,lc))
+    else
+      metasenv, subst, NCic.Rel ~-1,n
+  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 = 
     try 
       NCicMetaSubst.delift 
@@ -323,7 +340,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
   with NCicUtils.Subst_not_found _ -> 
     (* by cumulativity when unify(?,Type_i) 
      * we could ? := Type_j with j <= i... *)
-    let subst = (n, (name, ctx, t, ty)) :: subst in
+    let subst = (n, (tags, ctx, t, ty)) :: subst in
     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
       ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
     let metasenv =