helm/software/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 TermAcicContent.interpretation_id
  33   | PrettyPrinterId of TermContentPres.pretty_printer_id
  34
  35 let compare_notation_id x y =
  36   match x,y with
  37   | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
  38   | RuleId _, _ -> ~-1
  39   | _, RuleId _ -> 1
  40   | x,y -> Pervasives.compare x y
  41
  42 let initial_parser_ref_counter () = RefCounter.create ()
  43 let initial_rule_ids_to_items ()= Hashtbl.create 113
  44
  45 let parser_ref_counter = ref (initial_parser_ref_counter ());;
  46 let rule_ids_to_items = ref (initial_rule_ids_to_items ());;
  47
  48 let process_notation st =
  49   match st with
  50   | Notation (loc, dir, l1, associativity, precedence, l2) ->
  51       let l1 =
  52         CicNotationParser.check_l1_pattern
  53          l1 (dir = Some `RightToLeft) precedence associativity
  54       in
  55       let item = (l1, precedence, associativity, l2) in
  56       let rule_id = ref [] in
  57       let _ =
  58         if dir <> Some `RightToLeft then
  59           let create_cb (l1, precedence, associativity, l2) =
  60             let id =
  61               CicNotationParser.extend l1
  62                 (fun env loc ->
  63                   CicNotationPt.AttributedTerm
  64                    (`Loc loc,TermContentPres.instantiate_level2 env l2)) in
  65             rule_id := [ RuleId id ];
  66             Hashtbl.add !rule_ids_to_items id item
  67           in
  68           RefCounter.incr ~create_cb !parser_ref_counter item
  69       in
  70       let pp_id =
  71         if dir <> Some `LeftToRight then
  72           [ PrettyPrinterId
  73               (TermContentPres.add_pretty_printer
  74                 l2 l1) ]
  75         else
  76           []
  77       in
  78       !rule_id @ pp_id
  79   | Interpretation (loc, dsc, l2, l3) ->
  80       let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in
  81        [InterpretationId interp_id]
  82   | st -> []
  83
  84 (* CSC: Matita compiled with recent OCaml triggers the assert false in the
  85    code below. The exception FOO trick ignores the failure. It seems to
  86    work, but it's the classical patch without understanding what the problem
  87    is. *)
  88 exception FOO;;
  89
  90 let remove_notation = function
  91 xxx -> try match xxx with
  92   | RuleId id ->
  93       let item =
  94         try
  95           Hashtbl.find !rule_ids_to_items id
  96         with Not_found -> raise FOO (*assert false*) in
  97       RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
  98         !parser_ref_counter item
  99   | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
 100   | InterpretationId id -> TermAcicContent.remove_interpretation id
 101 with FOO -> ();;
 102
 103 let get_all_notations () =
 104   List.map
 105     (fun (interp_id, dsc) ->
 106       InterpretationId interp_id, "interpretation: " ^ dsc)
 107     (TermAcicContent.get_all_interpretations ())
 108
 109 let get_active_notations () =
 110   List.map (fun id -> InterpretationId id)
 111     (TermAcicContent.get_active_interpretations ())
 112
 113 let set_active_notations ids =
 114   let interp_ids =
 115     HExtlib.filter_map
 116       (function InterpretationId interp_id -> Some interp_id | _ -> None)
 117       ids
 118   in
 119   TermAcicContent.set_active_interpretations interp_ids
 120
 121 let history = ref [];;
 122
 123 let push () =
 124  history := (!parser_ref_counter,!rule_ids_to_items) :: !history;
 125  parser_ref_counter := initial_parser_ref_counter ();
 126  rule_ids_to_items := initial_rule_ids_to_items ();
 127  TermContentPres.push ();
 128  TermAcicContent.push ();
 129  CicNotationParser.push ()
 130 ;;
 131
 132 let pop () =
 133  TermContentPres.pop ();
 134  TermAcicContent.pop ();
 135  CicNotationParser.pop ();
 136  match !history with
 137  | [] -> assert false
 138  | (prc,riti) :: tail ->
 139      parser_ref_counter := prc;
 140      rule_ids_to_items := riti;
 141      history := tail;
 142 ;;