diff options
| author | Alasdair Armstrong | 2017-08-15 17:42:04 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-08-15 17:42:04 +0100 |
| commit | 92c6808329dbffd54a2a687049eabe8ddb5391af (patch) | |
| tree | 1b43c0efec61ba492cf99cea21e51fc1ed67cd1c /src | |
| parent | 838a7ff721d04d9fcc7e86e97651d685572ed992 (diff) | |
Export utility functions from type_check.ml
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 2 | ||||
| -rw-r--r-- | src/type_check.mli | 19 |
2 files changed, 19 insertions, 2 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index bd27c2ba..4210f6a1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -196,7 +196,7 @@ let rec nc_negate (NC_aux (nc, _)) = | NC_or (n1, n2) -> mk_nc (NC_and (nc_negate n1, nc_negate n2)) | NC_false -> mk_nc NC_true | NC_true -> mk_nc NC_false - | NC_nat_set_bounded (kid, []) -> typ_error Parse_ast.Unknown "Cannot negate empty nexp set" + | NC_nat_set_bounded (kid, []) -> nc_false | NC_nat_set_bounded (kid, [int]) -> nc_neq (nvar kid) (nconstant int) | NC_nat_set_bounded (kid, int :: ints) -> mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_nat_set_bounded (kid, ints))))) diff --git a/src/type_check.mli b/src/type_check.mli index 0a85624c..6b23e9ac 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -135,6 +135,7 @@ module Env : sig end +(* Push all the type variables and constraints from a typquant into an environment *) val add_typquant : typquant -> Env.t -> Env.t (* Some handy utility functions for constructing types. *) @@ -155,9 +156,24 @@ val nsum : nexp -> nexp -> nexp val ntimes : nexp -> nexp -> nexp val npow2 : nexp -> nexp val nvar : kid -> nexp -val nid : id -> nexp +val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *) +(* Numeric constraint builders *) +val nc_eq : nexp -> nexp -> n_constraint +val nc_neq : nexp -> nexp -> n_constraint +val nc_lteq : nexp -> nexp -> n_constraint val nc_gteq : nexp -> nexp -> n_constraint +val nc_lt : nexp -> nexp -> n_constraint +val nc_gt : nexp -> nexp -> n_constraint +val nc_and : n_constraint -> n_constraint -> n_constraint +val nc_or : n_constraint -> n_constraint -> n_constraint +val nc_true : n_constraint +val nc_false : n_constraint + +(* Negate a n_constraint. Note that there's no NC_not constructor, so + this flips all the inequalites a the n_constraint leaves and uses + de-morgans to switch and to or and vice versa. *) +val nc_negate : n_constraint -> n_constraint (* Sail builtin types. *) val int_typ : typ @@ -172,6 +188,7 @@ val real_typ : typ val vector_typ : nexp -> nexp -> order -> typ -> typ val list_typ : typ -> typ val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ +val exc_typ : typ val inc_ord : order val dec_ord : order |