X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=2775aed3b97428354897113d441a2c48c69e0f50;hb=bb49c457d64878ed9611656f620548b5151e5dbd;hp=0f169fc27ee65da0cd07920b10870fbf99ade62c;hpb=90f02ec7eb997c4d4961dabcfce04d26bb77ca91;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 0f169fc27..2775aed3b 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -66,8 +66,8 @@ let refine metasenv context term ugraph =
 	CicRefine.type_of_aux' metasenv context term ugraph in
 	(Ok (term', metasenv')),ugraph1
     with
-      | CicRefine.Uncertain _ ->
-          debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+      | CicRefine.Uncertain s ->
+          debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
           Uncertain,ugraph
       | CicRefine.RefineFailure msg ->
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
@@ -250,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 "; "
@@ -265,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 =
@@ -279,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
@@ -309,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
@@ -325,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
@@ -454,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))
@@ -508,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)
@@ -609,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