prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 552e3d30b21898eb7596194b6a7c3f7d4c263d8f..b71e908856ba017df051a5d244f7ab39a1fd9035 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -73,9 +73,6 @@ let refine metasenv context term ugraph =
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) msg);
           Ko,ugraph
-      | CicUnification.UnificationFailure s -> 
-        prerr_endline ("PASSADI QUI: " ^ s);
-          raise ( CicUnification.UnificationFailure s )
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   try
@@ -253,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 "; "
@@ -268,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 =
@@ -282,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
@@ -312,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
@@ -328,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
@@ -457,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))
@@ -474,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));
@@ -510,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)
@@ -611,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