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.
25 module Env = Map.Make (String)
27 type loc = position * position
28 let noloc = dummy_pos, dummy_pos
30 let string_loc () loc =
32 sprintf "%s:%d:%d" pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol)
33 let print_loc fp loc =
34 fprintf fp "%s" (string_loc () loc)
38 | PTactic of loc * id * substs list
42 | ECall of loc * id * expr list
43 | ETactic of loc * id * expr list
45 | EList of loc * expr list
46 | ESubsts of loc * substs
47 | EConstant of loc * constant
50 and goal = id list * pattern list * expr list * code option
53 and substs = subst list
58 let getvar env loc name =
61 failwithf "%a: variable ‘%s’ not found" string_loc loc name
63 let getgoal env loc name =
67 failwithf "%a: goal ‘%s’ not found" string_loc loc name in
70 | EGoal (loc, goal) -> goal
72 failwithf "%a: tried to call ‘%s’ which is not a goal"
73 string_loc loc name in
76 let rec to_constant env = function
77 | EConstant (loc, c) -> c
80 let expr = getvar env loc name in
83 | ESubsts (loc, str) ->
84 CString (substitute env loc str)
87 failwithf "%a: list found where constant expression expected"
90 | ECall (loc, name, _) ->
91 failwithf "%a: cannot use goal ‘%s’ in constant expression"
94 | ETactic (loc, name, _) ->
95 failwithf "%a: cannot use tactic ‘*%s’ in constant expression"
99 failwithf "%a: cannot use goal in constant expression"
102 and substitute env loc substs =
103 let b = Buffer.create 13 in
106 | SString s -> Buffer.add_string b s
108 let expr = getvar env loc name in
109 match to_constant env expr with
110 | CString s -> Buffer.add_string b s
114 module Substs = struct
116 mutable elems : subst list; (* built in reverse order *)
117 curr : Buffer.t; (* current string *)
120 let create () = { elems = []; curr = Buffer.create 13 }
123 if Buffer.length t.curr > 0 then
124 t.elems <- SString (Buffer.contents t.curr) :: t.elems;
127 let get t = finalize t; List.rev t.elems
129 let add_char { curr } = Buffer.add_char curr
130 let add_string { curr} = Buffer.add_string curr
131 let add_var t id = finalize t; t.elems <- SVar id :: t.elems
135 : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
137 let comma = ref false in
140 if !comma then fprintf fp ", ";
145 let rec print_env fp env =
146 Env.iter (print_def fp) env
148 and print_def fp name expr =
150 | EGoal (loc, (params, patterns, exprs, code)) ->
151 fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
153 iter_with_commas fp print_pattern patterns;
155 iter_with_commas fp print_expr exprs;
165 fprintf fp "let %s = " name;
169 and string_pattern () = function
170 | PTactic (loc, name, params) ->
171 sprintf "*%s (%s)" name (String.concat ", "
172 (List.map (string_substs ()) params));
173 | PVar (loc, id) -> id
175 and print_pattern fp p = output_string fp (string_pattern () p)
177 and string_expr () = function
178 | EGoal (loc, (params, patterns, exprs, code)) ->
179 sprintf "goal (%s) = %s : %s%s"
180 (String.concat ", " params)
181 (String.concat ", " (List.map (string_pattern ()) patterns))
182 (String.concat ", " (List.map (string_expr ()) exprs))
183 (match code with None -> "" | Some code -> " = { ... }")
184 | ECall (loc, name, params) ->
186 name (String.concat ", " (List.map (string_expr ()) params))
187 | ETactic (loc, name, params) ->
189 name (String.concat ", " (List.map (string_expr ()) params))
190 | EVar (loc, var) -> var
192 sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
193 | ESubsts (loc, s) -> string_substs () s
194 | EConstant (loc, c) -> string_constant () c
196 and print_expr fp expr = output_string fp (string_expr () expr)
198 and string_constant () = function
199 | CString s -> sprintf "%S" s
201 and print_constant fp c = output_string fp (string_constant () c)
203 and print_id = output_string
205 and string_substs () ss =
209 | SString s -> sprintf "%S" s
212 (String.concat "+" ss)
214 and print_substs fp ss = output_string fp (string_substs () ss)
216 and print_code fp xs =
219 | SString s -> fprintf fp "%s" s
220 | SVar id -> fprintf fp "%%%s" id