From: Claudio Sacerdoti Coen Date: Thu, 15 Sep 2005 17:21:07 +0000 (+0000) Subject: Yet another implementation of the single aliases / multi aliases idea. X-Git-Tag: LAST_BEFORE_NEW~121 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8539d00ff2ed0ffd9b7a08ac8e62376e88987960;p=helm.git Yet another implementation of the single aliases / multi aliases idea. The new implementation is much simpler: single aliases are used everywhere in the disambiguation phase; however, when a term needs to be looked for in the library, it can be looked in a user-provided multi aliases environment instead. NOTE: the new implementation fixes a bug of the previous implementation: the most recent alias in the multi-alias set was printed last in the .moo files, changing the performances of the system. --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 5096789d9..b9aa8f844 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -359,7 +359,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.singleton_env_of_list name_to_uris env in + let con_env = DisambiguateTypes.env_of_list name_to_uris env in let undebrujin t = snd (List.fold_right @@ -635,7 +635,8 @@ sig context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:aliases -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> CicNotationPt.term -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) @@ -646,7 +647,8 @@ sig val disambiguate_obj : ?fresh_instances:bool -> dbd:Mysql.dbd -> - aliases:aliases -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> (environment * (* new interpretation status *) @@ -689,15 +691,10 @@ module Make (C: Callbacks) = uris let disambiguate_thing ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing = 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) @@ -708,9 +705,11 @@ module Make (C: Callbacks) = debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" (string_of_domain thing_dom)); debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s" - (DisambiguatePp.pp_environment (snd aliases))); + (DisambiguatePp.pp_environment aliases)); + debug_print (sprintf "DISAMBIGUATION UNIVERSE: %s" + (match universe with None -> "None" | Some _ -> "Some _")); let current_dom = - Environment.fold (fun item _ dom -> item :: dom) current_env [] + Environment.fold (fun item _ dom -> item :: dom) aliases [] in let todo_dom = domain_diff thing_dom current_dom in (* (2) lookup function for any item (Id/Symbol/Num) *) @@ -727,7 +726,7 @@ module Make (C: Callbacks) = | Num instance -> DisambiguateChoices.lookup_num_choices () in - match multi_aliases_env with + match universe with | None -> lookup_in_library () | Some e -> (try @@ -764,7 +763,7 @@ module Make (C: Callbacks) = (* (3) test an interpretation filling with meta uninterpreted identifiers *) - let test_env current_env todo_dom ugraph = + let test_env aliases todo_dom ugraph = let filled_env = List.fold_left (fun env item -> @@ -773,7 +772,7 @@ module Make (C: Callbacks) = (match item with | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) - current_env todo_dom + aliases todo_dom in try let cic_thing = @@ -787,12 +786,12 @@ module Make (C: Callbacks) = | Invalid_choice -> Ko, ugraph in (* (4) build all possible interpretations *) - let rec aux current_env todo_dom base_univ = + let rec aux aliases todo_dom base_univ = match todo_dom with | [] -> - (match test_env current_env [] base_univ with + (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> - [ current_env, metasenv, thing, new_univ ] + [ aliases, metasenv, thing, new_univ ] | Ko,_ | Uncertain,_ -> []) | item :: remaining_dom -> debug_print (sprintf "CHOOSED ITEM: %s" @@ -803,7 +802,7 @@ module Make (C: Callbacks) = | codomain_item :: tl -> debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ; let new_env = - Environment.add item codomain_item current_env + Environment.add item codomain_item aliases in (match test_env new_env remaining_dom univ with | Ok (thing, metasenv),new_univ -> @@ -823,7 +822,7 @@ module Make (C: Callbacks) = let base_univ = initial_ugraph in try let res = - match aux current_env todo_dom base_univ with + match aux aliases todo_dom base_univ with | [] -> raise NoWellTypedInterpretation | [ e,me,t,u ] -> debug_print "SINGLE INTERPRETATION"; @@ -858,7 +857,7 @@ module Make (C: Callbacks) = let choices, b = res in (List.map (fun (env, metasenv, t, ugraph) -> - Environment.fold Environment.cons env (snd aliases), + Environment.fold Environment.add env aliases, metasenv, t, ugraph) choices), b @@ -867,21 +866,23 @@ module Make (C: Callbacks) = failwith "Disambiguate: circular dependency" let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term = 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 + ~universe ~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 disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri + obj + = let obj = if fresh_instances then CicNotationUtil.freshen_obj obj else obj in - disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri + disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj obj @@ -906,7 +907,7 @@ struct let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in try fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast - ?initial_ugraph ~aliases:(false, aliases)) + ?initial_ugraph ~aliases ~universe:None) with Exit -> raise (Ambiguous_term term) end diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 5de2e5759..87e09daef 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -32,9 +32,6 @@ val interpretate_path : 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 @@ -46,7 +43,8 @@ sig context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:aliases -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> DisambiguateTypes.term -> (DisambiguateTypes.environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) @@ -58,7 +56,8 @@ sig val disambiguate_obj : ?fresh_instances:bool -> dbd:Mysql.dbd -> - aliases:aliases -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> (DisambiguateTypes.environment * (* new interpretation status *) diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml index d0b6447c5..b7c1012a8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml @@ -28,6 +28,7 @@ open DisambiguateTypes let parse_environment str = let stream = Stream.of_string str in let environment = ref Environment.empty in + let multiple_environment = ref Environment.empty in try while true do let alias = @@ -49,25 +50,23 @@ let parse_environment str = Num instance, DisambiguateChoices.lookup_num_by_dsc desc in - environment := Environment.cons key value !environment; + environment := Environment.add key value !environment; + multiple_environment := Environment.cons key value !multiple_environment; done; assert false with End_of_file -> - !environment + !environment, !multiple_environment let aliases_of_environment env = Environment.fold - (fun domain_item codomain_items acc -> - List.fold_left - (fun strings (dsc, _) -> - let s = - match domain_item with - | Id id -> GrafiteAst.Ident_alias (id, dsc) - | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc) - | Num i -> GrafiteAst.Number_alias (i, dsc) - in - s :: strings) - acc codomain_items) + (fun domain_item (dsc,_) acc -> + let s = + match domain_item with + | Id id -> GrafiteAst.Ident_alias (id, dsc) + | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc) + | Num i -> GrafiteAst.Number_alias (i, dsc) + in + s :: acc) env [] let commands_of_environment env = diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.mli b/helm/ocaml/cic_disambiguation/disambiguatePp.mli index 9d2051134..e5a656d22 100644 --- a/helm/ocaml/cic_disambiguation/disambiguatePp.mli +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.mli @@ -23,11 +23,12 @@ * http://helm.cs.unibo.it/ *) -val parse_environment: string -> DisambiguateTypes.environment +val parse_environment: + string -> + DisambiguateTypes.environment * DisambiguateTypes.multiple_environment val commands_of_environment: DisambiguateTypes.environment -> (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list val pp_environment: DisambiguateTypes.environment -> string - diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 3e969c87a..a3c7c82c6 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -73,20 +73,21 @@ end type codomain_item = string * (* description *) - (singleton_environment -> string -> Cic.term list -> Cic.term) + (environment -> string -> Cic.term list -> Cic.term) (* environment, literal number, arguments as needed *) -and environment = codomain_item list Environment.t +and environment = codomain_item Environment.t + +type multiple_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 = +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 singleton_env_of_list l e = +let env_of_list l e = List.fold_left (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e) e l @@ -113,8 +114,6 @@ let string_of_domain_item = function let string_of_domain dom = String.concat "; " (List.map string_of_domain_item dom) -let empty_environment = Environment.empty - let floc_of_loc (loc_begin, loc_end) = let floc_begin = { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index df598a3f7..7f955d673 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -45,21 +45,20 @@ exception Invalid_choice type codomain_item = string * (* description *) - (singleton_environment -> string -> Cic.term list -> Cic.term) + (environment -> string -> Cic.term list -> Cic.term) (* environment, literal number, arguments as needed *) -and environment = codomain_item list Environment.t +and environment = codomain_item Environment.t -and singleton_environment = codomain_item Environment.t +type multiple_environment = codomain_item list Environment.t (* a simple case of extension of a disambiguation 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 + (string * string * Cic.term) list -> environment -> environment + +val multiple_env_of_list: + (string * string * Cic.term) list -> multiple_environment -> + multiple_environment module type Callbacks = sig @@ -94,7 +93,5 @@ type script_entry = | Comment of CicNotationPt.location * string type script = CicNotationPt.location * script_entry list -val empty_environment: environment - val dummy_floc: Lexing.position * Lexing.position