Replacing stdlib N by our Nat

Author: tomaz1502

Lam.cabal

@@ -25,6 +25,7 @@ library
   exposed-modules:
     Lam.Context
     Lam.Data
+    Lam.Nat
     Lam.Evaluator
     Lam.Handler
     Lam.Parser

src/Lam/Agda/Lam/Data.agda

@@ -1,5 +1,7 @@
 module Lam.Data where
 
+open import Lam.Nat
+
 open import Data.Bool using (true; false)
 
 open import Haskell.Prelude using (Int; Bool; String; _×_; Eq; _==_; _&&_)
@@ -9,18 +11,6 @@ Id = String
 
 {-# COMPILE AGDA2HS Id #-}
 
-data Nat : Set where
-  Z : Nat
-  S : Nat → Nat
-
-instance
-  iEqNat : Eq Nat
-  iEqNat ._==_ Z Z = true
-  iEqNat ._==_ (S x) (S y) = x == y
-  iEqNat ._==_ _ _ = false
-
-{-# COMPILE AGDA2HS Nat deriving (Eq, Show) #-}
-
 data RawTypeL : Set where
   RawBoolT : RawTypeL
   RawIntT  : RawTypeL

src/Lam/Agda/Lam/Evaluator.agda

@@ -5,6 +5,7 @@ open import Haskell.Prelude hiding (Nat)
 open import Data.Bool using (Bool; true; false)
 
 open import Lam.Data
+open import Lam.Nat hiding (_<_)
 open import Lam.UtilsAgda
 
 shiftUp' : Nat → Expr → Expr
@@ -62,7 +63,7 @@ shiftDown = shiftDown' Z
 substitute' : Nat → Expr → Expr → Expr
 substitute' i s (App e1 e2) = App (substitute' i s e1) (substitute' i s e2)
 substitute' i s (Lam n t e) = Lam n t (substitute' (S i) (shiftUp s) e)
-substitute' i s (Var x)     = if eqNat i x then s else Var x
+substitute' i s (Var x)     = if i == x then s else Var x
 substitute' i s (Ite b t e) = Ite b' t' e'
   where b' = substitute' i s b
         t' = substitute' i s t

src/Lam/Agda/Lam/Export.agda

@@ -3,3 +3,4 @@ module Lam.Export where
 open import Lam.TypeChecker public
 open import Lam.Evaluator public
 open import Lam.Data public
+open import Lam.Nat public

src/Lam/Agda/Lam/FormalizationEvaluator.agda

@@ -2,6 +2,7 @@ module Lam.FormalizationEvaluator where
 
 open import Lam.Data
 open import Lam.Evaluator
+open import Lam.Nat hiding (_<_)
 open import Lam.UtilsAgda
 
 open import Haskell.Prelude                       using (Just; Nothing; Int; Bool; _+_; _-_; _*_; _&&_; _||_; not; _<_)

src/Lam/Agda/Lam/FormalizationTypeChecker.agda

@@ -2,9 +2,7 @@
 
 module Lam.FormalizationTypeChecker where
 
-open import Data.Fin.Base         using (fromℕ<)
-open import Data.List
-open import Data.Nat              using (ℕ; _<_)
+open import Data.List             hiding (length; lookup)
 open import Data.Product          using (_×_) renaming (_,_ to ⟨_,_⟩)
 open import Function.Base         using (id)
 open import Relation.Binary.PropositionalEquality using
@@ -16,6 +14,7 @@ open import Haskell.Prelude using
   (Bool; Int; Maybe; Just; Nothing; _>>=_; case_of_; if_then_else_; maybe; _==_)
 
 open import Lam.Data
+open import Lam.Nat
 open import Lam.TypeChecker
 open import Lam.UtilsAgda
 
@@ -69,9 +68,9 @@ data _⊢_∶_ : TypingContext → Expr → TypeL → Set where
     → Γ ⊢ Ite b t e ∶ A
 
   ⊢v : ∀ {Γ : TypingContext} {i : Nat}
-    → {h : natToℕ i < length Γ}
+    → {h : i < length Γ}
     --------------------------------
-    → Γ ⊢ Var i ∶ lookup Γ (fromℕ< h)
+    → Γ ⊢ Var i ∶ lookup Γ i h
 
   ⊢l : ∀ {Γ : TypingContext} {name : Id} {body : Expr} {dom codom : TypeL}
     → (dom ∷ Γ) ⊢ body ∶ codom

src/Lam/Agda/Lam/Nat.agda

@@ -0,0 +1,55 @@
+module Lam.Nat where
+
+open import Haskell.Prelude using (Eq; _==_; True; False; Bool; []; _∷_; List; Maybe; Nothing; Just)
+
+data Nat : Set where
+  Z : Nat
+  S : Nat → Nat
+
+instance
+  iEqNat : Eq Nat
+  iEqNat ._==_ Z Z = True
+  iEqNat ._==_ (S x) (S y) = x == y
+  iEqNat ._==_ _ _ = False
+
+{-# COMPILE AGDA2HS Nat deriving (Eq, Show) #-}
+
+ltNat : Nat → Nat → Bool
+ltNat Z (S _) = True
+ltNat (S x) (S y) = ltNat x y
+ltNat _ _     = False
+
+{-# COMPILE AGDA2HS ltNat #-}
+
+inc : Nat → Nat
+inc = S
+
+{-# COMPILE AGDA2HS inc #-}
+
+dec : Nat → Nat
+dec Z = Z
+dec (S x) = x
+
+{-# COMPILE AGDA2HS dec #-}
+
+length : {A : Set} → List A -> Nat
+length [] = Z
+length (_ ∷ xs) = S (length xs)
+
+data _≤_ : Nat → Nat → Set where
+  z≤ : ∀ {i} → Z ≤ i
+  s≤s : ∀ {i j} → i ≤ j → (S i) ≤ (S j)
+
+_<_ : Nat -> Nat -> Set
+i < j = S i ≤ j
+
+lookupMaybe : {t : Set} → Nat → List t → Maybe t
+lookupMaybe _ []           = Nothing
+lookupMaybe Z (h ∷ _)      = Just h
+lookupMaybe (S i) (_ ∷ t) = lookupMaybe i t
+
+{-# COMPILE AGDA2HS lookupMaybe #-}
+
+lookup : {A : Set} -> (l : List A) -> (i : Nat) -> (h : i < length l) -> A
+lookup (x ∷ l) Z h = x
+lookup (x ∷ l) (S i) (s≤s h) = lookup l i h

src/Lam/Agda/Lam/TypeChecker.agda

@@ -5,6 +5,7 @@ open import Data.List using (List)
 open import Haskell.Prelude
 
 open import Lam.Data
+open import Lam.Nat
 open import Lam.UtilsAgda
 
 TypingContext : Set

src/Lam/Agda/Lam/UtilsAgda.agda

@@ -3,53 +3,22 @@ module Lam.UtilsAgda where
 import Agda.Builtin.Nat
 open import Data.Empty       using (⊥-elim)
 open import Data.Fin.Base    using (fromℕ<)
-open import Data.List
-open import Data.Nat         using (ℕ; zero; suc; _<_)
+open import Data.List hiding (length; lookup)
 open import Data.Product     using (_×_) renaming (_,_ to ⟨_,_⟩)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
 open import Relation.Nullary using (¬_)
 
 open import Haskell.Prelude hiding (_<_; length; lookup; _×_; Nat; cong; cong₂; case_of_)
 
 open import Lam.Data
+open import Lam.Nat
 
 -- removing the equality proof of case_of_
 myCaseOf : {a b : Set} → a → (a → b) → b
 myCaseOf x f = f x
 
 {-# COMPILE AGDA2HS myCaseOf #-}
 
--- Operations defined over our naturals
-
-natToℕ : Nat → ℕ
-natToℕ Z = zero
-natToℕ (S x) = suc (natToℕ x)
-
-eqNat : Nat → Nat → Bool
-eqNat Z Z         = True
-eqNat (S x) (S y) = eqNat x y
-eqNat _ _         = False
-
-{-# COMPILE AGDA2HS eqNat #-}
-
-ltNat : Nat → Nat → Bool
-ltNat Z (S _) = True
-ltNat (S x) (S y) = ltNat x y
-ltNat _ _     = False
-
-{-# COMPILE AGDA2HS ltNat #-}
-
-inc : Nat → Nat
-inc = S
-
-{-# COMPILE AGDA2HS inc #-}
-
-dec : Nat → Nat
-dec Z = Z
-dec (S x) = x
-
-{-# COMPILE AGDA2HS dec #-}
-
 eqType : TypeL → TypeL → Bool
 eqType BoolT        BoolT       = True
 eqType IntT         IntT        = True
@@ -61,16 +30,9 @@ eqType _            _           = False
 
 {-# COMPILE AGDA2HS eqType #-}
 
-lookupMaybe : {t : Set} → Nat → List t → Maybe t
-lookupMaybe _ []           = Nothing
-lookupMaybe Z (h ∷ _)      = Just h
-lookupMaybe (S i) (_ ∷ t) = lookupMaybe i t
-
-{-# COMPILE AGDA2HS lookupMaybe #-}
-
-lookup≡ : {t : Set} {l : List t} {i : Nat} → (h : (natToℕ i) < length l) → (lookupMaybe i l) ≡ Just (lookup l (fromℕ< h))
-lookup≡ {t} {x ∷ l} {Z} h  = _≡_.refl
-lookup≡ {t} {x ∷ l} {S i} h = lookup≡ {t} {l} {i} (Data.Nat.≤-pred h)
+lookup≡ : {t : Set} {l : List t} {i : Nat} → (h : i < length l) → (lookupMaybe i l) ≡ Just (lookup l i h)
+lookup≡ {t} {x ∷ l} {Z} h = refl
+lookup≡ {t} {x ∷ l} {S i} (s≤s h) = lookup≡ h 
 
 &&to× : {a b : Bool} → (a && b) ≡ True → a ≡ True × b ≡ True
 &&to× {True} {True} h = ⟨ refl , refl ⟩
@@ -100,19 +62,15 @@ eqType-refl (Sum t1 t2) =
 injection-maybe : ∀ {t : Set} {a : t} → ¬ (Nothing ≡ Just a)
 injection-maybe = λ ()
 
-lookup?< : {t : Set} {l : List t} {i : Nat} {a : t} → lookupMaybe i l ≡ Just a → (natToℕ i) < length l
+lookup?< : {t : Set} {l : List t} {i : Nat} {a : t} → lookupMaybe i l ≡ Just a → i < length l
 lookup?< {_} {[]} {_} {_} eq    = ⊥-elim (injection-maybe eq)
-lookup?< {t} {x ∷ l} {Z} eq  = Data.Nat.s≤s Data.Nat.z≤n
-lookup?< {t} {x ∷ l} {S i} eq = Data.Nat.s≤s (lookup?< {t} {l} {i} eq)
+lookup?< {t} {x ∷ l} {Z} eq  = s≤s z≤
+lookup?< {t} {x ∷ l} {S i} eq = s≤s (lookup?< eq)
 
 iteAbs : {t : Set} {x y z : t} {b : Bool} →
         ¬ y ≡ z → (if b then x else y) ≡ z → b ≡ True × x ≡ z
 iteAbs {t} {x} {y} {z} {False} h₁ h₂ = ⊥-elim (h₁ h₂)
 iteAbs {t} {x} {y} {z} {True} h₁ h₂ = ⟨ refl , h₂ ⟩
 
-liftEqNat : {n1 n2 : ℕ} → Agda.Builtin.Nat._==_ n1 n2 ≡ Bool.true → n1 ≡ n2
-liftEqNat {zero} {zero} h = refl
-liftEqNat {suc n1} {suc n2} h = cong suc (liftEqNat {n1} {n2} h)
-
 Just-injective : ∀ {A : Set} {a b : A} → (Just a) ≡ (Just b) → _≡_ a b
 Just-injective refl = refl

src/Lam/Nat.hs

@@ -0,0 +1,23 @@
+module Lam.Nat where
+
+data Nat = Z
+         | S Nat
+             deriving (Eq, Show)
+
+ltNat :: Nat -> Nat -> Bool
+ltNat Z (S _) = True
+ltNat (S x) (S y) = ltNat x y
+ltNat _ _ = False
+
+inc :: Nat -> Nat
+inc = S
+
+dec :: Nat -> Nat
+dec Z = Z
+dec (S x) = x
+
+lookupMaybe :: Nat -> [t] -> Maybe t
+lookupMaybe _ [] = Nothing
+lookupMaybe Z (h : _) = Just h
+lookupMaybe (S i) (_ : t) = lookupMaybe i t
+