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.
26 include Map.Make (String)
29 List.fold_left (fun env (k, v) -> add k v env) env (bindings env')
32 type loc = position * position
33 let noloc = dummy_pos, dummy_pos
35 let string_loc () loc =
37 sprintf "%s:%d:%d" pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol)
38 let print_loc fp loc =
39 fprintf fp "%s" (string_loc () loc)
43 | PTactic of loc * id * substs list
45 | EGoalDefn of loc * goal
46 | EFuncDefn of loc * func
47 | ETacticDefn of loc * tactic
48 | ECall of loc * id * expr list
49 | ETacticCtor of loc * id * expr list
51 | EList of loc * expr list
52 | ESubsts of loc * substs
53 | EConstant of loc * constant
56 and goal = param_decl list * pattern list * expr list * code option
57 and func = param_decl list * returning * bool * code
58 and tactic = param_decl list * code
61 and code = substs * bool
62 and returning = RetExpr | RetStrings | RetString
63 and substs = subst list
68 let getvar env loc name =
71 failwithf "%a: variable ‘%s’ not found" string_loc loc name
73 let getgoal env loc name =
77 failwithf "%a: goal ‘%s’ not found" string_loc loc name in
80 | EGoalDefn (loc, goal) -> goal
82 failwithf "%a: tried to call ‘%s’ which is not a goal"
83 string_loc loc name in
86 let getfunc env loc name =
90 failwithf "%a: func ‘%s’ not found" string_loc loc name in
93 | EFuncDefn (loc, func) -> func
95 failwithf "%a: tried to call ‘%s’ which is not a function"
96 string_loc loc name in
99 let gettactic env loc name =
100 assert (name.[0] = '*');
102 try Env.find name env
104 failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
107 | ETacticDefn (loc, tactic) -> tactic
109 failwithf "%a: tried to call ‘%s’ which is not a tactic"
110 string_loc loc name in
113 module Substs = struct
115 mutable elems : subst list; (* built in reverse order *)
116 curr : Buffer.t; (* current string *)
119 let create () = { elems = []; curr = Buffer.create 13 }
122 if Buffer.length t.curr > 0 then
123 t.elems <- SString (Buffer.contents t.curr) :: t.elems;
126 let get t = finalize t; List.rev t.elems
128 let add_char { curr } = Buffer.add_char curr
129 let add_string { curr} = Buffer.add_string curr
130 let add_var t id = finalize t; t.elems <- SVar id :: t.elems
134 : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
136 let comma = ref false in
139 if !comma then fprintf fp ", ";
144 let rec string_env () env =
145 let env = Env.bindings env in
146 String.concat "" (List.map (string_def ()) env)
148 and print_env fp env = output_string fp (string_env () env)
150 and string_def () (name, expr) =
152 | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
153 | EFuncDefn (loc, func) -> string_func () (Some name, func) ^ "\n"
154 | ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
155 | expr -> sprintf "let %s = %a\n" name string_expr expr;
157 and print_def fp name expr = output_string fp (string_def () (name, expr))
159 and string_goal () (name, (param_decls, patterns, exprs, code)) =
160 sprintf "goal%s (%s) = %s : %s%s"
161 (match name with None -> "" | Some name -> " " ^ name)
162 (String.concat ", " (List.map (string_param_decl ()) param_decls))
163 (String.concat ", " (List.map (string_pattern ()) patterns))
164 (String.concat ", " (List.map (string_expr ()) exprs))
165 (match code with None -> ""
166 | Some (code, false) -> " = { ... }"
167 | Some (code, true) -> " = @{ ... }")
169 and string_func () (name, (param_decls, returning, pure, (code, quiet))) =
170 sprintf "%sfunction%s returning %s (%s) = %s{ ... }"
171 (if pure then "pure " else "")
172 (match name with None -> "" | Some name -> " " ^ name)
173 (match returning with RetExpr -> "expression"
174 | RetString -> "string"
175 | RetStrings -> "strings")
176 (String.concat ", " (List.map (string_param_decl ()) param_decls))
177 (if quiet then "@" else "")
179 and string_tactic () (name, (param_decls, (code, quiet))) =
180 sprintf "tactic%s (%s) = %s{ ... }"
181 (match name with None -> "" | Some name -> " " ^ name)
182 (String.concat ", " (List.map (string_param_decl ()) param_decls))
183 (if quiet then "@" else "")
185 and string_param_decl () name = name
187 and string_pattern () = function
188 | PTactic (loc, name, params) ->
189 sprintf "%s (%s)" name (String.concat ", "
190 (List.map (string_substs ()) params))
192 and print_pattern fp p = output_string fp (string_pattern () p)
194 and string_expr () = function
195 | EGoalDefn (loc, goal) -> string_goal () (None, goal)
196 | EFuncDefn (loc, func) -> string_func () (None, func)
197 | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
198 | ECall (loc, name, params) ->
200 name (String.concat ", " (List.map (string_expr ()) params))
201 | ETacticCtor (loc, name, params) ->
203 name (String.concat ", " (List.map (string_expr ()) params))
204 | EVar (loc, var) -> var
206 sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
207 | ESubsts (loc, s) -> string_substs () s
208 | EConstant (loc, c) -> string_constant () c
210 and print_expr fp expr = output_string fp (string_expr () expr)
212 and string_constant () = function
213 | CString s -> sprintf "%S" s
215 and print_constant fp c = output_string fp (string_constant () c)
217 and print_id = output_string
219 and string_substs () ss =
223 | SString s -> sprintf "%S" s
226 (String.concat "+" ss)
228 and print_substs fp ss = output_string fp (string_substs () ss)
230 and print_code fp xs =
233 | SString s -> fprintf fp "%s" s
234 | SVar id -> fprintf fp "%%%s" id