From bcb579eafc65e93bda208386d65bd4abeca575cb Mon Sep 17 00:00:00 2001
From: Olivier <olivier.martinot@inria.fr>
Date: Wed, 18 Jan 2023 15:04:44 +0100
Subject: [PATCH] Change 'int' to more correct 'nat' in the test suite.
---
client/test/TestF.ml | 154 +++++++++++++++++++++----------------------
1 file changed, 77 insertions(+), 77 deletions(-)
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index f5ab310..20a2246 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -248,29 +248,29 @@ let bool_env =
let bool_datatype =
Datatype.Type "bool", []
-let int_env =
- let int_typedecl =
+let nat_env =
+ let nat_typedecl =
let open Datatype in {
- name = Type "int";
+ name = Type "nat";
type_params = [];
data_kind = Variant;
labels_descr = [
{
label_name = Label "O";
- type_name = Type "int";
+ type_name = Type "nat";
arg_type = F.TyProduct [];
} ; {
label_name = Label "S";
- type_name = Type "int";
- arg_type = F.TyConstr (Type "int", []);
+ type_name = Type "nat";
+ arg_type = F.TyConstr (Type "nat", []);
}
]
}
in
- Datatype.Env.add_decl bool_env int_typedecl
+ Datatype.Env.add_decl bool_env nat_typedecl
-let int_datatype =
- Datatype.Type "int", []
+let nat_datatype =
+ Datatype.Type "nat", []
(* small gadt *)
let small_gadt_env =
@@ -282,9 +282,9 @@ let small_gadt_env =
data_kind = Variant;
labels_descr = [
{
- label_name = Label "Int";
+ label_name = Label "Nat";
type_name = Type "ty";
- arg_type = F.TyEq (F.TyVar alpha, F.TyConstr int_datatype);
+ arg_type = F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype);
} ; {
label_name = Label "Bool";
type_name = Type "ty";
@@ -293,11 +293,11 @@ let small_gadt_env =
];
}
in
- Datatype.Env.add_decl int_env small_gadt_typedecl
+ Datatype.Env.add_decl nat_env small_gadt_typedecl
-let int_pattern arg_type pat =
+let nat_pattern arg_type pat =
pvariant
- (Datatype.Label "Int")
+ (Datatype.Label "Nat")
(Datatype.Type "ty", arg_type)
pat
@@ -322,42 +322,42 @@ let mu_under_forall =
(*
Λα.
- λ(w : Eq(α,int)).
+ λ(w : Eq(α,nat)).
use w in
( O : α )
*)
let cast =
let alpha = 0 in
tyabs alpha @@
- abs "w" (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype)) @@
+ abs "w" (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype)) @@
use (var "w") @@
- annot (variant (Datatype.Label "O") int_datatype unit) (F.TyVar alpha)
+ annot (variant (Datatype.Label "O") nat_datatype unit) (F.TyVar alpha)
(*
Λα.
λ(n : α ty).
match_α n with
- | Int p ->
- use (p : Eq(α,int)) in (O : α)
+ | Nat p ->
+ use (p : Eq(α,nat)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α)
*)
let match_gadt_default =
let alpha = 0 in
- let int_pat =
- int_pattern [F.TyVar alpha] (pvar "p")
+ let nat_pat =
+ nat_pattern [F.TyVar alpha] (pvar "p")
in
- let int_payoff =
+ let nat_payoff =
use
(annot
(var "p")
- (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype)))
+ (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype)))
(annot
(variant
(Datatype.Label "O")
- int_datatype
+ nat_datatype
unit)
(F.TyVar alpha))
in
@@ -381,7 +381,7 @@ let match_gadt_default =
tyabs alpha @@
abs "n" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
match_ (F.TyVar alpha) (var "n") [
- (int_pat , int_payoff);
+ (nat_pat , nat_payoff);
(bool_pat , bool_payoff)
]
@@ -389,27 +389,27 @@ let match_gadt_default =
(Λα.
λ(n : α ty).
match_α n with
- | Int p ->
- use (p : Eq(α,int)) in (O : α)
+ | Nat p ->
+ use (p : Eq(α,nat)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α))
-int
-(Int (refl_int))
+nat
+(Nat (refl_nat))
*)
-let default_int =
+let default_nat =
app
- (tyapp match_gadt_default (F.TyConstr int_datatype))
+ (tyapp match_gadt_default (F.TyConstr nat_datatype))
(variant
- (Datatype.Label "Int")
- (Datatype.Type "ty", [F.TyConstr int_datatype])
- (refl (F.TyConstr int_datatype)))
+ (Datatype.Label "Nat")
+ (Datatype.Type "ty", [F.TyConstr nat_datatype])
+ (refl (F.TyConstr nat_datatype)))
(*
(Λα.
λ(n : α ty).
match_α n with
- | Int p ->
- use (p : Eq(α,int)) in (O : α)
+ | Nat p ->
+ use (p : Eq(α,nat)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α))
bool
@@ -427,8 +427,8 @@ let default_bool =
(Λα.
λ(n : α ty).
match_α n with
- | Int p ->
- use (p : Eq(α,int)) in (O : α)
+ | Nat p ->
+ use (p : Eq(α,nat)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α))
bool
@@ -437,16 +437,16 @@ bool
let default_absurd_wrong =
let alpha = 0 in
- let int_pat =
- int_pattern [F.TyVar alpha] (pvar "p")
+ let nat_pat =
+ nat_pattern [F.TyVar alpha] (pvar "p")
in
- let int_payoff =
- use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype))) @@
+ let nat_payoff =
+ use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype))) @@
annot
(variant
(Datatype.Label "O")
- int_datatype
+ nat_datatype
(absurd unit_type))
(F.TyVar alpha)
in
@@ -468,7 +468,7 @@ let default_absurd_wrong =
tyabs alpha @@
abs "n" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
match_ (F.TyVar alpha) (var "n") [
- (int_pat , int_payoff);
+ (nat_pat , nat_payoff);
(bool_pat , bool_payoff)
]
@@ -477,13 +477,13 @@ let default_absurd_wrong =
λ(x : α ty).
λ(y : α ty).
match (x, y) with
- | (Int p1, Int p2) ->
+ | (Nat p1, Nat p2) ->
payoff1
| (Bool p1, Bool p2) ->
payoff2
- | (Int p1, Bool p2) ->
+ | (Nat p1, Bool p2) ->
payoff3
- | (Bool p1, Int p2) ->
+ | (Bool p1, Nat p2) ->
payoff4
*)
let test_absurd payoff1 payoff2 payoff3 payoff4 =
@@ -506,15 +506,15 @@ let test_absurd payoff1 payoff2 payoff3 payoff4 =
in
(*
- (Int p1, Int p2) ->
- use (p1 : Eq(α,int)) in use (p2 : Eq(α,int)) in payoff1
+ (Nat p1, Nat p2) ->
+ use (p1 : Eq(α,nat)) in use (p2 : Eq(α,nat)) in payoff1
*)
- let int_int_branch =
+ let nat_nat_branch =
ptuple [
- (variant_ty "Int" (pvar "p1"));
- (variant_ty "Int" (pvar "p2"));
+ (variant_ty "Nat" (pvar "p1"));
+ (variant_ty "Nat" (pvar "p2"));
] ,
- double_use int_datatype int_datatype payoff1
+ double_use nat_datatype nat_datatype payoff1
(*
(Bool p1, Bool p2) ->
@@ -528,36 +528,36 @@ let test_absurd payoff1 payoff2 payoff3 payoff4 =
double_use bool_datatype bool_datatype payoff2
(*
- (Int p1, Bool p2) ->
- use (p1 : Eq(α,int)) in use (p2 : Eq(α,bool)) in payoff3
+ (Nat p1, Bool p2) ->
+ use (p1 : Eq(α,nat)) in use (p2 : Eq(α,bool)) in payoff3
*)
- and int_bool_branch =
+ and nat_bool_branch =
ptuple [
- (variant_ty "Int" (pvar "p1"));
+ (variant_ty "Nat" (pvar "p1"));
(variant_ty "Bool" (pvar "p2"));
] ,
- double_use int_datatype bool_datatype payoff3
+ double_use nat_datatype bool_datatype payoff3
(*
- (Bool p1, Int p2) ->
- use (p1 : Eq(α,bool)) in use (p2 : Eq(α,int)) in payoff4
+ (Bool p1, Nat p2) ->
+ use (p1 : Eq(α,bool)) in use (p2 : Eq(α,nat)) in payoff4
*)
- and bool_int_branch =
+ and bool_nat_branch =
ptuple [
(variant_ty "Bool" (pvar "p1"));
- (variant_ty "Int" (pvar "p2"));
+ (variant_ty "Nat" (pvar "p2"));
] ,
- double_use bool_datatype int_datatype payoff4
+ double_use bool_datatype nat_datatype payoff4
in
tyabs alpha @@
abs "x" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
abs "y" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
match_ unit_type (tuple [ var "x"; var "y" ]) [
- int_int_branch ;
+ nat_nat_branch ;
bool_bool_branch;
- int_bool_branch;
- bool_int_branch;
+ nat_bool_branch;
+ bool_nat_branch;
]
(*
@@ -565,13 +565,13 @@ let test_absurd payoff1 payoff2 payoff3 payoff4 =
λ(x : α ty).
λ(y : α ty).
match (x, y) with
- | (Int p1, Int p2) ->
+ | (Nat p1, Nat p2) ->
()
| (Bool p1, Bool p2) ->
()
- | (Int p1, Bool p2) ->
+ | (Nat p1, Bool p2) ->
.
- | (Bool p1, Int p2) ->
+ | (Bool p1, Nat p2) ->
.
*)
(* This example is ok : the two last branches are unreachable. *)
@@ -588,13 +588,13 @@ let test_absurd_ok =
λ(x : α ty).
λ(y : α ty).
match (x, y) with
- | (Int p1, Int p2) ->
+ | (Nat p1, Nat p2) ->
()
| (Bool p1, Bool p2) ->
()
- | (Int p1, Bool p2) ->
+ | (Nat p1, Bool p2) ->
()
- | (Bool p1, Int p2) ->
+ | (Bool p1, Nat p2) ->
()
*)
(* This example is ok : the two last branches are unreachable, but it is not
@@ -611,13 +611,13 @@ let test_absurd_ok2 =
λ(x : α ty).
λ(y : α ty).
match (x, y) with
- | (Int p1, Int p2) ->
+ | (Nat p1, Nat p2) ->
.
| (Bool p1, Bool p2) ->
.
- | (Int p1, Bool p2) ->
+ | (Nat p1, Bool p2) ->
.
- | (Bool p1, Int p2) ->
+ | (Bool p1, Nat p2) ->
.
*)
(* This example is wrong : the first two branches are reachable, i.e. they
@@ -656,9 +656,9 @@ let test_suite =
test_ok_from_ast "symmetry" Datatype.Env.empty sym;
test_ok_from_ast "transitivity" Datatype.Env.empty trans;
test_ok_from_ast "mu under forall" Datatype.Env.empty mu_under_forall;
- test_ok_from_ast "cast" int_env cast;
+ test_ok_from_ast "cast" nat_env cast;
test_ok_from_ast "default" small_gadt_env match_gadt_default;
- test_ok_from_ast "default int" small_gadt_env default_int;
+ test_ok_from_ast "default nat" small_gadt_env default_nat;
test_ok_from_ast "default bool" small_gadt_env default_bool;
test_type_error "default absurd wrong" small_gadt_env default_absurd_wrong;
test_ok_from_ast "pair of gadt" small_gadt_env test_absurd_ok;
--
GitLab