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