more work

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index e2063e451a692ccb25fa045de3f88b21c726a499..361587b7d33402f4d3989ffde01d72538a88deb6 100644 (file)
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -539,6 +539,7 @@ let rec mk_list x = function
 ;;
 
 let list_seq start stop =
+  if start > stop then [] else
   let rec aux pos =
     if pos = stop then []
     else pos :: (aux (pos+1))

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index cde028be4417b58b8985607368e1f18a4875912b..cebdaf0b29908916a601c04756058aed1d1c8450 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -137,7 +137,7 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
           end;
         F.fprintf f "])"
    | C.Sort C.Prop -> F.fprintf f "Prop"
-   | C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse"
+   | C.Sort (C.Type []) -> F.fprintf f "Type0"
    | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
    | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
    | C.Sort (C.Type l) -> 

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 569dcb7df91b0a7cd84c9f1ae15f1f5ba86cc62c..7fe8cf3663303b9820f10141be11a79f7c3cae09 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -198,7 +198,7 @@ let _ =
       let u = OCic2NCic.nuri_of_ouri u in
       indent := 0;
       match NCicLibrary.get_obj u with
-      | _,_,_,_,NCic.Constant (_,_,_, ty, _) ->
+      | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) ->
           let rec intros = function
             | NCic.Prod (name, s, t) ->
                 let ctx, t = intros t in
@@ -209,25 +209,36 @@ let _ =
             | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
               when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
                 let menv, ty =  perforate ctx menv ty in
-                let a,b,_ = NCicMetaSubst.mk_meta menv ctx (Some ty) in a,b
+                let a,b,_ = NCicMetaSubst.mk_meta menv ctx (`WithType ty) in a,b
             | t -> 
                 NCicUntrusted.map_term_fold_a
                  (fun e ctx -> e::ctx) ctx perforate menv t
           in
+          let rec curryfy ctx = function
+            | NCic.Lambda (name, s, tgt) ->
+                let tgt = curryfy ((name,NCic.Decl s) :: ctx) tgt in
+                NCic.Lambda (name, NCic.Implicit `Type, tgt)
+            | t -> 
+                NCicUtils.map
+                 (fun e ctx -> e::ctx) ctx curryfy t
+          in
+(*
           let ctx, pty = intros ty in
           let menv, pty = perforate ctx [] pty in
+*)
 (*
           let sty, menv, _ = 
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
 *)
 (*           let ctx, ty = intros ty in *)
+(*
           let left, right = 
             match  NCicReduction.whd ~delta:max_int ctx pty with
             | NCic.Appl [eq;t;a;b] -> a, b
             | _-> assert false
           in
-               
+*)             
 
 (*
           let whd ty =
@@ -243,9 +254,12 @@ let _ =
                  (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
                  (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
 *)
+          let menv, subst, bo, infty = 
+            NCicRefiner.typeof [] [] [] (curryfy [] bo) None
+          in
           let metasenv, subst = 
             try 
-              NCicUnification.unify menv [] ctx left right
+              NCicUnification.unify menv subst [] infty ty
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg 
@@ -254,11 +268,16 @@ let _ =
                 [], []
             | Sys.Break -> [],[]
           in
-          if (NCicReduction.are_convertible ~subst ctx left right)
+          if (NCicReduction.are_convertible ~subst [] infty ty)
           then
             prerr_endline ("OK: " ^ NUri.string_of_uri u)
           else
-            (prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+            (
+          let ctx = [] in
+          let right = infty in
+          let left = ty in
+                    
+                    prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
                 prerr_endline 
                  (Printf.sprintf 
                    ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmenv:\n%s\n" ^^ 

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 102958869817e6123245a4f299a0b3f0b91ad4c6..72151deb802e4e1ca6f9c3c2f3349195a00a3090 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -572,15 +572,22 @@ let delift_rels subst metasenv n t =
 
 let mk_meta ?name metasenv context ty = 
   match ty with
-  | None ->
-    let len = List.length context in
+  | `Typeless ->
+    let n = newmeta () in
+    let ty = NCic.Implicit (`Typeof n) in
+    let menv_entry = (n, (name, context, ty)) in
+    menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty
+  | `Type 
+  | `Term ->
+    let context_for_ty = if ty = `Type then [] else context in
     let n = newmeta () in
-    let ty_menv_entry = (n, (name, context, NCic.Implicit (`Typeof n))) in
+    let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in
     let m = newmeta () in
-    let ty = NCic.Meta (n, (0,NCic.Irl len)) in
+    let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in
     let menv_entry = (m, (name, context, ty)) in
-    menv_entry :: ty_menv_entry :: metasenv, NCic.Meta (m, (0,NCic.Irl len)), ty
-  | Some ty ->
+    menv_entry :: ty_menv_entry :: metasenv, 
+      NCic.Meta (m, (0,NCic.Irl (List.length context))), ty
+  | `WithType ty ->
     let n = newmeta () in
     let len = List.length context in
     let menv_entry = (n, (name, context, ty)) in
@@ -591,7 +598,8 @@ let saturate ?(delta=0) metasenv context ty goal_arity =
  assert (goal_arity >= 0);
   let rec aux metasenv = function
    | NCic.Prod (name,s,t) ->
-       let metasenv1, arg,_ = mk_meta ~name:name metasenv context (Some s) in            
+       let metasenv1, arg,_ = 
+          mk_meta ~name:name metasenv context (`WithType s) in            
        let t, metasenv1, args, pno = 
            aux metasenv1 (NCicSubstitution.subst arg t) 
        in

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 77c6d479c732dd65005c5ff92aa877dc8891c50b..ca2bfb71415c3776e1550c3b81103594187dc047 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -52,10 +52,12 @@ val restrict:
     NCic.substitution ->
       int -> int list -> NCic.metasenv * NCic.substitution * int
 
+(* bool = true if the type of the new meta is closed *)
 val mk_meta: 
-    ?name:string -> 
-    NCic.metasenv -> NCic.context -> NCic.term option -> 
-      NCic.metasenv * NCic.term * NCic.term (* menv, instance, type *)
+   ?name:string -> 
+   NCic.metasenv -> NCic.context -> 
+    [ `WithType of NCic.term | `Term | `Type | `Typeless ] -> 
+    NCic.metasenv * NCic.term * NCic.term (* menv, instance, type *)
 
 (* returns the resulting type, the metasenv and the arguments *)
 val saturate:

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index cae9cf54fcec9e0590eae6032077715bf8d8c504..36e9b3d24b3cc6c81e39cd3e86556f968f4dcab2 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -26,30 +26,37 @@ let wrap_exc msg = function
 ;;
 
 let exp_implicit metasenv context expty =
+ let foo x = match expty with Some t -> `WithType t | None -> x in
  function      
-  | `Closed -> NCicMetaSubst.mk_meta metasenv [] expty
-  | `Type | `Term -> NCicMetaSubst.mk_meta metasenv context expty
+  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Type)
+  | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
+  | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+  | _ -> assert false
+;;
+
+let force_to_sort metasenv subst context t =
+  match NCicReduction.whd ~subst context t with
+  | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> 
+     metasenv, subst, t
+  | C.Meta (i,(_,lc)) as t ->
+     let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
+     prerr_endline "RESTRICT";
+     let metasenv, subst, _ = 
+       NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 len) 
+     in
+     metasenv, subst, t
+  | C.Sort _ -> metasenv, subst, t 
   | _ -> assert false
 ;;
 
 let sort_of_prod 
   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) 
 =
-   let restrict metasenv subst = function
-     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> 
-        metasenv, subst, t
-     | C.Meta (i,(_,lc)) as t ->
-        let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-        let metasenv, subst, _ = 
-          NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 len) 
-        in
-        metasenv, subst, t
-     | t -> metasenv, subst, t 
-   in
-   let t1 = NCicReduction.whd ~subst context t1 in
-   let t2 = NCicReduction.whd ~subst ((name,C.Decl s)::context) t2 in
-   let metasenv, subst, t1 = restrict metasenv subst t1 in
-   let metasenv, subst, t2 = restrict metasenv subst t2 in
+   let metasenv, subst, t1 = force_to_sort metasenv subst context t1 in
+   let metasenv, subst, t2 = 
+     force_to_sort metasenv subst ((name,C.Decl s)::context) t2 in
+   prerr_endline ("S1:"^NCicPp.ppterm ~metasenv ~subst ~context t1);
+   prerr_endline ("S2:"^NCicPp.ppterm ~metasenv ~subst ~context:((name,C.Decl s)::context) t2);
    match t1, t2 with
    | C.Sort _, C.Sort C.Prop -> metasenv, subst, t2
    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
@@ -80,7 +87,7 @@ let check_allowed_sort_elimination localise r orig =
      match arity1 with
      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
         let metasenv, meta, _ = 
-          NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) None 
+          NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Typeless 
         in
         let metasenv, subst = 
           try NCicUnification.unify metasenv subst context 
@@ -93,9 +100,11 @@ let check_allowed_sort_elimination localise r orig =
         aux metasenv subst ((name, C.Decl so1)::context)
          (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
      | C.Sort _ (* , t ==?== C.Prod _ *) ->
-        let metasenv, meta, _ = 
-          NCicMetaSubst.mk_meta metasenv (("_",C.Decl ind)::context) None 
-        in
+        let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Typeless in
+        prerr_endline (
+            (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta))) ^ " ==== " ^
+            (NCicPp.ppterm ~subst ~metasenv ~context arity2) ^ "\nMENV:\n"
+            ^ NCicPp.ppmetasenv ~subst metasenv);
         let metasenv, subst = 
           try NCicUnification.unify metasenv subst context 
                 (C.Prod ("_", ind, meta)) arity2 
@@ -105,7 +114,8 @@ let check_allowed_sort_elimination localise r orig =
             (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
         in
         (try NCicTypeChecker.check_allowed_sort_elimination
-             ~metasenv ~subst r context ind arity1 arity2
+            ~metasenv ~subst r context ind arity1 arity2; 
+            metasenv, subst
         with exc -> raise (wrap_exc (lazy (localise orig, 
           "Sort elimination not allowed ")) exc))
      | _ -> assert false
@@ -122,6 +132,10 @@ let rec typeof
        | C.Implicit _ 
        | C.Lambda _ -> metasenv, subst, t, expty
        | _ ->
+          prerr_endline ("F:" ^
+          (NCicPp.ppterm ~metasenv ~subst ~context infty) ^  " === " ^
+          (NCicPp.ppterm ~metasenv ~subst ~context expty) ^ "\nMENV:\n" ^
+          NCicPp.ppmetasenv ~subst metasenv);
          let metasenv, subst = 
            try NCicUnification.unify metasenv subst context infty expty
            with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
@@ -134,7 +148,8 @@ let rec typeof
     | None -> metasenv, subst, t, infty
   in
   let rec typeof_aux metasenv subst context expty = 
-    fun t as orig -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*)
+    fun t as orig -> 
+    prerr_endline ("R:"^NCicPp.ppterm ~metasenv ~subst ~context t);
     let metasenv, subst, t, infty = 
     match t with
     | C.Rel n ->
@@ -187,7 +202,9 @@ let rec typeof
              | C.Prod (_,s,t) -> Some s, Some t
              | _ -> None, None
        in
-       let metasenv, subst, s, _ = typeof_aux metasenv subst context None s in
+       let metasenv, subst, s, ty_s = 
+         typeof_aux metasenv subst context None s in
+       let metasenv, subst, _ = force_to_sort metasenv subst context ty_s in
        let (metasenv,subst), exp_ty_t = 
          match exp_s with 
          | Some exp_s -> 
@@ -205,7 +222,9 @@ let rec typeof
        in
        metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
     | C.LetIn (n,ty,t,bo) ->
-       let metasenv, subst, ty, _ = typeof_aux metasenv subst context None ty in
+       let metasenv, subst, ty, ty_ty = 
+         typeof_aux metasenv subst context None ty in
+       let metasenv, subst, _ = force_to_sort metasenv subst context ty_ty in
        let metasenv, subst, t, _ = 
          typeof_aux metasenv subst context (Some ty) t in
        let context = (n, C.Def (t,ty)) :: context in
@@ -238,8 +257,10 @@ let rec typeof
         else C.Appl ((C.Const r)::parameters) in
       let metasenv, subst, ind, ind_ty = 
         typeof_aux metasenv subst context None ind in
-      check_allowed_sort_elimination localise r orig_term metasenv subst context
-       ind ind_ty outsort;
+      let metasenv, subst = 
+         check_allowed_sort_elimination localise r orig_term metasenv subst 
+           context ind ind_ty outsort 
+      in
       (* let's check if the type of branches are right *)
       if List.length pl <> constructorsno then
        raise (RefineFailure (lazy (localise orig, 
@@ -286,9 +307,14 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
             typeof ~localise metasenv subst context arg None in
           let metasenv, meta, _ = 
             NCicMetaSubst.mk_meta metasenv 
-              (("_",C.Decl ty_arg) :: context) None
+              (("_",C.Decl ty_arg) :: context) `Type
           in
           let flex_prod = C.Prod ("_", ty_arg, meta) in
+          prerr_endline ("F:" ^
+          (NCicPp.ppterm ~metasenv ~subst ~context t) ^  " === " ^
+          (NCicPp.ppterm ~metasenv ~subst ~context flex_prod) ^ "\nMENV:\n" ^
+          NCicPp.ppmetasenv ~subst metasenv ^ "\nCTX:\n" ^
+          NCicPp.ppcontext ~metasenv ~subst context);
           let metasenv, subst = 
              try NCicUnification.unify metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d34e3efcc00abb6a485ecafe1de844b8ea9f902d..10bc29a62d2ca398aa9b092859fea079b1d6f5db 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -147,19 +147,24 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
   in
-  let ty_t = 
-    try NCicTypeChecker.typeof ~subst ~metasenv context t 
-    with NCicTypeChecker.TypeCheckerFailure msg -> 
-      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-      prerr_endline (Lazy.force msg);
-      assert false
-  in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let lty = NCicSubstitution.subst_meta lc ty in
-  pp (lazy("On the types: " ^
-   NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
-    ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
-  let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
+  let metasenv, subst = 
+    match ty with 
+    | NCic.Implicit (`Typeof _) -> metasenv, subst
+    | _ ->
+       let lty = NCicSubstitution.subst_meta lc ty in
+       let ty_t = 
+         try NCicTypeChecker.typeof ~subst ~metasenv context t 
+         with NCicTypeChecker.TypeCheckerFailure msg -> 
+           prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+           prerr_endline (Lazy.force msg);
+           assert false
+       in
+       pp (lazy("On the types: " ^
+        NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+         ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
+       unify test_eq_only metasenv subst context lty ty_t 
+  in
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
     with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)