summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--language/l2.ott2
-rw-r--r--src/ast_util.ml44
-rw-r--r--src/ast_util.mli9
-rw-r--r--src/monomorphise.ml5
-rw-r--r--src/ocaml_backend.ml4
-rw-r--r--src/pretty_print_common.ml1
-rw-r--r--src/pretty_print_lem.ml4
-rw-r--r--src/pretty_print_lem_ast.ml3
-rw-r--r--src/pretty_print_ocaml.ml1
-rw-r--r--src/pretty_print_sail2.ml1
-rw-r--r--src/rewriter.ml1
-rw-r--r--src/spec_analysis.ml2
-rw-r--r--src/type_check.ml65
-rw-r--r--src/type_check.mli8
14 files changed, 63 insertions, 87 deletions
diff --git a/language/l2.ott b/language/l2.ott
index d010bc67..3418e673 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -263,8 +263,6 @@ grammar
typ :: 'Typ_' ::=
{{ com type expressions, of kind $[[Type]]$ }}
{{ aux _ l }}
- | _ :: :: wild
- {{ com unspecified type }}
| id :: :: id
{{ com defined type }}
| kid :: :: var
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 746d54ea..7d472891 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -260,6 +260,21 @@ let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
let nc_true = mk_nc NC_true
let nc_false = mk_nc NC_false
+let rec nc_negate (NC_aux (nc, _)) =
+ match nc with
+ | NC_bounded_ge (n1, n2) -> nc_lt n1 n2
+ | NC_bounded_le (n1, n2) -> nc_gt n1 n2
+ | NC_equal (n1, n2) -> nc_neq n1 n2
+ | NC_not_equal (n1, n2) -> nc_eq n1 n2
+ | NC_and (n1, n2) -> mk_nc (NC_or (nc_negate n1, nc_negate n2))
+ | 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_set (kid, []) -> nc_false
+ | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
+ | NC_set (kid, int :: ints) ->
+ mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints)))))
+
let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
let mk_typquant qis = TypQ_aux (TypQ_tq qis, Parse_ast.Unknown)
@@ -283,6 +298,18 @@ let quant_kopts typq =
in
quant_items typq |> List.map qi_kopt |> List.concat
+let quant_split typq =
+ let qi_kopt = function
+ | QI_aux (QI_id kopt, _) -> [kopt]
+ | _ -> []
+ in
+ let qi_nc = function
+ | QI_aux (QI_const nc, _) -> [nc]
+ | _ -> []
+ in
+ let qis = quant_items typq in
+ List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis)
+
let unaux_nexp (Nexp_aux (nexp, _)) = nexp
let unaux_order (Ord_aux (ord, _)) = ord
let unaux_typ (Typ_aux (typ, _)) = typ
@@ -469,7 +496,6 @@ and string_of_nexp_aux = function
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 ^ ")"
@@ -737,6 +763,21 @@ let has_effect (Effect_aux (eff,_)) searched_for = match eff with
let effect_set (Effect_aux (eff,_)) = match eff with
| Effect_set effs -> BESet.of_list effs
+(* Utilities for constructing effect sets *)
+
+let union_effects e1 e2 =
+ match e1, e2 with
+ | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) ->
+ let base_effs3 = BESet.elements (BESet.of_list (base_effs1 @ base_effs2)) in
+ Effect_aux (Effect_set base_effs3, Parse_ast.Unknown)
+ | _, _ -> assert false (* We don't do Effect variables *)
+
+let equal_effects e1 e2 =
+ match e1, e2 with
+ | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) ->
+ BESet.compare (BESet.of_list base_effs1) (BESet.of_list base_effs2) = 0
+ | _, _ -> assert false (* We don't do Effect variables *)
+
let rec tyvars_of_nexp (Nexp_aux (nexp,_)) =
match nexp with
| Nexp_id _
@@ -750,7 +791,6 @@ let rec tyvars_of_nexp (Nexp_aux (nexp,_)) =
let rec tyvars_of_typ (Typ_aux (t,_)) =
match t with
- | Typ_wild
| Typ_id _ -> KidSet.empty
| Typ_var kid -> KidSet.singleton kid
| Typ_fn (t1,t2,_) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index a41f3737..8f8a2889 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -131,8 +131,14 @@ val nc_true : n_constraint
val nc_false : n_constraint
val nc_set : kid -> int list -> 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
+
val quant_items : typquant -> quant_item list
val quant_kopts : typquant -> kinded_id list
+val quant_split : typquant -> kinded_id list * n_constraint list
(* Functions to map over the annotations in sub-expressions *)
val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
@@ -247,6 +253,9 @@ val has_effect : effect -> base_effect_aux -> bool
val effect_set : effect -> BESet.t
+val equal_effects : effect -> effect -> bool
+val union_effects : effect -> effect -> effect
+
val tyvars_of_nexp : nexp -> KidSet.t
val tyvars_of_typ : typ -> KidSet.t
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 74242509..7f9eea57 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -69,7 +69,6 @@ let subst_src_typ substs t =
let rec s_styp substs ((Typ_aux (t,l)) as ty) =
let re t = Typ_aux (t,l) in
match t with
- | Typ_wild
| Typ_id _
| Typ_var _
-> ty
@@ -209,7 +208,6 @@ let apply_kid_insts kid_insts t =
let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
match ty with
- | Typ_wild
| Typ_id _
| Typ_var _
-> insts,typ
@@ -245,7 +243,6 @@ and inst_src_typ_arg insts (Typ_arg_aux (ta,l) as tyarg) =
let rec contains_exist (Typ_aux (ty,_)) =
match ty with
- | Typ_wild
| Typ_id _
| Typ_var _
-> false
@@ -282,7 +279,6 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
more manageable prenex-form below *)
let rec size_nvars_ty (Typ_aux (ty,l) as typ) =
match ty with
- | Typ_wild
| Typ_id _
| Typ_var _
-> (KidSet.empty,[[],typ])
@@ -1518,7 +1514,6 @@ let tyvars_bound_in_lb (LB_aux (LB_val (pat,_),_)) = tyvars_bound_in_pat pat
let rec sizes_of_typ (Typ_aux (t,l)) =
match t with
- Typ_wild
| Typ_id _
| Typ_var _
-> KidSet.empty
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index e8fd34b1..5fb0d177 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -80,7 +80,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
^^ space ^^ arg
| Typ_fn (typ1, typ2, _) -> string "\"FN\""
| Typ_var kid -> string "\"VAR\""
- | Typ_exist _ | Typ_wild -> assert false
+ | Typ_exist _ -> assert false
let ocaml_typ_id ctx = function
| id when Id.compare id (mk_id "string") = 0 -> string "string"
@@ -102,7 +102,7 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
| Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
| Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2]
| Typ_var kid -> zencode_kid kid
- | Typ_exist _ | Typ_wild -> assert false
+ | Typ_exist _ -> assert false
and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
match typ_arg_aux with
| Typ_arg_typ typ -> ocaml_typ ctx typ
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 83c28a7d..5cf85002 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -177,7 +177,6 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
| Typ_id id -> doc_id id
| Typ_var v -> doc_var v
- | Typ_wild -> underscore
| Typ_app _ | Typ_tup _ | Typ_fn _ ->
(* exhaustiveness matters here to avoid infinite loops
* if we add a new Typ constructor *)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c32212a6..22f210e8 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -191,7 +191,6 @@ let rec orig_nexp (Nexp_aux (nexp, l)) =
let rec lem_nexps_of_typ sequential mwords (Typ_aux (t,_)) =
let trec = lem_nexps_of_typ sequential mwords in
match t with
- | Typ_wild
| Typ_id _ -> NexpSet.empty
| Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid))
| Typ_fn (t1,t2,_) -> NexpSet.union (trec t1) (trec t2)
@@ -294,7 +293,6 @@ let doc_typ_lem, doc_atomic_typ_lem =
then string "register"
else*) doc_id_lem_type id
| Typ_var v -> doc_var v
- | Typ_wild -> underscore
| Typ_app _ | Typ_tup _ | Typ_fn _ ->
(* exhaustiveness matters here to avoid infinite loops
* if we add a new Typ constructor *)
@@ -322,7 +320,6 @@ let doc_typ_lem, doc_atomic_typ_lem =
a bitvector; for other types of vectors, the length is not pretty-printed
in the type, and the start index is never pretty-printed in vector types. *)
let rec contains_t_pp_var mwords (Typ_aux (t,a) as typ) = match t with
- | Typ_wild -> true
| Typ_id _ -> false
| Typ_var _ -> true
| Typ_exist _ -> true
@@ -423,7 +420,6 @@ let doc_typquant_lem (TypQ_aux(tq,_)) vars_included typ = match tq with
approach will do for now. *)
let rec typeclass_nexps (Typ_aux(t,_)) = match t with
-| Typ_wild
| Typ_id _
| Typ_var _
-> NexpSet.empty
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 8031ba3e..1b7e2fca 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -162,8 +162,7 @@ let rec pp_format_typ_lem (Typ_aux(t,l)) =
(pp_format_effects_lem efct) ^ ")"
| Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
| Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
- | Typ_exist(kids,nc,typ) -> "(Typ_exist ([" ^ list_format ";" pp_format_var_lem kids ^ "], " ^ pp_format_nexp_constraint_lem nc ^ ", " ^ pp_format_typ_lem typ ^ "))"
- | Typ_wild -> "Typ_wild") ^ " " ^
+ | Typ_exist(kids,nc,typ) -> "(Typ_exist ([" ^ list_format ";" pp_format_var_lem kids ^ "], " ^ pp_format_nexp_constraint_lem nc ^ ", " ^ pp_format_typ_lem typ ^ "))") ^ " " ^
(pp_format_l_lem l) ^ ")"
and pp_format_nexp_lem (Nexp_aux(n,l)) =
"(Nexp_aux " ^
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index b1238f8a..74461aab 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -112,7 +112,6 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml =
and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
| Typ_id id -> doc_id_ocaml_type id
| Typ_var v -> doc_var v
- | Typ_wild -> underscore
| Typ_app _ | Typ_tup _ | Typ_fn _ ->
(* exhaustiveness matters here to avoid infinite loops
* if we add a new Typ constructor *)
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index ce64d1b4..56560de2 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -83,7 +83,6 @@ let rec doc_typ (Typ_aux (typ_aux, _)) =
| Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
| Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
| Typ_var kid -> doc_kid kid
- | Typ_wild -> assert false
(* Resugar set types like {|1, 2, 3|} *)
| Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 2f83d532..025bade2 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2634,7 +2634,6 @@ let rewrite_undefined mwords =
let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l)
and simple_typ_aux = function
- | Typ_wild -> Typ_wild
| Typ_id id -> Typ_id id
| Typ_app (id, [_; _; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
Typ_app (mk_id "list", [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)])
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 2ff2f9ba..bdbc031a 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -210,7 +210,6 @@ let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with
(free_type_names_t consider_var t2)
| Typ_tup ts -> free_type_names_ts consider_var ts
| Typ_app (name,targs) -> Nameset.add (string_of_id name) (free_type_names_t_args consider_var targs)
- | Typ_wild -> mt
| Typ_exist (kids,_,t') -> List.fold_left (fun s kid -> Nameset.remove (string_of_kid kid) s) (free_type_names_t consider_var t') kids
and free_type_names_ts consider_var ts = nameset_bigunion (List.map (free_type_names_t consider_var) ts)
and free_type_names_maybe_t consider_var = function
@@ -230,7 +229,6 @@ let rec free_type_names_tannot consider_var = function
let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t =
match t with
- | Typ_wild -> used
| Typ_var (Kid_aux (Var v,l)) ->
if consider_var
then conditional_add_typ bound used (Ast.Id_aux (Ast.Id v,l))
diff --git a/src/type_check.ml b/src/type_check.ml
index 2688af50..0c4c9f8e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -147,38 +147,6 @@ let is_list (Typ_aux (typ_aux, _)) =
when string_of_id f = "list" -> Some typ
| _ -> None
-let rec nc_negate (NC_aux (nc, _)) =
- match nc with
- | NC_bounded_ge (n1, n2) -> nc_lt n1 n2
- | NC_bounded_le (n1, n2) -> nc_gt n1 n2
- | NC_equal (n1, n2) -> nc_neq n1 n2
- | NC_not_equal (n1, n2) -> nc_eq n1 n2
- | NC_and (n1, n2) -> mk_nc (NC_or (nc_negate n1, nc_negate n2))
- | 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_set (kid, []) -> nc_false
- | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
- | NC_set (kid, int :: ints) ->
- mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints)))))
-
-(* Utilities for constructing effect sets *)
-
-module BESet = Set.Make(BE)
-
-let union_effects e1 e2 =
- match e1, e2 with
- | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) ->
- let base_effs3 = BESet.elements (BESet.of_list (base_effs1 @ base_effs2)) in
- Effect_aux (Effect_set base_effs3, Parse_ast.Unknown)
- | _, _ -> assert false (* We don't do Effect variables *)
-
-let equal_effects e1 e2 =
- match e1, e2 with
- | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) ->
- BESet.compare (BESet.of_list base_effs1) (BESet.of_list base_effs2) = 0
- | _, _ -> assert false (* We don't do Effect variables *)
-
(* An index_sort is a more general form of range type: it can either
be IS_int, which represents every natural number, or some set of
natural numbers given by an IS_prop expression of the form
@@ -194,18 +162,6 @@ let string_of_index_sort = function
^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints
^ "}"
-let quant_split typq =
- let qi_kopt = function
- | QI_aux (QI_id kopt, _) -> [kopt]
- | _ -> []
- in
- let qi_nc = function
- | QI_aux (QI_const nc, _) -> [nc]
- | _ -> []
- in
- let qis = quant_items typq in
- List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis)
-
(**************************************************************************)
(* 1. Substitutions *)
(**************************************************************************)
@@ -244,7 +200,6 @@ and nc_subst_nexp_aux l sv subst = function
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)
@@ -260,7 +215,6 @@ and typ_subst_arg_nexp_aux sv subst = function
let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l)
and typ_subst_typ_aux sv subst = function
- | Typ_wild -> Typ_wild
| Typ_id v -> Typ_id v
| Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid
| Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2, effs)
@@ -282,7 +236,6 @@ let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst
let rec typ_subst_order sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_order_aux sv subst typ, l)
and typ_subst_order_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_order sv subst typ1, typ_subst_order sv subst typ2, effs)
@@ -297,7 +250,6 @@ and typ_subst_arg_order_aux sv subst = function
let rec typ_subst_kid sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_kid_aux sv subst typ, l)
and typ_subst_kid_aux sv subst = function
- | Typ_wild -> Typ_wild
| Typ_id v -> Typ_id v
| Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid
| Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2, effs)
@@ -393,7 +345,15 @@ module Env : sig
(* Well formedness-checks *)
val wf_typ : ?exs:KidSet.t -> t -> typ -> unit
val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit
+
+ (* Some of the code in the environment needs to use the Z3 prover,
+ which is defined below. To break the circularity this would cause
+ (as the prove code depends on the environment), we add a
+ reference to the prover to the initial environment. *)
val add_prover : (t -> n_constraint -> bool) -> t -> t
+
+ (* This must not be exported, initial_env sets up a correct initial
+ environment. *)
val empty : t
end = struct
type t =
@@ -571,7 +531,6 @@ end = struct
typ_debug ("Well-formed " ^ string_of_typ typ);
let (Typ_aux (typ_aux, l)) = expand_synonyms env typ in
match typ_aux with
- | Typ_wild -> ()
| Typ_id id when bound_typ_id env id ->
let typq = infer_kind env id in
if quant_kopts typq != []
@@ -1041,7 +1000,6 @@ let destruct_vector env typ =
let rec is_typ_monomorphic (Typ_aux (typ, _)) =
match typ with
- | Typ_wild -> assert false (* Typ_wild is bad in general *)
| Typ_id _ -> true
| Typ_tup typs -> List.for_all is_typ_monomorphic typs
| Typ_app (id, args) -> List.for_all is_typ_arg_monomorphic args
@@ -1106,7 +1064,6 @@ and string_of_tnf_arg = function
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)]))
@@ -1315,7 +1272,6 @@ let order_frees (Ord_aux (ord_aux, l)) =
let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
match typ_aux with
- | Typ_wild -> KidSet.empty
| Typ_id v -> KidSet.empty
| Typ_var kid when KidSet.mem kid exs -> KidSet.empty
| Typ_var kid -> KidSet.singleton kid
@@ -1364,7 +1320,6 @@ let rec nc_identical (NC_aux (nc1, _)) (NC_aux (nc2, _)) =
let typ_identical env typ1 typ2 =
let rec typ_identical' (Typ_aux (typ1, _)) (Typ_aux (typ2, _)) =
match typ1, typ2 with
- | Typ_wild, Typ_wild -> true
| Typ_id v1, Typ_id v2 -> Id.compare v1 v2 = 0
| Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2 = 0
| Typ_tup typs1, Typ_tup typs2 ->
@@ -1513,7 +1468,6 @@ let rec unify l env typ1 typ2 =
let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) =
typ_debug ("UNIFYING TYPES " ^ 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 Id.compare v1 v2 = 0 then KBindings.empty
else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
@@ -1628,7 +1582,7 @@ let rec alpha_equivalent env typ1 typ2 =
let rec relabel (Typ_aux (aux, l) as typ) =
let relabelled_aux =
match aux with
- | Typ_wild | Typ_id _ | Typ_var _ -> aux
+ | Typ_id _ | Typ_var _ -> aux
| Typ_fn (typ1, typ2, eff) -> Typ_fn (relabel typ1, relabel typ2, eff)
| Typ_tup typs -> Typ_tup (List.map relabel typs)
| Typ_exist (kids, nc, typ) ->
@@ -1976,7 +1930,6 @@ let rec match_typ env typ1 typ2 =
match typ1_aux, typ2_aux with
| Typ_exist (_, _, typ1), _ -> match_typ env typ1 typ2
| _, Typ_exist (_, _, typ2) -> match_typ env typ1 typ2
- | Typ_wild, Typ_wild -> true
| _, Typ_var kid2 -> true
| Typ_id v1, Typ_id v2 when Id.compare v1 v2 = 0 -> true
| Typ_id v1, Typ_id v2 when string_of_id v1 = "int" && string_of_id v2 = "nat" -> true
diff --git a/src/type_check.mli b/src/type_check.mli
index 52afeab7..1254ec36 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -165,14 +165,6 @@ val add_typquant : typquant -> Env.t -> Env.t
not of this form. *)
val orig_kid : kid -> kid
-val union_effects : effect -> effect -> effect
-val equal_effects : effect -> effect -> bool
-
-(* 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
-
(* Vector with default order. *)
val dvector_typ : Env.t -> nexp -> nexp -> typ -> typ
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:41:25 +0000