summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/constraint.ml138
-rw-r--r--src/constraint.mli2
-rw-r--r--src/process_file.ml1
-rw-r--r--src/process_file.mli1
-rw-r--r--src/rewriter.ml16
-rw-r--r--src/rewriter.mli1
-rw-r--r--src/sail.ml9
-rw-r--r--src/type_check.ml106
-rw-r--r--src/util.ml6
-rw-r--r--src/util.mli3
10 files changed, 154 insertions, 129 deletions
diff --git a/src/constraint.ml b/src/constraint.ml
index 37d1fae9..5dcc10f0 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -45,7 +45,7 @@ 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)
+ | Forall of (int list * 'a constraint_bool)
| Boolean of bool
let rec pairs (xs : 'a list) (ys : 'a list) : ('a * 'b) list =
@@ -53,77 +53,6 @@ let rec pairs (xs : 'a list) (ys : 'a list) : ('a * 'b) list =
| [] -> []
| (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
@@ -131,21 +60,18 @@ module IntSet = Set.Make(
type t = int
end)
-let rec int_expr_vars : nexp -> IntSet.t = function
+let rec nexp_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)
+ | NFun (_, x, y) -> IntSet.union (nexp_vars x) (nexp_vars y)
+ | N2n x -> nexp_vars x
-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
+let rec constraint_vars : nexp constraint_bool -> IntSet.t = function
+ | BFun (_, x, y) -> IntSet.union (constraint_vars x) (constraint_vars y)
+ | Not x -> constraint_vars x
+ | CFun (_, x, y) -> IntSet.union (nexp_vars x) (nexp_vars y)
+ | Forall (vars, x) -> IntSet.diff (constraint_vars x) (IntSet.of_list vars)
+ | Boolean _ -> IntSet.empty
(* SMTLIB v2.0 format is based on S-expressions so we have a
lightweight representation of those here. *)
@@ -184,27 +110,17 @@ let rec sexpr_of_nexp = function
| 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]
+let rec sexpr_of_constraint = function
+ | BFun (And, x, y) -> sfun "and" [sexpr_of_constraint x; sexpr_of_constraint y]
+ | BFun (Or, x, y) -> sfun "or" [sexpr_of_constraint x; sexpr_of_constraint y]
+ | Not x -> sfun "not" [sexpr_of_constraint x]
| CFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp (arith x)) (sexpr_of_nexp (arith y))
- | Branch xs -> sfun "BRANCH" (List.map sexpr_of_cbool xs)
+ | Forall (vars, x) ->
+ sfun "forall" [List (List.map (fun v -> List [Atom ("v" ^ string_of_int v); Atom "Int"]) vars); sexpr_of_constraint x]
| Boolean true -> Atom "true"
| Boolean false -> Atom "false"
-let sexpr_of_constraint_leaf = function
- | LFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp (arith x)) (sexpr_of_nexp (arith 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 =
+let smtlib_of_constraints constr : string =
"(push)\n"
^ var_decs constr ^ "\n"
^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; sexpr_of_constraint constr])
@@ -252,13 +168,8 @@ let save_digests () =
close_out out_chan
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
+ let problems = [constraints] in
+ let z3_file = smtlib_of_constraints constraints in
(* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *)
@@ -298,12 +209,7 @@ let rec call_z3 constraints : smt_result =
else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
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)
+let string_of = smtlib_of_constraints
(* ===== Abstract API for building constraints ===== *)
@@ -319,9 +225,9 @@ let conj (x : t) (y : t) : t =
let disj (x : t) (y : t) : t =
BFun (Or, x, y)
-let negate (x : t) : t = Not x
+let forall (vars : int list) (x : t) : t = Forall (vars, x)
-let branch (xs : t list) : t = Branch xs
+let negate (x : t) : t = Not x
let literal (b : bool) : t = Boolean b
diff --git a/src/constraint.mli b/src/constraint.mli
index ad75f453..4f69d51f 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -14,8 +14,8 @@ 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 forall : int list -> t -> t
val lt : nexp -> nexp -> t
val lteq : nexp -> nexp -> t
diff --git a/src/process_file.ml b/src/process_file.ml
index b95d54f7..5d362af2 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -262,3 +262,4 @@ let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
let rewrite_undefined = rewrite [("undefined", fun x -> Rewriter.rewrite_undefined !opt_lem_mwords x)]
let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewriter.rewrite_defs_ocaml
+let rewrite_ast_check = rewrite Rewriter.rewrite_defs_check
diff --git a/src/process_file.mli b/src/process_file.mli
index fae38100..4bf48aec 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -48,6 +48,7 @@ val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val load_file_no_check : Ast.order -> string -> unit Ast.defs
val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
diff --git a/src/rewriter.ml b/src/rewriter.ml
index edda208d..2f83d532 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -3624,3 +3624,19 @@ let rewrite_defs_ocaml = [
("exp_lift_assign", rewrite_defs_exp_lift_assign);
(* ("separate_numbs", rewrite_defs_separate_numbs) *)
]
+
+let rewrite_check_annot =
+ let check_annot exp =
+ try
+ prerr_endline ("CHECKING: " ^ string_of_exp exp ^ " : " ^ string_of_typ (typ_of exp));
+ let _ = check_exp (env_of exp) (strip_exp exp) (typ_of exp) in
+ exp
+ with
+ Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
+ in
+ let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> check_annot (E_aux (exp, annot))) } in
+ rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) }
+
+let rewrite_defs_check = [
+ ("check_annotations", rewrite_check_annot);
+ ]
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 3f375e25..412852d4 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -59,6 +59,7 @@ val rewrite_defs : tannot defs -> tannot defs
val rewrite_undefined : bool -> tannot defs -> tannot defs
val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for lem out*)
+val rewrite_defs_check : (string * (tannot defs -> tannot defs)) list
val simple_typ : typ -> typ
diff --git a/src/sail.ml b/src/sail.ml
index 2714b6a4..68dbcdbe 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -52,6 +52,7 @@ let opt_print_lem = ref false
let opt_print_ocaml = ref false
let opt_convert = ref false
let opt_memo_z3 = ref false
+let opt_sanity = ref false
let opt_libs_lem = ref ([]:string list)
let opt_libs_ocaml = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
@@ -128,6 +129,9 @@ let options = Arg.align ([
( "-dno_cast",
Arg.Set opt_dno_cast,
" (debug) typecheck without any implicit casting");
+ ( "-dsanity",
+ Arg.Set opt_sanity,
+ " (debug) sanity check the AST (slow)");
( "-v",
Arg.Set opt_print_version,
" print version");
@@ -183,6 +187,11 @@ let main() =
(*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
begin
+ (if !(opt_sanity)
+ then
+ let _ = rewrite_ast_check ast in
+ ()
+ else ());
(if !(opt_print_verbose)
then ((Pretty_print.pp_defs stdout) ast)
else ());
diff --git a/src/type_check.ml b/src/type_check.ml
index f380b54b..f7716bc9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1139,8 +1139,7 @@ let rec nc_constraints env var_of ncs =
| (nc :: ncs) ->
Constraint.conj (nc_constraint env var_of nc) (nc_constraints env var_of ncs)
-let prove_z3 env nc =
- typ_print ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc);
+let prove_z3' env constr =
let module Bindings = Map.Make(Kid) in
let bindings = ref Bindings.empty in
let fresh_var kid =
@@ -1152,12 +1151,16 @@ let prove_z3 env nc =
try Bindings.find kid !bindings with
| Not_found -> fresh_var kid
in
- let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (Constraint.negate (nc_constraint env var_of nc)) in
+ let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (constr var_of) in
match Constraint.call_z3 constr with
| Constraint.Unsat -> typ_debug "unsat"; true
| Constraint.Sat -> typ_debug "sat"; false
| Constraint.Unknown -> typ_debug "unknown"; false
+let prove_z3 env nc =
+ typ_print ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc);
+ prove_z3' env (fun var_of -> Constraint.negate (nc_constraint env var_of nc))
+
let prove env (NC_aux (nc_aux, _) as nc) =
let compare_const f (Nexp_aux (n1, _)) (Nexp_aux (n2, _)) =
match n1, n2 with
@@ -1287,6 +1290,20 @@ let ord_identical (Ord_aux (ord1, _)) (Ord_aux (ord2, _)) =
| Ord_dec, Ord_dec -> true
| _, _ -> false
+let rec nc_identical (NC_aux (nc1, _)) (NC_aux (nc2, _)) =
+ match nc1, nc2 with
+ | NC_equal (n1a, n1b), NC_equal (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b
+ | NC_not_equal (n1a, n1b), NC_not_equal (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b
+ | NC_bounded_ge (n1a, n1b), NC_bounded_ge (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b
+ | NC_bounded_le (n1a, n1b), NC_bounded_le (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b
+ | NC_or (nc1a, nc1b), NC_or (nc2a, nc2b) -> nc_identical nc1a nc2a && nc_identical nc1b nc2b
+ | NC_and (nc1a, nc1b), NC_and (nc2a, nc2b) -> nc_identical nc1a nc2a && nc_identical nc1b nc2b
+ | NC_true, NC_true -> true
+ | NC_false, NC_false -> true
+ | NC_set (kid1, ints1), NC_set (kid2, ints2) when List.length ints1 = List.length ints2 ->
+ Kid.compare kid1 kid2 = 0 && List.for_all2 (fun i1 i2 -> i1 = i2) ints1 ints2
+ | _, _ -> false
+
let typ_identical env typ1 typ2 =
let rec typ_identical' (Typ_aux (typ1, _)) (Typ_aux (typ2, _)) =
match typ1, typ2 with
@@ -1303,6 +1320,8 @@ let typ_identical env typ1 typ2 =
try Id.compare f1 f2 = 0 && List.for_all2 typ_arg_identical args1 args2 with
| Invalid_argument _ -> false
end
+ | Typ_exist (kids1, nc1, typ1), Typ_exist (kids2, nc2, typ2) when List.length kids1 = List.length kids2 ->
+ List.for_all2 (fun k1 k2 -> Kid.compare k1 k2 = 0) kids1 kids2 && nc_identical nc1 nc2 && typ_identical' typ1 typ2
| _, _ -> false
and typ_arg_identical (Typ_arg_aux (arg1, _)) (Typ_arg_aux (arg2, _)) =
match arg1, arg2 with
@@ -1506,6 +1525,23 @@ let merge_uvars l unifiers1 unifiers2 =
(* 4.5. Subtyping with existentials *)
(**************************************************************************)
+let destruct_atom_nexp env typ =
+ match Env.expand_synonyms env typ with
+ | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)]), _)
+ when string_of_id f = "atom" -> Some n
+ | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_nexp m, _)]), _)
+ when string_of_id f = "range" && nexp_identical n m -> Some n
+ | _ -> None
+
+let destruct_atom_kid env typ =
+ match Env.expand_synonyms env typ with
+ | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, _)), _)]), _)
+ when string_of_id f = "atom" -> Some kid
+ | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid1, _)), _);
+ Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _)
+ when string_of_id f = "range" && Kid.compare kid1 kid2 = 0 -> Some kid1
+ | _ -> None
+
let nc_subst_uvar kid uvar nc =
match uvar with
| U_nexp nexp -> nc_subst_nexp kid (unaux_nexp nexp) nc
@@ -1516,9 +1552,60 @@ let uv_nexp_constraint env (kid, uvar) =
| U_nexp nexp -> Env.add_constraint (nc_eq (nvar kid) nexp) env
| _ -> env
+let rec alpha_equivalent env typ1 typ2 =
+ let counter = ref 0 in
+ let new_kid () = let kid = mk_kid ("alpha#" ^ string_of_int !counter) in (incr counter; kid) in
+
+ let rec relabel (Typ_aux (aux, l) as typ) =
+ let relabelled_aux =
+ match aux with
+ | Typ_wild | 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) ->
+ let kids = List.map (fun kid -> (kid, new_kid ())) kids in
+ let nc = List.fold_left (fun nc (kid, nk) -> nc_subst_nexp kid (Nexp_var nk) nc) nc kids in
+ let typ = List.fold_left (fun nc (kid, nk) -> typ_subst_nexp kid (Nexp_var nk) nc) typ kids in
+ Typ_exist (List.map snd kids, nc, typ)
+ | Typ_app (id, args) ->
+ Typ_app (id, List.map relabel_arg args)
+ in
+ Typ_aux (relabelled_aux, l)
+ and relabel_arg (Typ_arg_aux (aux, l) as arg) =
+ match aux with
+ | Typ_arg_nexp _ | Typ_arg_order _ -> arg
+ | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (relabel typ), l)
+ in
+
+ let typ1 = relabel (Env.expand_synonyms env typ1) in
+ counter := 0;
+ let typ2 = relabel (Env.expand_synonyms env typ2) in
+ typ_debug ("Alpha equivalence for " ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2);
+ if typ_identical env typ1 typ2
+ then (typ_debug "alpha-equivalent"; true)
+ else (typ_debug "Not alpha-equivalent"; false)
+
let rec subtyp l env typ1 typ2 =
typ_print ("Subtype " ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2);
match destruct_exist env typ1, destruct_exist env typ2 with
+ (* Ensure alpha equivalent types are always subtypes of one another
+ - this ensures that we can always re-check inferred types. *)
+ | _, _ when alpha_equivalent env typ1 typ2 -> ()
+ (* Special case for two existentially quantified numeric (atom) types *)
+ | Some (kids1, nc1, typ1), Some (_ :: _ :: _ as kids2, nc2, typ2)
+ when is_some (destruct_atom_kid env typ1) && is_some (destruct_atom_kid env typ2) ->
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids1 in
+ let env = Env.add_constraint nc1 env in
+ let Some atom_kid1 = destruct_atom_kid env typ1 in
+ let Some atom_kid2 = destruct_atom_kid env typ2 in
+ let kids2 = List.filter (fun kid -> Kid.compare atom_kid2 kid <> 0) kids2 in
+ let env = Env.add_typ_var atom_kid2 BK_nat env in
+ let env = Env.add_constraint (nc_eq (nvar atom_kid1) (nvar atom_kid2)) env in
+ let constr var_of =
+ Constraint.forall (List.map var_of kids2) (Constraint.negate (nc_constraint env var_of nc2))
+ in
+ if prove_z3' env constr then ()
+ else typ_error l ("Existential atom subtyping failed")
| Some (kids, nc, typ1), _ ->
let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
let env = Env.add_constraint nc env in
@@ -1696,14 +1783,6 @@ let destruct_atom (Typ_aux (typ_aux, _)) =
end
| _ -> None
-let destruct_atom_nexp env typ =
- match Env.expand_synonyms env typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)]), _)
- when string_of_id f = "atom" -> Some n
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_nexp m, _)]), _)
- when string_of_id f = "range" && nexp_identical n m -> Some n
- | _ -> None
-
exception Not_a_constraint;;
let rec assert_nexp env (E_aux (exp_aux, _)) =
@@ -2116,6 +2195,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
+ let switch_typ (E_aux (exp, (l, Some (env, _, eff)))) typ = E_aux (exp, (l, Some (env, typ, eff))) in
let rec try_casts trigger errs = function
| [] -> typ_raise l (Err_no_casts (trigger, errs))
| (cast :: casts) -> begin
@@ -2130,7 +2210,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
begin
try
typ_debug ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ);
- subtyp l env (typ_of annotated_exp) typ; annotated_exp
+ subtyp l env (typ_of annotated_exp) typ; switch_typ annotated_exp typ
with
| Type_error (_, trigger) when Env.allow_casts env ->
let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
@@ -2146,6 +2226,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
+ let switch_typ (E_aux (exp, (l, Some (env, _, eff)))) typ = E_aux (exp, (l, Some (env, typ, eff))) in
let rec try_casts = function
| [] -> unify_error l "No valid casts resulted in unification"
| (cast :: casts) -> begin
@@ -2768,6 +2849,7 @@ and instantiation_of (E_aux (exp_aux, (l, _)) as exp) =
and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
let annot_exp exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
+ let switch_annot env typ (E_aux (exp, (l, Some (_, _, eff)))) = E_aux (exp, (l, Some (env, typ, eff))) in
let all_unifiers = ref KBindings.empty in
let ex_goal = ref None in
let prove_goal env = match !ex_goal with
diff --git a/src/util.ml b/src/util.ml
index 59ba7026..762e0f88 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -359,3 +359,9 @@ let rec string_of_list sep string_of = function
let string_of_option string_of = function
| None -> ""
| Some x -> string_of x
+
+let is_some = function
+ | Some _ -> true
+ | None -> false
+
+let is_none opt = not (is_some opt)
diff --git a/src/util.mli b/src/util.mli
index a7818f93..15ddfef0 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -215,3 +215,6 @@ val string_of_list : string -> ('a -> string) -> 'a list -> string
val string_of_option : ('a -> string) -> 'a option -> string
val split_on_char : char -> string -> string list
+
+val is_some : 'a option -> bool
+val is_none : 'a option -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 05:57:15 +0000