From 7a2fcf5c07a06d4f437bd031e6a78b7eda336aa6 Mon Sep 17 00:00:00 2001 From: Heinrich Apfelmus Date: Fri, 22 Sep 2023 13:28:58 +0200 Subject: [PATCH] wip Add `fine-types-core` package with Agda proofs --- .gitignore | 4 + lib/fine-types-core/CHANGELOG.md | 5 + lib/fine-types-core/README.md | 15 ++ lib/fine-types-core/fine-types-core.agda-lib | 6 + lib/fine-types-core/fine-types-core.cabal | 63 +++++ lib/fine-types-core/generate-haskell.sh | 6 + .../src/agda/Data/Embedding.agda | 21 ++ .../src/agda/Language/FineTypes.agda | 12 + .../agda/Language/FineTypes/Embedding.agda | 77 ++++++ .../src/agda/Language/FineTypes/Typ.agda | 149 +++++++++++ .../src/agda/Language/FineTypes/Value.agda | 199 ++++++++++++++ .../agda/Language/FineTypes/Value/Def.agda | 135 ++++++++++ .../Language/FineTypes/Value/Typcheck.agda | 243 ++++++++++++++++++ .../src/haskell/Data/Embedding.hs | 7 + .../src/haskell/Language/FineTypes.hs | 5 + .../haskell/Language/FineTypes/Embedding.hs | 37 +++ .../src/haskell/Language/FineTypes/Typ.hs | 46 ++++ .../haskell/Language/FineTypes/Value/Def.hs | 63 +++++ 18 files changed, 1093 insertions(+) create mode 100644 lib/fine-types-core/CHANGELOG.md create mode 100644 lib/fine-types-core/README.md create mode 100644 lib/fine-types-core/fine-types-core.agda-lib create mode 100644 lib/fine-types-core/fine-types-core.cabal create mode 100755 lib/fine-types-core/generate-haskell.sh create mode 100644 lib/fine-types-core/src/agda/Data/Embedding.agda create mode 100644 lib/fine-types-core/src/agda/Language/FineTypes.agda create mode 100644 lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda create mode 100644 lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda create mode 100644 lib/fine-types-core/src/agda/Language/FineTypes/Value.agda create mode 100644 lib/fine-types-core/src/agda/Language/FineTypes/Value/Def.agda create mode 100644 lib/fine-types-core/src/agda/Language/FineTypes/Value/Typcheck.agda create mode 100644 lib/fine-types-core/src/haskell/Data/Embedding.hs create mode 100644 lib/fine-types-core/src/haskell/Language/FineTypes.hs create mode 100644 lib/fine-types-core/src/haskell/Language/FineTypes/Embedding.hs create mode 100644 lib/fine-types-core/src/haskell/Language/FineTypes/Typ.hs create mode 100644 lib/fine-types-core/src/haskell/Language/FineTypes/Value/Def.hs diff --git a/.gitignore b/.gitignore index 33b36198..1c8a6a12 100644 --- a/.gitignore +++ b/.gitignore @@ -15,6 +15,10 @@ *.hp *.eventlog +### agda2hs ### +_build +*.agdai + ### Cabal ### dist dist-* diff --git a/lib/fine-types-core/CHANGELOG.md b/lib/fine-types-core/CHANGELOG.md new file mode 100644 index 00000000..228efdd6 --- /dev/null +++ b/lib/fine-types-core/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for fine-types-core + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/lib/fine-types-core/README.md b/lib/fine-types-core/README.md new file mode 100644 index 00000000..5c8f3661 --- /dev/null +++ b/lib/fine-types-core/README.md @@ -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 diff --git a/lib/fine-types-core/fine-types-core.agda-lib b/lib/fine-types-core/fine-types-core.agda-lib new file mode 100644 index 00000000..10a0609e --- /dev/null +++ b/lib/fine-types-core/fine-types-core.agda-lib @@ -0,0 +1,6 @@ +name: fine-types-core +include: src/agda +depend: + standard-library + agda2hs +flags: -W noUnsupportedIndexedMatch --erasure diff --git a/lib/fine-types-core/fine-types-core.cabal b/lib/fine-types-core/fine-types-core.cabal new file mode 100644 index 00000000..e3f89dd9 --- /dev/null +++ b/lib/fine-types-core/fine-types-core.cabal @@ -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 diff --git a/lib/fine-types-core/generate-haskell.sh b/lib/fine-types-core/generate-haskell.sh new file mode 100755 index 00000000..a86e90f7 --- /dev/null +++ b/lib/fine-types-core/generate-haskell.sh @@ -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/ diff --git a/lib/fine-types-core/src/agda/Data/Embedding.agda b/lib/fine-types-core/src/agda/Data/Embedding.agda new file mode 100644 index 00000000..974801be --- /dev/null +++ b/lib/fine-types-core/src/agda/Data/Embedding.agda @@ -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 #-} diff --git a/lib/fine-types-core/src/agda/Language/FineTypes.agda b/lib/fine-types-core/src/agda/Language/FineTypes.agda new file mode 100644 index 00000000..b4a3d6fb --- /dev/null +++ b/lib/fine-types-core/src/agda/Language/FineTypes.agda @@ -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 diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda new file mode 100644 index 00000000..91bfc368 --- /dev/null +++ b/lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda @@ -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 #-} diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda new file mode 100644 index 00000000..bf778e43 --- /dev/null +++ b/lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda @@ -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 diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Value.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Value.agda new file mode 100644 index 00000000..bff15b94 --- /dev/null +++ b/lib/fine-types-core/src/agda/Language/FineTypes/Value.agda @@ -0,0 +1,199 @@ +module Language.FineTypes.Value 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; case_of_) +open import Function.Base using (case_of_) +open import Language.FineTypes.Typ + +isJust : ∀ {a : Set} → Maybe a → Bool +isJust (Just _) = True +isJust Nothing = False + +{----------------------------------------------------------------------------- + Values index by a typ +------------------------------------------------------------------------------} +data Val : @0 Typ → Set where + Unit : Val (Zero TUnit) + Pair : ∀ {@0 A B : Typ} → Val A → Val B → Val (A × B) + SumL : ∀ {@0 A B : Typ} → Val A → Val (A + B) + SumR : ∀ {@0 A B : Typ} → Val B → Val (A + B) + +{-# COMPILE AGDA2HS Val #-} + +{----------------------------------------------------------------------------- + Equality of Values at run-time +------------------------------------------------------------------------------} +data Eq-runtime : {@0 A B : Typ} → Val A → Val B → Set where + eq-Unit : Eq-runtime Unit Unit + eq-Pair + : ∀ {@0 A1 A2 B1 B2 : Typ} + {a1 : Val A1} {a2 : Val A2} + {b1 : Val B1} {b2 : Val B2} + → Eq-runtime a1 a2 + → Eq-runtime b1 b2 + → Eq-runtime (Pair a1 b1) (Pair a2 b2) + eq-SumL + : ∀ {@0 A1 A2 B1 B2 : Typ} + {a1 : Val A1} {a2 : Val A2} + → Eq-runtime a1 a2 + → Eq-runtime (SumL {A1} {B1} a1) (SumL {A2} {B2} a2) + eq-SumR + : ∀ {@0 A1 A2 B1 B2 : Typ} + {b1 : Val B1} {b2 : Val B2} + → Eq-runtime b1 b2 + → Eq-runtime (SumR {A1} {B1} b1) (SumR {A2} {B2} b2) + +-- Lemma: +-- When to values are related by a run-time equality, +-- we can translate this into a function that maps one into the other. + +{----------------------------------------------------------------------------- + Type checking on the value level +------------------------------------------------------------------------------} +data Typchecks {@0 A : Typ} (va : Val A) (B : Typ) : Set where + Checks + : (vb : Val B) + → Eq-runtime va vb + → Typchecks va B + +-- | Helper function that recurses into the typ and returns proof. +checkTyp + : ∀ {@0 A : Typ} (v : Val A) (B : Typ) + → Maybe (Typchecks v B) +checkTyp Unit (Zero TUnit) = + Just (Checks Unit eq-Unit) +checkTyp (Pair x y) (Two Product2 X Y) = + case (checkTyp x X) of λ + { Nothing → Nothing + ; (Just (Checks x' ex)) → + case (checkTyp y Y) of λ + { Nothing → Nothing + ; (Just (Checks y' ey)) → + Just (Checks (Pair x' y') (eq-Pair ex ey)) + } + } +checkTyp (SumL x) (Two Sum2 X _) = + case (checkTyp x X) of λ + { Nothing → Nothing + ; (Just (Checks x' ex)) → + Just (Checks (SumL x') (eq-SumL ex)) + } +checkTyp (SumR y) (Two Sum2 _ Y) = + case (checkTyp y Y) of λ + { Nothing → Nothing + ; (Just (Checks y' ey)) → + Just (Checks (SumR y') (eq-SumR ey)) + } +checkTyp _ _ = Nothing + +-- | Value-level check whether the typ matches. +hasTyp : ∀ {@0 A : Typ} → Val A → Typ → Bool +hasTyp Unit (Zero TUnit) = True +hasTyp (Pair x y) (Two Product2 tx ty) = + hasTyp x tx && hasTyp y ty +hasTyp (SumL x) (Two Sum2 tx _) = + hasTyp x tx +hasTyp (SumR y) (Two Sum2 _ ty) = + hasTyp y ty +hasTyp _ _ = + False + +{- +test : (A : Typ) {@0 A = A₁ : Typ} (a : Val A₁) + (w : Maybe (Typchecks a A)) → + checkTyp a A ≡ w → + (B : Typ) {@0 B = B₁ : Typ} (b : Val B₁) → + (isJust w && isJust (checkTyp b B)) ≡ + isJust + ((λ { Nothing → Nothing + ; (Just (Checks x' ex)) + → case checkTyp b B of + (λ { Nothing → Nothing + ; (Just (Checks y' ey)) + → Just (Checks (Pair x' y') (eq-Pair ex ey)) + }) + }) + w) +test = {! !} +-} + +{- +lemma-upgrade-hasTyp + : ∀ {@0 A : Typ} (va : Val A) (B : Typ) + → hasTyp va B ≡ isJust (checkTyp va B) +lemma-upgrade-hasTyp Unit (Zero TUnit) = refl +lemma-upgrade-hasTyp (Pair x y) (Two Product2 X Y) + rewrite lemma-upgrade-hasTyp x X + rewrite lemma-upgrade-hasTyp y Y + with checkTyp y Y in eqY +... | Nothing with checkTyp x X in eqX +... | _ = ? + +-} +{- +postulate + A : Set + B : A → Set + H : (x : A) → B x → Set + +import Agda.Builtin.Sigma as S + +test : (p : S.Σ A B) (w : A) → H w (S.snd p) +test = ? +-} + +lemma-upgrade-hasTyp + : ∀ {@0 A : Typ} (B : Typ) (va : Val A) + → hasTyp va B ≡ isJust (checkTyp va B) +lemma-upgrade-hasTyp (Zero TUnit) Unit = refl +lemma-upgrade-hasTyp (Two Product2 A B) (Pair a b) + rewrite lemma-upgrade-hasTyp A a + rewrite lemma-upgrade-hasTyp B b + with checkTyp a A +... | Nothing = refl +... | Just (Checks _ _) with checkTyp b B +... | Nothing = refl +... | Just (Checks _ _) = refl +lemma-upgrade-hasTyp (Two Sum2 A _) (SumL a) + rewrite lemma-upgrade-hasTyp A a + with checkTyp a A +... | Nothing = refl +... | (Just (Checks x' ex)) = refl +lemma-upgrade-hasTyp (Two Sum2 _ B) (SumR b) + rewrite lemma-upgrade-hasTyp B b + with checkTyp b B +... | Nothing = refl +... | (Just (Checks y' ey)) = refl +lemma-upgrade-hasTyp (Zero TBool) Unit = refl +lemma-upgrade-hasTyp (Zero TNatural) Unit = refl +lemma-upgrade-hasTyp (One x B) Unit = refl +lemma-upgrade-hasTyp (Two x B B₁) Unit = refl +lemma-upgrade-hasTyp (Zero x) (Pair va va₁) = refl +lemma-upgrade-hasTyp (One x B) (Pair va va₁) = refl +lemma-upgrade-hasTyp (Two Sum2 B B₁) (Pair va va₁) = refl +lemma-upgrade-hasTyp (Zero x) (SumL va) = refl +lemma-upgrade-hasTyp (One x B) (SumL va) = refl +lemma-upgrade-hasTyp (Two Product2 B B₁) (SumL va) = refl +lemma-upgrade-hasTyp (Zero x) (SumR va) = refl +lemma-upgrade-hasTyp (One x B) (SumR va) = refl +lemma-upgrade-hasTyp (Two Product2 B B₁) (SumR va) = refl + +lemma-good-hasTyp + : ∀ (A : Typ) (a : Val A) + → hasTyp a A ≡ True +lemma-good-hasTyp (Zero TUnit) Unit = refl +lemma-good-hasTyp (Two Product2 A B) (Pair a b) + rewrite lemma-good-hasTyp A a + rewrite lemma-good-hasTyp B b + = refl +lemma-good-hasTyp (Two Sum2 A _) (SumL a) = + lemma-good-hasTyp A a +lemma-good-hasTyp (Two Sum2 _ B) (SumR b) = + lemma-good-hasTyp B b + +{-# COMPILE AGDA2HS hasTyp #-} + \ No newline at end of file diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Value/Def.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Def.agda new file mode 100644 index 00000000..526f3696 --- /dev/null +++ b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Def.agda @@ -0,0 +1,135 @@ +module Language.FineTypes.Value.Def where + +open import Haskell.Prelude + hiding (_×_; _+_; Pair; case_of_; Bool; Integer ) +open import Function.Base + using (case_of_) +open import Language.FineTypes.Typ + using (Typ; OpOne; OpTwo; _×_; _+_) + +import Haskell.Prelude as Hs +import Language.FineTypes.Typ as Typ + +{----------------------------------------------------------------------------- + Values +------------------------------------------------------------------------------} +data ZeroF : @0 Typ.TypConst → Set where + Bool : Hs.Bool → ZeroF Typ.Bool +-- Bytes : ByteString → ZeroF + Integer : Hs.Integer → ZeroF Typ.Integer + Natural : Nat → ZeroF Typ.Natural +-- Rational : Hs.Rational → ZeroF +-- Text : Text → ZeroF + Unit : ZeroF Typ.Unit + + +data OneF (a : Set) : @0 Typ.OpOne → Set where + Option : Maybe a → OneF a Typ.Option + Sequence : List a → OneF a Typ.Sequence +-- PowerSet : Set a → OneF a + +data TwoF (a b : Set) : @0 Typ.OpTwo → Set where +-- FiniteMap : Map a b → TwoF a b + +Ix = Hs.Int + +data Value : @0 Typ → Set where + Zero : ∀ {@0 A : Typ.TypConst} → ZeroF A → Value (Typ.Zero A) + One : ∀ {@0 A : Typ} {@0 op : OpOne} + → OneF (Value A) op → Value (Typ.One op A) + Two : ∀ {@0 A B : Typ} {@0 op : OpTwo} + → TwoF (Value A) (Value B) op + → Value (Typ.Two op A B) + Product2 : ∀ {@0 A B : Typ} → Value A → Value B → Value (A × B) + Sum2L : ∀ {@0 A B : Typ} → Value A → Value (A + B) + Sum2R : ∀ {@0 A B : Typ} → Value B → Value (A + B) + +-- Product : ∀ {@0 A : Typ} → List Value → Value +-- Sum : Ix → Value → Value + +{-# COMPILE AGDA2HS ZeroF #-} +{-# COMPILE AGDA2HS OneF #-} +{-# COMPILE AGDA2HS TwoF #-} +{-# COMPILE AGDA2HS Ix #-} +{-# COMPILE AGDA2HS Value #-} + +{----------------------------------------------------------------------------- + Equality of Value +------------------------------------------------------------------------------} +eqZeroF : ∀{@0 A B : Typ.TypConst} → ZeroF A → ZeroF B → Hs.Bool +eqZeroF (Bool x) (Bool y) = x == y +eqZeroF (Bool _) _ = False +eqZeroF (Integer x) (Integer y) = True +eqZeroF (Integer _) _ = False +eqZeroF (Natural _) (Natural _) = True +eqZeroF (Natural _) _ = False +eqZeroF Unit Unit = False +eqZeroF Unit _ = False + +-- mutually recursive definitions +eqValue + : ∀{@0 A B : Typ} → Value A → Value B → Hs.Bool +eqMaybeValue + : ∀{@0 A B : Typ} + → Maybe (Value A) → Maybe (Value B) → Hs.Bool +eqListValue + : ∀{@0 A B : Typ} + → List (Value A) → List (Value B) → Hs.Bool + +eqMaybeValue (Just x) (Just y) = eqValue x y +eqMaybeValue (Just _) _ = False +eqMaybeValue Nothing Nothing = True +eqMaybeValue Nothing _ = False + +eqListValue (x ∷ xs) (y ∷ ys) = eqValue x y && eqListValue xs ys +eqListValue (_ ∷ _) _ = False +eqListValue [] [] = True +eqListValue [] _ = False + +eqValue (Zero x) (Zero y) = eqZeroF x y +eqValue (Zero _) _ = False +eqValue (One (Option x)) (One (Option y)) = eqMaybeValue x y +eqValue (One (Option _)) _ = False +eqValue (One (Sequence x)) (One (Sequence y)) = eqListValue x y +eqValue (One (Sequence _)) _ = False +eqValue (Two _) (Two _) = True +eqValue (Two _) _ = False +eqValue (Product2 x1 x2) (Product2 y1 y2) = + (eqValue x1 y1 && eqValue x2 y2) +eqValue (Product2 _ _) _ = False +eqValue (Sum2L x) (Sum2L y) = eqValue x y +eqValue (Sum2L _) _ = False +eqValue (Sum2R x) (Sum2R y) = eqValue x y +eqValue (Sum2R _) _ = False + +{-# COMPILE AGDA2HS eqZeroF #-} +{-# COMPILE AGDA2HS eqValue #-} +{-# COMPILE AGDA2HS eqMaybeValue #-} +{-# COMPILE AGDA2HS eqListValue #-} + +{- +data Eq-runtime : {@0 A B : Typ} → Value A → Val B → Set where + eq-Unit : Eq-runtime Unit Unit + eq-Pair + : ∀ {@0 A1 A2 B1 B2 : Typ} + {a1 : Val A1} {a2 : Val A2} + {b1 : Val B1} {b2 : Val B2} + → Eq-runtime a1 a2 + → Eq-runtime b1 b2 + → Eq-runtime (Pair a1 b1) (Pair a2 b2) + eq-SumL + : ∀ {@0 A1 A2 B1 B2 : Typ} + {a1 : Val A1} {a2 : Val A2} + → Eq-runtime a1 a2 + → Eq-runtime (SumL {A1} {B1} a1) (SumL {A2} {B2} a2) + eq-SumR + : ∀ {@0 A1 A2 B1 B2 : Typ} + {b1 : Val B1} {b2 : Val B2} + → Eq-runtime b1 b2 + → Eq-runtime (SumR {A1} {B1} b1) (SumR {A2} {B2} b2) +-} + +-- Lemma: +-- When to values are related by a run-time equality, +-- we can translate this into a function that maps one into the other. + diff --git a/lib/fine-types-core/src/agda/Language/FineTypes/Value/Typcheck.agda b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Typcheck.agda new file mode 100644 index 00000000..e8a7c05d --- /dev/null +++ b/lib/fine-types-core/src/agda/Language/FineTypes/Value/Typcheck.agda @@ -0,0 +1,243 @@ +module Language.FineTypes.Value.Typcheck where + +open import Haskell.Prelude + hiding (_×_; _+_; Pair; case_of_; Bool; Integer ) +open import Function.Base + using (case_of_) + +open import Language.FineTypes.Value.Def +open import Language.FineTypes.Typ + using (Typ) + +import Haskell.Prelude as Hs +import Language.FineTypes.Typ as Typ + +{----------------------------------------------------------------------------- + Haskell — type checking +------------------------------------------------------------------------------} +typOf0 : ∀{@0 A : Typ.TypConst} → ZeroF A -> Typ.TypConst +typOf0 a = case a of λ where + (Bool _) -> Typ.Bool +-- Bytes _ -> Typ.Bytes + (Integer _) -> Typ.Integer + (Natural _) -> Typ.Natural +-- Text _ -> Typ.Text + Unit -> Typ.Unit +-- Rational _ -> Typ.Rational + +-- mutually recursive definitions +hasTyp + : ∀{@0 A : Typ} → Value A → Typ → Hs.Bool +hasTyp1 + : ∀{@0 A : Typ} {@0 op : Typ.OpOne} + → OneF (Value A) op + -> Typ.OpOne -> Typ -> Hs.Bool +hasTyp2 + : ∀{@0 A B : Typ} {@0 op : Typ.OpTwo} + → TwoF (Value A) (Value B) op + → Typ.OpTwo -> Typ -> Typ -> Hs.Bool + +hasTyp1 (Option v) Typ.Option t = + all (λ v → hasTyp v t) v +hasTyp1 (Option _) _ _ = + False +hasTyp1 (Sequence vs) Typ.Sequence t = + all (λ v → hasTyp v t) vs +hasTyp1 (Sequence _) _ _ = + False + +hasTyp2 = λ() + +hasTyp (Zero a) (Typ.Zero b) = + typOf0 a == b +hasTyp (Zero _) _ = + False +hasTyp (One a) (Typ.One op typ) = + hasTyp1 a op typ +hasTyp (One _) _ = + False +hasTyp (Product2 a b) (Typ.Two Typ.Product2 ta tb) = + (hasTyp a ta) && (hasTyp b tb) +hasTyp (Product2 _ _) _ = + False +hasTyp (Sum2L a) (Typ.Two Typ.Sum2 ta _) = + hasTyp a ta +hasTyp (Sum2L _) _ = + False +hasTyp (Sum2R b) (Typ.Two Typ.Sum2 _ tb) = + hasTyp b tb +hasTyp (Sum2R _) _ = + False +hasTyp (Two a) (Typ.Two op typ1 typ2) = + hasTyp2 a op typ1 typ2 +hasTyp (Two _) _ = + False + +{-# COMPILE AGDA2HS typOf0 #-} +{-# COMPILE AGDA2HS hasTyp1 #-} +{-# COMPILE AGDA2HS hasTyp2 #-} +{-# COMPILE AGDA2HS hasTyp #-} + +{----------------------------------------------------------------------------- + Agda +------------------------------------------------------------------------------} +lemma-hasTyp-accepts-own-Typ + : ∀ (A : Typ) (v : Value A) + → hasTyp v A ≡ True + +lemma-sequence-accepts-own-Typ + : ∀ (B : Typ) (vs : List (Value B)) + → hasTyp + (One (Sequence vs)) + (Typ.One Typ.Sequence B) ≡ True + +lemma-sequence-accepts-own-Typ B [] = refl +lemma-sequence-accepts-own-Typ B (v ∷ vs) + rewrite lemma-hasTyp-accepts-own-Typ B v + rewrite lemma-sequence-accepts-own-Typ B vs + = refl + +lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Unit) (Zero Unit) + = refl +lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Bool) (Zero (Bool _)) + = refl +lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Integer) (Zero (Integer x)) + = refl +lemma-hasTyp-accepts-own-Typ (Typ.Zero Typ.Natural) (Zero (Natural x)) + = refl +lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Option A) (One (Option Nothing)) + = refl +lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Option A) (One (Option (Just x))) + = lemma-hasTyp-accepts-own-Typ A x +lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Sequence A) (One (Sequence [])) + = refl +lemma-hasTyp-accepts-own-Typ (Typ.One Typ.Sequence A) (One (Sequence (v ∷ vs))) + rewrite lemma-hasTyp-accepts-own-Typ A v + rewrite lemma-sequence-accepts-own-Typ A vs + = refl +lemma-hasTyp-accepts-own-Typ (Typ.Two Typ.Product2 A1 A2) (Product2 v1 v2) + rewrite lemma-hasTyp-accepts-own-Typ A1 v1 + rewrite lemma-hasTyp-accepts-own-Typ A2 v2 + = refl +lemma-hasTyp-accepts-own-Typ (Typ.Two Typ.Sum2 A1 A2) (Sum2L v1) + = lemma-hasTyp-accepts-own-Typ A1 v1 +lemma-hasTyp-accepts-own-Typ (Typ.Two Typ.Sum2 A1 A2) (Sum2R v2) + = lemma-hasTyp-accepts-own-Typ A2 v2 + +{----------------------------------------------------------------------------- + Type checking on the value level +------------------------------------------------------------------------------} +{- +lemma-hasTyp-respects-equality + : ∀ (A B : Typ) (v : Value A) (w : Value B) + → eqValue v w ≡ True + → hasTyp v A ≡ hasTyp w A + +lemma-eqZeroF-respects-equality + : ∀ {A B : Typ.TypConst} (v : ZeroF A) (w : ZeroF B) + → eqZeroF v w ≡ True + → typOf0 v ≡ typOf0 w + +lemma-eqZeroF-respects-equality (Bool _) (Bool _) = λ _ → refl +lemma-eqZeroF-respects-equality (Bool _) (Integer x) = λ() +lemma-eqZeroF-respects-equality (Bool _) (Natural x) = λ() +lemma-eqZeroF-respects-equality (Bool _) Unit = λ() +lemma-eqZeroF-respects-equality (Integer _) (Integer _) = λ _ → refl +lemma-eqZeroF-respects-equality (Integer _) (Bool x) = λ () +lemma-eqZeroF-respects-equality (Integer _) (Natural x) = λ () +lemma-eqZeroF-respects-equality (Integer _) Unit = λ () +lemma-eqZeroF-respects-equality (Natural _) (Natural _) = λ _ → refl +lemma-eqZeroF-respects-equality (Natural _) (Bool x) = λ () +lemma-eqZeroF-respects-equality (Natural _) (Integer x) = λ () +lemma-eqZeroF-respects-equality (Natural _) Unit = λ () +lemma-eqZeroF-respects-equality Unit Unit = λ _ → refl +lemma-eqZeroF-respects-equality Unit (Bool x) = λ () +lemma-eqZeroF-respects-equality Unit (Integer x) = λ () +lemma-eqZeroF-respects-equality Unit (Natural x) = λ () + +lemma-hasTyp-respects-equality _ _ (Zero x) (Zero y) p + rewrite lemma-eqZeroF-respects-equality x y p + = {! !} +lemma-hasTyp-respects-equality (Typ.Zero x) (Typ.One x₂ B) (Zero x₁) (One x₃) () +lemma-hasTyp-respects-equality (Typ.Zero x) (Typ.Two .Typ.Product2 B B₁) (Zero x₁) (Product2 w w₁) () +lemma-hasTyp-respects-equality (Typ.Zero x) (Typ.Two .Typ.Sum2 B B₁) (Zero x₁) (Sum2L w) () +lemma-hasTyp-respects-equality (Typ.Zero x) (Typ.Two .Typ.Sum2 B B₁) (Zero x₁) (Sum2R w) () +lemma-hasTyp-respects-equality (Typ.One x A) B v w = {! !} +lemma-hasTyp-respects-equality (Typ.Two x A A₁) B v w = {! !} +-} + +{- +data Typchecks {@0 A : Typ} (va : Val A) (B : Typ) : Set where + Checks + : (vb : Val B) + → Eq-runtime va vb + → Typchecks va B + +-- | Helper function that recurses into the typ and returns proof. +checkTyp + : ∀ {@0 A : Typ} (v : Val A) (B : Typ) + → Maybe (Typchecks v B) +checkTyp Unit (Zero TUnit) = + Just (Checks Unit eq-Unit) +checkTyp (Pair x y) (Two Product2 X Y) = + case (checkTyp x X) of λ + { Nothing → Nothing + ; (Just (Checks x' ex)) → + case (checkTyp y Y) of λ + { Nothing → Nothing + ; (Just (Checks y' ey)) → + Just (Checks (Pair x' y') (eq-Pair ex ey)) + } + } +checkTyp (SumL x) (Two Sum2 X _) = + case (checkTyp x X) of λ + { Nothing → Nothing + ; (Just (Checks x' ex)) → + Just (Checks (SumL x') (eq-SumL ex)) + } +checkTyp (SumR y) (Two Sum2 _ Y) = + case (checkTyp y Y) of λ + { Nothing → Nothing + ; (Just (Checks y' ey)) → + Just (Checks (SumR y') (eq-SumR ey)) + } +checkTyp _ _ = Nothing + + +lemma-upgrade-hasTyp + : ∀ {@0 A : Typ} (B : Typ) (va : Val A) + → hasTyp va B ≡ isJust (checkTyp va B) +lemma-upgrade-hasTyp (Zero TUnit) Unit = refl +lemma-upgrade-hasTyp (Two Product2 A B) (Pair a b) + rewrite lemma-upgrade-hasTyp A a + rewrite lemma-upgrade-hasTyp B b + with checkTyp a A +... | Nothing = refl +... | Just (Checks _ _) with checkTyp b B +... | Nothing = refl +... | Just (Checks _ _) = refl +lemma-upgrade-hasTyp (Two Sum2 A _) (SumL a) + rewrite lemma-upgrade-hasTyp A a + with checkTyp a A +... | Nothing = refl +... | (Just (Checks x' ex)) = refl +lemma-upgrade-hasTyp (Two Sum2 _ B) (SumR b) + rewrite lemma-upgrade-hasTyp B b + with checkTyp b B +... | Nothing = refl +... | (Just (Checks y' ey)) = refl +lemma-upgrade-hasTyp (Zero TBool) Unit = refl +lemma-upgrade-hasTyp (Zero TNatural) Unit = refl +lemma-upgrade-hasTyp (One x B) Unit = refl +lemma-upgrade-hasTyp (Two x B B₁) Unit = refl +lemma-upgrade-hasTyp (Zero x) (Pair va va₁) = refl +lemma-upgrade-hasTyp (One x B) (Pair va va₁) = refl +lemma-upgrade-hasTyp (Two Sum2 B B₁) (Pair va va₁) = refl +lemma-upgrade-hasTyp (Zero x) (SumL va) = refl +lemma-upgrade-hasTyp (One x B) (SumL va) = refl +lemma-upgrade-hasTyp (Two Product2 B B₁) (SumL va) = refl +lemma-upgrade-hasTyp (Zero x) (SumR va) = refl +lemma-upgrade-hasTyp (One x B) (SumR va) = refl +lemma-upgrade-hasTyp (Two Product2 B B₁) (SumR va) = refl + +-} \ No newline at end of file diff --git a/lib/fine-types-core/src/haskell/Data/Embedding.hs b/lib/fine-types-core/src/haskell/Data/Embedding.hs new file mode 100644 index 00000000..65ec12c0 --- /dev/null +++ b/lib/fine-types-core/src/haskell/Data/Embedding.hs @@ -0,0 +1,7 @@ +module Data.Embedding where + +-- !!! This Haskell module has been autogenerated by agda2hs. +-- !!! Do NOT change; change the original .agda file instead. + +data Embedding a b = Embedding{to :: a -> b, from :: b -> a} + diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes.hs b/lib/fine-types-core/src/haskell/Language/FineTypes.hs new file mode 100644 index 00000000..6d8976f9 --- /dev/null +++ b/lib/fine-types-core/src/haskell/Language/FineTypes.hs @@ -0,0 +1,5 @@ +module Language.FineTypes where + +-- !!! This Haskell module has been autogenerated by agda2hs. +-- !!! Do NOT change; change the original .agda file instead. + diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes/Embedding.hs b/lib/fine-types-core/src/haskell/Language/FineTypes/Embedding.hs new file mode 100644 index 00000000..0328f462 --- /dev/null +++ b/lib/fine-types-core/src/haskell/Language/FineTypes/Embedding.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE LambdaCase #-} +module Language.FineTypes.Embedding where + +import Data.Embedding (Embedding) +import Language.FineTypes.Typ (Typ(Two)) +import qualified Language.FineTypes.Typ (OpTwo(Product2, Sum2)) +import Language.FineTypes.Value.Def (Value(Product2, Sum2L, Sum2R)) + +-- !!! This Haskell module has been autogenerated by agda2hs. +-- !!! Do NOT change; change the original .agda file instead. + +data EmbeddingTyp = EmbeddingTyp{embed :: Embedding Value Value, + typcheck :: Typ -> Maybe Typ} + +distributeVal :: Embedding Value Value +distributeVal + = Embedding + (\case + Product2 (Sum2L a) c -> Sum2L (Product2 a c) + Product2 (Sum2R b) c -> Sum2R (Product2 b c)) + (\case + Sum2L (Product2 a c) -> Product2 (Sum2L a) c + Sum2R (Product2 b c) -> Product2 (Sum2R b) c) + +distribute :: EmbeddingTyp +distribute + = EmbeddingTyp distributeVal + (\case + Two Language.FineTypes.Typ.Product2 + (Two Language.FineTypes.Typ.Sum2 a b) c -> Just + (Two Language.FineTypes.Typ.Sum2 + (Two Language.FineTypes.Typ.Product2 a + c) + (Two Language.FineTypes.Typ.Product2 b + c)) + _ -> Nothing) + diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes/Typ.hs b/lib/fine-types-core/src/haskell/Language/FineTypes/Typ.hs new file mode 100644 index 00000000..eddf6afd --- /dev/null +++ b/lib/fine-types-core/src/haskell/Language/FineTypes/Typ.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE StandaloneDeriving #-} +module Language.FineTypes.Typ where + +-- !!! This Haskell module has been autogenerated by agda2hs. +-- !!! Do NOT change; change the original .agda file instead. + +type ConstructorName = String + +type FieldName = String + +type TypName = String + +type VarName = String + +data TypConst = Bool + | Bytes + | Integer + | Natural + | Text + | Rational + | Unit + +data OpOne = Option + | Sequence + | PowerSet + +data OpTwo = Sum2 + | Product2 + | PartialFunction + | FiniteSupport + +data Constraint1 = Braces [Constraint1] + | Token String + +type Constraint = [Constraint1] + +data Typ = Var TypName + | Zero TypConst + | One OpOne Typ + | Two OpTwo Typ Typ + | ProductN [(FieldName, Typ)] + | SumN [(ConstructorName, Typ)] + | Constrained VarName Typ Constraint + +deriving instance Eq TypConst + diff --git a/lib/fine-types-core/src/haskell/Language/FineTypes/Value/Def.hs b/lib/fine-types-core/src/haskell/Language/FineTypes/Value/Def.hs new file mode 100644 index 00000000..92b48ccf --- /dev/null +++ b/lib/fine-types-core/src/haskell/Language/FineTypes/Value/Def.hs @@ -0,0 +1,63 @@ +module Language.FineTypes.Value.Def where + +import Numeric.Natural (Natural) +import qualified Prelude as Hs (Bool, False, Integer, True) + +data ZeroF = Bool Hs.Bool + | Integer Hs.Integer + | Natural Natural + | Unit + +data OneF a = Option (Maybe a) + | Sequence [a] + +data TwoF a b + +type Ix = Int + +data Value = Zero ZeroF + | One (OneF Value) + | Two (TwoF Value Value) + | Product2 Value Value + | Sum2L Value + | Sum2R Value + +eqZeroF :: ZeroF -> ZeroF -> Hs.Bool +eqZeroF (Bool x) (Bool y) = x == y +eqZeroF (Bool _) _ = Hs.False +eqZeroF (Integer x) (Integer y) = Hs.True +eqZeroF (Integer _) _ = Hs.False +eqZeroF (Natural _) (Natural _) = Hs.True +eqZeroF (Natural _) _ = Hs.False +eqZeroF Unit Unit = Hs.False +eqZeroF Unit _ = Hs.False + +eqValue :: Value -> Value -> Hs.Bool +eqValue (Zero x) (Zero y) = eqZeroF x y +eqValue (Zero _) _ = Hs.False +eqValue (One (Option x)) (One (Option y)) = eqMaybeValue x y +eqValue (One (Option _)) _ = Hs.False +eqValue (One (Sequence x)) (One (Sequence y)) = eqListValue x y +eqValue (One (Sequence _)) _ = Hs.False +eqValue (Two _) (Two _) = Hs.True +eqValue (Two _) _ = Hs.False +eqValue (Product2 x1 x2) (Product2 y1 y2) + = eqValue x1 y1 && eqValue x2 y2 +eqValue (Product2 _ _) _ = Hs.False +eqValue (Sum2L x) (Sum2L y) = eqValue x y +eqValue (Sum2L _) _ = Hs.False +eqValue (Sum2R x) (Sum2R y) = eqValue x y +eqValue (Sum2R _) _ = Hs.False + +eqMaybeValue :: Maybe Value -> Maybe Value -> Hs.Bool +eqMaybeValue (Just x) (Just y) = eqValue x y +eqMaybeValue (Just _) _ = Hs.False +eqMaybeValue Nothing Nothing = Hs.True +eqMaybeValue Nothing _ = Hs.False + +eqListValue :: [Value] -> [Value] -> Hs.Bool +eqListValue (x : xs) (y : ys) = eqValue x y && eqListValue xs ys +eqListValue (_ : _) _ = Hs.False +eqListValue [] [] = Hs.True +eqListValue [] _ = Hs.False +