From: Claudio Sacerdoti Coen Date: Tue, 22 Nov 2011 09:35:32 +0000 (+0000) Subject: Changes to disambiguation: X-Git-Tag: make_still_working~2066 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46ee64f692a1e5e65864ebb82ec875e8d115843c;p=helm.git 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 c83760782..4476d562a 100644 --- 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))); (* (* *) @@ -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 d2fa70184..95d26c073 100644 --- 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 ea502b685..a59a6fd35 100644 --- 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 ec21d6643..510a31136 100644 --- 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) ]