summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile2
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/c_backend.ml350
-rw-r--r--src/isail.ml4
-rw-r--r--src/ocaml_backend.ml20
-rw-r--r--src/sail.odocl5
-rw-r--r--src/specialize.ml15
-rw-r--r--src/specialize.mli69
-rw-r--r--src/type_check.mli118
-rw-r--r--src/util.ml18
-rw-r--r--src/util.mli4
11 files changed, 532 insertions, 75 deletions
diff --git a/src/Makefile b/src/Makefile
index a39067b6..3539088e 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -267,7 +267,7 @@ clean:
-rm -f ast.lem
doc:
- ocamlbuild sail.docdir/index.html
+ ocamlbuild -use-ocamlfind sail.docdir/index.html
lib:
ocamlbuild pretty_print.cmxa pretty_print.cma
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 349faac2..c9869cce 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -48,6 +48,8 @@
(* SUCH DAMAGE. *)
(**************************************************************************)
+(** Utilities for operating on Sail ASTs *)
+
open Ast
module Big_int = Nat_big_num
diff --git a/src/c_backend.ml b/src/c_backend.ml
new file mode 100644
index 00000000..1527c99b
--- /dev/null
+++ b/src/c_backend.ml
@@ -0,0 +1,350 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* 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 Ast
+open Ast_util
+open Type_check
+open PPrint
+module Big_int = Nat_big_num
+
+let zencode_id = function
+ | Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l)
+ | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
+
+type aexp =
+ | AE_val of aval
+ | AE_app of id * aval list * typ
+ | AE_let of id * aexp * aexp * typ
+ | AE_block of aexp list * aexp * typ
+ | AE_return of aval * typ
+
+and aval =
+ | AV_lit of lit * typ
+ | AV_id of id * Type_check.lvar
+ | AV_tuple of aval list
+ | AV_C_fragment of string * typ
+
+let rec map_aval f = function
+ | AE_val v -> AE_val (f v)
+ | AE_app (id, vs, typ) -> AE_app (id, List.map f vs, typ)
+ | AE_let (id, aexp1, aexp2, typ) -> AE_let (id, map_aval f aexp1, map_aval f aexp2, typ)
+ | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ)
+ | AE_return (aval, typ) -> AE_return (f aval, typ)
+
+let rec map_functions f = function
+ | AE_app (id, vs, typ) -> f id vs typ
+ | AE_let (id, aexp1, aexp2, typ) -> AE_let (id, map_functions f aexp1, map_functions f aexp2, typ)
+ | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ)
+ | AE_val _ | AE_return _ as v -> v
+
+let pp_id ?color:(color=Util.green) id =
+ string (string_of_id id |> color |> Util.clear)
+
+let pp_lvar lvar doc =
+ match lvar with
+ | Register typ ->
+ string "[R/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
+ | Local (Mutable, typ) ->
+ string "[M/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
+ | Local (Immutable, typ) ->
+ string "[I/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
+ | Enum typ ->
+ string "[E/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
+ | Union (typq, typ) ->
+ string "[U/" ^^ string (string_of_typquant typq ^ "/" ^ string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
+ | Unbound -> string "[?]" ^^ doc
+
+let pp_annot typ doc =
+ string "[" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
+
+let rec pp_aexp = function
+ | AE_val v -> pp_aval v
+ | AE_app (id, args, typ) ->
+ pp_annot typ (pp_id ~color:Util.red id ^^ parens (separate_map (comma ^^ space) pp_aval args))
+ | AE_let (id, binding, body, typ) -> group
+ begin
+ match binding with
+ | AE_let _ ->
+ (pp_annot typ (separate space [string "let"; pp_id id; string "="])
+ ^^ hardline ^^ nest 2 (pp_aexp binding))
+ ^^ hardline ^^ string "in" ^^ space ^^ pp_aexp body
+ | _ ->
+ pp_annot typ (separate space [string "let"; pp_id id; string "="; pp_aexp binding; string "in"])
+ ^^ hardline ^^ pp_aexp body
+ end
+ | AE_block (aexps, aexp, typ) ->
+ pp_annot typ (surround 2 0 lbrace (pp_block (aexps @ [aexp])) rbrace)
+ | AE_return (v, typ) -> pp_annot typ (string "return" ^^ parens (pp_aval v))
+
+and pp_block = function
+ | [] -> string "()"
+ | [aexp] -> pp_aexp aexp
+ | aexp :: aexps -> pp_aexp aexp ^^ semi ^^ hardline ^^ pp_block aexps
+
+and pp_aval = function
+ | AV_lit (lit, typ) -> pp_annot typ (string (string_of_lit lit))
+ | AV_id (id, lvar) -> pp_lvar lvar (pp_id id)
+ | AV_tuple avals -> parens (separate_map (comma ^^ space) pp_aval avals)
+ | AV_C_fragment (str, typ) -> pp_annot typ (string (str |> Util.cyan |> Util.clear))
+
+let ae_lit lit typ = AE_val (AV_lit (lit, typ))
+
+let gensym_counter = ref 0
+
+let gensym () =
+ let id = mk_id ("v" ^ string_of_int !gensym_counter) in
+ incr gensym_counter;
+ id
+
+let rec split_block = function
+ | [exp] -> [], exp
+ | exp :: exps ->
+ let exps, last = split_block exps in
+ exp :: exps, last
+ | [] -> failwith "empty block"
+
+let rec anf (E_aux (e_aux, _) as exp) =
+ let to_aval = function
+ | AE_val v -> (v, fun x -> x)
+ | AE_app (_, _, typ) | AE_let (_, _, _, typ) | AE_return (_, typ) as aexp ->
+ let id = gensym () in
+ (AV_id (id, Local (Immutable, typ)), fun x -> AE_let (id, aexp, x, typ_of exp))
+ in
+ match e_aux with
+ | E_lit lit -> ae_lit lit (typ_of exp)
+
+ | E_block exps ->
+ let exps, last = split_block exps in
+ let aexps = List.map anf exps in
+ let alast = anf last in
+ AE_block (aexps, alast, typ_of exp)
+
+ | E_app (id, exps) ->
+ let aexps = List.map anf exps in
+ let avals = List.map to_aval aexps in
+ let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in
+ wrap (AE_app (id, List.map fst avals, typ_of exp))
+
+ | E_id id ->
+ let lvar = Env.lookup_id id (env_of exp) in
+ AE_val (AV_id (zencode_id id, lvar))
+
+ | E_return exp ->
+ let aval, wrap = to_aval (anf exp) in
+ wrap (AE_return (aval, typ_of exp))
+
+ | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) ->
+ AE_let (zencode_id id, anf binding, anf body, typ_of exp)
+
+ | E_tuple exps ->
+ let aexps = List.map anf exps in
+ let avals = List.map to_aval aexps in
+ let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in
+ wrap (AE_val (AV_tuple (List.map fst avals)))
+
+ | E_cast (typ, exp) -> anf exp
+
+ | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ ->
+ (* Should be re-written by type checker *)
+ failwith "encountered raw vector operation when converting to ANF"
+
+ | E_internal_value _ ->
+ (* Interpreter specific *)
+ failwith "encountered E_internal_value when converting to ANF"
+
+
+let max_int64 = Big_int.of_int64 Int64.max_int
+let min_int64 = Big_int.of_int64 Int64.min_int
+
+let stack_typ (Typ_aux (typ_aux, _) as typ) =
+ match typ_aux with
+ | Typ_id id when string_of_id id = "bit" -> Some "uint64_t"
+ | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" ->
+ begin
+ match destruct_range typ with
+ | None -> None
+ | Some (n, m) ->
+ match nexp_simp n, nexp_simp m with
+ | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) ->
+ if Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 then
+ Some "int64_t"
+ else
+ None
+ | _ -> None
+ end
+ | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _); _; _]) when string_of_id id = "vector" ->
+ begin
+ match nexp_simp n with
+ | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> Some "uint64_t"
+ | _ -> None
+ end
+ | _ -> None
+
+let is_stack_typ typ = match stack_typ typ with
+ | Some _ -> true
+ | None -> false
+
+let literal_to_cstring (L_aux (l_aux, _) as lit) =
+ match l_aux with
+ | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
+ Some (Big_int.to_string n ^ "L")
+ | L_hex str when String.length str <= 16 ->
+ let padding = 16 - String.length str in
+ Some ("0x" ^ String.make padding '0' ^ str ^ "L")
+ | _ -> None
+
+let c_literals =
+ let c_literal = function
+ | AV_lit (lit, typ) as v ->
+ begin
+ match literal_to_cstring lit with
+ | Some str -> AV_C_fragment (str, typ)
+ | None -> v
+ end
+ | v -> v
+ in
+ map_aval c_literal
+
+let mask m =
+ if Big_int.less_equal m (Big_int.of_int 64) then
+ let n = Big_int.to_int m in
+ if n mod 4 == 0
+ then "0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ "L"
+ else "0b" ^ String.make (64 - n) '0' ^ String.make n '1' ^ "L"
+ else
+ failwith "Tried to create a mask literal for a vector greater than 64 bits."
+
+let c_aval = function
+ | AV_lit (lit, typ) as v ->
+ begin
+ match literal_to_cstring lit with
+ | Some str -> AV_C_fragment (str, typ)
+ | None -> v
+ end
+ | AV_C_fragment (str, typ) -> AV_C_fragment (str, typ)
+ (* An id can be converted to a C fragment if it's type can be stack-allocated. *)
+ | AV_id (id, lvar) as v ->
+ begin
+ match lvar with
+ | Local (Immutable, typ) when is_stack_typ typ ->
+ AV_C_fragment (string_of_id id, typ)
+ | _ -> v
+ end
+ | AV_tuple avals -> AV_tuple avals
+
+let is_c_fragment = function
+ | AV_C_fragment _ -> true
+ | _ -> false
+
+let c_fragment_string = function
+ | AV_C_fragment (str, _) -> str
+ | _ -> assert false
+
+let analyze_primop id args typ =
+ let no_change = AE_app (id, args, typ) in
+
+ (* primops add_range and add_atom *)
+ if string_of_id id = "add_range" || string_of_id id = "add_atom" then
+ begin
+ let n, m, x, y = match destruct_range typ, args with
+ | Some (n, m), [x; y] -> n, m, x, y
+ | _ -> failwith ("add_range has incorrect return type or arity ^ " ^ string_of_typ typ)
+ in
+ match nexp_simp n, nexp_simp m with
+ | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) ->
+ if Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 then
+ let x, y = c_aval x, c_aval y in
+ if is_c_fragment x && is_c_fragment y then
+ AE_val (AV_C_fragment (c_fragment_string x ^ " + " ^ c_fragment_string y, typ))
+ else
+ no_change
+ else
+ no_change
+ | _ -> no_change
+ end
+
+ else if string_of_id id = "add_vec" then
+ begin
+ let n, x, y = match typ, args with
+ | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _); _; _]), _), [x; y]
+ when string_of_id id = "vector" -> n, x, y
+ | _ -> failwith ("add_vec has incorrect return type or arity " ^ string_of_typ typ)
+ in
+ match nexp_simp n with
+ | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) ->
+ print_endline "small";
+ let x, y = c_aval x, c_aval y in
+ if is_c_fragment x && is_c_fragment y then
+ AE_val (AV_C_fragment ("(" ^ c_fragment_string x ^ " + " ^ c_fragment_string y ^ ") & " ^ mask n, typ))
+ else
+ no_change
+ | _ -> no_change
+ end
+
+ else
+ no_change
+
+let compile_exp exp =
+ let aexp = anf exp in
+ let aexp = c_literals aexp in
+ let aexp = map_functions analyze_primop aexp in
+ aexp
+
+
+(*
+
+{
+ uint64_t zx = 0x000000000000F000L;
+ uint64_t v0 = (zx + 0x000000000000000FL) & 0x000000000000FFFFL;
+ uint64_t res = (v0 + 0x000000000000FFFFL) & 0x000000000000FFFFL;
+ return res;
+}
+
+*)
diff --git a/src/isail.ml b/src/isail.ml
index ce17561d..235e46a2 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -294,6 +294,10 @@ let handle_input' input =
interactive_state := initial_state !interactive_ast;
interactive_env := env;
vs_ids := Initial_check.val_spec_ids !interactive_ast
+ | ":compile" ->
+ let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord arg) in
+ let anf = C_backend.compile_exp exp in
+ print_endline (Pretty_print_sail.to_string (C_backend.pp_aexp anf))
| ":u" | ":unload" ->
interactive_ast := Ast.Defs [];
interactive_env := Type_check.initial_env;
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 970dea83..a2c40b03 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -52,6 +52,7 @@ open Ast
open Ast_util
open PPrint
open Type_check
+open Util
module Big_int = Nat_big_num
@@ -77,25 +78,6 @@ let gensym () =
incr gensym_counter;
string gs
-let zchar c =
- let zc c = "z" ^ String.make 1 c in
- if Char.code c <= 41 then zc (Char.chr (Char.code c + 16))
- else if Char.code c <= 47 then zc (Char.chr (Char.code c + 23))
- else if Char.code c <= 57 then String.make 1 c
- else if Char.code c <= 64 then zc (Char.chr (Char.code c + 13))
- else if Char.code c <= 90 then String.make 1 c
- else if Char.code c <= 94 then zc (Char.chr (Char.code c - 13))
- else if Char.code c <= 95 then "_"
- else if Char.code c <= 96 then zc (Char.chr (Char.code c - 13))
- else if Char.code c <= 121 then String.make 1 c
- else if Char.code c <= 122 then "zz"
- else if Char.code c <= 126 then zc (Char.chr (Char.code c - 39))
- else raise (Invalid_argument "zchar")
-
-let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
-
-let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
-
let zencode ctx id =
try string (string_of_id (Bindings.find id ctx.externs)) with
| Not_found -> string (zencode_string (string_of_id id))
diff --git a/src/sail.odocl b/src/sail.odocl
index 445d6b73..87209053 100644
--- a/src/sail.odocl
+++ b/src/sail.odocl
@@ -1,4 +1,5 @@
ast
+ast_util
finite_map
initial_check
lexer
@@ -6,10 +7,10 @@ sail
parse_ast
parser
pp
-pre_lexer
-pre_parser
pretty_print
process_file
reporting_basic
+rewriter
+specialize
type_check
util
diff --git a/src/specialize.ml b/src/specialize.ml
index 2d32a90c..10c4945e 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -71,22 +71,18 @@ let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.ma
let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
-let is_typ_uvar = function
+let is_typ_ord_uvar = function
| Type_check.U_typ _ -> true
+ | Type_check.U_order _ -> true
| _ -> false
(* We have to be careful about whether the typechecker has renamed anything returned by instantiation_of.
This part of the typechecker API is a bit ugly. *)
let fix_instantiation instantiation =
- let instantiation = KBindings.bindings (KBindings.filter (fun _ uvar -> is_typ_uvar uvar) instantiation) in
+ let instantiation = KBindings.bindings (KBindings.filter (fun _ uvar -> is_typ_ord_uvar uvar) instantiation) in
let instantiation = List.map (fun (kid, uvar) -> Type_check.orig_kid kid, uvar) instantiation in
List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty instantiation
-(* Returns an IdSet with the function ids that have X-kinded
- parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first
- argument specifies what X should be - it should be one of:
- is_nat_kopt, is_order_kopt, or is_typ_kopt from Ast_util.
-*)
let rec polymorphic_functions is_kopt (Defs defs) =
match defs with
| DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, _, externs), _)) :: defs ->
@@ -180,7 +176,7 @@ let specialize_id_valspec instantiations id ast =
(* Remove type variables from the type quantifier. *)
let kopts, constraints = quant_split typq in
- let kopts = List.filter (fun kopt -> not (is_typ_kopt kopt)) kopts in
+ let kopts = List.filter (fun kopt -> not (is_typ_kopt kopt || is_order_kopt kopt)) kopts in
let typq = mk_typquant (List.map (mk_qi_id BK_type) frees @ List.map mk_qi_kopt kopts @ List.map mk_qi_nc constraints) in
let typschm = mk_typschm typq typ in
@@ -261,7 +257,6 @@ let remove_unused_valspecs ast =
List.fold_left (fun ast id -> Defs (remove_unused ast id)) ast (IdSet.elements unused)
let specialize_id id ast =
- print_endline ("Specializing: " ^ string_of_id id);
let instantiations = instantiations_of id ast in
let ast = specialize_id_valspec instantiations id ast in
@@ -296,7 +291,7 @@ let specialize_ids ids ast =
ast, env
let rec specialize ast env =
- let ids = polymorphic_functions is_typ_kopt ast in
+ let ids = polymorphic_functions (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt) ast in
if IdSet.is_empty ids then
ast, env
else
diff --git a/src/specialize.mli b/src/specialize.mli
new file mode 100644
index 00000000..0c4a2495
--- /dev/null
+++ b/src/specialize.mli
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* 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. *)
+(**************************************************************************)
+
+(** Rewrites for removing polymorphism from specifications *)
+
+open Ast
+open Ast_util
+open Type_check
+
+(** Returns an IdSet with the function ids that have X-kinded
+ parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first
+ argument specifies what X should be - it should be one of:
+ [is_nat_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
+ or some combination of those. *)
+val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
+
+(** specialize returns an AST with all the Order and Type polymorphism
+ removed, as well as the environment produced by type checking that
+ AST with [Type_check.initial_env]. The env parameter is the
+ environment to return if there is no polymorphism to remove, in
+ which case specialize returns the AST unmodified. *)
+val specialize : tannot defs -> Env.t -> tannot defs * Env.t
diff --git a/src/type_check.mli b/src/type_check.mli
index 68e3ad09..b904769f 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -48,13 +48,30 @@
(* SUCH DAMAGE. *)
(**************************************************************************)
+(** The type checker API *)
+
open Ast
open Ast_util
module Big_int = Nat_big_num
+(** [opt_tc_debug] controls the verbosity of the type checker. 0 is
+ silent, 1 prints a tree of the type derivation and 2 is like 1 but
+ with much more debugging information. *)
val opt_tc_debug : int ref
+
+(** [opt_no_effects] turns of the effect checking. This can break
+ re-writer passes, so it should only be used for debugging. *)
val opt_no_effects : bool ref
+type mut = Immutable | Mutable
+
+(** [lvar] is the type of variables - they can either be registers,
+ local mutable or immutable variables, nullary union constructors
+ (i.e. None in option), or unbound identifiers *)
+type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
+
+(** {2 Type errors} *)
+
type type_error =
| Err_no_casts of unit exp * type_error * type_error list
| Err_no_overloading of id * (id * type_error) list
@@ -67,37 +84,38 @@ exception Type_error of l * type_error;;
val string_of_type_error : type_error -> string
-type mut = Immutable | Mutable
-
-type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
+(** {2 Environments} *)
+(** The env module defines the internal type checking environment, and
+ contains functions that operate on that state. *)
module Env : sig
- (* Env.t is the type of environments *)
+ (** Env.t is the type of environments *)
type t
- (* Note: Most get_ functions assume the identifiers exist, and throw type
- errors if it doesn't. *)
+ (** Note: Most get_ functions assume the identifiers exist, and throw
+ type errors if it doesn't. *)
+ (** get the quantifier and type for a function identifier. *)
val get_val_spec : id -> t -> typquant * typ
val update_val_spec : id -> typquant * typ -> t -> t
val get_register : id -> t -> typ
- (* Return all the identifiers in an enumeration. Throws a type error
- if the enumeration doesn't exist. *)
+ (** Return all the identifiers in an enumeration. Throws a type
+ error if the enumeration doesn't exist. *)
val get_enum : id -> t -> id list
val get_locals : t -> (mut * typ) Bindings.t
val add_local : id -> mut * typ -> t -> t
- (* Check if a local variable is mutable. Throws Type_error if it
+ (** Check if a local variable is mutable. Throws Type_error if it
isn't a local variable. Probably best to use Env.lookup_id
instead *)
val is_mutable : id -> t -> bool
- (* Get the current set of constraints. *)
+ (** Get the current set of constraints. *)
val get_constraints : t -> n_constraint list
val add_constraint : n_constraint -> t -> t
@@ -110,13 +128,13 @@ module Env : sig
val is_record : id -> t -> bool
- (* Return type is: quantifier, argument type, return type, effect *)
+ (** Return type is: quantifier, argument type, return type, effect *)
val get_accessor : id -> id -> t -> typquant * typ * typ * effect
- (* If the environment is checking a function, then this will get the
- expected return type of the function. It's useful for checking or
- inserting early returns. Returns an option type and won't throw
- any exceptions. *)
+ (** If the environment is checking a function, then this will get
+ the expected return type of the function. It's useful for
+ checking or inserting early returns. Returns an option type and
+ won't throw any exceptions. *)
val get_ret_typ : t -> typ option
val get_typ_synonym : id -> t -> (t -> typ_arg list -> typ)
@@ -129,7 +147,7 @@ module Env : sig
val get_extern : id -> t -> string -> string
- (* Lookup id searchs for a specified id in the environment, and
+ (** Lookup id searchs for a specified id in the environment, and
returns it's type and what kind of identifier it is, using the
lvar type. Returns Unbound if the identifier is unbound, and
won't throw any exceptions. *)
@@ -137,17 +155,17 @@ module Env : sig
val is_union_constructor : id -> t -> bool
- (* Return a fresh kind identifier that doesn't exist in the
+ (** Return a fresh kind identifier that doesn't exist in the
environment. The optional argument bases the new identifer on the
old one. *)
val fresh_kid : ?kid:kid -> t -> kid
val expand_synonyms : t -> typ -> typ
- (* Expand type synonyms and remove register annotations (i.e. register<t> -> t)) *)
+ (** Expand type synonyms and remove register annotations (i.e. register<t> -> t)) *)
val base_typ_of : t -> typ -> typ
- (* no_casts removes all the implicit type casts/coercions from the
+ (** no_casts removes all the implicit type casts/coercions from the
environment, so checking a term with such an environment will
guarantee not to insert any casts. Not that this is only about
the implicit casting and has nothing to do with the E_cast AST
@@ -161,13 +179,12 @@ module Env : sig
end
-(* Push all the type variables and constraints from a typquant into an environment *)
+(** Push all the type variables and constraints from a typquant into
+ an environment *)
val add_typquant : typquant -> Env.t -> Env.t
-val typ_frees : ?exs:KidSet.t -> typ -> KidSet.t
-
-(* When the typechecker creates new type variables it gives them fresh
- names of the form 'fvXXX#name, where XXX is a number (not
+(** When the typechecker creates new type variables it gives them
+ fresh names of the form 'fvXXX#name, where XXX is a number (not
necessarily three digits), and name is the original name when the
type variable was created by renaming an exisiting type variable to
avoid shadowing. orig_kid takes such a type variable and strips out
@@ -180,14 +197,23 @@ val dvector_typ : Env.t -> nexp -> typ -> typ
val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
+(** The type of type annotations *)
type tannot = (Env.t * typ * effect) option
-(* Strip the type annotations from an expression. *)
+(** {2 Removing type annotations} *)
+
+(** Strip the type annotations from an expression. *)
val strip_exp : 'a exp -> unit exp
+
+(** Strip the type annotations from a pattern *)
val strip_pat : 'a pat -> unit pat
+
+(** Strip the type annotations from an l-expression *)
val strip_lexp : 'a lexp -> unit lexp
-(* Check an expression has some type. Returns a fully annotated
+(** {2 Checking expressions and patterns} *)
+
+(** Check an expression has some type. Returns a fully annotated
version of the expression, where each subexpression is annotated
with it's type and the Environment used while checking it. The can
be used to re-start the typechecking process on any
@@ -202,14 +228,16 @@ val prove : Env.t -> n_constraint -> bool
val subtype_check : Env.t -> typ -> typ -> bool
val bind_pat : Env.t -> unit pat -> typ -> tannot pat * Env.t * unit Ast.exp list
-(* Variant that doesn't introduce new guards for literal patterns, but raises
- a type error instead. This should always be safe to use on patterns that
- have previously been type checked. *)
+
+(** Variant that doesn't introduce new guards for literal patterns,
+ but raises a type error instead. This should always be safe to use
+ on patterns that have previously been type checked. *)
val bind_pat_no_guard : Env.t -> unit pat -> typ -> tannot pat * Env.t
-(* Partial functions: The expressions and patterns passed to these
- functions must be guaranteed to have tannots of the form Some (env,
- typ) for these to work. *)
+(** {2 Destructuring type annotations} Partial functions: The
+ expressions and patterns passed to these functions must be
+ guaranteed to have tannots of the form Some (env, typ) for these to
+ work. *)
val env_of : tannot exp -> Env.t
val env_of_annot : Ast.l * tannot -> Env.t
@@ -224,10 +252,12 @@ val effect_of : tannot exp -> effect
val effect_of_annot : tannot -> effect
val add_effect_annot : tannot -> effect -> tannot
+(** {2 Utilities } *)
+
val destruct_atom_nexp : Env.t -> typ -> nexp option
-(* Safely destructure an existential type. Returns None if the type is
- not existential. This function will pick a fresh name for the
+(** Safely destructure an existential type. Returns None if the type
+ is not existential. This function will pick a fresh name for the
existential to ensure that no name-clashes occur. *)
val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option
@@ -247,33 +277,37 @@ val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constrai
val alpha_equivalent : Env.t -> typ -> typ -> bool
-(* Throws Invalid_argument if the argument is not a E_app expression *)
+(** Throws Invalid_argument if the argument is not a E_app expression *)
val instantiation_of : tannot exp -> uvar KBindings.t
val propagate_exp_effect : tannot exp -> tannot exp
+
val propagate_pexp_effect : tannot pexp -> tannot pexp * effect
-(* Fully type-check an AST
+(** {2 Checking full AST} *)
+
+(** Fully type-check an AST
Some invariants that will hold of a fully checked AST are:
- * No internal nodes, such as E_internal_exp, or E_comment nodes.
+ - No internal nodes, such as E_internal_exp, or E_comment nodes.
- * E_vector_access nodes and similar will be replaced by function
+ - E_vector_access nodes and similar will be replaced by function
calls E_app to vector access functions. This is different to the
old type checker.
- * Every expressions type annotation (tannot) will be Some (typ, env).
+ - Every expressions type annotation [tannot] will be Some (typ, env).
- * Also every pattern will be annotated with the type it matches.
+ - Also every pattern will be annotated with the type it matches.
- * Toplevel expressions such as typedefs and some subexpressions such
+ - Toplevel expressions such as typedefs and some subexpressions such
as letbinds may have None as their tannots if it doesn't make sense
for them to have type annotations. *)
val check : Env.t -> 'a defs -> tannot defs * Env.t
-(* Like check but throws type_errors rather than Sail generic errors
+(** Like check but throws type_errors rather than Sail generic errors
from Reporting_basic. *)
val check' : Env.t -> 'a defs -> tannot defs * Env.t
+(** The initial type checking environment *)
val initial_env : Env.t
diff --git a/src/util.ml b/src/util.ml
index e902b2dd..94bbc6dc 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -395,3 +395,21 @@ let cyan str = termcode 96 ^ str
let blue str = termcode 94 ^ str
let clear str = str ^ termcode 0
+let zchar c =
+ let zc c = "z" ^ String.make 1 c in
+ if Char.code c <= 41 then zc (Char.chr (Char.code c + 16))
+ else if Char.code c <= 47 then zc (Char.chr (Char.code c + 23))
+ else if Char.code c <= 57 then String.make 1 c
+ else if Char.code c <= 64 then zc (Char.chr (Char.code c + 13))
+ else if Char.code c <= 90 then String.make 1 c
+ else if Char.code c <= 94 then zc (Char.chr (Char.code c - 13))
+ else if Char.code c <= 95 then "_"
+ else if Char.code c <= 96 then zc (Char.chr (Char.code c - 13))
+ else if Char.code c <= 121 then String.make 1 c
+ else if Char.code c <= 122 then "zz"
+ else if Char.code c <= 126 then zc (Char.chr (Char.code c - 39))
+ else raise (Invalid_argument "zchar")
+
+let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str))
+
+let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str))
diff --git a/src/util.mli b/src/util.mli
index 39bc8a19..8fcf68be 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -108,7 +108,6 @@ val option_these : 'a option list -> 'a list
application of [f], [x] is used in case [g x] returns [None] and
similarly [y] in case [h y] returns [None]. *)
val changed2 : ('a -> 'b -> 'c) -> ('a -> 'a option) -> 'a -> ('b -> 'b option) -> 'b -> 'c option
-
(** {2 List Functions} *)
@@ -240,3 +239,6 @@ val yellow : string -> string
val cyan : string -> string
val blue : string -> string
val clear : string -> string
+
+val zencode_string : string -> string
+val zencode_upper_string : string -> string
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 03:55:48 +0000