X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=8bd26637047900ac5b58733437df8fbd7584816a;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=c8376078285100419e9ba228cadce6fc60170de7;hpb=08affd483123f36da15b38c89d58a0477bc96244;p=helm.git

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index c83760782..8bd266370 100644
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -51,8 +51,8 @@ type 'a disambiguator_input = string * int * 'a
 type domain = domain_tree list
 and domain_tree = Node of Stdpp.location list * domain_item * domain
 
-let mono_uris_callback ~selection_mode ?ok
-          ?(enable_button_for_non_vars = true) ~title ~msg ~id =
+let mono_uris_callback ~selection_mode:_ ?ok:(_)
+          ?enable_button_for_non_vars:(_ = true) ~title:(_) ~msg:(_) ~id:(_) =
  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
       "matita.auto_disambiguation"
  then
@@ -69,7 +69,7 @@ let set_choose_interp_callback f = _choose_interp_callback := f
 
 let interactive_user_uri_choice = !_choose_uris_callback
 let interactive_interpretation_choice interp = !_choose_interp_callback interp
-let input_or_locate_uri ~(title:string) ?id () = None
+let input_or_locate_uri ~title:(_:string) ?id:(_) () = None
   (* Zack: I try to avoid using this callback. I therefore assume that
   * the presence of an identifier that can't be resolved via "locate"
   * query is a syntax error *)
@@ -139,7 +139,7 @@ let resolve ~env ~mk_choice (item: domain_item) arg =
    match snd (mk_choice (Environment.find item env)), arg with
       `Num_interp f, `Num_arg n -> f n
     | `Sym_interp f, `Args l -> f l
-    | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f []
+    | `Sym_interp f, `Num_arg _n -> (* Implicit number! *) f []
     | _,_ -> assert false
   with Not_found -> 
     failwith ("Domain item not found: " ^ 
@@ -149,7 +149,7 @@ let resolve ~env ~mk_choice (item: domain_item) arg =
 let find_in_context name context =
   let rec aux acc = function
     | [] -> raise Not_found
-    | Some hd :: tl when hd = name -> acc
+    | Some hd :: _tl when hd = name -> acc
     | _ :: tl ->  aux (acc + 1) tl
   in
   aux 1 context
@@ -231,7 +231,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
         | _ :: tl -> get_first_constructor tl in
       let do_branch =
        function
-          Ast.Pattern (head, _, args), term ->
+          Ast.Pattern (_head, _, args), term ->
            let (term_context, args_domain) =
              List.fold_left
                (fun (cont, dom) (name, typ) ->
@@ -261,34 +261,6 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
       let where_dom =
         domain_of_term ~loc ~context:(string_of_name var :: context) where in
       body_dom @ type_dom @ where_dom
-  | Ast.LetRec (kind, defs, where) ->
-      let add_defs context =
-        List.fold_left
-          (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
-          ) context defs in
-      let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
-      let defs_dom =
-        List.fold_left
-          (fun dom (params, (_, typ), body, _) ->
-            let context' =
-             add_defs
-              (List.fold_left
-                (fun acc (var,_) -> string_of_name var :: acc)
-                context params)
-            in
-            List.rev
-             (snd
-               (List.fold_left
-                (fun (context,res) (var,ty) ->
-                  string_of_name var :: context,
-                  domain_of_term_option ~loc ~context ty @ res)
-                (add_defs context,[]) params))
-            @ dom
-            @ domain_of_term_option ~loc ~context:context' typ
-            @ domain_of_term ~loc ~context:context' body
-          ) [] defs
-      in
-      defs_dom @ where_dom
   | Ast.Ident (name, subst) ->
       (try
         (* the next line can raise Not_found *)
@@ -312,8 +284,8 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.NRef _ -> []
   | Ast.NCic _ -> []
   | Ast.Implicit _ -> []
-  | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
-  | Ast.Meta (index, local_context) ->
+  | Ast.Num (_num, i) -> [ Node ([loc], Num i, []) ]
+  | Ast.Meta (_index, local_context) ->
       List.fold_left
        (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
        [] local_context
@@ -331,15 +303,19 @@ and domain_of_term_option ~loc ~context = function
 let domain_of_term ~context term = 
  uniq_domain (domain_of_term ~context term)
 
+let domain_of_term_option ~context = function
+   | None      -> []
+   | Some term -> domain_of_term ~context term
+
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
-   | Ast.Theorem (_,_,ty,bo,_) ->
+   | Ast.Theorem (_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []
         | Some bo -> domain_of_term [] bo)
-   | Ast.Inductive (params,tyl) ->
+   | Ast.Inductive (params,tyl,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->
@@ -359,7 +335,7 @@ let domain_of_obj ~context ast =
                List.map
                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
                 tyl)
-   | Ast.Record (params,var,ty,fields) ->
+   | Ast.Record (params,var,ty,fields,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->
@@ -376,6 +352,33 @@ let domain_of_obj ~context ast =
           (fun (context,res) (name,ty,_,_) ->
             Some name::context, res @ domain_of_term context ty
           ) (context_w_types,[]) fields)
+   | Ast.LetRec (_kind, defs, _) ->
+       let add_defs context =
+         List.fold_left
+           (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
+           ) context defs in
+       let defs_dom =
+         List.fold_left
+           (fun dom (params, (_, typ), body, _) ->
+             let context' =
+              add_defs
+               (List.fold_left
+                 (fun acc (var,_) -> string_of_name var :: acc)
+                 context params)
+             in
+             List.rev
+              (snd
+                (List.fold_left
+                 (fun (context,res) (var,ty) ->
+                   string_of_name var :: context,
+                   domain_of_term_option ~context ty @ res)
+                 (add_defs context,[]) params))
+             @ dom
+             @ domain_of_term_option ~context:context' typ
+             @ domain_of_term ~context:context' body
+           ) [] defs
+      in
+      defs_dom
 
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
@@ -390,7 +393,7 @@ let domain_diff dom1 dom2 =
           (match elt with
               Symbol (symb',_) when symb = symb' -> true
             | _ -> false)
-       | Num i ->
+       | Num _i ->
           (match elt with
               Num _ -> true
             | _ -> false)
@@ -446,9 +449,14 @@ let disambiguate_thing
    let aliases, todo_dom = 
      let rec aux (aliases,acc) = function 
        | [] -> aliases, acc
-       | (Node (_, item,extra) as node) :: tl -> 
+       | Node (locs, item,extra) :: tl -> 
            let choices = lookup_choices item in
-           if List.length choices <> 1 then aux (aliases, acc@[node]) tl
+           if List.length choices = 0 then
+            (* Quick failure *)
+            raise (NoWellTypedInterpretation (0,[[],[],(lazy (List.hd locs, "No choices for " ^ string_of_domain_item item)),true]))
+           else if List.length choices <> 1 then
+            let aliases,extra = aux (aliases,[]) extra in
+             aux (aliases, acc@[Node (locs,item,extra)]) tl
            else
            let tl = tl @ extra in
            if Environment.mem item aliases then aux (aliases, acc) tl
@@ -456,6 +464,8 @@ let disambiguate_thing
      in
        aux (aliases,[]) todo_dom
    in
+   debug_print
+    (lazy(sprintf "TODO DOM: %s"(string_of_domain todo_dom)));
 
 (*
       (* <benchmark> *)
@@ -538,41 +548,6 @@ in refine_profiler.HExtlib.profile foo ()
                (lazy (List.hd locs,
                  "No choices for " ^ string_of_domain_item item)),
                true]
-(*
-          | [codomain_item] ->
-              (* just one choice. We perform a one-step look-up and
-                 if the next set of choices is also a singleton we
-                 skip this refinement step *)
-              debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
-              let new_env = Environment.add item codomain_item aliases in
-              let new_diff = (item,codomain_item)::diff in
-              let lookup_in_todo_dom,next_choice_is_single =
-               match remaining_dom with
-                  [] -> None,false
-                | (_,he)::_ ->
-                   let choices = lookup_choices he in
-                    Some choices,List.length choices = 1
-              in
-               if next_choice_is_single then
-                aux new_env new_diff lookup_in_todo_dom remaining_dom
-                 base_univ
-               else
-                 (match test_env new_env remaining_dom base_univ with
-                 | Ok (thing, metasenv),new_univ ->
-                     (match remaining_dom with
-                     | [] ->
-                        [ new_env, new_diff, metasenv, thing, new_univ ], []
-                     | _ ->
-                        aux new_env new_diff lookup_in_todo_dom
-                         remaining_dom new_univ)
-                 | Uncertain (loc,msg),new_univ ->
-                     (match remaining_dom with
-                     | [] -> [], [new_env,new_diff,loc,msg,true]
-                     | _ ->
-                        aux new_env new_diff lookup_in_todo_dom
-                         remaining_dom new_univ)
-                 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
-*)
           | _::_ ->
               let mark_not_significant failures =
                 List.map
@@ -595,7 +570,7 @@ in refine_profiler.HExtlib.profile foo ()
                     (inner_dom@remaining_dom@rem_dom) base_univ
                  with
                 | Ok (thing, metasenv,subst,new_univ) ->
-(*                     prerr_endline "OK"; *)
+(*prerr_endline ((sprintf "CHOOSED ITEM OK: %s" (string_of_domain_item item)));*)
                     let res = 
                       (match inner_dom with
                       | [] ->
@@ -608,7 +583,7 @@ in refine_profiler.HExtlib.profile foo ()
                     in
                      res @@ filter tl
                 | Uncertain loc_msg ->
-(*                     prerr_endline ("UNCERTAIN"); *)
+(*prerr_endline ((sprintf "CHOOSED ITEM UNCERTAIN: %s" (string_of_domain_item item) ^ snd (Lazy.force loc_msg)));*)
                     let res =
                       (match inner_dom with
                       | [] -> [],[new_env,new_diff,loc_msg],[]
@@ -619,7 +594,7 @@ in refine_profiler.HExtlib.profile foo ()
                     in
                      res @@ filter tl
                 | Ko loc_msg ->
-(*                     prerr_endline "KO"; *)
+(*prerr_endline ((sprintf "CHOOSED ITEM KO: %s" (string_of_domain_item item)));*)
                     let res = [],[],[new_env,new_diff,loc_msg,true] in
                      res @@ filter tl)
            in