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.
22 module StringMap = Map.Make (String)
24 type env = expr StringMap.t
26 | PTactic of id * substs list
30 | ECall of id * expr list
34 | EConstant of constant
37 and goal = id list * pattern list * expr list * code option
40 and substs = subst list
45 module Substs = struct
47 mutable elems : subst list; (* built in reverse order *)
48 curr : Buffer.t; (* current string *)
51 let create () = { elems = []; curr = Buffer.create 13 }
54 if Buffer.length t.curr > 0 then
55 t.elems <- SString (Buffer.contents t.curr) :: t.elems;
58 let get t = finalize t; List.rev t.elems
60 let add_char { curr } = Buffer.add_char curr
61 let add_string { curr} = Buffer.add_string curr
62 let add_var t id = finalize t; t.elems <- SVar id :: t.elems
66 : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
68 let comma = ref false in
71 if !comma then fprintf fp ", ";
76 let rec print_env fp env =
77 StringMap.iter (print_def fp) env
79 and print_def fp name expr =
81 | EGoal (params, patterns, exprs, code) ->
82 fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
84 iter_with_commas fp print_pattern patterns;
86 iter_with_commas fp print_expr exprs;
96 fprintf fp "let %s = " name;
100 and print_pattern fp = function
101 | PTactic (name, params) ->
102 fprintf fp "%s (" name;
103 iter_with_commas fp print_substs params;
105 | PVar id -> print_id fp id
107 and print_expr fp = function
108 | EGoal _ -> assert false (* printed above *)
109 | ECall (name, params) ->
110 fprintf fp "%s (" name;
111 iter_with_commas fp print_expr params;
113 | EVar var -> print_id fp var
116 iter_with_commas fp print_expr xs;
118 | ESubsts s -> print_substs fp s
119 | EConstant c -> print_constant fp c
121 and print_constant fp = function
122 | CString s -> fprintf fp "%S" s
124 and print_id = output_string
126 and print_substs fp xs =
130 | SString s -> sprintf "%S" s
133 fprintf fp "%s" (String.concat "+" xs)
135 and print_code fp xs =
138 | SString s -> fprintf fp "%s" s
139 | SVar id -> fprintf fp "%%%s" id