matita/components/lexicon/cicNotation.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open LexiconAst
  29
  30 type notation_id =
  31   | RuleId of CicNotationParser.rule_id
  32   | InterpretationId of Interpretations.interpretation_id
  33   | PrettyPrinterId of TermContentPres.pretty_printer_id
  34
  35 class type g_status =
  36  object ('self)
  37   inherit Interpretations.g_status
  38   inherit TermContentPres.g_status
  39  end
  40
  41 class status =
  42  object (self)
  43   inherit Interpretations.status
  44   inherit TermContentPres.status
  45   method set_notation_status
  46    : 'status. #g_status as 'status -> 'self
  47       = fun o -> (self#set_interp_status o)#set_content_pres_status o
  48  end
  49
  50 let compare_notation_id x y =
  51   match x,y with
  52   | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
  53   | RuleId _, _ -> ~-1
  54   | _, RuleId _ -> 1
  55   | x,y -> Pervasives.compare x y
  56
  57 let initial_parser_ref_counter () = RefCounter.create ()
  58 let initial_rule_ids_to_items ()= Hashtbl.create 113
  59
  60 let parser_ref_counter = ref (initial_parser_ref_counter ());;
  61 let rule_ids_to_items = ref (initial_rule_ids_to_items ());;
  62
  63 let process_notation status st =
  64   match st with
  65   | Notation (loc, dir, l1, associativity, precedence, l2) ->
  66       let l1 =
  67         CicNotationParser.check_l1_pattern
  68          l1 (dir = Some `RightToLeft) precedence associativity
  69       in
  70       let item = (l1, precedence, associativity, l2) in
  71       let rule_id = ref [] in
  72       let _ =
  73         if dir <> Some `RightToLeft then
  74           let create_cb (l1, precedence, associativity, l2) =
  75             let id =
  76               CicNotationParser.extend l1
  77                 (fun env loc ->
  78                   NotationPt.AttributedTerm
  79                    (`Loc loc,TermContentPres.instantiate_level2 env l2)) in
  80             rule_id := [ RuleId id ];
  81             Hashtbl.add !rule_ids_to_items id item
  82           in
  83           RefCounter.incr ~create_cb !parser_ref_counter item
  84       in
  85       let status,pp_id =
  86         if dir <> Some `LeftToRight then
  87          let status,id = TermContentPres.add_pretty_printer status l2 l1 in
  88           status,[ PrettyPrinterId id ]
  89         else
  90           status,[]
  91       in
  92        status,!rule_id @ pp_id
  93   | Interpretation (loc, dsc, l2, l3) ->
  94       let status,interp_id =
  95         Interpretations.add_interpretation status dsc l2 l3
  96       in
  97        status,[InterpretationId interp_id]
  98   | st -> status,[]
  99
 100 let remove_notation = function
 101   | RuleId id ->
 102       let item =
 103         try
 104           Hashtbl.find !rule_ids_to_items id
 105         with Not_found -> assert false in
 106       RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
 107         !parser_ref_counter item
 108   | PrettyPrinterId id -> ()
 109   | InterpretationId id -> ()
 110
 111 let history = ref [];;
 112
 113 let push () =
 114  history := (!parser_ref_counter,!rule_ids_to_items) :: !history;
 115  parser_ref_counter := initial_parser_ref_counter ();
 116  rule_ids_to_items := initial_rule_ids_to_items ();
 117  CicNotationParser.push ()
 118 ;;
 119
 120 let pop () =
 121  CicNotationParser.pop ();
 122  match !history with
 123  | [] -> assert false
 124  | (prc,riti) :: tail ->
 125      parser_ref_counter := prc;
 126      rule_ids_to_items := riti;
 127      history := tail;
 128 ;;