need to throw this stuff on git

.gitignore

@@ -0,0 +1 @@
+.stack-work

LICENSE

@@ -0,0 +1,30 @@
+Copyright Abigail Magalhães (c) 2020
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Abigail Magalhães nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1 @@
+# setoid

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

hie.yaml

@@ -0,0 +1,2 @@
+cradle:
+  stack:

setoid.cabal

@@ -0,0 +1,36 @@
+name:                setoid
+version:             0.1.0.0
+-- synopsis:
+-- description:
+homepage:            https://github.com/plt-hokusai/setoid#readme
+license:             BSD3
+license-file:        LICENSE
+author:              Abigail Magalhães
+maintainer:          [email protected]
+copyright:           2020 Abigail Magalhães
+category:            Web
+build-type:          Simple
+cabal-version:       >=1.10
+extra-source-files:  README.md
+
+executable setoid
+  hs-source-dirs:      src
+  main-is:             Main.hs
+  default-language:    Haskell2010
+  build-depends:       mtl
+                     , syb
+                     , base
+                     , text
+                     , ghc-prim
+                     , containers
+                     , unordered-containers
+
+  other-modules:       Syntax
+                     , Syntax.Pretty
+                     , Presyntax
+                     , Evaluate
+                     , Elaboration
+                     , Value
+                     , Presyntax.Lexer
+                     , Presyntax.Parser
+                     , Elaboration.Monad

src/Elaboration.hs

@@ -0,0 +1,253 @@
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DerivingVia #-}
+module Elaboration where
+
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Concurrent
+
+import qualified Data.HashMap.Strict as HashMap
+import qualified Data.IntMap.Strict as IntMap
+import Data.Text (Text)
+
+import Elaboration.Monad
+
+import Evaluate
+
+import Presyntax
+
+import Syntax
+
+import System.IO.Unsafe ( unsafeDupablePerformIO )
+
+import Value
+
+elabNext :: MVar Int
+elabNext = unsafeDupablePerformIO (newMVar 0)
+{-# NOINLINE elabNext #-}
+
+freshMeta :: Value -> ElabM Term
+freshMeta expected = do
+  ctx <- ask
+  names <- getNames
+  thisMeta <- liftIO $ do
+    m <- modifyMVar elabNext $ \x -> pure (x + 1, x)
+    modifyMVar_ elabMetas $ pure . IntMap.insert m (Unsolved names expected)
+    pure m
+  pure $ NewMeta (MV thisMeta) (elabBound ctx)
+
+insert :: Term -> VTy -> ElabM (Term, VTy)
+insert f (VPi Im _ d r) = do
+  t <- freshMeta d
+  t_nf <- asks (flip evaluate t . elabEnv)
+  insert (App Im f t) (r $$ t_nf)
+insert f x = pure (f, x)
+
+insert' :: Term -> VTy -> ElabM (Term, VTy)
+insert' t@(Lam Im _ _) ty = pure (t, ty)
+insert' t ty = insert t ty
+
+infer :: RawExpr -> ElabM (Term, VTy)
+infer (RSrcPos start end expr) = local (\st -> st { elabSourcePos = (start, end) }) (infer expr)
+
+infer (Rvar name) = ask >>= lookup where
+  lookup ElabState{elabNames, elabConstrs, elabLevel} =
+    case HashMap.lookup name elabNames of
+      Just (l, t) -> pure (Bv (lvl2Ix elabLevel l), t)
+      Nothing ->
+        case HashMap.lookup name elabConstrs of
+          Just t  -> pure (Con name, t)
+          Nothing -> typeError (NotInScope name)
+
+infer (Rapp p x y) = do
+  (x, x_ty) <-
+    infer x >>= \(x, x_ty) ->
+      case p of
+        Ex -> insert x x_ty
+        _  -> pure (x, x_ty)
+
+  (_, d, r) <- isPiType p x_ty
+  y         <- check y d
+  y_nf      <- asks (flip evaluate y . elabEnv)
+
+  pure (App p x y, r $$ y_nf)
+
+infer (Rpi e v d r) = do
+  d <- check d VType
+  d_nf <- asks (flip evaluate d . elabEnv)
+  assumeLocal v d_nf $ do
+    r <- check r VType
+    pure (Pi e v d r, VType)
+
+infer (Rsigma v d r) = do
+  d <- check d VType
+  d_nf <- asks (flip evaluate d . elabEnv)
+  assumeLocal v d_nf $ do
+    r <- check r VType
+    pure (Sigma v d r, VType)
+
+infer (Rlet v t d b) = do
+  t    <- check t VType
+  t_nf <- asks (flip evaluate t . elabEnv)
+
+  d    <- check d t_nf
+  d_nf <- asks (flip evaluate d . elabEnv)
+
+  defineLocal v t_nf d_nf $ do
+    (b, ty) <- infer b
+    pure (Let v t d b, ty)
+
+infer Rtype = pure (Type, VType)
+
+infer Rhole = do
+  ty <- freshMeta VType
+  ty_nf <- asks (flip evaluate ty . elabEnv)
+  tm <- freshMeta ty_nf
+  pure (tm, ty_nf)
+
+infer (Rlam p v t) = do
+  env <- asks elabEnv
+  lvl <- asks elabLevel
+  dom <- freshMeta VType
+  let dom_nf = evaluate env dom
+  assumeLocal v dom_nf $ do
+    (b, rng) <- infer t
+    pure (Lam p v b, VPi p v dom_nf (Closure env (quote (succ lvl) rng)))
+
+infer Rtop  = pure (Top, VType)
+infer Runit = pure (Unit, VTop)
+
+infer (Req a b) = do
+  t <- freshMeta VType
+  t_nf <- asks (flip evaluate t . elabEnv)
+  a <- check a t_nf
+  b <- check b t_nf
+  pure (Id t a b, VType)
+
+infer Rrefl =
+  pure (Refl, forAll Im "A" VType $ \a -> forAll Im "x" a $ \x -> VEq a x x)
+
+infer Rcoe =
+  pure ( Coe
+       , forAll Im "A" VType $ \a ->
+         forAll Im "B" VType $ \b ->
+         forAll Ex "_" (VEq VType a b) $ \_ ->
+         forAll Ex "_" a $ const b
+       )
+
+infer Rcong =
+  pure ( Cong
+       , forAll Im "A" VType $ \a ->
+         forAll Im "B" VType $ \b ->
+         forAll Im "x" a $ \x ->
+         forAll Im "y" a $ \y ->
+         forAll Ex "f" (forAll Ex "_" a (const b)) $ \f ->
+         forAll Ex "p" (VEq a x y) $ \_ ->
+           VEq b (vApp f Ex x) (vApp f Ex y)
+       )
+
+infer Rsym =
+  pure ( Sym
+       , forAll Im "A" VType $ \a -> forAll Im "x" a $ \x -> forAll Im "y" a $ \y -> forAll Ex "p" (VEq a x y) $ \_ -> VEq a y x
+       )
+
+infer (Rproj1 e) = do
+  (t, ty)   <- infer e
+  (_, d, _) <- isSigmaType ty
+  pure (Proj1 t, d)
+
+infer (Rproj2 e) = do
+  (t, ty)   <- infer e
+  t_nf      <- asks (flip evaluate t . elabEnv)
+  (_, _, r) <- isSigmaType ty
+  pure (Proj2 t, r $$ vProj1 t_nf)
+
+infer c = do
+  t <- asks elabSwitches
+  when (t >= 128) $
+    error $ "Unhandled case in type checker, stack overflew etc: " ++ show c
+
+  t    <- freshMeta VType
+  t_nf <- asks (flip evaluate t . elabEnv)
+
+  c <- local (\e -> e { elabSwitches = succ (elabSwitches e)}) $
+    check c t_nf
+
+  pure (c, t_nf)
+
+check :: RawExpr -> VTy -> ElabM Term
+check (RSrcPos start end expr) ty = local (\st -> st { elabSourcePos = (start, end) }) (check expr ty)
+
+check (Rlam e v t) (VPi e' _ d r) | e == e' = do
+  level <- asks (unLvl . elabLevel)
+  assumeLocal v d $
+    Lam e v <$> check t (r $$ vVar (Bound level))
+
+check t (VPi Im x d r) = do
+  level <- asks (unLvl . elabLevel)
+  assumeLocal x d $
+    Lam Im x <$> check t (r $$ vVar (Bound level))
+
+check (Rlam e v t) ty = do
+  (_, d, r) <- isPiType e ty
+  level <- asks (unLvl . elabLevel)
+  assumeLocal v d $
+    Lam e v <$> check t (r $$ vVar (Bound level))
+
+check (Rlet v t d b) ty = do
+  t    <- check t VType
+  t_nf <- asks (flip evaluate t . elabEnv)
+
+  d    <- check d t_nf
+  d_nf <- asks (flip evaluate d . elabEnv)
+
+  defineLocal v t_nf d_nf $ do
+    b <- check b ty
+    pure (Let v t d b)
+
+check (Rpair a b) ty = do
+  (_, d, r) <- isSigmaType ty
+  a <- check a d
+  a_nf <- asks (flip evaluate a . elabEnv)
+  b <- check b (r $$ a_nf)
+  pure (Pair a b)
+
+check e ty = do
+  (new, e_ty) <- uncurry insert =<< infer e
+  unify e_ty ty
+    `catchError` \_ -> do
+      l <- asks elabLevel
+      names <- getNames
+      typeError (NotEqual names (quote l (zonk ty)) (quote l (zonk e_ty)))
+  pure new
+
+isPiType :: Plicity -> VTy -> ElabM (Text, VTy, Closure)
+isPiType i = go . force where
+  go (VPi i' a b c)
+    | i == i' = pure (a, b, c)
+  go ty | not (flexible ty) = do
+    l <- asks elabLevel
+    names <- getNames
+    typeError (NotFunction names (quote l ty))
+  go ty = do
+    env <- asks elabEnv
+    t <- freshMeta VType
+    let t_nf = evaluate env t
+    assumeLocal "α" t_nf $ do
+      r <- freshMeta VType
+      unify ty (VPi i "α" t_nf (Closure env r))
+      pure ("α", t_nf, Closure env r)
+
+isSigmaType :: VTy -> ElabM (Text, VTy, Closure)
+isSigmaType = go . force where
+  go (VSigma a b c) = pure (a, b, c)
+  go ty = do
+    env <- asks elabEnv
+    t <- freshMeta VType
+    let t_nf = evaluate env t
+    assumeLocal "α" t_nf $ do
+      r <- freshMeta VType
+      unify ty (VSigma "α" t_nf (Closure env r))
+      pure ("α", t_nf, Closure env r)

src/Elaboration/Monad.hs

@@ -0,0 +1,97 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DerivingVia #-}
+module Elaboration.Monad where
+
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Applicative
+
+import qualified Data.HashMap.Strict as HashMap
+import qualified Data.Sequence as Seq
+import Data.HashMap.Strict (HashMap)
+import Data.Text (Text)
+
+import Syntax
+
+import Value
+
+
+data ElabState =
+  ElabState
+    { elabEnv       :: {-# UNPACK #-} !Env
+    , elabLevel     :: {-# UNPACK #-} !Level
+    , elabSwitches  :: {-# UNPACK #-} !Int
+    , elabNames     :: HashMap Text (Level, VTy)
+    , elabConstrs   :: HashMap Text VTy
+    , elabBound     :: [BoundDef]  
+    , elabSourcePos :: ((Int, Int), (Int, Int))
+    }
+  deriving (Eq)
+
+emptyElabState :: ElabState
+emptyElabState = ElabState emptyEnv (Lvl 0) 0 mempty mempty [] ((0, 0), (0, 0))
+
+getNames :: MonadReader ElabState m => m [Text]
+getNames = asks (map go . elabBound) where
+  go (BDBound n) = n
+  go (BDDefined n) = n
+
+data ElabError
+  = NotInScope     Text
+  | NotFunction    [Text] Term
+  | NotEqual       [Text] Term Term
+  | CantSolveMeta  [Text] Term Term
+  deriving (Show)
+
+data ProgError
+  = ProgError { peErr :: ElabError
+              , peSL :: !Int
+              , peSC :: !Int
+              , peEL :: !Int
+              , peEC :: !Int
+              }
+  deriving (Show)
+
+newtype ElabM a
+  = ElabM { runElab :: ElabState -> IO (Either [ProgError] a) }
+  deriving
+    ( Functor
+    , Applicative
+    , Monad
+
+    , Alternative
+    , MonadPlus
+
+    , MonadReader ElabState
+    , MonadError [ProgError]
+    , MonadIO
+    )
+  via ReaderT ElabState (ExceptT [ProgError] IO)
+
+typeError :: ElabError -> ElabM a
+typeError err = do
+  (s, e) <- asks elabSourcePos
+  throwError [uncurry (uncurry (ProgError err) s) e]
+
+assumeLocal :: Text -> VTy -> ElabM a -> ElabM a
+assumeLocal name tipe = local go where
+  go r =
+    r { elabLevel = succ (elabLevel r)
+      , elabNames = HashMap.insert name (elabLevel r, tipe) (elabNames r)
+      , elabEnv = (elabEnv r) {
+          locals = VGlued (HVar (Bound (unLvl (elabLevel r)))) mempty Nothing
+            Seq.<| locals (elabEnv r)
+        } 
+      , elabBound = BDBound name:elabBound r  
+      }
+
+defineLocal :: Text -> VTy -> Value -> ElabM a -> ElabM a
+defineLocal name tipe val = local go where
+  go r =
+    r { elabLevel = succ (elabLevel r)
+      , elabNames = HashMap.insert name (elabLevel r, tipe) (elabNames r)
+      , elabEnv = (elabEnv r) {
+          locals = val Seq.<| locals (elabEnv r)
+        } 
+      , elabBound = BDDefined name:elabBound r  
+      }

src/Evaluate.hs

@@ -0,0 +1,441 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Evaluate where
+
+import qualified Control.Exception as Exc
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Concurrent
+
+import qualified Data.IntMap.Strict as IntMap
+import qualified Data.Sequence as Seq
+import qualified Data.Text as T
+
+import Elaboration.Monad
+
+import GHC.Stack (HasCallStack)
+
+import Generics.SYB (mkT, everywhere)
+
+import Syntax
+
+import System.IO.Unsafe
+
+import Value
+import Data.Foldable
+import Syntax.Pretty (showWithPrec)
+
+evaluate :: HasCallStack => Env -> Term -> Value
+evaluate env (Var (Bound i)) =
+  case Seq.lookup i (locals env) of
+    Just x -> x
+    Nothing -> error $ "Variable of index " ++ show i ++ " not in scope"
+
+evaluate _ (Con t) = VGlued (HCon t) mempty Nothing
+
+evaluate _   Type = VType
+
+evaluate env (Pi p t d r)  = VPi p t (evaluate env d) (Closure env r)
+evaluate env (Lam p t b)   = VLam p t (Closure env b)
+evaluate env (App p f x)   = vApp (evaluate env f) p (evaluate env x)
+
+evaluate env (Sigma t d r) = VSigma t (evaluate env d) (Closure env r)
+evaluate env (Pair a b)    = VPair (evaluate env a) (evaluate env b)
+evaluate env (Proj1 a)     = vProj1 (evaluate env a)
+evaluate env (Proj2 a)     = vProj2 (evaluate env a)
+
+evaluate _   (Meta m)         = VGlued (HMeta m) mempty Nothing
+evaluate env (NewMeta m mask) = VGlued (HMeta m) (getVals (locals env) mask) Nothing where
+  getVals Seq.Empty []                    = Seq.Empty
+  getVals (v Seq.:<| seq) (BDBound _:bds)   = AppEx v Seq.:<| getVals seq bds
+  getVals (_ Seq.:<| seq) (BDDefined _:bds) = getVals seq bds
+
+evaluate _ Top = VTop
+evaluate _ Unit = VUnit
+
+evaluate _ Refl = VGlued HRefl mempty Nothing
+evaluate _ Coe  =
+  function Im (T.pack "A") $ \a ->
+  function Im (T.pack "B") $ \b ->
+  function Ex (T.pack "p") $ \p ->
+  function Ex (T.pack "x") $ \x ->
+    vCoe a b p x
+
+evaluate _ Cong =
+  function Im (T.pack "A") $ \a ->
+  function Im (T.pack "B") $ \b ->
+  function Im (T.pack "x") $ \x ->
+  function Im (T.pack "y") $ \y ->
+  function Ex (T.pack "f") $ \f ->
+  function Ex (T.pack "p") $ \p ->
+    vCong a b x y f p
+
+evaluate _ Sym =
+  function Im (T.pack "A") $ \a ->
+  function Im (T.pack "x") $ \x ->
+  function Im (T.pack "y") $ \y ->
+  function Ex (T.pack "p") $ \p ->
+    vSym a x y p
+
+evaluate e (Let _ _ c d) = evaluate e' d where
+  e' = e { locals = evaluate e c Seq.:<| locals e }
+
+evaluate env (Id a b c) = vId (evaluate env a) (evaluate env b) (evaluate env c)
+
+vId :: Value -> Value -> Value -> Value
+vId kind a b =
+  let stuck  = VEq kind a b
+      solve  = VEqG kind a b
+      never  = solve vBottom
+      always = solve VTop
+   in
+  case force kind of
+    VType ->
+      case (a, b) of
+        (VTop, VTop) -> always
+
+        (VType, VType) -> always
+
+        (VEqG _ _ _ a, b) -> vId VType a b
+        (a, VEqG _ _ _ b) -> vId VType a b
+
+        (VEq a _ _, VEq b _ _) -> vId VType a b
+
+        (VPi i _ d r, VPi i' _ d' r')
+          | i == i' ->
+            solve $
+              exists "p" (vId VType d d') $ \p ->
+              forAll Ex "x" d $ \x ->
+                vId VType (r $$ x) (r' $$ vCoe d d' p x)
+          | otherwise -> never
+
+        (VSigma _ d r, VSigma _ d' r') ->
+          solve $
+            exists "p" (vId VType d d') $ \p ->
+            forAll Ex "x" d $ \x ->
+              vId VType (r $$ x) (r' $$ vCoe d d' p x)
+
+        (VNe _ _, _) -> stuck
+        (_, VNe _ _) -> stuck
+
+        _ -> never
+
+    VTop -> always
+
+    VPi i t dom cod ->
+      solve $ forAll i t dom \vl -> vId (cod $$ vl) (vApp a i vl) (vApp b i vl)
+
+    VSigma t dom cod ->
+      -- a = (x, p)
+      -- b = (y, q)
+      -- (a, b) ≡ (c, d) : (x : A) * P x
+      --   ~> (path : a == c) * coe (cong A Type P path) b == d
+      let x = vProj1 a
+          y = vProj1 b
+          p = vProj2 a
+          q = vProj2 b
+       in solve $
+         exists t (vId dom x y) $ \pr ->
+           vId (cod $$ y) (vCoe (cod $$ x) (cod $$ y) (vCong dom VType x y (function Ex (T.pack "x") (cod $$)) pr) p) q
+
+    VEq{} -> solve VTop
+
+    _ -> stuck
+
+vBottom :: Value
+vBottom = forAll Im "A" VType id
+
+vCoe :: VTy -> VTy -> Value -> Value -> Value
+-- vCoe _ _ (VGlued HRefl _ _) element = element
+vCoe (VPi i _ d r) ty2@(VPi i' _ d' r') p f
+  | i /= i' = vApp p Ex ty2
+  | otherwise =
+    function i "x" $ \x ->
+      let p1 = vProj1 p -- d == d'
+          p2 = vProj2 p -- (x : A) -> r x == r' (coe p1 x)
+          x0 = vCoe d' d (vSym VType d d' p1) x
+       in vCoe (r $$ x0) (r' $$ x) (vApp p2 Ex x0) (vApp f i x0)
+ 
+vCoe tyA tyB proof element = splitFibration tyA tyB $ VGlued HCoe (Seq.fromList spine) Nothing where
+  spine = [AppIm tyA, AppIm tyB, AppEx proof, AppEx element]
+
+  -- Types are split fibrations
+  -- coe {A} {A} p x = x even when p /= refl
+  splitFibration tA tB vstuck = unsafeDupablePerformIO $ do
+    old <- readMVar elabMetas
+    t <- runElab (unify tA tB) emptyElabState
+    case t of
+      Left _ -> do
+        swapMVar elabMetas old
+        pure vstuck
+      Right _ -> pure element
+
+vCong :: Value -> Value -> Value -> Value -> Value -> Value -> Value
+vCong _a c _x _y g (force -> VGlued HCong (toList -> [AppIm a, AppIm _b, AppIm x, AppIm y, AppEx f, AppEx p]) _) =
+  VGlued HCong (Seq.fromList [AppIm a, AppIm c, AppIm x, AppIm y, AppEx (function Ex "x" (vApp g Ex . vApp f Ex)), AppEx p]) Nothing
+vCong _a b _x _ f (force -> VGlued HRefl (toList -> [AppIm _, AppIm x]) _) =
+  VGlued HRefl (Seq.fromList [AppIm b, AppIm (vApp f Ex x)]) Nothing
+vCong a b x y f p =
+  VGlued HCong (Seq.fromList [AppIm a, AppIm b, AppIm x, AppIm y, AppEx f, AppEx p]) Nothing
+
+vSym :: Value -> Value -> Value -> Value -> Value
+vSym a _ y (VGlued HRefl _ Nothing) =
+  VGlued HRefl (Seq.fromList [AppIm a, AppIm y]) Nothing
+vSym _ _ _ (VGlued HSym (toList -> [_a, _y, _x, AppEx p]) Nothing) = p
+vSym a x y p = VGlued HSym (Seq.fromList [AppIm a, AppIm x, AppIm y, AppEx p]) Nothing
+
+vApp :: HasCallStack => Value -> Plicity -> Value -> Value
+vApp (VGlued x s v) p r = VGlued x (s Seq.|> thing) (fmap (\v -> vApp v p r) v) where
+  thing =
+    case p of
+      Ex -> AppEx r
+      Im -> AppIm r
+vApp (VLam _ _ c) _ a = c $$ a
+vApp _fun _plic _arg = error "invalid application"
+
+vProj1 :: Value -> Value
+vProj1 (VPair a _) = a
+vProj1 x           = VProj1 x
+
+vProj2 :: Value -> Value
+vProj2 (VPair _ a) = a
+vProj2 x           = VProj2 x
+
+($$) :: HasCallStack => Closure -> Value -> Value
+Closure e t $$ v = evaluate e' t where
+  e' = e { locals = v Seq.:<| locals e }
+ClMeta (MetaFun f) $$ v = f v
+
+forAll :: Plicity -> T.Text -> Value -> (Value -> Value) -> Value
+forAll i t d = VPi i t d . ClMeta . MetaFun
+
+exists :: T.Text -> Value -> (Value -> Value) -> Value
+exists t d = VSigma t d . ClMeta . MetaFun
+
+function :: Plicity -> T.Text -> (Value -> Value) -> Value
+function i t = VLam i t . ClMeta . MetaFun
+
+quote :: HasCallStack => Level -> Value -> Term
+quote _ VType = Type
+
+quote l (VPi p t d r) = Pi p t (quote l d) (quote (succ l) (r $$ vVar (Bound (unLvl l))))
+quote l (VLam p t  b) = Lam p t (quote (succ l) (b $$ vVar (Bound (unLvl l))))
+
+quote l (VSigma t d r) = Sigma t (quote l d) (quote (succ l) (r $$ vVar (Bound (unLvl l))))
+quote l (VPair a b)    = Pair (quote l a) (quote l b)
+quote l (VProj1 a)     = Proj1 (quote l a)
+quote l (VProj2 a)     = Proj2 (quote l a)
+
+quote _ VTop  = Top
+quote _ VUnit = Unit
+
+quote l (VEq a b c) = Id (quote l a) (quote l b) (quote l c)
+-- quote l (VEqG _ _ _ d) = quote l d
+quote l (VEqG a b c _) = Id (quote l a) (quote l b) (quote l c)
+
+quote l (VGlued v s _) = foldl app v' s where
+  v' = case v of
+    HVar (Bound i) -> Bv (lvl2Ix l (Lvl i))
+    HCon t         -> Con t
+    HMeta m        -> Meta m
+    HRefl          -> Refl
+    HCoe           -> Coe
+    HCong          -> Cong
+    HSym           -> Sym
+
+  app f (AppEx t) = App Ex f (quote l t)
+  app f (AppIm t) = App Im f (quote l t)
+  app f SProj1 = Proj1 f
+  app f SProj2 = Proj2 f
+
+force :: Value -> Value
+force = unsafeDupablePerformIO . go where
+  go stuck@(VGlued (HMeta (MV m)) sp Nothing) = do
+    t <- readMVar elabMetas
+    case IntMap.lookup m t of
+      Just (Solved vl) -> go $ foldl vAppSp vl sp
+      _ -> pure stuck
+  go (VGlued _ _ (Just vl)) = go vl
+  go x = pure x
+
+vAppSp :: Value -> SpineThing -> Value
+vAppSp vl (AppEx f) = vApp vl Ex f
+vAppSp vl (AppIm f) = vApp vl Im f
+vAppSp vl SProj1 = vProj1 vl
+vAppSp vl SProj2 = vProj2 vl
+
+zonk :: Value -> Value
+zonk (VLam vis var body) = VLam vis var (ClMeta (MetaFun (\v -> zonk (body $$ v))))
+zonk (VPi vis var dom body) = VPi vis var (zonk dom) (ClMeta (MetaFun (\v -> zonk (body $$ v))))
+zonk (VSigma var dom body) = VSigma var (zonk dom) (ClMeta (MetaFun (\v -> zonk (body $$ v))))
+zonk t = everywhere (mkT force) t
+
+unify :: VTy -> VTy -> ElabM ()
+unify a b = asks elabLevel >>= flip go (a, b) where
+  go, go' :: Level -> (VTy, VTy) -> ElabM ()
+  go' l (VGlued h sp x, VGlued h' sp' y)
+    | h == h'                  = goSpine l sp sp'
+    | Just x <- x, Just y <- y = go l (x, y)
+
+  -- flexible head (solve meta)
+  go' l (VGlued (HMeta m) sp _, y) = solveMeta m sp y
+  go' _ (x, VGlued (HMeta m) sp _) = solveMeta m sp x
+
+  -- rigid heads (compare unfolding)
+  go' l (VGlued _ _ (Just x), y) = go l (x, y)
+  go' l (x, VGlued _ _ (Just y)) = go l (x, y)
+
+  go' _ (VType, VType) = pure ()
+  go' _ (VTop, VTop) = pure ()
+  go' _ (VUnit, VUnit) = pure ()
+
+  go' l (VPi i _ d r, VPi i' _ d' r') | i == i' = do
+    go l (d, d')
+    let i = unLvl l
+    go (succ l) (r $$ vVar (Bound i), r' $$ vVar (Bound i))
+
+  go' l (VSigma _ d r, VSigma _ d' r') = do
+    go l (d, d')
+    let i = unLvl l
+    go (succ l) (r $$ vVar (Bound i), r' $$ vVar (Bound i))
+
+  go' l (VLam i _ r, VLam i' _ r') | i == i' = do
+    let i = unLvl l
+    go (succ l) (r $$ vVar (Bound i), r' $$ vVar (Bound i))
+
+  go' l (VLam p _ r, t) = do
+    let i = unLvl l
+    go (succ l) (r $$ vVar (Bound i), vApp t p (vVar (Bound i)))
+
+  go' l (r, VLam p _ t) = do
+    let i = unLvl l
+    go (succ l) (vApp r p (vVar (Bound i)), t $$ vVar (Bound i))
+
+  go' l (VEqG a b c _, VEqG a' b' c' _) = go l (a, a') *> go l (b, b') *> go l (c, c')
+  go' l (VEq a b c, VEqG a' b' c' _)    = go l (a, a') *> go l (b, b') *> go l (c, c')
+  go' l (VEqG a b c _, VEq a' b' c')    = go l (a, a') *> go l (b, b') *> go l (c, c')
+  go' l (VEq a b c, VEq a' b' c')       = go l (a, a') *> go l (b, b') *> go l (c, c')
+
+  go' l (VEqG _ _ _ a, b) = go l (a, b)
+  go' l (a, VEqG _ _ _ b) = go l (a, b)
+
+  go' l (VProj1 a, VProj1 b) = go l (a, b)
+  go' l (VProj2 a, VProj2 b) = go l (a, b)
+  go' l (VPair a b, VPair a' b') = go l (a, a') >> go l (b, b')
+
+  go' l (a, b) = do
+    ns <- getNames
+    typeError (NotEqual ns (quote l a) (quote l b))
+  
+  go l (a, b) = go' l (force a, force b)
+
+  goSpine _ Seq.Empty Seq.Empty           = pure ()
+  goSpine l (AppEx x Seq.:<| xs) (AppEx y Seq.:<| ys) = do
+    go l (x, y)
+    goSpine l xs ys
+  goSpine l (AppIm x Seq.:<| xs) (AppIm y Seq.:<| ys) = do
+    go l (x, y)
+    goSpine l xs ys
+  goSpine l (x Seq.:<| xs) (y Seq.:<| ys) | x == y = goSpine l xs ys
+  goSpine l _ _ = do
+    ns <- getNames
+    typeError (NotEqual ns (quote l a) (quote l b))
+
+solveMeta :: HasCallStack => MetaVar -> Seq.Seq SpineThing -> VTy -> ElabM ()
+solveMeta (MV meta) spine rhs =
+  do
+    level <- asks elabLevel
+
+    pren <- invert level spine
+    rhs <- rename (MV meta) pren rhs
+    let solution = evaluate emptyEnv (lams (dom pren) rhs) 
+
+    -- need to deepSeq solutions here
+    -- no deepSeq? no problem
+
+    liftIO $ Exc.evaluate (length (show solution))
+
+    liftIO . modifyMVar_ elabMetas $ pure . IntMap.insert meta (Solved solution)
+  `catchError` \case
+    [] -> do
+      level <- asks elabLevel
+      names <- getNames
+      typeError (CantSolveMeta names (quote level (VGlued (HMeta (MV meta)) spine Nothing)) (quote level rhs))
+    cs -> throwError cs
+
+elabMetas :: MVar (IntMap.IntMap Meta)
+elabMetas = unsafeDupablePerformIO (newMVar mempty)
+{-# NOINLINE elabMetas #-}
+
+lams :: Level -> Term -> Term
+lams l = go (Lvl 0) where
+  go x t | x == l = t
+  go x t = Lam Ex (T.pack ("x" ++ show (unLvl x))) $ go (succ x) t
+
+data PartialRen
+  = PRen { dom :: {-# UNPACK #-} !Level
+         , rng :: {-# UNPACK #-} !Level
+         , sub :: IntMap.IntMap Level
+         }
+  deriving (Eq, Show, Ord)
+
+liftRen :: PartialRen -> PartialRen
+liftRen (PRen d r s) = PRen (succ d) (succ r) (IntMap.insert (unLvl r) d s)
+
+invert :: Level -> Seq.Seq SpineThing -> ElabM PartialRen
+invert gamma spine =
+  do
+    (dom, ren) <- go spine
+    pure (PRen dom gamma ren)
+  where
+    go Seq.Empty = pure (Lvl 0, mempty)
+    go (sp Seq.:|> AppEx t) = do
+      (dom, ren) <- go sp
+      case force t of
+        VGlued (HVar (Bound l)) Seq.Empty _
+          | IntMap.notMember l ren -> pure (succ dom, IntMap.insert l dom ren)
+        _ -> throwError []
+    go (_ Seq.:|> _) = throwError []
+
+rename :: HasCallStack => MetaVar -> PartialRen -> Value -> ElabM Term
+rename meta pren = go pren where
+  go :: HasCallStack => PartialRen -> Value -> ElabM Term
+  go pren (VGlued (HMeta m) sp _)
+    | m == meta = throwError []
+    | otherwise = goSp pren (Meta m) sp
+
+  go pren (VGlued (HVar (Bound m)) sp _) =
+    case IntMap.lookup m (sub pren) of
+      Just v -> goSp pren (Bv (lvl2Ix (dom pren) v)) sp
+      Nothing -> throwError []
+
+  go pren (VGlued h sp _) = goHead h >>= \h -> goSp pren h sp where
+    goHead HRefl      = pure Refl
+    goHead HCong      = pure Cong
+    goHead HCoe       = pure Coe
+    goHead HSym       = pure Sym
+
+  go pren (VPi p t d r) = Pi p t <$> go pren d <*> go (liftRen pren) (r $$ vVar (Bound (unLvl (rng pren))))
+  go pren (VLam p t x)  = Lam p t <$> go (liftRen pren) (x $$ vVar (Bound (unLvl (rng pren))))
+  go _ VType            = pure Type
+  go _ VTop             = pure Top
+  go _ VUnit            = pure Unit
+  
+  go pren (VSigma t d r) = Sigma t <$> go pren d <*> go (liftRen pren) (r $$ vVar (Bound (unLvl (rng pren))))
+  go pren (VPair a b) = Pair <$> go pren a <*> go pren b
+  go pren (VProj1 a) = Proj1 <$> go pren a
+  go pren (VProj2 a) = Proj2 <$> go pren a
+
+  go pren (VEq a b c)    = Id <$> go pren a <*> go pren b <*> go pren c
+  go pren (VEqG _ _ _ d) = go pren d
+
+  -- go pren x = error (show x)
+
+  goSp _ t Seq.Empty               = pure t
+  goSp pren t (sp Seq.:|> AppEx tm) = App Ex <$> goSp pren t sp <*> go pren tm
+  goSp pren t (sp Seq.:|> AppIm tm) = App Im <$> goSp pren t sp <*> go pren tm
+  goSp pren t (sp Seq.:|> SProj1) = Proj1 <$> goSp pren t sp
+  goSp pren t (sp Seq.:|> SProj2) = Proj2 <$> goSp pren t sp

src/Main.hs

@@ -0,0 +1,61 @@
+{-# LANGUAGE LambdaCase #-}
+module Main where
+
+import Presyntax.Parser
+
+import System.Environment (getArgs)
+import Elaboration
+import Elaboration.Monad
+import Control.Monad.Reader
+import Syntax
+import Evaluate (elabMetas, zonk, evaluate, quote)
+import Syntax.Pretty
+import Data.Foldable
+import Control.Concurrent
+import qualified Data.IntMap.Strict as Map
+import Value (Meta(Solved, Unsolved))
+
+main :: IO ()
+main = do
+  [path] <- getArgs
+  text <- readFile path
+  x <-
+    case parseString body text of
+      Left e -> error (show e)
+      Right x -> pure x
+
+  swapMVar elabMetas mempty
+  swapMVar elabNext 0
+
+  t <- runElab ((,) <$> infer x <*> ask) emptyElabState
+  case t of
+    Left e -> traverse_ (putStrLn . showProgError text) e
+    Right ((x, t), e) -> do
+      metas <- readMVar elabMetas
+      for_ (Map.toList metas) $ \case
+        (n, Unsolved names v) ->
+          putStrLn $ '?':show n ++ " : " ++ showWithPrec names 0 (quote (Lvl (length names)) (zonk v)) "" ++ " = ? " 
+        (n, Solved v) ->
+          putStrLn $ '?':show n ++ " = " ++ showTerm 0 (quote (Lvl 0) v) ""
+
+      putStrLn . flip id "" $ showTerm 0 x
+      putStrLn . flip id "" $ showString "Type: " . showTerm 0 (quote (Lvl 0) (zonk t))
+      let t = quote (Lvl 0) . zonk . evaluate (elabEnv e) $ x
+      putStrLn $ "Normal form: " ++ showTerm 0 t ""
+
+showProgError :: String -> ProgError -> String
+showProgError text (ProgError e sl sc el ec)
+  | sl == el, sl < length (lines text) =
+    let code = lines text
+        line = code !! sl
+
+        linum = show sl
+
+        caretLine = replicate (length linum) ' ' ++ " | " ++ replicate sc ' ' ++ "^" ++ replicate (ec - sc) '~'
+        paddedLine = replicate (length linum) ' ' ++ " | "
+     in unlines [ paddedLine
+                , linum ++ " | " ++ line
+                , caretLine
+                , showElabError e ""
+                ]
+  | otherwise = showElabError e ""

src/Presyntax.hs

@@ -0,0 +1,29 @@
+module Presyntax where
+
+import Data.Text (Text)
+import Syntax (Plicity)
+
+data RawExpr
+  = Rvar  Text
+  | Rapp  Plicity RawExpr RawExpr
+  | Rlam  Plicity Text    RawExpr
+  | Rpi   Plicity Text    RawExpr RawExpr
+  | Rlet  Text    RawExpr RawExpr RawExpr
+  | Rtype
+  | Rhole
+
+  | Rtop | Runit
+  | Rbot
+  | Req RawExpr RawExpr
+  | Rrefl
+  | Rcoe
+  | Rcong
+  | Rsym
+
+  | Rsigma Text RawExpr RawExpr
+  | Rpair RawExpr RawExpr
+  | Rproj1 RawExpr
+  | Rproj2 RawExpr
+
+  | RSrcPos (Int, Int) (Int, Int) RawExpr
+  deriving (Eq, Show, Ord)

src/Presyntax/Lexer.hs

@@ -0,0 +1,172 @@
+{-# LANGUAGE BangPatterns #-}
+module Presyntax.Lexer where
+
+import Data.Text (Text)
+
+import Data.Char
+import qualified Data.Text as T
+
+{- HLINT ignore -}
+data TokenClass
+  = Tok_var Text
+  | Tok_lambda
+
+  | Tok_type
+  | Tok_let
+  | Tok_in
+
+  -- Operations on equality
+  | Tok_coe
+  | Tok_cong
+  | Tok_refl
+  | Tok_sym
+
+  | Tok_proj1
+  | Tok_proj2
+
+  | Tok_top
+
+  | Tok_oparen
+  | Tok_cparen
+
+  | Tok_obrace
+  | Tok_cbrace
+
+  | Tok_arrow
+  | Tok_times
+  | Tok_colon
+  | Tok_comma
+  | Tok_semi
+  | Tok_equal
+  | Tok_under
+  | Tok_equiv
+  deriving (Eq, Show, Ord)
+
+data Token
+  = Token { tokLine  :: {-# UNPACK #-} !Int
+          , tokCol   :: {-# UNPACK #-} !Int
+          , tokSOff  :: {-# UNPACK #-} !Int
+          , tokOff   :: {-# UNPACK #-} !Int
+          , tokClass :: !TokenClass
+          }
+  deriving (Eq, Show, Ord)
+
+data LexError
+  = LexError { leChar :: {-# UNPACK #-} !Char
+             , leLine :: {-# UNPACK #-} !Int
+             , leCol  :: {-# UNPACK #-} !Int
+             }
+  | EOFInComment { leLine :: {-# UNPACK #-} !Int
+                 , leCol :: {-# UNPACK #-} !Int
+                 }
+  deriving (Eq, Show, Ord)
+
+lexString :: String -> Either LexError [Token]
+lexString = go 0 0 0 where
+  go :: Int -> Int -> Int -> String -> Either LexError [Token]
+  go !off !line !_   ('\n':xs) =
+    go (off + 1) (line + 1) 0 xs
+
+  go !off !line !col (' ':xs) =
+    go (off + 1) line (col + 1) xs
+
+  go !off !line !_ ('-':'-':xs) =
+    let (a, b) = span (/= '\n') xs
+     in go (off + length a) line 0 b
+  
+  go !off !line !col ('{':'-':xs) = skipComment off line col 1 xs
+
+  go !off !line !col ('(':cs) =
+    Token line col off (off + 1) Tok_oparen `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col (')':cs) =
+    Token line col off (off + 1) Tok_cparen `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('{':cs) =
+    Token line col off (off + 1) Tok_obrace `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('}':cs) =
+    Token line col off (off + 1) Tok_cbrace `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col (':':cs) =
+    Token line col off (off + 1) Tok_colon `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col (';':cs) =
+    Token line col off (off + 1) Tok_semi `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('⊤':cs) =
+    Token line col off (off + 1) Tok_top `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('≡':cs) =
+    Token line col off (off + 1) Tok_equiv `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('=':'=':cs) =
+    Token line col off (off + 2) Tok_equiv `yield` go (off + 2) line (col + 2) cs
+
+  go !off !line !col ('=':cs) =
+    Token line col off (off + 1) Tok_equal `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('→':cs) =
+    Token line col off (off + 1) Tok_arrow `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col (',':cs) =
+    Token line col off (off + 1) Tok_comma `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('_':cs) =
+    Token line col off (off + 1) Tok_under `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('*':cs) =
+    Token line col off (off + 1) Tok_times `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('×':cs) =
+    Token line col off (off + 1) Tok_times `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('\\':cs) =
+    Token line col off (off + 1) Tok_lambda `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('λ':cs) =
+    Token line col off (off + 1) Tok_lambda `yield` go (off + 1) line (col + 1) cs
+
+  go !off !line !col ('-':'>':cs) =
+    Token line col off (off + 2) Tok_arrow `yield` go (off + 2) line (col + 2) cs
+
+  go !off !line !col ('.':'1':cs) =
+    Token line col off (off + 2) Tok_proj1 `yield` go (off + 2) line (col + 2) cs
+
+  go !off !line !col ('.':'2':cs) =
+    Token line col off (off + 2) Tok_proj2 `yield` go (off + 2) line (col + 2) cs
+
+  go !off !line !col (c:cs)
+    | isAlpha c = goIdent off off line col (T.singleton c) cs
+
+  go !_ !line !col (c:_) = Left (LexError c line col)
+
+  go _ _ _ [] = pure []
+
+  goIdent !soff !off !line !col !acc [] =
+    pure [Token line col soff off (finishIdent acc)]
+
+  goIdent !soff !off !line !col !acc (c:cs)
+    | isAlphaNum c || c == '\''
+    = goIdent soff (off + 1) line (col + 1) (T.snoc acc c) cs
+    | otherwise
+    = Token line col soff off (finishIdent acc) `yield` go (off + 1) line (col + 1) (c:cs)
+
+  skipComment off line col level ('-':'}':cs)
+    | level == 1 = go off line col cs
+    | otherwise = skipComment off line col (level - 1) cs
+  skipComment off line col level ('{':'-':cs) =
+    skipComment off line col (level + 1) cs
+  skipComment _ line col _ [] = Left (EOFInComment line col)
+
+  yield c = fmap (c:)
+
+  finishIdent c
+    | T.pack "let" == c   = Tok_let
+    | T.pack "Type" == c  = Tok_type
+    | T.pack "in" == c    = Tok_in
+    | T.pack "refl" == c  = Tok_refl
+    | T.pack "coe" == c   = Tok_coe
+    | T.pack "cong" == c  = Tok_cong
+    | T.pack "sym" == c   = Tok_sym
+    | otherwise           = Tok_var c

src/Presyntax/Parser.hs

@@ -0,0 +1,219 @@
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DerivingVia #-}
+module Presyntax.Parser where
+
+import Control.Applicative
+import Control.Monad.State
+
+import qualified Data.Text as T
+import Data.Text (Text)
+
+import Presyntax.Lexer
+import Presyntax
+
+import Syntax
+
+
+data ParseError
+  = UnexpectedEof Int Int
+  | Unexpected Token
+  | Empty
+  | AltError ParseError ParseError
+  deriving (Show)
+
+data ParseState
+  = ParseState { ptTs   :: [Token]
+               , ptLine :: !Int
+               , ptCol  :: !Int
+               }
+
+newtype Parser a =
+  Parser { runParser :: ParseState -> Either ParseError (a, ParseState) }
+  deriving
+    ( Functor
+    , Applicative
+    , Monad
+    , MonadState ParseState
+    )
+  via (StateT ParseState (Either ParseError))
+
+parseString :: Parser a -> String -> Either (Either LexError ParseError) a
+parseString (Parser k) s =
+  case lexString s of
+    Left e -> Left (Left e)
+    Right xs ->
+      case k (ParseState xs 0 0) of
+        Left e -> Left (pure e)
+        Right (x, _) -> Right x
+
+selectToken :: (Token -> Maybe a) -> Parser a
+selectToken k = Parser \case
+  ParseState [] l c -> Left (UnexpectedEof l c)
+  ParseState (x:xs) _ _ ->
+    case k x of
+      Just p -> pure (p, ParseState xs (tokLine x) (tokCol x))
+      Nothing -> Left (Unexpected x)
+
+expect :: TokenClass -> Parser ()
+expect t = selectToken (\x -> if tokClass x == t then Just () else Nothing)
+
+var :: Parser Text
+var = selectToken \case
+  Token _ _ _ _ (Tok_var v) -> pure v
+  _ -> Nothing
+
+optionally :: Parser a -> Parser (Maybe a)
+optionally p = fmap Just p <|> pure Nothing
+
+braces :: Parser a -> Parser a
+braces k = do
+  expect Tok_obrace
+  x <- k
+  expect Tok_cbrace
+  pure x
+
+parens :: Parser a -> Parser a
+parens k = do
+  expect Tok_oparen
+  x <- k
+  expect Tok_cparen
+  pure x
+
+instance Alternative Parser where
+  empty = Parser \_ -> Left Empty
+  Parser kx <|> Parser ky = Parser \x ->
+    case kx x of
+      Right x -> Right x
+      Left e  ->
+        case ky x of
+          Left _ -> Left e
+          Right y -> Right y
+
+attachPos :: Parser RawExpr -> Parser RawExpr
+attachPos k = do
+  start <- gets (\(ParseState ~(x:_) _ _) -> (tokLine x, tokCol x - (tokOff x - tokSOff x)))
+  x <- k
+  end <- gets (\(ParseState _ l c) -> (l, c))
+  pure (RSrcPos start end x)
+
+body :: Parser RawExpr
+body = attachPos letExpr <|> attachPos lamExpr <|> attachPos exprPi where
+  letExpr = do
+    expect Tok_let
+    n <- var
+    expect Tok_colon
+    t <- body
+    letSmol n t <|> letBig n t
+
+  letSmol n t = do
+    expect Tok_equal
+    d <- body
+    expect Tok_semi
+    Rlet n t d <$> body
+
+  letBig n t = do
+    expect Tok_semi
+    selectToken \case
+      Token _ _ _ _ (Tok_var n') | n' == n -> Just ()
+      _ -> Nothing
+    args <- many arg
+    expect Tok_equal
+    d <- body
+    expect Tok_semi
+    Rlet n t (foldr lam d args) <$> body
+
+  lamExpr = do
+    expect Tok_lambda
+    vs <- some arg
+    expect Tok_arrow
+    e <- body
+    pure (foldr lam e vs)
+
+  arg = fmap (Ex,) var <|> fmap (Im,) (braces var)
+
+  lam (p, v) b = Rlam p v b
+
+exprPi :: Parser RawExpr
+exprPi = attachPos $
+  do
+    bs <- optionally binder
+    case bs of
+      Just k -> foldl (.) id k <$> attachPos exprPi
+      Nothing -> attachPos exprArr
+  where
+    binder = (some (parens (bind Ex) <|> braces (bind Im)) <* expect Tok_arrow)
+         <|> (fmap pure (parens sigma) <* expect Tok_times)
+
+    bind p = do
+      names <- some var
+      expect Tok_colon
+      t <- exprPi
+      pure (foldr (\n k -> Rpi p n t . k) id names)
+
+    sigma = do
+      n <- var
+      expect Tok_colon
+      Rsigma n <$> exprPi
+
+exprArr :: Parser RawExpr
+exprArr = attachPos $ do
+  t <- attachPos exprApp
+  c <- optionally (fmap (const True) (expect Tok_arrow) <|> fmap (const False) (expect Tok_times))
+  case c of
+    Just True -> Rpi Ex (T.singleton '_') t <$> exprPi
+    Just False -> Rsigma (T.singleton '_') t <$> exprPi
+    Nothing -> pure t
+
+exprEq0 :: Parser RawExpr
+exprEq0 = attachPos $
+  do
+    head <- atom
+    spine <- many spineEntry
+    pure (foldl app head spine)
+  where
+    spineEntry = fmap (Ex,) atom <|> fmap (Im,) (braces exprPi)
+    app f (x, s) = Rapp x f s
+
+exprApp :: Parser RawExpr
+exprApp = attachPos $ do
+  t <- exprEq0
+  c <- optionally (expect Tok_equiv)
+  case c of
+    Just () -> Req t <$> exprEq0
+    Nothing -> pure t
+
+atom0 :: Parser RawExpr
+atom0 = attachPos $
+       fmap Rvar var
+   <|> fmap (const Rtype)  (expect Tok_type)
+   <|> fmap (const Rhole)  (expect Tok_under)
+   <|> fmap (const Rtop)   (expect Tok_top)
+   <|> fmap (const Rrefl)  (expect Tok_refl)
+   <|> fmap (const Rcoe)   (expect Tok_coe)
+   <|> fmap (const Rcong)  (expect Tok_cong)
+   <|> fmap (const Rsym)   (expect Tok_sym)
+   <|> fmap (const Runit)  (parens (pure ()))
+   <|> parens pair
+
+pair :: Parser RawExpr
+pair = attachPos $ do
+  t <- body
+  c <- optionally (expect Tok_comma)
+  case c of
+    Just () -> Rpair t <$> pair
+    Nothing -> pure t
+
+atom :: Parser RawExpr
+atom = attachPos $
+  do
+    e <- atom0
+    c <- many (selectToken (projection . tokClass))
+    pure $ case c of
+      []  -> e
+      sls -> foldl (flip ($)) e sls
+  where
+    projection Tok_proj1 = pure Rproj1
+    projection Tok_proj2 = pure Rproj2
+    projection _         = Nothing

src/Syntax.hs

@@ -0,0 +1,62 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PatternSynonyms #-}
+module Syntax where
+
+import Data.Text (Text)
+import Data.Data (Data, Typeable)
+
+data Plicity
+  = Im
+  | Ex
+  deriving (Eq, Show, Ord, Data, Typeable)
+
+newtype Var = Bound Int
+  deriving (Eq, Show, Ord, Data, Typeable)
+
+data BoundDef = BDBound Text | BDDefined Text
+  deriving (Eq, Show, Ord, Data, Typeable)
+
+newtype MetaVar = MV { getMV :: Int }
+  deriving (Eq, Show, Ord, Data, Typeable)
+
+data Term
+  = Var Var
+  | Con Text
+  | Let Text Term Term Term
+  | Type | Prop
+
+  | Pi  Plicity Text Term Term
+  | Lam Plicity Text Term
+  | App Plicity Term Term
+
+  | Sigma Text Term Term
+  | Pair Term Term
+  | Proj1 Term
+  | Proj2 Term
+
+  | Meta    MetaVar
+  | NewMeta MetaVar [BoundDef]
+
+  | Id Term Term Term
+  | Refl
+  | Coe
+  | Cong
+  | Sym
+
+  | Top | Unit
+  deriving (Eq, Show, Ord, Typeable, Data)
+
+pattern Bv :: Int -> Term
+pattern Bv i = Var (Bound i)
+
+data Telescope
+  = End
+  | Ext Telescope Text Term
+  deriving (Eq, Show, Ord)
+
+newtype Level = Lvl {unLvl :: Int}
+  deriving (Eq, Show, Ord, Enum)
+
+lvl2Ix :: Level -> Level -> Int
+lvl2Ix (Lvl l) (Lvl x) = l - x - 1

src/Syntax/Pretty.hs

@@ -0,0 +1,135 @@
+{-# LANGUAGE ViewPatterns #-}
+module Syntax.Pretty where
+
+import Syntax
+import Data.Text ( Text )
+import qualified Data.Text as T
+import Elaboration.Monad
+type Prec = Int
+
+domainPrec, funcPrec, argPrec :: Int
+domainPrec = 3
+argPrec = 2
+funcPrec = 1
+
+showWithPrec :: [Text] -> Int -> Term -> ShowS
+showWithPrec names p (App Ex x y) =
+  showParen (p >= argPrec) $
+      showWithPrec names funcPrec x
+    . showChar ' '
+    . showWithPrec names argPrec y
+
+showWithPrec names p (App Im x _) = showWithPrec names p x
+
+showWithPrec _ _ Type               = showString "Type"
+showWithPrec _ _ Top                = showString "⊤"
+showWithPrec _ _ Unit               = showString "()"
+
+-- Reflexivity
+showWithPrec _ _ Refl               = showString "refl"
+-- Casting
+showWithPrec _ _ Coe                = showString "coe"
+-- Congruence (x == y → f x == f y)
+showWithPrec _ _ Cong               = showString "cong"
+-- Symmetry
+showWithPrec _ _ Sym                = showString "sym"
+
+showWithPrec _ _ (Meta (MV i))      = showChar '?' . shows i
+showWithPrec _ _ (NewMeta (MV i) _) = showChar '?' . shows i
+
+showWithPrec names _ (Bv i)    =
+  if i < 0
+    then showString "α"
+    else showString (T.unpack (names !! i))
+
+showWithPrec names _ (Proj1 x) = showWithPrec names funcPrec x . showString ".1"
+showWithPrec names _ (Proj2 x) = showWithPrec names funcPrec x . showString ".2"
+
+showWithPrec names p (Lam i t e) =
+  showParen (p >= funcPrec) $
+    showChar 'λ'
+      . showsPlicity i id (showString (T.unpack t))
+      . showString " → "
+      . showWithPrec (t:names) 0 e
+
+showWithPrec names p (Pi Ex (T.unpack -> "_") d r) =
+  showParen (p >= argPrec) $
+    showWithPrec names domainPrec d
+    . showString " -> "
+    . showWithPrec (T.singleton '_':names) 0 r
+
+showWithPrec names p (Pi i n d r) =
+  showParen (p >= argPrec) $
+    showsPlicity i (showParen True)
+      ( showString (T.unpack n)
+      . showString " : "
+      . showWithPrec names 0 d
+      )
+    . showString " -> "
+    . showWithPrec (n:names) 0 r
+
+showWithPrec names p (Sigma (T.unpack -> "_") d r) =
+  showParen (p >= argPrec) $
+    showWithPrec names domainPrec d
+    . showString " × "
+    . showWithPrec (T.singleton '_':names) 0 r
+
+showWithPrec names p (Sigma n d r) =
+  showParen (p >= argPrec) $
+    showParen True
+      ( showString (T.unpack n)
+      . showString " : "
+      . showWithPrec names 0 d
+      )
+    . showString " × "
+    . showWithPrec (n:names) 0 r
+
+showWithPrec names _ (Pair a b) =
+  showParen True $
+    showWithPrec names 0 a
+    . showString " , "
+    . showWithPrec names 0 b
+
+showWithPrec names p (Id _ b c) =
+  showParen (p >= funcPrec) $
+    showWithPrec names argPrec b . showString " == " . showWithPrec names argPrec c
+
+showWithPrec names p (Let x t d e) =
+  showParen (p >= funcPrec) $
+    showString "let\n"
+    . showString ("  " ++ T.unpack x)
+    . showString " : "
+    . showWithPrec names 0 t
+    . showChar '\n'
+    . showString ("  " ++ T.unpack x ++ " = ")
+    . showWithPrec names 0 d
+    . showString ";\n"
+    . showWithPrec (x:names) 0 e
+
+showTerm :: Int -> Term -> ShowS
+showTerm = showWithPrec (iterate (`T.snoc` '\'') (T.pack "x"))
+
+showsPlicity :: Plicity -> (ShowS -> ShowS) -> ShowS -> ShowS
+showsPlicity Ex f k = f k
+showsPlicity Im _ k = showChar '{' . k . showChar '}'
+
+showElabError :: ElabError -> ShowS
+showElabError (NotInScope t)  = showString "Variable not in scope: " . shows t
+showElabError (NotFunction names t) =
+  showString "Type is not a function type: "
+    . showWithPrec (names ++ exes) 0 t
+  where
+    exes = iterate (`T.snoc` '\'') (T.pack "x")
+showElabError (NotEqual names a b) =
+  showString "Types are not equal:"
+    . showString "\n  * " . showWithPrec (names ++ exes) 0 a
+    . showString "\n  vs"
+    . showString "\n  * " . showWithPrec (names ++ exes) 0 b
+  where
+    exes = iterate (`T.snoc` '\'') (T.pack "x")
+showElabError (CantSolveMeta ns q t) =
+  showString "Equation has no (unique) solution: "
+    . showString "\n  " . showWithPrec (ns ++ exes) 0 q
+    . showString " ≡? " . showWithPrec (ns ++ exes) 0 t
+  where
+    exes = iterate (`T.snoc` '\'') (T.pack "x")

src/Value.hs

@@ -0,0 +1,124 @@
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE StrictData, PatternSynonyms #-}
+module Value where
+
+import Data.Sequence (Seq)
+import Data.Text (Text)
+
+import Syntax
+import Data.Data
+import qualified Data.Sequence as Seq
+
+newtype Env =
+  Env { locals  :: Seq Value }
+  deriving (Eq, Show, Ord, Data, Typeable)
+
+emptyEnv :: Env
+emptyEnv = Env mempty
+
+type VTy = Value
+
+data Closure
+  = Closure !Env !Term
+  | ClMeta  MetaFun
+  deriving (Eq, Ord, Data, Typeable)
+
+instance Show Closure where
+  showsPrec x (Closure _ t) = showsPrec x t
+  showsPrec x (ClMeta f) = showsPrec x f
+
+newtype MetaFun = MetaFun { runMC :: Value -> Value }
+
+instance Eq MetaFun where
+  _ == _ = False
+
+instance Ord MetaFun where
+  _ <= _ = True
+
+instance Show MetaFun where
+  show _ = "«meta»"
+
+instance Data MetaFun where
+  gunfold _ _ _ = error "gunfold MetaFun"
+  toConstr _ = error "gunfold MetaFun"
+  dataTypeOf _ = mkNoRepType "MetaFun"
+
+data Value
+  -- Universes
+  = VType
+
+  -- Canonical Π-types and λ values
+  | VPi   Plicity Text ~Value {-# UNPACK #-} Closure
+  | VLam  Plicity Text        {-# UNPACK #-} Closure
+  -- Variable applied to some values, with a
+  -- suspended evaluated result that might
+  -- be forced later
+  | VGlued Head (Seq SpineThing) ~(Maybe Value)
+
+  -- Canonical Σ-types and pair values
+  | VSigma Text ~Value {-# UNPACK #-} Closure
+  | VPair  Value Value
+
+  -- Id A a b
+  | VEq Value Value Value
+  -- Id A a b ≡ t
+  | VEqG Value Value Value Value
+
+  | VTop | VUnit
+  deriving (Eq, Show, Ord, Data, Typeable)
+
+data SpineThing
+  = AppEx Value
+  | AppIm Value
+  | SProj1
+  | SProj2
+  deriving (Eq, Show, Ord, Data, Typeable)
+
+flexible :: Value -> Bool
+flexible VGlued{} = True
+flexible VEqG{} = True
+flexible _ = False
+
+pattern VNe :: Head -> Seq SpineThing -> Value
+pattern VNe x y = VGlued x y Nothing
+
+pattern VProj1 :: Value -> Value
+pattern VProj1 t <- (matchP1 -> Just t) where
+  VProj1 t =
+    case t of
+      VGlued h s n -> VGlued h (s Seq.:|> SProj1) n
+
+matchP1 :: Value -> Maybe Value
+matchP1 (VPair x _) = Just x
+matchP1 (VGlued h (s Seq.:|> SProj1) n) = Just (VGlued h s n)
+matchP1 _ = Nothing
+
+pattern VProj2 :: Value -> Value
+pattern VProj2 t <- (matchP2 -> Just t) where
+  VProj2 t =
+    case t of
+      VGlued h s n -> VGlued h (s Seq.:|> SProj2) n
+
+matchP2 :: Value -> Maybe Value
+matchP2 (VPair _ x) = Just x
+matchP2 (VGlued h (s Seq.:|> SProj2) n) = Just (VGlued h s n)
+matchP2 _ = Nothing
+
+data Meta
+  = Unsolved [Text] Value
+  | Solved Value
+  deriving (Eq, Show)
+
+vVar :: Var -> Value
+vVar x = VGlued (HVar x) mempty Nothing
+
+data Head
+  = HVar  Var
+  | HCon  Text
+  | HMeta MetaVar
+  | HRefl
+  | HCoe
+  | HCong
+  | HSym
+  deriving (Eq, Show, Ord, Data, Typeable)

stack.yaml

@@ -0,0 +1,66 @@
+# This file was automatically generated by 'stack init'
+#
+# Some commonly used options have been documented as comments in this file.
+# For advanced use and comprehensive documentation of the format, please see:
+# https://docs.haskellstack.org/en/stable/yaml_configuration/
+
+# Resolver to choose a 'specific' stackage snapshot or a compiler version.
+# A snapshot resolver dictates the compiler version and the set of packages
+# to be used for project dependencies. For example:
+#
+# resolver: lts-3.5
+# resolver: nightly-2015-09-21
+# resolver: ghc-7.10.2
+#
+# The location of a snapshot can be provided as a file or url. Stack assumes
+# a snapshot provided as a file might change, whereas a url resource does not.
+#
+# resolver: ./custom-snapshot.yaml
+# resolver: https://example.com/snapshots/2018-01-01.yaml
+resolver: lts-16.20
+
+# User packages to be built.
+# Various formats can be used as shown in the example below.
+#
+# packages:
+# - some-directory
+# - https://example.com/foo/bar/baz-0.0.2.tar.gz
+#   subdirs:
+#   - auto-update
+#   - wai
+packages:
+- .
+# Dependency packages to be pulled from upstream that are not in the resolver.
+# These entries can reference officially published versions as well as
+# forks / in-progress versions pinned to a git hash. For example:
+#
+# extra-deps:
+# - acme-missiles-0.3
+# - git: https://github.com/commercialhaskell/stack.git
+#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+#
+# extra-deps: []
+
+# Override default flag values for local packages and extra-deps
+# flags: {}
+
+# Extra package databases containing global packages
+# extra-package-dbs: []
+
+# Control whether we use the GHC we find on the path
+# system-ghc: true
+#
+# Require a specific version of stack, using version ranges
+# require-stack-version: -any # Default
+# require-stack-version: ">=2.4"
+#
+# Override the architecture used by stack, especially useful on Windows
+# arch: i386
+# arch: x86_64
+#
+# Extra directories used by stack for building
+# extra-include-dirs: [/path/to/dir]
+# extra-lib-dirs: [/path/to/dir]
+#
+# Allow a newer minor version of GHC than the snapshot specifies
+# compiler-check: newer-minor

stack.yaml.lock

@@ -0,0 +1,12 @@
+# This file was autogenerated by Stack.
+# You should not edit this file by hand.
+# For more information, please see the documentation at:
+#   https://docs.haskellstack.org/en/stable/lock_files
+
+packages: []
+snapshots:
+- completed:
+    size: 532177
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/20.yaml
+    sha256: 0e14ba5603f01e8496e8984fd84b545a012ca723f51a098c6c9d3694e404dc6d
+  original: lts-16.20

test.stt

@@ -0,0 +1,137 @@
+-- Equality with an explicit domain
+let
+  Eq : (A : Type) (x y : A) -> Type;
+  Eq A x y = x == y;
+
+-- Identity function with an explicit domain
+-- (works as a type annotation)
+let
+  the : (A : Type) -> A -> A;
+  the A x = x;
+
+-- Singleton types
+-- The subtype of A generated by "being equal to x : A"
+let
+  singl : (A : Type) (x : A) -> Type;
+  singl A x = (y : A) * x == y;
+
+-- Singletons are contractible
+let
+  singlC : {A : Type} {a b : A} (p : a == b) -> Eq (singl A a) (a, refl) (b, p);
+  singlC p = (p, ());
+
+-- Substitution follows from transport + congruence
+-- (just transport by the congruence under P)
+let
+  subst : {A : Type} (P : A -> Type) {x y : A} (p : x == y) -> P x -> P y;
+  subst P path px = coe (cong P path) px;
+
+let
+  coe2 : {A B : Type} (p : A == B) → A → B;
+  coe2 p = subst (λ x → x) p;
+
+-- Based path induction follows from contractibility of singletons +
+-- substitution
+let
+  J : {A : Type} (a : A) (P : (b : A) -> a == b -> Type)
+           (d : P a refl) (b : A) (p : a == b) -> P b p;
+  J {A} a P d b p =
+    subst {singl A a} (λ y → P y.1 y.2) (singlC p) d;
+
+let
+  JComp : {A : Type} (a : A) (P : (b : A) -> a == b -> Type)
+               (d : P a refl)
+             → J {A} a P d a refl == d;
+  JComp {A} a P d = refl;
+
+-- Symmetry follows from axiom J
+let
+  symm : {A : Type} {x y : A} (p : x == y) -> y == x;
+  symm {A} {x} {y} p = J x (λ y p -> y == x) refl y p;
+
+let
+  symIsRefl : {A : Type} {a : A} → symm (refl {A} {a}) == refl {A} {a};
+  symIsRefl = refl;
+
+let
+  isContr : Type -> Type;
+  isContr A = (x : A) * (y : A) -> y == x;
+
+let
+  comp : {A : Type} {a b c : A} → a == b → b == c → a == c;
+  comp {A} {a} p q = subst (λ x → a == x) q (subst (λ x → a == x) p (refl {A} {a}));
+
+let
+  trans : {A : Type} {a b c : A} → b == c → a == b → a == c;
+  trans {A} {a} p q = comp q p;
+
+let
+  transSym : {A : Type} {a : A} → (p : a == a) → comp p (symm p) == refl;
+  transSym p = refl;
+
+let
+  existsOne : (A : Type) (B : A -> Type) -> ((x : A) × B x) -> isContr A -> (x : A) -> B x;
+  existsOne A B prf contr it =
+    subst B (comp (contr.2 prf.1) (sym (contr.2 it))) prf.2;
+
+let
+  indOne : (P : ⊤ -> Type) -> P () -> (x : ⊤) -> P x;
+  indOne P p x = subst P () p;
+
+let
+  false : Type;
+  false = (A : Type) → A;
+
+let
+  exFalso : (P : Type) -> false -> P;
+  exFalso P f = f P;
+
+let
+  funExt : {A : Type} {B : A -> Type} {f g : (x : A) -> B x}
+        -> ((x : A) -> f x == g x) -> f == g;
+  funExt p = p;
+
+let
+  hfunext : {A : Type} {B : A -> Type} {f g : (x : A) -> B x}
+        -> ((x : A) -> f x == g x) == (f == g);
+  hfunext = refl;
+
+let
+  allAbsurd : {A : Type} (f g : false -> A) -> f == g;
+  allAbsurd f g x = exFalso (f x == g x) x;
+
+let
+  coerceR1 : {A : Type}
+           → Eq (A == A → A → A)
+                (λ p x → coe {A} {A} p x)
+                (λ x y → y);
+  coerceR1 = refl;
+
+let
+  K : {A : Type} {x : A} (P : x == x → Type)
+    → P refl → (p : x == x) → P p;
+  K P p path = subst P (the (refl == path) ()) p;
+
+let
+  foo : {A : Type} {B : A -> Type} {f : (x : A) -> B x}
+         -> Eq (f == f) refl (λ x → refl);
+  foo = K (λ e → (refl {_} {f}) == e) refl (λ x → refl);
+
+let
+  coh : {A : Type} (p : A == A) (x : A) → coe p == (λ x → x);
+  coh path elem x = refl;
+
+let
+  coh2 : {A : Type} (p : A == A) (x : A) → coe p x == x;
+  coh2 path elem = K (λ path → coe {A} {A} path elem == elem) refl path;
+
+-- let
+--   cohsAgree : {A : Type} (p : A == A) (x : A) → coh {A} p x == coh2 {A} p x;
+--   cohsAgree path elem = refl;
+
+let
+  congComp : {A B : Type} (f : A -> B) {x : A}
+          -> cong f (refl {A} {x}) == refl {B} {f x};
+  congComp f = refl;
+
+coe

test2.stt

@@ -0,0 +1,25 @@
+let
+  congComp : {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x == y)
+          -> cong (λ a → g (f a)) p == cong g (cong f p);
+  congComp f g p = refl;
+
+let
+  the : (A : Type) -> A -> A;
+  the A x = x;
+
+let
+  congId : {A : Type} {x y : A} (p : x == y)
+        -> cong (λ x → x) p == p;
+  congId p = ();
+
+let
+  axUIP : {A : Type} {x y : A} (p q : x == y)
+       -> p == q;
+  axUIP p q = ();
+
+let
+  symSym : {A : Type} {x y : A} (p : x == y)
+         -> sym (sym p) == p;
+  symSym p = refl;
+
+congComp

test3.stt

@@ -0,0 +1,6 @@
+let
+  congComp : {A B : Type} (f : A -> B) {x : A}
+          -> cong f (refl {A} {x}) == refl {B} {f x};
+  congComp f = refl;
+  
+congComp