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 Printf
  21
  22 module StringMap = Map.Make (String)
  23
  24 type env = expr StringMap.t
  25 and pattern =
  26   | PTactic of id * substs list
  27   | PVarSubst of id
  28 and expr =
  29   | EGoal of goal
  30   | ECall of id * expr list
  31   | EVar of id
  32   | EList of expr list
  33   | ESubsts of substs
  34   | EString of string
  35 and goal = id list * pattern list * expr list * code option
  36 and id = string
  37 and code = substs
  38 and substs = subst list
  39 and subst =
  40   | SString of string
  41   | SVar of id
  42
  43 module Substs = struct
  44   type t = {
  45       mutable elems : subst list; (* built in reverse order *)
  46       curr : Buffer.t;            (* current string *)
  47     }
  48
  49   let create () = { elems = []; curr = Buffer.create 13 }
  50
  51   let finalize t =
  52     if Buffer.length t.curr > 0 then
  53       t.elems <- SString (Buffer.contents t.curr) :: t.elems;
  54     Buffer.clear t.curr
  55
  56   let get t = finalize t; List.rev t.elems
  57
  58   let add_char { curr } = Buffer.add_char curr
  59   let add_string { curr} = Buffer.add_string curr
  60   let add_var t id = finalize t; t.elems <- SVar id :: t.elems
  61 end
  62
  63 let iter_with_commas
  64     : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
  65   fun fp f xs ->
  66   let comma = ref false in
  67   List.iter (
  68     fun x ->
  69       if !comma then fprintf fp ", ";
  70       comma := true;
  71       f fp x
  72   ) xs
  73
  74 let rec print_env fp env =
  75   StringMap.iter (print_def fp) env
  76
  77 and print_def fp name expr =
  78   match expr with
  79   | EGoal (params, patterns, exprs, code) ->
  80      fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
  81      fprintf fp "    ";
  82      iter_with_commas fp print_pattern patterns;
  83      fprintf fp " : ";
  84      iter_with_commas fp print_expr exprs;
  85      (match code with
  86       | None -> ()
  87       | Some code ->
  88          fprintf fp " {\n";
  89          print_code fp code;
  90          fprintf fp "\n    }"
  91      );
  92      fprintf fp "\n"
  93   | expr ->
  94      fprintf fp "let %s = " name;
  95      print_expr fp expr;
  96      fprintf fp "\n"
  97
  98 and print_pattern fp = function
  99   | PTactic (name, params) ->
 100      fprintf fp "%s (" name;
 101      iter_with_commas fp print_substs params;
 102      fprintf fp ")"
 103   | PVarSubst id -> print_id fp id
 104
 105 and print_expr fp = function
 106   | EGoal _ -> assert false (* printed above *)
 107   | ECall (name, params) ->
 108      fprintf fp "%s (" name;
 109      iter_with_commas fp print_expr params;
 110      fprintf fp ")"
 111   | EVar var -> print_id fp var
 112   | EList xs ->
 113      fprintf fp "[";
 114      iter_with_commas fp print_expr xs;
 115      fprintf fp "]"
 116   | ESubsts s -> print_substs fp s
 117   | EString s -> fprintf fp "%S" s
 118
 119 and print_id = output_string
 120
 121 and print_substs fp xs =
 122   let xs =
 123     List.map (
 124       function
 125       | SString s -> sprintf "%S" s
 126       | SVar id -> id
 127     ) xs in
 128   fprintf fp "%s" (String.concat "+" xs)
 129
 130 and print_code fp xs =
 131   List.iter (
 132     function
 133     | SString s -> fprintf fp "%s" s
 134     | SVar id -> fprintf fp "%%%s" id
 135   ) xs