X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b71e908856ba017df051a5d244f7ab39a1fd9035;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=bb70ce279bdaf2ba376a784a666d52c7d758c5ef;hpb=722256712b8b0c6acc08a36fa6c9cde8cc5ecc4b;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index bb70ce279..b71e90885 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -73,13 +73,6 @@ let refine metasenv context term ugraph =
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) msg);
           Ko,ugraph
-      | CicUniv.UniverseInconsistency s ->
-         prerr_endline (
-           "INTERPRETAZIONE FALLITA PER UNIVERSE INCONSISTENCY:\n" ^ s);
-           (* non mi e' chiaro se debba essere wrappata dal typechecker o dal
-            * refiner, in ogni caso non andrebbe qui 
-            *)
-         Ko, ugraph
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   try
@@ -257,7 +250,7 @@ let interpretate ~context ~env ast =
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
 (*
-                prerr_endline (sprintf
+                debug_print (sprintf
                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
                   (CicPp.ppterm t)
                   (String.concat "; "
@@ -272,6 +265,8 @@ let interpretate ~context ~env ast =
              CicEnvironment.CircularDependency _ -> 
                raise DisambiguateChoices.Invalid_choice))
     | CicAst.Implicit -> Cic.Implicit None
+    | CicAst.UserInput -> Cic.Implicit (Some `Hole)
+(*    | CicAst.UserInput -> assert false*)
     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
     | CicAst.Meta (index, subst) ->
         let cic_subst =
@@ -286,7 +281,6 @@ let interpretate ~context ~env ast =
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
-    | CicAst.UserInput -> assert false
   and aux_option loc context = function
     | None -> Cic.Implicit (Some `Type)
     | Some term -> aux loc context term
@@ -316,6 +310,10 @@ let domain_of_term ~context ast =
     | CicAst.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
+        let get_first_constructor = function
+          | [] -> []
+          | ((head, _), _) :: _ -> [ Id head ]
+        in
         let do_branch ((head, args), term) =
           let (term_context, args_domain) =
             List.fold_left
@@ -332,7 +330,9 @@ let domain_of_term ~context ast =
           List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
         in
         branches_dom @ outtype_dom @ term_dom @
-        (match indty_ident with None -> [] | Some ident -> [ Id ident ])
+        (match indty_ident with
+         | None -> get_first_constructor branches
+         | Some ident -> [ Id ident ])
     | CicAst.LetIn ((var, typ), body, where) ->
         let body_dom = aux loc context body in
         let type_dom = aux_option loc context typ in
@@ -461,8 +461,8 @@ module Make (C: Callbacks) =
              try
                CicUtil.term_of_uri uri
              with exn ->
-               prerr_endline uri;
-               prerr_endline (Printexc.to_string exn);
+               debug_print uri;
+               debug_print (Printexc.to_string exn);
                assert false
             in
            fun _ _ _ -> term))
@@ -478,6 +478,7 @@ module Make (C: Callbacks) =
           (function None -> Cic.Anonymous | Some (name, _) -> name)
           context
       in
+      debug_print ("TERM IS: " ^ (CicAstPp.pp_term term));
       let term_dom = domain_of_term ~context:disambiguate_context term in
       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain term_dom));
@@ -514,7 +515,7 @@ module Make (C: Callbacks) =
               (fun dom_item ->
                 try
                   let len = List.length (lookup_choices dom_item) in
-                  prerr_endline (sprintf "BENCHMARK %s: %d"
+                  debug_print (sprintf "BENCHMARK %s: %d"
                     (string_of_domain_item dom_item) len);
                   len
                 with No_choices _ -> 0)
@@ -615,7 +616,7 @@ module Make (C: Callbacks) =
 (*
         (if benchmark then
           let res_size = List.length res in
-          prerr_endline (sprintf
+          debug_print (sprintf
             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
             "BENCHMARK:   estimated %.2f")
             !actual_refinements !max_refinements !domain_size res_size