]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/binaries/transcript/grafite.ml
transcript updated
[helm.git] / helm / software / components / binaries / transcript / grafite.ml
1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
24  *)
25
26 module T = Types
27
28 module NP = CicNotationPp
29 module GP = GrafiteAstPp
30 module G = GrafiteAst
31 module H = HExtlib
32
33 let floc = H.dummy_floc
34
35 let out_verbatim och s =
36    Printf.fprintf och "%s" s
37
38 let out_comment och s =
39    let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in 
40    Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
41
42 let out_unexported och head s =
43    let s = Printf.sprintf " %s\n%s\n" head s in
44    out_comment och s
45
46 let out_line_comment och s =
47    let l = 70 - String.length s in
48    let s = Printf.sprintf " %s %s" s (String.make l '*') in
49    out_comment och s
50
51 let out_preamble och (path, lines) =
52    let ich = open_in path in
53    let rec print i =
54       if i > 0 then 
55          let s = input_line ich in
56          begin Printf.fprintf och "%s\n" s; print (pred i) end
57    in 
58    print lines;
59    out_line_comment och "This file was automatically generated: do not edit"
60       
61 let out_command och cmd =
62    let term_pp = NP.pp_term in
63    let lazy_term_pp = NP.pp_term in
64    let obj_pp = NP.pp_obj in
65    let s = GP.pp_statement ~term_pp ~lazy_term_pp ~obj_pp cmd in
66    Printf.fprintf och "%s\n\n" s
67
68 let command_of_obj obj =
69    G.Executable (floc, G.Command (floc, obj))
70
71 let command_of_macro macro =
72    G.Executable (floc, G.Macro (floc, macro))
73
74 let set key value =
75    command_of_obj (G.Set (floc, key, value))
76
77 let require value =
78    command_of_obj (G.Include (floc, value ^ ".ma"))
79
80 let inline value =
81     command_of_macro (G.Inline (floc, value))
82
83 let commit och items =
84    let commit = function
85       | T.Heading heading   -> out_preamble och heading
86       | T.Line line         -> out_line_comment och line
87       | T.BaseUri baseuri   -> out_command och (set "baseuri" baseuri)
88       | T.Include inc       -> out_unexported och "INCLUDE" inc (**)
89       | T.Coercion coercion -> out_unexported och "COERCION" coercion (**)
90       | T.Notation notation -> out_unexported och "NOTATION" notation (**)
91       | T.Inline (_, uri)   -> out_command och (inline uri)  
92       | T.Comment comment   -> out_comment och comment
93       | T.Unexport unexport -> out_unexported och "UNEXPORTED" unexport 
94       | T.Verbatim verbatim -> out_verbatim och verbatim
95       | T.Discard _         -> ()
96    in 
97    List.iter commit (List.rev items)
98
99 let string_of_inline_kind = function
100    | T.Con -> ".con"
101    | T.Var -> ".var"
102    | T.Ind -> ".ind"