X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=7e395e1c19bb096a7bc57845002624ba54c48b66;hb=8a74607bfb8c49e529c4b55a8cad92dd0c68012f;hp=c8376078285100419e9ba228cadce6fc60170de7;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index c83760782..7e395e1c1 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -31,14 +31,8 @@ open DisambiguateTypes module Ast = NotationPt -(* the integer is an offset to be added to each location *) -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception NoWellTypedInterpretation of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * bool) list +exception NoWellTypedInterpretation of (Stdpp.location * string) + exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -51,6 +45,7 @@ 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 = if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true @@ -60,15 +55,21 @@ let mono_uris_callback ~selection_mode ?ok else raise Ambiguous_input -let mono_interp_callback _ _ _ = raise Ambiguous_input +let mono_interp_callback _ _ _ = assert false +let mono_disamb_callback _ = assert false let _choose_uris_callback = ref mono_uris_callback let _choose_interp_callback = ref mono_interp_callback +let _choose_disamb_callback = ref mono_disamb_callback let set_choose_uris_callback f = _choose_uris_callback := f let set_choose_interp_callback f = _choose_interp_callback := f +let set_choose_disamb_callback f = _choose_disamb_callback := f let interactive_user_uri_choice = !_choose_uris_callback let interactive_interpretation_choice interp = !_choose_interp_callback interp +let interactive_ast_choice interp = !_choose_disamb_callback interp +*) + 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" @@ -124,26 +125,45 @@ let domain_size = ref 0 let choices_avg = ref 0. *) -let descr_of_domain_item = function - | Id s -> s - | Symbol (s, _) -> s - | Num i -> string_of_int i - type ('term,'metasenv,'subst,'graph) test_result = | Ok of 'term * 'metasenv * 'subst * 'graph | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t -let resolve ~env ~mk_choice (item: domain_item) arg = +type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result = + | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list + (* each element of this list is a list of partially instantiated asts, + * sharing the last instantiated node, together with the location of that + * node; each ast is associated with the actual instantiation of the node, + * the refinement error, and the location at which refinement fails *) + | Disamb_failure of + (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list + +let resolve ~env ~universe ~mk_choice item interpr arg = + (* let _ = (mk_choice : (GrafiteAst.alias_spec -> 'b + DisambiguateTypes.codomain_item)) in *) try - match snd (mk_choice (Environment.find item env)), arg with + let interpr = + match interpr with + | None -> InterprEnv.find item env + | Some i -> i + in + (* one, and only one interpretation is returned (or Not_found) *) + (*if (List.length interpr <> 1) + then (let strinterpr = + String.concat ", " (List.map GrafiteAst.description_of_alias interpr) in + prerr_endline (Printf.sprintf "choices for %s: %s" + (DisambiguateTypes.string_of_domain_item item) strinterpr); + assert false) + else + let interpr = List.hd interpr in*) + match snd (mk_choice interpr), 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 [] | _,_ -> assert false with Not_found -> - failwith ("Domain item not found: " ^ - (DisambiguateTypes.string_of_domain_item item)) + failwith (": InterprEnv.find failed") (* TODO move it to Cic *) let find_in_context name context = @@ -156,20 +176,23 @@ let find_in_context name context = let string_of_name = function - | Ast.Ident (n, None) -> Some n + | Ast.Ident (n, _) -> Some n | _ -> assert false ;; +(* XXX: assuming the domain is composed of uninterpreted items only *) let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | Ast.AttributedTerm (`Loc loc, term) -> domain_of_term ~loc ~context term | Ast.AttributedTerm (_, term) -> domain_of_term ~loc ~context term - | Ast.Symbol (symbol, instance) -> - [ Node ([loc], Symbol (symbol, instance), []) ] + | Ast.Symbol (name, attr) -> + (match attr with + | None -> [ Node ([loc], Symbol name, []) ] + | _ -> []) (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *) - | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args) - | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args) + | Ast.Appl (Ast.Symbol (name, None) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,None)) as hd :: args) -> let args_dom = List.fold_right @@ -180,9 +203,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function Ast.AttributedTerm (`Loc loc,_) -> loc | _ -> loc in - [ Node ([loc], Symbol (symbol, instance), args_dom) ] - | Ast.Appl (Ast.Ident (name, subst) as hd :: args) - | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) -> + [ Node ([loc], Symbol name, args_dom) ] + | Ast.Appl (Ast.Ident (id,`Ambiguous) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,`Ambiguous)) as hd :: args) -> let args_dom = List.fold_right (fun term acc -> domain_of_term ~loc ~context term @ acc) @@ -194,22 +217,10 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function in (try (* the next line can raise Not_found *) - ignore(find_in_context name context); - if subst <> None then - Ast.fail loc "Explicit substitutions not allowed here" - else + ignore(find_in_context id context); args_dom with Not_found -> - (match subst with - | None -> [ Node ([loc], Id name, args_dom) ] - | Some subst -> - let terms = - List.fold_left - (fun dom (_, term) -> - let dom' = domain_of_term ~loc ~context term in - dom @ dom') - [] subst in - [ Node ([loc], Id name, terms @ args_dom) ])) + [ Node ([loc], Id id, args_dom) ] ) | Ast.Appl terms -> List.fold_right (fun term acc -> domain_of_term ~loc ~context term @ acc) @@ -220,14 +231,17 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function domain_of_term ~loc ~context:(string_of_name var :: context) body in (match kind with - | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ] + | `Exists -> [ Node ([loc], Symbol "exists", (type_dom @ body_dom)) ] | _ -> type_dom @ body_dom) | Ast.Case (term, indty_ident, outtype, branches) -> let term_dom = domain_of_term ~loc ~context term in let outtype_dom = domain_of_term_option ~loc ~context outtype in let rec get_first_constructor = function | [] -> [] - | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ] + | (Ast.Pattern (head, Some r, _), _) :: _ -> [] + (* [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] *) + | (Ast.Pattern (head, None, _), _) :: _ -> + [ Node ([loc], Id head, []) ] | _ :: tl -> get_first_constructor tl in let do_branch = function @@ -249,7 +263,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in (match indty_ident with | None -> get_first_constructor branches - | Some (ident, _) -> [ Node ([loc], Id ident, []) ]) + | Some (ident, None) -> [ Node ([loc], Id ident , []) ] + | Some (ident, Some r) -> []) + (* [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ]) *) @ term_dom @ outtype_dom @ branches_dom | Ast.Cast (term, ty) -> let term_dom = domain_of_term ~loc ~context term in @@ -289,15 +305,16 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function ) [] defs in defs_dom @ where_dom - | Ast.Ident (name, subst) -> + | Ast.Ident (name, _x) -> + (* let x = match x with + | `Uri u -> Some u + | _ -> None + in *) (try (* the next line can raise Not_found *) - ignore(find_in_context name context); - if subst <> None then - Ast.fail loc "Explicit substitutions not allowed here" - else - [] + ignore(find_in_context name context); [] with Not_found -> + (* (match subst with | None -> [ Node ([loc], Id name, []) ] | Some subst -> @@ -307,12 +324,12 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function let dom' = domain_of_term ~loc ~context term in dom @ dom') [] subst in - [ Node ([loc], Id name, terms) ])) - | Ast.Uri _ -> [] + [ Node ([loc], Id name, terms) ]))*) + [ Node ([loc], Id name, []) ]) | Ast.NRef _ -> [] | Ast.NCic _ -> [] | Ast.Implicit _ -> [] - | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] + | Ast.Num (num, i) -> [ Node ([loc], Num, []) ] | Ast.Meta (index, local_context) -> List.fold_left (fun dom term -> dom @ domain_of_term_option ~loc ~context term) @@ -381,18 +398,19 @@ let domain_of_obj ~context obj = uniq_domain (domain_of_obj ~context obj) (* dom1 \ dom2 *) +(* XXX: possibly should take into account locs? *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) let is_in_dom2 elt = List.exists (function - | Symbol (symb, 0) -> + | Symbol symb -> (match elt with - Symbol (symb',_) when symb = symb' -> true + Symbol symb' when symb = symb' -> true | _ -> false) - | Num i -> + | Num -> (match elt with - Num _ -> true + Num -> true | _ -> false) | item -> elt = item ) dom2 @@ -407,298 +425,369 @@ let domain_diff dom1 dom2 = let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" -let disambiguate_thing - ~context ~metasenv ~subst ~use_coercions - ~string_context_of_context - ~initial_ugraph:base_univ ~expty - ~mk_implicit ~description_of_alias ~fix_instance - ~aliases ~universe ~lookup_in_library - ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing - ~mk_localization_tbl - (thing_txt,thing_txt_prefix_len,thing) -= - debug_print (lazy "DISAMBIGUATE INPUT"); - debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); - let thing_dom = - domain_of_thing ~context:(string_context_of_context context) thing in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); - let current_dom = - Environment.fold (fun item _ dom -> item :: dom) aliases [] in - let todo_dom = domain_diff thing_dom current_dom in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); - (* (2) lookup function for any item (Id/Symbol/Num) *) - let lookup_choices = - fun item -> - match universe with - | None -> - lookup_in_library - interactive_user_uri_choice - input_or_locate_uri item - | Some e -> - (try - fix_instance item (Environment.find item e) - with Not_found -> []) - in +(* generic function lifting splitting from type T to type (T list) *) +let rec list_split item_split ctx pre post = + match post with + | [] -> [] + | x :: post' -> + (item_split (fun v1 -> ctx (pre@v1::post')) x)@ + list_split item_split ctx (pre@[x]) post' +;; - (* items with 1 choice are interpreted ASAP *) - let aliases, todo_dom = - let rec aux (aliases,acc) = function - | [] -> aliases, acc - | (Node (_, item,extra) as node) :: tl -> - let choices = lookup_choices item in - if List.length choices <> 1 then aux (aliases, acc@[node]) tl - else - let tl = tl @ extra in - if Environment.mem item aliases then aux (aliases, acc) tl - else aux (Environment.add item (List.hd choices) aliases, acc) tl - in - aux (aliases,[]) todo_dom - in +(* splits a 'term capture_variable *) +let var_split ctx = function + | (_,None) -> [] + | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty] +;; -(* - (* *) - let _ = - if benchmark then begin - let per_item_choices = - List.map - (fun dom_item -> - try - let len = List.length (lookup_choices dom_item) in - debug_print (lazy (sprintf "BENCHMARK %s: %d" - (string_of_domain_item dom_item) len)); - len - with No_choices _ -> 0) - thing_dom - in - max_refinements := List.fold_left ( * ) 1 per_item_choices; - actual_refinements := 0; - domain_size := List.length thing_dom; - choices_avg := - (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size) - end - in - (* *) -*) +let ity_split ctx (n,isind,ty,cl) = + [(fun x -> ctx (n,isind,x,cl)),ty]@ + list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty]) + (fun x -> ctx (n,isind,ty,x)) [] cl +;; + +let field_split ctx (n,ty,b,m) = + [(fun x -> ctx (n,x,b,m)),ty] +;; - (* (3) test an interpretation filling with meta uninterpreted identifiers - *) - let test_env aliases todo_dom ugraph = - try - let rec aux env = function - | [] -> env - | Node (_, item, l) :: tl -> - let env = - Environment.add item - (mk_implicit - (match item with | Id _ | Num _ -> true | Symbol _ -> false)) - env in - aux (aux env l) tl in - let filled_env = aux aliases todo_dom in - let localization_tbl = mk_localization_tbl 503 in - let cic_thing = - interpretate_thing ~context ~env:filled_env - ~uri ~is_path:false thing ~localization_tbl +(* splits a defn. in a mutual LetRec block *) +let letrecaux_split ctx (args,f,bo,n) = + list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@ + var_split (fun x -> ctx (args,x,bo,n)) f@ + [(fun x -> ctx (args,f,x,n)),bo] +;; + +let mk_ident s = function +| None -> Ast.Ident (s,`Ambiguous) +| Some u -> Ast.Ident (s,`Uri (NReference.string_of_reference u)) +;; + +(* splits a pattern (for case analysis) *) +let pattern_split ctx = function + | Ast.Wildcard -> [] + | Ast.Pattern (s,href,pl) -> + let rec auxpatt pre = function + | [] -> [] + | (x,Some y as x')::post' -> + ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y) + ::auxpatt (pre@[x']) post' + | (x,None as x')::post' -> auxpatt (pre@[x']) post' + in + ((fun x -> + let id0, href0 = + match x with + | Ast.Ident (id,`Ambiguous) -> id, None + | Ast.Ident (id,`Uri u) -> id, Some u + | _ -> assert false in -let foo () = - refine_thing metasenv subst context uri - ~use_coercions cic_thing expty ugraph ~localization_tbl -in refine_profiler.HExtlib.profile foo () - with - | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) - | Invalid_choice loc_msg -> Ko loc_msg - in - (* (4) build all possible interpretations *) - let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in - (* aux returns triples Ok/Uncertain/Ko *) - (* rem_dom is the concatenation of all the remainin domains *) - let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = - debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); - match todo_dom with - | [] -> - assert (lookup_in_todo_dom = None); - (match test_env aliases rem_dom base_univ with - | Ok (thing, metasenv,subst,new_univ) -> - [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] - | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] - | Uncertain loc_msg -> - [],[aliases,diff,loc_msg],[]) - | Node (locs,item,inner_dom) :: remaining_dom -> - debug_print (lazy (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item))); - let choices = - match lookup_in_todo_dom with - None -> lookup_choices item - | Some choices -> choices in - match choices with - [] -> - [], [], - [aliases, diff, - (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 - (fun (env, diff, loc_msg, _b) -> - env, diff, loc_msg, false) - failures in - let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = - if ok_l <> [] || uncertain_l <> [] then - ok_l,uncertain_l,mark_not_significant error_l - else - outcome in - let rec filter = function - | [] -> [],[],[] - | codomain_item :: tl -> - (*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 - (match - test_env new_env - (inner_dom@remaining_dom@rem_dom) base_univ - with - | Ok (thing, metasenv,subst,new_univ) -> -(* prerr_endline "OK"; *) - let res = - (match inner_dom with - | [] -> - [new_env,new_diff,metasenv,subst,thing,new_univ], - [], [] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Uncertain loc_msg -> -(* prerr_endline ("UNCERTAIN"); *) - let res = - (match inner_dom with - | [] -> [],[new_env,new_diff,loc_msg],[] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Ko loc_msg -> -(* prerr_endline "KO"; *) - let res = [],[],[new_env,new_diff,loc_msg,true] in - res @@ filter tl) - in - let ok_l,uncertain_l,error_l = - classify_errors (filter choices) - in - let res_after_ok_l = - List.fold_right - (fun (env,diff,_,_,_,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) ok_l ([],[],error_l) - in - List.fold_right - (fun (env,diff,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) uncertain_l res_after_ok_l + let href0 = HExtlib.map_option NReference.reference_of_string href0 + in ctx (Ast.Pattern (id0,href0,pl))), + mk_ident s href)::auxpatt [] pl +;; + + (* this function is used to get the children of a given node, together with + * their context and their location + * contexts are expressed in the form of functions Ast -> Ast *) +(* split : location -> ('term -> 'a) -> 'term -> (('term -> 'a) * 'term * loc) list *) +let rec split loc ctx t = + let loc_of_attr oldloc = function + | `Loc l -> l + | _ -> oldloc in - let aux' aliases diff lookup_in_todo_dom todo_dom = - if todo_dom = [] then - aux aliases diff lookup_in_todo_dom todo_dom [] - else - match test_env aliases todo_dom base_univ with - | Ok _ - | Uncertain _ -> - aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] + match t with + | Ast.AttributedTerm (attr,t) -> + [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t, loc_of_attr loc attr] + | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0,loc]) (fun x -> ctx (Ast.Appl x)) [] tl + | Ast.Binder (k,((n,None) as n'),body) -> + [ (fun v -> ctx (Ast.Binder (k,n',v))),body, loc] + | Ast.Binder (k,((n,Some ty) as n'),body) -> + [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty, loc + ;(fun v -> ctx (Ast.Binder (k,n',v))),body, loc] + | Ast.Case (t,ity,outty,pl) -> + let outty_split = match outty with + | None -> [] + | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u] + in + List.map (fun (a,b) -> a,b,loc) + (((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t):: + outty_split@list_split + (fun ctx0 (p,x) -> + ((fun y -> ctx0 (p,y)),x)::pattern_split + (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x))) + [] pl) + | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u,loc + ; (fun x -> ctx (Ast.Cast (u,x))),v,loc ] + | Ast.LetIn ((n,None) as n',u,v) -> + [ (fun x -> ctx (Ast.LetIn (n',x,v))), u,loc + ; (fun x -> ctx (Ast.LetIn (n',u,x))), v,loc ] + | Ast.LetIn ((n,Some t) as n',u,v) -> + [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t,loc + ; (fun x -> ctx (Ast.LetIn (n',x,v))), u, loc + ; (fun x -> ctx (Ast.LetIn (n',u,x))), v, loc ] + | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *) + List.map (fun (a,b) -> a,b,loc) + (list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs) + | _ -> [] (* leaves *) +;; + +type 'ast marked_ast = + (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location + +(* top_split : 'a -> ((term -> 'a) * term * loc) list + * such that it returns all the possible top-level (ctx,t,dummy_loc) for its input *) +let bfvisit ~pp_term top_split test t = + let rec aux = function + | [] -> None + | (ctx0,t0,loc as hd)::tl -> +(* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *) + debug_print (lazy ("visiting t0 = " ^ pp_term t0)); + if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd) + else + (* + (prerr_endline ("splitting not ambiguous t0:"); + let t0' = split ctx0 t0 in + List.iter (fun (ctx',t') -> prerr_endline ("-- subnode " ^ + (pp_term t'))) t0'; + aux (tl@t0')) *) + let t0' = split loc ctx0 t0 in + aux (tl@t0') + (* in aux [(fun x -> x),t] *) + in aux (top_split t) +;; + +let obj_split (o:Ast.term Ast.obj) = match o with + | Ast.Inductive (ls,itl) -> + List.map (fun (a,b) -> a,b,Stdpp.dummy_loc) + (list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@ + list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl) + | Ast.Theorem (flav,n,ty,None,p) -> + [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty, Stdpp.dummy_loc] + | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) -> + [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty, Stdpp.dummy_loc + ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo, Stdpp.dummy_loc] + | Ast.Record (ls,n,ty,fl) -> + List.map (fun (a,b) -> a,b,Stdpp.dummy_loc) + (list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@ + [(fun x -> Ast.Record (ls,n,x,fl)),ty]@ + list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl) +;; + +let bfvisit_obj = bfvisit obj_split;; + +let bfvisit = bfvisit (fun t -> [(fun x -> x),t,Stdpp.dummy_loc]) ;; + +let domain_item_of_ast = function + | Ast.Ident (id,_) -> DisambiguateTypes.Id id + | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym + | Ast.Num (n,_) -> DisambiguateTypes.Num + | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id ityname + | _ -> assert false +;; + +let ast_of_alias_spec t alias = match (t,alias) with + | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri) + | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) -> + Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl) + | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc)) + | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc)) + | _ -> assert false +;; + +(* returns an optional (loc*string): + * - None means success (the ast is refinable) + * - Some (loc,err) means refinement has failed with error err at location loc + *) +let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe ~uri + ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t = + try + let localization_tbl = mk_localization_tbl 503 in + let cic_thing = + interpretate_thing ~context ~env ~universe + ~uri ~is_path:false t ~localization_tbl + in + let foo () = + refine_thing metasenv subst context uri + ~use_coercions cic_thing expty ugraph ~localization_tbl + in match (refine_profiler.HExtlib.profile foo ()) with + | Ko x -> + let loc,err = Lazy.force x in + debug_print (lazy ("test_interpr error: " ^ err)); + Some (loc,err) + | _ -> None + with + (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) + | Invalid_choice loc_msg -> Ko loc_msg*) + | Invalid_choice x -> + let loc,err = Lazy.force x in + debug_print (lazy ("test_interpr invalid choice: " ^ err)); + Some (loc,err) + | e -> debug_print (lazy ("uncaught error: "^ Printexc.to_string e));None +;; + +exception Not_ambiguous;; + +let rec disambiguate_list + ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing + ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term + ts errors = + + let disambiguate_list = + disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri + ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe + ~mk_localization_tbl ~pp_thing ~pp_term + in + let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty + ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl in + let find_choices item = + let a2s = function + | GrafiteAst.Ident_alias (_id,uri) -> uri + | GrafiteAst.Symbol_alias (_id,_,desc) -> desc + | GrafiteAst.Number_alias (_,desc) -> desc + in + let d2s = function + | Id id + | Symbol id -> id + | Num -> "NUM" + in let res = - match aux' aliases [] None todo_dom with - | [],uncertain,errors -> - let errors = - List.map - (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true) - ) uncertain @ errors - in - let errors = - List.map - (fun (env,diff,loc_msg,significant) -> - let env' = - filter_map_domain - (fun locs domain_item -> - try - let description = - description_of_alias (Environment.find domain_item env) - in - Some (locs,descr_of_domain_item domain_item,description) - with - Not_found -> None) - thing_dom - in - let diff= List.map (fun a,b -> a,description_of_alias b) diff in - env',diff,loc_msg,significant - ) errors - in - raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,subst,t,ugraph],_,_ -> - debug_print (lazy "SINGLE INTERPRETATION"); - [diff,metasenv,subst,t,ugraph], false - | l,_,_ -> - debug_print - (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); - let choices = - List.map - (fun (env, _, _, _, _, _) -> - map_domain - (fun locs domain_item -> - let description = - description_of_alias (Environment.find domain_item env) - in - locs,descr_of_domain_item domain_item, description) - thing_dom) - l - in - let choosed = - interactive_interpretation_choice - thing_txt thing_txt_prefix_len choices - in - (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u) - choosed), - true + Environment.find item universe in - res + debug_print (lazy (Printf.sprintf "choices for %s :\n%s" + (d2s item) (String.concat ", " (List.map a2s res)))); + res + in + + let get_instances ctx t = + try + let choices = find_choices (domain_item_of_ast t) in + List.map (fun t0 -> ctx (ast_of_alias_spec t t0), t0) choices + with + | Not_found -> [] + in + + match ts with + | [] -> [], errors + | _ -> + (* debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); *) + let is_ambiguous = function + | Ast.Ident (_,`Ambiguous) + | Ast.Num (_,None) + | Ast.Symbol (_,None) -> true + | Ast.Case (_,Some (ity,None),_,_) -> true + | _ -> false + in + let astpp = function + | Ast.Ident (id,_) -> "ID " ^ id + | Ast.Num _ -> "NUM" + | Ast.Symbol (sym,_) -> "SYM " ^ sym + | _ -> "ERROR!" + in + let process_ast t0 = + (* get first ambiguous subterm (or return disambiguated term) *) + match visit ~pp_term is_ambiguous t0 with + | None -> +(* debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing + * t0));*) + (* Some (t0,tl), errors *) + raise Not_ambiguous + | Some (ctx, t, loc_t) -> + debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^ + "\nin " ^ pp_thing (ctx t))); + (* get possible instantiations of t *) + let instances = get_instances ctx t in + if instances = [] then + raise (NoWellTypedInterpretation (loc_t, "No choices for " ^ astpp t)); + debug_print (lazy "-- possible instances:"); +(* List.iter + (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) +instances; *) + (* perforate ambiguous subterms and test refinement *) + let instances = List.map (fun (x,a) -> (x,Some a),test_interpr x) instances in + debug_print (lazy "-- survivors:"); + let survivors, defuncts = + List.partition (fun (_,o) -> o = None) instances in + survivors, (defuncts, loc_t) + + in + try + let ts', new_errors = List.split (List.map process_ast ts) in + let ts' = List.map (fun ((t,_),_) -> t) (List.flatten ts') in + let errors' = match new_errors with + | (_,l)::_ -> + let ne' = + List.map (fun (a,b) -> a, HExtlib.unopt b) + (List.flatten (List.map fst new_errors)) in + let ne' = List.map (fun ((x,a),(l,e)) -> x,a,l,e) ne' in + (ne',l)::errors + | _ -> errors + in disambiguate_list ts' errors' + with Not_ambiguous -> ts,errors +;; + +let disambiguate_thing + ~context ~metasenv ~subst ~use_coercions + ~string_context_of_context ~initial_ugraph:base_univ + ~expty ~mk_implicit ~description_of_alias + ~fix_instance ~aliases ~universe + ~lookup_in_library ~uri ~pp_thing ~pp_term + ~domain_of_thing ~interpretate_thing ~refine_thing + ~visit ~mk_localization_tbl + (thing_txt,thing_txt_prefix_len,thing) += + let env = aliases in + + let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty + ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl + in +(* real function *) + let aux tl = + disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst + ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit + ~use_coercions ~expty ~uri ~env ~universe ~pp_thing + ~pp_term tl [] + in + let refine t = + let localization_tbl = mk_localization_tbl 503 in + debug_print (lazy "before interpretate_thing"); + let t' = + interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl + in + debug_print (lazy "after interpretate_thing"); + match refine_thing metasenv subst context uri ~use_coercions t' expty + base_univ ~localization_tbl with + | Ok (t',m',s',u') -> t,m',s',t',u' + | Uncertain x | Ko x -> + let loc,err = Lazy.force x in + debug_print (lazy ("refinement uncertain after disambiguation: " ^ err)); + raise (NoWellTypedInterpretation (loc,err)) + in + match (test_interpr thing) with + | Some (loc,err) -> + debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); + Disamb_failure ([[thing,None,loc,err],loc]) + | None -> + let res,errors = aux [thing] in + let res,inner_errors = + List.split + (List.map (fun t -> + try (Some (refine t), None) + (* this error is actually a singleton *) + with NoWellTypedInterpretation loc_err -> + debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t))); + None, Some loc_err) res) in + let res = HExtlib.filter_map (fun x -> x) res in + let inner_errors = + HExtlib.filter_map + (function Some (loc,err) -> Some (thing,None,loc,err) | None -> None) + inner_errors + in + let errors = + if inner_errors <> [] then (inner_errors,Stdpp.dummy_loc)::errors + else errors + in + (match res with + | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors + | _ -> Disamb_success res) +;; +