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 = struct
  26   include Map.Make (String)
  27
  28   let merge env env' =
  29     List.fold_left (fun env (k, v) -> add k v env) env (bindings env')
  30 end
  31
  32 type loc = position * position
  33 let noloc = dummy_pos, dummy_pos
  34
  35 let string_loc () loc =
  36   let pos = fst loc in
  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)
  40
  41 type env = expr Env.t
  42 and pattern =
  43   | PTactic of loc * id * substs list
  44 and expr =
  45   | EGoalDefn of loc * goal
  46   | ETacticDefn of loc * tactic
  47   | ECallGoal of loc * id * expr list
  48   | ETacticConstructor of loc * id * expr list
  49   | EVar of loc * id
  50   | EList of loc * expr list
  51   | ESubsts of loc * substs
  52   | EConstant of loc * constant
  53 and constant =
  54   | CString of string
  55 and goal = param_decl list * pattern list * expr list * code option
  56 and tactic = param_decl list * code
  57 and param_decl = id
  58 and id = string
  59 and code = substs
  60 and substs = subst list
  61 and subst =
  62   | SString of string
  63   | SVar of id
  64
  65 let getvar env loc name =
  66   try Env.find name env
  67   with Not_found ->
  68     failwithf "%a: variable ‘%s’ not found" string_loc loc name
  69
  70 let getgoal env loc name =
  71   let expr =
  72     try Env.find name env
  73     with Not_found ->
  74       failwithf "%a: goal ‘%s’ not found" string_loc loc name in
  75   let goal =
  76     match expr with
  77     | EGoalDefn (loc, goal) -> goal
  78     | _ ->
  79        failwithf "%a: tried to call ‘%s’ which is not a goal"
  80          string_loc loc name in
  81   goal
  82
  83 let gettactic env loc name =
  84   assert (name.[0] = '*');
  85   let expr =
  86     try Env.find name env
  87     with Not_found ->
  88       failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
  89   let tactic =
  90     match expr with
  91     | ETacticDefn (loc, tactic) -> tactic
  92     | _ ->
  93        failwithf "%a: tried to call ‘%s’ which is not a tactic"
  94          string_loc loc name in
  95   tactic
  96
  97 let rec to_constant env = function
  98   | EConstant (loc, c) -> c
  99
 100   | EVar (loc, name) ->
 101      let expr = getvar env loc name in
 102      to_constant env expr
 103
 104   | ESubsts (loc, str) ->
 105      CString (substitute env loc str)
 106
 107   | EList (loc, _) ->
 108      failwithf "%a: list found where constant expression expected"
 109        string_loc loc
 110
 111   | ECallGoal (loc, name, _) ->
 112      failwithf "%a: cannot use goal ‘%s’ in constant expression"
 113        string_loc loc name
 114
 115   | ETacticConstructor (loc, name, _) ->
 116      failwithf "%a: cannot use tactic ‘%s’ in constant expression"
 117        string_loc loc name
 118
 119   | EGoalDefn (loc, _) ->
 120      failwithf "%a: cannot use goal in constant expression"
 121        string_loc loc
 122
 123   | ETacticDefn (loc, _) ->
 124      failwithf "%a: cannot use tactic in constant expression"
 125        string_loc loc
 126
 127 and substitute env loc substs =
 128   let b = Buffer.create 13 in
 129   List.iter (
 130     function
 131     | SString s -> Buffer.add_string b s
 132     | SVar name ->
 133        let expr = getvar env loc name in
 134        match to_constant env expr with
 135        | CString s -> Buffer.add_string b s
 136   ) substs;
 137   Buffer.contents b
 138
 139 let rec to_shell_script env loc substs =
 140   let b = Buffer.create 13 in
 141   List.iter (
 142     function
 143     | SString s -> Buffer.add_string b s
 144     | SVar name ->
 145        let expr = getvar env loc name in
 146        let s = expr_to_shell_string env expr in
 147        Buffer.add_string b s
 148   ) substs;
 149   Buffer.contents b
 150
 151 and expr_to_shell_string env = function
 152   | EConstant (loc, CString s) -> Filename.quote s
 153
 154   | EVar (loc, name) ->
 155      let expr = getvar env loc name in
 156      expr_to_shell_string env expr
 157
 158   | ESubsts (loc, str) ->
 159      Filename.quote (substitute env loc str)
 160
 161   | EList (loc, exprs) ->
 162      let strs = List.map (expr_to_shell_string env) exprs in
 163      (* These are shell quoted so we can just concat them with space. *)
 164      String.concat " " strs
 165
 166   | ECallGoal (loc, name, _) ->
 167      failwithf "%a: cannot use goal ‘%s’ in shell expansion"
 168        string_loc loc name
 169
 170   (* Tactics expand to the first parameter. *)
 171   | ETacticConstructor (loc, _, []) -> Filename.quote ""
 172   | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 173
 174   | EGoalDefn (loc, _) ->
 175      failwithf "%a: cannot use goal in shell expansion"
 176        string_loc loc
 177
 178   | ETacticDefn (loc, _) ->
 179      failwithf "%a: cannot use tactic in shell expansion"
 180        string_loc loc
 181
 182 module Substs = struct
 183   type t = {
 184       mutable elems : subst list; (* built in reverse order *)
 185       curr : Buffer.t;            (* current string *)
 186     }
 187
 188   let create () = { elems = []; curr = Buffer.create 13 }
 189
 190   let finalize t =
 191     if Buffer.length t.curr > 0 then
 192       t.elems <- SString (Buffer.contents t.curr) :: t.elems;
 193     Buffer.clear t.curr
 194
 195   let get t = finalize t; List.rev t.elems
 196
 197   let add_char { curr } = Buffer.add_char curr
 198   let add_string { curr} = Buffer.add_string curr
 199   let add_var t id = finalize t; t.elems <- SVar id :: t.elems
 200 end
 201
 202 let iter_with_commas
 203     : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
 204   fun fp f xs ->
 205   let comma = ref false in
 206   List.iter (
 207     fun x ->
 208       if !comma then fprintf fp ", ";
 209       comma := true;
 210       f fp x
 211   ) xs
 212
 213 let rec string_env () env =
 214   let env = Env.bindings env in
 215   String.concat "" (List.map (string_def ()) env)
 216
 217 and print_env fp env = output_string fp (string_env () env)
 218
 219 and string_def () (name, expr) =
 220   match expr with
 221   | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
 222   | ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
 223   | expr -> sprintf "let %s = %a\n" name string_expr expr;
 224
 225 and print_def fp name expr = output_string fp (string_def () (name, expr))
 226
 227 and string_goal () (name, (param_decls, patterns, exprs, code)) =
 228   sprintf "goal%s (%s) = %s : %s%s"
 229     (match name with None -> "" | Some name -> " " ^ name)
 230     (String.concat ", " (List.map (string_param_decl ()) param_decls))
 231     (String.concat ", " (List.map (string_pattern ()) patterns))
 232     (String.concat ", " (List.map (string_expr ()) exprs))
 233     (match code with None -> "" | Some code -> " = { ... }")
 234
 235 and string_tactic () (name, (param_decls, code)) =
 236   sprintf "tactic%s (%s) = { ... }"
 237     (match name with None -> "" | Some name -> " " ^ name)
 238     (String.concat ", " (List.map (string_param_decl ()) param_decls))
 239
 240 and string_param_decl () name = name
 241
 242 and string_pattern () = function
 243   | PTactic (loc, name, params) ->
 244      sprintf "%s (%s)" name (String.concat ", "
 245                                 (List.map (string_substs ()) params))
 246
 247 and print_pattern fp p = output_string fp (string_pattern () p)
 248
 249 and string_expr () = function
 250   | EGoalDefn (loc, goal) -> string_goal () (None, goal)
 251   | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
 252   | ECallGoal (loc, name, params) ->
 253      sprintf "%s (%s)"
 254        name (String.concat ", " (List.map (string_expr ()) params))
 255   | ETacticConstructor (loc, name, params) ->
 256      sprintf "%s (%s)"
 257        name (String.concat ", " (List.map (string_expr ()) params))
 258   | EVar (loc, var) -> var
 259   | EList (loc, xs) ->
 260      sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
 261   | ESubsts (loc, s) -> string_substs () s
 262   | EConstant (loc, c) -> string_constant () c
 263
 264 and print_expr fp expr = output_string fp (string_expr () expr)
 265
 266 and string_constant () = function
 267   | CString s -> sprintf "%S" s
 268
 269 and print_constant fp c = output_string fp (string_constant () c)
 270
 271 and print_id = output_string
 272
 273 and string_substs () ss =
 274   let ss =
 275     List.map (
 276       function
 277       | SString s -> sprintf "%S" s
 278       | SVar id -> id
 279     ) ss in
 280   (String.concat "+" ss)
 281
 282 and print_substs fp ss = output_string fp (string_substs () ss)
 283
 284 and print_code fp xs =
 285   List.iter (
 286     function
 287     | SString s -> fprintf fp "%s" s
 288     | SVar id -> fprintf fp "%%%s" id
 289   ) xs