X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=f3600b7cbc34602ba9e8a433ae853aaf66f4d3b8;hb=12404305178bb29f7428ba912fce30c524076705;hp=667c50770536bb7187df52a2cc460991b32cf20f;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 667c50770..f3600b7cb 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -32,13 +32,17 @@ open UriManager (* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of - int * (Token.flocation option * string Lazy.t) list + int * + ((Token.flocation list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Token.flocation option * string Lazy.t) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) exception Try_again of string Lazy.t type aliases = bool * DisambiguateTypes.environment +type 'a disambiguator_input = string * int * 'a let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -214,7 +218,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast | CicNotationPt.LetRec (kind, defs, body) -> let context' = List.fold_left - (fun acc ((name, _), _, _) -> + (fun acc (_, (name, _), _, _) -> CicNotationUtil.cic_name_of_name name :: acc) context defs in @@ -258,10 +262,16 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast in let inductiveFuns = List.map - (fun ((name, typ), body, decr_idx) -> - let cic_body = aux ~localize loc context' body in + (fun (params, (name, typ), body, decr_idx) -> + let add_binders kind t = + List.fold_right + (fun var t -> CicNotationPt.Binder (kind, var, t)) params t + in + let cic_body = + aux ~localize loc context' (add_binders `Lambda body) in let cic_type = - aux_option ~localize loc context (Some `Type) typ in + aux_option ~localize loc context (Some `Type) + (HExtlib.map_option (add_binders `Pi) typ) in let name = match CicNotationUtil.cic_name_of_name name with | Cic.Anonymous -> @@ -431,14 +441,17 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let context,res = List.fold_left (fun (context,res) (name,t) -> - Cic.Name name :: context, - (name, interpretate_term context env None false t)::res + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res ) ([],[]) params in context,List.rev res in let add_params = - List.fold_right - (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in + List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in let name_to_uris = snd ( List.fold_left @@ -470,19 +483,23 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let context,res = List.fold_left (fun (context,res) (name,t) -> - (Cic.Name name :: context), - (name, interpretate_term context env None false t)::res + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res ) ([],[]) params in context,List.rev res in let add_params = List.fold_right - (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in + (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in let ty' = add_params (interpretate_term context env None false ty) in let fields' = snd ( List.fold_left - (fun (context,res) (name,ty,_coercion) -> + (fun (context,res) (name,ty,_coercion,arity) -> let context' = Cic.Name name :: context in context',(name,interpretate_term context env None false ty)::res ) (context,[]) fields) in @@ -499,16 +516,19 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = concl fields' in let con' = add_params con in let tyl = [name,true,ty',["mk_" ^ name,con']] in - let field_names = List.map (fun (x,_,y) -> x,y) fields in + let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) | CicNotationPt.Theorem (flavour, name, ty, bo) -> let attrs = [`Flavour flavour] in let ty' = interpretate_term [] env None false ty in - (match bo with - None -> + (match bo,flavour with + None,`Axiom -> + Cic.Constant (name,None,ty',[],attrs) + | Some bo,`Axiom -> assert false + | None,_ -> Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs) - | Some bo -> + | Some bo,_ -> let bo' = Some (interpretate_term [] env None false bo) in Cic.Constant (name,bo',ty',[],attrs)) @@ -521,19 +541,25 @@ let rev_uniq = let compare = Pervasives.compare end in - let module Set = Set.Make (SortedItem) in + let module Map = Map.Make (SortedItem) in fun l -> let rev_l = List.rev l in - let (_, uniq_rev_l) = + let (members, uniq_rev_l) = List.fold_left - (fun (members, rev_l) elt -> - if Set.mem elt members then - (members, rev_l) - else - Set.add elt members, elt :: rev_l) - (Set.empty, []) rev_l + (fun (members, rev_l) (loc,elt) -> + try + let locs = Map.find elt members in + if List.mem loc locs then + members, rev_l + else + Map.add elt (loc::locs) members, rev_l + with + | Not_found -> Map.add elt [loc] members, elt :: rev_l) + (Map.empty, []) rev_l in - List.rev uniq_rev_l + List.rev_map + (fun e -> try Map.find e members,e with Not_found -> assert false) + uniq_rev_l (* "aux" keeps domain in reverse order and doesn't care about duplicates. * Domain item more in deep in the list will be processed first. @@ -549,10 +575,10 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function | CicNotationPt.Binder (kind, (var, typ), body) -> let kind_dom = match kind with - | `Exists -> [ Symbol ("exists", 0) ] + | `Exists -> [ loc, Symbol ("exists", 0) ] | _ -> [] in - let type_dom = domain_rev_of_term_option loc context typ in + let type_dom = domain_rev_of_term_option ~loc context typ in let body_dom = domain_rev_of_term ~loc (CicNotationUtil.cic_name_of_name var :: context) body @@ -563,7 +589,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function let outtype_dom = domain_rev_of_term_option loc context outtype in let get_first_constructor = function | [] -> [] - | ((head, _, _), _) :: _ -> [ Id head ] + | ((head, _, _), _) :: _ -> [ loc, Id head ] in let do_branch ((head, _, args), term) = let (term_context, args_domain) = @@ -583,7 +609,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function branches_dom @ outtype_dom @ term_dom @ (match indty_ident with | None -> get_first_constructor branches - | Some (ident, _) -> [ Id ident ]) + | Some (ident, _) -> [ loc, Id ident ]) | CicNotationPt.Cast (term, ty) -> let term_dom = domain_rev_of_term ~loc context term in let ty_dom = domain_rev_of_term ~loc context ty in @@ -597,19 +623,31 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function in where_dom @ type_dom @ body_dom | CicNotationPt.LetRec (kind, defs, where) -> - let context' = + let add_defs context = List.fold_left - (fun acc ((var, typ), _, _) -> - CicNotationUtil.cic_name_of_name var :: acc) - context defs - in - let where_dom = domain_rev_of_term ~loc context' where in + (fun acc (_, (var, _), _, _) -> + CicNotationUtil.cic_name_of_name var :: acc + ) context defs in + let where_dom = domain_rev_of_term ~loc (add_defs context) where in let defs_dom = List.fold_left - (fun dom ((_, typ), body, _) -> + (fun dom (params, (_, typ), body, _) -> + let context' = + add_defs + (List.fold_left + (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc) + context params) + in domain_rev_of_term ~loc context' body @ - domain_rev_of_term_option loc context typ) - [] defs + domain_rev_of_term_option ~loc context typ @ + List.rev + (snd + (List.fold_left + (fun (context,res) (var,ty) -> + CicNotationUtil.cic_name_of_name var :: context, + res @ domain_rev_of_term_option ~loc context ty) + (add_defs context,[]) params)) + ) [] defs in where_dom @ defs_dom | CicNotationPt.Ident (name, subst) -> @@ -622,29 +660,29 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function [] with Not_found -> (match subst with - | None -> [Id name] + | None -> [loc, Id name] | Some subst -> List.fold_left (fun dom (_, term) -> let dom' = domain_rev_of_term ~loc context term in dom' @ dom) - [Id name] subst)) + [loc, Id name] subst)) | CicNotationPt.Uri _ -> [] | CicNotationPt.Implicit -> [] - | CicNotationPt.Num (num, i) -> [ Num i ] + | CicNotationPt.Num (num, i) -> [loc, Num i ] | CicNotationPt.Meta (index, local_context) -> List.fold_left (fun dom term -> domain_rev_of_term_option loc context term @ dom) [] local_context | CicNotationPt.Sort _ -> [] - | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] + | CicNotationPt.Symbol (symbol, instance) -> [loc, Symbol (symbol, instance) ] | CicNotationPt.UserInput | CicNotationPt.Literal _ | CicNotationPt.Layout _ | CicNotationPt.Magic _ | CicNotationPt.Variable _ -> assert false -and domain_rev_of_term_option loc context = function +and domain_rev_of_term_option ~loc context = function | None -> [] | Some t -> domain_rev_of_term ~loc context t @@ -658,7 +696,7 @@ let domain_of_obj ~context ast = (match bo with None -> [] | Some bo -> domain_rev_of_term [] bo) @ - domain_of_term [] ty + domain_rev_of_term [] ty | CicNotationPt.Inductive (params,tyl) -> let dom = List.flatten ( @@ -671,28 +709,38 @@ let domain_of_obj ~context ast = let dom = List.fold_left (fun dom (_,ty) -> - domain_rev_of_term [] ty @ dom + match ty with + None -> dom + | Some ty -> domain_rev_of_term [] ty @ dom ) dom params in List.filter - (fun name -> - not ( List.exists (fun (name',_) -> name = Id name') params + (fun (_,name) -> + not ( List.exists (fun (name',_) -> + match CicNotationUtil.cic_name_of_name name' with + Cic.Anonymous -> false + | Cic.Name name' -> name = Id name') params || List.exists (fun (name',_,_,_) -> name = Id name') tyl) ) dom | CicNotationPt.Record (params,_,ty,fields) -> let dom = List.flatten - (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in + (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in let dom = - List.fold_left - (fun dom (_,ty) -> - domain_rev_of_term [] ty @ dom - ) (dom @ domain_rev_of_term [] ty) params + List.fold_right + (fun (_,ty) dom -> + match ty with + None -> dom + | Some ty -> dom @ domain_rev_of_term [] ty + ) params (dom @ domain_rev_of_term [] ty) in List.filter - (fun name-> - not ( List.exists (fun (name',_) -> name = Id name') params - || List.exists (fun (name',_,_) -> name = Id name') fields) + (fun (_,name) -> + not ( List.exists (fun (name',_) -> + match CicNotationUtil.cic_name_of_name name' with + Cic.Anonymous -> false + | Cic.Name name' -> name = Id name') params + || List.exists (fun (name',_,_,_) -> name = Id name') fields) ) dom in rev_uniq domain_rev @@ -700,11 +748,21 @@ let domain_of_obj ~context ast = (* dom1 \ dom2 *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) - let is_in_dom2 = - List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt')) - (fun _ -> false) dom2 + let is_in_dom2 elt = + List.exists + (function + | Symbol (symb, 0) -> + (match elt with + Symbol (symb',_) when symb = symb' -> true + | _ -> false) + | Num i -> + (match elt with + Num _ -> true + | _ -> false) + | item -> elt = item + ) dom2 in - List.filter (fun elt -> not (is_in_dom2 elt)) dom1 + List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1 module type Disambiguator = sig @@ -716,7 +774,7 @@ sig ?initial_ugraph:CicUniv.universe_graph -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> - CicNotationPt.term -> + CicNotationPt.term disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term* @@ -729,7 +787,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.obj -> + CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * @@ -744,8 +802,12 @@ module Make (C: Callbacks) = let uris = match uris with | [] -> - [(C.input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())] + (match + (C.input_or_locate_uri + ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ()) + with + | None -> [] + | Some uri -> [uri]) | [uri] -> [uri] | _ -> C.interactive_user_uri_choice ~selection_mode:`MULTIPLE @@ -773,7 +835,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe - ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + (thing_txt,thing_txt_prefix_len,thing) = debug_print (lazy "DISAMBIGUATE INPUT"); let disambiguate_context = (* cic context -> disambiguate context *) @@ -784,7 +847,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); let thing_dom = domain_of_thing ~context:disambiguate_context thing in debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s" - (string_of_domain thing_dom))); + (string_of_domain (List.map snd thing_dom)))); (* debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" (DisambiguatePp.pp_environment aliases))); @@ -803,8 +866,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" match item with | Id id -> choices_of_id dbd id | Symbol (symb, _) -> - List.map DisambiguateChoices.mk_choice + (try + List.map DisambiguateChoices.mk_choice (TermAcicContent.lookup_interpretations symb) + with + TermAcicContent.Interpretation_not_found -> []) | Num instance -> DisambiguateChoices.lookup_num_choices () in @@ -818,7 +884,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" | item -> item in Environment.find item e - with Not_found -> []) + with Not_found -> lookup_in_library ()) in choices in @@ -852,7 +918,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let test_env aliases todo_dom ugraph = let filled_env = List.fold_left - (fun env item -> + (fun env (_,item) -> Environment.add item ("Implicit", (match item with @@ -885,8 +951,9 @@ in refine_profiler.HExtlib.profile foo () (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> [ aliases, diff, metasenv, thing, new_univ ], [] - | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg]) - | item :: remaining_dom -> + | Ko (loc,msg),_ + | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg]) + | (locs,item) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); let choices = @@ -895,7 +962,9 @@ in refine_profiler.HExtlib.profile foo () | Some choices -> choices in match choices with [] -> - [], [None,lazy ("No choices for " ^ string_of_domain_item item)] + [], [aliases, diff, + Some (List.hd locs), + lazy ("No choices for " ^ string_of_domain_item item)] | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -906,7 +975,7 @@ in refine_profiler.HExtlib.profile foo () let lookup_in_todo_dom,next_choice_is_single = match remaining_dom with [] -> None,false - | he::_ -> + | (_,he)::_ -> let choices = lookup_choices he in Some choices,List.length choices = 1 in @@ -924,11 +993,11 @@ in refine_profiler.HExtlib.profile foo () remaining_dom new_univ) | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [], [loc,msg] + | [] -> [], [new_env,new_diff,loc,msg] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [loc,msg]) + | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg]) | _::_ -> let rec filter univ = function | [] -> [],[] @@ -939,43 +1008,72 @@ in refine_profiler.HExtlib.profile foo () (match test_env new_env remaining_dom univ with | Ok (thing, metasenv),new_univ -> (match remaining_dom with - | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], [] + | [] -> [new_env,new_diff,metasenv,thing,new_univ], [] | _ -> aux new_env new_diff None remaining_dom new_univ ) @@ filter univ tl | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [],[loc,msg] + | [] -> [],[new_env,new_diff,loc,msg] | _ -> aux new_env new_diff None remaining_dom new_univ ) @@ filter univ tl - | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl) + | Ko (loc,msg),_ -> ([],[new_env,new_diff,loc,msg]) @@ filter univ tl) in filter base_univ choices in + let aux' aliases diff lookup_in_todo_dom todo_dom base_univ = + match test_env aliases todo_dom base_univ with + | Ok _,_ + | Uncertain _,_ -> + aux aliases diff lookup_in_todo_dom todo_dom base_univ + | Ko (loc,msg),_ -> ([],[aliases,diff,loc,msg]) in let base_univ = initial_ugraph in try let res = - match aux aliases [] None todo_dom base_univ with - | [],errors -> raise (NoWellTypedInterpretation (0,errors)) + match aux' aliases [] None todo_dom base_univ with + | [],errors -> + let errors = + List.map + (fun (env,diff,loc,msg) -> + let env' = + HExtlib.filter_map + (fun (locs,domain_item) -> + try + let description = + fst (Environment.find domain_item env) + in + Some (locs,descr_of_domain_item domain_item,description) + with + Not_found -> None) + thing_dom + in + env',diff,loc,msg + ) errors + in + raise (NoWellTypedInterpretation (0,errors)) | [_,diff,metasenv,t,ugraph],_ -> debug_print (lazy "SINGLE INTERPRETATION"); [diff,metasenv,t,ugraph], false | l,_ -> - debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); + debug_print + (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map (fun (env, _, _, _, _) -> List.map - (fun domain_item -> + (fun (locs,domain_item) -> let description = fst (Environment.find domain_item env) in - (descr_of_domain_item domain_item, description)) + locs,descr_of_domain_item domain_item, description) thing_dom) l in - let choosed = C.interactive_interpretation_choice choices in + let choosed = + C.interactive_interpretation_choice + thing_txt thing_txt_prefix_len choices + in (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed), true in @@ -985,7 +1083,8 @@ in refine_profiler.HExtlib.profile foo () failwith "Disambiguate: circular dependency" let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe + (text,prefix_len,term) = let term = if fresh_instances then CicNotationUtil.freshen_term term else term @@ -993,10 +1092,10 @@ in refine_profiler.HExtlib.profile foo () disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term - ~refine_thing:refine_term term + ~refine_thing:refine_term (text,prefix_len,term) let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri - obj + (text,prefix_len,obj) = let obj = if fresh_instances then CicNotationUtil.freshen_obj obj else obj @@ -1004,6 +1103,6 @@ in refine_profiler.HExtlib.profile foo () disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj - obj + (text,prefix_len,obj) end