the trie indexes terms up to 10 nested applications and skips applications with more...

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

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 225c1898e022f78fa5758e5d51c83e9b8e2afa31..c3765f3f0261eb092bbb93e87c8e12df6d0a9bc7 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -20,23 +20,33 @@ module Ref = NReference
 
 let debug = ref false;;
 let indent = ref "";;
+let times = ref [];;
 let pp s =
  if !debug then
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
- else 
-  ()
 ;;
 let inside c =
- indent := !indent ^ String.make 1 c;
- if !debug then prerr_endline ("{{{" ^ !indent ^ " ")
+ 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 prerr_endline "}}}";
- if not ok then pp (lazy "exception raised!");
- try
-  indent := String.sub !indent 0 (String.length !indent -1)
- with
-  Invalid_argument _ -> indent := "??"; ()
+ 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
 ;;
 
 
@@ -47,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")))
@@ -165,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 -> 
@@ -489,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: " ^ 
@@ -515,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) ->
@@ -579,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 *)