...

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 24ab7b4afbf1129cafb2d0462a169bf26ca42913..d3c86d2816c2c9bd050bbe1b336d033d95e4c8dd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -72,13 +72,23 @@ let indent = ref "";;
 let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
-(*
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
-*)
 
-let pp _ = ();;
+(* let pp _ = ();; *)
+
+let fix_sorts metasenv subst context meta t =
+  let rec aux () = function
+    | NCic.Sort (NCic.Type u) as orig ->
+       (match NCicEnvironment.sup u with
+       | None ->  raise (fail_exc metasenv subst context meta t)
+       | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1))
+    | NCic.Meta _ as orig -> orig
+    | t -> NCicUtils.map (fun _ _ -> ()) () aux t
+  in
+    aux () t
+;;
 
 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
@@ -142,28 +152,44 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
 (* (*D*)  in outside (); rc with exn -> outside (); raise exn *)
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
-(* (*D*)  inside 'I'; try let rc =  *)
+ (*D*)  inside 'I'; try let rc =  
   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
   in
+  let fix_sorts t = 
+    if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t
+    else 
+      NCic.Sort (NCic.Type (
+        match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ ->
+                assert false))
+  in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let metasenv, subst = 
+  let metasenv, subst, t = 
     match ty with 
-    | NCic.Implicit (`Typeof _) -> metasenv, subst
+    | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t
     | _ ->
-       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
+       pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+       let t, ty_t = 
+         try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
+         with NCicTypeChecker.TypeCheckerFailure _ -> 
+           let ft = fix_sorts t in
+           if ft == t then assert false else
+            try 
+              pp (lazy ("typeof: " ^ 
+                NCicPp.ppterm ~metasenv ~subst ~context ft));
+              ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
+            with NCicTypeChecker.TypeCheckerFailure msg -> 
+              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
+              prerr_endline (Lazy.force msg);
+              assert false
        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)); 
-       unify test_eq_only metasenv subst context lty ty_t 
+       let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
+       metasenv, subst, t
   in
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
@@ -187,16 +213,14 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in
     metasenv, subst
-(* (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+ (*D*)  in outside(); rc with exn -> outside (); raise exn 
 
 and unify test_eq_only metasenv subst context t1 t2 =
-(* (*D*) inside 'U'; try let rc = *)
+ (*D*) inside 'U'; try let rc = 
    let fo_unif test_eq_only metasenv subst t1 t2 =
-(*    (*D*) inside 'F'; try let rc =  *)
-(*
+    (*D*) inside 'F'; try let rc =  
      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
          NCicPp.ppterm ~metasenv ~subst ~context t2));
-*)
      if t1 === t2 then
        metasenv, subst
      else
@@ -380,7 +404,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
                raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
-(*     (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+     (*D*)  in outside(); rc with exn -> outside (); raise exn 
     in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
@@ -411,7 +435,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
     let rec unif_machines metasenv subst = 
       function
       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
-(*     (*D*) inside 'M'; try let rc = *)
+     (*D*) inside 'M'; try let rc = 
 (*
          pp (lazy((if are_normal then "*" else " ") ^ " " ^
            NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
@@ -446,7 +470,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
         try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
         with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
            unif_machines metasenv subst (small_delta_step m1 m2)
-(*      (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+      (*D*)  in outside(); rc with exn -> outside (); raise exn 
      in
      try fo_unif test_eq_only metasenv subst t1 t2
      with UnificationFailure msg | Uncertain msg as exn -> 
@@ -456,7 +480,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn
-(* (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+ (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
 let unify =