X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=58e600a425e6af9bbf437aa57e42e2f7afa9a11b;hb=53b8e2af661ad4165aa0b1deccd0a7522d96ce2e;hp=8be47f06313688268623d958ff724c68264e7ebc;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index 8be47f063..58e600a42 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -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 *) @@ -331,10 +303,14 @@ 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 -> [] @@ -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) @@ -407,11 +410,6 @@ let domain_diff dom1 dom2 = let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" -type alias_spec = - | Ident_alias of string * string (* identifier, uri *) - | Symbol_alias of string * int * string (* name, instance no, description *) - | Number_alias of int * string (* instance no, description *) - let disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context @@ -451,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) 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 @@ -461,6 +464,8 @@ let disambiguate_thing in aux (aliases,[]) todo_dom in + debug_print + (lazy(sprintf "TODO DOM: %s"(string_of_domain todo_dom))); (* (* *) @@ -543,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 @@ -600,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 | [] -> @@ -613,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],[] @@ -624,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