Bigger demo + quickfix for PSeq

Author: omelkonian

.gitignore

@@ -17,6 +17,7 @@ CoqMakefile.conf
 .direnv
 result
 
-test/*.txt
-test/*.v
-test/*.glob
+*.txt
+*.ast
+*.v
+*.glob

agda2lambox.agda-lib

@@ -1,3 +1,4 @@
 name: agda2lambox
+depend: standard-library
 include: test
 flags: --no-projection-like

src/Agda2Lambox/Compile/Term.hs

@@ -19,7 +19,8 @@ import Agda.Syntax.Builtin ( builtinNat, builtinZero, builtinSuc )
 import Agda.Syntax.Common ( Erased(..) )
 import Agda.Syntax.Common.Pretty
 import Agda.Syntax.Literal
-import Agda.Syntax.Treeless ( TTerm(..), TAlt(..), CaseInfo(..), CaseType(..) )
+import Agda.Syntax.Treeless
+  ( TTerm(..), TAlt(..), CaseInfo(..), CaseType(..), TPrim(..) )
 import Agda.TypeChecking.Datatypes ( getConstructorData, getConstructors )
 import Agda.TypeChecking.Monad.Base ( TCM , liftTCM, MonadTCEnv, MonadTCM )
 import Agda.TypeChecking.Monad.Builtin ( getBuiltinName_ )
@@ -89,7 +90,7 @@ compileTermC = \case
     if n < bound then pure $ LRel n
                  else pure $ LBox -- a type variable
 
-  TPrim p -> genericError "primitives not supported"
+  TPrim p -> genericError $ "primitives not supported: " <> show p
 
   -- NOTE(flupe):
   -- Assumption:
@@ -108,6 +109,9 @@ compileTermC = \case
     lift $ requireDef q
     liftTCM $ toConApp q []
 
+  -- TODO: maybe not ignore seq? (c.f. issue #12)
+  TApp (TPrim PSeq) args -> compileTermC (last args)
+
   TApp (TCon q) args -> do
     lift $ requireDef q
     traverse compileTermC args

test/BigDemo.agda

@@ -0,0 +1,83 @@
+module _ where
+
+-- - decision procedure (barebones)
+module BAREBONES where
+  open import Agda.Primitive using (Level)
+  open import Agda.Builtin.Bool using (Bool; true; false)
+  open import Agda.Builtin.Nat using (Nat; zero; suc)
+  open import Agda.Builtin.Equality using (_≡_; refl)
+
+  private variable
+    ℓ : Level
+    A B : Set ℓ
+    x y : Nat
+
+  data ⊥ : Set where
+
+  ¬_ : Set → Set
+  ¬ A = A → ⊥
+
+  data Dec (A : Set) : Set where
+    yes : A → Dec A
+    no  : ¬ A → Dec A
+
+  isYes : Dec A → Bool
+  isYes = λ where
+    (yes _) → true
+    (no  _) → false
+
+  record HasDec (A : Set) : Set where
+    field dec : Dec A
+  open HasDec ⦃...⦄
+
+  cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
+  cong _ refl = refl
+
+  instance
+    HasDecEq-Nat : HasDec (x ≡ y)
+    HasDecEq-Nat {x}{y} .dec with x | y
+    ... | zero | zero = yes refl
+    ... | zero | suc n = no λ ()
+    ... | suc m | zero = no λ ()
+    ... | suc m | suc n with dec
+    ... | yes eq  = yes (cong suc eq)
+    ... | no  m≢n = no λ where refl → m≢n refl
+
+  test : Bool
+  test = isYes (dec {A = 42 ≡ 42})
+  -- {-# COMPILE AGDA2LAMBOX test #-}
+
+-- - decision procedure (importing stdlib)
+module STDLIB where
+  open import Relation.Nullary using (isYes)
+
+  open import Data.Bool using (Bool; true; false)
+  open import Data.Bool.Properties using (_≟_)
+  test : Bool
+  test = isYes (true ≟ false)
+  -- {-# COMPILE AGDA2LAMBOX test #-}
+
+  -- open import Data.Bool using (Bool)
+  -- open import Data.Nat.Properties using (_≟_)
+  -- test : Bool
+  -- test = isYes (42 ≟ 42)
+  -- {-# COMPILE AGDA2LAMBOX test #-}
+
+-- - sort
+module SORT where
+  open import Data.List.Base using (List; _∷_; [])
+
+  open import Data.Bool.Properties using (≤-decTotalOrder)
+  open import Data.Bool using (Bool; true; false)
+  open import Data.List.Sort ≤-decTotalOrder using (sort)
+  test : List Bool
+  test = sort (true ∷ false ∷ true ∷ false ∷ [])
+  {-# COMPILE AGDA2LAMBOX test #-}
+
+  -- open import Data.Nat.Properties using (≤-decTotalOrder)
+  -- open import Data.Bool using (Bool; true; false)
+  -- open import Data.List.Base using (List; _∷_; [])
+  -- open import Data.List.Sort ≤-decTotalOrder using (sort)
+  -- test : List Bool
+  -- test = sort (42 ∷ 0 ∷ 5 ∷ 3 ∷ [])
+  -- {-# COMPILE AGDA2LAMBOX test #-}

test/Equality.agda

@@ -0,0 +1,64 @@
+open import Agda.Primitive using (Level; lzero)
+open import Agda.Builtin.Nat using (Nat; zero; suc)
+
+infix 4 _≡_
+data _≡_ {A : Set} (x : A) : A → Set where
+  instance refl : x ≡ x
+
+private variable ℓ : Level
+
+eqzero : 0 ≡ 0
+eqzero = refl
+
+private variable A B C : Set ℓ
+
+cong : ∀ {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
+cong f refl = refl
+
+EqNat = _≡_ {A = Nat}
+
+eqOne : EqNat 1 1
+eqOne = cong suc eqzero
+
+sym : {a b : A} → a ≡ b → b ≡ a
+sym refl = refl
+
+infixr 9 _∘_
+infixr -1 _$_
+
+_∘_ : (B → C) → (A → B) → (A → C)
+(f ∘ g) x = f (g x)
+
+_$_ : (A → B) → A → B
+f $ x = f x
+
+eqTwo : EqNat 2 2
+eqTwo = sym $ cong (suc ∘ suc) eqzero
+
+trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
+trans refl refl = refl
+
+subst : ∀ {P : A → Set} {a b : A} → a ≡ b → P a → P b
+subst refl p = p
+
+add : Nat → Nat → Nat
+add zero    y = y
+add (suc x) y = suc (add x y)
+
+add-left-id : (a : Nat) → EqNat (add zero a) a
+add-left-id zero = refl
+add-left-id (suc a) = cong suc $ add-left-id a
+
+suc-left-add : (a b : Nat) → add (suc a) b ≡ suc (add a b)
+suc-left-add a zero = refl
+suc-left-add a (suc b) = refl
+
+eqLevel : lzero ≡ lzero
+eqLevel = refl
+
+toNat : ∀ {x y : Nat} → x ≡ y → Nat
+toNat {x = x} {y = .x} refl = x
+
+test : Nat
+test = toNat $ suc-left-add 1 0
+{-# COMPILE AGDA2LAMBOX test #-}

test/Levels.agda

@@ -0,0 +1,62 @@
+-- {-# OPTIONS --level-universe #-}
+open import Agda.Builtin.Nat using (Nat; suc)
+
+open import Agda.Primitive
+
+-- ** level definitions should be ignored
+0ℓ : Level
+0ℓ = lzero
+
+mkLevel : Nat → Level
+mkLevel 0 = 0ℓ
+mkLevel (suc n) = lsuc (mkLevel n)
+
+-- ** level function arguments should be erased
+testLevel : Level → Nat
+testLevel _ = 42
+
+-- ** level application arguments should be erased
+testMkLevel : Nat
+testMkLevel = testLevel (mkLevel 42)
+{-# COMPILE AGDA2LAMBOX testMkLevel #-}
+
+-- ** level record fields should be erased
+record SomeLvl : Set where
+  constructor this
+  field ℓ : Level
+open SomeLvl public
+
+someLvl : SomeLvl
+someLvl = this 0ℓ
+
+lvlToNat : Level → Nat
+lvlToNat _ = 42
+
+testSomeLvl : Nat
+testSomeLvl = lvlToNat (someLvl .ℓ)
+{-# COMPILE AGDA2LAMBOX testSomeLvl #-}
+
+constLvl : ∀ {A : Set} → A → Level → A
+constLvl x _ = x
+
+testConstLvl : Nat
+testConstLvl = constLvl 42 (someLvl .ℓ)
+{-# COMPILE AGDA2LAMBOX testConstLvl #-}
+
+const : ∀ {A B : Set} → A → B → A
+const x _ = x
+
+testConst : Nat
+testConst = const 42 0
+{-# COMPILE AGDA2LAMBOX testConst #-}
+
+testConstLvl2 : Nat
+testConstLvl2 = const 42 (someLvl .ℓ)
+{-# COMPILE AGDA2LAMBOX testConstLvl2 #-}
+
+testWhere : Nat
+testWhere = toNat (someLvl .ℓ)
+  where
+  toNat : Level → Nat
+  toNat _ = 42
+{-# COMPILE AGDA2LAMBOX testWhere #-}