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