Skip to content

Commit 1904885

Browse files
HeinrichApfelmusHeinrichApfelmus
committed
wip Add fine-types-core package with Agda proofs
1 parent 7c7646a commit 1904885

File tree

18 files changed

+1081
-0
lines changed

18 files changed

+1081
-0
lines changed

‎.gitignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,10 @@
1515
*.hp
1616
*.eventlog
1717

18+
### agda2hs ###
19+
_build
20+
*.agdai
21+
1822
### Cabal ###
1923
dist
2024
dist-*

‎lib/fine-types-core/CHANGELOG.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
# Revision history for fine-types-core
2+
3+
## 0.1.0.0 -- YYYY-mm-dd
4+
5+
* First version. Released on an unsuspecting world.

‎lib/fine-types-core/README.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
[FineTypes][] is an interface description language (IDL) focussing on types.
2+
3+
[finetypes]: https://github.com/cardano-foundation/fine-types
4+
5+
The `fine-types-core` package defines the core data types and functions — and it includes machine-checked proofs!
6+
7+
The proofs are written in Agda and the code is exported to Haskell using [agda2hs][].
8+
9+
The repository layout includes:
10+
11+
* `./src/agda` — Agda source code with proofs.
12+
* `./src/haskell` — Haskell source code that was **autogenerated** from the Agda code. These files are still checked into the repository.
13+
* `./generate-haskell.sh` — Script which uses [agda2hs][] to generate the Haskell source code. Run this script whenever you change the Agda source.
14+
15+
[agda2hs]: https://github.com/agda/agda2hs

‎lib/fine-types-core/fine-types-core.agda-lib‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
name: fine-types-core
2+
include: ./src/agda
3+
depend: agda2hs, standard-library

‎lib/fine-types-core/fine-types-core.cabal‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
cabal-version: 3.0
2+
name: fine-types-core
3+
version: 0.1.0.0
4+
synopsis: A interface description language (IDL) focusing on types
5+
description: Core definitions and proofs for fine-types.
6+
homepage: https://github.com/cardano-foundation/fine-types
7+
license: Apache-2.0
8+
license-file: LICENSE
9+
author: HAL, Cardano Foundation
10+
maintainer: hal@cardanofoundation.org
11+
copyright: 2023 Cardano Foundation
12+
category: Language
13+
14+
extra-doc-files:
15+
CHANGELOG.md
16+
extra-source-files:
17+
generate-haskell.sh
18+
fine-types-core.agda-lib
19+
src/agda/**/*.agda
20+
21+
common language
22+
default-language:
23+
Haskell2010
24+
default-extensions:
25+
NoImplicitPrelude
26+
other-extensions:
27+
NamedFieldPuns
28+
OverloadedStrings
29+
30+
common opts-lib
31+
ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates
32+
33+
if flag(release)
34+
ghc-options: -O2 -Werror
35+
36+
common opts-exe
37+
ghc-options: -threaded -rtsopts
38+
ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates
39+
40+
if flag(release)
41+
ghc-options: -O2 -Werror
42+
43+
flag release
44+
description: Enable optimization and `-Werror`
45+
default: False
46+
manual: True
47+
48+
library
49+
import: language, opts-lib
50+
hs-source-dirs:
51+
src/haskell
52+
build-depends:
53+
, base >=4.14.3.0
54+
, containers
55+
, deepseq >= 1.4.4
56+
, QuickCheck
57+
exposed-modules:
58+
Data.Embedding
59+
Language.FineTypes
60+
Language.FineTypes.Embedding
61+
Language.FineTypes.Typ
62+
Language.FineTypes.Value.Def
63+
Language.FineTypes.Value.Typcheck

‎lib/fine-types-core/generate-haskell.sh‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#!/bin/sh
2+
agda2hs ./src/agda/Language/FineTypes.agda -o ./src/haskell/
3+
# agda2hs -v agda2hs.compile:7 ./src/agda/Language/FineTypes.agda -o ./src/haskell/

‎lib/fine-types-core/src/agda/Data/Embedding.agda‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
module Data.Embedding where
2+
3+
{-# FOREIGN AGDA2HS
4+
-- !!! This Haskell module has been autogenerated by agda2hs.
5+
-- !!! Do NOT change; change the original .agda file instead.
6+
#-}
7+
8+
open import Haskell.Prelude
9+
10+
{-----------------------------------------------------------------------------
11+
Embedding
12+
------------------------------------------------------------------------------}
13+
record Embedding (a b : Set) : Set where
14+
field
15+
to : a → b
16+
from : b → a
17+
@0 from∘to : ∀ (x : a) → from (to x) ≡ x
18+
19+
open Embedding public
20+
21+
{-# COMPILE AGDA2HS Embedding #-}

‎lib/fine-types-core/src/agda/Language/FineTypes.agda‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
module Language.FineTypes where
2+
3+
{-# FOREIGN AGDA2HS
4+
-- !!! This Haskell module has been autogenerated by agda2hs.
5+
-- !!! Do NOT change; change the original .agda file instead.
6+
#-}
7+
8+
import Data.Embedding
9+
import Language.FineTypes.Typ
10+
import Language.FineTypes.Value.Def
11+
import Language.FineTypes.Embedding
12+
-- import Language.FineTypes.Value.Typcheck

‎lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
module Language.FineTypes.Embedding where
2+
3+
{-# FOREIGN AGDA2HS
4+
-- !!! This Haskell module has been autogenerated by agda2hs.
5+
-- !!! Do NOT change; change the original .agda file instead.
6+
#-}
7+
8+
open import Haskell.Prelude hiding (_×_; _+_; Pair)
9+
open import Relation.Nullary using (¬_)
10+
11+
open import Data.Embedding
12+
open import Language.FineTypes.Value.Def
13+
open import Language.FineTypes.Typ
14+
using (Typ; _+_; _×_)
15+
16+
import Language.FineTypes.Typ as Typ
17+
18+
{-----------------------------------------------------------------------------
19+
Embedding with Typ information
20+
------------------------------------------------------------------------------}
21+
record EmbeddingTyp (@0 A B : Typ) : Set where
22+
field
23+
embed : Embedding (Value A) (Value B)
24+
typcheck : Typ → Maybe Typ
25+
@0 accepts : typcheck A ≡ Just B
26+
@0 rejects : ∀ (C : Typ) → typcheck C ≡ Nothing → ¬(C ≡ A)
27+
28+
open EmbeddingTyp public
29+
30+
{-# COMPILE AGDA2HS EmbeddingTyp #-}
31+
32+
{-----------------------------------------------------------------------------
33+
Specific Embeddings
34+
------------------------------------------------------------------------------}
35+
distributeVal
36+
: ∀ {@0 A B C : Typ}
37+
→ Embedding
38+
(Value ((A + B) × C))
39+
(Value ((A × C) + (B × C)))
40+
distributeVal =
41+
record
42+
{ to = λ
43+
{ (Product2 (Sum2L a) c) → Sum2L (Product2 a c)
44+
; (Product2 (Sum2R b) c) → Sum2R (Product2 b c)
45+
}
46+
; from = λ
47+
{ (Sum2L (Product2 a c)) → (Product2 (Sum2L a) c)
48+
; (Sum2R (Product2 b c)) → (Product2 (Sum2R b) c)
49+
}
50+
; from∘to = λ
51+
{ (Product2 (Sum2L a) c) → refl
52+
; (Product2 (Sum2R b) c) → refl
53+
}
54+
}
55+
56+
{-# COMPILE AGDA2HS distributeVal #-}
57+
58+
distribute
59+
: ∀ {@0 A B C : Typ}
60+
→ EmbeddingTyp
61+
((A + B) × C)
62+
((A × C) + (B × C))
63+
distribute =
64+
record
65+
{ embed = distributeVal
66+
; typcheck = λ
67+
{ (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 a b) c)
68+
→ Just (Typ.Two Typ.Sum2 (Typ.Two Typ.Product2 a c) (Typ.Two Typ.Product2 b c))
69+
; _ → Nothing
70+
}
71+
; accepts = refl
72+
; rejects = λ
73+
{ (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 _ _) _) → λ ()
74+
}
75+
}
76+
77+
{-# COMPILE AGDA2HS distribute #-}

‎lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
module Language.FineTypes.Typ where
2+
3+
{-# FOREIGN AGDA2HS
4+
-- !!! This Haskell module has been autogenerated by agda2hs.
5+
-- !!! Do NOT change; change the original .agda file instead.
6+
#-}
7+
8+
open import Haskell.Prelude
9+
using (String; List; True; False)
10+
renaming (_×_ to Pair)
11+
open import Haskell.Law.Eq
12+
open import Haskell.Prim.Eq
13+
14+
import Haskell.Prelude as Hs
15+
16+
ConstructorName = String
17+
FieldName = String
18+
TypName = String
19+
VarName = String
20+
21+
{-# COMPILE AGDA2HS ConstructorName #-}
22+
{-# COMPILE AGDA2HS FieldName #-}
23+
{-# COMPILE AGDA2HS TypName #-}
24+
{-# COMPILE AGDA2HS VarName #-}
25+
26+
{-----------------------------------------------------------------------------
27+
Haskell - Typ
28+
------------------------------------------------------------------------------}
29+
data TypConst : Set where
30+
Bool : TypConst
31+
Bytes : TypConst
32+
Integer : TypConst
33+
Natural : TypConst
34+
Text : TypConst
35+
Rational : TypConst
36+
Unit : TypConst
37+
38+
data OpOne : Set where
39+
Option : OpOne
40+
Sequence : OpOne
41+
PowerSet : OpOne
42+
43+
data OpTwo : Set where
44+
Sum2 : OpTwo
45+
Product2 : OpTwo
46+
PartialFunction : OpTwo
47+
FiniteSupport : OpTwo
48+
49+
data Constraint1 : Set where
50+
Braces : List Constraint1 → Constraint1
51+
Token : String → Constraint1
52+
53+
Constraint = List Constraint1
54+
55+
data Typ : Set where
56+
Var : TypName → Typ
57+
Zero : TypConst → Typ
58+
One : OpOne → Typ → Typ
59+
Two : OpTwo → Typ → Typ → Typ
60+
ProductN : List (Pair FieldName Typ) → Typ
61+
SumN : List (Pair ConstructorName Typ) → Typ
62+
Constrained : VarName → Typ → Constraint → Typ
63+
64+
{-# COMPILE AGDA2HS TypConst #-}
65+
{-# COMPILE AGDA2HS OpOne #-}
66+
{-# COMPILE AGDA2HS OpTwo #-}
67+
{-# COMPILE AGDA2HS Constraint1 #-}
68+
{-# COMPILE AGDA2HS Constraint #-}
69+
{-# COMPILE AGDA2HS Typ #-}
70+
71+
{-----------------------------------------------------------------------------
72+
Agda - Equality
73+
------------------------------------------------------------------------------}
74+
instance
75+
iTypConst : Eq TypConst
76+
iTypConst ._==_ Bool Bool = True
77+
iTypConst ._==_ Bytes Bytes = True
78+
iTypConst ._==_ Integer Integer = True
79+
iTypConst ._==_ Natural Natural = True
80+
iTypConst ._==_ Text Text = True
81+
iTypConst ._==_ Rational Rational = True
82+
iTypConst ._==_ Unit Unit = True
83+
iTypConst ._==_ _ _ = Hs.False
84+
85+
{-# COMPILE AGDA2HS iTypConst derive #-}
86+
87+
-- Created by automati case splitting C^c C^c
88+
-- and automatic goal finding C^c C^a
89+
instance
90+
iLawfulEqTypConst : IsLawfulEq TypConst
91+
92+
iLawfulEqTypConst .isEquality Bool Bool = Hs.ofY Hs.refl
93+
iLawfulEqTypConst .isEquality Bool Bytes = Hs.ofN (λ ())
94+
iLawfulEqTypConst .isEquality Bool Integer = Hs.ofN (λ ())
95+
iLawfulEqTypConst .isEquality Bool Natural = Hs.ofN (λ ())
96+
iLawfulEqTypConst .isEquality Bool Text = Hs.ofN (λ ())
97+
iLawfulEqTypConst .isEquality Bool Rational = Hs.ofN (λ ())
98+
iLawfulEqTypConst .isEquality Bool Unit = Hs.ofN (λ ())
99+
iLawfulEqTypConst .isEquality Bytes Bool = Hs.ofN (λ ())
100+
iLawfulEqTypConst .isEquality Bytes Bytes = Hs.ofY Hs.refl
101+
iLawfulEqTypConst .isEquality Bytes Integer = Hs.ofN (λ ())
102+
iLawfulEqTypConst .isEquality Bytes Natural = Hs.ofN (λ ())
103+
iLawfulEqTypConst .isEquality Bytes Text = Hs.ofN (λ ())
104+
iLawfulEqTypConst .isEquality Bytes Rational = Hs.ofN (λ ())
105+
iLawfulEqTypConst .isEquality Bytes Unit = Hs.ofN (λ ())
106+
iLawfulEqTypConst .isEquality Integer Bool = Hs.ofN (λ ())
107+
iLawfulEqTypConst .isEquality Integer Bytes = Hs.ofN (λ ())
108+
iLawfulEqTypConst .isEquality Integer Integer = Hs.ofY Hs.refl
109+
iLawfulEqTypConst .isEquality Integer Natural = Hs.ofN (λ ())
110+
iLawfulEqTypConst .isEquality Integer Text = Hs.ofN (λ ())
111+
iLawfulEqTypConst .isEquality Integer Rational = Hs.ofN (λ ())
112+
iLawfulEqTypConst .isEquality Integer Unit = Hs.ofN (λ ())
113+
iLawfulEqTypConst .isEquality Natural Bool = Hs.ofN (λ ())
114+
iLawfulEqTypConst .isEquality Natural Bytes = Hs.ofN (λ ())
115+
iLawfulEqTypConst .isEquality Natural Integer = Hs.ofN (λ ())
116+
iLawfulEqTypConst .isEquality Natural Natural = Hs.ofY Hs.refl
117+
iLawfulEqTypConst .isEquality Natural Text = Hs.ofN (λ ())
118+
iLawfulEqTypConst .isEquality Natural Rational = Hs.ofN (λ ())
119+
iLawfulEqTypConst .isEquality Natural Unit = Hs.ofN (λ ())
120+
iLawfulEqTypConst .isEquality Text Bool = Hs.ofN (λ ())
121+
iLawfulEqTypConst .isEquality Text Bytes = Hs.ofN (λ ())
122+
iLawfulEqTypConst .isEquality Text Integer = Hs.ofN (λ ())
123+
iLawfulEqTypConst .isEquality Text Natural = Hs.ofN (λ ())
124+
iLawfulEqTypConst .isEquality Text Text = Hs.ofY Hs.refl
125+
iLawfulEqTypConst .isEquality Text Rational = Hs.ofN (λ ())
126+
iLawfulEqTypConst .isEquality Text Unit = Hs.ofN (λ ())
127+
iLawfulEqTypConst .isEquality Rational Bool = Hs.ofN (λ ())
128+
iLawfulEqTypConst .isEquality Rational Bytes = Hs.ofN (λ ())
129+
iLawfulEqTypConst .isEquality Rational Integer = Hs.ofN (λ ())
130+
iLawfulEqTypConst .isEquality Rational Natural = Hs.ofN (λ ())
131+
iLawfulEqTypConst .isEquality Rational Text = Hs.ofN (λ ())
132+
iLawfulEqTypConst .isEquality Rational Rational = Hs.ofY Hs.refl
133+
iLawfulEqTypConst .isEquality Rational Unit = Hs.ofN (λ ())
134+
iLawfulEqTypConst .isEquality Unit Bool = Hs.ofN (λ ())
135+
iLawfulEqTypConst .isEquality Unit Bytes = Hs.ofN (λ ())
136+
iLawfulEqTypConst .isEquality Unit Integer = Hs.ofN (λ ())
137+
iLawfulEqTypConst .isEquality Unit Natural = Hs.ofN (λ ())
138+
iLawfulEqTypConst .isEquality Unit Text = Hs.ofN (λ ())
139+
iLawfulEqTypConst .isEquality Unit Rational = Hs.ofN (λ ())
140+
iLawfulEqTypConst .isEquality Unit Unit = Hs.ofY Hs.refl
141+
142+
{-----------------------------------------------------------------------------
143+
Agda - Syntactic sugar
144+
------------------------------------------------------------------------------}
145+
_×_ : Typ → Typ → Typ
146+
A × B = Two Product2 A B
147+
148+
_+_ : Typ → Typ → Typ
149+
A + B = Two Sum2 A B

0 commit comments

Comments
 (0)