Everything moved to new typechecker

Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.

Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.

1 files changed, 0 insertions, 152 deletions

diff --git a/src/pretty_print_t_ascii.ml b/src/pretty_print_t_ascii.ml
deleted file mode 100644
index 273ceb29..00000000
--- a/src/pretty_print_t_ascii.ml
+++ /dev/null
@@ -1,152 +0,0 @@
-(**************************************************************************)
-(*     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_rmemt -> "rmemt"
-    | BE_wmem -> "wmem"
-    | BE_wmv  -> "wmv"
-    | BE_wmvt  -> "wmvt"
-    | BE_eamem -> "eamem"
-    | BE_exmem -> "exmem"
-    | 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)
-