Factor out pretty printers into separate files. Hopefully this will make searching easier.

1 files changed, 149 insertions, 0 deletions

diff --git a/src/pretty_print_t_ascii.ml b/src/pretty_print_t_ascii.ml
new file mode 100644
index 00000000..79897f4b
--- /dev/null
+++ b/src/pretty_print_t_ascii.ml
@@ -0,0 +1,149 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Type_internal
+open Ast
+open Pretty_print_common
+open Big_int
+
+(* **************************************************************************
+ * pp from tannot to ASCII source, for pp of built-in type environment
+ *)
+
+let rec pp_format_t_ascii t =
+  match t.t with
+    | Tid i -> i
+    | Tvar i -> "'" ^ i
+    | Tfn(t1,t2,_,e) -> (pp_format_t_ascii t1) ^ " -> " ^ (pp_format_t_ascii t2) ^ (match e.effect with Eset [] -> "" | _ -> " effect " ^ pp_format_e_ascii e)
+    | Ttup(tups) -> "(" ^ (list_format ", " pp_format_t_ascii tups) ^ ")"
+    | Tapp(i,args) ->  i ^ "<" ^  list_format ", " pp_format_targ_ascii args ^ ">"
+    | Tabbrev(ti,ta) -> (pp_format_t_ascii ti) (* (pp_format_t_ascii ta) *)
+    | Tuvar(_) -> failwith "Tuvar in pp_format_t_ascii"
+    | Toptions _ -> failwith "Toptions in pp_format_t_ascii"
+and pp_format_targ_ascii = function
+  | TA_typ t ->  pp_format_t_ascii t
+  | TA_nexp n -> pp_format_n_ascii n
+  | TA_eft e ->  pp_format_e_ascii e
+  | TA_ord o ->  pp_format_o_ascii o
+and pp_format_n_ascii n =
+  match n.nexp with
+  | Nid (i, n) -> i (* from an abbreviation *)
+  | Nvar i -> "'" ^ i
+  | Nconst i -> (string_of_int (int_of_big_int i))
+  | Npos_inf -> "infinity"
+  | Nadd(n1,n2) -> (pp_format_n_ascii n1) ^ "+" ^ (pp_format_n_ascii n2)
+  | Nsub(n1,n2) -> (pp_format_n_ascii n1) ^ "-" ^ (pp_format_n_ascii n2)
+  | Nmult(n1,n2) -> (pp_format_n_ascii n1) ^ "*" ^ (pp_format_n_ascii n2)
+  | N2n(n,_) -> "2**"^(pp_format_n_ascii n) (* string_of_big_int i ^ *)
+  | Nneg n -> "-" ^ (pp_format_n_ascii n) 
+  | Nuvar _ -> failwith "Nuvar in pp_format_n_ascii"
+  | Nneg_inf -> "-infinity"
+  | Npow _ -> failwith "Npow in pp_format_n_ascii"
+  | Ninexact -> failwith "Ninexact in pp_format_n_ascii"
+and pp_format_e_ascii e =
+  match e.effect with
+  | Evar i -> "'" ^ i
+  | Eset es -> "{" ^
+                  (list_format ", " pp_format_base_effect_ascii es) ^ "}"
+  | Euvar(_) -> failwith "Euvar in pp_format_e_ascii"
+and pp_format_o_ascii o =
+  match o.order with
+  | Ovar i -> "'" ^ i
+  | Oinc -> "inc"
+  | Odec -> "dec"
+  | Ouvar(_) -> failwith "Ouvar in pp_format_o_ascii"
+and pp_format_base_effect_ascii (BE_aux(e,l)) =
+  match e with
+    | BE_rreg -> "rreg"
+    | BE_wreg -> "wreg"
+    | BE_rmem -> "rmem"
+    | BE_wmem -> "wmem"
+    | BE_wmv  -> "wmv"
+    | BE_eamem -> "eamem"
+    | BE_barr -> "barr"
+    | BE_depend -> "depend"
+    | BE_undef -> "undef"
+    | BE_unspec -> "unspec"
+    | BE_nondet -> "nondet"
+    | BE_lset -> "lset"
+    | BE_lret -> "lret"
+    | BE_escape -> "escape"
+
+and pp_format_nes_ascii nes =
+  list_format ", " pp_format_ne_ascii nes
+
+and pp_format_ne_ascii ne =
+  match ne with
+  | Lt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " < " ^ pp_format_n_ascii n2
+  | LtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " <= " ^ pp_format_n_ascii n2
+  | NtEq(_,n1,n2) ->   pp_format_n_ascii n1 ^ " != " ^ pp_format_n_ascii n2
+  | Eq(_,n1,n2) ->   pp_format_n_ascii n1 ^ " = " ^ pp_format_n_ascii n2
+  | GtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " >= " ^ pp_format_n_ascii n2
+  | Gt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " > " ^ pp_format_n_ascii n2
+  | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) ->
+  i ^ " IN {" ^ (list_format ", " string_of_int ns)^ "}"
+  | InS(_,_,ns)  -> (* when the variable has been replaced by a unification variable, we use this *)
+  failwith "InS in pp_format_nes_ascii" (*"(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"*)
+  | Predicate(_,n1,n2) -> "flow_constraints(" ^ pp_format_ne_ascii n1 ^", "^ pp_format_ne_ascii n2 ^")"
+  | CondCons(_,_,_,nes_c,nes_t) ->
+  failwith "CondCons in pp_format_nes_ascii" (*"(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")"*)
+  | BranchCons(_,_,nes_b) ->
+  failwith "BranchCons in pp_format_nes_ascii" (*"(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"*)
+
+let rec pp_format_annot_ascii = function
+  | NoTyp -> "Nothing"
+  | Base((targs,t),tag,nes,efct,efctsum,_) ->
+    (*TODO print out bindings for use in pattern match in interpreter*)
+      (match tag with External (Some s) -> "("^s^") " | _ -> "") ^
+      (match (targs,nes) with ([],[]) -> "\n" | _ -> 
+        "forall " ^ list_format ", " (function (i,k) -> kind_to_string k ^" '"^ i) targs ^ 
+        (match nes with [] -> "" | _ -> ", " ^ pp_format_nes_ascii nes)
+        ^ ".\n") ^ "     "
+      ^ pp_format_t_ascii t 
+      ^ "\n"
+(*
+^ " ********** " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^
+       pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))"
+*)
+  | Overload (tannot, return_type_overloading_allowed, tannots) -> 
+  (*pp_format_annot_ascii tannot*) "\n" ^ String.concat "" (List.map (function tannot' -> "   " ^ pp_format_annot_ascii tannot' ) tannots)
+