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 ()
| 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))
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.
| 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 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) =
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
[]
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 _
(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 (
) dom params
in
List.filter
- (fun name ->
+ (fun (_,name) ->
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_,_) -> name = Id name') tyl)
) dom
) (dom @ domain_rev_of_term [] ty) params
in
List.filter
- (fun name->
+ (fun (_,name) ->
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_) -> name = Id name') fields)
) dom
List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
(fun _ -> false) 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
?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*
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 *
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
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 *)
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)));
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
| Ok (thing, metasenv),new_univ ->
[ aliases, diff, metasenv, thing, new_univ ], []
| Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
- | item :: remaining_dom ->
+ | (locs,item) :: remaining_dom ->
debug_print (lazy (sprintf "CHOOSED ITEM: %s"
(string_of_domain_item item)));
let choices =
| Some choices -> choices in
match choices with
[] ->
- [], [None,lazy ("No choices for " ^ string_of_domain_item item)]
+ [], [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
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
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
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
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
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
projects / helm.git / blobdiff