Still mostly untested.
joint.Content.joint_kind joint.Content.joint_defs]
| _ -> raise ToDo
-let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
+let ncontent2pres status ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
let lookup_uri id =
try
let nref = Hashtbl.find ids_to_nrefs id in
ncontent2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
(fun ?(prec=90) ast ->
CicNotationPres.box_of_mpres
- (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast)))
+ (CicNotationPres.render ~lookup_uri ~prec
+ (TermContentPres.pp_ast status ast)))
(**************************************************************************)
val ncontent2pres:
+ #TermContentPres.status ->
?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool ->
ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t ->
NotationPt.term Content.cobj ->
CicNotationPres.boxml_markup
-
Box.b_space;
pres_goal]))])
-let nsequent2pres ~ids_to_nrefs ~subst =
+let nsequent2pres status ~ids_to_nrefs ~subst =
let lookup_uri id =
try
let nref = Hashtbl.find ids_to_nrefs id in
(fun ast ->
CicNotationPres.box_of_mpres
(CicNotationPres.render ~lookup_uri
- (TermContentPres.pp_ast ast)))
+ (TermContentPres.pp_ast status ast)))
(***************************************************************************)
val nsequent2pres :
+ #TermContentPres.status ->
ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t ->
subst:NCic.substitution -> NotationPt.term Content.conjecture ->
CicNotationPres.boxml_markup
(* persistent state *)
-let initial_level1_patterns21 () = Hashtbl.create 211
-let level1_patterns21 = ref (initial_level1_patterns21 ())
-let compiled21 = ref None
-let pattern21_matrix = ref []
-let counter = ref ~-1
-
-let stack = ref [];;
-
-let push () =
- stack := (!counter,!level1_patterns21,!compiled21,!pattern21_matrix)::!stack;
- counter := ~-1;
- level1_patterns21 := initial_level1_patterns21 ();
- compiled21 := None;
- pattern21_matrix := []
-;;
-
-let pop () =
- match !stack with
- [] -> assert false
- | (ocounter,olevel1_patterns21,ocompiled21,opatterns21_matrix)::old ->
- stack := old;
- counter := ocounter;
- level1_patterns21 := olevel1_patterns21;
- compiled21 := ocompiled21;
- pattern21_matrix := opatterns21_matrix
-;;
-
-let get_compiled21 () =
- match !compiled21 with
+module IntMap = Map.Make(struct type t = int let compare = compare end);;
+
+type db = {
+ level1_patterns21: NotationPt.term IntMap.t;
+ compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t option;
+ pattern21_matrix: (NotationPt.term * pattern_id) list;
+ counter: pattern_id
+}
+
+let initial_db = {
+ level1_patterns21 = IntMap.empty;
+ compiled21 = None;
+ pattern21_matrix = [];
+ counter = ~-1
+}
+
+class type g_status =
+ object
+ method content_pres_db: db
+ end
+
+class status =
+ object
+ val content_pres_db = initial_db
+ method content_pres_db = content_pres_db
+ method set_content_pres_db v = {< content_pres_db = v >}
+ method set_content_pres_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< content_pres_db = o#content_pres_db >}
+ end
+
+let get_compiled21 status =
+ match status#content_pres_db.compiled21 with
| None -> assert false
| Some f -> Lazy.force f
-let set_compiled21 f = compiled21 := Some f
+let set_compiled21 status f =
+ status#set_content_pres_db
+ { status#content_pres_db with compiled21 = Some f }
let add_idrefs =
List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
in
subst_singleton `Left env l1
-let rec pp_ast1 term =
+let rec pp_ast1 status term =
let rec pp_value = function
| NotationEnv.NumValue _ as v -> v
| NotationEnv.StringValue _ as v -> v
(* | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 t pp_ast1) *)
- | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 t)
+ | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 status t)
| NotationEnv.OptValue None as v -> v
| NotationEnv.OptValue (Some v) ->
NotationEnv.OptValue (Some (pp_value v))
(* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *)
match term with
| Ast.AttributedTerm (attrs, term') ->
- Ast.AttributedTerm (attrs, pp_ast1 term')
+ Ast.AttributedTerm (attrs, pp_ast1 status term')
| _ ->
- (match (get_compiled21 ()) term with
- | None -> pp_ast0 term pp_ast1
+ (match get_compiled21 status term with
+ | None -> pp_ast0 term (pp_ast1 status)
| Some (env, ctors, pid) ->
let idrefs =
List.flatten (List.map NotationUtil.get_idrefs ctors)
in
let l1 =
try
- Hashtbl.find !level1_patterns21 pid
+ IntMap.find pid status#content_pres_db.level1_patterns21
with Not_found -> assert false
in
instantiate21 idrefs (ast_env_of_env env) l1)
-let load_patterns21 t =
- set_compiled21 (lazy (Content2presMatcher.Matcher21.compiler t))
+let load_patterns21 status t =
+ set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t))
-let pp_ast ast =
+let pp_ast status ast =
debug_print (lazy "pp_ast <-");
- let ast' = pp_ast1 ast in
+ let ast' = pp_ast1 status ast in
debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term ast'));
ast'
-exception Pretty_printer_not_found
-
let fill_pos_info l1_pattern = l1_pattern
(* let rec aux toplevel pos =
function
in
aux true l1_pattern *)
-let fresh_id =
- fun () ->
- incr counter;
- !counter
+let fresh_id status =
+ let counter = status#content_pres_db.counter+1 in
+ status#set_content_pres_db ({ status#content_pres_db with counter = counter }), counter
-let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) =
- let id = fresh_id () in
+let add_pretty_printer status l2 (CicNotationParser.CL1P (l1,precedence)) =
+ let status,id = fresh_id status in
let l1' = add_level_info precedence (fill_pos_info l1) in
let l2' = NotationUtil.strip_attributes l2 in
- Hashtbl.add !level1_patterns21 id l1';
- pattern21_matrix := (l2', id) :: !pattern21_matrix;
- load_patterns21 !pattern21_matrix;
- id
-
-let remove_pretty_printer id =
- (try
- Hashtbl.remove !level1_patterns21 id;
- with Not_found -> raise Pretty_printer_not_found);
- pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix;
- load_patterns21 !pattern21_matrix
+ let status =
+ status#set_content_pres_db
+ { status#content_pres_db with
+ level1_patterns21 =
+ IntMap.add id l1' status#content_pres_db.level1_patterns21;
+ pattern21_matrix = (l2',id)::status#content_pres_db.pattern21_matrix } in
+ let status = load_patterns21 status status#content_pres_db.pattern21_matrix in
+ status,id
(* presentation -> content *)
| _ -> assert false
in
aux env term
-
- (* initialization *)
-
-let _ = load_patterns21 []
-
-
-
* http://helm.cs.unibo.it/
*)
- (** {2 Persistant state handling} *)
+ (** {2 state handling} *)
+
+type db
+
+class type g_status =
+ object
+ method content_pres_db: db
+ end
+
+class status :
+ object ('self)
+ method content_pres_db: db
+ method set_content_pres_db: db -> 'self
+ method set_content_pres_status: #g_status -> 'self
+ end
type pretty_printer_id
val add_pretty_printer:
+ #status as 'status ->
NotationPt.term -> (* level 2 pattern *)
CicNotationParser.checked_l1_pattern ->
- pretty_printer_id
-
-exception Pretty_printer_not_found
-
- (** @raise Pretty_printer_not_found *)
-val remove_pretty_printer: pretty_printer_id -> unit
+ 'status * pretty_printer_id
(** {2 content -> pres} *)
-val pp_ast: NotationPt.term -> NotationPt.term
+val pp_ast: #status -> NotationPt.term -> NotationPt.term
(** {2 pres -> content} *)
val instantiate_level2:
NotationEnv.t -> NotationPt.term ->
NotationPt.term
-
-val push: unit -> unit
-val pop: unit -> unit
| InterpretationId of Interpretations.interpretation_id
| PrettyPrinterId of TermContentPres.pretty_printer_id
+class type g_status =
+ object ('self)
+ inherit Interpretations.g_status
+ inherit TermContentPres.g_status
+ end
+
+class status =
+ object (self)
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ method set_notation_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> (self#set_interp_status o)#set_content_pres_status o
+ end
+
let compare_notation_id x y =
match x,y with
| RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
in
RefCounter.incr ~create_cb !parser_ref_counter item
in
- let pp_id =
+ let status,pp_id =
if dir <> Some `LeftToRight then
- [ PrettyPrinterId
- (TermContentPres.add_pretty_printer
- l2 l1) ]
+ let status,id = TermContentPres.add_pretty_printer status l2 l1 in
+ status,[ PrettyPrinterId id ]
else
- []
+ status,[]
in
status,!rule_id @ pp_id
| Interpretation (loc, dsc, l2, l3) ->
with Not_found -> assert false in
RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
!parser_ref_counter item
- | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
+ | PrettyPrinterId id -> ()
| InterpretationId id -> ()
let history = ref [];;
history := (!parser_ref_counter,!rule_ids_to_items) :: !history;
parser_ref_counter := initial_parser_ref_counter ();
rule_ids_to_items := initial_rule_ids_to_items ();
- TermContentPres.push ();
CicNotationParser.push ()
;;
let pop () =
- TermContentPres.pop ();
CicNotationParser.pop ();
match !history with
| [] -> assert false
type notation_id
+class type g_status =
+ object ('self)
+ inherit Interpretations.g_status
+ inherit TermContentPres.g_status
+ end
+
+class status :
+ object ('self)
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ method set_notation_status: #g_status -> 'self
+ end
+
val compare_notation_id : notation_id -> notation_id -> int
val process_notation:
- #Interpretations.status as 'status -> LexiconAst.command
- -> 'status * notation_id list
+ #status as 'status -> LexiconAst.command -> 'status * notation_id list
val remove_notation: notation_id -> unit
class type g_status =
object
- inherit Interpretations.g_status
+ inherit CicNotation.g_status
method lstatus: lexicon_status
end
class status =
object(self)
- inherit Interpretations.status
+ inherit CicNotation.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
+ = fun o -> (self#set_lstatus o#lstatus)#set_notation_status o
end
let dump_aliases out msg status =
class type g_status =
object
- inherit Interpretations.g_status
+ inherit CicNotation.g_status
method lstatus: lexicon_status
end
class status :
object ('self)
inherit g_status
- inherit Interpretations.status
+ inherit CicNotation.status
method set_lstatus: lexicon_status -> 'self
method set_lexicon_engine_status: #g_status -> 'self
end
grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion)
|--> dumpable | |
- |--> nciclibrary interpretation unif_hint
+ |--> nciclibrary | unif_hint
+ |
+ interpretation + termcontentpres = cicnotation
+
+
+
+
ntermciccontent = nciccoercion+interpretation
|
unif_hint
+
+applytransformation = ntermciccontent+termcontentpres
(* $Id$ *)
+class status =
+ object
+ inherit NTermCicContent.status
+ inherit TermContentPres.status
+ end
+
+
let mpres_document pres_box =
Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
let content_sequent,ids_to_refs =
NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in
let pres_sequent =
- Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
+ Sequent2pres.nsequent2pres status ids_to_refs subst content_sequent in
let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size pres_sequent
let ntxt_of_cic_object ~map_unicode_to_tex size status obj =
let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in
- let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
+ let pres_sequent = Content2pres.ncontent2pres status ~ids_to_nrefs cobj in
let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size pres_sequent
(* *)
(***************************************************************************)
+class status :
+ object ('self)
+ inherit NTermCicContent.status
+ inherit TermContentPres.status
+ end
+
val ntxt_of_cic_sequent:
map_unicode_to_tex:bool -> int ->
- #NTermCicContent.status ->
+ #status ->
NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
int * NCic.conjecture -> (* sequent *)
string (* text *)
val ntxt_of_cic_object:
- map_unicode_to_tex:bool -> int -> #NTermCicContent.status -> NCic.obj -> string
+ map_unicode_to_tex:bool -> int -> #status -> NCic.obj -> string
(** load a sequent and render it into parent widget *)
method nload_sequent:
- #NTermCicContent.status -> NCic.metasenv -> NCic.substitution -> int -> unit
+ #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit
- method load_nobject: #NTermCicContent.status -> NCic.obj -> unit
+ method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit
end
class type sequentsViewer =
method load_logo_with_qed: unit
method nload_sequents: #NTacStatus.tac_status -> unit
method goto_sequent:
- #NTermCicContent.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. #NTermCicContent.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. #NTermCicContent.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
self#render_page status ~page ~goal_switch))
method private render_page:
- 'status. #NTermCicContent.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. #NTermCicContent.status as 'status -> int -> unit
+ method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
= fun status goal ->
let goal_switch, page =
try
-.unnamed.ma datatypes/list.ma sets/setoids.ma
-PTS/subst.ma basics/list2.ma
topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma
+PTS/subst.ma basics/list2.ma
basics/functions.ma Plogic/connectives.ma Plogic/equality.ma
nat/compare.ma datatypes/bool.ma nat/order.ma
arithmetics/compare.ma arithmetics/nat.ma
basics/list2.ma arithmetics/nat.ma basics/list.ma
arithmetics/nat.ma basics/bool.ma basics/eq.ma basics/functions.ma hints_declaration.ma
sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma
+B.ma A.ma
nat/minus.ma nat/order.ma
logic/cologic.ma Plogic/connectives.ma Plogic/equality.ma datatypes/bool.ma logic/equality.ma logic/pts.ma
-SET171^3.ma TPTP.ma
datatypes/list.ma logic/pts.ma
Plogic/jmeq.ma Plogic/equality.ma
sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
topology/igft-setoid.ma sets/sets.ma
sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma
properties/relations.ma logic/pts.ma
-nat/big_ops.ma algebra/magmas.ma nat/order.ma
+nat/big_ops.ma algebra/magmas.ma logic/equality.ma nat/order.ma
arithmetics/R.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma topology/igft.ma
arithmetics/minimization.ma arithmetics/nat.ma
algebra/unital_magmas.ma algebra/magmas.ma
properties/relations1.ma logic/pts.ma
basics/bool.ma basics/eq.ma basics/functions.ma
-datatypes/bool-setoids.ma datatypes/bool.ma sets/setoids.ma
-logic/equality.ma logic/connectives.ma properties/relations.ma
+datatypes/bool-setoids.ma datatypes/bool.ma properties/relations.ma sets/setoids.ma
datatypes/pairs-setoids.ma datatypes/pairs.ma sets/setoids.ma
+logic/equality.ma logic/connectives.ma properties/relations.ma
topology/igft4.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma
basics/eq.ma basics/relations.ma
datatypes/sums.ma datatypes/pairs.ma
hints_declaration.ma logic/pts.ma
+A.ma logic/pts.ma
logic/destruct_bb.ma logic/equality.ma
topology/igft.ma logic/equality.ma sets/sets.ma
-algebra/abelian_magmas.ma algebra/magmas.ma
overlap/o-algebra.ma sets/categories2.ma
+algebra/abelian_magmas.ma algebra/magmas.ma
re/re.ma arithmetics/nat.ma datatypes/list.ma datatypes/pairs.ma hints_declaration.ma
basics/list.ma basics/bool.ma basics/eq.ma
nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma
projects / helm.git / commitdiff