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