From: Stefano Zacchiroli Date: Mon, 12 Sep 2005 16:02:02 +0000 (+0000) Subject: added support for multi-aliases in disambiguation environment(s) X-Git-Tag: V_0_1_2_1~41 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=35c68efd0a44da26d4aa6ae760ee03712b33dfed;p=helm.git added support for multi-aliases in disambiguation environment(s) --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index c33462f8f..919c33eb7 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -35,7 +35,9 @@ exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) exception Try_again -let debug = false +type aliases = bool * DisambiguateTypes.environment + +let debug = true let debug_print = if debug then prerr_endline else ignore (* @@ -102,7 +104,7 @@ let refine_obj metasenv context uri obj ugraph = (CicPp.ppobj obj) msg); Ko,ugraph -let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = +let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args with Not_found -> @@ -339,8 +341,8 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term | term -> aux dummy_floc context term -let interpretate_path ~context ~env path = - interpretate_term ~context ~env ~uri:None ~is_path:true path +let interpretate_path ~context path = + interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path let interpretate_obj ~context ~env ~uri ~is_path obj = assert (context = []); @@ -367,7 +369,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = (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 + let con_env = DisambiguateTypes.singleton_env_of_list name_to_uris env in let undebrujin t = snd (List.fold_right @@ -577,8 +579,7 @@ and domain_rev_of_term_option loc context = function | None -> [] | Some t -> domain_rev_of_term ~loc context t -let domain_of_term ~context ast = - rev_uniq (domain_rev_of_term context ast) +let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast) let domain_of_obj ~context ast = assert (context = []); @@ -639,26 +640,30 @@ let domain_diff dom1 dom2 = module type Disambiguator = sig val disambiguate_term : + ?fresh_instances:bool -> dbd:Mysql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:environment -> (* previous interpretation status *) + aliases:aliases -> (* previous interpretation status *) CicNotationPt.term -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term* - CicUniv.universe_graph) list (* disambiguated term *) + CicUniv.universe_graph) list * (* disambiguated term *) + bool val disambiguate_obj : + ?fresh_instances:bool -> dbd:Mysql.dbd -> - aliases:environment -> (* previous interpretation status *) + aliases:aliases -> (* previous interpretation status *) uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.obj * - CicUniv.universe_graph) list (* disambiguated obj *) + CicUniv.universe_graph) list * (* disambiguated obj *) + bool end module Make (C: Callbacks) = @@ -694,10 +699,15 @@ module Make (C: Callbacks) = uris let disambiguate_thing ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing = - debug_print "NEW DISAMBIGUATE INPUT"; + debug_print "DISAMBIGUATE INPUT"; + let current_env, multi_aliases_env = + match aliases with + | false, e -> Environment.hd e, None + | true, e -> Environment.empty, Some e + in let disambiguate_context = (* cic context -> disambiguate context *) List.map (function None -> Cic.Anonymous | Some (name, _) -> name) @@ -707,6 +717,8 @@ module Make (C: Callbacks) = let thing_dom = domain_of_thing ~context:disambiguate_context thing in debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" (string_of_domain thing_dom)); + debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s" + (DisambiguatePp.pp_environment (snd aliases))); let current_dom = Environment.fold (fun item _ dom -> item :: dom) current_env [] in @@ -715,25 +727,26 @@ module Make (C: Callbacks) = let lookup_choices = let id_choices = Hashtbl.create 1023 in fun item -> - let choices = - match item with - | Id id -> - (try - Hashtbl.find id_choices id - with Not_found -> - let choices = choices_of_id dbd id in - Hashtbl.add id_choices id choices; - choices) - | Symbol (symb, _) -> - List.map DisambiguateChoices.mk_choice - (CicNotationRew.lookup_interpretations symb) -(* DisambiguateChoices.lookup_symbol_choices symb *) - | Num instance -> DisambiguateChoices.lookup_num_choices () - in - if choices = [] then raise (No_choices item); - choices + let choices = + let lookup_in_library () = + match item with + | Id id -> choices_of_id dbd id + | Symbol (symb, _) -> + List.map DisambiguateChoices.mk_choice + (CicNotationRew.lookup_interpretations symb) + | Num instance -> + DisambiguateChoices.lookup_num_choices () + in + match multi_aliases_env with + | None -> lookup_in_library () + | Some e -> + (try + Environment.find item e + with Not_found -> lookup_in_library ()) + in + if choices = [] then raise (No_choices item); + choices in - (* (* *) let _ = @@ -823,14 +836,10 @@ module Make (C: Callbacks) = match aux current_env todo_dom base_univ with | [] -> raise NoWellTypedInterpretation | [ e,me,t,u ] -> - debug_print "UNA SOLA SCELTA"; - (* Experimental: we forget the environment [e] since we are able - to recompute it. In this way we are forced to do more work - later (since we have less aliases), but we have more freedom - (since we have less aliases) in the future disambiguations. *) - [ current_env,me,t,u] + debug_print "SINGLE INTERPRETATION"; + [ e,me,t,u ], false | l -> - debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); + debug_print (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)); let choices = List.map (fun (env, _, _, _) -> @@ -844,7 +853,7 @@ module Make (C: Callbacks) = l in let choosed = C.interactive_interpretation_choice choices in - List.map (List.nth l) choosed + (List.map (List.nth l) choosed), true in (* (if benchmark then @@ -856,23 +865,36 @@ module Make (C: Callbacks) = !choices_avg (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg))); *) - res + let choices, b = res in + (List.map + (fun (env, metasenv, t, ugraph) -> + Environment.fold Environment.cons env (snd aliases), + metasenv, t, ugraph) + choices), + b with CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" - let disambiguate_term ~dbd ~context ~metasenv + let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term = - disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases - ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term - ~interpretate_thing:interpretate_term ~refine_thing:refine_term term - - let disambiguate_obj ~dbd ~aliases ~uri obj = - disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri - ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj - ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj - obj + let term = + if fresh_instances then CicNotationUtil.freshen_term term else term + in + disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases + ~uri:None ~pp_thing:CicNotationPp.pp_term + ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term + ~refine_thing:refine_term term + + let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~uri obj = + let obj = + if fresh_instances then CicNotationUtil.freshen_obj obj else obj + in + disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri + ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj + ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj + obj end module Trivial = @@ -893,8 +915,8 @@ struct = let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in try - Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast - ?initial_ugraph ~aliases + fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast + ?initial_ugraph ~aliases:(false, aliases)) with Exit -> raise (Ambiguous_term term) end diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 6f74c23c0..10b1c7633 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -29,33 +29,43 @@ exception NoWellTypedInterpretation exception PathNotWellFormed val interpretate_path : - context:Cic.name list -> env:DisambiguateTypes.environment -> - DisambiguateTypes.term -> + context:Cic.name list -> DisambiguateTypes.term -> Cic.term + (** @param multi true if multi aliases are used, false otherwise *) +type aliases = bool * DisambiguateTypes.environment + module type Disambiguator = sig + (** @param fresh_instances when set to true fresh instances will be generated + * for each number _and_ symbol in the disambiguation domain. Instances of the + * input AST will be ignored. Defaults to false. *) val disambiguate_term : + ?fresh_instances:bool -> dbd:Mysql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + aliases:aliases -> (* previous interpretation status *) DisambiguateTypes.term -> (DisambiguateTypes.environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term * - CicUniv.universe_graph) list (* disambiguated term *) + CicUniv.universe_graph) list * (* disambiguated term *) + bool (* has interactive_interpretation_choice been invoked? *) + (** @param fresh_instances as per disambiguate_term *) val disambiguate_obj : + ?fresh_instances:bool -> dbd:Mysql.dbd -> - aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + aliases:aliases -> (* previous interpretation status *) uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> (DisambiguateTypes.environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.obj * - CicUniv.universe_graph) list (* disambiguated obj *) + CicUniv.universe_graph) list * (* disambiguated obj *) + bool (* has interactive_interpretation_choice been invoked? *) end module Make (C : DisambiguateTypes.Callbacks) : Disambiguator diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml index d6a33cfae..24f9ea37e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml @@ -49,7 +49,7 @@ let parse_environment str = Num instance, DisambiguateChoices.lookup_num_by_dsc desc in - environment := Environment.add key value !environment; + environment := Environment.cons key value !environment; done; assert false with End_of_file -> @@ -58,18 +58,21 @@ let parse_environment str = let pp_environment env = let aliases = Environment.fold - (fun domain_item (dsc, _) acc -> - let s = - match domain_item with - | Id id -> - GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "." - | Symbol (symb, i) -> - GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc)) - ^ "." - | Num i -> - GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "." - in - s :: acc) + (fun domain_item codomain_items acc -> + List.fold_left + (fun strings (dsc, _) -> + let s = + match domain_item with + | Id id -> + GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "." + | Symbol (symb, i) -> + GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc)) + ^ "." + | Num i -> + GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "." + in + s :: strings) + acc codomain_items) env [] in String.concat "\n" (List.sort compare aliases) diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 6c530c2bf..bb513aa6c 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -45,17 +45,48 @@ module OrderedDomain = end (* module Domain = Set.Make (OrderedDomain) *) -module Environment = Map.Make (OrderedDomain) +module Environment = +struct + module Environment' = Map.Make (OrderedDomain) + + include Environment' + + let cons 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 + with Not_found -> + add k [v] env + + let hd list_env = + try + map List.hd list_env + with Failure _ -> assert false + + let fold_flatten f env base = + fold + (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc) + env base + +end type codomain_item = string * (* description *) - (environment -> string -> Cic.term list -> Cic.term) + (singleton_environment -> string -> Cic.term list -> Cic.term) (* environment, literal number, arguments as needed *) -and environment = codomain_item Environment.t +and environment = codomain_item list Environment.t + +and singleton_environment = codomain_item Environment.t (** adds a (name,uri) list l to a disambiguation environment e **) let env_of_list l e = + List.fold_left + (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e) + e l + +let singleton_env_of_list l e = List.fold_left (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e) e l diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index b6d74a7fd..1a8dc4ac0 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -29,7 +29,15 @@ type domain_item = | Num of int (* instance num *) (* module Domain: Set.S with type elt = domain_item *) -module Environment: Map.S with type key = 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 hd: 'a list t -> 'a t + + (** last alias cons-ed will be processed first *) + val fold_flatten: (domain_item -> 'a -> 'b -> 'b) -> 'a list t -> 'b -> 'b +end (** to be raised when a choice is invalid due to some given parameter (e.g. * wrong number of Cic.term arguments received) *) @@ -37,13 +45,21 @@ exception Invalid_choice type codomain_item = string * (* description *) - (environment -> string -> Cic.term list -> Cic.term) + (singleton_environment -> string -> Cic.term list -> Cic.term) (* environment, literal number, arguments as needed *) -and environment = codomain_item Environment.t +and environment = codomain_item list Environment.t + +and singleton_environment = codomain_item Environment.t (* a simple case of extension of a disambiguation environment *) -val env_of_list: (string * string * Cic.term) list -> environment -> environment +val singleton_env_of_list: + (string * string * Cic.term) list -> singleton_environment -> + singleton_environment + +val env_of_list: + (string * string * Cic.term) list -> environment -> + environment module type Callbacks = sig