Skip to content

Commit

Permalink
wip Add fine-types-core package with Agda proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
HeinrichApfelmus committed Dec 1, 2023
1 parent 5b8107e commit 8064570
Show file tree
Hide file tree
Showing 18 changed files with 1,093 additions and 0 deletions.
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,10 @@
*.hp
*.eventlog

### agda2hs ###
_build
*.agdai

### Cabal ###
dist
dist-*
Expand Down
5 changes: 5 additions & 0 deletions lib/fine-types-core/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
# Revision history for fine-types-core

## 0.1.0.0 -- YYYY-mm-dd

* First version. Released on an unsuspecting world.
15 changes: 15 additions & 0 deletions lib/fine-types-core/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
[FineTypes][] is an interface description language (IDL) focussing on types.

[finetypes]: https://github.com/cardano-foundation/fine-types

The `fine-types-core` package defines the core data types and functions — and it includes machine-checked proofs!

The proofs are written in Agda and the code is exported to Haskell using [agda2hs][].

The repository layout includes:

* `./src/agda` — Agda source code with proofs.
* `./src/haskell` — Haskell source code that was **autogenerated** from the Agda code. These files are still checked into the repository.
* `./generate-haskell.sh` — Script which uses [agda2hs][] to generate the Haskell source code. Run this script whenever you change the Agda source.

[agda2hs]: https://github.com/agda/agda2hs
6 changes: 6 additions & 0 deletions lib/fine-types-core/fine-types-core.agda-lib
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
name: fine-types-core
include: src/agda
depend:
standard-library
agda2hs
flags: -W noUnsupportedIndexedMatch --erasure
63 changes: 63 additions & 0 deletions lib/fine-types-core/fine-types-core.cabal
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
cabal-version: 3.0
name: fine-types-core
version: 0.1.0.0
synopsis: A interface description language (IDL) focusing on types
description: Core definitions and proofs for fine-types.
homepage: https://github.com/cardano-foundation/fine-types
license: Apache-2.0
license-file: LICENSE
author: HAL, Cardano Foundation
maintainer: hal@cardanofoundation.org
copyright: 2023 Cardano Foundation
category: Language

extra-doc-files:
CHANGELOG.md
extra-source-files:
generate-haskell.sh
fine-types-core.agda-lib
src/agda/**/*.agda

common language
default-language:
Haskell2010
default-extensions:
NoImplicitPrelude
other-extensions:
NamedFieldPuns
OverloadedStrings

common opts-lib
ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates

if flag(release)
ghc-options: -O2 -Werror

common opts-exe
ghc-options: -threaded -rtsopts
ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates

if flag(release)
ghc-options: -O2 -Werror

flag release
description: Enable optimization and `-Werror`
default: False
manual: True

library
import: language, opts-lib
hs-source-dirs:
src/haskell
build-depends:
, base >=4.14.3.0
, containers
, deepseq >= 1.4.4
, QuickCheck
exposed-modules:
Data.Embedding
Language.FineTypes
Language.FineTypes.Embedding
Language.FineTypes.Typ
Language.FineTypes.Value.Def
Language.FineTypes.Value.Typcheck
6 changes: 6 additions & 0 deletions lib/fine-types-core/generate-haskell.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
#!/bin/sh
agda2hs \
--no-default-libraries \
-o ./src/haskell/ \
./src/agda/Language/FineTypes.agda
# agda2hs -v agda2hs.compile:7 ./src/agda/Language/FineTypes.agda -o ./src/haskell/
21 changes: 21 additions & 0 deletions lib/fine-types-core/src/agda/Data/Embedding.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
module Data.Embedding where

{-# FOREIGN AGDA2HS
-- !!! This Haskell module has been autogenerated by agda2hs.
-- !!! Do NOT change; change the original .agda file instead.
#-}

open import Haskell.Prelude

{-----------------------------------------------------------------------------
Embedding
------------------------------------------------------------------------------}
record Embedding (a b : Set) : Set where
field
to : a b
from : b a
@0 from∘to : (x : a) from (to x) ≡ x

open Embedding public

{-# COMPILE AGDA2HS Embedding #-}
12 changes: 12 additions & 0 deletions lib/fine-types-core/src/agda/Language/FineTypes.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
module Language.FineTypes where

{-# FOREIGN AGDA2HS
-- !!! This Haskell module has been autogenerated by agda2hs.
-- !!! Do NOT change; change the original .agda file instead.
#-}

import Data.Embedding
import Language.FineTypes.Typ
import Language.FineTypes.Value.Def
import Language.FineTypes.Embedding
-- import Language.FineTypes.Value.Typcheck
77 changes: 77 additions & 0 deletions lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
module Language.FineTypes.Embedding where

{-# FOREIGN AGDA2HS
-- !!! This Haskell module has been autogenerated by agda2hs.
-- !!! Do NOT change; change the original .agda file instead.
#-}

open import Haskell.Prelude hiding (_×_; _+_; Pair)
open import Relation.Nullary using (¬_)

open import Data.Embedding
open import Language.FineTypes.Value.Def
open import Language.FineTypes.Typ
using (Typ; _+_; _×_)

import Language.FineTypes.Typ as Typ

{-----------------------------------------------------------------------------
Embedding with Typ information
------------------------------------------------------------------------------}
record EmbeddingTyp (@0 A B : Typ) : Set where
field
embed : Embedding (Value A) (Value B)
typcheck : Typ Maybe Typ
@0 accepts : typcheck A ≡ Just B
@0 rejects : (C : Typ) typcheck C ≡ Nothing ¬(C ≡ A)

open EmbeddingTyp public

{-# COMPILE AGDA2HS EmbeddingTyp #-}

{-----------------------------------------------------------------------------
Specific Embeddings
------------------------------------------------------------------------------}
distributeVal
: {@0 A B C : Typ}
Embedding
(Value ((A + B) × C))
(Value ((A × C) + (B × C)))
distributeVal =
record
{ to = λ
{ (Product2 (Sum2L a) c) Sum2L (Product2 a c)
; (Product2 (Sum2R b) c) Sum2R (Product2 b c)
}
; from = λ
{ (Sum2L (Product2 a c)) (Product2 (Sum2L a) c)
; (Sum2R (Product2 b c)) (Product2 (Sum2R b) c)
}
; from∘to = λ
{ (Product2 (Sum2L a) c) refl
; (Product2 (Sum2R b) c) refl
}
}

{-# COMPILE AGDA2HS distributeVal #-}

distribute
: {@0 A B C : Typ}
EmbeddingTyp
((A + B) × C)
((A × C) + (B × C))
distribute =
record
{ embed = distributeVal
; typcheck = λ
{ (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 a b) c)
Just (Typ.Two Typ.Sum2 (Typ.Two Typ.Product2 a c) (Typ.Two Typ.Product2 b c))
; _ Nothing
}
; accepts = refl
; rejects = λ
{ (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 _ _) _) λ ()
}
}

{-# COMPILE AGDA2HS distribute #-}
149 changes: 149 additions & 0 deletions lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,149 @@
module Language.FineTypes.Typ where

{-# FOREIGN AGDA2HS
-- !!! This Haskell module has been autogenerated by agda2hs.
-- !!! Do NOT change; change the original .agda file instead.
#-}

open import Haskell.Prelude
using (String; List; True; False)
renaming (_×_ to Pair)
open import Haskell.Law.Eq
open import Haskell.Prim.Eq

import Haskell.Prelude as Hs

ConstructorName = String
FieldName = String
TypName = String
VarName = String

{-# COMPILE AGDA2HS ConstructorName #-}
{-# COMPILE AGDA2HS FieldName #-}
{-# COMPILE AGDA2HS TypName #-}
{-# COMPILE AGDA2HS VarName #-}

{-----------------------------------------------------------------------------
Haskell - Typ
------------------------------------------------------------------------------}
data TypConst : Set where
Bool : TypConst
Bytes : TypConst
Integer : TypConst
Natural : TypConst
Text : TypConst
Rational : TypConst
Unit : TypConst

data OpOne : Set where
Option : OpOne
Sequence : OpOne
PowerSet : OpOne

data OpTwo : Set where
Sum2 : OpTwo
Product2 : OpTwo
PartialFunction : OpTwo
FiniteSupport : OpTwo

data Constraint1 : Set where
Braces : List Constraint1 Constraint1
Token : String Constraint1

Constraint = List Constraint1

data Typ : Set where
Var : TypName Typ
Zero : TypConst Typ
One : OpOne Typ Typ
Two : OpTwo Typ Typ Typ
ProductN : List (Pair FieldName Typ) Typ
SumN : List (Pair ConstructorName Typ) Typ
Constrained : VarName Typ Constraint Typ

{-# COMPILE AGDA2HS TypConst #-}
{-# COMPILE AGDA2HS OpOne #-}
{-# COMPILE AGDA2HS OpTwo #-}
{-# COMPILE AGDA2HS Constraint1 #-}
{-# COMPILE AGDA2HS Constraint #-}
{-# COMPILE AGDA2HS Typ #-}

{-----------------------------------------------------------------------------
Agda - Equality
------------------------------------------------------------------------------}
instance
iTypConst : Eq TypConst
iTypConst ._==_ Bool Bool = True
iTypConst ._==_ Bytes Bytes = True
iTypConst ._==_ Integer Integer = True
iTypConst ._==_ Natural Natural = True
iTypConst ._==_ Text Text = True
iTypConst ._==_ Rational Rational = True
iTypConst ._==_ Unit Unit = True
iTypConst ._==_ _ _ = Hs.False

{-# COMPILE AGDA2HS iTypConst derive #-}

-- Created by automati case splitting C^c C^c
-- and automatic goal finding C^c C^a
instance
iLawfulEqTypConst : IsLawfulEq TypConst

iLawfulEqTypConst .isEquality Bool Bool = Hs.ofY Hs.refl
iLawfulEqTypConst .isEquality Bool Bytes = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bool Integer = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bool Natural = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bool Text = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bool Rational = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bool Unit = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bytes Bool = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bytes Bytes = Hs.ofY Hs.refl
iLawfulEqTypConst .isEquality Bytes Integer = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bytes Natural = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bytes Text = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bytes Rational = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Bytes Unit = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Integer Bool = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Integer Bytes = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Integer Integer = Hs.ofY Hs.refl
iLawfulEqTypConst .isEquality Integer Natural = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Integer Text = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Integer Rational = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Integer Unit = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Natural Bool = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Natural Bytes = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Natural Integer = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Natural Natural = Hs.ofY Hs.refl
iLawfulEqTypConst .isEquality Natural Text = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Natural Rational = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Natural Unit = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Text Bool = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Text Bytes = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Text Integer = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Text Natural = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Text Text = Hs.ofY Hs.refl
iLawfulEqTypConst .isEquality Text Rational = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Text Unit = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Rational Bool = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Rational Bytes = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Rational Integer = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Rational Natural = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Rational Text = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Rational Rational = Hs.ofY Hs.refl
iLawfulEqTypConst .isEquality Rational Unit = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Unit Bool = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Unit Bytes = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Unit Integer = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Unit Natural = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Unit Text = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Unit Rational = Hs.ofN (λ ())
iLawfulEqTypConst .isEquality Unit Unit = Hs.ofY Hs.refl

{-----------------------------------------------------------------------------
Agda - Syntactic sugar
------------------------------------------------------------------------------}
_×_ : Typ Typ Typ
A × B = Two Product2 A B

_+_ : Typ Typ Typ
A + B = Two Sum2 A B
Loading

0 comments on commit 8064570

Please sign in to comment.