From 599930a7256340c9ecb6d872c82a487149ee551e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 15 Nov 2017 16:54:48 +0000 Subject: Allow user defined operations in nexps (experimental) There are several key changes here: 1) This commit allows for user defined operations in n-expressions using the Nexp_app constructor. These operations are linked to operators in the SMT solver, by using the smt extern when defining operations. Notably, this allows integer division and modular arithmetic to be used in types. This is best demonstrated with an example: infixl 7 / infixl 7 % val operator / = { smt: "div", ocaml: "quotient" } : forall 'n 'm, 'm != 0. (atom('n), atom('m)) -> {'o, 'o = 'n / 'm. atom('o)} val mod_atom = { smt: "mod", ocaml: "modulus" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod_atom('n, 'm). atom('o)} val "print_int" : (string, int) -> unit overload operator % = mod_atom val main : unit -> unit function main () = { let 'm : {'x, 'x % 3 = 1. atom('x)} = 4; let 'n = m / 3; _prove(constraint(('m - 1) % 3 = 0)); _prove(constraint('n * 3 + 1 = 'm)); (* let x = 3 / 0; (* Will fail *) *) print_int("n = ", n); () } As can be seen, these nexp ops can be arbitrary user defined operators and even operator overloading works (although there are some caveats). This feature is very experimental, and some things won't work very well once you use custom operators - notably unification. However, this not necissarily a downside, because if restrict yourself to the subset of sail types that correspond to liquid types, then there is never a need to unify n-expressions. Looking further ahead, if we switch to a liquid type system a la minisail, then we no longer need to treat + - and * specially in n-expressions. So possible future refactorings could involve collapsing the Nexp datatype. 2) The typechecker is stricter about valspecs (and other types) being well-formed. This is a breaking change because previously we allowed things like: val f : atom('n) -> atom('n) and now this must be val f : forall 'n. atom('n) -> atom('n) if we want to allow the first syntax, then initial-check should desugar it this way - but it must be well-formed by the time it hits the type-checker, otherwise it's not clear that we do the right thing. Note we can actually have top-level type variables by using top-level let bindings with P_var. There's a future line of refactoring that would make it so that type variables can shadow each other properly (we should do this) - currently they all have to have unique names. 3) atom('n) is no longer syntactic sugar for range('n, 'n). The reason why we want to do this is that if we wanted to be smart about what sail operations can be translated into SMT operations at the type level we care very much that they talk about atoms and not ranges. Why? Because atom is the term level representation of a specific type variable so it's clear how to map between term level functions and type level functions, i.e. (atom('n) -> atom('n)) can be reflected at the type level by a type level function with kind Int -> Int, but the same is not true for range. Furthermore, both are interdefinable as atom('n) -> range('n, 'n) range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('n)} and I think the second is actually slightly more elegant. This change *should* be backwards compatible, as the type-checker knows how to convert from atom to ranges and unify them with each other, but there may be bugs introduced here... --- src/ast_util.ml | 1 + src/constraint.ml | 40 +++++------ src/constraint.mli | 1 + src/initial_check.ml | 3 + src/type_check.ml | 185 ++++++++++++++++++++++++++++++--------------------- 5 files changed, 134 insertions(+), 96 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 5393bb81..aa3efc40 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -458,6 +458,7 @@ and string_of_nexp_aux = function | 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_app (id, nexps) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_nexp nexps ^ ")" | Nexp_exp n -> "2 ^ " ^ string_of_nexp n | Nexp_neg n -> "- " ^ string_of_nexp n diff --git a/src/constraint.ml b/src/constraint.ml index 5dcc10f0..37073ff2 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -3,27 +3,33 @@ open Util (* ===== Integer Constraints ===== *) -type nexp_op = Plus | Minus | Mult +type nexp_op = string type nexp = - | NFun of (nexp_op * nexp * nexp) + | NFun of (nexp_op * nexp list) | 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 big_int_op : nexp_op -> (big_int -> big_int -> big_int) option = function + | "+" -> Some add_big_int + | "-" -> Some sub_big_int + | "*" -> Some mult_big_int + | _ -> None let rec arith constr = let constr' = match constr with - | NFun (op, x, y) -> NFun (op, arith x, arith y) + | NFun (op, [x; y]) -> NFun (op, [arith x; arith y]) | N2n c -> N2n (arith c) | c -> c in match constr' with - | NFun (op, NConstant x, NConstant y) -> NConstant (big_int_op op x y) + | NFun (op, [NConstant x; NConstant y]) as c -> + begin + match big_int_op op with + | Some op -> NConstant (op x y) + | None -> c + end | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x) | c -> c @@ -63,7 +69,7 @@ module IntSet = Set.Make( let rec nexp_vars : nexp -> IntSet.t = function | NConstant _ -> IntSet.empty | NVar v -> IntSet.singleton v - | NFun (_, x, y) -> IntSet.union (nexp_vars x) (nexp_vars y) + | NFun (_, xs) -> List.fold_left IntSet.union IntSet.empty (List.map nexp_vars xs) | N2n x -> nexp_vars x let rec constraint_vars : nexp constraint_bool -> IntSet.t = function @@ -98,14 +104,8 @@ let cop_sexpr op 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) + | NFun (op, xs) -> sfun op (List.map sexpr_of_nexp xs) | 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) @@ -245,11 +245,13 @@ 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 add x y : nexp = NFun ("+", [x; y]) + +let sub x y : nexp = NFun ("-", [x; y]) -let sub x y : nexp = NFun (Minus, x, y) +let mult x y : nexp = NFun ("*", [x; y]) -let mult x y : nexp = NFun (Mult, x, y) +let app f xs : nexp = NFun (f, xs) let constant (x : big_int) : nexp = NConstant x diff --git a/src/constraint.mli b/src/constraint.mli index 4f69d51f..33881fcf 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -28,6 +28,7 @@ val pow2 : nexp -> nexp val add : nexp -> nexp -> nexp val sub : nexp -> nexp -> nexp val mult : nexp -> nexp -> nexp +val app : string -> nexp list -> nexp val constant : Big_int.big_int -> nexp val variable : int -> nexp diff --git a/src/initial_check.ml b/src/initial_check.ml index df715e17..e80ff9a4 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -238,6 +238,9 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = let n1 = to_ast_nexp k_env t1 in let n2 = to_ast_nexp k_env t2 in Nexp_aux (Nexp_minus (n1, n2), l) + | Parse_ast.ATyp_app (id, ts) -> + let nexps = List.map (to_ast_nexp k_env) ts in + Nexp_aux (Nexp_app (to_ast_id id, nexps), l) | _ -> typ_error l "Required an item of kind Nat, encountered an illegal form for this kind" None None None) and to_ast_order (k_env : kind Envmap.t) (def_ord : order) (o: Parse_ast.atyp) : Ast.order = diff --git a/src/type_check.ml b/src/type_check.ml index 8a56d9b2..f71e52c1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -225,6 +225,7 @@ and nexp_subst_aux sv subst = function | 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_app (id, nexps) -> Nexp_app (id, List.map (nexp_subst sv subst) nexps) | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp) | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp) @@ -238,6 +239,7 @@ and nc_subst_nexp_aux l sv subst = function | NC_equal (n1, n2) -> NC_equal (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_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_set (kid, ints) as set_nc -> if Kid.compare kid sv = 0 then nexp_set_to_or l (mk_nexp subst) ints @@ -393,6 +395,11 @@ module Env : sig val fresh_kid : ?kid:kid -> t -> kid val expand_synonyms : t -> typ -> typ val base_typ_of : t -> typ -> typ + val add_smt_op : id -> string -> t -> t + val get_smt_op : id -> t -> string + (* Well formedness-checks *) + val wf_typ : ?exs:KidSet.t -> t -> typ -> unit + val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit val empty : t end = struct type t = @@ -411,6 +418,7 @@ end = struct records : (typquant * (typ * id) list) Bindings.t; accessors : (typquant * typ) Bindings.t; externs : (string -> string option) Bindings.t; + smt_ops : string Bindings.t; casts : id list; allow_casts : bool; constraints : n_constraint list; @@ -435,6 +443,7 @@ end = struct records = Bindings.empty; accessors = Bindings.empty; externs = Bindings.empty; + smt_ops = Bindings.empty; casts = []; allow_casts = true; constraints = []; @@ -443,56 +452,16 @@ end = struct poly_undefineds = false; } - let counter = ref 0 - - let fresh_kid ?kid:(kid=mk_kid "") env = - let suffix = if Kid.compare kid (mk_kid "") = 0 then "#" else "#" ^ string_of_id (id_of_kid kid) in - let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter ^ suffix), Parse_ast.Unknown) in - incr counter; fresh - - let freshen_kid env kid (typq, typ) = - let fresh = fresh_kid ~kid:kid env in - (typquant_subst_kid kid fresh typq, typ_subst_kid kid fresh typ) - - let freshen_bind env bind = - List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) - - let get_val_spec id env = - try - let bind = Bindings.find id env.top_val_specs in - typ_debug ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, bk) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars)); - let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in - typ_debug ("get_val_spec: freshened to " ^ string_of_bind bind'); - bind' - with - | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) - - let update_val_spec id bind env = - begin - typ_print ("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 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 update_val_spec id bind env - - let is_union_constructor id env = - let is_ctor id (Tu_aux (tu, _)) = match tu with - | Tu_id ctor_id when Id.compare id ctor_id = 0 -> true - | Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true - | _ -> false - in - let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in - List.exists (is_ctor id) type_unions - 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 get_typ_vars env = env.typ_vars + let builtin_typs = + IdSet.of_list (List.map mk_id + [ "range"; "atom"; "vector"; "register"; "bit"; "unit"; "int"; "nat"; "bool"; "real"; "list"; "string"; "itself"]) + (* FIXME: Add an IdSet for builtin types *) let bound_typ_id env id = Bindings.mem id env.typ_synonyms @@ -500,18 +469,27 @@ end = struct || Bindings.mem id env.records || Bindings.mem id env.regtyps || Bindings.mem id env.enums - || Id.compare id (mk_id "range") = 0 - || Id.compare id (mk_id "vector") = 0 - || Id.compare id (mk_id "register") = 0 - || Id.compare id (mk_id "bit") = 0 - || Id.compare id (mk_id "unit") = 0 - || Id.compare id (mk_id "int") = 0 - || Id.compare id (mk_id "nat") = 0 - || Id.compare id (mk_id "bool") = 0 - || Id.compare id (mk_id "real") = 0 - || Id.compare id (mk_id "list") = 0 - || Id.compare id (mk_id "string") = 0 - || Id.compare id (mk_id "itself") = 0 + || IdSet.mem id builtin_typs + + let get_overloads id env = + try Bindings.find id env.overloads with + | Not_found -> [] + + let add_overloads id ids env = + typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"); + { env with overloads = Bindings.add id ids env.overloads } + + let add_smt_op id str env = + typ_print ("Adding smt binding " ^ string_of_id id ^ " to " ^ str); + { env with smt_ops = Bindings.add id str env.smt_ops } + + let get_smt_op (Id_aux (_, l) as id) env = + let rec first_smt_op = function + | id :: ids -> (try Bindings.find id env.smt_ops with Not_found -> first_smt_op ids) + | [] -> typ_error l ("No SMT op for " ^ string_of_id id) + in + try Bindings.find id env.smt_ops with + | Not_found -> first_smt_op (get_overloads id env) (* Check if a type, order, or n-expression is well-formed. Throws a type error if the type is badly formed. FIXME: Add arity to type @@ -529,7 +507,8 @@ end = struct | Typ_app (id, args) when bound_typ_id env id -> List.iter (wf_typ_arg ~exs:exs env) args | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id) | Typ_exist ([], _, _) -> typ_error l ("Existential must have some type variables") - | Typ_exist (kids, nc, typ) when KidSet.is_empty exs -> wf_typ ~exs:(KidSet.of_list kids) env typ + | Typ_exist (kids, nc, typ) when KidSet.is_empty exs -> + wf_constraint ~exs:(KidSet.of_list kids) env nc; wf_typ ~exs:(KidSet.of_list kids) env typ | Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed") and wf_typ_arg ?exs:(exs=KidSet.empty) env (Typ_arg_aux (typ_arg_aux, _)) = match typ_arg_aux with @@ -549,6 +528,9 @@ end = struct ^ string_of_base_kind_aux kind ^ " but should have kind Nat") end | Nexp_constant _ -> () + | Nexp_app (id, nexps) -> + let _ = get_smt_op id env in + List.iter (fun n -> wf_nexp ~exs:exs env n) nexps | Nexp_times (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 | Nexp_sum (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 | Nexp_minus (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 @@ -565,6 +547,60 @@ end = struct ^ string_of_base_kind_aux kind ^ " but should have kind Order") end | Ord_inc | Ord_dec -> () + and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc, _)) = + match nc with + | NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_bounded_ge (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_bounded_le (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *) + | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 + | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 + | NC_true | NC_false -> () + + let counter = ref 0 + + let fresh_kid ?kid:(kid=mk_kid "") env = + let suffix = if Kid.compare kid (mk_kid "") = 0 then "#" else "#" ^ string_of_id (id_of_kid kid) in + let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter ^ suffix), Parse_ast.Unknown) in + incr counter; fresh + + let freshen_kid env kid (typq, typ) = + let fresh = fresh_kid ~kid:kid env in + (typquant_subst_kid kid fresh typq, typ_subst_kid kid fresh typ) + + let freshen_bind env bind = + List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) + + let get_val_spec id env = + try + let bind = Bindings.find id env.top_val_specs in + typ_debug ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, bk) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars)); + let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in + typ_debug ("get_val_spec: freshened to " ^ string_of_bind bind'); + bind' + with + | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) + + let update_val_spec id bind env = + begin + typ_print ("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 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 update_val_spec id bind env + + let is_union_constructor id env = + let is_ctor id (Tu_aux (tu, _)) = match tu with + | Tu_id ctor_id when Id.compare id ctor_id = 0 -> true + | Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true + | _ -> false + in + let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in + List.exists (is_ctor id) type_unions let add_enum id ids env = if bound_typ_id env id @@ -666,14 +702,6 @@ end = struct try Bindings.find id env.registers with | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id) - let get_overloads id env = - try Bindings.find id env.overloads with - | Not_found -> [] - - let add_overloads id ids env = - typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"); - { env with overloads = Bindings.add id ids env.overloads } - let is_extern id env backend = try not (Bindings.find id env.externs backend = None) with | Not_found -> false @@ -793,17 +821,6 @@ end = struct try Bindings.find id env.num_defs with | Not_found -> typ_raise (id_loc id) (Err_no_num_ident id) - let rec wf_constraint env (NC_aux (nc, _)) = - match nc with - | NC_equal (n1, n2) -> wf_nexp env n1; wf_nexp env n2 - | NC_not_equal (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_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *) - | NC_or (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2 - | NC_and (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2 - | NC_true | NC_false -> () - let get_constraints env = env.constraints let add_constraint (NC_aux (_, l) as constr) env = @@ -936,7 +953,7 @@ let lvector_typ env l typ = let initial_env = Env.empty - |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) + (* |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) *) (* Internal functions for Monomorphise.AtomToItself *) @@ -1066,6 +1083,9 @@ let rec normalize_typ env (Typ_aux (typ, l)) = | Typ_var kid -> Tnf_var kid | Typ_tup typs -> Tnf_tup (List.map (normalize_typ env) typs) | Typ_app (f, []) -> normalize_typ env (Typ_aux (Typ_id f, l)) + | Typ_app (Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp n, _)]) -> + let kid = Env.fresh_kid env in + Tnf_index_sort (IS_prop (kid, [(n, nvar kid); (nvar kid, n)])) | 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)])) @@ -1115,6 +1135,7 @@ let rec nexp_constraint env var_of (Nexp_aux (nexp, l)) = | Nexp_minus (nexp1, nexp2) -> Constraint.sub (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) | Nexp_exp nexp -> Constraint.pow2 (nexp_constraint env var_of nexp) | Nexp_neg nexp -> Constraint.sub (Constraint.constant (big_int_of_int 0)) (nexp_constraint env var_of nexp) + | Nexp_app (id, nexps) -> Constraint.app (Env.get_smt_op id env) (List.map (nexp_constraint env var_of) nexps) let rec nc_constraint env var_of (NC_aux (nc, l)) = match nc with @@ -1248,6 +1269,7 @@ let rec nexp_frees ?exs:(exs=KidSet.empty) (Nexp_aux (nexp, l)) = | Nexp_times (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) | Nexp_sum (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) | Nexp_minus (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) + | Nexp_app (id, ns) -> List.fold_left KidSet.union KidSet.empty (List.map (fun n -> nexp_frees ~exs:exs n) ns) | Nexp_exp n -> nexp_frees ~exs:exs n | Nexp_neg n -> nexp_frees ~exs:exs n @@ -1474,6 +1496,9 @@ let rec unify l env typ1 typ2 = | Invalid_argument _ -> unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2 ^ " tuple type is of different length") end + | Typ_app (f1, [arg1a; arg1b]), Typ_app (f2, [arg2]) + when Id.compare (mk_id "range") f1 = 0 && Id.compare (mk_id "atom") f2 = 0 -> + unify_typ_arg_list 0 KBindings.empty [] [] [arg1a; arg1b] [arg2; arg2] | Typ_app (f1, args1), Typ_app (f2, args2) when Id.compare f1 f2 = 0 -> unify_typ_arg_list 0 KBindings.empty [] [] args1 args2 | _, _ -> unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) @@ -2115,6 +2140,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ begin match letbind with | LB_val (P_aux (P_typ (ptyp, _), _) as pat, bind) -> + Env.wf_typ env ptyp; let checked_bind = crule check_exp env bind ptyp in let tpat, env = bind_pat env pat ptyp in annot_exp (E_let (LB_aux (LB_val (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ @@ -2126,6 +2152,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | E_app_infix (x, op, y), _ -> check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ | E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_prove") = 0 -> + Env.wf_constraint env nc; if prove env nc then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ else typ_error l ("Cannot prove " ^ string_of_n_constraint nc) @@ -2405,6 +2432,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = | Enum enum -> annot_pat (P_id v) enum, env end | P_typ (typ_annot, pat) -> + Env.wf_typ env typ_annot; let (typed_pat, env) = bind_pat env pat typ_annot in annot_pat (P_typ (typ_annot, typed_pat)) typ_annot, env | P_lit lit -> @@ -2695,6 +2723,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | 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_constraint nc -> + Env.wf_constraint env nc; annot_exp (E_constraint nc) bool_typ | E_field (exp, field) -> begin @@ -3392,6 +3421,8 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) let check_val_spec env (VS_aux (vs, (l, _))) = let (id, quants, typ, env) = match vs with | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext_opt, is_cast) -> + let env = match ext_opt "smt" with Some op -> Env.add_smt_op id op env | None -> env in + Env.wf_typ (add_typquant quants env) typ; let env = (* match ext_opt with | None -> env -- cgit v1.2.3 From ff68c0250d43869f8cc62b79ebc9930f27158bee Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 15 Nov 2017 17:25:58 +0000 Subject: Fix rule for allowing atom to unify with range --- src/type_check.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index f71e52c1..c0cd1161 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1496,6 +1496,11 @@ let rec unify l env typ1 typ2 = | Invalid_argument _ -> unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2 ^ " tuple type is of different length") end + | Typ_app (f1, [arg1]), Typ_app (f2, [Typ_arg_aux (Typ_arg_nexp n1, _) as arg2a; Typ_arg_aux (Typ_arg_nexp n2, _)]) + when Id.compare (mk_id "atom") f1 = 0 && Id.compare (mk_id "range") f2 = 0 -> + if prove env (nc_eq n1 n2) + then unify_typ_arg_list 0 KBindings.empty [] [] [arg1] [arg2a] + else typ_error l ("Cannot unify atom with range when range indices " ^ string_of_nexp n1 ^ " and " ^ string_of_nexp n2 ^ " are not equal") | Typ_app (f1, [arg1a; arg1b]), Typ_app (f2, [arg2]) when Id.compare (mk_id "range") f1 = 0 && Id.compare (mk_id "atom") f2 = 0 -> unify_typ_arg_list 0 KBindings.empty [] [] [arg1a; arg1b] [arg2; arg2] -- cgit v1.2.3 From ab2b7e532247e03fc6c4e2ca0ccd139e7a4aca0f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 15 Nov 2017 17:28:03 +0000 Subject: Fix atom - range unification again --- src/type_check.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index c0cd1161..589a5cf7 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1496,11 +1496,9 @@ let rec unify l env typ1 typ2 = | Invalid_argument _ -> unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2 ^ " tuple type is of different length") end - | Typ_app (f1, [arg1]), Typ_app (f2, [Typ_arg_aux (Typ_arg_nexp n1, _) as arg2a; Typ_arg_aux (Typ_arg_nexp n2, _)]) + | Typ_app (f1, [arg1]), Typ_app (f2, [arg2a; arg2b]) when Id.compare (mk_id "atom") f1 = 0 && Id.compare (mk_id "range") f2 = 0 -> - if prove env (nc_eq n1 n2) - then unify_typ_arg_list 0 KBindings.empty [] [] [arg1] [arg2a] - else typ_error l ("Cannot unify atom with range when range indices " ^ string_of_nexp n1 ^ " and " ^ string_of_nexp n2 ^ " are not equal") + unify_typ_arg_list 0 KBindings.empty [] [] [arg1; arg1] [arg2a; arg2b] | Typ_app (f1, [arg1a; arg1b]), Typ_app (f2, [arg2]) when Id.compare (mk_id "range") f1 = 0 && Id.compare (mk_id "atom") f2 = 0 -> unify_typ_arg_list 0 KBindings.empty [] [] [arg1a; arg1b] [arg2; arg2] -- cgit v1.2.3