Add GitHub Workflow (#129)

.github/workflows/agda.yaml

@@ -0,0 +1,65 @@
+on:
+  pull_request:
+    branches:
+      master
+
+jobs:
+  Compile:
+    strategy:
+      matrix:
+        agda-ref: ["v2.6.2"]
+        ghc-ver: ["8.10.2"]
+        cabal-ver: ["3.4.0.0"]
+
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/cache@v2
+        name: Cache cabal packages
+        id: cache-cabal
+        with:
+          path: |
+            ~/.cabal/packages
+            ~/.cabal/store
+            ~/.cabal/bin
+            dist-newstyle
+          key: ${{ runner.os }}-${{ matrix.ghc-ver }}-${{ matrix.cabal-ver }}-${{ matrix.agda-ref }}
+
+      - name: Install cabal
+        if: steps.cache-cabal.outputs.cache-hit != 'true'
+        uses: actions/setup-haskell@v1.1.3
+        with:
+          ghc-version: ${{ matrix.ghc-ver }}
+          cabal-version: ${{ matrix.cabal-ver }}
+
+      - name: Put cabal programs in PATH
+        run: echo "~/.cabal/bin" >> $GITHUB_PATH
+
+      - name: Download Agda from github
+        if: steps.cache-cabal.outputs.cache-hit != 'true'
+        uses: actions/checkout@v2
+        with:
+          repository: agda/agda
+          path: agda
+          ref: ${{ matrix.agda-ref }}
+
+      - name: Install Agda
+        if: steps.cache-cabal.outputs.cache-hit != 'true'
+        run: |
+          cabal update
+          cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' alex-3.2.5
+          cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' happy-1.19.12
+          cd agda
+          mkdir -p doc
+          touch doc/user-manual.pdf
+          cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
+
+      - name: Checkout master
+        uses: actions/checkout@v2
+
+      - name: Compile main library
+        run: |
+          agda Everything/Unsafe.agda
+          agda Everything/Safe.agda
+          agda Everything/WithK.agda
+          agda Everything/Guardedness.agda

Everything/Unsafe.agda

@@ -2,6 +2,6 @@
 
 -- This file contains everything that cannot be compiled in --safe mode.
 
-open import Lists.SortList
+--open import Lists.SortList
 
 module Everything.Unsafe where

UnorderedSet/Definition.agda

@@ -0,0 +1,42 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Decidable.Sets
+open import Lists.Lists
+open import Numbers.Naturals.Semiring
+
+module UnorderedSet.Definition {a : _} {V : Set a} (dec : DecidableSet V) where
+
+data UnorderedSetOf : List V → Set a where
+  empty' : UnorderedSetOf []
+  addCons : (v : V) → (vs : List V) → .(contains vs v → False) → UnorderedSetOf vs → UnorderedSetOf (v :: vs)
+
+record UnorderedSet : Set a where
+  field
+    elts : List V
+    set : UnorderedSetOf elts
+
+empty : UnorderedSet
+empty = record { elts = [] ; set = empty' }
+
+add : V → UnorderedSet → UnorderedSet
+add v record { elts = elts ; set = set } with containsDecidable dec elts v
+... | inl x = record { elts = elts ; set = set }
+... | inr x = record { elts = v :: elts ; set = addCons v elts x set }
+
+singleton : V → UnorderedSet
+singleton v = record { elts = v :: [] ; set = addCons v [] (λ ()) empty' }
+
+ofList : (l : List V) → UnorderedSet
+ofList [] = record { elts = [] ; set = empty' }
+ofList (x :: l) = add x (ofList l)
+
+union : UnorderedSet → UnorderedSet → UnorderedSet
+union record { elts = eltsA ; set = setA } record { elts = eltsB ; set = setB } = ofList (eltsA ++ eltsB)
+
+count : UnorderedSet → ℕ
+count record { elts = e ; set = _ } = length e
+
+setContains : (v : V) → UnorderedSet → Set a
+setContains v record { elts = elts ; set = set } = contains elts v