Dama is now in the night benchmarks.

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 0ef14696c5d46c68075698cde0f36070629f072c..54055ebb6478633c47f3e2f952b6f1c11a707c93 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -78,6 +78,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn =
   match exn with
      RefineFailure msg -> RefineFailure (f msg)
    | Uncertain msg -> Uncertain (f msg)
+   | Sys.Break -> raise exn
    | _ -> assert false in
  let loc =
   try
@@ -140,7 +141,7 @@ let is_a_double_coercion t =
       | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
           let sib2,head = last_of tl2 in
           true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
-            (c2::sib2@[Cic.Implicit None])]) 
+            (c2::sib2@[imp])]) 
       | _ -> dummyres)
   | _ -> dummyres
 
@@ -320,8 +321,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
      ugraph
 =
   let rec type_of_aux subst metasenv context t ugraph =
+    let module C = Cic in
+    let module S = CicSubstitution in
+    let module U = UriManager in
     let try_coercion t subst metasenv context ugraph coercion_tgt c =
-      let coerced = Cic.Appl[c;t] in
+      let coerced = C.Appl[c;t] in
       try
         let newt,_,subst,metasenv,ugraph = 
           type_of_aux subst metasenv context coerced ugraph 
@@ -333,9 +337,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       with 
       | RefineFailure _ | Uncertain _ -> None
     in
-    let module C = Cic in
-    let module S = CicSubstitution in
-    let module U = UriManager in
      let (t',_,_,_,_) as res =
       match t with
           (*    function *)
@@ -357,9 +358,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     enrich localization_tbl t
                      (RefineFailure (lazy "Rel to hidden hypothesis"))
              with
-              _ ->
+              Failure _ ->
                enrich localization_tbl t
-                (RefineFailure (lazy "Not a close term")))
+                (RefineFailure (lazy "Not a closed term")))
         | C.Var (uri,exp_named_subst) ->
             let exp_named_subst',subst',metasenv',ugraph1 =
               check_exp_named_subst 
@@ -578,8 +579,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                * Even faster than the previous solution.
                * Moreover the inferred type is closer to the expected one. 
                *)
-              C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
-                subst'',metasenv'',ugraph2
+              C.LetIn (n,s',t'),
+               CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
+               subst'',metasenv'',ugraph2
         | C.Appl (he::((_::_) as tl)) ->
             let he',hetype,subst',metasenv',ugraph1 = 
               type_of_aux subst metasenv context he ugraph 
@@ -1059,6 +1061,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                | Some t,Some (_,C.Def (ct,_)) ->
                    let subst',metasenv',ugraph' = 
                    (try
+prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
                       fo_unif_subst subst context metasenv t ct ugraph
                     with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
                    in
@@ -1174,6 +1177,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (CicPp.ppterm t2''))))
 
   and avoid_double_coercion context subst metasenv ugraph t ty = 
+   if not !pack_coercions then
+    t,ty,subst,metasenv,ugraph
+   else
     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
     if b then
       let source_carr = CoercGraph.source_of c2 in
@@ -1214,11 +1220,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                | RefineFailure s | Uncertain s -> 
                    debug_print s;debug_print (lazy "goon\n");
                    try 
+                     let old_pack_coercions = !pack_coercions in
                      pack_coercions := false; (* to avoid diverging *)
                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
                        type_of_aux subst metasenv context c1_c2_implicit ugraph 
                      in
-                     pack_coercions := true;
+                     pack_coercions := old_pack_coercions;
                      let b, _, _, _, _ = 
                        is_a_double_coercion refined_c1_c2_implicit 
                      in 
@@ -1463,8 +1470,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                            context ^ " has type " ^
                           CicMetaSubst.ppterm_in_context subst hety
                            context ^ " but is here used with type " ^
-                          CicMetaSubst.ppterm_in_context subst s context ^
-                           "\nReason: " ^ Printexc.to_string exn))) exn
+                          CicMetaSubst.ppterm_in_context subst s context
+                           (* "\nReason: " ^ Printexc.to_string exn*)))) exn
                   (* }}} end coercion stuff *)
                 in
                   eat_prods_and_args pristinemenv metasenv subst context pristinehe he
@@ -1492,7 +1499,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
      else
        (* this (says CSC) is also useful to infer dependent types *)
-       fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+       try
+        fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+       with RefineFailure _ | Uncertain _ as exn ->
+         (* unable to fix arity *)
+          more_args_than_expected localization_tbl 
+            subst he context hetype args_bo_and_ty exn
     in
     let coerced_args,subst,metasenv,he,t,ugraph =
       eat_prods_and_args 
@@ -1724,7 +1736,11 @@ let pack_coercion metasenv ctx t =
        let ctx' = (Some (name,C.Decl so))::ctx in
        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
    | C.LetIn (name,so,dest) -> 
-       let ctx' = Some (name,(C.Def (so,None)))::ctx in
+       let _,ty,metasenv,ugraph =
+        pack_coercions := false;
+        type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
+        pack_coercions := true;
+       let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
    | C.Appl l -> 
       let l = List.map (merge_coercions ctx) l in
@@ -1739,7 +1755,6 @@ let pack_coercion metasenv ctx t =
            try 
              type_of_aux' metasenv ctx t ugraph 
            with RefineFailure _ | Uncertain _ -> 
-             prerr_endline (CicPp.ppterm t);
              t, t, [], ugraph 
          in
          insert_coercions := old_insert_coercions;