From 1b4abb8fdd81f6de2166ef3f064a77fd5622fe83 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 6 May 2026 11:21:22 +0100 Subject: clean up examples vs tests --- examples/alpha_equiv.makkai | 4 ---- examples/equality.makkai | 21 ++++++++++++--------- examples/ext_codomain.makkai | 5 ----- examples/inline_nested.makkai | 9 --------- examples/nested_for.makkai | 3 --- examples/one_simplex.makkai | 2 -- examples/signature_merge.makkai | 12 ------------ examples/signature_param.makkai | 4 ---- examples/tests/test_alpha_equiv.makkai | 4 ++++ examples/tests/test_ext_codomain.makkai | 5 +++++ examples/tests/test_inline_nested.makkai | 9 +++++++++ examples/tests/test_nested_for.makkai | 3 +++ examples/tests/test_signature_merge.makkai | 12 ++++++++++++ examples/tests/test_signature_param.makkai | 4 ++++ 14 files changed, 49 insertions(+), 48 deletions(-) delete mode 100644 examples/alpha_equiv.makkai delete mode 100644 examples/ext_codomain.makkai delete mode 100644 examples/inline_nested.makkai delete mode 100644 examples/nested_for.makkai delete mode 100644 examples/signature_merge.makkai delete mode 100644 examples/signature_param.makkai create mode 100644 examples/tests/test_alpha_equiv.makkai create mode 100644 examples/tests/test_ext_codomain.makkai create mode 100644 examples/tests/test_inline_nested.makkai create mode 100644 examples/tests/test_nested_for.makkai create mode 100644 examples/tests/test_signature_merge.makkai create mode 100644 examples/tests/test_signature_param.makkai diff --git a/examples/alpha_equiv.makkai b/examples/alpha_equiv.makkai deleted file mode 100644 index 2ae067a..0000000 --- a/examples/alpha_equiv.makkai +++ /dev/null @@ -1,4 +0,0 @@ -let signature S = (n : Nat) -> Set -let signature T = (m : Nat) -> Set -let instance i :: S = for (x : Nat), (Nat :: Set) -let instance j :: T = i diff --git a/examples/equality.makkai b/examples/equality.makkai index a9b3368..ede2a54 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -4,16 +4,19 @@ let element pt : Unit = {} let set Three = variant [ zero : Unit | one : Unit | two : Unit ] -let signature EqS = (x : Three) (y: Three) -> theory { E :: Set } -let instance eqThree :: EqS = for (x: Three) (y: Three), { - .E = case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ] - | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ] - | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] - ] +let signature SetWitRelation = theory { + Carrier :: Set, + Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set + +} +let instance eqThree :: SetWitRelation = { + .Carrier = Three :: Set, + .Relation = for (x: Three) (y: Three), + case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ] + | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ] + | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] ] } -let set Diagonal = record { x : Three, y : Three, equal : set-of((eqThree x y) .E) } +let set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) } let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt } - -let element oopsOneEqualsTwo : Diagonal = { .x = one. pt, .y = two. pt, .equal = pt } diff --git a/examples/ext_codomain.makkai b/examples/ext_codomain.makkai deleted file mode 100644 index da0ddae..0000000 --- a/examples/ext_codomain.makkai +++ /dev/null @@ -1,5 +0,0 @@ -let signature S = (x : Nat) -> theory { G :: Set } - -let instance s :: S = for (x : Nat), { .G = (Nat :: Set) } - -let set NatAgain = set-of((s 42) .G) diff --git a/examples/inline_nested.makkai b/examples/inline_nested.makkai deleted file mode 100644 index e891349..0000000 --- a/examples/inline_nested.makkai +++ /dev/null @@ -1,9 +0,0 @@ -let signature Outer = theory { - Inner :: theory { F :: Set } -} - -let instance my_outer :: Outer = { - .Inner = { .F = (Nat :: Set) } -} - -let set MyF = set-of(my_outer .Inner .F) diff --git a/examples/nested_for.makkai b/examples/nested_for.makkai deleted file mode 100644 index b3618cc..0000000 --- a/examples/nested_for.makkai +++ /dev/null @@ -1,3 +0,0 @@ -let signature F = (n : Nat) -> (m : Nat) -> Set -let instance f :: F = for (n : Nat), for (m : Nat), (Nat :: Set) -let set Result = set-of(f 1 2) diff --git a/examples/one_simplex.makkai b/examples/one_simplex.makkai index 590cf04..f7e7bff 100644 --- a/examples/one_simplex.makkai +++ b/examples/one_simplex.makkai @@ -6,8 +6,6 @@ let signature Graph = theory { let set Empty = variant[] let set Unit = record{} let element pt : Unit = {} -let set F1 = variant [ one0 : Unit ] -let set F2 = variant [ two0 : Unit | two1 : Unit ] let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ] let instance oneSimplex :: Graph = { diff --git a/examples/signature_merge.makkai b/examples/signature_merge.makkai deleted file mode 100644 index 5f575d5..0000000 --- a/examples/signature_merge.makkai +++ /dev/null @@ -1,12 +0,0 @@ -let signature S = (n : Nat) -> Set -let signature U = (k : Bool) -> S -let signature W = (k : Bool)(n : Nat) -> Set - -let instance u :: U = for (k : Bool), for (n : Nat), (Nat :: Set) -let instance w :: W = u - -let signature F = (n : Nat) (m : Nat) -> Set -let signature G = (n : Nat) -> (m : Nat) -> Set - -let instance f :: F = for (n : Nat) (m : Nat), (Nat :: Set) -let instance g :: G = f diff --git a/examples/signature_param.makkai b/examples/signature_param.makkai deleted file mode 100644 index 9dae31b..0000000 --- a/examples/signature_param.makkai +++ /dev/null @@ -1,4 +0,0 @@ -let signature S = theory { - F :: (x : Nat) (y : Bool) -> Set, - G :: (z : set-of(F 3 4)) -> Set // this sould fail -} diff --git a/examples/tests/test_alpha_equiv.makkai b/examples/tests/test_alpha_equiv.makkai new file mode 100644 index 0000000..2ae067a --- /dev/null +++ b/examples/tests/test_alpha_equiv.makkai @@ -0,0 +1,4 @@ +let signature S = (n : Nat) -> Set +let signature T = (m : Nat) -> Set +let instance i :: S = for (x : Nat), (Nat :: Set) +let instance j :: T = i diff --git a/examples/tests/test_ext_codomain.makkai b/examples/tests/test_ext_codomain.makkai new file mode 100644 index 0000000..da0ddae --- /dev/null +++ b/examples/tests/test_ext_codomain.makkai @@ -0,0 +1,5 @@ +let signature S = (x : Nat) -> theory { G :: Set } + +let instance s :: S = for (x : Nat), { .G = (Nat :: Set) } + +let set NatAgain = set-of((s 42) .G) diff --git a/examples/tests/test_inline_nested.makkai b/examples/tests/test_inline_nested.makkai new file mode 100644 index 0000000..e891349 --- /dev/null +++ b/examples/tests/test_inline_nested.makkai @@ -0,0 +1,9 @@ +let signature Outer = theory { + Inner :: theory { F :: Set } +} + +let instance my_outer :: Outer = { + .Inner = { .F = (Nat :: Set) } +} + +let set MyF = set-of(my_outer .Inner .F) diff --git a/examples/tests/test_nested_for.makkai b/examples/tests/test_nested_for.makkai new file mode 100644 index 0000000..b3618cc --- /dev/null +++ b/examples/tests/test_nested_for.makkai @@ -0,0 +1,3 @@ +let signature F = (n : Nat) -> (m : Nat) -> Set +let instance f :: F = for (n : Nat), for (m : Nat), (Nat :: Set) +let set Result = set-of(f 1 2) diff --git a/examples/tests/test_signature_merge.makkai b/examples/tests/test_signature_merge.makkai new file mode 100644 index 0000000..5f575d5 --- /dev/null +++ b/examples/tests/test_signature_merge.makkai @@ -0,0 +1,12 @@ +let signature S = (n : Nat) -> Set +let signature U = (k : Bool) -> S +let signature W = (k : Bool)(n : Nat) -> Set + +let instance u :: U = for (k : Bool), for (n : Nat), (Nat :: Set) +let instance w :: W = u + +let signature F = (n : Nat) (m : Nat) -> Set +let signature G = (n : Nat) -> (m : Nat) -> Set + +let instance f :: F = for (n : Nat) (m : Nat), (Nat :: Set) +let instance g :: G = f diff --git a/examples/tests/test_signature_param.makkai b/examples/tests/test_signature_param.makkai new file mode 100644 index 0000000..9dae31b --- /dev/null +++ b/examples/tests/test_signature_param.makkai @@ -0,0 +1,4 @@ +let signature S = theory { + F :: (x : Nat) (y : Bool) -> Set, + G :: (z : set-of(F 3 4)) -> Set // this sould fail +} -- cgit v1.3.1