X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=c3765f3f0261eb092bbb93e87c8e12df6d0a9bc7;hb=d00e19c7000a00659ffd609ef79675eb0f010659;hp=b84c23aae9db4cb27c8ad6d64cb5317d08c75207;hpb=1b1a51a03ebfc8b16df3731729f857377183425f;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index b84c23aae..c3765f3f0 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -18,16 +18,37 @@ exception AssertFailure of string Lazy.t;;
 module C = NCic
 module Ref = NReference
 
+let debug = ref false;;
 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 = 
+let times = ref [];;
+let pp s =
+ if !debug then
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
-;;  
+;;
+let inside c =
+ if !debug then
+  begin
+   let time1 = Unix.gettimeofday () in
+   indent := !indent ^ String.make 1 c;
+   times := time1 :: !times;
+   prerr_endline ("{{{" ^ !indent ^ " ")
+  end
+;;
+let outside ok =
+ if !debug then
+  begin
+   let time2 = Unix.gettimeofday () in
+   let time1 =
+    match !times with time1::tl -> times := tl; time1 | [] -> assert false in
+   prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+   if not ok then prerr_endline "exception raised!";
+   try
+    indent := String.sub !indent 0 (String.length !indent -1)
+   with
+    Invalid_argument _ -> indent := "??"; ()
+ end
+;;
 
-let pp _ = ();;
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
@@ -36,14 +57,34 @@ let wrap_exc msg = function
   | e -> raise e
 ;;
 
-let exp_implicit ~localise metasenv context expty t =
- let foo x = match expty with Some t -> `WithType t | None -> x in
+let exp_implicit rdb ~localise metasenv subst context expty t =
+ let foo x = function Some t -> `WithType t | None -> x in
  function      
-  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
-  | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
-  | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+  | `Closed ->
+      let metasenv,subst,expty =
+       match expty with
+          None -> metasenv,subst,None
+        | Some typ ->
+           let (metasenv,subst),typ =
+            try
+             NCicMetaSubst.delift
+              ~unify:(fun m s c t1 t2 ->
+                try Some (NCicUnification.unify rdb m s c t1 t2)
+                with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
+              metasenv subst context 0 (0,NCic.Irl 0) typ
+            with
+              NCicMetaSubst.MetaSubstFailure _
+            | NCicMetaSubst.Uncertain _ ->
+               raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type")))
+
+           in
+            metasenv,subst,Some typ
+      in
+       NCicMetaSubst.mk_meta metasenv [] (foo `Term expty),subst
+  | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type expty),subst
+  | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term expty),subst
   | `Tagged s ->
-      NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term)
+      NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term expty),subst
   | `Vector ->
       raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
        "can only be used in argument position")))
@@ -93,7 +134,7 @@ let check_allowed_sort_elimination rdb localise r orig =
         with exc -> raise (wrap_exc (lazy (localise orig, 
           "Sort elimination not allowed ")) exc))
      | _ -> assert false
-     (*D*)in outside(); rc with exc -> outside (); raise exc
+     (*D*)in outside true; rc with exc -> outside false; raise exc
    in
     aux
 ;;
@@ -118,7 +159,7 @@ let rec typeof rdb
              let metasenv, subst =
     (*D*)inside 'U'; try let rc = 
                NCicUnification.unify rdb metasenv subst context infty expty 
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
              in
              metasenv, subst, t, expty
            with 
@@ -127,7 +168,7 @@ let rec typeof rdb
              try_coercions rdb ~localise 
                metasenv subst context t orig infty expty true exc)
     | None -> metasenv, subst, t, infty
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
   in
   let rec typeof_aux metasenv subst context expty = 
     fun t as orig -> 
@@ -154,8 +195,8 @@ let rec typeof rdb
               raise (RefineFailure (lazy (localise t, Lazy.force msg)))
          | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
     | C.Implicit infos -> 
-         let metasenv,_,t,ty =
-           exp_implicit ~localise metasenv context expty t infos
+         let (metasenv,_,t,ty),subst =
+           exp_implicit rdb ~localise metasenv subst context expty t infos
          in
           metasenv, subst, t, ty 
     | C.Meta (n,l) as t -> 
@@ -365,7 +406,7 @@ let rec typeof rdb
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty true true metasenv subst context orig t infty expty
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
   in
     typeof_aux metasenv subst context expty term
 
@@ -478,7 +519,9 @@ and guess_name subst ctx ty =
 
 and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args =
   (*D*)inside 'E'; try let rc = 
-  let rec aux metasenv subst args_so_far he ty_he = function 
+  let rec aux metasenv subst args_so_far he ty_he xxx =
+  (*D*)inside 'V'; try let rc = 
+   match xxx with
   | [] ->
      let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
      pp(lazy("FORCE FINAL APPL: " ^ 
@@ -504,7 +547,10 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
            aux metasenv subst args_so_far he ty_he
             (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl)
           with
-           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc)))
+           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
+     | RefineFailure msg when not (has_some_more_pis ty_he) ->
+        (* instantiating the head could change the has_some_more_pis flag *)
+        raise (Uncertain msg))
   | arg::tl ->
       match NCicReduction.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
@@ -568,6 +614,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
                (List.length args) (List.length args_so_far))))
           in
            aux metasenv subst [] newhead newheadty (arg :: tl)
+  (*D*)in outside true; rc with exc -> outside false; raise exc
   in
    (* We need to reverse the order of the new created metas since they
       are pushed on top of the metasenv in the wrong order *)
@@ -578,7 +625,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
     List.partition (fun (i,_) -> i <= highest_meta) metasenv
    in
     (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty
-  (*D*)in outside(); rc with exc -> outside (); raise exc
+  (*D*)in outside true; rc with exc -> outside false; raise exc
 ;;
 
 let rec first f l1 l2 =