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
41 | ETactic of loc * tactic
42 | ECallGoal of loc * id * expr list
43 | ECallTactic of loc * id * expr list
45 | EList of loc * expr list
46 | ESubsts of loc * substs
47 | EConstant of loc * constant
50 and goal = param_decl list * pattern list * expr list * code option
51 and tactic = param_decl list * code
55 and substs = subst list
60 let getvar env loc name =
63 failwithf "%a: variable ‘%s’ not found" string_loc loc name
65 let getgoal env loc name =
69 failwithf "%a: goal ‘%s’ not found" string_loc loc name in
72 | EGoal (loc, goal) -> goal
74 failwithf "%a: tried to call ‘%s’ which is not a goal"
75 string_loc loc name in
78 let gettactic env loc name =
79 assert (name.[0] = '*');
83 failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
86 | ETactic (loc, tactic) -> tactic
88 failwithf "%a: tried to call ‘%s’ which is not a tactic"
89 string_loc loc name in
92 let rec to_constant env = function
93 | EConstant (loc, c) -> c
96 let expr = getvar env loc name in
99 | ESubsts (loc, str) ->
100 CString (substitute env loc str)
103 failwithf "%a: list found where constant expression expected"
106 | ECallGoal (loc, name, _) ->
107 failwithf "%a: cannot use goal ‘%s’ in constant expression"
110 | ECallTactic (loc, name, _) ->
111 failwithf "%a: cannot use tactic ‘%s’ in constant expression"
115 failwithf "%a: cannot use goal in constant expression"
118 | ETactic (loc, _) ->
119 failwithf "%a: cannot use tactic in constant expression"
122 and substitute env loc substs =
123 let b = Buffer.create 13 in
126 | SString s -> Buffer.add_string b s
128 let expr = getvar env loc name in
129 match to_constant env expr with
130 | CString s -> Buffer.add_string b s
134 let rec to_shell_script env loc substs =
135 let b = Buffer.create 13 in
138 | SString s -> Buffer.add_string b s
140 let expr = getvar env loc name in
141 let s = expr_to_shell_string env expr in
142 Buffer.add_string b s
146 and expr_to_shell_string env = function
147 | EConstant (loc, CString s) -> Filename.quote s
149 | EVar (loc, name) ->
150 let expr = getvar env loc name in
151 expr_to_shell_string env expr
153 | ESubsts (loc, str) ->
154 Filename.quote (substitute env loc str)
156 | EList (loc, exprs) ->
157 let strs = List.map (expr_to_shell_string env) exprs in
158 (* These are shell quoted so we can just concat them with space. *)
159 String.concat " " strs
161 | ECallGoal (loc, name, _) ->
162 failwithf "%a: cannot use goal ‘%s’ in shell expansion"
165 (* Tactics expand to the first parameter. *)
166 | ECallTactic (loc, _, []) -> Filename.quote ""
167 | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
170 failwithf "%a: cannot use goal in shell expansion"
173 | ETactic (loc, _) ->
174 failwithf "%a: cannot use tactic in shell expansion"
177 module Substs = struct
179 mutable elems : subst list; (* built in reverse order *)
180 curr : Buffer.t; (* current string *)
183 let create () = { elems = []; curr = Buffer.create 13 }
186 if Buffer.length t.curr > 0 then
187 t.elems <- SString (Buffer.contents t.curr) :: t.elems;
190 let get t = finalize t; List.rev t.elems
192 let add_char { curr } = Buffer.add_char curr
193 let add_string { curr} = Buffer.add_string curr
194 let add_var t id = finalize t; t.elems <- SVar id :: t.elems
198 : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
200 let comma = ref false in
203 if !comma then fprintf fp ", ";
208 let rec string_env () env =
209 let env = Env.bindings env in
210 String.concat "" (List.map (string_def ()) env)
212 and print_env fp env = output_string fp (string_env () env)
214 and string_def () (name, expr) =
216 | EGoal (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
217 | ETactic (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
218 | expr -> sprintf "let %s = %a\n" name string_expr expr;
220 and print_def fp name expr = output_string fp (string_def () (name, expr))
222 and string_goal () (name, (param_decls, patterns, exprs, code)) =
223 sprintf "goal%s (%s) = %s : %s%s"
224 (match name with None -> "" | Some name -> " " ^ name)
225 (String.concat ", " (List.map (string_param_decl ()) param_decls))
226 (String.concat ", " (List.map (string_pattern ()) patterns))
227 (String.concat ", " (List.map (string_expr ()) exprs))
228 (match code with None -> "" | Some code -> " = { ... }")
230 and string_tactic () (name, (param_decls, code)) =
231 sprintf "tactic%s (%s) = { ... }"
232 (match name with None -> "" | Some name -> " " ^ name)
233 (String.concat ", " (List.map (string_param_decl ()) param_decls))
235 and string_param_decl () name = name
237 and string_pattern () = function
238 | PTactic (loc, name, params) ->
239 sprintf "%s (%s)" name (String.concat ", "
240 (List.map (string_substs ()) params))
242 and print_pattern fp p = output_string fp (string_pattern () p)
244 and string_expr () = function
245 | EGoal (loc, goal) -> string_goal () (None, goal)
246 | ETactic (loc, goal) -> string_tactic () (None, goal)
247 | ECallGoal (loc, name, params) ->
249 name (String.concat ", " (List.map (string_expr ()) params))
250 | ECallTactic (loc, name, params) ->
252 name (String.concat ", " (List.map (string_expr ()) params))
253 | EVar (loc, var) -> var
255 sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
256 | ESubsts (loc, s) -> string_substs () s
257 | EConstant (loc, c) -> string_constant () c
259 and print_expr fp expr = output_string fp (string_expr () expr)
261 and string_constant () = function
262 | CString s -> sprintf "%S" s
264 and print_constant fp c = output_string fp (string_constant () c)
266 and print_id = output_string
268 and string_substs () ss =
272 | SString s -> sprintf "%S" s
275 (String.concat "+" ss)
277 and print_substs fp ss = output_string fp (string_substs () ss)
279 and print_code fp xs =
282 | SString s -> fprintf fp "%s" s
283 | SVar id -> fprintf fp "%%%s" id