src/ast.ml

   1 (* Goalfile Abstract Syntax Tree
   2  * Copyright (C) 2019 Richard W.M. Jones
   3  * Copyright (C) 2019 Red Hat Inc.
   4  *
   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.
   9  *
  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.
  14  *
  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.
  18  *)
  19
  20 open Lexing
  21 open Printf
  22
  23 open Utils
  24
  25 module Env = Map.Make (String)
  26
  27 type loc = position * position
  28 let noloc = dummy_pos, dummy_pos
  29
  30 let string_loc () loc =
  31   let pos = fst loc in
  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)
  35
  36 type env = expr Env.t
  37 and pattern =
  38   | PTactic of loc * id * substs list
  39 and expr =
  40   | EGoal of loc * goal
  41   | ETactic of loc * tactic
  42   | ECallGoal of loc * id * expr list
  43   | ECallTactic of loc * id * expr list
  44   | EVar of loc * id
  45   | EList of loc * expr list
  46   | ESubsts of loc * substs
  47   | EConstant of loc * constant
  48 and constant =
  49   | CString of string
  50 and goal = param_decl list * pattern list * expr list * code option
  51 and tactic = param_decl list * code
  52 and param_decl = id
  53 and id = string
  54 and code = substs
  55 and substs = subst list
  56 and subst =
  57   | SString of string
  58   | SVar of id
  59
  60 let getvar env loc name =
  61   try Env.find name env
  62   with Not_found ->
  63     failwithf "%a: variable ‘%s’ not found" string_loc loc name
  64
  65 let getgoal env loc name =
  66   let expr =
  67     try Env.find name env
  68     with Not_found ->
  69       failwithf "%a: goal ‘%s’ not found" string_loc loc name in
  70   let goal =
  71     match expr with
  72     | EGoal (loc, goal) -> goal
  73     | _ ->
  74        failwithf "%a: tried to call ‘%s’ which is not a goal"
  75          string_loc loc name in
  76   goal
  77
  78 let gettactic env loc name =
  79   assert (name.[0] = '*');
  80   let expr =
  81     try Env.find name env
  82     with Not_found ->
  83       failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
  84   let tactic =
  85     match expr with
  86     | ETactic (loc, tactic) -> tactic
  87     | _ ->
  88        failwithf "%a: tried to call ‘%s’ which is not a tactic"
  89          string_loc loc name in
  90   tactic
  91
  92 let rec to_constant env = function
  93   | EConstant (loc, c) -> c
  94
  95   | EVar (loc, name) ->
  96      let expr = getvar env loc name in
  97      to_constant env expr
  98
  99   | ESubsts (loc, str) ->
 100      CString (substitute env loc str)
 101
 102   | EList (loc, _) ->
 103      failwithf "%a: list found where constant expression expected"
 104        string_loc loc
 105
 106   | ECallGoal (loc, name, _) ->
 107      failwithf "%a: cannot use goal ‘%s’ in constant expression"
 108        string_loc loc name
 109
 110   | ECallTactic (loc, name, _) ->
 111      failwithf "%a: cannot use tactic ‘%s’ in constant expression"
 112        string_loc loc name
 113
 114   | EGoal (loc, _) ->
 115      failwithf "%a: cannot use goal in constant expression"
 116        string_loc loc
 117
 118   | ETactic (loc, _) ->
 119      failwithf "%a: cannot use tactic in constant expression"
 120        string_loc loc
 121
 122 and substitute env loc substs =
 123   let b = Buffer.create 13 in
 124   List.iter (
 125     function
 126     | SString s -> Buffer.add_string b s
 127     | SVar name ->
 128        let expr = getvar env loc name in
 129        match to_constant env expr with
 130        | CString s -> Buffer.add_string b s
 131   ) substs;
 132   Buffer.contents b
 133
 134 let rec to_shell_script env loc substs =
 135   let b = Buffer.create 13 in
 136   List.iter (
 137     function
 138     | SString s -> Buffer.add_string b s
 139     | SVar name ->
 140        let expr = getvar env loc name in
 141        let s = expr_to_shell_string env expr in
 142        Buffer.add_string b s
 143   ) substs;
 144   Buffer.contents b
 145
 146 and expr_to_shell_string env = function
 147   | EConstant (loc, CString s) -> Filename.quote s
 148
 149   | EVar (loc, name) ->
 150      let expr = getvar env loc name in
 151      expr_to_shell_string env expr
 152
 153   | ESubsts (loc, str) ->
 154      Filename.quote (substitute env loc str)
 155
 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
 160
 161   | ECallGoal (loc, name, _) ->
 162      failwithf "%a: cannot use goal ‘%s’ in shell expansion"
 163        string_loc loc name
 164
 165   (* Tactics expand to the first parameter. *)
 166   | ECallTactic (loc, _, []) -> Filename.quote ""
 167   | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 168
 169   | EGoal (loc, _) ->
 170      failwithf "%a: cannot use goal in shell expansion"
 171        string_loc loc
 172
 173   | ETactic (loc, _) ->
 174      failwithf "%a: cannot use tactic in shell expansion"
 175        string_loc loc
 176
 177 module Substs = struct
 178   type t = {
 179       mutable elems : subst list; (* built in reverse order *)
 180       curr : Buffer.t;            (* current string *)
 181     }
 182
 183   let create () = { elems = []; curr = Buffer.create 13 }
 184
 185   let finalize t =
 186     if Buffer.length t.curr > 0 then
 187       t.elems <- SString (Buffer.contents t.curr) :: t.elems;
 188     Buffer.clear t.curr
 189
 190   let get t = finalize t; List.rev t.elems
 191
 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
 195 end
 196
 197 let iter_with_commas
 198     : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
 199   fun fp f xs ->
 200   let comma = ref false in
 201   List.iter (
 202     fun x ->
 203       if !comma then fprintf fp ", ";
 204       comma := true;
 205       f fp x
 206   ) xs
 207
 208 let rec string_env () env =
 209   let env = Env.bindings env in
 210   String.concat "" (List.map (string_def ()) env)
 211
 212 and print_env fp env = output_string fp (string_env () env)
 213
 214 and string_def () (name, expr) =
 215   match expr with
 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;
 219
 220 and print_def fp name expr = output_string fp (string_def () (name, expr))
 221
 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 -> " = { ... }")
 229
 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))
 234
 235 and string_param_decl () name = name
 236
 237 and string_pattern () = function
 238   | PTactic (loc, name, params) ->
 239      sprintf "%s (%s)" name (String.concat ", "
 240                                 (List.map (string_substs ()) params))
 241
 242 and print_pattern fp p = output_string fp (string_pattern () p)
 243
 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) ->
 248      sprintf "%s (%s)"
 249        name (String.concat ", " (List.map (string_expr ()) params))
 250   | ECallTactic (loc, name, params) ->
 251      sprintf "%s (%s)"
 252        name (String.concat ", " (List.map (string_expr ()) params))
 253   | EVar (loc, var) -> var
 254   | EList (loc, xs) ->
 255      sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
 256   | ESubsts (loc, s) -> string_substs () s
 257   | EConstant (loc, c) -> string_constant () c
 258
 259 and print_expr fp expr = output_string fp (string_expr () expr)
 260
 261 and string_constant () = function
 262   | CString s -> sprintf "%S" s
 263
 264 and print_constant fp c = output_string fp (string_constant () c)
 265
 266 and print_id = output_string
 267
 268 and string_substs () ss =
 269   let ss =
 270     List.map (
 271       function
 272       | SString s -> sprintf "%S" s
 273       | SVar id -> id
 274     ) ss in
 275   (String.concat "+" ss)
 276
 277 and print_substs fp ss = output_string fp (string_substs () ss)
 278
 279 and print_code fp xs =
 280   List.iter (
 281     function
 282     | SString s -> fprintf fp "%s" s
 283     | SVar id -> fprintf fp "%%%s" id
 284   ) xs