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   | EFuncDefn of loc * func
  47   | ETacticDefn of loc * tactic
  48   | ECall of loc * id * expr list
  49   | ETacticCtor of loc * id * expr list
  50   | EVar of loc * id
  51   | EList of loc * expr list
  52   | ESubsts of loc * substs
  53   | EConstant of loc * constant
  54 and constant =
  55   | CString of string
  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
  59 and param_decl = id
  60 and id = string
  61 and code = substs * bool
  62 and returning = RetExpr | RetStrings | RetString
  63 and substs = subst list
  64 and subst =
  65   | SString of string
  66   | SVar of id
  67
  68 let getvar env loc name =
  69   try Env.find name env
  70   with Not_found ->
  71     failwithf "%a: variable ‘%s’ not found" string_loc loc name
  72
  73 let getgoal env loc name =
  74   let expr =
  75     try Env.find name env
  76     with Not_found ->
  77       failwithf "%a: goal ‘%s’ not found" string_loc loc name in
  78   let goal =
  79     match expr with
  80     | EGoalDefn (loc, goal) -> goal
  81     | _ ->
  82        failwithf "%a: tried to call ‘%s’ which is not a goal"
  83          string_loc loc name in
  84   goal
  85
  86 let getfunc env loc name =
  87   let expr =
  88     try Env.find name env
  89     with Not_found ->
  90       failwithf "%a: func ‘%s’ not found" string_loc loc name in
  91   let func =
  92     match expr with
  93     | EFuncDefn (loc, func) -> func
  94     | _ ->
  95        failwithf "%a: tried to call ‘%s’ which is not a function"
  96          string_loc loc name in
  97   func
  98
  99 let gettactic env loc name =
 100   assert (name.[0] = '*');
 101   let expr =
 102     try Env.find name env
 103     with Not_found ->
 104       failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
 105   let tactic =
 106     match expr with
 107     | ETacticDefn (loc, tactic) -> tactic
 108     | _ ->
 109        failwithf "%a: tried to call ‘%s’ which is not a tactic"
 110          string_loc loc name in
 111   tactic
 112
 113 module Substs = struct
 114   type t = {
 115       mutable elems : subst list; (* built in reverse order *)
 116       curr : Buffer.t;            (* current string *)
 117     }
 118
 119   let create () = { elems = []; curr = Buffer.create 13 }
 120
 121   let finalize t =
 122     if Buffer.length t.curr > 0 then
 123       t.elems <- SString (Buffer.contents t.curr) :: t.elems;
 124     Buffer.clear t.curr
 125
 126   let get t = finalize t; List.rev t.elems
 127
 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
 131 end
 132
 133 let iter_with_commas
 134     : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
 135   fun fp f xs ->
 136   let comma = ref false in
 137   List.iter (
 138     fun x ->
 139       if !comma then fprintf fp ", ";
 140       comma := true;
 141       f fp x
 142   ) xs
 143
 144 let rec string_env () env =
 145   let env = Env.bindings env in
 146   String.concat "" (List.map (string_def ()) env)
 147
 148 and print_env fp env = output_string fp (string_env () env)
 149
 150 and string_def () (name, expr) =
 151   match expr with
 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;
 156
 157 and print_def fp name expr = output_string fp (string_def () (name, expr))
 158
 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) -> " = @{ ... }")
 168
 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 "")
 178
 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 "")
 184
 185 and string_param_decl () name = name
 186
 187 and string_pattern () = function
 188   | PTactic (loc, name, params) ->
 189      sprintf "%s (%s)" name (String.concat ", "
 190                                 (List.map (string_substs ()) params))
 191
 192 and print_pattern fp p = output_string fp (string_pattern () p)
 193
 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) ->
 199      sprintf "%s (%s)"
 200        name (String.concat ", " (List.map (string_expr ()) params))
 201   | ETacticCtor (loc, name, params) ->
 202      sprintf "%s (%s)"
 203        name (String.concat ", " (List.map (string_expr ()) params))
 204   | EVar (loc, var) -> var
 205   | EList (loc, xs) ->
 206      sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
 207   | ESubsts (loc, s) -> string_substs () s
 208   | EConstant (loc, c) -> string_constant () c
 209
 210 and print_expr fp expr = output_string fp (string_expr () expr)
 211
 212 and string_constant () = function
 213   | CString s -> sprintf "%S" s
 214
 215 and print_constant fp c = output_string fp (string_constant () c)
 216
 217 and print_id = output_string
 218
 219 and string_substs () ss =
 220   let ss =
 221     List.map (
 222       function
 223       | SString s -> sprintf "%S" s
 224       | SVar id -> id
 225     ) ss in
 226   (String.concat "+" ss)
 227
 228 and print_substs fp ss = output_string fp (string_substs () ss)
 229
 230 and print_code fp xs =
 231   List.iter (
 232     function
 233     | SString s -> fprintf fp "%s" s
 234     | SVar id -> fprintf fp "%%%s" id
 235   ) xs