X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=5ce1386aeb0b16a9aca5a0f4abbde42270d3afe9;hb=988cf01c5bd740d6e75767327f201a3c43d635ed;hp=62d708a7fdfcce6797bff7e0fa07926a3e128a1e;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index 62d708a7f..5ce1386ae 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -61,14 +61,18 @@ let mono_uris_callback ~selection_mode ?ok raise Ambiguous_input let mono_interp_callback _ _ _ = raise Ambiguous_input +let mono_disamb_callback _ = raise Ambiguous_input 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" @@ -129,16 +133,31 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t -let resolve ~env ~mk_choice (item: domain_item) arg = +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 = @@ -155,16 +174,19 @@ let string_of_name = | _ -> 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 (name, attr) -> - [ Node ([loc], 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 (name, attr) as hd :: args) - | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) 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 @@ -175,13 +197,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function Ast.AttributedTerm (`Loc loc,_) -> loc | _ -> loc in - [ Node ([loc], Symbol (name,attr), args_dom) ] - | Ast.Appl (Ast.Ident (id,uri) as hd :: args) - | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) -> - let uri = match uri with - | `Uri u -> Some u - | _ -> None - in + [ 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) @@ -196,7 +214,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function ignore(find_in_context id context); args_dom with Not_found -> - [ Node ([loc], Id (id,uri), args_dom) ] ) + [ Node ([loc], Id id, args_dom) ] ) | Ast.Appl terms -> List.fold_right (fun term acc -> domain_of_term ~loc ~context term @ acc) @@ -207,17 +225,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",None), (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, Some r, _), _) :: _ -> - [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] + | (Ast.Pattern (head, Some r, _), _) :: _ -> [] + (* [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] *) | (Ast.Pattern (head, None, _), _) :: _ -> - [ Node ([loc], Id (head,None), []) ] + [ Node ([loc], Id head, []) ] | _ :: tl -> get_first_constructor tl in let do_branch = function @@ -239,9 +257,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, None) -> [ Node ([loc], Id (ident,None) , []) ] - | Some (ident, Some r) -> - [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ]) + | 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 @@ -301,11 +319,11 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function dom @ dom') [] subst in [ Node ([loc], Id name, terms) ]))*) - [ Node ([loc], Id (name,x), []) ]) + [ 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) @@ -374,18 +392,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,None) -> + | Symbol symb -> (match elt with - Symbol (symb',_) when symb = symb' -> true + Symbol symb' when symb = symb' -> true | _ -> false) - | Num _ -> + | Num -> (match elt with - Num _ -> true + Num -> true | _ -> false) | item -> elt = item ) dom2 @@ -432,6 +451,11 @@ let letrecaux_split ctx (args,f,bo,n) = [(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 -> [] @@ -442,7 +466,17 @@ let pattern_split ctx = function ((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 auxpatt [] pl + 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 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 @@ -452,7 +486,7 @@ let pattern_split ctx = function let rec split ctx = function | Ast.AttributedTerm (attr,t) -> [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t] - | Ast.Appl tl -> list_split split (fun x -> ctx (Ast.Appl x)) [] tl + | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0]) (fun x -> ctx (Ast.Appl x)) [] tl | Ast.Binder (k,((n,None) as n'),body) -> [ (fun v -> ctx (Ast.Binder (k,n',v))),body] | Ast.Binder (k,((n,Some ty) as n'),body) -> @@ -491,12 +525,17 @@ let bfvisit ~pp_term top_split test t = | [] -> None | (ctx0,t0 as hd)::tl -> (* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *) - prerr_endline ("t0 = " ^ pp_term t0); - if test t0 then (prerr_endline "caso 1"; Some hd) + debug_print (lazy ("visiting t0 = " ^ pp_term t0)); + if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd) else - let t0' = split ctx0 t0 in - (prerr_endline ("caso 2: length t0' = " ^ string_of_int - (List.length t0')); aux (tl@t0' (*split ctx0 t0*))) + (* + (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 ctx0 t0 in + aux (tl@t0') (* in aux [(fun x -> x),t] *) in aux (top_split t) ;; @@ -520,44 +559,11 @@ let bfvisit_obj = bfvisit obj_split;; let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;; -(*let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t = - let mk_alias = function - | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None) - | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None) - | Ast.Num _ -> DisambiguateTypes.Num None - | _ -> assert false - in - let lookup_choices = - fun item -> - (*match universe with - | None -> - lookup_in_library - interactive_user_uri_choice - input_or_locate_uri item - | Some e -> - (try Environment.find item e - with Not_found -> []) -*) - (try Environment.find item universe - with Not_found -> []) - in - match t with - | Ast.Ident (_,None) - | Ast.Num (_,None) - | Ast.Symbol (_,None) -> - let choices = lookup_choices (mk_alias t) in - if List.length choices <> 1 then t - else List.hd choices - (* but we lose info on closedness *) - | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) t -;; -*) - let domain_item_of_ast = function - | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None) - | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None) - | Ast.Num (n,_) -> DisambiguateTypes.Num None - | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None) + | 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 ;; @@ -570,19 +576,22 @@ let ast_of_alias_spec t alias = match (t,alias) with | _ -> assert false ;; -let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri +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 + 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 _ -> false + | Ko x -> + let _,err = Lazy.force x in + debug_print (lazy ("test_interpr error: " ^ err)); + false | _ -> true with (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) @@ -600,24 +609,24 @@ let rec disambiguate_list ~mk_localization_tbl ~pp_thing ~pp_term in let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty - ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl + ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl in let find_choices item = let a2s = function - | GrafiteAst.Ident_alias (id,_) - | GrafiteAst.Symbol_alias (id,_,_) -> id - | GrafiteAst.Number_alias _ -> "NUM" + | 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" + | Id id + | Symbol id -> id + | Num -> "NUM" in let res = Environment.find item universe in - prerr_endline (Printf.sprintf "choices for %s :\n%s" - (d2s item) (String.concat ", " (List.map a2s res))); + debug_print (lazy (Printf.sprintf "choices for %s :\n%s" + (d2s item) (String.concat ", " (List.map a2s res)))); res in @@ -632,18 +641,12 @@ let rec disambiguate_list match ts with | [] -> None | t0 :: tl -> - prerr_endline ("disambiguation of t0 = " ^ pp_thing t0); + 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),_,_) -> - (prerr_endline ("ambiguous case" ^ ity);true) - | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false - | Ast.Case (_,Some (ity,Some r),_,_) -> - (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false) - | Ast.Ident (n,`Uri u) -> - (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false ) + | Ast.Case (_,Some (ity,None),_,_) -> true | _ -> false in let astpp = function @@ -655,50 +658,24 @@ let rec disambiguate_list (* get first ambiguous subterm (or return disambiguated term) *) match visit ~pp_term is_ambiguous t0 with | None -> - prerr_endline ("not ambiguous:\n" ^ pp_thing t0); + debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0)); Some (t0,tl) | Some (ctx, t) -> - prerr_endline ("disambiguating node " ^ astpp t ^ - "\nin " ^ pp_thing (ctx 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 + debug_print (lazy "-- possible instances:"); + List.iter + (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances; (* perforate ambiguous subterms and test refinement *) + debug_print (lazy "-- survivors:"); let survivors = List.filter test_interpr instances in + List.iter + (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors; disambiguate_list (survivors@tl) ;; - -(* let rec aux l = - match l with - | [] -> None - | (ctx,u)::vl -> - if test u - then (ctx,u) - else aux (vl@split ctx u) - in aux [t] -;;*) - -(* let rec instantiate_ast = function - | Ident (n,Some _) - | Symbol (s,Some _) - | Num (n,Some _) as t -> [] - | Ident (n,None) -> (* output: all possible instantiations of n *) - | Symbol (s,None) -> - | Num (n,None) -> - - - | AttributedTerm (a,u) -> AttributedTerm (a,f u) - | Appl tl -> Appl (List.map f tl) - | Binder (k,n,body) -> Binder (k,n,f body) - | Case (t,ity,oty,pl) -> - let pl' = List.map (fun (p,u) -> p,f u) pl in - Case (f t,ity,map_option f oty,pl') - | Cast (u,v) -> Cast (f u,f v) - | LetIn (n,u,v) -> LetIn (n,f u,f v) - | LetRec -> ada (* TODO *) - | t -> t -*) - let disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context @@ -709,22 +686,10 @@ let disambiguate_thing ~visit ~mk_localization_tbl (thing_txt,thing_txt_prefix_len,thing) = -(* XXX: will be thrown away *) - let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing - in - let rec aux_env 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_env (aux_env env l) tl in - let env = aux_env aliases todo_dom in + let env = aliases in let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty - ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl + ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl in (* real function *) let rec aux tl = @@ -738,323 +703,39 @@ let disambiguate_thing let refine t = let localization_tbl = mk_localization_tbl 503 in - match refine_thing metasenv subst context uri - ~use_coercions - (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl) - expty base_univ ~localization_tbl with - | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u' + 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 -> let _,err = Lazy.force x in - prerr_endline ("refinement uncertain after disambiguation: " ^ err); + debug_print (lazy ("refinement uncertain after disambiguation: " ^ err)); assert false | _ -> assert false in - if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[])) + if not (test_interpr thing) then + (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); + raise (NoWellTypedInterpretation (0,[]))) else let res = aux [thing] in let res = - HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res + HExtlib.filter_map (fun t -> + try Some (refine t) + with _ -> + debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res in match res with | [] -> raise (NoWellTypedInterpretation (0,[])) | [t] -> res,false - | _ -> res,true + | _ -> + let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in + let user_choice = interactive_ast_choice choices in + [ List.nth res user_choice ], true + (* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in + List.iter pp_thing res; res,true *) ;; -(* -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 - - (* 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 - -(* - (* *) - 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 - (* *) -*) - - (* (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 - 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 - 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] - 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 - in - res - *)