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   | PVar of loc * id
  40 and expr =
  41   | EGoal of loc * goal
  42   | ECall of loc * id * expr list
  43   | ETactic 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 = id list * pattern list * expr list * code option
  51 and id = string
  52 and code = substs
  53 and substs = subst list
  54 and subst =
  55   | SString of string
  56   | SVar of id
  57
  58 let getvar env loc name =
  59   try Env.find name env
  60   with Not_found ->
  61     failwithf "%a: variable ‘%s’ not found" string_loc loc name
  62
  63 let getgoal env loc name =
  64   let expr =
  65     try Env.find name env
  66     with Not_found ->
  67       failwithf "%a: goal ‘%s’ not found" string_loc loc name in
  68   let goal =
  69     match expr with
  70     | EGoal (loc, goal) -> goal
  71     | _ ->
  72        failwithf "%a: tried to call ‘%s’ which is not a goal"
  73          string_loc loc name in
  74   goal
  75
  76 let rec to_constant env = function
  77   | EConstant (loc, c) -> c
  78
  79   | EVar (loc, name) ->
  80      let expr = getvar env loc name in
  81      to_constant env expr
  82
  83   | ESubsts (loc, str) ->
  84      CString (substitute env loc str)
  85
  86   | EList (loc, _) ->
  87      failwithf "%a: list found where constant expression expected"
  88        string_loc loc
  89
  90   | ECall (loc, name, _) ->
  91      failwithf "%a: cannot use goal ‘%s’ in constant expression"
  92        string_loc loc name
  93
  94   | ETactic (loc, name, _) ->
  95      failwithf "%a: cannot use tactic ‘*%s’ in constant expression"
  96        string_loc loc name
  97
  98   | EGoal (loc, _) ->
  99      failwithf "%a: cannot use goal in constant expression"
 100        string_loc loc
 101
 102 and substitute env loc substs =
 103   let b = Buffer.create 13 in
 104   List.iter (
 105     function
 106     | SString s -> Buffer.add_string b s
 107     | SVar name ->
 108        let expr = getvar env loc name in
 109        match to_constant env expr with
 110        | CString s -> Buffer.add_string b s
 111   ) substs;
 112   Buffer.contents b
 113
 114 module Substs = struct
 115   type t = {
 116       mutable elems : subst list; (* built in reverse order *)
 117       curr : Buffer.t;            (* current string *)
 118     }
 119
 120   let create () = { elems = []; curr = Buffer.create 13 }
 121
 122   let finalize t =
 123     if Buffer.length t.curr > 0 then
 124       t.elems <- SString (Buffer.contents t.curr) :: t.elems;
 125     Buffer.clear t.curr
 126
 127   let get t = finalize t; List.rev t.elems
 128
 129   let add_char { curr } = Buffer.add_char curr
 130   let add_string { curr} = Buffer.add_string curr
 131   let add_var t id = finalize t; t.elems <- SVar id :: t.elems
 132 end
 133
 134 let iter_with_commas
 135     : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
 136   fun fp f xs ->
 137   let comma = ref false in
 138   List.iter (
 139     fun x ->
 140       if !comma then fprintf fp ", ";
 141       comma := true;
 142       f fp x
 143   ) xs
 144
 145 let rec print_env fp env =
 146   Env.iter (print_def fp) env
 147
 148 and print_def fp name expr =
 149   match expr with
 150   | EGoal (loc, (params, patterns, exprs, code)) ->
 151      fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
 152      fprintf fp "    ";
 153      iter_with_commas fp print_pattern patterns;
 154      fprintf fp " : ";
 155      iter_with_commas fp print_expr exprs;
 156      (match code with
 157       | None -> ()
 158       | Some code ->
 159          fprintf fp " {\n";
 160          print_code fp code;
 161          fprintf fp "\n    }"
 162      );
 163      fprintf fp "\n"
 164   | expr ->
 165      fprintf fp "let %s = " name;
 166      print_expr fp expr;
 167      fprintf fp "\n"
 168
 169 and string_pattern () = function
 170   | PTactic (loc, name, params) ->
 171      sprintf "*%s (%s)" name (String.concat ", "
 172                                 (List.map (string_substs ()) params));
 173   | PVar (loc, id) -> id
 174
 175 and print_pattern fp p = output_string fp (string_pattern () p)
 176
 177 and string_expr () = function
 178   | EGoal (loc, (params, patterns, exprs, code)) ->
 179      sprintf "goal (%s) = %s : %s%s"
 180        (String.concat ", " params)
 181        (String.concat ", " (List.map (string_pattern ()) patterns))
 182        (String.concat ", " (List.map (string_expr ()) exprs))
 183        (match code with None -> "" | Some code -> " = { ... }")
 184   | ECall (loc, name, params) ->
 185      sprintf "%s (%s)"
 186        name (String.concat ", " (List.map (string_expr ()) params))
 187   | ETactic (loc, name, params) ->
 188      sprintf "*%s (%s)"
 189        name (String.concat ", " (List.map (string_expr ()) params))
 190   | EVar (loc, var) -> var
 191   | EList (loc, xs) ->
 192      sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
 193   | ESubsts (loc, s) -> string_substs () s
 194   | EConstant (loc, c) -> string_constant () c
 195
 196 and print_expr fp expr = output_string fp (string_expr () expr)
 197
 198 and string_constant () = function
 199   | CString s -> sprintf "%S" s
 200
 201 and print_constant fp c = output_string fp (string_constant () c)
 202
 203 and print_id = output_string
 204
 205 and string_substs () ss =
 206   let ss =
 207     List.map (
 208       function
 209       | SString s -> sprintf "%S" s
 210       | SVar id -> id
 211     ) ss in
 212   (String.concat "+" ss)
 213
 214 and print_substs fp ss = output_string fp (string_substs () ss)
 215
 216 and print_code fp xs =
 217   List.iter (
 218     function
 219     | SString s -> fprintf fp "%s" s
 220     | SVar id -> fprintf fp "%%%s" id
 221   ) xs