Last active
February 22, 2022 11:53
-
-
Save cheery/1451f2caa4b14e539be0b243dbad61b1 to your computer and use it in GitHub Desktop.
Dynamic pattern matching attempt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs, FlexibleContexts #-} | |
module SimplyDifficult where | |
-- This thing demonstrates dynamic pattern unification, | |
-- however the examples are too simple to verify that the unifier is | |
-- working correctly. | |
-- There were also a thing or two that were way too hard to implement. | |
-- I've omitted them. | |
import Data.Set as Set (Set, singleton, unions, union, member, isSubsetOf) | |
import qualified Data.Set as Set | |
import Data.Monoid (Any(..), getAny) | |
import Data.List (unionBy) | |
import Data.Function (on) | |
import Data.Foldable (fold) | |
import qualified Data.Map as Map | |
import Data.Map (Map) | |
import Control.Monad.Reader | |
import Control.Monad.State | |
import Control.Monad.Except | |
import Control.Monad.Identity | |
import Control.Monad.Trans.Maybe | |
import Control.Applicative (Alternative, (<|>), empty, optional, many) | |
import Debug.Trace | |
data Trail a = B0 | Trail a :< a | |
deriving (Eq,Show) | |
instance Functor Trail where | |
fmap f B0 = B0 | |
fmap f (xs:<x) = fmap f xs :< f x | |
instance Foldable Trail where | |
foldr f y B0 = y | |
foldr f y (xs:<x) = foldr f (f x y) xs | |
instance Traversable Trail where | |
sequenceA B0 = pure B0 | |
sequenceA (xs:<x) = pure (:<) <*> sequenceA xs <*> x | |
(<.>) :: Trail a -> Trail a -> Trail a | |
a <.> B0 = a | |
a <.> (xs:<x) = (a <.> xs) :< x | |
------------------------------------------------------------ | |
-- Terms | |
------------------------------------------------------------ | |
newtype Bind a = Bind a | |
deriving (Eq,Show) | |
data Term | |
= Rigid RName (Trail (Elim Term)) | |
| Flex Name (Trail (Elim Term)) | |
| Abs (Bind Term) | |
| Pi Term (Bind Term) | |
| Sigma Term (Bind Term) | |
| Pair Term Term | |
| Star | |
deriving (Eq,Show) | |
data Head = Var RName | Meta Name | |
deriving (Eq,Show) | |
data Elim a = App a | Fst | Snd | |
deriving (Eq,Show) | |
data RName | |
= Unquoted Int | |
| Closed Int | |
| Bound Name | |
deriving (Eq,Show,Ord) | |
newtype Name = Name Int | |
deriving (Eq,Show,Ord) | |
type Type = Term | |
instance Functor Elim where | |
fmap f (App a) = App (f a) | |
fmap f Fst = Fst | |
fmap f Snd = Snd | |
instance Foldable Elim where | |
foldMap f (App a) = (f a) | |
foldMap f Fst = mempty | |
foldMap f Snd = mempty | |
------------------------------------------------------------ | |
-- Evaluator | |
------------------------------------------------------------ | |
data Env = Env {context :: Signature, scope :: [Value]} | |
data Value | |
= VFlex Name (Trail (Elim Value)) | |
| VRigid RName (Trail (Elim Value)) | |
| VAbs (Value -> Value) | |
| VPi Value (Value -> Value) | |
| VSigma Value (Value -> Value) | |
| VPair Value Value | |
| VStar | |
extend :: Value -> Env -> Env | |
extend v env = env { scope = v : scope env } | |
bindEval :: Env -> Bind Term -> (Value -> Value) | |
bindEval env (Bind term) x = eval (extend x env) term | |
eval :: Env -> Term -> Value | |
eval env (Rigid h e) = vsp (rigidEval env h) (fmap (fmap (eval env)) e) | |
eval env (Flex m e) = vsp (vmeta (context env) m) (fmap (fmap (eval env)) e) | |
eval env (Abs e) = VAbs (bindEval env e) | |
eval env (Pi a b) = VPi (eval env a) (bindEval env b) | |
eval env (Sigma a b) = VSigma (eval env a) (bindEval env b) | |
eval env (Pair a b) = VPair (eval env a) (eval env b) | |
eval env Star = VStar | |
rigidEval :: Env -> RName -> Value | |
rigidEval env (Closed i) = scope env !! i | |
rigidEval env name = vpar (context env) name | |
vsp :: Value -> Trail (Elim Value) -> Value | |
vsp head (xs:<App arg) = vsp head xs `vapp` arg | |
vsp head (xs:<Fst) = vfst (vsp head xs) | |
vsp head (xs:<Snd) = vsnd (vsp head xs) | |
vsp head B0 = head | |
vapp :: Value -> Value -> Value | |
vapp (VAbs f) v = f v | |
vapp (VFlex i e) v = VFlex i (e:<App v) | |
vapp (VRigid n e) v = VRigid n (e:<App v) | |
vapp _ v = error "runtime type error" | |
vfst :: Value -> Value | |
vfst (VPair a b) = a | |
vfst (VFlex i e) = VFlex i (e:<Fst) | |
vfst (VRigid n e) = VRigid n (e:<Fst) | |
vfst _ = error "runtime type error" | |
vsnd :: Value -> Value | |
vsnd (VPair a b) = b | |
vsnd (VFlex i e) = VFlex i (e:<Snd) | |
vsnd (VRigid n e) = VRigid n (e:<Snd) | |
vsnd _ = error "runtime type error" | |
vmeta :: Signature -> Name -> Value | |
vmeta ctx i = case Map.lookup i ctx of | |
Just (_, DEFN v) -> eval (Env ctx []) v | |
Just (_, HOLE) -> VFlex i B0 | |
Nothing -> VFlex i B0 | |
vpar :: Signature -> RName -> Value | |
-- vpar ctx (Bound i) = case lookup i ctx of | |
-- Just (_, DEFN v) -> v | |
-- Just (_, HOLE) -> VRigid (Bound i) B0 | |
-- Nothing -> VRigid (Bound i) B0 | |
vpar ctx n = VRigid n B0 | |
vunquoted :: Int -> Value | |
vunquoted i = VRigid (Unquoted i) B0 | |
------------------------------------------------------------ | |
-- Binding | |
------------------------------------------------------------ | |
class Binding t where | |
binding :: Int -> (Int -> RName -> RName) -> t -> t | |
instance Binding Term where | |
binding i f (Rigid h e) = Rigid (f i h) (fmap (fmap (binding i f)) e) | |
binding i f (Flex m e) = Flex m (fmap (fmap (binding i f)) e) | |
binding i f (Abs e) = Abs (binding i f e) | |
binding i f (Pi t t') = Pi (binding i f t) (binding i f t') | |
binding i f (Sigma t t') = Sigma (binding i f t) (binding i f t') | |
binding i f (Pair a b) = Pair (binding i f a) (binding i f b) | |
binding i f Star = Star | |
instance Binding t => Binding (Bind t) where | |
binding i f (Bind t) = Bind (binding (i+1) f t) | |
bind :: Binding t => Name -> t -> Bind t | |
bind k v = Bind (binding 0 help v) | |
where help :: Int -> RName -> RName | |
help i (Bound k') | (k == k') = (Closed i) | |
--help i (Meta k') | (k == k') = Var (Closed i) | |
help i head = head | |
unbind :: Binding t => Name -> Bind t -> t | |
unbind name (Bind v) = binding 0 help v | |
where help :: Int -> RName -> RName | |
help i (Closed j) | (i == j) = (Bound name) | |
help i head = head | |
loosen :: Binding t => t -> t | |
loosen v = binding 0 help v | |
where help :: Int -> RName -> RName | |
help i (Closed j) | (i <= j) = (Closed (j+1)) | |
help i head = head | |
tighten :: Binding t => Int -> t -> t | |
tighten k v = binding k help v | |
where help :: Int -> RName -> RName | |
help i (Closed j) | (i < j) = (Closed (j-1)) | |
help i (Closed j) | (i == j) = error "bug, did you use fv?" | |
help i head = head | |
tighten' :: Binding t => Trail Int -> t -> t | |
tighten' ts v = binding 0 help v | |
where help :: Int -> RName -> RName | |
help i (Closed j) | (i <= j) = Closed (j - sum (take' (j-i) ts)) | |
help i head = head | |
take' :: Int -> Trail a -> [a] | |
take' n B0 = [] | |
take' 0 (xs:<x) = [] | |
take' n (xs:<x) = x : take' (n-1) xs | |
raise v k = binding 0 help v | |
where help :: Int -> RName -> RName | |
help i (Closed j) | (i <= j) = (Closed (j+k)) | |
help i head = head | |
-- This alone should be sufficient for flowing values inside metavars. | |
remap :: Term -> Trail Term -> Term | |
remap t xs = abss (binding 0 help t) xs | |
where help :: Int -> RName -> RName | |
help i (Closed j) | (i <= j) = Closed (locate xs (j-i) 0+i) | |
help i head = head | |
abss :: Term -> Trail Term -> Term | |
abss term B0 = term | |
abss term (xs:<_) = abss (Abs (Bind term)) xs | |
locate :: Trail Term -> Int -> Int -> Int | |
locate B0 _ _ = error "should have been there" | |
locate (xs:<Rigid (Closed j) B0) i n | (i == j) = n | |
locate (xs:<x) i n = locate xs i (n+1) | |
-- subst :: Binding t => Head -> Bind t -> t | |
-- subst head (Bind v) = binding 0 help v | |
-- where help :: Int -> Head -> Head | |
-- help i (Var (Closed j)) | (i == j) = head | |
-- help i head = head | |
-- ------------------------------------------------------------ | |
-- -- Value forcing | |
-- ------------------------------------------------------------ | |
-- force :: Subs -> Value -> Value | |
-- force ctx (VFlex m sp) = case lookup ( m) ctx of | |
-- Just v -> vsp v sp | |
-- Nothing -> VFlex m sp | |
-- force ctx v = v | |
------------------------------------------------------------ | |
-- Quotation | |
------------------------------------------------------------ | |
quote0 :: Value -> Term | |
quote0 = quote 0 | |
quote :: Int -> Value -> Term | |
quote i (VFlex j e) = Flex j (fmap (fmap (quote i)) e) | |
quote i (VRigid h e) = Rigid (varpar i h) (fmap (fmap (quote i)) e) | |
quote i (VAbs f) = Abs (bindQuote i f) | |
quote i (VPi a f) = Pi (quote i a) (bindQuote i f) | |
quote i (VSigma a f) = Sigma (quote i a) (bindQuote i f) | |
quote i (VPair a b) = Pair (quote i a) (quote i b) | |
quote i VStar = Star | |
bindQuote i f = Bind (quote (i+1) (f (vunquoted i))) | |
varpar :: Int -> RName -> RName | |
varpar i (Unquoted k) = Closed (i - k - 1) | |
varpar i x = x | |
ctxToScope :: Ctx -> [Value] | |
ctxToScope ctx = snd (help ctx) | |
where help :: Ctx -> (Int, [Value]) | |
help B0 = (0, []) | |
help (xs:<x) = let (n, ys) = help xs | |
in (n+1, vunquoted n : ys) | |
class Nf a where | |
nf :: Env -> a -> a | |
instance Nf Term where | |
nf env t = quote (length (scope env)) (eval env t) | |
instance Nf a => Nf (Bind a) where | |
nf env (Bind a) = Bind (nf (extend (vunquoted (length (scope env))) env) a) | |
instance Nf a => Nf [a] where | |
nf env xs = fmap (nf env) xs | |
-- Some weirdness | |
-- bonk :: Env | |
-- bonk = Env Map.empty [] | |
-- | |
-- ($$) :: Term -> Term -> Term | |
-- f $$ a = quote0 $ vapp (eval bonk f) (eval bonk a) | |
-- | |
-- hd :: Term -> Term | |
-- hd a = quote0 $ vfst (eval bonk a) | |
-- | |
-- tl :: Term -> Term | |
-- tl a = quote0 $ vsnd (eval bonk a) | |
inst :: Env -> Bind Term -> Term -> Term | |
inst env a b = quote (length (scope env)) $ | |
vapp (eval env (Abs a)) (eval env b) | |
-- | |
-- (%%) :: Term -> Elim Term -> Term | |
-- t %% e = quote0 $ vsp (eval bonk t) (B0:<(fmap (eval bonk) e)) | |
-- Rather than definining functions to determine the free metavariables | |
-- and variables of terms directly, I use a typeclass to make them | |
-- available on the whole syntax. | |
data Flavour = Vars | RigVars | Metas | |
class Occurs t where | |
free :: Flavour -> t -> Set Name | |
fvs, fvrigs :: Occurs t => t -> Set Name | |
fvs = free Vars | |
fvrigs = free RigVars | |
fmvs :: Occurs t => t -> Set Name | |
fmvs = free Metas | |
instance Occurs Term where | |
free RigVars (Rigid (Bound x) e) = singleton x `union` free RigVars e | |
free RigVars (Flex i _) = Set.empty | |
free Vars (Flex _ e) = free Vars e | |
--free RigVars (Flex _ e) = free RigVars e | |
free Metas (Flex alpha e) = singleton alpha `union` free Metas e | |
free Vars (Rigid (Bound x) e) = singleton x `union` free Vars e | |
--free RigVars (Rigid (Bound x) e) = singleton x `union` free RigVars e | |
free Metas (Rigid (Bound _) e) = Set.empty `union` free Metas e | |
free l (Rigid _ e) = Set.empty `union` free l e | |
free l (Abs b) = free l b | |
free l (Pi s t) = free l s `union` free l t | |
free l (Sigma s t) = free l s `union` free l t | |
free l (Pair s t) = free l s `union` free l t | |
free l Star = Set.empty | |
instance (Occurs t, Occurs u, Occurs v) => Occurs (t,u,v) where | |
free l (a,b,c) = unions [free l a, free l b, free l c] | |
instance Occurs t => Occurs [t] where | |
free l = unions . map (free l) | |
instance Occurs t => Occurs (Trail t) where | |
free l B0 = Set.empty | |
free l (xs :< x) = free l xs `union` free l x | |
instance Occurs t => Occurs (Elim t) where | |
free l (App a) = free l a | |
free l Fst = Set.empty | |
free l Snd = Set.empty | |
instance Occurs a => Occurs (Bind a) where | |
free l (Bind a) = free l a | |
class Fv a where | |
fv :: a -> Set Int | |
fvr :: a -> Set Int | |
instance Fv Term where | |
fv (Rigid h e) = fv h `union` fv e | |
fv (Flex _ e) = fv e | |
fv (Abs b) = fv b | |
fv (Pi s t) = fv s `union` fv t | |
fv (Sigma s t) = fv s `union` fv t | |
fv (Pair s t) = fv s `union` fv t | |
fv Star = Set.empty | |
fvr (Rigid h e) = fvr h `union` fvr e | |
fvr (Flex _ e) = Set.empty | |
fvr (Abs b) = fvr b | |
fvr (Pi s t) = fvr s `union` fvr t | |
fvr (Sigma s t) = fvr s `union` fvr t | |
fvr (Pair s t) = fvr s `union` fvr t | |
fvr Star = Set.empty | |
instance Fv RName where | |
fv (Closed i) = singleton i | |
fv _ = Set.empty | |
fvr (Closed i) = singleton i | |
fvr _ = Set.empty | |
instance Fv a => Fv (Trail a) where | |
fv B0 = Set.empty | |
fv (xs:<x) = fv xs `union` fv x | |
fvr B0 = Set.empty | |
fvr (xs:<x) = fvr xs `union` fvr x | |
instance Fv a => Fv (Elim a) where | |
fv (App a) = fv a | |
fv Fst = Set.empty | |
fv Snd = Set.empty | |
fvr (App a) = fvr a | |
fvr Fst = Set.empty | |
fvr Snd = Set.empty | |
instance Fv a => Fv (Bind a) where | |
fv (Bind a) = (-1) `Set.delete` Set.map (\x -> x-1) (fv a) | |
fvr (Bind a) = (-1) `Set.delete` Set.map (\x -> x-1) (fvr a) | |
data Decl v = HOLE | DEFN v | |
deriving (Eq, Show) | |
type Entry = (Type, Decl Term) | |
type Signature = Map Name Entry | |
-- Metavariables in the signature | |
--support (xs:<_) = support xs | |
-- I don't have atom decls, for now, but they would go here. | |
-- atomDecls :: Signature -> Set Name | |
-- atomDecls B0 = Set.empty | |
-- atomDecls (xs:<SA name _) = Set.insert name (atomDecls xs) | |
-- atomDecls (xs:<_) = atomDecls xs | |
-- decls :: Signature -> Set Name | |
-- decls xs = support xs `union` atomDecls xs | |
metas :: Occurs t => t -> Set Name | |
metas = fmvs | |
-- atoms :: Occurs t => t -> Set Name | |
-- atoms = fvs -- I'm not certain these are atoms. | |
-- consts :: Occurs t => t -> Set Name | |
-- consts t = metas t `union` atoms t | |
type Ctx = Trail Type | |
data Constraint = C Ctx Ctx Term Term Type Type | |
deriving (Eq,Show) | |
data Solver = Solver { | |
signature :: Signature, | |
constraints :: [(Status, Constraint)], | |
nextVar :: Int } | |
deriving (Eq,Show) | |
emptySolver :: Int -> Solver | |
emptySolver = Solver (Map.empty) [] | |
data Status = Active | Blocked | |
deriving (Eq,Show) | |
type Context a | |
= ReaderT Ctx (StateT Solver (ExceptT String Identity)) a | |
fresh :: MonadState Solver m => m Name | |
fresh = do | |
n <- Name <$> gets nextVar | |
modify (\ctx -> ctx { nextVar = nextVar ctx + 1 }) | |
pure n | |
support :: MonadState Solver m => m (Set Name) | |
support = help <$> gets signature | |
where help :: Signature -> Set Name | |
help sig = Set.fromList (Map.keys sig) | |
runContext :: Ctx -> Solver -> Context a -> Either String (a, Solver) | |
runContext ctx solver m = | |
runIdentity (runExceptT (runStateT (runReaderT m ctx) solver)) | |
index :: Trail a -> Int -> a | |
index B0 i = error "overshoot" | |
index (xs:<x) 0 = x | |
index (xs:<x) n = index xs (n-1) | |
eq :: (MonadState Solver m, MonadReader Ctx m) => Term -> Type | |
-> Term -> Type -> m () | |
eq s _S t _T = do | |
ctx <- ask | |
let c = C ctx ctx s t _S _T | |
modify (\ctx -> ctx { constraints = (Active, c) : constraints ctx }) | |
let c' = C ctx ctx _S _T Star Star | |
modify (\ctx -> ctx { constraints = (Active, c') : constraints ctx }) | |
lookupVar :: (MonadState Solver m) => Ctx -> RName -> m Type | |
lookupVar ctx (Closed i) = pure (raise (ctx `index` i) (i+1)) | |
addSignature :: (MonadState Solver m) => Name -> Entry -> m () | |
addSignature name se = modify (\sol -> sol { signature = Map.insert name se (signature sol) }) | |
expand :: (MonadReader Ctx m) => Type -> m a -> m a | |
expand ty m = local (:<ty) m | |
elaborate :: Term -> Type -> Context Term | |
elaborate t ty = do | |
a0 <- fresh | |
ctx <- ask | |
addSignature a0 (fromTelescope ctx ty, HOLE) | |
let u = Flex a0 (vector 0 ctx) | |
case t of | |
Rigid name elim -> do | |
(f, elim, ty') <- inferRName name >>= inferElims elim | |
eq u ty (f elim) ty' | |
Flex alpha elim -> do | |
(f, elim, ty') <- inferMeta alpha >>= inferElims elim | |
eq u ty (f elim) ty' | |
Abs (Bind body) -> do | |
y1 <- fresh | |
y2 <- fresh | |
let _Y1 = (Flex y1 (vector 0 ctx)) | |
let _Y2 = (Flex y2 (vector 0 (ctx:<_Y1))) | |
addSignature y1 (fromTelescope ctx Star, HOLE) | |
addSignature y2 (fromTelescope (ctx:<_Y1) Star, HOLE) | |
u' <- expand _Y1 (elaborate body _Y2) | |
eq u ty (Abs (Bind u')) (Pi _Y1 (Bind _Y2)) | |
Pi a (Bind b) -> do | |
s <- elaborate a Star | |
t <- expand s (elaborate b Star) | |
eq u ty (Pi s (Bind t)) Star | |
Sigma a (Bind b) -> do | |
s <- elaborate a Star | |
t <- expand s (elaborate b Star) | |
eq u ty (Sigma s (Bind t)) Star | |
Pair a b -> do | |
y1 <- fresh | |
y2 <- fresh | |
let _Y1 = (Flex y1 (vector 0 ctx)) | |
let _Y2 = (Flex y2 (vector 0 (ctx:<_Y1))) | |
addSignature y1 (fromTelescope ctx Star, HOLE) | |
addSignature y2 (fromTelescope (ctx:<_Y1) Star, HOLE) | |
s <- elaborate a _Y1 | |
t <- elaborate b (Flex y2 (vector 0 ctx:<App s)) | |
eq u ty (Pair s t) (Sigma _Y1 (Bind _Y2)) | |
Star -> eq u Star Star Star | |
pure u | |
type HeadTrail = (Trail (Elim Term) -> Term, Trail (Elim Term), Type) | |
inferRName :: RName -> Context HeadTrail | |
inferRName var = do | |
ctx <- ask | |
ty <- lookupVar ctx var | |
pure (Rigid var, B0, ty) | |
inferMeta :: Name -> Context HeadTrail | |
inferMeta alpha = do | |
isFresh <- (not . member alpha) <$> support | |
if isFresh then do | |
ctx <- ask | |
ty <- fresh | |
let _TY = Flex ty (vector 0 ctx) | |
addSignature ty (fromTelescope ctx Star, HOLE) | |
addSignature alpha (fromTelescope ctx _TY, HOLE) | |
pure (Flex alpha, vector 0 ctx, _TY) | |
else error "unfresh meta" | |
inferElims :: Trail (Elim Term) -> HeadTrail -> Context HeadTrail | |
inferElims B0 ht = pure ht | |
inferElims (xs:<x) ht = inferElims xs ht >>= inferElim x | |
inferElim :: Elim Term -> HeadTrail -> Context HeadTrail | |
inferElim (App x) (f, e, ty) = do | |
ctx <- ask | |
y1 <- fresh | |
y2 <- fresh | |
let _Y1 = (Flex y1 (vector 0 ctx)) | |
let _Y2 = (Flex y2 (vector 0 (ctx:<_Y1))) | |
addSignature y1 (fromTelescope ctx Star, HOLE) | |
addSignature y2 (fromTelescope (ctx:<_Y1) Star, HOLE) | |
u <- elaborate x _Y1 | |
eq ty Star (Pi _Y1 (Bind _Y2)) Star | |
pure (f, e:<App u, Flex y2 (vector 0 ctx:<App u)) | |
inferElim Fst (f, e, ty) = do | |
ctx <- ask | |
y1 <- fresh | |
y2 <- fresh | |
let _Y1 = (Flex y1 (vector 0 ctx)) | |
let _Y2 = (Flex y2 (vector 0 (ctx:<_Y1))) | |
addSignature y1 (fromTelescope ctx Star, HOLE) | |
addSignature y2 (fromTelescope (ctx:<_Y1) Star, HOLE) | |
eq ty Star (Sigma _Y1 (Bind _Y2)) Star | |
pure (f, e:<Fst, _Y1) | |
inferElim Snd (f, e, ty) = do | |
ctx <- ask | |
y1 <- fresh | |
y2 <- fresh | |
let _Y1 = (Flex y1 (vector 0 ctx)) | |
let _Y2 = (Flex y2 (vector 0 (ctx:<_Y1))) | |
addSignature y1 (fromTelescope ctx Star, HOLE) | |
addSignature y2 (fromTelescope (ctx:<_Y1) Star, HOLE) | |
eq ty Star (Sigma _Y1 (Bind _Y2)) Star | |
pure (f, e:<Snd, Flex y2 (vector 0 ctx:<App (f (e:<Fst)))) | |
fromTelescope :: Trail Type -> Type -> Type | |
fromTelescope xs t = foldr (\x y -> Pi x (Bind y)) t xs | |
--fromTelescope B0 t = t | |
--fromTelescope (xs:<x) t = fromTelescope xs (Pi x (Bind t)) | |
telescope :: Type -> (Trail Type, Type) | |
telescope t = telescope' B0 t | |
where telescope' :: Trail Type -> Type -> (Trail Type, Type) | |
telescope' xs (Pi a (Bind b)) = telescope' (xs :< a) b | |
telescope' xs a = (xs, a) | |
vector :: Int -> Trail a -> Trail (Elim Term) | |
vector i B0 = B0 | |
vector i (xs:<x) = vector (i+1) xs :< App (Rigid (Closed i) B0) | |
hole :: Ctx -> Type -> Solving Name | |
hole _Gam _T = do | |
alpha <- fresh | |
sol <- get | |
put sol { signature = Map.insert alpha (fromTelescope _Gam _T, HOLE) | |
(signature sol) } | |
pure alpha | |
define :: Ctx -> Name -> Type -> Term -> Solving () | |
define _Gam alpha _S v = do | |
sol <- get | |
put sol { signature = Map.insert alpha | |
(fromTelescope _Gam _S, DEFN (abss v _Gam)) | |
(signature sol) } | |
normalize :: Signature -> Constraint -> Constraint | |
normalize sig (C ctx ctx' t t' ty ty') = C | |
(nfContext sig ctx) | |
(nfContext sig ctx') | |
(nf (Env sig (ctxToScope ctx)) t) | |
(nf (Env sig (ctxToScope ctx')) t') | |
(nf (Env sig (ctxToScope ctx)) ty) | |
(nf (Env sig (ctxToScope ctx')) ty') | |
nfContext :: Signature -> Ctx -> Ctx | |
nfContext sig B0 = B0 | |
nfContext sig (xs:<x) = let xs' = nfContext sig xs | |
in xs':<nf (Env sig (ctxToScope xs')) x | |
postpone :: Status -> Constraint -> Solving () | |
postpone status constraint = do | |
--trace (show (status, constraint)) $ | |
modify (\sol -> sol { constraints = (status, constraint) : constraints sol }) | |
active :: Constraint -> Solving () | |
active = postpone Active | |
block :: Constraint -> Solving () | |
block = postpone Blocked | |
id_ty :: Term | |
id_ty = Pi Star (Bind (Pi (Rigid (Closed 0) B0) (Bind (Rigid (Closed 1) B0)))) | |
id_term :: Term | |
id_term = Abs (Bind (Abs (Bind (Rigid (Closed 0) B0)))) | |
var :: Int -> Term | |
var i = Rigid (Closed i) B0 | |
ab :: Term -> Term | |
ab t = Abs (Bind t) | |
pi' :: Term -> Term -> Term | |
pi' t u = Pi t (Bind u) | |
const_ty :: Term | |
const_ty = Pi Star (Bind (Pi Star (Bind | |
(Pi (var 1) (Bind (Pi (var 1) (Bind (var 3)))))))) | |
const_term :: Term | |
const_term = Abs (Bind (Abs (Bind (Abs (Bind (Abs (Bind (var 1)))))))) | |
num_ty = pi' Star (pi' (pi' (var 0) (var 1)) (pi' (var 1) (var 2))) | |
zero_term = ab (ab (ab (var 0))) | |
one_term = ab (ab (ab (Rigid (Closed 1) (B0:<App (var 0))))) | |
two_term = ab (ab (ab (Rigid (Closed 1) (B0:<App (Rigid (Closed 1) (B0:<App (var 0))))))) | |
--call_id_term = ab (ab (ab (var 0))) | |
call_id_ty = (pi' id_ty (pi' Star Star)) | |
call_id_term = (ab (ab (var 0))) | |
call_id_term2 = (ab (ab (Rigid (Closed 1) (B0:<App Star:<App (var 0))))) | |
call_id_ty2 = pi' Star (pi' id_ty (pi' (var 1) (var 2))) | |
call_id_term3 = ab (ab (ab (Rigid (Closed 1) (B0:<App (Flex (Name (-1)) B0):<App (var 0))))) | |
--call_id_term = ab (ab (ab (Rigid (Closed 1) (B0:<App (Flex (Name (-1)) B0):<App (var 0))))) | |
runSolver test = do | |
(u, solver) <- runContext B0 (emptySolver 0) test | |
let solver' = solve solver | |
case solver' of | |
(Solver sig [] _) -> Right (nf (Env sig []) u, sig) | |
(Solver sig cons _) -> Left (show (sig, cons)) | |
runTest1Print :: IO () | |
runTest1Print = do | |
case runSolver (elaborate const_ty Star) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (ty, solver) -> do | |
putStrLn ("success: " ++ show ty) | |
-- let result = runContext B0 (emptySolver 0) (elaborate id_term ty) | |
-- putStrLn (show result) | |
case runSolver (elaborate const_term ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
case runSolver (elaborate id_ty Star) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (ty, solver) -> do | |
putStrLn ("success: " ++ show ty) | |
-- let result = runContext B0 (emptySolver 0) (elaborate id_term ty) | |
-- putStrLn (show result) | |
case runSolver (elaborate id_term ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
case runSolver (elaborate num_ty Star) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (ty, solver) -> do | |
putStrLn ("success: " ++ show ty) | |
case runSolver (elaborate zero_term ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
case runSolver (elaborate one_term ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
case runSolver (elaborate two_term ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
case runSolver (elaborate call_id_ty Star) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (ty, solver) -> do | |
putStrLn ("success: " ++ show ty) | |
case runSolver (elaborate call_id_term ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
case runSolver (elaborate call_id_term2 ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
case runSolver (elaborate call_id_ty2 Star) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (ty, solver) -> do | |
putStrLn ("success: " ++ show ty) | |
case runSolver (elaborate call_id_term3 ty) of | |
Left error -> putStrLn ("error: " ++ error) | |
Right (term, solver) -> do | |
putStrLn ("success: " ++ show term) | |
solve :: Solver -> Solver | |
solve solver = case runIdentity (runStateT (runMaybeT solveSteps) solver) of | |
(Nothing, solver') -> solver' | |
(Just (), solver') -> solve solver' | |
type Solving a = MaybeT (StateT Solver Identity) a | |
solveSteps :: Solving () | |
solveSteps = do | |
sol <- get | |
let cons = constraints sol | |
put sol { constraints = [] } | |
progress <- solveConstraints cons | |
guard progress <|> (gets signature >>= lowering . Map.toList >>= guard) | |
-- <|> TODO: unblockConstraints by eta-expanding | |
-- uninstantiated metavariables | |
solveConstraints :: [(Status, Constraint)] -> Solving Bool | |
solveConstraints [] = pure False | |
solveConstraints ((a,x):xs) = do | |
progress <- solveConstraints xs | |
sig <- gets signature | |
let x' = normalize sig x | |
if isActive a || (x' /= x) then do | |
optional (refine x') | |
pure True | |
else do | |
block x | |
pure progress | |
isActive :: Status -> Bool | |
isActive Active = True | |
isActive Blocked = False | |
(<||) :: Monad m => m Bool -> m () -> m () | |
a <|| b = do x <- a | |
unless x b | |
infixr 5 <|| | |
sym :: Constraint -> Constraint | |
sym (C ctx ctx' t t' ty ty') = C ctx' ctx t' t ty' ty | |
refine :: Constraint -> Solving () | |
refine (C ctx1 ctx2 t1 t2 ty1 ty2) | (t1 == t2) = pure () | |
refine (C ctx1 ctx2 t1 t2 ty1 ty2) = do | |
sig <- gets signature | |
--trace ("refine " ++ (show (C ctx1 ctx2 t1 t2 ty1 ty2))) $ | |
-- pure () | |
-- The if case of Definition 2.158 (strongly neutral term) has a | |
-- condition on the number of argumetns which may be fullfilled | |
-- by n-expanding the terms. | |
let t1'' = etaExpandDefHeaded t1 | |
let t2'' = etaExpandDefHeaded t2 | |
case (t1'', t2'') of | |
(Rigid a e1, Rigid b e2) -> do -- by rule schema 14 (strongly neutral term) | |
optional (matchSpine ctx1 a e1 ctx2 b e2) | |
block (C ctx1 ctx2 t1'' t2'' ty1 ty2) | |
(Flex a e1, Flex b e2) | a == b -> do | |
flexFlexSame ctx1 ctx2 a e1 e2 ty1 ty2 | |
(Flex a e1, Flex b e2) -> do | |
let t1''' = etaContractWhnf t1'' | |
let t2''' = etaContractWhnf t2'' | |
let q = (C ctx1 ctx2 t1''' t2''' ty1 ty2) | |
tryPrune q <|| tryPrune (sym q) <|| tryInvert q <|| tryInvert (sym q) <|| block q | |
(Flex a e1, u) -> do | |
let t1''' = etaContractWhnf t1'' | |
let t2''' = etaContractWhnf t2'' | |
let q = (C ctx1 ctx2 t1''' t2''' ty1 ty2) | |
tryPrune q <|| tryInvert q <|| block q | |
(u, Flex b e2) -> do | |
let t1''' = etaContractWhnf t1'' | |
let t2''' = etaContractWhnf t2'' | |
let q = (C ctx2 ctx1 t2''' t1''' ty2 ty1) | |
tryPrune q <|| tryInvert q <|| block q | |
(_, _) -> do | |
(t1''', ty1') <- etaExpand ctx1 t1'' (nf (Env sig (ctxToScope ctx1)) ty1) | |
(t2''', ty2') <- etaExpand ctx2 t2'' (nf (Env sig (ctxToScope ctx2)) ty2) | |
splitDown ctx1 ctx2 t1''' t2''' ty1' ty2' | |
-- by rule schema 11 (λ-abstraction) | |
-- by rule schema 12 (pairs) | |
-- by rule schema 13 (booleans) | |
-- by rule schema 3 (injectivity of ∏) | |
-- by rule schema 4 (injectivity of Σ) | |
-- by rule schema 5 (bool) | |
-- by rule schema 6 set | |
--pure [(Never, C ctx1 ctx2 t1''' t2''' ty1' ty2')] | |
splitDown :: Ctx -> Ctx -> Term -> Term -> Type -> Type -> Solving () | |
splitDown ctx ctx' (Pi a (Bind b)) (Pi a' (Bind b')) Star Star = do | |
let c1 = C ctx ctx' a a' Star Star | |
let c2 = C (ctx:<a) (ctx':<a') b b' Star Star | |
active c1 | |
active c2 | |
splitDown ctx1 ctx2 s t _S _T = block (C ctx1 ctx2 s t _S _T) | |
tryInvert :: Constraint -> Solving Bool | |
tryInvert (C ctx1 ctx2 (Flex alpha e1) t2 ty1 ty2) = do | |
ty <- getType alpha | |
m <- invert alpha ty e1 t2 | |
case m of | |
Nothing -> | |
pure False | |
Just t2' -> do | |
active (C ctx1 ctx2 (Flex alpha e1) t2 ty1 ty2) | |
define B0 alpha ty t2' | |
pure True | |
invert :: Name -> Type -> Trail (Elim Term) -> Term -> Solving (Maybe Term) | |
invert alpha _T e t | alpha `Set.notMember` fmvs t, | |
Just xs <- varList e, | |
fv t `Set.isSubsetOf` fvd xs = do | |
pure (Just (remap t xs)) | |
| otherwise = pure Nothing | |
fvd :: Trail Term -> Set Int | |
fvd B0 = Set.empty | |
fvd (xs:<x) = (fvd xs `Set.difference` fv x) `Set.union` (fv x `Set.difference` fvd xs) | |
getType :: Name -> Solving Type | |
getType name = do | |
sig <- gets signature | |
case Map.lookup name sig of | |
Just (ty,_) -> pure ty | |
Nothing -> error "variable not installed" | |
tryPrune :: Constraint -> Solving Bool | |
tryPrune q@(C _ _ (Flex alpha e) t _ _) = do | |
u <- pruneTerm (fv e) t | |
case u of | |
(d:_) -> | |
--instantiate d | |
--sig <- gets signature | |
--let q' = normalize sig q | |
--trace "pruned" (active q') | |
--pure True | |
active q >> instantiate d >> pure True | |
[] -> pure False | |
pruneTerm :: Set Int -> Term -> Solving [Instantiation] | |
pruneTerm vs (Pi s t) = (++) <$> pruneTerm vs s <*> pruneUnder vs t | |
pruneTerm vs (Sigma s t) = (++) <$> pruneTerm vs s <*> pruneUnder vs t | |
pruneTerm vs (Pair s t) = (++) <$> pruneTerm vs s <*> pruneTerm vs t | |
pruneTerm vs (Abs b) = pruneUnder vs b | |
pruneTerm vs Star = pure [] | |
pruneTerm vs (Rigid r e) = pruneElims vs e | |
pruneTerm vs (Flex beta e) = pruneMeta vs beta e | |
pruneUnder :: Set Int -> Bind Term -> Solving [Instantiation] | |
pruneUnder vs (Bind term) = pruneTerm (Set.insert 0 (Set.map (+1) vs)) term | |
pruneElims :: Set Int -> Trail (Elim Term) -> Solving [Instantiation] | |
pruneElims vs e = fold <$> traverse pruneElim e | |
where pruneElim :: Elim Term -> Solving [Instantiation] | |
pruneElim (App x) = pruneTerm vs x | |
pruneElim Fst = pure [] | |
pruneElim Snd = pure [] | |
pruneMeta :: Set Int -> Name -> Trail (Elim Term) -> Solving [Instantiation] | |
pruneMeta vs alpha e = do | |
(tel, ty) <- telescope <$> getType alpha | |
case pruneVars vs (fv ty) tel e of | |
Just dropList | any (/=0) dropList -> do | |
let ty' = tighten' dropList ty | |
let tel' = tightenCtx dropList tel | |
pure [(alpha, fromTelescope tel' ty', | |
\beta -> abss (Flex beta (revec dropList (vector 0 tel))) tel)] | |
_ -> pure [] | |
tightenCtx :: Trail Int -> Ctx -> Ctx | |
tightenCtx _ B0 = B0 | |
tightenCtx (ts:<_) (xs:<x) = tightenCtx ts xs :< tighten' ts x | |
revec :: Trail Int -> Trail (Elim Term) -> Trail (Elim Term) | |
revec _ B0 = B0 | |
revec (ts:<0) (xs:<x) = revec ts xs :< x | |
revec (ts:<_) (xs:<x) = revec ts xs | |
pruneVars :: Set Int -> Set Int -> Ctx -> Trail (Elim Term) -> Maybe (Trail Int) | |
pruneVars vs ks B0 B0 = Just B0 | |
pruneVars vs ks (xs :< _S) (e :< App s) = | |
if 0 `member` ks | |
then do dropList <- pruneVars vs (Set.map (subtract 1) ks `union` fv _S) xs e | |
Just (dropList :< 0) | |
else case toVar s of | |
Just y | y `member` vs -> do | |
dropList <- pruneVars vs (Set.map (subtract 1) ks `union` fv _S) xs e | |
Just (dropList :< 0) | |
_ | not (fvr s `Set.isSubsetOf` vs) -> do | |
dropList <- pruneVars vs (Set.map (subtract 1) ks) xs e | |
Just (dropList :< 1) | |
| otherwise -> Nothing | |
pruneVars vs ks _ _ = Nothing | |
-- Similar to prune, so it's down here | |
flexFlexSame :: Ctx -> Ctx -> Name | |
-> Trail (Elim Term) -> Trail (Elim Term) | |
-> Type -> Type -> Solving () | |
flexFlexSame ctx ctx' alpha e e' ty ty' = do | |
(tel, _T) <- telescope <$> getType alpha | |
case intersect (fv _T) tel e e' of | |
Just dropList | any (/=0) dropList -> let _T' = tighten' dropList _T | |
tel' = tightenCtx dropList tel | |
in instantiate (alpha, fromTelescope tel' _T', | |
\beta -> abss (Flex beta (revec dropList (vector 0 tel))) tel) | |
_ -> block (C ctx ctx' (Flex alpha e) (Flex alpha e') ty ty') | |
-- Given a telescope and the two evaluation contexts, |intersect| | |
-- checks the evaluation contexts are lists of variables and produces the | |
-- telescope on which they agree. | |
intersect :: Set Int -> Trail Type -> Trail (Elim Term) -> Trail (Elim Term) -> Maybe (Trail Int) | |
intersect ks B0 B0 B0 = pure B0 | |
intersect ks (tel :< _S) (e :< App s) (e' :< App s') = do | |
x <- toVar s | |
y <- toVar s' | |
if x == y then do | |
tel <- intersect (Set.map (subtract 1) ks `union` fv _S) tel e e' | |
pure (tel :< 0) | |
else if 0 `member` ks then empty | |
else do tel <- intersect (Set.map (subtract 1) ks) tel e e' | |
pure (tel :< 1) | |
-- For rigid-rigid interaction. | |
matchSpine :: Ctx -> RName -> Trail (Elim Term) | |
-> Ctx -> RName -> Trail (Elim Term) | |
-> Solving (Type, Type) | |
matchSpine ctx x B0 ctx' x' B0 | |
| x == x' = do | |
a <- lookupVar ctx x | |
b <- lookupVar ctx' x' | |
pure (a, b) | |
| otherwise = empty | |
matchSpine ctx x (e :< App a) ctx' x' (e' :< App a') = do | |
(Pi _A _B, Pi _S _T) <- matchSpine ctx x e ctx' x' e' | |
active $ C ctx ctx' a a' _A _S | |
pure (inst (Env Map.empty (ctxToScope ctx)) _B a, | |
inst (Env Map.empty (ctxToScope ctx')) _T a') | |
matchSpine ctx x (e :< Fst) ctx' x' (e' :< Fst) = do | |
(Sigma _A _B, Sigma _S _T) <- matchSpine ctx x e ctx' x' e' | |
pure (_A, _S) | |
matchSpine ctx x (e :< Snd) ctx' x' (e' :< Snd) = do | |
(Sigma _A _B, Sigma _S _T) <- matchSpine ctx x e ctx' x' e' | |
pure (inst (Env Map.empty (ctxToScope ctx)) _B (Rigid x (e :< Fst)), | |
inst (Env Map.empty (ctxToScope ctx')) _T (Rigid x' (e' :< Fst))) | |
matchSpine _ _ _ _ _ _ = empty | |
lowering :: [(Name, Entry)] -> Solving Bool | |
lowering [] = pure False | |
lowering ((alpha,(ty,HOLE)):xs) = do | |
status <- lowering xs | |
status' <- lower B0 alpha ty | |
pure (status || status') | |
lowering (_:xs) = lowering xs | |
-- Given the name and type of a metavariable, |lower| attempts to | |
-- simplify it by removing $\Sigma$-types, according to the metavariable | |
-- simplification steps \eqref{eqn:miller:metasimp:sigma} and | |
-- \eqref{eqn:miller:metasimp:pi-sigma} in | |
-- Figure~\longref{fig:miller:solve}, as described in | |
-- Subsection~\longref{subsec:miller:spec:metasimp}. | |
lower :: Ctx -> Name -> Type -> Solving Bool | |
lower phi alpha (Sigma _S _T) = do | |
beta <- hole phi _S | |
let betaTerm = Flex beta (vector 0 phi) | |
ceta <- hole phi (inst (Env Map.empty (ctxToScope phi)) _T betaTerm) | |
let cetaTerm = Flex ceta (vector 0 phi) | |
define phi alpha (Sigma _S _T) (Pair betaTerm cetaTerm) | |
pure True | |
lower phi alpha (Pi _S (Bind _T)) = lower (phi :< _S) alpha _T | |
lower _ _ _ = pure False | |
-- > lower :: Telescope -> Nom -> Type -> Contextual Bool | |
-- > lower _Phi alpha (Sig _S _T) = hole _Phi _S $ \ s -> | |
-- > hole _Phi (inst _T s) $ \ t -> | |
-- > define _Phi alpha (Sig _S _T) (PAIR s t) >> | |
-- > return True | |
-- > | |
-- > lower _Phi alpha (Pi _S _T) = do x <- fresh (s2n "x") | |
-- > splitSig B0 x _S >>= maybe | |
-- > (lower (_Phi :< (x, _S)) alpha (inst _T (var x))) | |
-- > (\ (y, _A, z, _B, s, (u, v)) -> | |
-- > hole _Phi (_Pi y _A (_Pi z _B (inst _T s))) $ \ w -> | |
-- > define _Phi alpha (Pi _S _T) (lam x (w $$ u $$ v)) >> | |
-- > return True) | |
-- > | |
-- > lower _Phi alpha _T = return False | |
-- | |
-- Lowering a metavariable needs to split $\Sigma$-types (possibly | |
-- underneath a bunch of parameters) into their components. For example, | |
-- $[[y : Pi x : X . Sigma z : S . T]]$ splits into | |
-- $[[y0 : Pi x : X . S]]$ and $[[y1 : Pi x : X . {y0 x/z} T]]$. Given | |
-- the name of a variable and its type, |splitSig| attempts to split it, | |
-- returning fresh variables for the two components of the $\Sigma$-type, | |
-- an inhabitant of the original type in terms of the new variables and | |
-- inhabitants of the new types by projecting the original variable. | |
-- | |
-- > splitSig :: Telescope -> Nom -> Type -> | |
-- > Contextual (Maybe (Nom, Type, Nom, Type, Tm, (Tm, Tm))) | |
-- > splitSig _Phi x (Sig _S _T) = do y <- fresh (s2n "y") | |
-- > z <- fresh (s2n "z") | |
-- > return $ Just (y, _Pis _Phi _S, z, _Pis _Phi (inst _T (var y $*$ _Phi)), | |
-- > lams' _Phi (PAIR (var y $*$ _Phi) (var z $*$ _Phi)), | |
-- > (lams' _Phi (var x $*$ _Phi %% Hd), | |
-- > lams' _Phi (var x $*$ _Phi %% Tl))) | |
-- > splitSig _Phi x (Pi _A _B) = do a <- fresh (s2n "a") | |
-- > splitSig (_Phi :< (a, _A)) x (inst _B (var a)) | |
-- > splitSig _ _ _ = return Nothing | |
type Instantiation = (Name, Type, Name -> Term) | |
instantiate :: Instantiation -> Solving () | |
instantiate d@(alpha, ty, f) = do | |
beta <- hole B0 ty | |
ty' <- getType alpha | |
define B0 alpha ty' (f beta) | |
tZip :: Trail a -> Trail b -> Trail (a, b) | |
tZip B0 _ = B0 | |
tZip _ B0 = B0 | |
tZip (xs:<x) (ys:<y) = tZip xs ys :< (x, y) | |
size :: Trail a -> Int | |
size B0 = 0 | |
size (xs:<_) = size xs + 1 | |
toVar :: Term -> Maybe Int | |
toVar (Rigid (Closed n) B0) = Just n | |
toVar _ = Nothing | |
varList :: Alternative m => Trail (Elim (Term)) -> m (Trail Term) | |
varList (xs:<App (Flex a B0)) = (:<Flex a B0) <$> varList xs | |
varList (xs:<App (Rigid n B0)) = (:<Rigid n B0) <$> varList xs | |
varList B0 = pure B0 | |
varList _ = empty | |
etaContractWhnf :: Term -> Term | |
etaContractWhnf t = t | |
--etaContractWhnf (Abs (Bind (VRigid head (elems:<App (VRigid (Closed 0) B0))))) | |
-- | not (0 `Set.member` fv (head, elems)) = | |
etaExpand :: Ctx -> Term -> Type -> Solving (Term, Type) | |
etaExpand ctx (Abs x) (Pi a b) = pure (Abs x, Pi a b) | |
etaExpand ctx (Pair x y) (Sigma a b) = pure (Pair x y, Sigma a b) | |
etaExpand ctx f (Pi a b) = pure (Abs (Bind expr), Pi a b) | |
where expr = quote (length scop) $ | |
eval (Env Map.empty scop) (loosen f) `vapp` (vunquoted (length scop)) | |
scop = (ctxToScope ctx) | |
etaExpand ctx p (Sigma a b) = pure (Pair e1 e2, Sigma a b) | |
where e1 = quote (length scop) $ vfst $ eval (Env Map.empty scop) p | |
e2 = quote (length scop) $ vsnd $ eval (Env Map.empty scop) p | |
scop = (ctxToScope ctx) | |
etaExpand ctx p q = pure (p, q) | |
etaExpandDefHeaded :: Term -> Term | |
etaExpandDefHeaded t = t |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment