1 (* Goalfile Abstract Syntax Tree
2 * Copyright (C) 2019 Richard W.M. Jones
3 * Copyright (C) 2019 Red Hat Inc.
5 * This program is free software; you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation; either version 2 of the License, or
8 * (at your option) any later version.
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License along
16 * with this program; if not, write to the Free Software Foundation, Inc.,
17 * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
23 module StringMap = Map.Make (String)
25 type loc = position * position
26 let noloc = dummy_pos, dummy_pos
28 let string_loc () loc =
30 sprintf "%s:%d:%d" pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol)
31 let print_loc fp loc =
32 fprintf fp "%s" (string_loc () loc)
34 type env = expr StringMap.t
36 | PTactic of loc * id * substs list
40 | ECall of loc * id * expr list
41 | ETactic of loc * id * expr list
43 | EList of loc * expr list
44 | ESubsts of loc * substs
45 | EConstant of loc * constant
48 and goal = id list * pattern list * expr list * code option
51 and substs = subst list
56 module Substs = struct
58 mutable elems : subst list; (* built in reverse order *)
59 curr : Buffer.t; (* current string *)
62 let create () = { elems = []; curr = Buffer.create 13 }
65 if Buffer.length t.curr > 0 then
66 t.elems <- SString (Buffer.contents t.curr) :: t.elems;
69 let get t = finalize t; List.rev t.elems
71 let add_char { curr } = Buffer.add_char curr
72 let add_string { curr} = Buffer.add_string curr
73 let add_var t id = finalize t; t.elems <- SVar id :: t.elems
77 : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
79 let comma = ref false in
82 if !comma then fprintf fp ", ";
87 let rec print_env fp env =
88 StringMap.iter (print_def fp) env
90 and print_def fp name expr =
92 | EGoal (loc, (params, patterns, exprs, code)) ->
93 fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
95 iter_with_commas fp print_pattern patterns;
97 iter_with_commas fp print_expr exprs;
107 fprintf fp "let %s = " name;
111 and print_pattern fp = function
112 | PTactic (loc, name, params) ->
113 fprintf fp "*%s (" name;
114 iter_with_commas fp print_substs params;
116 | PVar (loc, id) -> print_id fp id
118 and print_expr fp = function
119 | EGoal _ -> assert false (* printed above *)
120 | ECall (loc, name, params) ->
121 fprintf fp "%s (" name;
122 iter_with_commas fp print_expr params;
124 | ETactic (loc, name, params) ->
125 fprintf fp "*%s (" name;
126 iter_with_commas fp print_expr params;
128 | EVar (loc, var) -> print_id fp var
131 iter_with_commas fp print_expr xs;
133 | ESubsts (loc, s) -> print_substs fp s
134 | EConstant (loc, c) -> print_constant fp c
136 and print_constant fp = function
137 | CString s -> fprintf fp "%S" s
139 and print_id = output_string
141 and print_substs fp xs =
145 | SString s -> sprintf "%S" s
148 fprintf fp "%s" (String.concat "+" xs)
150 and print_code fp xs =
153 | SString s -> fprintf fp "%s" s
154 | SVar id -> fprintf fp "%%%s" id