let eval_unification_hint status t n =
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst subst [] t in
let status = basic_eval_unification_hint (t,n) status in
let diff =
[DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
in
- LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
;;
let inject_interpretation =
(fun status (name,cpos,arity) ->
try
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] []
("",0,NotationPt.Ident (name,None)) in
assert (metasenv = [] && subst = []);
let status, nuris =
let metasenv,subst,status,sort = match sort with
| None -> [],[],status,NCic.Sort NCic.Prop
| Some s ->
- GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] []
(text,prefix_len,s)
in
assert (metasenv = []);
(NCicPp.ppterm ~metasenv ~subst ~context:[] sort))) in
let status = status#set_ng_mode `ProofMode in
let metasenv,subst,status,indty =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] subst
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
(text,prefix_len,indty) in
let indtyno,(_,leftno,tys,_,_) =
match indty with
try
match
DisambiguateTypes.Environment.find item
- status#lstatus.LexiconTypes.aliases
+ status#disambiguate_db.GrafiteDisambiguate.aliases
with
GrafiteAst.Ident_alias (_, uri) ->
NotationPt.NRefPattern (NReference.reference_of_string uri)
prerr_endline
("LexiconEngine.eval_command: domain item not found: " ^
(DisambiguateTypes.string_of_domain_item item));
- LexiconEngine.dump_aliases prerr_endline "" status;
+ GrafiteDisambiguate.dump_aliases prerr_endline "" status;
raise
(Failure
((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
[DisambiguateTypes.Num instance,spec]
in
let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
- LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
(* assert false (* MANCA SALVATAGGIO SU DISCO *) *)
;;
inherit NCicLibrary.dumpable_status
inherit NCicLibrary.status
inherit GrafiteParser.status
+ inherit TermContentPres.status
val baseuri = b
val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
method baseuri = baseuri
inherit NCicLibrary.dumpable_status
inherit NCicLibrary.status
inherit GrafiteParser.status
+ inherit TermContentPres.status
method baseuri: string
method set_baseuri: string -> 'self
method ng_mode: [`ProofMode | `CommandMode]
(try
let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
- None status ctx [] [] ("",0,src) in
+ status None ctx [] [] ("",0,src) in
let src = NCicUntrusted.apply_subst subst [] src in
(* CHECK that the declared pattern matches the abstraction *)
let _ = NCicUnification.unify status metasenv subst ctx ty src in
let status, tgt, arity =
let metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
- None status [] [] [] ("",0,tgt) in
+ status None [] [] [] ("",0,tgt) in
let tgt = NCicUntrusted.apply_subst subst [] tgt in
(* CHECK che sia unificabile mancante *)
let rec count_prod = function
let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
let metasenv,subst,status,ty =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst subst [] ty in
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst subst [] t in
let status, src, tgt, cpos, arity =
dependenciesParser.cmi:
grafiteParser.cmi:
-grafiteDisambiguate.cmi:
print_grammar.cmi: grafiteParser.cmi
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
-grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
print_grammar.cmo: print_grammar.cmi
print_grammar.cmx: print_grammar.cmi
INTERFACE_FILES = \
dependenciesParser.mli \
grafiteParser.mli \
- grafiteDisambiguate.mli \
- print_grammar.mli \
+ print_grammar.mli \
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+++ /dev/null
-(*
- *
- * 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$ *)
-
-class type g_status =
- object
- inherit LexiconTypes.g_status
- end
-
-class status =
- object (self)
- inherit LexiconTypes.status
- method set_grafite_disambiguate_status
- : 'status. #g_status as 'status -> 'self
- = fun o -> (self#set_lexicon_engine_status o)
- end
-
-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 expty estatus context metasenv subst thing
-=
- let diff, metasenv, subst, cic =
- singleton "first"
- (NCicDisambiguate.disambiguate_term
- ~rdb:estatus
- ~aliases:estatus#lstatus.LexiconTypes.aliases
- ~expty
- ~universe:(Some estatus#lstatus.LexiconTypes.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 =
- LexiconEngine.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#lstatus.LexiconTypes.aliases
- ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
- (text,prefix_len,obj)) in
- let estatus =
- LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
- GrafiteAst.WithPreferences diff
- in
- estatus, cic
-;;
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * 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/
- *)
-
-exception BaseUriNotSetYet
-
-val disambiguate_nterm :
- NCic.term option ->
- (#LexiconTypes.status as 'status) ->
- NCic.context -> NCic.metasenv -> NCic.substitution ->
- NotationPt.term Disambiguate.disambiguator_input ->
- NCic.metasenv * NCic.substitution * 'status * NCic.term
-
-val disambiguate_nobj :
- #LexiconTypes.status as 'status ->
- ?baseuri:string ->
- (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
- 'status * NCic.obj
-
-type pattern =
- NotationPt.term Disambiguate.disambiguator_input option *
- (string * NCic.term) list * NCic.term option
-
-val disambiguate_npattern:
- GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
module N = NotationPt
module G = GrafiteAst
-module LE = LexiconEngine
type 'a localized_option =
LSome of 'a
-lexiconTypes.cmi:
-lexiconEngine.cmi: lexiconTypes.cmi
+grafiteDisambiguate.cmi:
+lexiconTypes.cmi: grafiteDisambiguate.cmi
lexiconSync.cmi: lexiconTypes.cmi
-lexiconTypes.cmo: lexiconTypes.cmi
-lexiconTypes.cmx: lexiconTypes.cmi
-lexiconEngine.cmo: lexiconTypes.cmi lexiconEngine.cmi
-lexiconEngine.cmx: lexiconTypes.cmx lexiconEngine.cmi
-lexiconSync.cmo: lexiconTypes.cmi lexiconEngine.cmi lexiconSync.cmi
-lexiconSync.cmx: lexiconTypes.cmx lexiconEngine.cmx lexiconSync.cmi
+grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
+lexiconTypes.cmo: grafiteDisambiguate.cmi lexiconTypes.cmi
+lexiconTypes.cmx: grafiteDisambiguate.cmx lexiconTypes.cmi
+lexiconSync.cmo: lexiconSync.cmi
+lexiconSync.cmx: lexiconSync.cmi
PREDICATES =
INTERFACE_FILES = \
- lexiconTypes.mli \
- lexiconEngine.mli \
+ grafiteDisambiguate.mli \
lexiconSync.mli \
$(NULL)
IMPLEMENTATION_FILES = \
--- /dev/null
+(*
+ *
+ * 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 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
+;;
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * 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/
+ *)
+
+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
+}
+
+class type g_status =
+ object
+ inherit Interpretations.g_status
+ method disambiguate_db: db
+ end
+
+class status :
+ object ('self)
+ inherit g_status
+ inherit Interpretations.status
+ method set_disambiguate_db: db -> 'self
+ method set_disambiguate_status: #g_status -> 'self
+ end
+
+val set_proof_aliases:
+ #status as 'status ->
+ implicit_aliases:bool -> (* implicit ones are made explicit *)
+ GrafiteAst.inclusion_mode ->
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
+
+(* args: print function, message (may be empty), status *)
+val dump_aliases: (string -> unit) -> string -> #status -> unit
+
+exception BaseUriNotSetYet
+
+val disambiguate_nterm :
+ #status as 'status ->
+ NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
+ NotationPt.term Disambiguate.disambiguator_input ->
+ NCic.metasenv * NCic.substitution * 'status * NCic.term
+
+val disambiguate_nobj :
+ #status as 'status -> ?baseuri:string ->
+ (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
+ 'status * NCic.obj
+
+type pattern =
+ NotationPt.term Disambiguate.disambiguator_input option *
+ (string * NCic.term) list * NCic.term option
+
+val disambiguate_npattern:
+ GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references
in
- LexiconEngine.set_proof_aliases status ~implicit_aliases:false
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
GrafiteAst.WithPreferences new_env
) status
*)
val add_aliases_for_objs:
- #LexiconTypes.status as 'status -> NUri.uri list -> 'status
+ #GrafiteDisambiguate.status as 'status -> NUri.uri list -> 'status
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * 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 lexicon_status = {
- 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
- inherit TermContentPres.g_status
- method lstatus: lexicon_status
- end
-
-class status =
- object(self)
- inherit Interpretations.status
- inherit TermContentPres.status
- val lstatus = initial_status
- method lstatus = lstatus
- method set_lstatus v = {< lstatus = v >}
- method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self
- = fun o -> ((self#set_lstatus o#lstatus)#set_interp_status o)#set_content_pres_status o
- end
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * 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/
- *)
-
-type lexicon_status = {
- 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
-}
-
-class type g_status =
- object
- inherit Interpretations.g_status
- inherit TermContentPres.g_status
- method lstatus: lexicon_status
- end
-
-class status :
- object ('self)
- inherit g_status
- inherit Interpretations.status
- inherit TermContentPres.status
- method set_lstatus: lexicon_status -> 'self
- method set_lexicon_engine_status: #g_status -> 'self
- end
class type g_pstatus =
object
- inherit LexiconTypes.g_status
+ inherit GrafiteDisambiguate.g_status
inherit g_auto_status
inherit g_eq_status
method obj: NCic.obj
class pstatus =
fun (o: NCic.obj) ->
object (self)
- inherit LexiconTypes.status
+ inherit GrafiteDisambiguate.status
inherit auto_status
inherit eq_status
val obj = o
method set_obj o = {< obj = o >}
method set_pstatus : 'status. #g_pstatus as 'status -> 'self
= fun o ->
- (((self#set_lexicon_engine_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o
+ (((self#set_disambiguate_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o
end
type tactic_term = NotationPt.term Disambiguate.disambiguator_input
in
let uri,height,metasenv,subst,obj = status#obj in
let metasenv, subst, status, t =
- GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t
+ GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t
in
let new_pstatus = uri,height,metasenv,subst,obj in
status#set_obj new_pstatus, (context, t)
class type g_pstatus =
object
- inherit LexiconTypes.g_status
+ inherit GrafiteDisambiguate.g_status
inherit g_auto_status
inherit g_eq_status
method obj: NCic.obj
class pstatus :
NCic.obj ->
object ('self)
- inherit LexiconTypes.status
+ inherit GrafiteDisambiguate.status
inherit auto_status
inherit eq_status
method obj: NCic.obj
|--> grafiteparser(db=ast_statement grammarentry)
| |--> cicnotationparser(db=grammars+keywords+items)
|
+ |--> termcontentpres(db=level1_patterns21,compiled21,
+ | pattern21_matrix,counter)
+ |
|--> tac(obj,stack)
|--> auto(automation_cache)
|--> eq(eq_cache)
- |--> lexicon(lstatus=aliases+multi_aliases+new_aliases)
+ |--> grafitedisambiguate(db=aliases+multi_aliases+new_aliases)
|--> interpretation(db=level2_patterns32,compiled32,
- | | pattern32_matrix,counter)
- | |--> nciccoercion(db=...)
- | |--> unif_hint(db=...)
- |
- |--> termcontentpres(db=level1_patterns21,compiled21,
- pattern21_matrix,counter)
+ | pattern32_matrix,counter)
+ |--> nciccoercion(db=...)
+ |--> unif_hint(db=...)
+
+applytransformation()
+ |--> termcontentpres(...)
+ |--> interpretation(...)
(* $Id$ *)
+class status =
+ object
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ end
+
let mpres_document pres_box =
Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
(* *)
(***************************************************************************)
+class status :
+ object
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ end
+
val ntxt_of_cic_sequent:
- map_unicode_to_tex:bool -> int -> #LexiconTypes.status ->
+ map_unicode_to_tex:bool -> int -> #status ->
NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
int * NCic.conjecture -> (* sequent *)
string (* text *)
val ntxt_of_cic_object:
- map_unicode_to_tex:bool -> int -> #LexiconTypes.status -> NCic.obj -> string
+ map_unicode_to_tex:bool -> int -> #status -> NCic.obj -> string
in
addDebugItem "dump aliases" (fun _ ->
let status = script#grafite_status in
- LexiconEngine.dump_aliases prerr_endline "" status);
+ GrafiteDisambiguate.dump_aliases prerr_endline "" status);
(* FG: DEBUGGING
addDebugItem "dump interpretations" (fun _ ->
let status = script#lexicon_status in
let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
let baseuri = status#baseuri in
let status =
- status#set_lstatus { status#lstatus with LexiconTypes.new_aliases = [] } in
+ status#set_disambiguate_db { status#disambiguate_db with GrafiteDisambiguate.new_aliases = [] } in
let status =
GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
(text,prefix_len,ast) in
- let new_aliases = status#lstatus.LexiconTypes.new_aliases in
+ let new_aliases = status#disambiguate_db.GrafiteDisambiguate.new_aliases in
let _,intermediate_states =
List.fold_left
(fun (status,acc) (k,value) ->
status,acc
else
let status =
- LexiconEngine.set_proof_aliases status ~implicit_aliases:false
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
GrafiteAst.WithPreferences [k,value]
in
status, (status ,Some (k,value))::acc
(** load a sequent and render it into parent widget *)
method nload_sequent:
- #LexiconTypes.status -> NCic.metasenv -> NCic.substitution -> int -> unit
+ #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit
- method load_nobject: #LexiconTypes.status -> NCic.obj -> unit
+ method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit
end
class type sequentsViewer =
method reset: unit
method load_logo: unit
method load_logo_with_qed: unit
- method nload_sequents: #NTacStatus.tac_status -> unit
+ method nload_sequents: #GrafiteTypes.status -> unit
method goto_sequent:
- #LexiconTypes.status -> int -> unit (* to be called _after_ load_sequents *)
+ #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *)
method cicMathView: cicMathView
end
val mutable current_mathml = None
method nload_sequent:
- 'status. #LexiconTypes.status as 'status -> NCic.metasenv ->
+ 'status. #ApplyTransformation.status as 'status -> NCic.metasenv ->
NCic.substitution -> int -> unit
= fun status metasenv subst metano ->
let sequent = List.assoc metano metasenv in
self#load_root ~root:txt
method load_nobject :
- 'status. #LexiconTypes.status as 'status -> NCic.obj -> unit
+ 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
= fun status obj ->
let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
80 status obj in
_metasenv <- `Old [];
self#script#setGoal None
- method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
- = fun (status : #NTacStatus.tac_status) ->
+ method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
+ = fun (status : #GrafiteTypes.status) ->
let _,_,metasenv,subst,_ = status#obj in
_metasenv <- `New (metasenv,subst);
pages <- 0;
self#render_page status ~page ~goal_switch))
method private render_page:
- 'status. #LexiconTypes.status as 'status -> page:int ->
+ 'status. #ApplyTransformation.status as 'status -> page:int ->
goal_switch:Stack.switch -> unit
= fun status ~page ~goal_switch ->
(match goal_switch with
List.assoc goal_switch goal2win ()
with Not_found -> assert false)
- method goto_sequent: 'status. #LexiconTypes.status as 'status -> int -> unit
+ method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
= fun status goal ->
let goal_switch, page =
try
in
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
- None status ctx menv subst (parsed_text,parsed_text_length,
+ status None ctx menv subst (parsed_text,parsed_text_length,
NotationPt.Cast (t,NotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
let initial_statuses current baseuri =
- let empty_lstatus = new LexiconTypes.status in
+ let empty_lstatus = new GrafiteDisambiguate.status in
(match current with
Some current ->
NCicLibrary.time_travel
- ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus);
+ ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db);
(* CSC: there is a known bug in invalidation; temporary fix here *)
NCicEnvironment.invalidate ()
| None -> ());
let lexicon_status = empty_lstatus in
- let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
+ let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
grafite_status
in
let read_include_paths file =
open GrafiteTypes
-exception AttemptToInsertAnAlias of LexiconTypes.status
+exception AttemptToInsertAnAlias of GrafiteDisambiguate.status
let slash_n_RE = Pcre.regexp "\\n" ;;
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
activate_extraction baseuri fname ;
- let lexicon_status = new LexiconTypes.status in
+ let lexicon_status = new GrafiteDisambiguate.status in
atstart (); (* FG: do not invoke before loading the core notation script *)
let grafite_status =
- (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
+ (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
| [] -> grafite_status
| (g,None)::_ -> g
| (g,Some _)::_ ->
- raise (AttemptToInsertAnAlias (g :> LexiconTypes.status))
+ raise (AttemptToInsertAnAlias (g :> GrafiteDisambiguate.status))
in
aux_for_dump print_cb grafite_status
in
projects / helm.git / commitdiff