From: Claudio Sacerdoti Coen Date: Wed, 3 Dec 2008 22:53:01 +0000 (+0000) Subject: The aliases and multi_aliases in the lexicon status are now X-Git-Tag: make_still_working~4461 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9a9c5b863f68367119450ae7b806d454ba1265e3;p=helm.git The aliases and multi_aliases in the lexicon status are now LexiconAst.alias_spec (they used to be DisambiguateTypes.codomain_item). Benefit: it is now possible to use the very same set of aliases both for the new and old terms. Moreover, this commits simplifies quite a bit of code. Known bugs: when clicking the "OK" button in the error message disambiguation window, an assertion is often raised. When the assertion is not raised, the set of aliases that are printed are not syntactically/semantically correct. --- diff --git a/helm/software/components/cic_disambiguation/Makefile b/helm/software/components/cic_disambiguation/Makefile index 2dc2984de..2fb5de515 100644 --- a/helm/software/components/cic_disambiguation/Makefile +++ b/helm/software/components/cic_disambiguation/Makefile @@ -1,8 +1,8 @@ PACKAGE = cic_disambiguation NOTATIONS = number INTERFACE_FILES = \ - disambiguateChoices.mli \ - cicDisambiguate.mli + cicDisambiguate.mli \ + disambiguateChoices.mli IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(patsubst %,%_notation.ml,$(NOTATIONS)) diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index 97f24c190..288be5fa2 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -99,8 +99,8 @@ let refine_obj metasenv subst context uri ~use_coercions obj ugraph process_exn Stdpp.dummy_loc exn ;; -let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl +let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri + ~is_path ast ~localization_tbl ~obj_context = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); @@ -112,8 +112,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve env - (DisambiguateTypes.Symbol (symb, i)) ~args:cic_args () + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args) | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> @@ -125,8 +125,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | `Pi | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) | `Exists -> - Disambiguate.resolve env (DisambiguateTypes.Symbol ("exists", 0)) - ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Symbol ("exists", 0)) + (`Args [ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ])) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context None outtype in @@ -152,8 +153,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast match indty_ident with | Some (indty_ident, _) -> (match - Disambiguate.resolve env - (DisambiguateTypes.Id indty_ident) () + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Id indty_ident) (`Args []) with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) | Cic.Implicit _ -> @@ -169,8 +170,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | (Ast.Wildcard, _) :: tl -> fst_constructor tl | [] -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))) in - (match Disambiguate.resolve env - (DisambiguateTypes.Id (fst_constructor branches)) () with + (match Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Id (fst_constructor branches)) + (`Args []) with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) | Cic.Implicit _ -> @@ -399,7 +401,12 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast with UriManager.IllFormedUri _ -> CicNotationPt.fail loc "Ill formed URI" else - Disambiguate.resolve env (DisambiguateTypes.Id name) () + try + List.assoc name obj_context + with + Not_found -> + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Id name) (`Args []) in let mk_subst uris = let ids_to_uris = @@ -462,7 +469,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment"))))) | CicNotationPt.Implicit -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) - | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (DisambiguateTypes.Num i) ~num () + | CicNotationPt.Num (num, i) -> + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Num i) (`Num_arg num) | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -477,7 +486,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) | CicNotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve env (DisambiguateTypes.Symbol (symbol, instance)) () + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Symbol (symbol, instance)) (`Args []) | _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> Cic.Implicit annotation @@ -489,14 +499,17 @@ let interpretate_path ~context path = let localization_tbl = Cic.CicHash.create 23 in (* here we are throwing away useful localization informations!!! *) fst ( - interpretate_term ~create_dummy_ids:true + interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true - path ~localization_tbl, localization_tbl) + path ~localization_tbl ~obj_context:[], localization_tbl) -let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = +let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj + ~localization_tbl += assert (context = []); assert (is_path = false); - let interpretate_term = interpretate_term ~localization_tbl in + let interpretate_term ?(obj_context=[]) = + interpretate_term ~mk_choice ~localization_tbl ~obj_context in match obj with | CicNotationPt.Inductive (params,tyl) -> let uri = match uri with Some uri -> uri | None -> assert false in @@ -515,14 +528,12 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = context,List.rev res in let add_params = List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in - let name_to_uris = + let obj_context = snd ( List.fold_left (*here the explicit_named_substituion is assumed to be of length 0 *) - (fun (i,res) (name,_,_,_) -> - i + 1,(name,name,Cic.MutInd (uri,i,[]))::res - ) (0,[]) tyl) in - let con_env = DisambiguateTypes.env_of_list name_to_uris env in + (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res) + (0,[]) tyl) in let tyl = List.map (fun (name,b,ty,cl) -> @@ -531,7 +542,9 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = List.map (fun (name,ty) -> let ty' = - add_params (interpretate_term context con_env None false ty) + add_params + (interpretate_term ~obj_context ~context ~env ~uri:None + ~is_path:false ty) in name,ty' ) cl @@ -596,17 +609,14 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = Cic.Constant (name,bo',ty',[],attrs)) ;; -let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl +let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri + ~is_path ast ~localization_tbl = - let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in -interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast -~localization_tbl -;; - -let mk_implicit = - function true -> Cic.Implicit (Some `Closed) - | _ -> Cic.Implicit None + let context = + List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context + in + interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path + ast ~localization_tbl ~obj_context:[] ;; let string_context_of_context = @@ -614,9 +624,9 @@ let string_context_of_context = (Cic.Anonymous,_) -> Some "_");; let disambiguate_term ~context ~metasenv ~subst ?goal - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe - ~lookup_in_library - (text,prefix_len,term) + ?(initial_ugraph = CicUniv.oblivion_ugraph) + ~mk_implicit ~description_of_alias ~mk_choice + ~aliases ~universe ~lookup_in_library (text,prefix_len,term) = let hint = match goal with | None -> (fun _ x -> x), fun k -> k @@ -634,29 +644,29 @@ let disambiguate_term ~context ~metasenv ~subst ?goal in let localization_tbl = Cic.CicHash.create 503 in MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst - ~initial_ugraph ~aliases ~mk_implicit ~string_context_of_context - ~universe ~lookup_in_library + ~initial_ugraph ~aliases ~string_context_of_context + ~universe ~lookup_in_library ~mk_implicit ~description_of_alias ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:Disambiguate.domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice) ~refine_thing:refine_term (text,prefix_len,term) ~localization_tbl ~hint ~freshen_thing:CicNotationUtil.freshen_term ~passes:(MultiPassDisambiguator.passes ()) -let disambiguate_obj ~aliases ~universe ~uri ~lookup_in_library - (text,prefix_len,obj) +let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice + ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = let hint = (fun _ x -> x), fun k -> k in let localization_tbl = Cic.CicHash.create 503 in MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] - ~aliases ~universe ~uri ~mk_implicit ~string_context_of_context - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~aliases ~universe ~uri ~string_context_of_context + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:Disambiguate.domain_of_obj - ~lookup_in_library + ~lookup_in_library ~mk_implicit ~description_of_alias ~initial_ugraph:CicUniv.empty_ugraph - ~interpretate_thing:interpretate_obj + ~interpretate_thing:(interpretate_obj ~mk_choice) ~refine_thing:refine_obj ~localization_tbl ~hint diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli index 0e228de10..86ede901c 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli @@ -33,16 +33,18 @@ val disambiguate_term : subst:Cic.substitution -> ?goal:int -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> + mk_implicit:(bool -> 'alias) -> + description_of_alias:('alias -> string) -> + mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> + 'alias list) -> CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.domain_item * 'alias) list * Cic.metasenv * Cic.substitution * Cic.term* @@ -50,17 +52,19 @@ val disambiguate_term : bool val disambiguate_obj : - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> - uri:UriManager.uri option -> (* required only for inductive types *) + mk_implicit:(bool -> 'alias) -> + description_of_alias:('alias -> string) -> + mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> + 'alias list) -> + uri:UriManager.uri option -> (* required only for inductive types *) CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.domain_item * 'alias) list * Cic.metasenv * Cic.substitution * Cic.obj * diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml index ed3f82fe8..b540033dc 100644 --- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml +++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml @@ -46,7 +46,8 @@ let lookup_num_by_dsc dsc = let mk_choice ~mk_appl ~mk_implicit ~term_of_uri (dsc, args, appl_pattern)= dsc, - (fun env _ cic_args -> + `Sym_interp + (fun cic_args -> let env',rest = let names = List.map (function CicNotationPt.IdentArg (_, name) -> name) args @@ -75,7 +76,7 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_uri (dsc, args, appl_pattern)= let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri symbol dsc = try - mk_choice~mk_appl ~mk_implicit ~term_of_uri + mk_choice ~mk_appl ~mk_implicit ~term_of_uri (List.find (fun (dsc', _, _) -> dsc = dsc') (TermAcicContent.lookup_interpretations symbol)) diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml index 37547bf58..06099dcfe 100644 --- a/helm/software/components/cic_disambiguation/number_notation.ml +++ b/helm/software/components/cic_disambiguation/number_notation.ml @@ -28,16 +28,16 @@ let _ = DisambiguateChoices.add_num_choice ("natural number", - (fun _ num _ -> LibraryObjects.build_nat (int_of_string num))); + `Num_interp (fun num -> LibraryObjects.build_nat (int_of_string num))); DisambiguateChoices.add_num_choice ("Coq natural number", - (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); + `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num))); DisambiguateChoices.add_num_choice ("real number", - (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num))); + `Num_interp (fun num -> HelmLibraryObjects.build_real (int_of_string num))); DisambiguateChoices.add_num_choice ("binary positive number", - (fun _ num _ -> + `Num_interp (fun num -> let num = int_of_string num in if num = 0 then raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number"))) @@ -45,7 +45,7 @@ let _ = HelmLibraryObjects.build_bin_pos num)); DisambiguateChoices.add_num_choice ("binary integer number", - (fun _ num _ -> + `Num_interp (fun num -> let num = int_of_string num in if num = 0 then HelmLibraryObjects.BinInt.z0 diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index 12b7b01a9..748722f5d 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -43,7 +43,7 @@ exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) exception Try_again of string Lazy.t -type 'term aliases = bool * 'term DisambiguateTypes.environment +type ('alias,'term) aliases= bool * 'term DisambiguateTypes.environment type 'a disambiguator_input = string * int * 'a type domain = domain_tree list @@ -108,9 +108,13 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t -let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = +let resolve ~env ~mk_choice (item: domain_item) arg = try - snd (Environment.find item env) env num args + match snd (mk_choice (Environment.find item env)), 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)) @@ -327,7 +331,7 @@ let domain_of_obj ~context ast = List.map (fun (_,ty) -> domain_of_term context_w_types ty) cl)) tyl) - | CicNotationPt.Record (params,var,ty,fields) -> + | Ast.Record (params,var,ty,fields) -> let context, dom = List.fold_left (fun (context, dom) (var, ty) -> @@ -382,29 +386,27 @@ sig metasenv:'metasenv -> subst:'subst -> use_coercions:bool -> - mk_implicit:(bool -> 'refined_term) -> string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * (('refined_thing,'metasenv,'subst,'ugraph) test_result -> ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> - aliases:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - universe:'refined_term DisambiguateTypes.codomain_item list - DisambiguateTypes.Environment.t option -> + mk_implicit:(bool -> 'alias) -> + description_of_alias:('alias -> string) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> - 'refined_term DisambiguateTypes.codomain_item list) -> + 'alias list) -> uri:'uri -> pp_thing:('ast_thing -> string) -> domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> interpretate_thing:( context:'context -> - env:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> + env:'alias DisambiguateTypes.Environment.t -> uri:'uri -> is_path:bool -> 'ast_thing -> @@ -416,8 +418,7 @@ sig ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> localization_tbl:'cichash -> string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * - 'refined_term DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.Environment.key * 'alias) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool end @@ -428,8 +429,9 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~context ~metasenv ~subst ~use_coercions - ~mk_implicit ~string_context_of_context + ~string_context_of_context ~initial_ugraph:base_univ ~hint + ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl @@ -455,26 +457,23 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" (* (2) lookup function for any item (Id/Symbol/Num) *) let lookup_choices = fun item -> - let choices = - match universe with - | None -> - lookup_in_library - C.interactive_user_uri_choice - C.input_or_locate_uri item - | Some e -> - (try - let item = - match item with - | Symbol (symb, _) -> Symbol (symb, 0) - | item -> item - in - Environment.find item e - with Not_found -> - lookup_in_library - C.interactive_user_uri_choice - C.input_or_locate_uri item) - in - choices + match universe with + | None -> + lookup_in_library + C.interactive_user_uri_choice + C.input_or_locate_uri item + | Some e -> + (try + let item = + match item with + | Symbol (symb, _) -> Symbol (symb, 0) + | item -> item + in + Environment.find item e + with Not_found -> + lookup_in_library + C.interactive_user_uri_choice + C.input_or_locate_uri item) in (* (* *) @@ -504,20 +503,17 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" (* (3) test an interpretation filling with meta uninterpreted identifiers *) let test_env aliases todo_dom ugraph = - let rec aux env = function + try + let rec aux env = function | [] -> env | Node (_, item, l) :: tl -> let env = Environment.add item - ("Implicit", - (match item with - | Id _ | Num _ -> - (fun _ _ _ -> mk_implicit true) - | Symbol _ -> (fun _ _ _ -> mk_implicit false))) + (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 - try + let filled_env = aux aliases todo_dom in let cic_thing = interpretate_thing ~context ~env:filled_env ~uri ~is_path:false thing ~localization_tbl @@ -613,7 +609,7 @@ in refine_profiler.HExtlib.profile foo () let rec filter = function | [] -> [],[],[] | codomain_item :: tl -> - debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + (*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 @@ -665,7 +661,8 @@ in refine_profiler.HExtlib.profile foo () | Ok _ | Uncertain _ -> aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in + | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] + in let res = match aux' aliases [] None todo_dom with | [],uncertain,errors -> @@ -682,14 +679,14 @@ in refine_profiler.HExtlib.profile foo () (fun locs domain_item -> try let description = - fst (Environment.find domain_item env) + 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,fst b) diff in + let diff= List.map (fun a,b -> a,description_of_alias b) diff in env',diff,loc_msg,significant ) errors in @@ -706,7 +703,7 @@ in refine_profiler.HExtlib.profile foo () map_domain (fun locs domain_item -> let description = - fst (Environment.find domain_item env) + description_of_alias (Environment.find domain_item env) in locs,descr_of_domain_item domain_item, description) thing_dom) diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli index 310b74b8b..5088f8a5f 100644 --- a/helm/software/components/disambiguation/disambiguate.mli +++ b/helm/software/components/disambiguation/disambiguate.mli @@ -55,9 +55,10 @@ type ('term,'metasenv,'subst,'graph) test_result = exception Try_again of string Lazy.t val resolve : - 'term DisambiguateTypes.environment -> + env:'alias DisambiguateTypes.Environment.t -> + mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) -> DisambiguateTypes.Environment.key -> - ?num:string -> ?args:'term list -> unit -> 'term + [`Num_arg of string | `Args of 'term list] -> 'term val find_in_context: string -> string option list -> int val domain_of_ast_term: context: @@ -74,29 +75,27 @@ sig metasenv:'metasenv -> subst:'subst -> use_coercions:bool -> - mk_implicit:(bool -> 'refined_term) -> string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * (('refined_thing,'metasenv,'subst,'ugraph) test_result -> ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> - aliases:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - universe:'refined_term DisambiguateTypes.codomain_item list - DisambiguateTypes.Environment.t option -> + mk_implicit:(bool -> 'alias) -> + description_of_alias:('alias -> string) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> - 'refined_term DisambiguateTypes.codomain_item list) -> + 'alias list) -> uri:'uri -> pp_thing:('ast_thing -> string) -> domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> interpretate_thing:( context:'context -> - env:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> + env:'alias DisambiguateTypes.Environment.t -> uri:'uri -> is_path:bool -> 'ast_thing -> @@ -108,8 +107,7 @@ sig ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> localization_tbl:'cichash -> string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * - 'refined_term DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.Environment.key * 'alias) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool end diff --git a/helm/software/components/disambiguation/disambiguateTypes.ml b/helm/software/components/disambiguation/disambiguateTypes.ml index 0ed285af0..eb1239523 100644 --- a/helm/software/components/disambiguation/disambiguateTypes.ml +++ b/helm/software/components/disambiguation/disambiguateTypes.ml @@ -25,16 +25,6 @@ (* $Id$ *) -(* -type term = CicNotationPt.term -type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic -type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical -type script_entry = - | Command of tactical - | Comment of CicNotationPt.location * string -type script = CicNotationPt.location * script_entry list -*) - type domain_item = | Id of string (* literal *) | Symbol of string * int (* literal, instance num *) @@ -65,11 +55,11 @@ struct with Not_found -> find (Num 0) env) | _ -> find k env - let cons k v env = + let cons desc_of_alias k v env = try let current = find k env in - let dsc, _ = v in - add k (v :: (List.filter (fun (dsc', _) -> dsc' <> dsc) current)) env + let dsc = desc_of_alias v in + add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env with Not_found -> add k [v] env @@ -87,24 +77,13 @@ end type 'term codomain_item = string * (* description *) - ('term environment -> string -> 'term list -> 'term) - (* environment, literal number, arguments as needed *) + [`Num_interp of string -> 'term + |`Sym_interp of 'term list -> 'term] and 'term environment = 'term codomain_item Environment.t -type 'term multiple_environment = 'term codomain_item list Environment.t - - -(** adds a (name,uri) list l to a disambiguation environment e **) -let multiple_env_of_list l e = - List.fold_left - (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e) - e l - -let env_of_list l e = - List.fold_left - (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e) - e l +type 'term multiple_environment = + 'term codomain_item list Environment.t type interactive_user_uri_choice_type = selection_mode:[`SINGLE | `MULTIPLE] -> diff --git a/helm/software/components/disambiguation/disambiguateTypes.mli b/helm/software/components/disambiguation/disambiguateTypes.mli index ae157e268..15f9d8d30 100644 --- a/helm/software/components/disambiguation/disambiguateTypes.mli +++ b/helm/software/components/disambiguation/disambiguateTypes.mli @@ -32,7 +32,7 @@ type domain_item = module Environment: sig include Map.S with type key = domain_item - val cons: domain_item -> ('a * 'b) -> ('a * 'b) list t -> ('a * 'b) list t + val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t val hd: 'a list t -> 'a t (** last alias cons-ed will be processed first *) @@ -45,20 +45,13 @@ exception Invalid_choice of (Stdpp.location * string) Lazy.t type 'term codomain_item = string * (* description *) - ('term environment -> string -> 'term list -> 'term) - (* environment, literal number, arguments as needed *) + [`Num_interp of string -> 'term + |`Sym_interp of 'term list -> 'term] and 'term environment = 'term codomain_item Environment.t -type 'term multiple_environment = 'term codomain_item list Environment.t - -(* a simple case of extension of a disambiguation environment *) -val env_of_list: - (string * string * 'term) list -> 'term environment -> 'term environment - -val multiple_env_of_list: - (string * string * 'term) list -> 'term multiple_environment -> - 'term multiple_environment +type 'term multiple_environment = + 'term codomain_item list Environment.t type interactive_user_uri_choice_type = selection_mode:[`SINGLE | `MULTIPLE] -> diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index af4a9e49e..039fdd57a 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -89,8 +89,11 @@ let passes () = (* *) ] ;; -let drop_aliases ?(minimize_instances=false) (choices, user_asked) = +let drop_aliases ?(minimize_instances=false) ~description_of_alias + (choices, user_asked) += let module D = DisambiguateTypes in + let compare ci1 ci2 = description_of_alias ci1 = description_of_alias ci2 in let minimize d = if not minimize_instances then d @@ -98,23 +101,23 @@ let drop_aliases ?(minimize_instances=false) (choices, user_asked) = let rec aux = function [] -> [] - | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 -> + | (D.Symbol (s,n),ci1) as he::tl when n > 0 -> if List.for_all (function - (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2 + (D.Symbol (s2,_),ci2) -> s2 <> s || compare ci1 ci2 | _ -> true ) d then - (D.Symbol (s,0),ci)::(aux tl) + (D.Symbol (s,0),ci1)::(aux tl) else he::(aux tl) - | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 -> + | (D.Num n,ci1) as he::tl when n > 0 -> if List.for_all - (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d + (function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d then - (D.Num 0,ci)::(aux tl) + (D.Num 0,ci1)::(aux tl) else he::(aux tl) | he::tl -> he::(aux tl) @@ -128,7 +131,8 @@ let drop_aliases_and_clear_diff (choices, user_asked) = (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices), user_asked -let disambiguate_thing ~passes ~aliases ~universe ~f thing = +let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing += assert (universe <> None); let library = false, DisambiguateTypes.Environment.empty, None in let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in @@ -145,9 +149,9 @@ let disambiguate_thing ~passes ~aliases ~universe ~f thing = in let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = if use_mono_aliases then - drop_aliases ~minimize_instances:true res (* one shot aliases *) + drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *) else if user_asked then - drop_aliases ~minimize_instances:true res (* one shot aliases *) + drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *) else drop_aliases_and_clear_diff res in @@ -169,19 +173,18 @@ let disambiguate_thing ~passes ~aliases ~universe ~f thing = aux 1 [] passes let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst - ~mk_implicit ~string_context_of_context ~initial_ugraph ~hint ~aliases - ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing - ~interpretate_thing ~refine_thing ~localization_tbl thing + ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit + ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing + ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl thing = let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) = let thing = if fresh_instances then freshen_thing thing else thing in Disambiguator.disambiguate_thing - ~context ~metasenv ~subst ~use_coercions - ~mk_implicit ~string_context_of_context - ~initial_ugraph ~hint + ~context ~metasenv ~subst ~use_coercions ~string_context_of_context + ~initial_ugraph ~hint ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl (txt,len,thing) in - disambiguate_thing ~passes ~aliases ~universe ~f thing + disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli index 7a4ae53aa..27d5ca618 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.mli +++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli @@ -61,30 +61,29 @@ val disambiguate_thing: context:'context -> metasenv:'metasenv -> subst:'subst -> - mk_implicit:(bool -> 'refined_term) -> string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * (('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result -> ('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result) -> - aliases:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - universe:'refined_term DisambiguateTypes.codomain_item list + mk_implicit:(bool -> 'alias) -> + description_of_alias:('alias -> string) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> - 'refined_term DisambiguateTypes.codomain_item list) -> + 'alias list) -> uri:'uri -> pp_thing:('ast_thing -> string) -> domain_of_thing: (context: string option list -> 'ast_thing -> Disambiguate.domain) -> interpretate_thing:( context:'context -> - env:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> + env:'alias DisambiguateTypes.Environment.t -> uri:'uri -> is_path:bool -> 'ast_thing -> @@ -96,7 +95,6 @@ val disambiguate_thing: ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) -> localization_tbl:'cichash -> string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * - 'refined_term DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.Environment.key * 'alias) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool diff --git a/helm/software/components/grafite_parser/cicNotation2.mli b/helm/software/components/grafite_parser/cicNotation2.mli index 972c55b51..9b47d8d6d 100644 --- a/helm/software/components/grafite_parser/cicNotation2.mli +++ b/helm/software/components/grafite_parser/cicNotation2.mli @@ -29,8 +29,9 @@ val parse_environment: include_paths:string list -> string -> - Cic.term DisambiguateTypes.environment * - Cic.term DisambiguateTypes.multiple_environment + LexiconAst.alias_spec DisambiguateTypes.Environment.t * + LexiconAst.alias_spec list DisambiguateTypes.Environment.t + (** @param fname file from which load notation *) val load_notation: include_paths:string list -> string -> LexiconEngine.status diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index a6c9effd7..58666eed5 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -45,6 +45,7 @@ let singleton msg = function in HLog.debug debug; assert false +(* let cic_codomain_of_uri uri = (UriManager.string_of_uri uri, let term = @@ -55,16 +56,34 @@ let cic_codomain_of_uri uri = in fun _ _ _ -> term) ;; - -let cic_num_choices = DisambiguateChoices.lookup_num_choices;; +*) -let cic_mk_choice = - DisambiguateChoices.mk_choice - ~mk_implicit:(function - | true -> Cic.Implicit (Some `Type) - | false -> Cic.Implicit None) - ~mk_appl:(function (Cic.Appl l)::tl -> Cic.Appl (l@tl) | l -> Cic.Appl l) - ~term_of_uri:CicUtil.term_of_uri +(*let cic_num_choices = DisambiguateChoices.lookup_num_choices;;*) + +let __Implicit = "__Implicit__" +let __Closed_Implicit = "__Closed_Implicit__" + +let cic_mk_choice = function + | LexiconAst.Symbol_alias (name, _, dsc) -> + if name = __Implicit then + dsc, `Sym_interp (fun _ -> Cic.Implicit None) + else if name = __Closed_Implicit then + dsc, `Sym_interp (fun _ -> Cic.Implicit (Some `Closed)) + else + DisambiguateChoices.cic_lookup_symbol_by_dsc name dsc + | LexiconAst.Number_alias (_, dsc) -> + DisambiguateChoices.lookup_num_by_dsc dsc + | LexiconAst.Ident_alias (name, uri) -> + uri, `Sym_interp + (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri)) +;; + +let cic_mk_implicit b = + match b with + | false -> + LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit") + | true -> + LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") ;; let ncic_codomain_of_uri uri = @@ -79,7 +98,6 @@ let ncic_codomain_of_uri uri = ;; let ncic_num_choices _ = (*assert false*) [];; - let ncic_mk_choice = DisambiguateChoices.mk_choice ~mk_implicit:(function @@ -91,9 +109,19 @@ let ncic_mk_choice = ;; let lookup_in_library - codomain_of_uri mk_choice num_choices interactive_user_uri_choice input_or_locate_uri item = + let mk_ident_alias id u = + LexiconAst.Ident_alias (id,UriManager.string_of_uri u) + in + let mk_num_alias instance = + List.map + (fun dsc,_ -> LexiconAst.Number_alias (instance,dsc)) + (DisambiguateChoices.lookup_num_choices()) + in + let mk_symbol_alias symb ino (dsc, _,_) = + LexiconAst.Symbol_alias (symb,ino,dsc) + in let dbd = LibraryDb.instance () in let choices_of_id id = let uris = Whelp.locate ~dbd id in @@ -120,13 +148,14 @@ let lookup_in_library match item with | DisambiguateTypes.Id id -> let uris = choices_of_id id in - List.map codomain_of_uri uris - | DisambiguateTypes.Symbol (symb, _) -> + List.map (mk_ident_alias id) uris + | DisambiguateTypes.Symbol (symb, ino) -> (try - List.map mk_choice (TermAcicContent.lookup_interpretations symb) + List.map (mk_symbol_alias symb ino) + (TermAcicContent.lookup_interpretations symb) with TermAcicContent.Interpretation_not_found -> []) - | DisambiguateTypes.Num instance -> num_choices () + | DisambiguateTypes.Num instance -> mk_num_alias instance ;; (** @param term not meaningful when context is given *) @@ -138,8 +167,10 @@ term = (CicDisambiguate.disambiguate_term ~aliases:lexicon_status.LexiconEngine.aliases ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) - ~lookup_in_library:(lookup_in_library cic_codomain_of_uri cic_mk_choice - cic_num_choices) + ~lookup_in_library + ~mk_choice:cic_mk_choice + ~mk_implicit:cic_mk_implicit + ~description_of_alias:LexiconAst.description_of_alias ~context ~metasenv ~subst:[] (text,prefix_len,term)) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in @@ -158,8 +189,10 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = let (diff, metasenv, _, cic, ugraph) = singleton "second" (CicDisambiguate.disambiguate_term - ~lookup_in_library:(lookup_in_library cic_codomain_of_uri - cic_mk_choice cic_num_choices) + ~lookup_in_library + ~mk_choice:cic_mk_choice + ~mk_implicit:cic_mk_implicit + ~description_of_alias:LexiconAst.description_of_alias ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~context ~metasenv ~subst:[] ?goal @@ -574,8 +607,10 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let (diff, metasenv, _, cic, _) = singleton "third" (CicDisambiguate.disambiguate_obj - ~lookup_in_library:(lookup_in_library cic_codomain_of_uri cic_mk_choice - cic_num_choices) + ~lookup_in_library + ~mk_choice:cic_mk_choice + ~mk_implicit:cic_mk_implicit + ~description_of_alias:LexiconAst.description_of_alias ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri (text,prefix_len,obj)) in diff --git a/helm/software/components/lexicon/lexiconAst.ml b/helm/software/components/lexicon/lexiconAst.ml index 5a09d590a..0c588d189 100644 --- a/helm/software/components/lexicon/lexiconAst.ml +++ b/helm/software/components/lexicon/lexiconAst.ml @@ -55,3 +55,8 @@ type command = (* composed magic: term + command magics. No need to change this value *) let magic = magic + 10000 * CicNotationPt.magic +let description_of_alias = + function + Ident_alias (_,desc) + | Symbol_alias (_,_,desc) + | Number_alias (_,desc) -> desc diff --git a/helm/software/components/lexicon/lexiconAstPp.ml b/helm/software/components/lexicon/lexiconAstPp.ml index ad317bec7..02383f4b8 100644 --- a/helm/software/components/lexicon/lexiconAstPp.ml +++ b/helm/software/components/lexicon/lexiconAstPp.ml @@ -33,14 +33,14 @@ let pp_l1_pattern = CicNotationPp.pp_term let pp_l2_pattern = CicNotationPp.pp_term let pp_alias = function - | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri + | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri | Symbol_alias (symb, instance, desc) -> - sprintf "alias symbol \"%s\" %s= \"%s\"" + sprintf "alias symbol \"%s\" %s= \"%s\"." symb (if instance=0 then "" else "(instance "^ string_of_int instance ^ ") ") desc | Number_alias (instance,desc) -> - sprintf "alias num (instance %d) = \"%s\"" instance desc + sprintf "alias num (instance %d) = \"%s\"." instance desc let pp_associativity = function | Gramext.LeftA -> "left associative" diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index cd7b0123d..22d9b2f33 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -34,8 +34,8 @@ exception IncludedFileNotCompiled of string * string exception MetadataNotFound of string (* file name *) type status = { - aliases: Cic.term DisambiguateTypes.environment; (** disambiguation aliases *) - multi_aliases: Cic.term DisambiguateTypes.multiple_environment; + aliases: LexiconAst.alias_spec DisambiguateTypes.Environment.t; + multi_aliases: LexiconAst.alias_spec list DisambiguateTypes.Environment.t; lexicon_content_rev: LexiconMarshal.lexicon; notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) } @@ -69,25 +69,25 @@ let set_proof_aliases mode status new_aliases = else let commands_of_aliases = List.map - (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) + (fun _,alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) in let aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) status.aliases new_aliases in let multi_aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) - status.multi_aliases new_aliases in + List.fold_left (fun acc (d,c) -> + DisambiguateTypes.Environment.cons LexiconAst.description_of_alias + d c acc) + status.multi_aliases new_aliases + in let new_status = { status with multi_aliases = multi_aliases ; aliases = aliases} in if new_aliases = [] then new_status else - let aliases = - DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases - in let status = - add_lexicon_content (commands_of_aliases aliases) new_status + add_lexicon_content (commands_of_aliases new_aliases) new_status in status @@ -107,10 +107,11 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = -> let item = DisambiguateTypes.Id id in (try - let t = - snd (DisambiguateTypes.Environment.find item status.aliases) - status.aliases "" [] in - let uri = CicUtil.uri_of_term t in + let uri = + match DisambiguateTypes.Environment.find item status.aliases with + LexiconAst.Ident_alias (_, uri)-> UriManager.uri_of_string uri + | _ -> assert false + in CicNotationPt.UriPattern uri with Not_found -> prerr_endline ("Domain item not found: " ^ @@ -148,14 +149,11 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = code in DisambiguatePp *) match spec with | LexiconAst.Ident_alias (id,uri) -> - [DisambiguateTypes.Id id, - (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] + [DisambiguateTypes.Id id,spec] | LexiconAst.Symbol_alias (symb, instance, desc) -> - [DisambiguateTypes.Symbol (symb,instance), - DisambiguateChoices.cic_lookup_symbol_by_dsc symb desc] + [DisambiguateTypes.Symbol (symb,instance),spec] | LexiconAst.Number_alias (instance,desc) -> - [DisambiguateTypes.Num instance, - DisambiguateChoices.lookup_num_by_dsc desc] + [DisambiguateTypes.Num instance,spec] in set_proof_aliases mode status diff | LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm -> @@ -163,7 +161,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = let diff = try [DisambiguateTypes.Symbol (symbol, 0), - DisambiguateChoices.cic_lookup_symbol_by_dsc symbol dsc] + LexiconAst.Symbol_alias (symbol,0,dsc)] with DisambiguateChoices.Choice_not_found msg -> prerr_endline (Lazy.force msg); diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli index 8447eb035..27d9b05eb 100644 --- a/helm/software/components/lexicon/lexiconEngine.mli +++ b/helm/software/components/lexicon/lexiconEngine.mli @@ -26,8 +26,8 @@ exception IncludedFileNotCompiled of string * string type status = { - aliases: Cic.term DisambiguateTypes.environment;(** disambiguation aliases *) - multi_aliases: Cic.term DisambiguateTypes.multiple_environment; + aliases: LexiconAst.alias_spec DisambiguateTypes.Environment.t; + multi_aliases: LexiconAst.alias_spec list DisambiguateTypes.Environment.t; lexicon_content_rev: LexiconMarshal.lexicon; notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) } @@ -37,9 +37,7 @@ val initial_status: status val eval_command : status -> LexiconAst.command -> status val set_proof_aliases: - status -> - (DisambiguateTypes.Environment.key * - Cic.term DisambiguateTypes.codomain_item) list -> + status -> (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list -> status (* this callback is called on every lexicon command *) diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml index ed243fe19..a3a0d766e 100644 --- a/helm/software/components/lexicon/lexiconSync.ml +++ b/helm/software/components/lexicon/lexiconSync.ml @@ -28,9 +28,13 @@ let alias_diff ~from status = let module Map = DisambiguateTypes.Environment in Map.fold - (fun domain_item (description1,_ as codomain_item) acc -> + (fun domain_item codomain_item acc -> + let description1 = LexiconAst.description_of_alias codomain_item in try - let description2,_ = Map.find domain_item from.LexiconEngine.aliases in + let description2 = + LexiconAst.description_of_alias + (Map.find domain_item from.LexiconEngine.aliases) + in if description1 <> description2 then (domain_item,codomain_item)::acc else @@ -39,6 +43,7 @@ let alias_diff ~from status = Not_found -> (domain_item,codomain_item)::acc) status.LexiconEngine.aliases [] +;; let alias_diff = let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in @@ -60,8 +65,8 @@ let extract_alias types uri = let build_aliases = List.map (fun (name,uri) -> - DisambiguateTypes.Id name, - (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri)) + DisambiguateTypes.Id name, LexiconAst.Ident_alias (name, + UriManager.string_of_uri uri)) let add_aliases_for_inductive_def status types uri = let aliases = build_aliases (extract_alias types uri) in diff --git a/helm/software/components/lexicon/lexiconSync.mli b/helm/software/components/lexicon/lexiconSync.mli index 03875690a..fd3892747 100644 --- a/helm/software/components/lexicon/lexiconSync.mli +++ b/helm/software/components/lexicon/lexiconSync.mli @@ -35,8 +35,7 @@ val time_travel: * order to be equal to aliases of the second argument *) val alias_diff: from:LexiconEngine.status -> LexiconEngine.status -> - (DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list + (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list val push: unit -> unit val pop: unit -> unit diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 8dd4bc634..267b40a20 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -61,7 +61,8 @@ let find_in_context name context = aux 1 context let interpretate_term - ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl + ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast + ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); @@ -74,7 +75,7 @@ let interpretate_term | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args () + Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args) | CicNotationPt.Appl terms -> NCic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> @@ -86,8 +87,8 @@ let interpretate_term | `Pi | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) | `Exists -> - Disambiguate.resolve env (Symbol ("exists", 0)) - ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ()) + Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0)) + (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context `Term outtype in @@ -125,7 +126,8 @@ let interpretate_term let indtype_ref = match indty_ident with | Some (indty_ident, _) -> - (match Disambiguate.resolve env (Id indty_ident) () with + (match Disambiguate.resolve ~env ~mk_choice + (Id indty_ident) (`Args []) with | NCic.Const r -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again @@ -144,7 +146,8 @@ let interpretate_term "because it is an inductive type without constructors "^ "or because all patterns use wildcards"))) in - (match Disambiguate.resolve env (Id (fst_constructor branches)) () with + (match Disambiguate.resolve ~env ~mk_choice + (Id (fst_constructor branches)) (`Args []) with | NCic.Const r -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again @@ -348,7 +351,8 @@ let interpretate_term assert (subst = None); (try NCic.Rel (find_in_context name context) - with Not_found -> Disambiguate.resolve env (Id name) ()) + with Not_found -> + Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) | CicNotationPt.Uri (name, subst) -> assert (subst = None); (try @@ -358,7 +362,8 @@ let interpretate_term | CicNotationPt.Implicit -> NCic.Implicit `Term | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole) patterns not implemented *) - | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (Num i) ~num () + | CicNotationPt.Num (num, i) -> + Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -373,7 +378,8 @@ patterns not implemented *) | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"]) | CicNotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve env (Symbol (symbol, instance)) () + Disambiguate.resolve ~env ~mk_choice + (Symbol (symbol, instance)) (`Args []) | _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> NCic.Implicit annotation @@ -401,6 +407,7 @@ let domain_of_term ~context = ;; let disambiguate_term ~context ~metasenv ~subst ?goal + ~mk_implicit ~description_of_alias ~mk_choice ~aliases ~universe ~lookup_in_library (text,prefix_len,term) = @@ -423,15 +430,15 @@ let disambiguate_term ~context ~metasenv ~subst ?goal MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_term ~context ~metasenv ~initial_ugraph:() ~aliases + ~mk_implicit ~description_of_alias ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~mk_implicit:(function false -> NCic.Implicit `Term - | true -> NCic.Implicit `Closed) ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) + ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) ~localization_tbl ~hint ~subst in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; + diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index ffcd8f99b..741bd3d0f 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -16,16 +16,18 @@ val disambiguate_term : metasenv:NCic.metasenv -> subst:NCic.substitution -> ?goal:int -> - aliases:NCic.term DisambiguateTypes.environment -> - universe:NCic.term DisambiguateTypes.multiple_environment option -> + mk_implicit: (bool -> 'alias) -> + description_of_alias:('alias -> string) -> + mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> - NCic.term DisambiguateTypes.codomain_item list) -> + 'alias list) -> CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - NCic.term DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.domain_item * 'alias) list * NCic.metasenv * NCic.substitution * NCic.term) list * diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 247e07d7a..4437f169c 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -118,7 +118,10 @@ let _ = in addDebugItem "dump aliases" (fun _ -> let status = script#lexicon_status in - HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases)); + HLog.debug (String.concat "\n" + (DisambiguateTypes.Environment.fold + (fun _ x l -> (LexiconAstPp.pp_alias x)::l) + status.LexiconEngine.aliases []))); addDebugItem "dump environment to \"env.dump\"" (fun _ -> let oc = open_out "env.dump" in CicEnvironment.dump_to_channel oc; diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index d0e1c1acb..a5331764e 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -75,7 +75,8 @@ let eval_ast ?do_heavy_checks lexicon_status LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in let _,intermediate_states = List.fold_left - (fun (lexicon_status,acc) (k,((v,_) as value)) -> + (fun (lexicon_status,acc) (k,value) -> + let v = LexiconAst.description_of_alias value in let b = try (* this hack really sucks! *) @@ -141,12 +142,8 @@ let eval_from_stream ~first_statement_only ~include_paths (fun (_,alias) -> match alias with None -> () - | Some (k,((v,_) as value)) -> - let newtxt = - DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k value - DisambiguateTypes.Environment.empty) - in + | Some (k,value) -> + let newtxt = LexiconAstPp.pp_alias value in raise (TryingToAdd newtxt)) new_statuses; let grafite_status,lexicon_status = match new_statuses with diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index bdde2dd39..032ee2c1e 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -32,9 +32,7 @@ val eval_ast : CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement) -> ((GrafiteTypes.status * LexiconEngine.status) * - (DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) option - ) list + (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list (* heavy checks slow down the compilation process but give you some interesting @@ -58,9 +56,7 @@ val eval_from_stream : CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement -> unit) -> ((GrafiteTypes.status * LexiconEngine.status) * - (DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) option - ) list + (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list (* this callback is called on every grafite command *) val set_callback: (GrafiteParser.ast_statement -> unit) -> unit diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 7f4571c55..eb0d83bc7 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -327,11 +327,9 @@ let rec interactive_error_interp ~all_passes String.concat "\n" ("" :: List.map - (fun k,value -> - DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k - (value,(fun _ _ _ -> Cic.Implicit None)) - DisambiguateTypes.Environment.empty)) + (fun k,desc -> + let id = DisambiguateTypes.string_of_domain_item k in + LexiconAstPp.pp_alias (LexiconAst.Ident_alias (id,desc))) diff) ^ "\n" in source_buffer#insert @@ -1486,7 +1484,6 @@ let interactive_string_choice let txt,_ = MatitaGtkMisc.utf8_parsed_text txt (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) in - prerr_endline ("txt:" ^ txt); dialog#uriChoiceLabel#set_label txt; List.iter model#easy_append uris; let return v = diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index d8e66dbf2..fe82e939c 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -94,8 +94,8 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g (fun (acc, to_prepend) (status,alias) -> match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" - | Some (k,((v,_) as value)) -> - let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in + | Some (k,value) -> + let newtxt = LexiconAstPp.pp_alias value in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment in