let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+let load_patterns32 = ref (fun _ -> assert false);;
+let set_load_patterns32 f = load_patterns32 := f;;
+
type interpretation_id = int
let idref id t = Ast.AttributedTerm (`IdRef id, t)
uri: (cic_id, NReference.reference) Hashtbl.t;
}
- (* persistent state *)
-
-let initial_level2_patterns32 () = Hashtbl.create 211
-let initial_interpretations () = Hashtbl.create 211
-
-let level2_patterns32 = ref (initial_level2_patterns32 ())
-(* symb -> id list ref *)
-let interpretations = ref (initial_interpretations ())
-let pattern32_matrix = ref []
-let counter = ref ~-1
-let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;;
-
-let stack = ref []
-
-let push () =
- stack := (!counter,!level2_patterns32,!interpretations,!pattern32_matrix)::!stack;
- counter := ~-1;
- level2_patterns32 := initial_level2_patterns32 ();
- interpretations := initial_interpretations ();
- pattern32_matrix := []
-;;
-
-let pop () =
- match !stack with
- [] -> assert false
- | (ocounter,olevel2_patterns32,ointerpretations,opattern32_matrix)::old ->
- stack := old;
- counter := ocounter;
- level2_patterns32 := olevel2_patterns32;
- interpretations := ointerpretations;
- pattern32_matrix := opattern32_matrix
-;;
+module IntMap = Map.Make(struct type t = int let compare = compare end);;
+module StringMap = Map.Make(String);;
+
+type db = {
+ counter: int;
+ pattern32_matrix: (bool * NotationPt.cic_appl_pattern * interpretation_id) list;
+ level2_patterns32:
+ (string * string * NotationPt.argument_pattern list *
+ NotationPt.cic_appl_pattern) IntMap.t;
+ interpretations: interpretation_id list StringMap.t; (* symb -> id list *)
+}
+
+let initial_db = {
+ counter = -1;
+ pattern32_matrix = [];
+ level2_patterns32 = IntMap.empty;
+ interpretations = StringMap.empty
+}
+
+class type g_status =
+ object
+ method interp_db: db
+ end
+
+class status =
+ object
+ val interp_db = initial_db
+ method interp_db = interp_db
+ method set_interp_db v = {< interp_db = v >}
+ method set_interp_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< interp_db = o#interp_db >}
+ end
+
+let find_level2_patterns32 status pid =
+ IntMap.find pid status#interp_db.level2_patterns32
let add_idrefs =
List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
if args = [] then head
else Ast.Appl (head :: List.map instantiate_arg args)
-let load_patterns32s = ref [];;
-
-let add_load_patterns32 f = load_patterns32s := f :: !load_patterns32s;;
-let fresh_id =
- fun () ->
- incr counter;
- !counter
-
-let add_interpretation dsc (symbol, args) appl_pattern =
- let id = fresh_id () in
- Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
- pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
- List.iter (fun f -> f !pattern32_matrix) !load_patterns32s;
- (try
- let ids = Hashtbl.find !interpretations symbol in
- ids := id :: !ids
- with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
- id
-
-let get_all_interpretations () =
- List.map
- (function (_, _, id) ->
- let (dsc, _, _, _) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- (id, dsc))
- !pattern32_matrix
-
-let get_active_interpretations () =
- HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
- !pattern32_matrix
-
-let set_active_interpretations ids =
- let pattern32_matrix' =
- List.map
- (function
- | (_, ap, id) when List.mem id ids -> (true, ap, id)
- | (_, ap, id) -> (false, ap, id))
- !pattern32_matrix
+let fresh_id status =
+ let counter = status#interp_db.counter+1 in
+ status#set_interp_db ({ status#interp_db with counter = counter }), counter
+
+let add_interpretation (status : #status) dsc (symbol, args) appl_pattern =
+ let status,id = fresh_id status in
+ let ids =
+ try
+ StringMap.find symbol status#interp_db.interpretations
+ with Not_found -> [id] in
+ let status =
+ status#set_interp_db { status#interp_db with
+ level2_patterns32 =
+ IntMap.add id (dsc, symbol, args, appl_pattern)
+ status#interp_db.level2_patterns32;
+ pattern32_matrix = (true,appl_pattern,id)::status#interp_db.pattern32_matrix;
+ interpretations = StringMap.add symbol ids status#interp_db.interpretations
+ }
in
- pattern32_matrix := pattern32_matrix';
- List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
+ !load_patterns32 status#interp_db.pattern32_matrix;
+ status,id
+
+let toggle_active_interpretations status b =
+ status#set_interp_db { status#interp_db with
+ pattern32_matrix =
+ List.map (fun (_,ap,id) -> b,ap,id) status#interp_db.pattern32_matrix }
exception Interpretation_not_found
-let lookup_interpretations ?(sorted=true) symbol =
+let lookup_interpretations status ?(sorted=true) symbol =
try
let raw =
List.map (
fun id ->
let (dsc, _, args, appl_pattern) =
- try
- Hashtbl.find !level2_patterns32 id
+ try IntMap.find id status#interp_db.level2_patterns32
with Not_found -> assert false
in
dsc, args, appl_pattern
- )
- !(Hashtbl.find !interpretations symbol)
+ ) (StringMap.find symbol status#interp_db.interpretations)
in
if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
else raw
with Not_found -> raise Interpretation_not_found
-let remove_interpretation id =
- (try
- let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
- let ids = Hashtbl.find !interpretations symbol in
- ids := List.filter ((<>) id) !ids;
- Hashtbl.remove !level2_patterns32 id;
- with Not_found -> raise Interpretation_not_found);
- pattern32_matrix :=
- List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
- List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
-
-let init () = List.iter (fun f -> f []) !load_patterns32s
-
let instantiate_appl_pattern
~mk_appl ~mk_implicit ~term_of_nref env appl_pattern
=
| Ast.ApplPattern terms -> mk_appl (List.map aux terms)
in
aux appl_pattern
-
*)
- (** {2 Persistant state handling} *)
+ (** {2 State handling} *)
+
+type db
+
+class type g_status =
+ object
+ method interp_db: db
+ end
+
+class status :
+ object ('self)
+ method interp_db: db
+ method set_interp_db: db -> 'self
+ method set_interp_status: #g_status -> 'self
+ end
type interpretation_id
type cic_id = string
val add_interpretation:
+ #status as 'status ->
string -> (* id / description *)
string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
NotationPt.cic_appl_pattern -> (* level 3 pattern *)
- interpretation_id
+ 'status * interpretation_id
- (** @raise Interpretation_not_found *)
-val lookup_interpretations:
- ?sorted:bool -> string -> (* symbol *)
- (string * NotationPt.argument_pattern list *
- NotationPt.cic_appl_pattern) list
+val set_load_patterns32:
+ ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit
exception Interpretation_not_found
(** @raise Interpretation_not_found *)
-val remove_interpretation: interpretation_id -> unit
+val lookup_interpretations:
+ #status ->
+ ?sorted:bool -> string -> (* symbol *)
+ (string * NotationPt.argument_pattern list *
+ NotationPt.cic_appl_pattern) list
(** {3 Interpretations toggling} *)
-val get_all_interpretations: unit -> (interpretation_id * string) list
-val get_active_interpretations: unit -> interpretation_id list
-val set_active_interpretations: interpretation_id list -> unit
+val toggle_active_interpretations: #status as 'status -> bool -> 'status
(** {2 content -> cic} *)
(string * 'term) list -> NotationPt.cic_appl_pattern ->
'term
-val push: unit -> unit
-val pop: unit -> unit
-
-(* for Matita NG *)
val find_level2_patterns32:
- int ->
- string * string *
- NotationPt.argument_pattern list * NotationPt.cic_appl_pattern
-
-val add_load_patterns32:
- ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit
-val init: unit -> unit
+ #status -> int ->
+ string * string * NotationPt.argument_pattern list *
+ NotationPt.cic_appl_pattern
=
let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
in
- NCicLibrary.Serializer.register#run "unification_hints"
- object(_ : 'a NCicLibrary.register_type)
- method run = basic_eval_unification_hint
- end
+ GrafiteTypes.Serializer.register#run "unification_hints"
+ basic_eval_unification_hint
;;
let eval_unification_hint status t n =
(fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v)
l)
in
- NCicLibrary.Serializer.register#run "index_obj"
- object(_ : 'a NCicLibrary.register_type)
- method run = aux
- end
+ GrafiteTypes.Serializer.register#run "index_obj" aux
;;
let compute_keys status uri height kind =
~refresh_uri_in_term
= index_eq (NCicLibrary.refresh_uri uri)
in
- NCicLibrary.Serializer.register#run "index_eq"
- object(_ : 'a NCicLibrary.register_type)
- method run = basic_index_eq
- end
+ GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
;;
let index_eq_for_auto status uri =
let u2 = refresh_uri_in_universe u2 in
basic_eval_add_constraint (u1,u2)
in
- NCicLibrary.Serializer.register#run "constraints"
- object(_:'a NCicLibrary.register_type)
- method run = basic_eval_add_constraint
- end
+ GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint
;;
let eval_add_constraint status u1 u2 =
let status,uris =
match cmd with
| GrafiteAst.Include (loc, baseuri) ->
- NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
- status, []
+ let status,obj =
+ GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
+ status in
+ let status = status#set_dump (obj::status#dump) in
+ status,[]
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Set (loc, name, value) -> status, []
in
NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular))
in
object
+ (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
+ inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
+ inherit NCicLibrary.dumpable_status
val baseuri = b
val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
method baseuri = baseuri
method set_baseuri v = {< baseuri = v >}
method ng_mode = ng_mode;
method set_ng_mode v = {< ng_mode = v >}
- (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
- inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
end
+
+module Serializer =
+ NCicLibrary.Serializer(struct type dumpable_status = status end)
class status :
string ->
object ('self)
+ (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
+ inherit NTacStatus.tac_status
+ inherit NCicLibrary.dumpable_status
method baseuri: string
method set_baseuri: string -> 'self
method ng_mode: [`ProofMode | `CommandMode]
method set_ng_mode: [`ProofMode | `CommandMode] -> 'self
- (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
- inherit NTacStatus.tac_status
end
+
+module Serializer: NCicLibrary.SerializerType with type dumpable_status = status
let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
in
- NCicLibrary.Serializer.register#run "ncoercion"
- object(self : 'a NCicLibrary.register_type)
- method run = aux_l
- end
+ GrafiteTypes.Serializer.register#run "ncoercion" aux_l
;;
let basic_eval_and_record_ncoercion infos status =
dependenciesParser.mli \
grafiteParser.mli \
cicNotation2.mli \
- nEstatus.mli \
grafiteDisambiguate.mli \
print_grammar.mli \
$(NULL)
(* $Id$ *)
+class g_status =
+ object
+ inherit LexiconEngine.g_status
+ inherit NCicCoercion.g_status
+ end
+
+class status =
+ object (self)
+ inherit LexiconEngine.status
+ inherit NCicCoercion.status
+ method set_grafite_disambiguate_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o
+ end
+
exception BaseUriNotSetYet
let singleton msg = function
let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"
-let ncic_mk_choice = function
+let ncic_mk_choice status = function
| LexiconAst.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
+ DisambiguateChoices.lookup_symbol_by_dsc status
~mk_implicit:(function
| true -> NCic.Implicit `Closed
| false -> NCic.Implicit `Term)
~expty
~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
~lookup_in_library:nlookup_in_library
- ~mk_choice:ncic_mk_choice
+ ~mk_choice:(ncic_mk_choice estatus)
~mk_implicit ~fix_instance
~description_of_alias:LexiconAst.description_of_alias
~context ~metasenv ~subst thing)
(NCicDisambiguate.disambiguate_obj
~lookup_in_library:nlookup_in_library
~description_of_alias:LexiconAst.description_of_alias
- ~mk_choice:ncic_mk_choice
+ ~mk_choice:(ncic_mk_choice estatus)
~mk_implicit ~fix_instance
~uri
~rdb:estatus
let estatus = LexiconEngine.set_proof_aliases estatus diff in
estatus, cic
;;
-
-let disambiguate_command estatus (text,prefix_len,cmd)=
- match cmd with
- | GrafiteAst.Include _
- | GrafiteAst.Print _
- | GrafiteAst.Set _ as cmd ->
- estatus,cmd
exception BaseUriNotSetYet
-val disambiguate_command:
- LexiconEngine.status as 'status ->
- GrafiteAst.command Disambiguate.disambiguator_input ->
- 'status * GrafiteAst.command
+class g_status :
+ object
+ inherit LexiconEngine.g_status
+ inherit NCicCoercion.g_status
+ end
+
+class status :
+ object
+ inherit LexiconEngine.status
+ inherit NCicCoercion.status
+ method set_grafite_disambiguate_status: #g_status -> 'self
+ end
val disambiguate_nterm :
NCic.term option ->
- (#NEstatus.status as 'status) ->
+ (#status as 'status) ->
NCic.context -> NCic.metasenv -> NCic.substitution ->
NotationPt.term Disambiguate.disambiguator_input ->
NCic.metasenv * NCic.substitution * 'status * NCic.term
val disambiguate_nobj :
- #NEstatus.status as 'status ->
+ #status as 'status ->
?baseuri:string ->
(NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
'status * NCic.obj
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-
-class type g_status =
- object
- inherit LexiconEngine.g_status
- inherit NCicLibrary.g_dumpable_status
- end
-
-class status =
- object (self)
- inherit LexiconEngine.status
- inherit NCicLibrary.dumpable_status
- method set_estatus : 'status. #g_status as 'status -> 'self
- = fun o -> (self#set_lexicon_engine_status o)#set_dumpable_status o
- end
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-
-class type g_status =
- object
- inherit LexiconEngine.g_status
- inherit NCicLibrary.g_dumpable_status
- end
-
-class status :
- object ('self)
- inherit LexiconEngine.status
- inherit NCicLibrary.dumpable_status
- inherit g_status
- method set_estatus: #g_status -> 'self
- end
let parser_ref_counter = ref (initial_parser_ref_counter ());;
let rule_ids_to_items = ref (initial_rule_ids_to_items ());;
-let process_notation st =
+let process_notation status st =
match st with
| Notation (loc, dir, l1, associativity, precedence, l2) ->
let l1 =
else
[]
in
- !rule_id @ pp_id
+ status,!rule_id @ pp_id
| Interpretation (loc, dsc, l2, l3) ->
- let interp_id = Interpretations.add_interpretation dsc l2 l3 in
- [InterpretationId interp_id]
- | st -> []
+ let status,interp_id =
+ Interpretations.add_interpretation status dsc l2 l3
+ in
+ status,[InterpretationId interp_id]
+ | st -> status,[]
let remove_notation = function
| RuleId id ->
RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
!parser_ref_counter item
| PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
- | InterpretationId id -> Interpretations.remove_interpretation id
-
-let get_all_notations () =
- List.map
- (fun (interp_id, dsc) ->
- InterpretationId interp_id, "interpretation: " ^ dsc)
- (Interpretations.get_all_interpretations ())
-
-let get_active_notations () =
- List.map (fun id -> InterpretationId id)
- (Interpretations.get_active_interpretations ())
-
-let set_active_notations ids =
- let interp_ids =
- HExtlib.filter_map
- (function InterpretationId interp_id -> Some interp_id | _ -> None)
- ids
- in
- Interpretations.set_active_interpretations interp_ids
+ | InterpretationId id -> ()
let history = ref [];;
parser_ref_counter := initial_parser_ref_counter ();
rule_ids_to_items := initial_rule_ids_to_items ();
TermContentPres.push ();
- Interpretations.push ();
CicNotationParser.push ()
;;
let pop () =
TermContentPres.pop ();
- Interpretations.pop ();
CicNotationParser.pop ();
match !history with
| [] -> assert false
val compare_notation_id : notation_id -> notation_id -> int
-val process_notation: LexiconAst.command -> notation_id list
+val process_notation:
+ #Interpretations.status as 'status -> LexiconAst.command
+ -> 'status * notation_id list
val remove_notation: notation_id -> unit
-(** {2 Notation enabling/disabling}
- * Right now, only disabling of notation during pretty printing is supported.
- * If it is useful to disable it also for the input phase is still to be
- * understood ... *)
-
-val get_all_notations: unit -> (notation_id * string) list (* id, dsc *)
-val get_active_notations: unit -> notation_id list
-val set_active_notations: notation_id list -> unit
-
val push: unit -> unit
val pop: unit -> unit
class type g_status =
object
+ inherit Interpretations.g_status
method lstatus: lexicon_status
end
class status =
object(self)
+ inherit Interpretations.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
+ = fun o -> (self#set_lstatus o#lstatus)#set_interp_status o
end
let dump_aliases out msg status =
(loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
| _-> cmd
in
- let notation_ids' = CicNotation.process_notation cmd in
+ let sstatus,notation_ids' = CicNotation.process_notation sstatus cmd in
let status =
{ status with notation_ids = notation_ids' @ status.notation_ids } in
let sstatus = sstatus#set_lstatus status in
class type g_status =
object
+ inherit Interpretations.g_status
method lstatus: lexicon_status
end
class status :
object ('self)
inherit g_status
+ inherit Interpretations.status
method set_lstatus: lexicon_status -> 'self
method set_lexicon_engine_status: #g_status -> 'self
end
let hide_coercions = ref true;;
-(*
-type interpretation_id = int
-
-type term_info =
- { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
- uri: (Cic.id, UriManager.uri) Hashtbl.t;
- }
-*)
+class status =
+ object
+ inherit NCicCoercion.status
+ inherit Interpretations.status
+ end
let idref register_ref =
let id = ref 0 in
idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
;;
- (* persistent state *)
-
-(*
-let initial_level2_patterns32 () = Hashtbl.create 211
-let initial_interpretations () = Hashtbl.create 211
-
-let level2_patterns32 = ref (initial_level2_patterns32 ())
-(* symb -> id list ref *)
-let interpretations = ref (initial_interpretations ())
-*)
let compiled32 = ref None
-(*
-let pattern32_matrix = ref []
-let counter = ref ~-1
-
-let stack = ref []
-
-let push () =
- stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack;
- counter := ~-1;
- level2_patterns32 := initial_level2_patterns32 ();
- interpretations := initial_interpretations ();
- compiled32 := None;
- pattern32_matrix := []
-;;
-
-let pop () =
- match !stack with
- [] -> assert false
- | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old ->
- stack := old;
- counter := ocounter;
- level2_patterns32 := olevel2_patterns32;
- interpretations := ointerpretations;
- compiled32 := ocompiled32;
- pattern32_matrix := opattern32_matrix
-;;
-*)
let get_compiled32 () =
match !compiled32 with
in
let _, symbol, args, _ =
try
- Interpretations.find_level2_patterns32 pid
+ Interpretations.find_level2_patterns32 status pid
with Not_found -> assert false
in
let ast = instantiate32 idrefs env symbol args in
HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
in
set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
-in
- Interpretations.add_load_patterns32 load_patterns32;
- Interpretations.init ()
;;
-(*
-let fresh_id =
- fun () ->
- incr counter;
- !counter
-
-let add_interpretation dsc (symbol, args) appl_pattern =
- let id = fresh_id () in
- Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
- pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
- load_patterns32 !pattern32_matrix;
- (try
- let ids = Hashtbl.find !interpretations symbol in
- ids := id :: !ids
- with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
- id
-
-let get_all_interpretations () =
- List.map
- (function (_, _, id) ->
- let (dsc, _, _, _) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- (id, dsc))
- !pattern32_matrix
-
-let get_active_interpretations () =
- HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
- !pattern32_matrix
-
-let set_active_interpretations ids =
- let pattern32_matrix' =
- List.map
- (function
- | (_, ap, id) when List.mem id ids -> (true, ap, id)
- | (_, ap, id) -> (false, ap, id))
- !pattern32_matrix
- in
- pattern32_matrix := pattern32_matrix';
- load_patterns32 !pattern32_matrix
-
-exception Interpretation_not_found
-
-let lookup_interpretations symbol =
- try
- HExtlib.list_uniq
- (List.sort Pervasives.compare
- (List.map
- (fun id ->
- let (dsc, _, args, appl_pattern) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- dsc, args, appl_pattern)
- !(Hashtbl.find !interpretations symbol)))
- with Not_found -> raise Interpretation_not_found
-
-let remove_interpretation id =
- (try
- let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
- let ids = Hashtbl.find !interpretations symbol in
- ids := List.filter ((<>) id) !ids;
- Hashtbl.remove !level2_patterns32 id;
- with Not_found -> raise Interpretation_not_found);
- pattern32_matrix :=
- List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
- load_patterns32 !pattern32_matrix
-
-let _ = load_patterns32 []
-
-let instantiate_appl_pattern
- ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern
-=
- let lookup name =
- try List.assoc name env
- with Not_found ->
- prerr_endline (sprintf "Name %s not found" name);
- assert false
- in
- let rec aux = function
- | Ast.UriPattern uri -> term_of_uri uri
- | Ast.ImplicitPattern -> mk_implicit false
- | Ast.VarPattern name -> lookup name
- | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
- in
- aux appl_pattern
-*)
-
let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
let module K = Content in
let nast_of_cic =
in
res,ids_to_refs
;;
+
+Interpretations.set_load_patterns32 load_patterns32
val hide_coercions: bool ref
+class status :
+ object ('self)
+ inherit NCicCoercion.status
+ inherit Interpretations.status
+ end
+
val nmap_sequent:
- #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+ #status as 'a -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
int * NCic.conjecture ->
NotationPt.term Content.conjecture *
(id, NReference.reference) Hashtbl.t (* id -> reference *)
val nmap_obj:
- #NCicCoercion.status -> NCic.obj ->
+ #status -> NCic.obj ->
NotationPt.term Content.cobj *
(id, NReference.reference) Hashtbl.t (* id -> reference *)
[] -> combined
| _::_ -> mk_appl (combined::rest))
-let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_nref symbol dsc =
- let interpretations = Interpretations.lookup_interpretations ~sorted:false symbol in
+let lookup_symbol_by_dsc status ~mk_appl ~mk_implicit ~term_of_nref symbol dsc =
+ let interpretations =
+ Interpretations.lookup_interpretations status ~sorted:false symbol in
try
mk_choice ~mk_appl ~mk_implicit ~term_of_nref
(List.find (fun (dsc', _, _) -> dsc = dsc') interpretations)
* @param dsc description (1st component of codomain_item)
*)
val lookup_symbol_by_dsc:
+ #Interpretations.status ->
mk_appl: ('term list -> 'term) ->
mk_implicit: (bool -> 'term) ->
term_of_nref: (NReference.reference -> 'term) ->
mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
aliases:'alias DisambiguateTypes.Environment.t ->
universe:'alias list DisambiguateTypes.Environment.t option ->
- rdb:#NRstatus.status ->
+ rdb:#NCicCoercion.status ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
aliases:'alias DisambiguateTypes.Environment.t ->
universe:'alias list DisambiguateTypes.Environment.t option ->
- rdb:#NRstatus.status ->
+ rdb:#NCicCoercion.status ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
let init = load_db;;
-type automation_cache = NDiscriminationTree.DiscriminationTree.t
-type unit_eq_cache = NCicParamod.state
-
-class type g_eq_status =
- object
- method eq_cache : unit_eq_cache
- end
-
-class eq_status =
- object(self)
- val eq_cache = NCicParamod.empty_state
- method eq_cache = eq_cache
- method set_eq_cache v = {< eq_cache = v >}
- method set_eq_status
- : 'status. #g_eq_status as 'status -> 'self
- = fun o -> self#set_eq_cache o#eq_cache
- end
-
-class type g_auto_status =
- object
- method auto_cache : automation_cache
- end
-
-class auto_status =
- object(self)
- val auto_cache = NDiscriminationTree.DiscriminationTree.empty
- method auto_cache = auto_cache
- method set_auto_cache v = {< auto_cache = v >}
- method set_auto_status
- : 'status. #g_auto_status as 'status -> 'self
- = fun o -> self#set_auto_cache o#auto_cache
- end
-
class type g_status =
object
- inherit NRstatus.g_status
method timestamp: timestamp
end
class status =
object(self)
- inherit NRstatus.status
val timestamp = (time0 : timestamp)
method timestamp = timestamp
method set_timestamp v = {< timestamp = v >}
type obj = string * Obj.t
-
-class type g_dumpable_status =
- object
- inherit g_status
- inherit g_auto_status
- inherit g_eq_status
- method dump: obj list
- end
-
class dumpable_status =
object(self)
- inherit status
- inherit auto_status
- inherit eq_status
val dump = ([] : obj list)
method dump = dump
method set_dump v = {< dump = v >}
- method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self
- = fun o ->
- (((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o)#set_eq_status o
end
-type 'a register_type =
- < run: 'status.
- 'a -> refresh_uri_in_universe:(NCic.universe ->
- NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) ->
- (#dumpable_status as 'status) -> 'status >
+module type SerializerType =
+ sig
+ type dumpable_status
+
+ type 'a register_type =
+ 'a ->
+ refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
+ refresh_uri_in_term:(NCic.term -> NCic.term) ->
+ dumpable_status -> dumpable_status
+
+ val register: < run: 'a. string -> 'a register_type -> ('a -> obj) >
+ val serialize: baseuri:NUri.uri -> obj list -> unit
+ (* the obj is the "include" command to be added to the dump list *)
+ val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj
+ end
-module Serializer =
+module Serializer(D: sig type dumpable_status end) =
struct
- let require1 = ref (object method run : 'status. obj -> (#dumpable_status as 'status) -> 'status = fun _ -> assert false end (* unknown data*))
+ type dumpable_status = D.dumpable_status
+ type 'a register_type =
+ 'a ->
+ refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
+ refresh_uri_in_term:(NCic.term -> NCic.term) ->
+ dumpable_status -> dumpable_status
+
+ let require1 = ref (fun _ -> assert false) (* unknown data*)
let already_registered = ref []
let register =
already_registered := tag :: !already_registered;
let old_require1 = !require1 in
require1 :=
- object
- method run : 'status. obj -> (#dumpable_status as 'status) -> 'status =
- fun ((tag',data) as x) ->
- if tag=tag' then
- require#run (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
- else
- old_require1#run x
- end;
+ (fun ((tag',data) as x) ->
+ if tag=tag' then
+ require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
+ else
+ old_require1 x);
(fun x -> tag,Obj.repr x)
end
try
includes := baseuri::!includes;
let dump = require0 ~baseuri in
- List.fold_right !require1#run dump status
+ List.fold_right !require1 dump status
with
Sys_error _ ->
raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri))
(* memorizzo baseuri in una tabella; *)
require2 ~baseuri
in
- register#run "include"
- object(self : 'a register_type)
- method run = aux
- end
+ register#run "include" aux
let require ~baseuri status =
let status = require2 ~baseuri status in
- let dump = record_include baseuri :: status#dump in
- status#set_dump dump
+ status,record_include baseuri
end
exception LibraryOutOfSync of string Lazy.t
-type automation_cache = NDiscriminationTree.DiscriminationTree.t
-type unit_eq_cache = NCicParamod.state
-
-class type g_eq_status =
- object
- method eq_cache : unit_eq_cache
- end
-
-class eq_status :
- object('self)
- inherit g_eq_status
- method set_eq_cache: unit_eq_cache -> 'self
- method set_eq_status: #g_eq_status -> 'self
- end
-
-class type g_auto_status =
- object
- method auto_cache : automation_cache
- end
-
-class auto_status :
- object('self)
- inherit g_auto_status
- method set_auto_cache: automation_cache -> 'self
- method set_auto_status: #g_auto_status -> 'self
- end
-
type timestamp
class type g_status =
object
method timestamp: timestamp
- inherit NRstatus.g_status
end
class status :
type obj
-class type g_dumpable_status =
- object
- inherit g_status
- inherit g_auto_status
- inherit g_eq_status
- method dump: obj list
- end
-
-class dumpable_status :
- object ('self)
- inherit status
- inherit auto_status
- inherit eq_status
- inherit g_dumpable_status
- method set_dump: obj list -> 'self
- method set_dumpable_status: #g_dumpable_status -> 'self
- end
+module type SerializerType =
+ sig
+ type dumpable_status
-type 'a register_type =
- < run: 'status.
- 'a -> refresh_uri_in_universe:(NCic.universe ->
- NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) ->
- (#dumpable_status as 'status) -> 'status >
+ type 'a register_type =
+ 'a ->
+ refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
+ refresh_uri_in_term:(NCic.term -> NCic.term) ->
+ dumpable_status -> dumpable_status
-module Serializer:
- sig
val register: < run: 'a. string -> 'a register_type -> ('a -> obj) >
val serialize: baseuri:NUri.uri -> obj list -> unit
- val require: baseuri:NUri.uri -> (#dumpable_status as 'status) -> 'status
+ (* the obj is the "include" command to be added to the dump list *)
+ val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj
+ end
+
+module Serializer(D: sig type dumpable_status end) :
+ SerializerType with type dumpable_status = D.dumpable_status
+
+class dumpable_status :
+ object ('self)
+ method dump: obj list
+ method set_dump: obj list -> 'self
end
(* CSC: only required during old-to-NG phase, to be deleted *)
(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
val nparamod :
- #NRstatus.status ->
+ #NCicCoercion.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
(NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
(NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
val is_equation: NCic.metasenv ->
NCic.substitution -> NCic.context -> NCic.term -> bool
val paramod :
- #NRstatus.status ->
+ #NCicCoercion.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
state ->
(NCic.term * NCic.term) ->
(NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
val fast_eq_check :
- #NRstatus.status ->
+ #NCicCoercion.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
state ->
(NCic.term * NCic.term) ->
(NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
val demod :
- #NRstatus.status ->
+ #NCicCoercion.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
state ->
(NCic.term * NCic.term) ->
nCicMetaSubst.mli \
nCicUnifHint.mli \
nCicCoercion.mli \
- nRstatus.mli \
- nCicRefineUtil.mli \
+ nCicRefineUtil.mli \
nCicUnification.mli \
nCicRefiner.mli
exception AssertFailure of string Lazy.t;;
val typeof :
- #NRstatus.status ->
+ #NCicCoercion.status ->
?localise:(NCic.term -> Stdpp.location) ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term option -> (* term, expected type *)
(* menv, subst,refined term, type *)
val typeof_obj :
- #NRstatus.status ->
+ #NCicCoercion.status ->
?localise:(NCic.term -> Stdpp.location) ->
NCic.obj -> NCic.obj
exception AssertFailure of string Lazy.t;;
val unify :
- #NRstatus.status ->
+ #NCicCoercion.status ->
?test_eq_only:bool -> (* default: false *)
?swap:bool -> (* default: false *)
NCic.metasenv -> NCic.substitution -> NCic.context ->
* [ rel 1 ... rel (len args) / lift (length args) (arg_1 .. arg_n) ]
*)
val delift_type_wrt_terms:
- #NRstatus.status ->
+ #NCicCoercion.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term list ->
NCic.metasenv * NCic.substitution * NCic.term
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
-
-class type g_status = NCicCoercion.status
-
-class status = NCicCoercion.status
-
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
-
-class type g_status = NCicCoercion.status
-
-class status : NCicCoercion.status
-
if !debug then prerr_endline (Lazy.force x) else ()
;;
+type automation_cache = NDiscriminationTree.DiscriminationTree.t
+type unit_eq_cache = NCicParamod.state
+
exception Error of string lazy_t * exn option
let fail ?exn msg = raise (Error (msg,exn))
| NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
;;
+class type g_eq_status =
+ object
+ method eq_cache : unit_eq_cache
+ end
+
+class eq_status =
+ object(self)
+ val eq_cache = NCicParamod.empty_state
+ method eq_cache = eq_cache
+ method set_eq_cache v = {< eq_cache = v >}
+ method set_eq_status
+ : 'status. #g_eq_status as 'status -> 'self
+ = fun o -> self#set_eq_cache o#eq_cache
+ end
+
+class type g_auto_status =
+ object
+ method auto_cache : automation_cache
+ end
+
+class auto_status =
+ object(self)
+ val auto_cache = NDiscriminationTree.DiscriminationTree.empty
+ method auto_cache = auto_cache
+ method set_auto_cache v = {< auto_cache = v >}
+ method set_auto_status
+ : 'status. #g_auto_status as 'status -> 'self
+ = fun o -> self#set_auto_cache o#auto_cache
+ end
+
class type g_pstatus =
object
- inherit NEstatus.g_status
+ inherit GrafiteDisambiguate.g_status
+ inherit g_auto_status
+ inherit g_eq_status
method obj: NCic.obj
end
class pstatus =
fun (o: NCic.obj) ->
object (self)
- inherit NEstatus.status
+ inherit GrafiteDisambiguate.status
+ inherit auto_status
+ inherit eq_status
val obj = o
method obj = obj
method set_obj o = {< obj = o >}
method set_pstatus : 'status. #g_pstatus as 'status -> 'self
- = fun o -> (self#set_estatus o)#set_obj o#obj
+ = fun o ->
+ (((self#set_lexicon_engine_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o
end
type tactic_term = NotationPt.term Disambiguate.disambiguator_input
exception Error of string lazy_t * exn option
val fail: ?exn:exn -> string lazy_t -> 'a
+type automation_cache = NDiscriminationTree.DiscriminationTree.t
+type unit_eq_cache = NCicParamod.state
+
+class type g_eq_status =
+ object
+ method eq_cache : unit_eq_cache
+ end
+
+class eq_status :
+ object('self)
+ inherit g_eq_status
+ method set_eq_cache: unit_eq_cache -> 'self
+ method set_eq_status: #g_eq_status -> 'self
+ end
+
+class type g_auto_status =
+ object
+ method auto_cache : automation_cache
+ end
+
+class auto_status :
+ object('self)
+ inherit g_auto_status
+ method set_auto_cache: automation_cache -> 'self
+ method set_auto_status: #g_auto_status -> 'self
+ end
+
class type g_pstatus =
object
- inherit NEstatus.g_status
+ inherit GrafiteDisambiguate.g_status
+ inherit g_auto_status
+ inherit g_eq_status
method obj: NCic.obj
end
class pstatus :
NCic.obj ->
object ('self)
- inherit NEstatus.status
+ inherit GrafiteDisambiguate.status
+ inherit auto_status
+ inherit eq_status
method obj: NCic.obj
method set_obj: NCic.obj -> 'self
method set_pstatus: #g_pstatus -> 'self
((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
;;
-let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
+let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
let repeat_tac t s =
let rec repeat t (status : #tac_status as 'a) : 'a =
?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic
val atomic_tac :
- (((int * Continuationals.Stack.switch) list * 'a list * 'b list *
- [> `NoTag ])
- list NTacStatus.status ->
- (< auto_cache : NCicLibrary.automation_cache;
- eq_cache : NCicLibrary.unit_eq_cache;
- coerc_db : NCicCoercion.db; dump : NCicLibrary.obj list;
- lstatus : LexiconEngine.lexicon_status; obj : NCic.obj;
- set_coerc_db : NCicCoercion.db -> 'c;
- set_coercion_status : 'd. (#NCicCoercion.g_status as 'd) -> 'c;
- set_uhint_db : NCicUnifHint.db -> 'c;
- set_unifhint_status : 'e. (#NCicUnifHint.g_status as 'e) -> 'c;
- timestamp : NCicLibrary.timestamp; uhint_db : NCicUnifHint.db; .. >
- as 'c)) ->
- (#NTacStatus.tac_status as 'f) -> 'f
+ (NTacStatus.tac_status -> 'c #NTacStatus.status) ->
+ (#NTacStatus.tac_status as 'f) -> 'f
type indtyinfo
--- /dev/null
+grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon +nciccoercion)
+ |--> dumpable |
+ |--> nciclibrary interpretation
+
+ntermciccontent -> nciccoercion+interpretation
+ |
+ unif_hint
val ntxt_of_cic_sequent:
map_unicode_to_tex:bool -> int ->
- #NCicCoercion.status ->
+ #NTermCicContent.status ->
NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
int * NCic.conjecture -> (* sequent *)
string (* text *)
val ntxt_of_cic_object:
- map_unicode_to_tex:bool -> int -> #NCicCoercion.status -> NCic.obj -> string
+ map_unicode_to_tex:bool -> int -> #NTermCicContent.status -> NCic.obj -> string
val mutable current_mathml = None
method nload_sequent:
- 'status. #NCicCoercion.status as 'status -> NCic.metasenv ->
+ 'status. #NTermCicContent.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. #NCicCoercion.status as 'status -> NCic.obj -> unit
+ 'status. #NTermCicContent.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
self#script#setGoal None
method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
- = fun status ->
+ = fun (status : #NTacStatus.tac_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. #NCicCoercion.status as 'status -> page:int ->
+ 'status. #NTermCicContent.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. #NCicCoercion.status as 'status -> int -> unit
+ method goto_sequent: 'status. #NTermCicContent.status as 'status -> int -> unit
= fun status goal ->
let goal_switch, page =
try
projects / helm.git / commitdiff