1 (* Copyright (C) 2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 let pp_l1_pattern = CicNotationPp.pp_term
31 let pp_l2_pattern = CicNotationPp.pp_term
33 let pp_alias = function
34 | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
35 | Symbol_alias (symb, instance, desc) ->
36 sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
38 | Number_alias (instance,desc) ->
39 sprintf "alias num (instance %d) = \"%s\"" instance desc
41 let pp_associativity = function
42 | Gramext.LeftA -> "left associative"
43 | Gramext.RightA -> "right associative"
44 | Gramext.NonA -> "non associative"
46 let pp_precedence i = sprintf "with precedence %d" i
48 let pp_argument_pattern = function
49 | CicNotationPt.IdentArg (eta_depth, name) ->
50 let eta_buf = Buffer.create 5 in
51 for i = 1 to eta_depth do
52 Buffer.add_string eta_buf "\\eta."
54 sprintf "%s%s" (Buffer.contents eta_buf) name
56 let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
57 sprintf "interpretation \"%s\" '%s %s = %s"
59 (String.concat " " (List.map pp_argument_pattern arg_patterns))
60 (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
62 let pp_dir_opt = function
64 | Some `LeftToRight -> "> "
65 | Some `RightToLeft -> "< "
67 let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
68 sprintf "notation %s\"%s\" %s %s for %s"
70 (pp_l1_pattern l1_pattern)
71 (pp_associativity assoc)
73 (pp_l2_pattern l2_pattern)
75 let pp_command = function
76 | Include (_,path) -> "include " ^ path
77 | Alias (_,s) -> pp_alias s
78 | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
79 pp_interpretation dsc symbol arg_patterns cic_appl_pattern
80 | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
81 pp_notation dir_opt l1_pattern assoc prec l2_pattern