X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=e56832fd502656a764891b6ce4da49ebd065a3e5;hb=7110ed13ffccb214bc3aafe37f6a7c24f59a49e5;hp=291dcabdde30c808b88db0c362bc09fbefa1e0b6;hpb=7ca0a000878e864c92d94f77900bc2ca0ac143b9;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 291dcabdd..e56832fd5 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -130,7 +130,7 @@ let fix_sorts swap exc t =
 let is_locked n subst =
    try
      match NCicUtils.lookup_subst n subst with
-     | Some tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
+     | tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
      | _ -> false
    with NCicUtils.Subst_not_found _ -> false
 ;;
@@ -200,98 +200,106 @@ 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,(None,[],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)
+         | NCicTypeChecker.AssertFailure msg as exn -> 
+              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 raise exn;
+              (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
+               with NCicTypeChecker.AssertFailure _ -> raise exn)
          | 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 _) -> assert false 
+    | 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 ~attrs:[`IsSort] [] (`WithType ty)
+           in
+           pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
+           let subst_entry = i, (tags, context, m, ty) in
+           let subst = subst_entry :: subst in
+           let metasenv = List.filter (fun x,_ -> i <> x) 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 +331,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 = 
@@ -427,11 +435,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
               let subst =
                List.map (fun (i,(tag,ctx,bo,ty)) ->
                 let tag =
-                 match tag with
-                    Some tag when
-                        tag = NCicMetaSubst.in_scope_tag
-                     || NCicMetaSubst.is_out_scope_tag tag -> None
-                  | _ -> tag
+                 List.filter
+                  (function `InScope | `OutScope _ -> false | _ -> true) tag
                 in
                   i,(tag,ctx,bo,ty)
                 ) subst