Changes to disambiguation:

* bug fixed: when pruning from the disambiguation domain symbols with
  just one interpretation, not all of them were pruned
* improvement: errors due to symbols with no interpretation are now
  immediately detected

Changes to refinement:

* major improvement:
  one error was always raised as an Uncertain; it is now raised as a
  Failure when it is the case (i.e. a term/type is found where a sort is
  expected and the term/type has no flexible head).
  This bug fix exponentially decrease the number of refinements performed
  in the disambiguation of some terms in ASM/Status.ma in CerCo

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index c8376078285100419e9ba228cadce6fc60170de7..4476d562a949d0e9a82e0bc69f49dfb8dacc3649 100644 (file)
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -446,9 +446,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) as node) :: 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 +461,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 +545,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 +567,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 +580,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 +591,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

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index d2fa70184dc87169ebc5feae4180271faf2fcf3a..95d26c0731a19378481ac9fe62b93b7625df3010 100644 (file)
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -66,6 +66,7 @@ let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_c
 let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
  ~localization_tbl 
 =
+  (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
   assert (metasenv=[]);
   assert (subst=[]);
   let localise t = 

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index ea502b68592070aad0062c6002c5143059cfd0dc..a59a6fd359109202b3c8aed7c39efcaf1c6e3339 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -909,12 +909,19 @@ and force_to_sort status metasenv subst context t orig_t localise ty =
       metasenv, subst, t, ty
   with
       Failure _ -> 
+        let msg =
+         (lazy (localise orig_t, 
+           "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
+           " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
         let ty = NCicReduction.whd status ~subst context ty in
+        let exn =
+         if NCicUnification.could_reduce ty then
+          Uncertain msg
+         else
+          RefineFailure msg
+        in
           try_coercions status ~localise metasenv subst context
-            t orig_t ty `Sort 
-             (Uncertain (lazy (localise orig_t, 
-             "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
-             " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)))
+            t orig_t ty `Sort exn
 
 and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
  t (t1, t2) 

diff --git a/matita/components/ng_refiner/nCicUnification.mli b/matita/components/ng_refiner/nCicUnification.mli
index ec21d66434fba1432521e56fa92e08288b5fed87..510a31136a983e3eb9d9c9b6f8e9d028569d499e 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.mli
+++ b/matita/components/ng_refiner/nCicUnification.mli
@@ -28,6 +28,10 @@ val fix_sorts:
   #NCic.status -> NCic.metasenv -> NCic.substitution -> 
     NCic.term -> NCic.metasenv * NCic.term
 
+(* this should be moved elsewhere *)
+(* The term must be in whd *)
+val could_reduce: NCic.term -> bool
+
 (* delift_type_wrt_terms st m s c t args
  *   lift t (length args) 
  *      [ rel 1 ... rel (len args) / lift (length args) (arg_1 .. arg_n) ]