unification pps can be activated by the menu debug

[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 d48dfaf460a4967a02aada9d8f7ee5f8bdecd03c..5353363d507bcbac84e6e939daa89dc0a343c038 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -78,20 +78,20 @@ let eta_reduce subst t =
 module C = NCic;;
 module Ref = NReference;;
 
-let debug = false;;
+let debug = ref false;;
 let indent = ref "";;
-let pp =
- if debug then
-  fun s -> prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+let pp s =
+ if !debug then
+  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
  else 
-  fun _ -> ()
+  ()
 ;;
 let inside c =
  indent := !indent ^ String.make 1 c;
- if debug then prerr_endline ("{{{" ^ !indent ^ " ")
+ if !debug then prerr_endline ("{{{" ^ !indent ^ " ")
 ;;
 let outside ok =
- if debug then prerr_endline "}}}";
+ if !debug then prerr_endline "}}}";
  if not ok then pp (lazy "exception raised!");
  try
   indent := String.sub !indent 0 (String.length !indent -1)
@@ -135,10 +135,9 @@ let is_locked n subst =
    with NCicUtils.Subst_not_found _ -> false
 ;;
 
-let rec mk_irl =
- function
-    0 -> []
-  | n -> NCic.Rel n :: mk_irl (n-1)
+let rec mk_irl stop base =
+  if base > stop then []
+  else (NCic.Rel base) :: mk_irl stop (base+1) 
 ;;
 
 (* the argument must be a term in whd *)
@@ -168,15 +167,16 @@ let rec lambda_intros rdb metasenv subst context t args =
        metasenv, subst, bo
    | (arg,ty)::tail ->
        pp(lazy("arg{ " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  ":" ^
+         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  " : " ^
          NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty));
        let metasenv, subst, telescopic_ty = 
          if processed_args = [] then metasenv, subst, ty else
          let _ = pp(lazy("delift")) in
-         delift_type_wrt_terms rdb metasenv subst context_of_args ty 
-           (List.rev processed_args)
+         delift_type_wrt_terms rdb metasenv subst context 
+           (NCicSubstitution.lift n ty)
+           (List.map (NCicSubstitution.lift n) (List.rev processed_args))
        in
-       pp(lazy("arg}"));
+       pp(lazy("arg} "^NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty));
        let name = "HBeta"^string_of_int n in
        let metasenv, subst, bo =
         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
@@ -328,6 +328,21 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
   with NCicUtils.Subst_not_found _ -> 
+    let metasenv, tags = 
+      let rec aux = function
+        | NCic.Meta (j,lc) -> 
+            (try 
+              let _, _, t, _ = NCicUtils.lookup_subst j subst in
+              aux (NCicSubstitution.subst_meta lc t)
+            with NCicUtils.Subst_not_found _ -> 
+              let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in
+              let metasenv = List.remove_assoc j metasenv in
+              let tags = tags @ tags' in
+              (j, (tags, ctx, ty)) :: metasenv, tags)
+        | _ -> metasenv, tags
+      in 
+        aux t
+    in
     (* by cumulativity when unify(?,Type_i) 
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (tags, ctx, t, ty)) :: subst in
@@ -596,11 +611,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
     in
     let try_hints metasenv subst t1 t2 (* exc*) =
     (*D*) inside 'H'; try let rc =  
-(*
-      prerr_endline ("\nProblema:\n" ^
+     pp(lazy ("\nProblema:\n" ^
         NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
-        NCicPp.ppterm ~metasenv ~subst ~context t2);
-*)
+        NCicPp.ppterm ~metasenv ~subst ~context t2));
       let candidates = 
         NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
       in
@@ -628,6 +641,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                      unify rdb test_eq_only metasenv subst context x y)
                   (metasenv, subst) premises
               in
+              pp(lazy("FUNZIONA!"));
               Some (metasenv, subst)
      (*D*)  in outside true; rc with exn -> outside false; raise exn 
             with
@@ -716,18 +730,27 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           | UnificationFailure _ -> raise (UnificationFailure msg)
           | Uncertain _ -> raise exn)
      | Uncertain msg as exn -> 
-       match try_hints metasenv subst t1 t2 with
+(*
+       prerr_endline "PROBLEMA";
+       prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1);
+       prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2);
+*)
+       let (t1,_ as t1m),(t2,_ as t2m) = put_in_whd (0,[],t1,[]) (0,[],t2,[]) in
+       match 
+         try_hints metasenv subst 
+           (NCicReduction.unwind t1) (NCicReduction.unwind t2) 
+       with
        | Some x -> x
        | None -> 
           try 
-            unif_machines metasenv subst 
-             (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
+            unif_machines metasenv subst (t1m, t2m)
           with 
           | UnificationFailure _ -> raise (UnificationFailure msg)
           | Uncertain _ -> raise exn
  (*D*)  in outside true; rc with exn -> outside false; raise exn 
 
 and delift_type_wrt_terms rdb metasenv subst context t args =
+  let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
   let (metasenv, subst), t =
    try
     NCicMetaSubst.delift 
@@ -738,8 +761,7 @@ and delift_type_wrt_terms rdb metasenv subst context t args =
            with UnificationFailure _ | Uncertain _ -> None
          in
          indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx (args @ 
-        List.rev (mk_irl (List.length context)))) t
+      metasenv subst context 0 (0,NCic.Ctx lc) t
    with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t
   in
    metasenv, subst, t