summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast.ml4
-rw-r--r--src/ast_util.ml8
-rw-r--r--src/initial_check.ml8
-rw-r--r--src/monomorphise.ml2
-rw-r--r--src/parse_ast.ml4
-rw-r--r--src/parser.mly6
-rw-r--r--src/parser2.mly6
-rw-r--r--src/pretty_print_common.ml4
-rw-r--r--src/pretty_print_lem_ast.ml4
-rw-r--r--src/rewriter.ml4
-rw-r--r--src/type_check.ml40
11 files changed, 45 insertions, 45 deletions
diff --git a/src/ast.ml b/src/ast.ml
index bf9b11aa..f57c0488 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -168,11 +168,11 @@ kinded_id_aux = (* optionally kind-annotated identifier *)
type
n_constraint_aux = (* constraint over kind $_$ *)
- NC_fixed of nexp * nexp
+ NC_equal of nexp * nexp
| NC_bounded_ge of nexp * nexp
| NC_bounded_le of nexp * nexp
| NC_not_equal of nexp * nexp
- | NC_nat_set_bounded of kid * (int) list
+ | NC_set of kid * (int) list
| NC_or of n_constraint * n_constraint
| NC_and of n_constraint * n_constraint
| NC_true
diff --git a/src/ast_util.ml b/src/ast_util.ml
index c57f2a12..61633236 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -183,8 +183,8 @@ let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
-let nc_set kid ints = mk_nc (NC_nat_set_bounded (kid, ints))
-let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
+let nc_set kid ints = mk_nc (NC_set (kid, ints))
+let nc_eq n1 n2 = mk_nc (NC_equal (n1, n2))
let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
@@ -390,7 +390,7 @@ and string_of_typ_arg_aux = function
| Typ_arg_typ typ -> string_of_typ typ
| Typ_arg_order o -> string_of_order o
and string_of_n_constraint = function
- | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
+ | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
| NC_aux (NC_not_equal (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
@@ -398,7 +398,7 @@ and string_of_n_constraint = function
"(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")"
| NC_aux (NC_and (nc1, nc2), _) ->
"(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
- | NC_aux (NC_nat_set_bounded (kid, ns), _) ->
+ | NC_aux (NC_set (kid, ns), _) ->
string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}"
| NC_aux (NC_true, _) -> "true"
| NC_aux (NC_false, _) -> "false"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 89da69e0..bbc417d5 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -311,10 +311,10 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
match c with
| Parse_ast.NC_aux(nc,l) ->
NC_aux( (match nc with
- | Parse_ast.NC_fixed(t1,t2) ->
+ | Parse_ast.NC_equal(t1,t2) ->
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
- NC_fixed(n1,n2)
+ NC_equal(n1,n2)
| Parse_ast.NC_not_equal(t1,t2) ->
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
@@ -327,8 +327,8 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
NC_bounded_le(n1,n2)
- | Parse_ast.NC_nat_set_bounded(id,bounds) ->
- NC_nat_set_bounded(to_ast_var id, bounds)
+ | Parse_ast.NC_set(id,bounds) ->
+ NC_set(to_ast_var id, bounds)
| Parse_ast.NC_or (nc1, nc2) ->
NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
| Parse_ast.NC_and (nc1, nc2) ->
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index e419370e..62b18042 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -177,7 +177,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
in
let find_set (Kid_aux (Var nvar,_) as kid) =
match list_extract (function
- | QI_aux (QI_const (NC_aux (NC_nat_set_bounded (Kid_aux (Var nvar',_),vals),_)),_)
+ | QI_aux (QI_const (NC_aux (NC_set (Kid_aux (Var nvar',_),vals),_)),_)
-> if nvar = nvar' then Some vals else None
| _ -> None) qs with
| None ->
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index cd5edce6..120a0db6 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -158,11 +158,11 @@ kinded_id_aux = (* optionally kind-annotated identifier *)
and
n_constraint_aux = (* constraint over kind $_$ *)
- NC_fixed of atyp * atyp
+ NC_equal of atyp * atyp
| NC_bounded_ge of atyp * atyp
| NC_bounded_le of atyp * atyp
| NC_not_equal of atyp * atyp
- | NC_nat_set_bounded of kid * (int) list
+ | NC_set of kid * (int) list
| NC_or of n_constraint * n_constraint
| NC_and of n_constraint * n_constraint
| NC_true
diff --git a/src/parser.mly b/src/parser.mly
index 70a6d132..678a7cc9 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1089,7 +1089,7 @@ nexp_constraint1:
nexp_constraint2:
| nexp_typ Eq nexp_typ
- { NC_aux(NC_fixed($1,$3), loc () ) }
+ { NC_aux(NC_equal($1,$3), loc () ) }
| nexp_typ ExclEq nexp_typ
{ NC_aux (NC_not_equal ($1, $3), loc ()) }
| nexp_typ GtEq nexp_typ
@@ -1097,9 +1097,9 @@ nexp_constraint2:
| nexp_typ LtEq nexp_typ
{ NC_aux(NC_bounded_le($1,$3), loc () ) }
| tyvar In Lcurly nums Rcurly
- { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
+ { NC_aux(NC_set($1,$4), loc ()) }
| tyvar IN Lcurly nums Rcurly
- { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
+ { NC_aux(NC_set($1,$4), loc ()) }
| True
{ NC_aux (NC_true, loc ()) }
| False
diff --git a/src/parser2.mly b/src/parser2.mly
index 7ee98f41..3de9b4f4 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -266,7 +266,7 @@ atomic_nc:
| False
{ mk_nc NC_false $startpos $endpos }
| typ Eq typ
- { mk_nc (NC_fixed ($1, $3)) $startpos $endpos }
+ { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
| typ ExclEq typ
{ mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
| nc_lchain
@@ -276,7 +276,7 @@ atomic_nc:
| Lparen nc Rparen
{ $2 }
| kid In Lcurly num_list Rcurly
- { mk_nc (NC_nat_set_bounded ($1, $4)) $startpos $endpos }
+ { mk_nc (NC_set ($1, $4)) $startpos $endpos }
num_list:
| Num
@@ -481,7 +481,7 @@ atomic_typ:
{ let v = mk_kid "n" $startpos $endpos in
let atom_id = mk_id (Id "atom") $startpos $endpos in
let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
- mk_typ (ATyp_exist ([v], NC_aux (NC_nat_set_bounded (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+ mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
| Lcurly kid_list Dot typ Rcurly
{ mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos }
| Lcurly kid_list Comma nc Dot typ Rcurly
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 02cc3574..83c28a7d 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -217,11 +217,11 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
group (parens (nexp ne))
and nexp_constraint (NC_aux(nc,_)) = match nc with
- | NC_fixed(n1,n2) -> doc_op equals (nexp n1) (nexp n2)
+ | NC_equal(n1,n2) -> doc_op equals (nexp n1) (nexp n2)
| NC_not_equal (n1, n2) -> doc_op (string "!=") (nexp n1) (nexp n2)
| NC_bounded_ge(n1,n2) -> doc_op (string ">=") (nexp n1) (nexp n2)
| NC_bounded_le(n1,n2) -> doc_op (string "<=") (nexp n1) (nexp n2)
- | NC_nat_set_bounded(v,bounds) ->
+ | NC_set(v,bounds) ->
doc_op (string "IN") (doc_var v)
(braces (separate_map comma_sp doc_int bounds))
| NC_or (nc1, nc2) ->
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index f0f25795..8de81d4d 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -215,7 +215,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
"(NC_aux " ^
(match nc with
- | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
+ | NC_equal(n1,n2) -> "(NC_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_not_equal(n1,n2) -> "(NC_not_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
@@ -223,7 +223,7 @@ and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
| NC_and(nc1,nc2) -> "(NC_and " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
| NC_true -> "NC_true"
| NC_false -> "NC_false"
- | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^
+ | NC_set(id,bounds) -> "(NC_set " ^
pp_format_var_lem id ^
" [" ^
list_format "; " string_of_int bounds ^
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 2f743e45..0f46afa5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2364,13 +2364,13 @@ let rewrite_constraint =
and rewrite_nc_aux = function
| NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
| NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
- | NC_fixed (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2))
+ | NC_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2))
| NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2))
| NC_and (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "&", rewrite_nc nc2)
| NC_or (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "|", rewrite_nc nc2)
| NC_false -> E_lit (mk_lit L_true)
| NC_true -> E_lit (mk_lit L_false)
- | NC_nat_set_bounded (kid, ints) ->
+ | NC_set (kid, ints) ->
unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (nc_eq (nvar kid) (nconstant int))) nc_true ints))
in
let rewrite_e_aux (E_aux (e_aux, _) as exp) =
diff --git a/src/type_check.ml b/src/type_check.ml
index bfd336d9..3bbd2323 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -153,16 +153,16 @@ 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_fixed (n1, n2) -> nc_neq 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_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)))))
+ | 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 *)
@@ -226,15 +226,15 @@ and nexp_subst_aux sv subst = function
let rec nexp_set_to_or l subst = function
| [] -> typ_error l "Cannot substitute into empty nexp set"
- | [int] -> NC_fixed (subst, nconstant int)
- | (int :: ints) -> NC_or (mk_nc (NC_fixed (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
+ | [int] -> NC_equal (subst, nconstant int)
+ | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
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_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_nat_set_bounded (kid, ints) as set_nc ->
+ | NC_set (kid, ints) as set_nc ->
if Kid.compare kid sv = 0
then nexp_set_to_or l (mk_nexp subst) ints
else set_nc
@@ -777,11 +777,11 @@ end = struct
let rec wf_constraint env (NC_aux (nc, _)) =
match nc with
- | NC_fixed (n1, n2) -> wf_nexp env n1; wf_nexp env n2
+ | 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_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
+ | 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 -> ()
@@ -1065,12 +1065,12 @@ let rec nexp_constraint env var_of (Nexp_aux (nexp, l)) =
let rec nc_constraint env var_of (NC_aux (nc, l)) =
match nc with
- | NC_fixed (nexp1, nexp2) -> Constraint.eq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
+ | NC_equal (nexp1, nexp2) -> Constraint.eq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
| NC_not_equal (nexp1, nexp2) -> Constraint.neq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
| NC_bounded_ge (nexp1, nexp2) -> Constraint.gteq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
| NC_bounded_le (nexp1, nexp2) -> Constraint.lteq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
- | NC_nat_set_bounded (_, []) -> Constraint.literal false
- | NC_nat_set_bounded (kid, (int :: ints)) ->
+ | NC_set (_, []) -> Constraint.literal false
+ | NC_set (kid, (int :: ints)) ->
List.fold_left Constraint.disj
(Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int int)))
(List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int i))) ints)
@@ -1112,10 +1112,10 @@ let prove env (NC_aux (nc_aux, _) as nc) =
| _, _ -> false
in
match nc_aux with
- | NC_fixed (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 = c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
+ | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 = c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
| NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
| NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 >= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
- | NC_fixed (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <> c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
+ | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <> c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
| NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 > c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
| NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 < c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
| NC_true -> true
@@ -1175,7 +1175,7 @@ let rec subtyp_tnf env tnf1 tnf2 =
and tnf_args_eq env arg1 arg2 =
match arg1, arg2 with
- | Tnf_arg_nexp n1, Tnf_arg_nexp n2 -> prove env (NC_aux (NC_fixed (n1, n2), Parse_ast.Unknown))
+ | Tnf_arg_nexp n1, Tnf_arg_nexp n2 -> prove env (NC_aux (NC_equal (n1, n2), Parse_ast.Unknown))
| Tnf_arg_order ord1, Tnf_arg_order ord2 -> order_eq ord1 ord2
| Tnf_arg_typ tnf1, Tnf_arg_typ tnf2 -> subtyp_tnf env tnf1 tnf2 && subtyp_tnf env tnf2 tnf1
| _, _ -> assert false
@@ -1274,7 +1274,7 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
if KidSet.is_empty (KidSet.inter (nexp_frees nexp1) goals)
then
begin
- if prove env (NC_aux (NC_fixed (nexp1, nexp2), Parse_ast.Unknown))
+ if prove env (NC_aux (NC_equal (nexp1, nexp2), Parse_ast.Unknown))
then None
else unify_error l ("Nexp " ^ string_of_nexp nexp1 ^ " and " ^ string_of_nexp nexp2 ^ " are not equal")
end
@@ -1305,7 +1305,7 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
then
begin
match nexp_aux2 with
- | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_fixed (n1a, n2a), Parse_ast.Unknown)) ->
+ | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1a, n2a), Parse_ast.Unknown)) ->
unify_nexps l env goals n1b n2b
| Nexp_constant c2 ->
begin
@@ -1320,7 +1320,7 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
then
begin
match nexp_aux2 with
- | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_fixed (n1b, n2b), Parse_ast.Unknown)) ->
+ | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1b, n2b), Parse_ast.Unknown)) ->
unify_nexps l env goals n1a n2a
| _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:41:29 +0000