more pedantry, making agda2hs happy

Makefile

@@ -4,7 +4,8 @@ LIBRARIES =
 
 .PHONY: app alllib clean clean-lib clean-agdai
 
-alllib: lib lib/Agda/Core/Syntax.hs lib/Agda/Core/Reduce.hs
+alllib: lib lib/Agda/Core/Syntax.hs lib/Agda/Core/Reduce.hs lib/Agda/Core/Typechecker.hs \
+  lib/Agda/Core/TCM.hs
 
 # alllib: lib lib/*.hs
 

src/Agda/Core/Context.agda

@@ -38,15 +38,15 @@ private variable
 
 lookupVar : (Γ : Context α) (@0 x : name) (p : x ∈ α) → Type α
 lookupVar CtxEmpty x p = inEmptyCase p
-lookupVar (CtxExtend Γ y s) x p = raise (rezz _) (inBindCase p
+lookupVar (CtxExtend g y s) x p = raise (rezz _) (inBindCase p
   (λ _ → s)
-  (λ q → lookupVar Γ x q))
+  (λ q → lookupVar g x q))
 
 {-# COMPILE AGDA2HS lookupVar #-}
 
-rezz-scope : (Γ : Context α) → Rezz (Scope name) α
-rezz-scope CtxEmpty = rezz _
-rezz-scope (CtxExtend Γ x _) =
-  rezzCong (λ t → (singleton x) <> t) (rezz-scope Γ)
+rezzScope : (Γ : Context α) → Rezz (Scope name) α
+rezzScope CtxEmpty = rezz _
+rezzScope (CtxExtend g x _) =
+  rezzCong (λ t → (singleton x) <> t) (rezzScope g)
 
-{-# COMPILE AGDA2HS rezz-scope #-}
+{-# COMPILE AGDA2HS rezzScope #-}

src/Agda/Core/Reduce.agda

@@ -6,14 +6,15 @@ module Agda.Core.Reduce
   (@0 globals : Globals name)
   where
 
-open import Haskell.Prelude hiding (All; coerce)
+open import Haskell.Prelude hiding (All; coerce; _,_,_) renaming (_,_ to infixr 5 _,_)
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Refinement
 open import Haskell.Extra.Erase
 open import Utils.Either
 
 open import Agda.Core.Syntax globals
 open import Agda.Core.Substitute globals
+open import Agda.Core.Utils
 
 private open module @0 G = Globals globals
 
@@ -148,12 +149,6 @@ opaque
 
 {-# COMPILE AGDA2HS step #-}
 
-data Fuel : Set where
-  None : Fuel
-  More : Fuel → Fuel
-
-{-# COMPILE AGDA2HS Fuel #-}
-
 -- TODO: make this into a `where` function once 
 -- https://github.com/agda/agda2hs/issues/264 is fixed
 reduceState : Rezz _ α
@@ -174,8 +169,16 @@ reduceClosed = reduce (rezz _)
 
 {-# COMPILE AGDA2HS reduceClosed #-}
 
-_reducesTo_ : (v w : Term α) → Set
-_reducesTo_ {α = α} v w = 
-  ∃ (Rezz _ α) λ r    → 
-  ∃ Fuel       λ fuel → 
-  reduce r v fuel ≡ Just w
+@0 _reducesTo_ : (v w : Term α) → Set
+_reducesTo_ {α = α} v w = Σ[ r ∈ Rezz _ α ] Σ[ f ∈ Fuel ] reduce r v f ≡ Just w
+
+reduceTo : Rezz _ α
+       → (v : Term α)
+       → Fuel
+       → Maybe (∃[ u ∈ Term α ] v reducesTo u)
+reduceTo r v f =
+  case reduce r v f of λ where
+    Nothing        → Nothing
+    (Just u) ⦃ p ⦄ → Just (u ⟨ r , f , p ⟩)
+
+{-# COMPILE AGDA2HS reduceTo #-}

src/Agda/Core/TCM.agda

@@ -1,100 +1,80 @@
+module Agda.Core.TCM where
+
+
 open import Haskell.Prelude hiding ( All; m )
 open import Scope
 open import Agda.Core.GlobalScope
+open import Agda.Core.Utils
 
-import Agda.Core.Syntax as Syntax
-
-module Agda.Core.TCM
-    {@0 name    : Set}
-    (@0 globals : Globals name)
-  where
 
-open import Agda.Core.Reduce globals
+TCError = String
+{-# COMPILE AGDA2HS TCError #-}
 
-module Pair where
-  open import Agda.Primitive
-  private variable
-    ℓ ℓ′ : Level
-
-  record Pair (a : Set ℓ) (p : (@0 _ : a) → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
-    constructor MkPair
-    field
-      pfst : a
-      psnd : p pfst
-  open Pair public
-  {-# COMPILE AGDA2HS Pair #-}
+record TCM (a : Set) : Set where
+  constructor MkTCM
+  field runTCM : Fuel → Either TCError a
+open TCM public
+{-# COMPILE AGDA2HS TCM #-}
 
-open Pair
+tcmFuel : TCM Fuel
+tcmFuel = MkTCM Right
+{-# COMPILE AGDA2HS tcmFuel #-}
 
-pattern _⟨_⟩ a b = MkPair a b
+tcError : TCError -> TCM a
+tcError = MkTCM ∘ const ∘ Left
+{-# COMPILE AGDA2HS tcError #-}
 
-infix 4 ∃
-∃ : (a : Set) (p : @0 a → Set) → Set
-∃ a p = Pair a p
-{-# COMPILE AGDA2HS ∃ inline #-}
+private
+  fmapTCM : (a → b) → TCM a → TCM b
+  fmapTCM f = MkTCM ∘ fmap (fmap f) ∘ runTCM
+  {-# COMPILE AGDA2HS fmapTCM #-}
 
-TCError = String
-
-record TCM (a : Set) : Set where
-  constructor mkTCM
-  field
-    runTCM : Fuel → Either TCError a
+  pureTCM : a → TCM a
+  pureTCM = MkTCM ∘ const ∘ Right
+  {-# COMPILE AGDA2HS pureTCM #-}
+
+  liftA2TCM : (a → b → c) → TCM a → TCM b → TCM c
+  liftA2TCM g ta tb = MkTCM λ f → g <$> runTCM ta f <*> runTCM tb f
+  {-# COMPILE AGDA2HS liftA2TCM #-}
 
-tcmFuel : TCM Fuel
-tcmFuel = mkTCM (λ f → Right f)
-
-fmapTCM : (a → b) → TCM a → TCM b
-fmapTCM f (mkTCM runTCM) = mkTCM (fmap (fmap f) runTCM)
-
-pureTCM : a → TCM a
-pureTCM a = mkTCM (pure (pure a))
-
-liftA2TCM : (a → b → c) → TCM a → TCM b → TCM c
-liftA2TCM f (mkTCM ta) (mkTCM tb) = mkTCM (liftA2Fuel (liftA2Either f) ta tb)
-  where
-    liftA2Fuel : {a b c f : Set} → (a → b → c) → (f → a) → (f → b) → (f → c)
-    liftA2Fuel f a b = f <$> a <*> b
-    liftA2Either : {a b c e : Set} → (a → b → c) → Either e a → Either e b → Either e c
-    liftA2Either f a b = f <$> a <*> b
-
-bindTCM : TCM a → (a → TCM b) → TCM b
-bindTCM ma mf = mkTCM (bindTCM' ma mf)
-  where
-  bindTCM' : TCM a → (a → TCM b) → Fuel → Either TCError b
-  bindTCM' (mkTCM ma) mf f with (ma f)
-  ... | Left e = Left e
-  ... | Right v = TCM.runTCM (mf v) f
+  bindTCM : TCM a → (a → TCM b) → TCM b
+  bindTCM ma mf = MkTCM λ f → do v ← runTCM ma f ; runTCM (mf v) f
+  {-# COMPILE AGDA2HS bindTCM #-}
 
 instance
   iFunctorTCM : Functor TCM
-  Functor.fmap iFunctorTCM = fmapTCM
-  Functor._<$>_ iFunctorTCM = fmapTCM
-  Functor._<&>_ iFunctorTCM = λ x f → fmapTCM f x
-  Functor._<$_ iFunctorTCM = λ x m → fmapTCM (λ b → x {{b}}) m
-  Functor._$>_ iFunctorTCM = λ m x → fmapTCM (λ b → x {{b}}) m
-  Functor.void iFunctorTCM = fmapTCM (const tt)
+  iFunctorTCM .fmap  = fmapTCM
+  iFunctorTCM ._<$>_ = fmapTCM
+  iFunctorTCM ._<&>_ = λ x f → fmapTCM f x
+  iFunctorTCM ._<$_  = λ x m → fmapTCM (λ b → x {{b}}) m
+  iFunctorTCM ._$>_  = λ m x → fmapTCM (λ b → x {{b}}) m
+  iFunctorTCM .void  = fmapTCM (const tt)
+  {-# COMPILE AGDA2HS iFunctorTCM #-}
 
+instance
   iApplicativeTCM : Applicative TCM
-  Applicative.pure iApplicativeTCM = pureTCM
-  Applicative._<*>_ iApplicativeTCM = liftA2TCM id
-  Applicative.super iApplicativeTCM = iFunctorTCM
-  Applicative._<*_ iApplicativeTCM = liftA2TCM (λ z _ → z)
-  Applicative._*>_ iApplicativeTCM = liftA2TCM (λ _ z → z)
+  iApplicativeTCM .pure  = pureTCM
+  iApplicativeTCM ._<*>_ = liftA2TCM id
+  iApplicativeTCM ._<*_  = liftA2TCM (λ z _ → z)
+  iApplicativeTCM ._*>_  = liftA2TCM (λ _ z → z)
+  {-# COMPILE AGDA2HS iApplicativeTCM #-}
 
+instance
   iMonadTCM : Monad TCM
-  Monad._>>=_ iMonadTCM = bindTCM
-  Monad.super iMonadTCM = iApplicativeTCM
-  Monad.return iMonadTCM = pureTCM
-  Monad._>>_ iMonadTCM = λ m m₁ → bindTCM m (λ x → m₁ {{x}})
-  Monad._=<<_ iMonadTCM = flip bindTCM
+  iMonadTCM ._>>=_  = bindTCM
+  iMonadTCM .return = pureTCM
+  iMonadTCM ._>>_   = λ x y → bindTCM x (λ z → y {{z}})
+  iMonadTCM ._=<<_  = flip bindTCM
+  {-# COMPILE AGDA2HS iMonadTCM #-}
 
 liftEither : Either TCError a → TCM a
-liftEither (Left e) = mkTCM λ f → Left e
-liftEither (Right v) = mkTCM λ f → Right v
+liftEither (Left e) = MkTCM λ f → Left e
+liftEither (Right v) = MkTCM λ f → Right v
+
+{-# COMPILE AGDA2HS liftEither #-}
 
 liftMaybe : Maybe a → TCError → TCM a
-liftMaybe Nothing e = mkTCM λ f → Left e
-liftMaybe (Just x) e = mkTCM λ f → Right x
+liftMaybe Nothing e = MkTCM λ f → Left e
+liftMaybe (Just x) e = MkTCM λ f → Right x
 
-tcError : TCError -> TCM a
-tcError e = mkTCM λ f → Left e
+{-# COMPILE AGDA2HS liftMaybe #-}