Sit 0.2017.5.1 → 0.2017.5.2
raw patch · 5 files changed
+2/−125 lines, 5 files
Files
- Sit.cabal +1/−5
- src/Evaluation.hs +1/−6
- src/Internal.hs +0/−9
- src/Substitute.hs +0/−73
- src/TypeChecker.hs +0/−32
Sit.cabal view
@@ -1,5 +1,5 @@ name: Sit-version: 0.2017.05.01+version: 0.2017.05.02 build-type: Simple cabal-version: >= 1.8 license: OtherLicense@@ -45,10 +45,6 @@ containers >= 0.3 && < 1.0, data-lens-light >= 0.1.2.2 && < 0.2, mtl >= 2.2.1 && < 3.0---- -- The lexer and parser are shipped as .hs files, thus, no tools necessary.--- build-tools: happy >= 1.15 && < 2,--- alex >= 3.0 && < 4 extensions: MultiParamTypeClasses FunctionalDependencies
src/Evaluation.hs view
@@ -3,7 +3,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}--- {-# LANGUAGE FunctionalDependencies, UndecidableInstances #-} -- | Values and weak head evaluation @@ -47,13 +46,10 @@ | VSuc VSize Val | VInfty | VPi (Dom VType) VClos- -- Functions | -- | Lambda abstraction VLam VClos | -- | @\ x -> x e@ for internal use in fix. VElimBy VElim- -- -- | -- | Constant function- -- -- VConst Val | -- | Neutrals. VUp VType VNe | -- | Type annotation for readback (normal form).@@ -191,7 +187,6 @@ Zero a -> VZero <$> eval (unArg a) Suc a t -> liftA2 VSuc (eval $ unArg a) (eval t) Pi u t -> liftA2 VPi (eval u) (eval t)- -- Lam ai (NoAbs x t) -> VConst <$> eval t Lam ai t -> VLam <$> eval t Var x -> eval x Def f -> lift $ getDef f@@ -222,7 +217,7 @@ (_ , Apply u ) -> apply v u (VZero _ , Case _ u _ _) -> return u (VSuc _ n , Case _ _ _ f) -> apply f $ defaultArg n- (VZero a , Fix t tf f ) -> unfoldFix t tf f a v -- apply f $ e : map (Apply . defaultArg) [ v , VZero ]+ (VZero a , Fix t tf f ) -> unfoldFix t tf f a v (VSuc a n , Fix t tf f ) -> unfoldFix t tf f a v (VUp (VNat a) n , _) -> elimNeNat a n e _ -> __IMPOSSIBLE__
src/Internal.hs view
@@ -128,15 +128,6 @@ suc :: Size -> Term -> Term suc = Suc . Arg Irrelevant --- var :: Index -> Term--- var i = Var i []---- app :: Term -> Arg Term -> Maybe Term--- app t u = case t of--- Var x es -> Just $ Var x $ es ++ [ Apply u ]--- Def f es -> Just $ Def f $ es ++ [ Apply u ]--- _ -> Nothing- defaultArg :: a -> Arg a defaultArg = Arg Relevant
src/Substitute.hs view
@@ -111,79 +111,6 @@ raise :: Substitute a => Int -> a -> a raise n = subst (wkS n) -{- TODO!?---- | Application--class Substitute a => Apply a where- applyE :: a -> Elims -> a- applyE t [] = t- applyE t es = substApply t idS es-- substApply :: a -> Subst -> Elims -> a- substApply t s es = subst s t `applyE` es--instance Apply a => Apply [a] where- applyE ts es = map (`applyE` es) ts- substApply ts s es = map (\ t -> substApply t s es) ts--instance Apply a => Apply (Dom a) where- applyE ts es = fmap (`applyE` es) ts- substApply ts s es = fmap (\ t -> substApply t s es) ts--instance Apply a => Apply (Arg a) where- applyE ts es = fmap (`applyE` es) ts- substApply ts s es = fmap (\ t -> substApply t s es) ts--instance Apply a => Apply (Elim' a) where- applyE ts es = fmap (`applyE` es) ts- substApply ts s es = fmap (\ t -> substApply t s es) ts--instance Apply Term where- substApply t s es = case t of- -- Eliminations- Var i -> lookupS s i `applyE` es- Def f -> foldl App (Def f) es- App t u -> substApply t s $ Apply (subst s u) : es- -- Eliminateables-- -- Types & non-eliminateables- Type l- | null es -> Type $ subst s l- | otherwise -> __IMPOSSIBLE__- Size- | null es -> Size- | otherwise -> __IMPOSSIBLE__- Nat a- | null es -> Nat $ subst s a- | otherwise -> __IMPOSSIBLE__- Zero- | null es -> Zero- | otherwise -> __IMPOSSIBLE__- Suc t- | null es -> Suc $ subst s t- | otherwise -> __IMPOSSIBLE__- Infty- | null es -> Infty- | otherwise -> __IMPOSSIBLE__- Pi u t- | null es -> Pi (subst s u) $ subst s t- | otherwise -> __IMPOSSIBLE__--instance Apply (Abs Term) where-- substApply (Abs x t) s = \case- (Apply (Arg _ u) : es) -> substApply t (consS u s) es- _ -> __IMPOSSIBLE__-- substApply (NoAbs x t) s = \case- (Apply _ : es) -> substApply t s es- _ -> __IMPOSSIBLE__----}-- -- | Construct the type of the functional for fix. --
src/TypeChecker.hs view
@@ -208,12 +208,6 @@ checkSize :: A.Exp -> Check Size checkSize e = checkExp e VSize--- checkSize = \case--- A.Infty -> return Infty--- A.LZero -> return $ sZero--- A.App A.LSuc e -> sSuc <$> checkSize e--- e@(A.Var x) -> checkExp e VSize--- e -> throwError $ "Not a valid size expression: " ++ printTree e checkLevel :: A.Exp -> Check Level checkLevel = \case@@ -222,10 +216,6 @@ e@(A.Var x) -> checkExp e VSize e -> throwError $ "Not a valid level expression: " ++ printTree e --- maxLevel :: A.Exp -> VLevel -> VLevel -> Check VLevel--- maxLevel e l1 l2 = maybe failure return $ maxSize l1 l2--- where failure = throwError $ "Cannot assign a universe level to type " ++ printTree e- checkExp :: A.Exp -> VType -> Check Term checkExp e0 t = do case e0 of@@ -250,8 +240,6 @@ -- Infer the type of the case expression tt <- reifyType t -- Make sure that b is a successor size- -- let failNotSuc = throwError $ "Splitting Nat is only possible at successor size, when checking " ++ printTree e- -- a <- maybe failNotSuc return $ sizePred b let a = fromMaybe __IMPOSSIBLE__ $ sizePred b ta <- reifySize a tz <- checkExp ez =<< applyClosure cl (VZero a)@@ -270,7 +258,6 @@ e -> do (u, ti) <- inferExp e coerce u ti t- -- e -> nyi $ "checking " ++ printTree e -- | Infers neutrals, natural numbers, types. @@ -323,11 +310,6 @@ u <- checkSize e return (sPlus u k, VSize) - -- (A.Plus x k, _) -> do- -- (u, t) <- inferId x- -- subType t VSize- -- return (sPlus u k, t)- (A.Var A.Under, _) -> throwError "Illegal expression: _" (A.Var (A.Id x), _) -> inferId x @@ -608,11 +590,6 @@ traceM $ "lowerSemi " ++ show k ++ " " ++ show t __IMPOSSIBLE__ --- antitone :: VGen -> VType -> Check Bool--- antitone k t = do--- traceM $ "\nantitone " ++ show k ++ " " ++ show t--- return True- monotone :: VGen -> Bool -> VType -> Check Bool monotone k b t = do debug (if b then "monotone" else "antitone") k t@@ -625,15 +602,6 @@ VType a -> monotoneSize k b a VNat a -> monotoneSize k b a VSize -> return True- -- VInfty -> return True- -- VZero _ -> return True- -- VSuc _ v -> monotone k b v- -- VLam cl -> addContext ("#", VSize) $ do- -- u <- lastVal- -- monotone k b =<< applyClosure cl u- -- VUp _ (VNe k' es)- -- | k == k' -> return b- -- | otherwise -> return True VUp (VType _) _ -> return True _ -> __IMPOSSIBLE__