open LexiconAst
-type notation_id =
- | RuleId of CicNotationParser.rule_id
- | 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
+ inherit CicNotationParser.g_status
+ end
-let compare_notation_id x y =
- match x,y with
- | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
- | RuleId _, _ -> ~-1
- | _, RuleId _ -> 1
- | x,y -> Pervasives.compare x y
+class status =
+ object (self)
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ inherit CicNotationParser.status
+ method set_notation_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> ((self#set_interp_status o)#set_content_pres_status o)#set_notation_parser_status o
+ end
-let initial_parser_ref_counter () = RefCounter.create ()
-let initial_rule_ids_to_items ()= Hashtbl.create 113
-
-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 =
CicNotationParser.check_l1_pattern
l1 (dir = Some `RightToLeft) precedence associativity
in
- let item = (l1, precedence, associativity, l2) in
- let rule_id = ref [] in
- let _ =
+ let status =
if dir <> Some `RightToLeft then
- let create_cb (l1, precedence, associativity, l2) =
- let id =
- CicNotationParser.extend l1
- (fun env loc ->
- NotationPt.AttributedTerm
- (`Loc loc,TermContentPres.instantiate_level2 env l2)) in
- rule_id := [ RuleId id ];
- Hashtbl.add !rule_ids_to_items id item
- in
- RefCounter.incr ~create_cb !parser_ref_counter item
+ CicNotationParser.extend status l1
+ (fun env loc ->
+ NotationPt.AttributedTerm
+ (`Loc loc,TermContentPres.instantiate_level2 env l2))
+ else status
in
- let pp_id =
+ let status =
if dir <> Some `LeftToRight then
- [ PrettyPrinterId
- (TermContentPres.add_pretty_printer
- l2 l1) ]
+ let status = TermContentPres.add_pretty_printer status l2 l1 in
+ status
else
- []
+ status
in
- !rule_id @ pp_id
- | Interpretation (loc, dsc, l2, l3) ->
- let interp_id = Interpretations.add_interpretation dsc l2 l3 in
- [InterpretationId interp_id]
- | st -> []
-
-let remove_notation = function
- | RuleId id ->
- let item =
- try
- Hashtbl.find !rule_ids_to_items id
- 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
- | 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
-
-let history = ref [];;
-
-let push () =
- 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 ();
- Interpretations.push ();
- CicNotationParser.push ()
-;;
+ status
+ | Interpretation (loc, dsc, l2, l3) ->
+ Interpretations.add_interpretation status dsc l2 l3
+ | st -> status
-let pop () =
- TermContentPres.pop ();
- Interpretations.pop ();
- CicNotationParser.pop ();
- match !history with
- | [] -> assert false
- | (prc,riti) :: tail ->
- parser_ref_counter := prc;
- rule_ids_to_items := riti;
- history := tail;
-;;