many bugs fixed

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index bb423690b177a2865aae6b19914822e555ffa61f..7d13b9a35df112e7a76d5441203d2dae77dbf129 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -282,7 +282,7 @@ let _ =
                   metasenv, subst
               | Sys.Break -> metasenv, subst
             in
-            if (NCicReduction.are_convertible ~subst [] infty ty)
+            if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty)
             then
               prerr_endline ("OK: " ^ NUri.string_of_uri u)
             else
@@ -308,11 +308,16 @@ let _ =
               NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
             in*)
           with
+          | Sys.Break -> ()
           | NCicRefiner.RefineFailure msg 
           | NCicRefiner.Uncertain msg ->
              let _, msg = Lazy.force msg in
              prerr_endline msg;
-             prerr_endline ("FAIL: " ^ NUri.string_of_uri u))
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+          | e -> 
+             prerr_endline (Printexc.to_string e); 
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+             )
       | _ -> ())
     alluris;
 ;;

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 12fe977083ec04a2c9ee309c116e2cb22419929b..6abe62e809de4803da53fdde26c71394e1292f5f 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -204,6 +204,7 @@ let rec force_does_not_occur metasenv subst restrictions t =
         * instantiated/restricted metavariabels *)
        let (metasenv,subst as ms), restrictions_for_n, l' =
          let l = NCicUtils.expand_local_context lc in
+
          let ms, _, restrictions_for_n, l =
           List.fold_right
             (fun t (ms, i, restrictions_for_n, l) ->
@@ -214,6 +215,7 @@ let rec force_does_not_occur metasenv subst restrictions t =
                 ms, i-1, i::restrictions_for_n, l)
             l (ms, List.length l, [], [])
          in
+             
           ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
        in
        if restrictions_for_n = [] then
@@ -374,8 +376,8 @@ let delift metasenv subst context n l t =
                   let low_gap = max 0 (shift - shift1) in
                   let high_gap = max 0 (stop1 - stop) in
                   let restrictions = 
-                     HExtlib.list_seq (k+1-shift1) (low_gap + 1) @
-                     HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1)
+                     HExtlib.list_seq (*max 1 (k+1-shift1)*) (k+1) (low_gap + 1) @
+                     HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1) 
                   in
                     let metasenv, subst, newmeta = 
                        restrict metasenv subst i restrictions 
@@ -402,9 +404,9 @@ let delift metasenv subst context n l t =
                   assert (List.length cctx = newlc_len);
                     (metasenv, subst), meta
                   
-              | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
+              | NCic.Irl _, NCic.Irl _ when shift = k -> ms, orig
               | NCic.Irl _, NCic.Irl _ ->
-                   ms, NCic.Meta (i, (max 0 (shift1 - shift), lc1))
+                   ms, NCic.Meta (i, (max 0 (shift1 - shift + k), lc1))
               | _ ->
                   let lc1 = NCicUtils.expand_local_context lc1 in
                   let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in
@@ -456,7 +458,8 @@ let delift metasenv subst context n l t =
       let l = List.map (NCicSubstitution.lift shift) lc in
        if
          List.exists
-          (fun t -> NCicUntrusted.metas_of_term subst context t = [])
+          (fun t -> 
+                  NCicUntrusted.metas_of_term subst context t = [])
             l
        then
         raise (Uncertain msg)
@@ -464,146 +467,6 @@ let delift metasenv subst context n l t =
         raise (MetaSubstFailure msg)
 ;;
 
-(*
-(* delifts a term t of n levels strating from k, that is changes (Rel m)
- * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
- *)
-let delift_rels_from subst metasenv k n =
- let rec liftaux subst metasenv k =
-  let module C = Cic in
-   function
-      C.Rel m as t ->
-       if m < k then
-        t, subst, metasenv
-       else if m < k + n then
-         raise DeliftingARelWouldCaptureAFreeVariable
-       else
-        C.Rel (m - n), subst, metasenv
-    | C.Var (uri,exp_named_subst) ->
-       let exp_named_subst',subst,metasenv = 
-        List.fold_right
-         (fun (uri,t) (l,subst,metasenv) ->
-           let t',subst,metasenv = liftaux subst metasenv k t in
-            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
-       in
-        C.Var (uri,exp_named_subst'),subst,metasenv
-    | C.Meta (i,l) ->
-        (try
-          let (_, t,_) = lookup_subst i subst in
-           liftaux subst metasenv k (CicSubstitution.subst_meta l t)
-         with CicUtil.Subst_not_found _ -> 
-          let l',to_be_restricted,subst,metasenv =
-           let rec aux con l subst metasenv =
-            match l with
-               [] -> [],[],subst,metasenv
-             | he::tl ->
-                let tl',to_be_restricted,subst,metasenv =
-                 aux (con + 1) tl subst metasenv in
-                let he',more_to_be_restricted,subst,metasenv =
-                 match he with
-                    None -> None,[],subst,metasenv
-                  | Some t ->
-                     try
-                      let t',subst,metasenv = liftaux subst metasenv k t in
-                       Some t',[],subst,metasenv
-                     with
-                      DeliftingARelWouldCaptureAFreeVariable ->
-                       None,[i,con],subst,metasenv
-                in
-                 he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
-           in
-            aux 1 l subst metasenv in
-          let metasenv,subst = restrict subst to_be_restricted metasenv in
-           C.Meta(i,l'),subst,metasenv)
-    | C.Sort _ as t -> t,subst,metasenv
-    | C.Implicit _ as t -> t,subst,metasenv
-    | C.Cast (te,ty) ->
-       let te',subst,metasenv = liftaux subst metasenv k te in
-       let ty',subst,metasenv = liftaux subst metasenv k ty in
-        C.Cast (te',ty'),subst,metasenv
-    | C.Prod (n,s,t) ->
-       let s',subst,metasenv = liftaux subst metasenv k s in
-       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
-        C.Prod (n,s',t'),subst,metasenv
-    | C.Lambda (n,s,t) ->
-       let s',subst,metasenv = liftaux subst metasenv k s in
-       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
-        C.Lambda (n,s',t'),subst,metasenv
-    | C.LetIn (n,s,ty,t) ->
-       let s',subst,metasenv = liftaux subst metasenv k s in
-       let ty',subst,metasenv = liftaux subst metasenv k ty in
-       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
-        C.LetIn (n,s',ty',t'),subst,metasenv
-    | C.Appl l ->
-       let l',subst,metasenv =
-        List.fold_right
-         (fun t (l,subst,metasenv) ->
-           let t',subst,metasenv = liftaux subst metasenv k t in
-            t'::l,subst,metasenv) l ([],subst,metasenv) in
-       C.Appl l',subst,metasenv
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst',subst,metasenv = 
-        List.fold_right
-         (fun (uri,t) (l,subst,metasenv) ->
-           let t',subst,metasenv = liftaux subst metasenv k t in
-            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
-       in
-        C.Const (uri,exp_named_subst'),subst,metasenv
-    | C.MutInd (uri,tyno,exp_named_subst) ->
-       let exp_named_subst',subst,metasenv = 
-        List.fold_right
-         (fun (uri,t) (l,subst,metasenv) ->
-           let t',subst,metasenv = liftaux subst metasenv k t in
-            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
-       in
-        C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
-    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-       let exp_named_subst',subst,metasenv = 
-        List.fold_right
-         (fun (uri,t) (l,subst,metasenv) ->
-           let t',subst,metasenv = liftaux subst metasenv k t in
-            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
-       in
-        C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
-    | C.MutCase (sp,i,outty,t,pl) ->
-       let outty',subst,metasenv = liftaux subst metasenv k outty in
-       let t',subst,metasenv = liftaux subst metasenv k t in
-       let pl',subst,metasenv =
-        List.fold_right
-         (fun t (l,subst,metasenv) ->
-           let t',subst,metasenv = liftaux subst metasenv k t in
-            t'::l,subst,metasenv) pl ([],subst,metasenv)
-       in
-        C.MutCase (sp,i,outty',t',pl'),subst,metasenv
-    | C.Fix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl,subst,metasenv =
-        List.fold_right
-         (fun (name, i, ty, bo) (l,subst,metasenv) ->
-           let ty',subst,metasenv = liftaux subst metasenv k ty in
-           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
-            (name,i,ty',bo')::l,subst,metasenv
-         ) fl ([],subst,metasenv)
-       in
-        C.Fix (i, liftedfl),subst,metasenv
-    | C.CoFix (i, fl) ->
-       let len = List.length fl in
-       let liftedfl,subst,metasenv =
-        List.fold_right
-         (fun (name, ty, bo) (l,subst,metasenv) ->
-           let ty',subst,metasenv = liftaux subst metasenv k ty in
-           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
-            (name,ty',bo')::l,subst,metasenv
-         ) fl ([],subst,metasenv)
-       in
-        C.CoFix (i, liftedfl),subst,metasenv
- in
-  liftaux subst metasenv k
-
-let delift_rels subst metasenv n t =
-  delift_rels_from subst metasenv 1 n t
-*) 
-
 let mk_meta ?name metasenv context ty = 
   match ty with
   | `Typeless ->

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index eb7b136c28f3ba948c9048a5f247241614181499..2dce2a4a70f0dad2de5ce0738c7f13b339043f41 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -48,16 +48,18 @@ let exp_implicit metasenv context expty =
 
 let force_to_sort metasenv subst context t =
   match NCicReduction.whd ~subst context t with
-  | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> 
+  | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as t -> 
      metasenv, subst, t
-  | C.Meta (i,(_,lc)) as t ->
+  | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> 
+     metasenv, subst, C.Meta(i,(0,C.Irl 0))
+  | C.Meta (i,(_,lc)) ->
      let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-     let metasenv, subst, _ = 
+     let metasenv, subst, newmeta = 
        if len > 0 then
          NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) 
-       else metasenv, subst, 0
+       else metasenv, subst, i
      in
-     metasenv, subst, t
+     metasenv, subst, C.Meta (newmeta,(0,C.Irl 0))
   | C.Sort _ -> metasenv, subst, t 
   | _ -> assert false
 ;;
@@ -73,9 +75,9 @@ let sort_of_prod
    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
         metasenv, subst, C.Sort (C.Type (u1@u2)) 
    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, t2
-   | C.Meta _, C.Sort _
-   | C.Meta _, C.Meta _
-   | C.Sort _, C.Meta  _ -> metasenv, subst, t2
+   | C.Meta _, C.Sort _ 
+   | C.Meta _, C.Meta (_,(_,_))
+   | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, t2 
    | x, (C.Sort _ | C.Meta _) | _, x -> 
       let y, context, orig = 
         if x == t1 then s, context, orig_s 
@@ -96,10 +98,9 @@ let check_allowed_sort_elimination localise r orig =
    let rec aux metasenv subst context ind arity1 arity2 =
      (*D*)inside 'S'; try let rc = 
      let arity1 = NCicReduction.whd ~subst context arity1 in
-     pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " ... " ^
-        NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nNEV:"^
-NCicPp.ppmetasenv ~subst metasenv
-));
+     pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ "   elimsto   " ^
+        NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
+        NCicPp.ppmetasenv ~subst metasenv));
      match arity1 with
      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
         let metasenv, meta, _ = 
@@ -166,6 +167,7 @@ let rec typeof
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
+    pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
     let metasenv, subst, t, infty = 
     match t with
     | C.Rel n ->
@@ -307,6 +309,8 @@ let rec typeof
       NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
     | C.Match _ -> assert false
     in
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
+         NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty metasenv subst context orig t infty expty
     (*D*)in outside(); rc with exc -> outside (); raise exc
   in

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 202e68e4c86c3d056a8914451a70b6c4b25aae13..d5cf3892270f3c05c81c9d4decb82e268c0b65cf 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -85,7 +85,8 @@ let fix_sorts swap metasenv subst context meta t =
     | NCic.Sort (NCic.Type u) as orig ->
         if swap then
          match NCicEnvironment.sup u with
-         | None ->  raise (fail_exc metasenv subst context meta t)
+         | None -> prerr_endline "no sup for" ;
+            raise (fail_exc metasenv subst context meta t)
          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
         else
          NCic.Sort (NCic.Type (
@@ -161,6 +162,8 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
+         pp (lazy(string_of_int n ^ " :=?= "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
   let unify test_eq_only m s c t1 t2 = 
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
@@ -169,23 +172,38 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   let metasenv, subst, t = 
     match ty with 
     | NCic.Implicit (`Typeof _) -> 
-       metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
+       metasenv,subst, t
+         (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
     | _ ->
-       pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+       pp (lazy (
+         "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
+          NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
+          NCicPp.ppmetasenv ~subst metasenv));
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
-         with NCicTypeChecker.TypeCheckerFailure _ -> 
+         with 
+         | NCicTypeChecker.AssertFailure msg -> 
+           (pp (lazy "fine typeof (fallimento)");
            let ft = 
             fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
            in
-           if ft == t then assert false
+           if ft == t then 
+             (prerr_endline ( ("ILLTYPED: " ^ 
+                NCicPp.ppterm ~metasenv ~subst ~context t
+            ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
+            NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
+            NCicPp.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.TypeCheckerFailure _ -> 
-              assert false
+            with NCicTypeChecker.AssertFailure _ -> 
+              assert false)
+         | NCicTypeChecker.TypeCheckerFailure msg ->
+              pp msg; assert false
        in
        let lty = NCicSubstitution.subst_meta lc ty in
        pp (lazy("On the types: " ^
@@ -195,11 +213,22 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
        let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
        metasenv, subst, t
   in
+         pp (lazy(string_of_int n ^ " := 111 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
-    with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
-    |    NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
+    with NCicMetaSubst.Uncertain msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (Uncertain msg)
+    | NCicMetaSubst.MetaSubstFailure msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (UnificationFailure msg)
   in
+         pp (lazy(string_of_int n ^ " := 222 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context:ctx t
+         ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv
+         
+         ));
   (* Unifying the types may have already instantiated n. *)
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
@@ -266,10 +295,12 @@ and unify test_eq_only metasenv subst context t1 t2 =
                   metasenv, subst, i::to_restrict, i-1)
              l1 l2 (metasenv, subst, [], List.length l1)
            in
-           let metasenv, subst, _ = 
-             NCicMetaSubst.restrict metasenv subst n1 to_restrict
-           in
-             metasenv, subst
+           if to_restrict <> [] then
+             let metasenv, subst, _ = 
+               NCicMetaSubst.restrict metasenv subst n1 to_restrict
+             in
+               metasenv, subst
+           else metasenv, subst
           with 
            | Invalid_argument _ -> assert false
            | NCicMetaSubst.MetaSubstFailure msg ->