-(*
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-type db = {
- aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
- multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
- new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
-}
-
-let initial_status = {
- aliases = DisambiguateTypes.Environment.empty;
- multi_aliases = DisambiguateTypes.Environment.empty;
- new_aliases = []
-}
-
-class type g_status =
- object
- inherit Interpretations.g_status
- method disambiguate_db: db
- end
-
-class status =
- object (self)
- inherit Interpretations.status
- val disambiguate_db = initial_status
- method disambiguate_db = disambiguate_db
- method set_disambiguate_db v = {< disambiguate_db = v >}
- method set_disambiguate_status
- : 'status. #g_status as 'status -> 'self
- = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
- end
-
-let eval_with_new_aliases status f =
- let status =
- status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
- let res = f status in
- let new_aliases = status#disambiguate_db.new_aliases in
- new_aliases,res
-;;
-
-let dump_aliases out msg status =
- out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
- DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
- status#disambiguate_db.aliases
-
-let set_proof_aliases status ~implicit_aliases mode new_aliases =
- if mode = GrafiteAst.WithoutPreferences then
- status
- else
- (* MATITA 1.0
- let new_commands =
- List.map
- (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
- in *)
- let aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status#disambiguate_db.aliases new_aliases in
- let multi_aliases =
- List.fold_left (fun acc (d,c) ->
- DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
- d c acc)
- status#disambiguate_db.multi_aliases new_aliases
- in
- let new_status =
- {multi_aliases = multi_aliases ;
- aliases = aliases;
- new_aliases =
- (if implicit_aliases then new_aliases else []) @
- status#disambiguate_db.new_aliases}
- in
- status#set_disambiguate_db new_status
-
-exception BaseUriNotSetYet
-
-let singleton msg = function
- | [x], _ -> x
- | l, _ ->
- let debug =
- Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
- msg (List.length l)
- in
- prerr_endline debug; assert false
-
-let __Implicit = "__Implicit__"
-let __Closed_Implicit = "__Closed_Implicit__"
-
-let ncic_mk_choice status = function
- | GrafiteAst.Symbol_alias (name, _, dsc) ->
- if name = __Implicit then
- dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
- else if name = __Closed_Implicit then
- dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
- else
- DisambiguateChoices.lookup_symbol_by_dsc status
- ~mk_implicit:(function
- | true -> NCic.Implicit `Closed
- | false -> NCic.Implicit `Term)
- ~mk_appl:(function
- (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
- ~term_of_nref:(fun nref -> NCic.Const nref)
- name dsc
- | GrafiteAst.Number_alias (_, dsc) ->
- let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
- desc, `Num_interp
- (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
- | GrafiteAst.Ident_alias (name, uri) ->
- uri, `Sym_interp
- (fun l->assert(l = []);
- let nref = NReference.reference_of_string uri in
- NCic.Const nref)
-;;
-
-
-let mk_implicit b =
- match b with
- | false ->
- GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
- | true ->
- GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
-;;
-
-let nlookup_in_library
- interactive_user_uri_choice input_or_locate_uri item
-=
- match item with
- | DisambiguateTypes.Id id ->
- (try
- let references = NCicLibrary.resolve id in
- List.map
- (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
- ) references
- with
- NCicEnvironment.ObjectNotFound _ -> [])
- | _ -> []
-;;
-
-let fix_instance item l =
- match item with
- DisambiguateTypes.Symbol (_,n) ->
- List.map
- (function
- GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
- | _ -> assert false
- ) l
- | DisambiguateTypes.Num n ->
- List.map
- (function
- GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
- | _ -> assert false
- ) l
- | DisambiguateTypes.Id _ -> l
-;;
-
-
-let disambiguate_nterm estatus expty context metasenv subst thing
-=
- let diff, metasenv, subst, cic =
- singleton "first"
- (NCicDisambiguate.disambiguate_term
- ~rdb:estatus
- ~aliases:estatus#disambiguate_db.aliases
- ~expty
- ~universe:(Some estatus#disambiguate_db.multi_aliases)
- ~lookup_in_library:nlookup_in_library
- ~mk_choice:(ncic_mk_choice estatus)
- ~mk_implicit ~fix_instance
- ~description_of_alias:GrafiteAst.description_of_alias
- ~context ~metasenv ~subst thing)
- in
- let estatus =
- set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
- diff
- in
- metasenv, subst, estatus, cic
-;;
-
-
-type pattern =
- NotationPt.term Disambiguate.disambiguator_input option *
- (string * NCic.term) list * NCic.term option
-
-let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
- let interp path = NCicDisambiguate.disambiguate_path path in
- let goal_path = HExtlib.map_option interp goal_path in
- let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
- let wanted =
- match wanted with None -> None | Some x -> Some (text,prefix_len,x)
- in
- (wanted, hyp_paths, goal_path)
-;;
-
-let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
- | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
- | `Normalize
- | `Simpl
- | `Unfold None
- | `Whd as kind -> kind
-;;
-
-let disambiguate_auto_params
- disambiguate_term metasenv context (oterms, params)
-=
- match oterms with
- | None -> metasenv, (None, params)
- | Some terms ->
- let metasenv, terms =
- List.fold_right
- (fun t (metasenv, terms) ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,t::terms) terms (metasenv, [])
- in
- metasenv, (Some terms, params)
-;;
-
-let disambiguate_just disambiguate_term context metasenv =
- function
- `Term t ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv, `Term t
- | `Auto params ->
- let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
- context params
- in
- metasenv, `Auto params
-;;
-
-let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
- let uri =
- let baseuri =
- match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
- in
- let name =
- match obj with
- | NotationPt.Inductive (_,(name,_,_,_)::_)
- | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
- | NotationPt.Inductive _ -> assert false
- in
- NUri.uri_of_string (baseuri ^ "/" ^ name)
- in
- let diff, _, _, cic =
- singleton "third"
- (NCicDisambiguate.disambiguate_obj
- ~lookup_in_library:nlookup_in_library
- ~description_of_alias:GrafiteAst.description_of_alias
- ~mk_choice:(ncic_mk_choice estatus)
- ~mk_implicit ~fix_instance
- ~uri
- ~rdb:estatus
- ~aliases:estatus#disambiguate_db.aliases
- ~universe:(Some estatus#disambiguate_db.multi_aliases)
- (text,prefix_len,obj)) in
- let estatus =
- set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
- diff
- in
- estatus, cic
-;;
-
-let disambiguate_cic_appl_pattern status args =
- let rec disambiguate =
- function
- NotationPt.ApplPattern l ->
- NotationPt.ApplPattern (List.map disambiguate l)
- | NotationPt.VarPattern id
- when not
- (List.exists
- (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
- ->
- let item = DisambiguateTypes.Id id in
- begin
- try
- match
- DisambiguateTypes.Environment.find item
- status#disambiguate_db.aliases
- with
- GrafiteAst.Ident_alias (_, uri) ->
- NotationPt.NRefPattern (NReference.reference_of_string uri)
- | _ -> assert false
- with Not_found ->
- prerr_endline
- ("LexiconEngine.eval_command: domain item not found: " ^
- (DisambiguateTypes.string_of_domain_item item));
- dump_aliases prerr_endline "" status;
- raise
- (Failure
- ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
- end
- | p -> p
- in
- disambiguate
-;;
-
-let add_aliases_for_objs status =
- List.fold_left
- (fun status nref ->
- let references = NCicLibrary.aliases_of nref in
- let new_env =
- List.map
- (fun u ->
- let name = NCicPp.r2s true u in
- DisambiguateTypes.Id name,
- GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
- ) references
- in
- set_proof_aliases status ~implicit_aliases:false
- GrafiteAst.WithPreferences new_env
- ) status