diff options
42 files changed, 1843 insertions, 3 deletions
@@ -1,7 +1,7 @@ true: -traverse, debug <**/*.ml>: bin_annot, annot <lem_interp> or <test>: include -<sail.{byte,native}>: use_pprint, use_nums +<sail.{byte,native}>: use_pprint, use_nums, use_unix <pprint> or <pprint/src>: include # see http://caml.inria.fr/mantis/view.php?id=4943 @@ -486,7 +486,7 @@ type type -'a val_spec_aux = (* Value type specification *) +val_spec_aux = (* Value type specification *) VS_val_spec of typschm * id | VS_extern_no_rename of typschm * id | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) @@ -536,7 +536,7 @@ type type 'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot + VS_aux of val_spec_aux * 'a annot type diff --git a/src/constraint.ml b/src/constraint.ml new file mode 100644 index 00000000..8b28fa4a --- /dev/null +++ b/src/constraint.ml @@ -0,0 +1,306 @@ +open Big_int +open Util + +(* ===== Integer Constraints ===== *) + +type nexp_op = Plus | Minus | Mult + +type nexp = + | NFun of (nexp_op * nexp * nexp) + | N2n of nexp + | NConstant of big_int + | NVar of int + +let big_int_op : nexp_op -> big_int -> big_int -> big_int = function + | Plus -> add_big_int + | Minus -> sub_big_int + | Mult -> mult_big_int + +let rec arith constr = + let constr' = match constr with + | NFun (op, x, y) -> NFun (op, arith x, arith y) + | N2n c -> arith c + | c -> c + in + match constr' with + | NFun (op, NConstant x, NConstant y) -> NConstant (big_int_op op x y) + | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x) + | c -> c + +(* ===== Boolean Constraints ===== *) + +type constraint_bool_op = And | Or + +type constraint_compare_op = Gt | Lt | GtEq | LtEq | Eq | NEq + +let negate_comparison = function + | Gt -> LtEq + | Lt -> GtEq + | GtEq -> Lt + | LtEq -> Gt + | Eq -> NEq + | NEq -> Eq + +type 'a constraint_bool = + | BFun of (constraint_bool_op * 'a constraint_bool * 'a constraint_bool) + | Not of 'a constraint_bool + | CFun of (constraint_compare_op * 'a * 'a) + | Branch of ('a constraint_bool list) + | Boolean of bool + +let rec pairs (xs : 'a list) (ys : 'a list) : ('a * 'b) list = + match xs with + | [] -> [] + | (x :: xs) -> List.map (fun y -> (x, y)) ys @ pairs xs ys + +let rec unbranch : 'a constraint_bool -> 'a constraint_bool list = function + | Branch xs -> List.map unbranch xs |> List.concat + | Not x -> unbranch x |> List.map (fun y -> Not y) + | BFun (op, x, y) -> + let xs, ys = unbranch x, unbranch y in + List.map (fun (z, w) -> BFun (op, z, w)) (pairs xs ys) + | c -> [c] + +(* Apply De Morgan's laws to push all negations to just before integer + constraints *) +let rec de_morgan : 'a constraint_bool -> 'a constraint_bool = function + | Not (Not x) -> de_morgan x + | Not (BFun (And, x, y)) -> BFun (Or, de_morgan (Not x), de_morgan (Not y)) + | Not (BFun (Or, x, y)) -> BFun (And, de_morgan (Not x), de_morgan (Not y)) + | Not (Boolean b) -> Boolean (not b) + | BFun (op, x, y) -> BFun (op, de_morgan x, de_morgan y) + | c -> c + +(* Once De Morgan's laws are applied we can push all the Nots into + comparison constraints *) +let rec remove_nots : 'a constraint_bool -> 'a constraint_bool = function + | BFun (op, x, y) -> BFun (op, remove_nots x, remove_nots y) + | Not (CFun (c, x, y)) -> CFun (negate_comparison c, x, y) + | c -> c + +(* Apply distributivity so all Or clauses are within And clauses *) +let rec distrib_step : 'a constraint_bool -> ('a constraint_bool * int) = function + | BFun (Or, x, BFun (And, y, z)) -> + let (xy, n) = distrib_step (BFun (Or, x, y)) in + let (xz, m) = distrib_step (BFun (Or, x, z)) in + BFun (And, xy, xz), n + m + 1 + | BFun (Or, BFun (And, x, y), z) -> + let (xz, n) = distrib_step (BFun (Or, x, z)) in + let (yz, m) = distrib_step (BFun (Or, y, z)) in + BFun (And, xz, yz), n + m + 1 + | BFun (op, x, y) -> + let (x', n) = distrib_step x in + let (y', m) = distrib_step y in + BFun (op, x', y'), n + m + | c -> (c, 0) + +let rec distrib (c : 'a constraint_bool) : 'a constraint_bool = + let (c', n) = distrib_step c in + if n = 0 then c else distrib c' + +(* Once these steps have been applied, the constraint language is a + list of And clauses, each a list of Or clauses, with either + explicit booleans (LBool) or integer comparisons LFun. The flatten + function coverts from a constraint_bool to this representation. *) +type 'a constraint_leaf = + | LFun of (constraint_compare_op * 'a * 'a) + | LBoolean of bool + +let rec flatten_or : 'a constraint_bool -> 'a constraint_leaf list = function + | BFun (Or, x, y) -> flatten_or x @ flatten_or y + | CFun comparison -> [LFun comparison] + | Boolean b -> [LBoolean b] + | _ -> assert false + +let rec flatten : 'a constraint_bool -> 'a constraint_leaf list list = function + | BFun (And, x, y) -> flatten x @ flatten y + | Boolean b -> [[LBoolean b]] + | c -> [flatten_or c] + +let normalize (constr : 'a constraint_bool) : 'a constraint_leaf list list = + constr + |> de_morgan + |> remove_nots + |> distrib + |> flatten + +(* Get a set of variables from a constraint *) +module IntSet = Set.Make( + struct + let compare = Pervasives.compare + type t = int + end) + +let rec int_expr_vars : nexp -> IntSet.t = function + | NConstant _ -> IntSet.empty + | NVar v -> IntSet.singleton v + | NFun (_, x, y) -> IntSet.union (int_expr_vars x) (int_expr_vars y) + | N2n x -> int_expr_vars x + +let leaf_expr_vars : nexp constraint_leaf -> IntSet .t = function + | LBoolean _ -> IntSet.empty + | LFun (_, x, y) -> IntSet.union (int_expr_vars x) (int_expr_vars y) + +let constraint_vars constr : IntSet.t = + constr + |> List.map (List.map leaf_expr_vars) + |> List.map (List.fold_left IntSet.union IntSet.empty) + |> List.fold_left IntSet.union IntSet.empty + +(* SMTLIB v2.0 format is based on S-expressions so we have a + lightweight representation of those here. *) +type sexpr = List of (sexpr list) | Atom of string + +let sfun (fn : string) (xs : sexpr list) : sexpr = List (Atom fn :: xs) + +let rec pp_sexpr : sexpr -> string = function + | List xs -> "(" ^ string_of_list " " pp_sexpr xs ^ ")" + | Atom x -> x + +let var_decs constr = + constraint_vars constr + |> IntSet.elements + |> List.map (fun var -> sfun "declare-const" [Atom ("v" ^ string_of_int var); Atom "Int"]) + |> string_of_list "\n" pp_sexpr + +let cop_sexpr op x y = + match op with + | Gt -> sfun ">" [x; y] + | Lt -> sfun "<" [x; y] + | GtEq -> sfun ">=" [x; y] + | LtEq -> sfun "<=" [x; y] + | Eq -> sfun "=" [x; y] + | NEq -> sfun "not" [sfun "=" [x; y]] + +let iop_sexpr op x y = + match op with + | Plus -> sfun "+" [x; y] + | Minus -> sfun "-" [x; y] + | Mult -> sfun "*" [x; y] + +let rec sexpr_of_nexp = function + | NFun (op, x, y) -> iop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y) + | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x] + | NConstant c -> Atom (string_of_big_int c) (* CHECK: do we do negative constants right? *) + | NVar var -> Atom ("v" ^ string_of_int var) + +let rec sexpr_of_cbool = function + | BFun (And, x, y) -> sfun "and" [sexpr_of_cbool x; sexpr_of_cbool y] + | BFun (Or, x, y) -> sfun "or" [sexpr_of_cbool x; sexpr_of_cbool y] + | Not x -> sfun "not" [sexpr_of_cbool x] + | CFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y) + | Branch xs -> sfun "BRANCH" (List.map sexpr_of_cbool xs) + | Boolean true -> Atom "true" + | Boolean false -> Atom "false" + +let sexpr_of_constraint_leaf = function + | LFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y) + | LBoolean true -> Atom "true" + | LBoolean false -> Atom "false" + +let sexpr_of_constraint constr : sexpr = + constr + |> List.map (List.map sexpr_of_constraint_leaf) + |> List.map (fun xs -> match xs with [x] -> x | _ -> (sfun "or" xs)) + |> sfun "and" + +let smtlib_of_constraint constr : string = + "(push)\n" + ^ var_decs constr ^ "\n" + ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; sexpr_of_constraint constr]) + ^ "\n(assert constraint)\n(check-sat)\n(pop)" + +type t = nexp constraint_bool + +type smt_result = Unknown of t list | Unsat of t + +let rec call_z3 constraints : smt_result = + let problems = unbranch constraints in + let z3_file = + problems + |> List.map normalize + |> List.map smtlib_of_constraint + |> string_of_list "\n" (fun x -> x) + in + + (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) + + let rec input_lines chan = function + | 0 -> [] + | n -> + begin + let l = input_line chan in + let ls = input_lines chan (n - 1) in + l :: ls + end + in + + begin + let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in + output_string tmp_chan z3_file; + close_out tmp_chan; + let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in + let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in + let _ = Unix.close_process_in z3_chan in + Sys.remove input_file; + try + let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in + Unsat problem + with + | Not_found -> + z3_output + |> List.filter (fun (_, result) -> result = "unknown") + |> List.map fst + |> (fun unsolved -> Unknown unsolved) + end + +let string_of constr = + constr + |> unbranch + |> List.map normalize + |> List.map (fun c -> smtlib_of_constraint c) + |> string_of_list "\n" (fun x -> x) + +(* ===== Abstract API for building constraints ===== *) + +(* These functions are exported from constraint.mli, and ensure that + the internal representation of constraints remains opaque. *) + +let implies (x : t) (y : t) : t = + BFun (Or, Not x, y) + +let conj (x : t) (y : t) : t = + BFun (And, x, y) + +let disj (x : t) (y : t) : t = + BFun (Or, x, y) + +let negate (x : t) : t = Not x + +let branch (xs : t list) : t = Branch xs + +let literal (b : bool) : t = Boolean b + +let lt x y : t = CFun (Lt, x, y) + +let lteq x y : t = CFun (LtEq, x, y) + +let gt x y : t = CFun (Gt, x, y) + +let gteq x y : t = CFun (GtEq, x, y) + +let eq x y : t = CFun (Eq, x, y) + +let neq x y : t = CFun (NEq, x, y) + +let pow2 x : nexp = N2n x + +let add x y : nexp = NFun (Plus, x, y) + +let sub x y : nexp = NFun (Minus, x, y) + +let mult x y : nexp = NFun (Mult, x, y) + +let constant (x : big_int) : nexp = NConstant x + +let variable (v : int) : nexp = NVar v diff --git a/src/constraint.mli b/src/constraint.mli new file mode 100644 index 00000000..3fb3d2f6 --- /dev/null +++ b/src/constraint.mli @@ -0,0 +1,30 @@ +type nexp +type t + +type smt_result = Unknown of t list | Unsat of t + +val call_z3 : t -> smt_result + +val string_of : t -> string + +val implies : t -> t -> t +val conj : t -> t -> t +val disj : t -> t -> t +val negate : t -> t +val branch : t list -> t +val literal : bool -> t + +val lt : nexp -> nexp -> t +val lteq : nexp -> nexp -> t +val gt : nexp -> nexp -> t +val gteq : nexp -> nexp -> t +val eq : nexp -> nexp -> t +val neq : nexp -> nexp -> t + +val pow2 : nexp -> nexp +val add : nexp -> nexp -> nexp +val sub : nexp -> nexp -> nexp +val mult : nexp -> nexp -> nexp + +val constant : Big_int.big_int -> nexp +val variable : int -> nexp diff --git a/src/process_file.ml b/src/process_file.ml index 273979cf..12a067e1 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -88,6 +88,8 @@ let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)= Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs +let opt_new_typecheck = ref false + let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs = let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env; Type_internal.nabbrevs = Envmap.empty; @@ -97,6 +99,9 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast. {Type_internal.order = (match o with | (Ast.Ord_aux(Ast.Ord_inc,_)) -> Type_internal.Oinc | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec | _ -> Type_internal.Oinc)};} in + if !opt_new_typecheck + then let _ = Type_check_new.check Type_check_new.initial_env defs in () + else (); Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs diff --git a/src/process_file.mli b/src/process_file.mli index 2c18b830..bfc719cc 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -48,6 +48,8 @@ val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs +val opt_new_typecheck : bool ref + type out_type = | Lem_ast_out | Lem_out of string option (* If present, the string is a file to open in the lem backend*) diff --git a/src/sail.ml b/src/sail.ml index 4e76551f..343a677c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -86,6 +86,9 @@ let options = Arg.align ([ ( "-skip_constraints", Arg.Clear Type_internal.do_resolve_constraints, " (debug) skip constraint resolution in type-checking"); + ( "-new_typecheck", + Arg.Set opt_new_typecheck, + " use new typechecker with Z3 constraint solving (experimental)"); ( "-v", Arg.Set opt_print_version, " print version"); diff --git a/src/type_check_new.ml b/src/type_check_new.ml new file mode 100644 index 00000000..175586ed --- /dev/null +++ b/src/type_check_new.ml @@ -0,0 +1,997 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* *) +(* 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 Util +open Big_int + +let debug = ref 1 +let depth = ref 0 + +let typ_debug m = if !debug > 1 then prerr_endline m else () + +let rec indent n = match n with + | 0 -> "" + | n -> "| " ^ indent (n - 1) + +let typ_print m = if !debug > 0 then (prerr_endline (indent !depth ^ m)) else () + +let typ_error l m = raise (Reporting_basic.err_typ l m) + +let string_of_id = function + | Id_aux (Id v, _) -> v + | Id_aux (DeIid v, _) -> v + +let string_of_kid = function + | Kid_aux (Var v, _) -> v + +let id_loc = function + | Id_aux (_, l) -> l + +let kid_loc = function + | Kid_aux (_, l) -> l + +let string_of_base_effect_aux = function + | BE_rreg -> "rreg" + | BE_wreg -> "wreg" + | BE_rmem -> "rmem" + | BE_rmemt -> "rmemt" + | BE_wmem -> "wmem" + | BE_eamem -> "eamem" + | BE_exmem -> "exmem" + | BE_wmv -> "wmv" + | BE_wmvt -> "wmvt" + | BE_barr -> "barr" + | BE_depend -> "depend" + | BE_undef -> "undef" + | BE_unspec -> "unspec" + | BE_nondet -> "nondet" + | BE_escape -> "escape" + | BE_lset -> "lset" + | BE_lret -> "lret" + +let string_of_base_kind_aux = function + | BK_type -> "Type" + | BK_nat -> "Nat" + | BK_order -> "Order" + | BK_effect -> "Effect" + +let string_of_base_effect = function + | BE_aux (beff, _) -> string_of_base_effect_aux beff + +let string_of_effect = function + | Effect_aux (Effect_var kid, _) -> + typ_debug "kid effect occured"; string_of_kid kid + | Effect_aux (Effect_set [], _) -> "pure" + | Effect_aux (Effect_set beffs, _) -> + "{" ^ string_of_list ", " string_of_base_effect beffs ^ "}" + +let string_of_order = function + | Ord_aux (Ord_var kid, _) -> string_of_kid kid + | Ord_aux (Ord_inc, _) -> "inc" + | Ord_aux (Ord_dec, _) -> "dec" + +let rec string_of_nexp = function + | Nexp_aux (nexp, _) -> string_of_nexp_aux nexp +and string_of_nexp_aux = function + | Nexp_id id -> string_of_id id + | Nexp_var kid -> string_of_kid kid + | Nexp_constant c -> string_of_int c + | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")" + | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")" + | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")" + | Nexp_exp n -> "2 ^ " ^ string_of_nexp n + | Nexp_neg n -> "- " ^ string_of_nexp n + +let rec string_of_typ = function + | Typ_aux (typ, l) -> string_of_typ_aux typ +and string_of_typ_aux = function + | Typ_wild -> "_" + | Typ_id id -> string_of_id id + | Typ_var kid -> string_of_kid kid + | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" + | Typ_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_typ_arg args ^ ">" + | Typ_fn (typ_arg, typ_ret, eff) -> + string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff +and string_of_typ_arg = function + | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg +and string_of_typ_arg_aux = function + | Typ_arg_nexp n -> string_of_nexp n + | Typ_arg_typ typ -> string_of_typ typ + | Typ_arg_order o -> string_of_order o + | Typ_arg_effect eff -> string_of_effect eff + +let string_of_n_constraint = function + | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 + | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 + | NC_aux (NC_nat_set_bounded (kid, ns), _) -> + string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}" + +let string_of_quant_item_aux = function + | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid + | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "KIND " ^ string_of_kid kid + | QI_const constr -> string_of_n_constraint constr + +let string_of_quant_item = function + | QI_aux (qi, _) -> string_of_quant_item_aux qi + +let string_of_typquant_aux = function + | TypQ_tq quants -> "forall " ^ string_of_list ", " string_of_quant_item quants + | TypQ_no_forall -> "" + +let string_of_typquant = function + | TypQ_aux (quant, _) -> string_of_typquant_aux quant + +let string_of_typschm (TypSchm_aux (TypSchm_ts (quant, typ), _)) = + string_of_typquant quant ^ ". " ^ string_of_typ typ + +let string_of_bind (typquant, typ) = string_of_typquant typquant ^ ". " ^ string_of_typ typ + +let string_of_lit (L_aux (lit, _)) = + match lit with + | L_unit -> "()" + | L_zero -> "bitzero" (* FIXME: Check *) + | L_one -> "bitone" + | L_true -> "true" + | L_false -> "false" + | L_num n -> string_of_int n + | L_hex n -> "0x" ^ n + | L_bin n -> "0b" ^ n + | L_undef -> "undefined" + | L_string str -> "\"" ^ str ^ "\"" + +let rec string_of_exp (E_aux (exp, _)) = + match exp with + | E_block exps -> "{ " ^ string_of_list "; " string_of_exp exps ^ " }" + | E_id v -> string_of_id v + | E_sizeof nexp -> "sizeof " ^ string_of_nexp nexp + | E_lit lit -> string_of_lit lit + | E_return exp -> "return " ^ string_of_exp exp + | E_app (f, args) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp args ^ ")" + | E_tuple exps -> "(" ^ string_of_list ", " string_of_exp exps ^ ")" + | E_case (exp, cases) -> + "switch " ^ string_of_exp exp ^ " { case " ^ string_of_list " case " string_of_pexp cases ^ "}" + | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp + | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind + | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp + | _ -> "INTERNAL" +and string_of_pexp (Pat_aux (Pat_exp (pat, exp), _)) = string_of_pat pat ^ " -> " ^ string_of_exp exp +and string_of_pat (P_aux (pat, l)) = + match pat with + | P_lit lit -> string_of_lit lit + | P_wild -> "_" + | P_id v -> string_of_id v + | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat + | P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")" + | _ -> "PAT" +and string_of_lexp (LEXP_aux (lexp, _)) = + match lexp with + | LEXP_id v -> string_of_id v + | LEXP_cast (typ, v) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_id v + | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" + | _ -> "LEXP" +and string_of_letbind (LB_aux (lb, l)) = + match lb with + | LB_val_implicit (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp + | LB_val_explicit (typschm, pat, exp) -> + string_of_typschm typschm ^ " " ^ string_of_pat pat ^ " = " ^ string_of_exp exp + +module Id = struct + type t = id + let compare id1 id2 = + match (id1, id2) with + | Id_aux (Id x, _), Id_aux (Id y, _) -> String.compare x y + | Id_aux (DeIid x, _), Id_aux (DeIid y, _) -> String.compare x y + | Id_aux (Id _, _), Id_aux (DeIid _, _) -> -1 + | Id_aux (DeIid _, _), Id_aux (Id _, _) -> 1 +end + +module Kid = struct + type t = kid + let compare kid1 kid2 = String.compare (string_of_kid kid1) (string_of_kid kid2) +end + +module Bindings = Map.Make(Id) +module KBindings = Map.Make(Kid) +module KidSet = Set.Make(Kid) + +module Env : sig + type t + val get_val_spec : id -> t -> typquant * typ + val add_val_spec : id -> typquant * typ -> t -> t + val get_local : id -> t -> typ + val add_local : id -> typ -> t -> t + val get_constraints : t -> n_constraint list + val add_constraint : n_constraint -> t -> t + val get_typ_var : kid -> t -> base_kind_aux + val add_typ_var : kid -> base_kind_aux -> t -> t + val get_ret_typ : t -> typ option + val add_ret_typ : typ -> t -> t + val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t + val get_typ_synonym : id -> t -> typ_arg list -> typ + val fresh_kid : t -> kid + val expand_synonyms : t -> typ -> typ + val empty : t +end = struct + type t = + { top_val_specs : (typquant * typ) Bindings.t; + locals : typ Bindings.t; + typ_vars : base_kind_aux KBindings.t; + typ_synonyms : (typ_arg list -> typ) Bindings.t; + constraints : n_constraint list; + ret_typ : typ option + } + + let empty = + { top_val_specs = Bindings.empty; + locals = Bindings.empty; + typ_vars = KBindings.empty; + typ_synonyms = Bindings.empty; + constraints = []; + ret_typ = None; + } + + let counter = ref 0 + + let get_val_spec id env = + try Bindings.find id env.top_val_specs with + | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) + + let add_val_spec id bind env = + if Bindings.mem id env.top_val_specs + then typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound") + else + begin + typ_debug ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind); + { env with top_val_specs = Bindings.add id bind env.top_val_specs } + end + + let get_local id env = + try Bindings.find id env.locals with + | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) + + let add_local id typ env = + begin + typ_print ("Adding local binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ); + { env with locals = Bindings.add id typ env.locals } + end + + let get_typ_var kid env = + try KBindings.find kid env.typ_vars with + | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) + + let add_typ_var kid k env = + if KBindings.mem kid env.typ_vars + then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound") + else + begin + typ_debug ("Adding kind identifier binding " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k); + { env with typ_vars = KBindings.add kid k env.typ_vars } + end + + let rec wf_nexp env (Nexp_aux (nexp, l)) = + match nexp with + | Nexp_id _ -> typ_error l "Unimplemented: Nexp_id" + | Nexp_var kid -> + begin + match get_typ_var kid env with + | BK_nat -> () + | kind -> typ_error l ("Constraint is badly formed, " + ^ string_of_kid kid ^ " has kind " + ^ string_of_base_kind_aux kind ^ " but should have kind Nat") + end + | Nexp_constant _ -> () + | Nexp_times (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2 + | Nexp_sum (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2 + | Nexp_minus (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2 + | Nexp_exp nexp -> wf_nexp env nexp (* MAYBE: Could put restrictions on what is allowed here *) + | Nexp_neg nexp -> wf_nexp env nexp + + let wf_constraint env (NC_aux (nc, _)) = + match nc with + | NC_fixed (n1, n2) -> wf_nexp env n1; wf_nexp env n2 + | NC_bounded_ge (n1, n2) -> wf_nexp env n1; wf_nexp env n2 + | NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2 + | NC_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *) + + let get_constraints env = env.constraints + + let add_constraint (NC_aux (_, l) as constr) env = + wf_constraint env constr; + begin + typ_debug ("Adding constraint " ^ string_of_n_constraint constr); + { env with constraints = constr :: env.constraints } + end + + let fresh_kid env = + let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter), Parse_ast.Unknown) in + incr counter; fresh + + let get_ret_typ env = env.ret_typ + + let add_ret_typ typ env = { env with ret_typ = Some typ } + + let add_typ_synonym id synonym env = + if Bindings.mem id env.typ_synonyms + then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists") + else + begin + typ_debug ("Adding typ synonym " ^ string_of_id id); + { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms } + end + + let get_typ_synonym id env = + try Bindings.find id env.typ_synonyms with + | Not_found -> typ_error (id_loc id) ("No type synonym " ^ string_of_id id) + + let rec expand_synonyms env (Typ_aux (typ, l)) = + match typ with + | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l) + | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l) + | Typ_app (id, args) -> + begin + try + let synonym = Bindings.find id env.typ_synonyms in + expand_synonyms env (synonym args) + with + | Not_found -> Typ_aux (Typ_app (id, List.map (expand_synonyms_arg env) args), l) + end + | typ -> Typ_aux (typ, l) + and expand_synonyms_arg env (Typ_arg_aux (typ_arg, l)) = + match typ_arg with + | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (expand_synonyms env typ), l) + | arg -> Typ_arg_aux (arg, l) + +end + +type tannot = (Env.t * typ) option + +let add_typquant (quant : typquant) (env : Env.t) : Env.t = + let rec add_quant_item env = function + | QI_aux (qi, _) -> add_quant_item_aux env qi + and add_quant_item_aux env = function + | QI_const constr -> Env.add_constraint constr env + | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var kid BK_nat env + | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var kid k env + | QI_id (KOpt_aux (_, l)) -> typ_error l "Type variable had non base kinds!" + in + match quant with + | TypQ_aux (TypQ_no_forall, _) -> env + | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants + +let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown) +let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) +let mk_id str = Id_aux (Id str, Parse_ast.Unknown) + +let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown) +let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown) +let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown) + +type index_sort = + | IS_int + | IS_prop of kid * (nexp * nexp) list + +type tnf = + | Tnf_wild + | Tnf_id of id + | Tnf_var of kid + | Tnf_tup of tnf list + | Tnf_index_sort of index_sort + | Tnf_app of id * tnf_arg list +and tnf_arg = + | Tnf_arg_nexp of nexp + | Tnf_arg_typ of tnf + | Tnf_arg_order of order + | Tnf_arg_effect of effect + +let rec string_of_tnf = function + | Tnf_wild -> "_" + | Tnf_id id -> string_of_id id + | Tnf_var kid -> string_of_kid kid + | Tnf_tup tnfs -> "(" ^ string_of_list ", " string_of_tnf tnfs ^ ")" + | Tnf_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_tnf_arg args ^ ">" + | Tnf_index_sort IS_int -> "INT" + | Tnf_index_sort (IS_prop (kid, props)) -> + "{" ^ string_of_kid kid ^ " | " ^ string_of_list " & " (fun (n1, n2) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2) props ^ "}" +and string_of_tnf_arg = function + | Tnf_arg_nexp n -> string_of_nexp n + | Tnf_arg_typ tnf -> string_of_tnf tnf + | Tnf_arg_order o -> string_of_order o + | Tnf_arg_effect eff -> string_of_effect eff + +let rec normalize_typ env (Typ_aux (typ, l)) = + match typ with + | Typ_wild -> Tnf_wild + | Typ_id (Id_aux (Id "int", _)) -> Tnf_index_sort IS_int + | Typ_id (Id_aux (Id "nat", _)) -> + let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(nconstant 0, nvar kid)])) + | Typ_id v -> Tnf_id v + | Typ_var kid -> Tnf_var kid + | Typ_tup typs -> Tnf_tup (List.map (normalize_typ env) typs) + | Typ_app (Id_aux (Id "range", _), [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)]) -> + let kid = Env.fresh_kid env in + Tnf_index_sort (IS_prop (kid, [(n1, nvar kid); (nvar kid, n2)])) + | Typ_app (id, args) -> normalize_typ env (Env.get_typ_synonym id env args) + | Typ_fn _ -> typ_error l ("Cannot normalize function type " ^ string_of_typ (Typ_aux (typ, l))) +and normalize_typ_arg env (Typ_arg_aux (typ_arg, _)) = + match typ_arg with + | Typ_arg_nexp n -> Tnf_arg_nexp n + | Typ_arg_typ typ -> Tnf_arg_typ (normalize_typ env typ) + | Typ_arg_order o -> Tnf_arg_order o + | Typ_arg_effect e -> Tnf_arg_effect e + +(* Here's how the constraint generation works for subtyping + +X(b,c...) --> {a. Y(a,b,c...)} \subseteq {a. Z(a,b,c...)} + +this is equivalent to + +\forall b c. X(b,c) --> \forall a. Y(a,b,c) --> Z(a,b,c) + +\forall b c. X(b,c) --> \forall a. !Y(a,b,c) \/ !Z^-1(a,b,c) + +\forall b c. X(b,c) --> !\exists a. Y(a,b,c) /\ Z^-1(a,b,c) + +\forall b c. !X(b,c) \/ !\exists a. Y(a,b,c) /\ Z^-1(a,b,c) + +!\exists b c. X(b,c) /\ \exists a. Y(a,b,c) /\ Z^-1(a,b,c) + +!\exists a b c. X(b,c) /\ Y(a,b,c) /\ Z^-1(a,b,c) + +which is then a problem we can feed to the constraint solver expecting unsat. + *) + +let unaux_nexp (Nexp_aux (nexp, _)) = nexp + +let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l) +and nexp_subst_aux sv subst = function + | Nexp_id v -> Nexp_id v + | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid + | Nexp_constant c -> Nexp_constant c + | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) + | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) + | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) + | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp) + | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp) + +let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l) +and nc_subst_nexp_aux l sv subst = function + | NC_fixed (n1, n2) -> NC_fixed (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_nat_set_bounded (kid, ints) as set_nc -> + if compare kid sv = 0 + then typ_error l ("Cannot substitute " ^ string_of_kid sv ^ " into set constraint " ^ string_of_n_constraint (NC_aux (set_nc, l))) + else set_nc + +let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l) +and typ_subst_nexp_aux sv subst = function + | Typ_wild -> Typ_wild + | Typ_id v -> Typ_id v + | Typ_var kid -> Typ_var kid + | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2, effs) + | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs) + | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args) +and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l) +and typ_subst_arg_nexp_aux sv subst = function + | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp) + | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ) + | Typ_arg_order o -> Typ_arg_order o + | Typ_arg_effect eff -> Typ_arg_effect eff + +let rec props_subst sv subst props = + match props with + | [] -> [] + | ((nexp1, nexp2) :: props) -> (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) :: props_subst sv subst props + +let rec nexp_constraint var_of (Nexp_aux (nexp, l)) = + match nexp with + | Nexp_id v -> typ_error l "Unimplemented: Cannot generate constraint from Nexp_id" + | Nexp_var kid -> Constraint.variable (var_of kid) + | Nexp_constant c -> Constraint.constant (big_int_of_int c) + | Nexp_times (nexp1, nexp2) -> Constraint.mult (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | Nexp_sum (nexp1, nexp2) -> Constraint.add (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | Nexp_minus (nexp1, nexp2) -> Constraint.sub (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | Nexp_exp nexp -> Constraint.pow2 (nexp_constraint var_of nexp) + | Nexp_neg nexp -> Constraint.sub (Constraint.constant (big_int_of_int 0)) (nexp_constraint var_of nexp) + +let nc_constraint var_of (NC_aux (nc, _)) = + match nc with + | NC_fixed (nexp1, nexp2) -> Constraint.eq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | NC_bounded_ge (nexp1, nexp2) -> Constraint.gteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | NC_bounded_le (nexp1, nexp2) -> Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | NC_nat_set_bounded (_, []) -> Constraint.literal false + | NC_nat_set_bounded (kid, (int :: ints)) -> + List.fold_left Constraint.disj + (Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int int))) + (List.map (fun i -> Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int i))) ints) + +let rec nc_constraints var_of ncs = + match ncs with + | [] -> Constraint.literal true + | [nc] -> nc_constraint var_of nc + | (nc :: ncs) -> + Constraint.conj (nc_constraint var_of nc) (nc_constraints var_of ncs) + +let prove env nc = + typ_print ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc); + let module Bindings = Map.Make(Kid) in + let bindings = ref Bindings.empty in + let fresh_var kid = + let n = Bindings.cardinal !bindings in + bindings := Bindings.add kid n !bindings; + n + in + let var_of kid = + try Bindings.find kid !bindings with + | Not_found -> fresh_var kid + in + let constr = Constraint.conj (nc_constraints var_of (Env.get_constraints env)) (Constraint.negate (nc_constraint var_of nc)) in + match Constraint.call_z3 constr with + | Constraint.Unsat _ -> typ_debug "unsat"; true + | Constraint.Unknown [] -> typ_debug "sat"; false + | Constraint.Unknown _ -> typ_debug "unknown"; false + +let rec subtyp_tnf env tnf1 tnf2 = + typ_print ("Subset " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_tnf tnf1 ^ " " ^ string_of_tnf tnf2); + let module Bindings = Map.Make(Kid) in + let bindings = ref Bindings.empty in + let fresh_var kid = + let n = Bindings.cardinal !bindings in + bindings := Bindings.add kid n !bindings; + n + in + let var_of kid = + try Bindings.find kid !bindings with + | Not_found -> fresh_var kid + in + let rec neg_props props = + match props with + | [] -> Constraint.literal false + | [(nexp1, nexp2)] -> Constraint.gt (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | ((nexp1, nexp2) :: props) -> + Constraint.disj (Constraint.gt (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)) (neg_props props) + in + let rec pos_props props = + match props with + | [] -> Constraint.literal true + | [(nexp1, nexp2)] -> Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) + | ((nexp1, nexp2) :: props) -> + Constraint.conj (Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)) (pos_props props) + in + match (tnf1, tnf2) with + | Tnf_wild, Tnf_wild -> true + | Tnf_id v1, Tnf_id v2 -> Id.compare v1 v2 = 0 + | Tnf_var kid1, Tnf_var kid2 -> Kid.compare kid1 kid2 = 0 + | Tnf_tup tnfs1, Tnf_tup tnfs2 -> + begin + try List.for_all2 (subtyp_tnf env) tnfs1 tnfs2 with + | Invalid_argument _ -> false + end + | Tnf_app (v1, args1), Tnf_app (v2, args2) -> Id.compare v1 v2 = 0 && List.for_all2 (tnf_args_eq env) args1 args2 + | Tnf_index_sort IS_int, Tnf_index_sort IS_int -> true + | Tnf_index_sort (IS_prop _), Tnf_index_sort IS_int -> true + | Tnf_index_sort (IS_prop (kid1, prop1)), Tnf_index_sort (IS_prop (kid2, prop2)) -> + begin + let kid3 = Env.fresh_kid env in + let (prop1, prop2) = props_subst kid1 (Nexp_var kid3) prop1, props_subst kid2 (Nexp_var kid3) prop2 in + let constr = Constraint.conj (nc_constraints var_of (Env.get_constraints env)) (Constraint.conj (pos_props prop1) (neg_props prop2)) in + match Constraint.call_z3 constr with + | Constraint.Unsat _ -> typ_debug "unsat"; true + | Constraint.Unknown [] -> typ_debug "sat"; false + | Constraint.Unknown _ -> typ_debug "unknown"; false + end + | _, _ -> false + +and tnf_args_eq env arg1 arg2 = true + +let subtyp l env typ1 typ2 = + if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2) + then () + else typ_error l (string_of_typ typ1 + ^ " is not a subtype of " ^ string_of_typ typ2 + ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)) + +let rec nexp_frees (Nexp_aux (nexp, l)) = + match nexp with + | Nexp_id _ -> typ_error l "Unimplemented Nexp_id in nexp_frees" + | Nexp_var kid -> KidSet.singleton kid + | Nexp_constant _ -> KidSet.empty + | Nexp_times (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2) + | Nexp_sum (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2) + | Nexp_minus (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2) + | Nexp_exp n -> nexp_frees n + | Nexp_neg n -> nexp_frees n + +let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) = + match nexp1, nexp2 with + | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 = 0 + | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 = 0 + | Nexp_constant c1, Nexp_constant c2 -> c1 = c2 + | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | Nexp_exp n1, Nexp_exp n2 -> nexp_identical n1 n2 + | Nexp_neg n1, Nexp_neg n2 -> nexp_identical n1 n2 + | _, _ -> false + +let rec unify_nexps l (Nexp_aux (nexp_aux1, _) as nexp1) nexp2 = + typ_debug ("UNIFYING NEXPS " ^ string_of_nexp nexp1 ^ " AND " ^ string_of_nexp nexp2); + match nexp_aux1 with + | Nexp_id v -> typ_error l "Unimplemented Nexp_id in unify nexp" + | Nexp_var kid -> (kid, nexp2) + | Nexp_sum (n1a, n1b) -> + if KidSet.is_empty (nexp_frees n1b) + then unify_nexps l n1a (nminus nexp2 n1b) + else + if KidSet.is_empty (nexp_frees n1a) + then unify_nexps l n1b (nminus nexp2 n1a) + else typ_error l ("Both sides of Nat expression " ^ string_of_nexp nexp1 + ^ " contain free type variables so it cannot be unified with " ^ string_of_nexp nexp2) + | _ -> typ_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + +let unify l env typ1 typ2 = + let merge_unifiers l kid nexp1 nexp2 = + match nexp1, nexp2 with + | Some n1, Some n2 -> + if nexp_identical n1 n2 then Some n1 + else typ_error l ("Multiple non-identical unifiers for " ^ string_of_kid kid + ^ ": " ^ string_of_nexp n1 ^ " and " ^ string_of_nexp n2) + | None, Some n2 -> Some n2 + | Some n1, None -> Some n1 + | None, None -> None + in + let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) = + typ_debug ("UNIFYING: " ^ string_of_typ typ1 ^ " AND " ^ string_of_typ typ2); + match typ1_aux, typ2_aux with + | Typ_wild, Typ_wild -> KBindings.empty + | Typ_id v1, Typ_id v2 -> + if compare v1 v2 = 0 then KBindings.empty + else typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) + | Typ_var _, Typ_var _ -> typ_error l "Raw identifiers during unification" + | Typ_tup typs1, Typ_tup typs2 -> + begin + try List.fold_left (KBindings.merge (merge_unifiers l)) KBindings.empty (List.map2 (unify_typ l) typs1 typs2) with + | Invalid_argument _ -> typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2 + ^ " tuple type is of different length") + end + | Typ_app (f1, args1), Typ_app (f2, args2) -> + begin + if Id.compare f1 f2 = 0 + then + try List.fold_left (KBindings.merge (merge_unifiers l)) KBindings.empty (List.map2 (unify_typ_args l) args1 args2) with + | Invalid_argument _ -> typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2 + ^ " functions applied to different number of arguments") + else typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) + end + | _, _ -> typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) + and unify_typ_args l (Typ_arg_aux (typ_arg_aux1, _) as typ_arg1) (Typ_arg_aux (typ_arg_aux2, _) as typ_arg2) = + match typ_arg_aux1, typ_arg_aux2 with + | Typ_arg_nexp n1, Typ_arg_nexp n2 -> let (kid, unifier) = unify_nexps l n1 n2 in KBindings.singleton kid unifier + | Typ_arg_typ typ1, Typ_arg_typ typ2 -> unify_typ l typ1 typ2 + | Typ_arg_order _, Typ_arg_order _ -> assert false (* FIXME *) + | Typ_arg_effect _, Typ_arg_effect _ -> assert false + | _, _ -> typ_error l (string_of_typ_arg typ_arg1 ^ " cannot be unified with type argument " ^ string_of_typ_arg typ_arg2) + in + let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in + unify_typ l typ1 typ2 + +let infer_lit env (L_aux (lit_aux, l) as lit) = + match lit_aux with + | L_unit -> mk_typ (Typ_id (mk_id "unit")) + | L_zero -> mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nconstant 0))])) + | L_one -> mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nconstant 1))])) + | L_num n -> mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nconstant n))])) + | _ -> typ_error l ("Unimplemented literal " ^ string_of_lit lit) + +let rec bind_pat env (P_aux (pat_aux, (l, _)) as pat) (Typ_aux (typ_aux, _) as typ) = + let annot_pat pat typ = P_aux (pat, (l, Some (env, typ))) in + match pat_aux with + | P_id v -> annot_pat (P_id v) typ, Env.add_local v typ env + | P_wild -> annot_pat P_wild typ, env + | P_typ (typ_annot, pat) -> + begin + subtyp l env typ_annot typ; + let (typed_pat, env) = bind_pat env pat typ_annot in + annot_pat (P_typ (typ_annot, typed_pat)) typ, env + end + | P_tup pats -> + begin + match typ_aux with + | Typ_tup typs -> + let bind_tuple_pat (tpats, env) pat typ = + let tpat, env = bind_pat env pat typ in tpat :: tpats, env + in + let tpats, env = + try List.fold_left2 bind_tuple_pat ([], env) pats typs with + | Invalid_argument _ -> typ_error l "Tuple pattern and tuple type have different length" + in + annot_pat (P_tup tpats) typ, env + | _ -> typ_error l "Cannot bind tuple pattern against non tuple type" + end + | P_lit lit -> + begin + let lit_typ = infer_lit env lit in + subtyp l env lit_typ typ; + annot_pat (P_lit lit) typ, env + end + | _ -> typ_error l ("Unhandled pat " ^ string_of_pat pat) + +and bind_lexp env (LEXP_aux (lexp_aux, (l, _))) typ = + let annot_lexp lexp typ = LEXP_aux (lexp, (l, Some (env, typ))) in + match lexp_aux with + | LEXP_id v -> annot_lexp (LEXP_id v) typ, Env.add_local v typ env + | LEXP_cast (typ_annot, v) -> + begin + subtyp l env typ typ_annot; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v typ_annot env + end + | LEXP_tup lexps -> + begin + let (Typ_aux (typ_aux, _)) = typ in + match typ_aux with + | Typ_tup typs -> + let bind_tuple_lexp (tlexps, env) lexp typ = + let tlexp, env = bind_lexp env lexp typ in tlexp :: tlexps, env + in + let tlexps, env = + try List.fold_left2 bind_tuple_lexp ([], env) lexps typs with + | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length" + in + annot_lexp (LEXP_tup tlexps) typ, env + | _ -> typ_error l "Cannot bind tuple l-expression against non tuple type" + end + | _ -> typ_error l ("Unhandled l-expression") + +let quant_items = function + | TypQ_aux (TypQ_tq qis, _) -> qis + | TypQ_aux (TypQ_no_forall, _) -> [] + +let is_nat_kid kid = function + | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0 + | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), kid'), _) -> Kid.compare kid kid' = 0 + | _ -> false + +let typ_of (E_aux (_, (_, tannot))) = match tannot with + | Some (_, typ) -> typ + | None -> assert false + +let crule r env exp typ = + incr depth; + typ_print ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ); + let checked_exp = r env exp typ in + decr depth; checked_exp + +let irule r env exp = + incr depth; + let inferred_exp = r env exp in + typ_print ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp)); + decr depth; + inferred_exp + +let rec check_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) (Typ_aux (typ_aux, _) as typ) : tannot exp = + let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in + match (exp_aux, typ_aux) with + | E_block exps, _ -> + begin + let rec check_block l env exps typ = match exps with + | [] -> typ_error l "Empty block found" + | [exp] -> [crule check_exp env exp typ] + | (E_aux (E_assign (lexp, bind), _) :: exps) -> + let texp, env = bind_assignment env lexp bind in + texp :: check_block l env exps typ + | (exp :: exps) -> + let texp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in + texp :: check_block l env exps typ + in + annot_exp (E_block (check_block l env exps typ)) typ + end + | E_case (exp, cases), _ -> + let inferred_exp = irule infer_exp env exp in + let check_case (Pat_aux (Pat_exp (pat, case), (l, _))) typ = + let tpat, env = bind_pat env pat (typ_of inferred_exp) in + Pat_aux (Pat_exp (tpat, crule check_exp env case typ), (l, None)) + in + annot_exp (E_case (inferred_exp, List.map (fun case -> check_case case typ) cases)) typ + | E_let (LB_aux (letbind, (let_loc, _)), exp), _ -> + begin + match letbind with + | LB_val_explicit (typschm, pat, bind) -> assert false + | LB_val_implicit (pat, bind) -> + let inferred_bind = irule infer_exp env bind in + let tpat, env = bind_pat env pat (typ_of inferred_bind) in + annot_exp (E_let (LB_aux (LB_val_implicit (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ + end + | _, _ -> + let inferred_exp = irule infer_exp env exp + in (subtyp l env (typ_of inferred_exp) typ; inferred_exp) + +and bind_assignment env lexp (E_aux (_, (l, _)) as exp) = + let inferred_exp = irule infer_exp env exp in + let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in + E_aux (E_assign (tlexp, inferred_exp), (l, Some (env, mk_typ (Typ_id (mk_id "unit"))))), env' + +and infer_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) : tannot exp = + let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in + match exp_aux with + | E_id v -> annot_exp (E_id v) (Env.get_local v env) + | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit) + | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)]))) + | E_return exp -> + begin + match Env.get_ret_typ env with + | Some typ -> annot_exp (E_return (crule check_exp env exp typ)) (mk_typ (Typ_id (mk_id "unit"))) + | None -> typ_error l "Return found in non-function environment" + end + | E_tuple exps -> + let inferred_exps = List.map (irule infer_exp env) exps in + annot_exp (E_tuple inferred_exps) (mk_typ (Typ_tup (List.map typ_of inferred_exps))) + | E_assign (lexp, bind) -> + fst (bind_assignment env lexp bind) + | E_cast (typ, exp) -> + let checked_exp = check_exp env exp typ in + annot_exp (E_cast (typ, checked_exp)) typ + | E_app (f, xs) -> + begin + let rec instantiate_quants quants kid nexp = match quants with + | [] -> [] + | ((QI_aux (QI_id kinded_id, _) as quant) :: quants) -> + if is_nat_kid kid kinded_id then instantiate_quants quants kid nexp else quant :: instantiate_quants quants kid nexp + | ((QI_aux (QI_const nc, l)) :: quants) -> + QI_aux (QI_const (nc_subst_nexp kid (unaux_nexp nexp) nc), l) :: quants + in + let solve_quant = function + | QI_aux (QI_id _, _) -> false + | QI_aux (QI_const nc, _) -> prove env nc + in + let rec instantiate quants typs ret_typ args = + match quants, typs, args with + | [], [], [] -> ([], ret_typ) + | _, [], [] -> + if List.for_all solve_quant quants + then ([], ret_typ) + else typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants + ^ " not resolved during function application of " ^ string_of_id f) + | _, [], _ -> typ_error l ("Function " ^ string_of_id f ^ " applied to too many arguments") + | _, _, [] -> typ_error l ("Function " ^ string_of_id f ^ " not applied to not enough arguments") + | _, (typ :: typs), (arg :: args) -> + begin + typ_debug ("INSTANTIATE: " ^ string_of_exp arg ^ " with " ^ string_of_typ typ ^ " NF " ^ string_of_tnf (normalize_typ env typ)); + let iarg = irule infer_exp env arg in + typ_debug ("INFER: " ^ string_of_exp arg ^ " type " ^ string_of_typ (typ_of iarg) ^ " NF " ^ string_of_tnf (normalize_typ env (typ_of iarg))); + let unifiers = unify l env typ (typ_of iarg) in + typ_debug (string_of_list ", " (fun (kid, nexp) -> string_of_kid kid ^ " => " ^ string_of_nexp nexp) (KBindings.bindings unifiers)); + let typs' = List.map (fun typ -> List.fold_left (fun typ (kid, nexp) -> typ_subst_nexp kid (unaux_nexp nexp) typ) + typ + (KBindings.bindings unifiers)) typs in + let quants' = List.fold_left (fun qs (kid, nexp) -> instantiate_quants qs kid nexp) quants (KBindings.bindings unifiers) in + let ret_typ' = List.fold_left (fun typ (kid, nexp) -> typ_subst_nexp kid (unaux_nexp nexp) typ) ret_typ (KBindings.bindings unifiers) in + let (iargs, ret_typ'') = instantiate quants' typs' ret_typ' args in + (iarg :: iargs, ret_typ'') + end + in + let (typq, f_typ) = Env.get_val_spec f env in + match f_typ with + | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, effs), _) -> + let (xs, typ_ret) = instantiate (quant_items typq) typ_args typ_ret xs in + annot_exp (E_app (f, xs)) typ_ret + | Typ_aux (Typ_fn (typ_arg, typ_ret, effs), _) -> + let (xs, typ_ret) = instantiate (quant_items typq) [typ_arg] typ_ret xs in + annot_exp (E_app (f, xs)) typ_ret + | _ -> typ_error l (string_of_id f ^ " is not a function") + end + | _ -> typ_error l "Unimplemented" + +let check_funcl env (FCL_aux (FCL_Funcl (id, pat, exp), (l, _))) typ = + match typ with + | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) -> + begin + let typed_pat, env = bind_pat env pat typ_arg in + let env = Env.add_ret_typ typ_ret env in + let exp = crule check_exp env exp typ_ret in + FCL_aux (FCL_Funcl (id, typed_pat, exp), (l, Some (env, typ))) + end + | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type") + +let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux : 'a fundef) : tannot def = + let (Typ_annot_opt_aux (Typ_annot_opt_some (annot_quant, annot_typ1), _)) = tannotopt in + let id = + match (List.fold_right + (fun (FCL_aux (FCL_Funcl (id, _, _), _)) id' -> + match id' with + | Some id' -> if string_of_id id' = string_of_id id then Some id' + else typ_error l ("Function declaration expects all definitions to have the same name, " + ^ string_of_id id ^ " differs from other definitions of " ^ string_of_id id') + | None -> Some id) funcls None) + with + | Some id -> id + | None -> typ_error l "funcl list is empty" + in + typ_print ("\nChecking function " ^ string_of_id id); + let (quant, typ) = Env.get_val_spec id env in + typ_debug ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ)); + typ_debug ("Annotation typ " ^ string_of_bind (annot_quant, annot_typ1)); + let funcl_env = add_typquant quant env in + let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in + DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, None))) + +(* Checking a val spec simply adds the type as a binding in the + context. We have to destructure the various kinds of val specs, but + the difference is irrelvant for the typechecker. *) +let check_val_spec env (VS_aux (vs, (l, _))) = + let (id, quants, typ) = match vs with + | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ) + | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ) + | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, _) -> (id, quants, typ) in + DEF_spec (VS_aux (vs, (l, None))), Env.add_val_spec id (quants, typ) env + +let rec check_def env def = + let cd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Case") in + match def with + | DEF_kind kdef -> cd_err () + | DEF_type tdef -> cd_err () + | DEF_fundef fdef -> check_fundef env fdef, env + | DEF_val letdef -> cd_err () + | DEF_spec vs -> check_val_spec env vs + | DEF_default default -> cd_err () + | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> cd_err () + | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) -> cd_err () + | DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) -> cd_err () + | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker") + | DEF_comm (DC_comm str) -> DEF_comm (DC_comm str), env + | DEF_comm (DC_comm_struct def) -> + let def, env = check_def env def + in DEF_comm (DC_comm_struct def), env + +let rec check env (Defs defs) = + match defs with + | [] -> (Defs []), env + | def :: defs -> + let (def, env) = check_def env def in + let (Defs defs, env) = check env (Defs defs) in + (Defs (def::defs)), env + +let initial_env = + Env.empty + |> Env.add_typ_synonym (mk_id "atom") (fun args -> mk_typ (Typ_app (mk_id "range", args @ args))) diff --git a/src/type_check_new.mli b/src/type_check_new.mli new file mode 100644 index 00000000..98e1171e --- /dev/null +++ b/src/type_check_new.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 *) +(* *) +(* 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 + +module Env : sig + type t + val get_val_spec : id -> t -> typquant * typ + val add_val_spec : id -> typquant * typ -> t -> t + val get_local : id -> t -> typ + val add_local : id -> typ -> t -> t + val get_constraints : t -> n_constraint list + val add_constraint : n_constraint -> t -> t + val get_typ_var : kid -> t -> base_kind_aux + val add_typ_var : kid -> base_kind_aux -> t -> t + val get_ret_typ : t -> typ option + val add_ret_typ : typ -> t -> t + val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t + val get_typ_synonym : id -> t -> typ_arg list -> typ + val fresh_kid : t -> kid + val expand_synonyms : t -> typ -> typ + val empty : t +end + +type tannot = (Env.t * typ) option + +val check : Env.t -> 'a defs -> tannot defs * Env.t + +val initial_env : Env.t diff --git a/test/typecheck/fail/assignment_simple1.sail b/test/typecheck/fail/assignment_simple1.sail new file mode 100644 index 00000000..1ad9f8bf --- /dev/null +++ b/test/typecheck/fail/assignment_simple1.sail @@ -0,0 +1,16 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + z := 9; + z +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple2.sail b/test/typecheck/fail/assignment_simple2.sail new file mode 100644 index 00000000..db45bbcf --- /dev/null +++ b/test/typecheck/fail/assignment_simple2.sail @@ -0,0 +1,15 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + f(z, z := 10) +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple3.sail b/test/typecheck/fail/assignment_simple3.sail new file mode 100644 index 00000000..2a596c29 --- /dev/null +++ b/test/typecheck/fail/assignment_simple3.sail @@ -0,0 +1,15 @@ + +val (unit, [:10:]) -> [:10:] effect pure f + +function [:10:] f (x, y) = y + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + f(z := 10, z) +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/case_simple1.sail b/test/typecheck/fail/case_simple1.sail new file mode 100644 index 00000000..471c3565 --- /dev/null +++ b/test/typecheck/fail/case_simple1.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> x + } +} diff --git a/test/typecheck/fail/cast_lexp1.sail b/test/typecheck/fail/cast_lexp1.sail new file mode 100644 index 00000000..dad4c84c --- /dev/null +++ b/test/typecheck/fail/cast_lexp1.sail @@ -0,0 +1,7 @@ + +val unit -> nat effect pure test + +function nat test () = { + (int) y := 10; + y +} diff --git a/test/typecheck/fail/cast_simple.sail b/test/typecheck/fail/cast_simple.sail new file mode 100644 index 00000000..19768fbe --- /dev/null +++ b/test/typecheck/fail/cast_simple.sail @@ -0,0 +1,7 @@ + +val unit -> nat effect pure test + +function nat test () = { + (int) y := ([|0:10|]) 10; + (nat) y +} diff --git a/test/typecheck/fail/fun_simple_constraints1.sail b/test/typecheck/fail/fun_simple_constraints1.sail new file mode 100644 index 00000000..979e0cdf --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints1.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:64|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints2.sail b/test/typecheck/fail/fun_simple_constraints2.sail new file mode 100644 index 00000000..43a0b6d7 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints2.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(9) diff --git a/test/typecheck/fail/fun_simple_constraints3.sail b/test/typecheck/fail/fun_simple_constraints3.sail new file mode 100644 index 00000000..098054e4 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints3.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(plus(sizeof 'N, 1)) diff --git a/test/typecheck/fail/fun_simple_constraints4.sail b/test/typecheck/fail/fun_simple_constraints4.sail new file mode 100644 index 00000000..07b8c596 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints4.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-54)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints5.sail b/test/typecheck/fail/fun_simple_constraints5.sail new file mode 100644 index 00000000..7e28db85 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints5.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-9)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints6.sail b/test/typecheck/fail/fun_simple_constraints6.sail new file mode 100644 index 00000000..6dc5e0e6 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints6.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'k, Nat 'm. ([:'n + 'k:], [:'m:]) -> [:'n + 'k + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints7.sail b/test/typecheck/fail/fun_simple_constraints7.sail new file mode 100644 index 00000000..00d2a172 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints7.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|11:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints8.sail b/test/typecheck/fail/fun_simple_constraints8.sail new file mode 100644 index 00000000..e4c02da0 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints8.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|11:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/return_simple1.sail b/test/typecheck/fail/return_simple1.sail new file mode 100644 index 00000000..1bbc0e73 --- /dev/null +++ b/test/typecheck/fail/return_simple1.sail @@ -0,0 +1,7 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x +} diff --git a/test/typecheck/fail/return_simple2.sail b/test/typecheck/fail/return_simple2.sail new file mode 100644 index 00000000..f212a945 --- /dev/null +++ b/test/typecheck/fail/return_simple2.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + x; + return x; + x +} diff --git a/test/typecheck/fail/return_simple3.sail b/test/typecheck/fail/return_simple3.sail new file mode 100644 index 00000000..df75c5bd --- /dev/null +++ b/test/typecheck/fail/return_simple3.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return 9; + x +} diff --git a/test/typecheck/fail/return_simple4.sail b/test/typecheck/fail/return_simple4.sail new file mode 100644 index 00000000..aa7c3010 --- /dev/null +++ b/test/typecheck/fail/return_simple4.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + 9 +} diff --git a/test/typecheck/fail/return_simple5.sail b/test/typecheck/fail/return_simple5.sail new file mode 100644 index 00000000..d6947d91 --- /dev/null +++ b/test/typecheck/fail/return_simple5.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N - 1|] -> [|10:'N - 1|] effect pure return_test + +function forall Nat 'N. [|10:'N - 1|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/fail/return_simple6.sail b/test/typecheck/fail/return_simple6.sail new file mode 100644 index 00000000..0e118632 --- /dev/null +++ b/test/typecheck/fail/return_simple6.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/pass/assignment_simple.sail b/test/typecheck/pass/assignment_simple.sail new file mode 100644 index 00000000..dc0c78d8 --- /dev/null +++ b/test/typecheck/pass/assignment_simple.sail @@ -0,0 +1,16 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + z := 10; + z +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10
\ No newline at end of file diff --git a/test/typecheck/pass/case_simple1.sail b/test/typecheck/pass/case_simple1.sail new file mode 100644 index 00000000..e4a81a36 --- /dev/null +++ b/test/typecheck/pass/case_simple1.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> y + } +} diff --git a/test/typecheck/pass/case_simple2.sail b/test/typecheck/pass/case_simple2.sail new file mode 100644 index 00000000..0ffba780 --- /dev/null +++ b/test/typecheck/pass/case_simple2.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N, 'N >= 10. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> x + } +} diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail new file mode 100644 index 00000000..f1b87235 --- /dev/null +++ b/test/typecheck/pass/case_simple_constraints.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + switch x { + case ([|10:30|]) y -> y + case ([:31:]) _ -> sizeof 'N + case ([|31:40|]) _ -> plus(60,3) + } +} +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/pass/cast_lexp1.sail b/test/typecheck/pass/cast_lexp1.sail new file mode 100644 index 00000000..b8b29b87 --- /dev/null +++ b/test/typecheck/pass/cast_lexp1.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (int) y := 10; + y +} diff --git a/test/typecheck/pass/cast_lexp2].sail b/test/typecheck/pass/cast_lexp2].sail new file mode 100644 index 00000000..a6f6d299 --- /dev/null +++ b/test/typecheck/pass/cast_lexp2].sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (nat) y := 10; + y +} diff --git a/test/typecheck/pass/cast_simple.sail b/test/typecheck/pass/cast_simple.sail new file mode 100644 index 00000000..c1507f26 --- /dev/null +++ b/test/typecheck/pass/cast_simple.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (nat) y := ([|0:10|]) 10; + (int) y +} diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail new file mode 100644 index 00000000..7fd502b0 --- /dev/null +++ b/test/typecheck/pass/fun_simple_constraints1.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N)
\ No newline at end of file diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail new file mode 100644 index 00000000..338ef8e8 --- /dev/null +++ b/test/typecheck/pass/fun_simple_constraints2.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [|'n:'n|] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/pass/return_simple1.sail b/test/typecheck/pass/return_simple1.sail new file mode 100644 index 00000000..26e6fc1d --- /dev/null +++ b/test/typecheck/pass/return_simple1.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + x +} diff --git a/test/typecheck/pass/return_simple2.sail b/test/typecheck/pass/return_simple2.sail new file mode 100644 index 00000000..06ce9757 --- /dev/null +++ b/test/typecheck/pass/return_simple2.sail @@ -0,0 +1,11 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + return x; + return x; + return x; + x +} diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail new file mode 100644 index 00000000..7e81b5b2 --- /dev/null +++ b/test/typecheck/pass/return_simple3.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N, 'N >= 10. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N, 'N >= 10. [|10:'N|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh new file mode 100755 index 00000000..49739b5a --- /dev/null +++ b/test/typecheck/run_tests.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + +for i in `ls $DIR/pass/`; +do + printf "testing $i expecting pass: " + if $DIR/../../sail $1 $DIR/pass/$i 2> /dev/null; + then + printf "${GREEN}pass${NC}\n" + else + printf "${RED}fail${NC}\n" + fi +done + +for i in `ls $DIR/fail/`; +do + printf "testing $i expecting fail: " + if $DIR/../../sail $1 $DIR/fail/$i 2> /dev/null; + then + printf "${RED}pass${NC}\n" + else + printf "${GREEN}fail${NC}\n" + fi +done |