summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/LambdaCube/Compiler/CoreToIR.hs26
-rw-r--r--src/LambdaCube/Compiler/Infer.hs1067
-rw-r--r--src/LambdaCube/Compiler/Parser.hs139
-rw-r--r--src/LambdaCube/Compiler/Pretty.hs5
-rw-r--r--testdata/Builtins.out2
-rw-r--r--testdata/Prelude.out20
-rw-r--r--testdata/language-features/adt/adt05.out2
-rw-r--r--testdata/record01.reject.out2
-rw-r--r--testdata/typesig.reject.out2
9 files changed, 641 insertions, 624 deletions
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index f2aca2dc..d3858c95 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -862,26 +862,32 @@ toExp = flip runReader [] . flip evalStateT freshTypeVars . f_
862 | otherwise = f__ (e, et) 862 | otherwise = f__ (e, et)
863 f__ (e, et) = case e of 863 f__ (e, et) = case e of
864 I.Var i -> asks $ fst . (!!! i) 864 I.Var i -> asks $ fst . (!!! i)
865 I.Pi b x (I.downE 0 -> Just y) -> Pi b "" <$> f_ (x, I.TType) <*> f_ (y, I.TType) 865 I.Pi b x (I.down 0 -> Just y) -> Pi b "" <$> f_ (x, I.TType) <*> f_ (y, I.TType)
866 I.Pi b x y -> newName >>= \n -> do 866 I.Pi b x y -> newName >>= \n -> do
867 t <- f_ (x, I.TType) 867 t <- f_ (x, I.TType)
868 Pi b n t <$> local ((Var n t, x):) (f_ (y, I.TType)) 868 Pi b n t <$> local ((Var n t, x):) (f_ (y, I.TType))
869 I.Lam b x y -> newName >>= \n -> do 869 I.Lam y -> case et of
870 t <- f_ (x, I.TType) 870 I.Pi b x yt -> newName >>= \n -> do
871 Lam b (PVar t n) t <$> local ((Var n t, x):) (ft y) 871 t <- f_ (x, I.TType)
872 I.Con (I.ConName s _ _ t) xs -> Con s <$> f_ (t, I.TType) <*> mapM ft xs 872 Lam b (PVar t n) t <$> local ((Var n t, x):) (f_ (y, yt))
873 I.TyCon (I.TyConName s _ _ t _ _) xs -> Con s <$> f_ (t, I.TType) <*> mapM ft xs 873 I.Con s n xs -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (I.mkConPars n et ++ xs)
874 I.TyCon s xs -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs
875 I.Fun s xs -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs
876 I.CaseFun s xs -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs
877 I.Neut (I.App_ a b) -> asks makeTE >>= \te -> do
878 let t = I.neutType te a
879 app' <$> f_ (I.Neut a, t) <*> (head <$> chain [] t [b])
874 I.ELit l -> pure $ ELit l 880 I.ELit l -> pure $ ELit l
875 I.Fun (I.FunName s _ t) xs -> Fun s <$> f_ (t, I.TType) <*> mapM ft xs
876 I.CaseFun x@(I.CaseFunName _ t _) xs -> Fun (show x) <$> f_ (t, I.TType) <*> mapM ft xs
877 I.App a b -> app' <$> ft a <*> ft b
878 I.TType -> pure TType 881 I.TType -> pure TType
879 I.PMLabel x _ -> f_ (x, et) 882 I.PMLabel x _ -> f_ (x, et)
880 I.FixLabel _ x -> f_ (x, et) 883 I.FixLabel _ x -> f_ (x, et)
881-- I.LabelEnd x -> f x -- not possible 884-- I.LabelEnd x -> f x -- not possible
882 z -> error $ "toExp: " ++ show z 885 z -> error $ "toExp: " ++ show z
883 886
884 ft x = asks makeTE >>= \te -> f_ (x, I.expType_ "8" te x) 887 chain acc t [] = return $ reverse acc
888 chain acc t@(I.Pi b at y) (a: as) = do
889 a' <- f_ (a, at)
890 chain (a': acc) (I.appTy t a) as
885 891
886 xs !!! i | i < 0 || i >= length xs = error $ show xs ++ " !! " ++ show i 892 xs !!! i | i < 0 || i >= length xs = error $ show xs ++ " !! " ++ show i
887 xs !!! i = xs !! i 893 xs !!! i = xs !! i
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 971c7197..9fdef49a 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -7,24 +7,26 @@
7{-# LANGUAGE ScopedTypeVariables #-} 7{-# LANGUAGE ScopedTypeVariables #-}
8{-# LANGUAGE RecursiveDo #-} 8{-# LANGUAGE RecursiveDo #-}
9{-# LANGUAGE RankNTypes #-} 9{-# LANGUAGE RankNTypes #-}
10{-# LANGUAGE MultiParamTypeClasses #-}
11{-# LANGUAGE UndecidableInstances #-}
10{-# LANGUAGE GeneralizedNewtypeDeriving #-} 12{-# LANGUAGE GeneralizedNewtypeDeriving #-}
11{-# LANGUAGE DeriveFunctor #-} 13{-# LANGUAGE DeriveFunctor #-}
12{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} -- TODO: remove 14{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} -- TODO: remove
13{-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove 15{-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove
14-- {-# OPTIONS_GHC -O0 #-} 16-- {-# OPTIONS_GHC -O0 #-}
15module LambdaCube.Compiler.Infer 17module LambdaCube.Compiler.Infer
16 ( Binder (..), SName, Lit(..), Visibility(..), FunName(..), CaseFunName(..), ConName(..), TyConName(..), Export(..), Module(..) 18 ( Binder (..), SName, Lit(..), Visibility(..), Export(..), Module(..)
17 , Exp (..), ExpType, GlobalEnv 19 , Exp (..), ExpType, GlobalEnv
18 , pattern Var, pattern Fun, pattern CaseFun, pattern TyCaseFun, pattern App, pattern PMLabel, pattern FixLabel 20 , pattern Var, pattern Fun, pattern CaseFun, pattern TyCaseFun, pattern App_, pattern PMLabel, pattern FixLabel
19 , pattern Con, pattern TyCon, pattern Lam, pattern Pi, pattern TTyCon0 21 , pattern Con, pattern TyCon, pattern Pi, pattern Lam
20 , outputType, boolType, trueExp 22 , outputType, boolType, trueExp
21 , downE 23 , down
22 , litType 24 , litType
23 , initEnv, Env(..), pattern EBind2 25 , initEnv, Env(..), pattern EBind2
24 , Infos(..), listInfos, ErrorMsg(..), PolyEnv(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_ 26 , Infos(..), listInfos, ErrorMsg(..), PolyEnv(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_
25 , ImportItems (..) 27 , ImportItems (..)
26 , SI(..), Range(..) 28 , SI(..), Range(..)
27 , expType_ 29 , nType, neutType, appTy, mkConPars
28 , MaxDB(..) 30 , MaxDB(..)
29 ) where 31 ) where
30import Data.Monoid 32import Data.Monoid
@@ -49,94 +51,84 @@ import LambdaCube.Compiler.Parser
49data Exp 51data Exp
50 = TType 52 = TType
51 | ELit Lit 53 | ELit Lit
52 | Con_ MaxDB ConName [Exp] 54 | Con_ MaxDB ConName Int [Exp]
53 | TyCon_ MaxDB TyConName [Exp] 55 | TyCon_ MaxDB TyConName [Exp]
54 | Pi_ MaxDB Visibility Exp Exp 56 | Pi_ MaxDB Visibility Exp Exp
55 | Lam_ MaxDB Visibility Exp Exp 57 | Lam_ MaxDB Exp
56 | Neut MaxDB Neutral 58 | Neut Neutral
57 | Label LabelKind Exp{-folded expression-} Exp{-unfolded expression-} 59 | Label LabelKind Exp{-folded expression-} Exp{-unfolded expression-}
58 | LabelEnd_ LEKind Exp 60 | LabelEnd_ LEKind Exp
59 deriving (Show) 61 deriving (Show)
60 62
61-- constraints env
62data CEnv a
63 = MEnd a
64 | Meta Exp (CEnv a)
65 | Assign !Int ExpType (CEnv a) -- De Bruijn index decreasing assign reservedOp, only for metavariables (non-recursive)
66 deriving (Show, Functor)
67
68data Neutral 63data Neutral
69 = Fun_ FunName [Exp] 64 = Fun__ MaxDB FunName [Exp]
70 | CaseFun_ CaseFunName [Exp] -- todo: neutral at the end 65 | CaseFun__ MaxDB CaseFunName [Exp] -- todo: neutral at the end
71 | TyCaseFun_ TyCaseFunName [Exp] -- todo: neutral at the end 66 | TyCaseFun__ MaxDB TyCaseFunName [Exp] -- todo: neutral at the end
72 | App_ Exp{-todo: Neutral-} Exp 67 | App__ MaxDB Neutral Exp
73 | Var_ !Int -- De Bruijn variable 68 | Var_ !Int -- De Bruijn variable
74 deriving (Show) 69 deriving (Show)
75 70
71data ConName = ConName SName MFixity Int{-ordinal number, e.g. Zero:0, Succ:1-} TyConName Type
72
73data TyConName = TyConName SName MFixity Int{-num of indices-} Type [ConName]{-constructors-} CaseFunName
74
75data FunName = FunName SName MFixity Type
76
77data CaseFunName = CaseFunName SName Type Int{-num of parameters-}
78
79data TyCaseFunName = TyCaseFunName SName Type
80
76type Type = Exp 81type Type = Exp
82type ExpType = (Exp, Type)
77type SExp2 = SExp' ExpType 83type SExp2 = SExp' ExpType
78 84
79data ConName = ConName SName MFixity Int{-ordinal number, e.g. Zero:0, Succ:1-} Type 85instance Show ConName where show (ConName n _ _ _ _) = n
80instance Show ConName where show (ConName n _ _ _) = n 86instance Eq ConName where ConName n _ _ _ _ == ConName n' _ _ _ _ = n == n'
81instance Eq ConName where ConName n _ _ _ == ConName n' _ _ _ = n == n'
82
83data TyConName = TyConName SName MFixity Int{-num of indices-} Type [ConName]{-constructors-} Type{-case type-}
84instance Show TyConName where show (TyConName n _ _ _ _ _) = n 87instance Show TyConName where show (TyConName n _ _ _ _ _) = n
85instance Eq TyConName where TyConName n _ _ _ _ _ == TyConName n' _ _ _ _ _ = n == n' 88instance Eq TyConName where TyConName n _ _ _ _ _ == TyConName n' _ _ _ _ _ = n == n'
86
87data FunName = FunName SName MFixity Type
88instance Show FunName where show (FunName n _ _) = n 89instance Show FunName where show (FunName n _ _) = n
89instance Eq FunName where FunName n _ _ == FunName n' _ _ = n == n' 90instance Eq FunName where FunName n _ _ == FunName n' _ _ = n == n'
90
91data CaseFunName = CaseFunName SName Type Int{-num of parameters-}
92instance Show CaseFunName where show (CaseFunName n _ _) = caseName n 91instance Show CaseFunName where show (CaseFunName n _ _) = caseName n
93instance Eq CaseFunName where CaseFunName n _ _ == CaseFunName n' _ _ = n == n' 92instance Eq CaseFunName where CaseFunName n _ _ == CaseFunName n' _ _ = n == n'
94
95data TyCaseFunName = TyCaseFunName SName Type
96instance Show TyCaseFunName where show (TyCaseFunName n _) = MatchName n 93instance Show TyCaseFunName where show (TyCaseFunName n _) = MatchName n
97instance Eq TyCaseFunName where TyCaseFunName n _ == TyCaseFunName n' _ = n == n' 94instance Eq TyCaseFunName where TyCaseFunName n _ == TyCaseFunName n' _ = n == n'
98 95
99type ExpType = (Exp, Type)
100
101-------------------------------------------------------------------------------- auxiliary functions and patterns 96-------------------------------------------------------------------------------- auxiliary functions and patterns
102 97
103infixl 2 `App`, `app_` 98infixl 2 `App`, `app_`
104infixr 1 :~> 99infixr 1 :~>
105 100
106pattern Fun a b <- Neut _ (Fun_ a b) where Fun a b = Neut (foldMap maxDB_ b) (Fun_ a b) 101pattern Fun_ a b <- Fun__ _ a b where Fun_ a b = Fun__ (foldMap maxDB_ b) a b
107pattern CaseFun a b <- Neut _ (CaseFun_ a b) where CaseFun a b = Neut (foldMap maxDB_ b) (CaseFun_ a b) 102pattern CaseFun_ a b <- CaseFun__ _ a b where CaseFun_ a b = CaseFun__ (foldMap maxDB_ b) a b
108pattern TyCaseFun a b <- Neut _ (TyCaseFun_ a b) where TyCaseFun a b = Neut (foldMap maxDB_ b) (TyCaseFun_ a b) 103pattern TyCaseFun_ a b <- TyCaseFun__ _ a b where TyCaseFun_ a b = TyCaseFun__ (foldMap maxDB_ b) a b
109pattern App a b <- Neut _ (App_ a b) where App a b = Neut (maxDB_ a <> maxDB_ b) (App_ a b) 104pattern App_ a b <- App__ _ a b where App_ a b = App__ (maxDB_ a <> maxDB_ b) a b
110pattern Var a <- Neut _ (Var_ a) where Var a = Neut (varDB a) (Var_ a) 105pattern Fun a b = Neut (Fun_ a b)
106pattern CaseFun a b = Neut (CaseFun_ a b)
107pattern TyCaseFun a b = Neut (TyCaseFun_ a b)
108pattern App a b <- Neut (App_ (Neut -> a) b)
109pattern Var a = Neut (Var_ a)
110
111conParams (conTypeName -> TyConName _ _ _ _ _ (CaseFunName _ _ pars)) = pars
112mkConPars n (snd . getParams -> TyCon (TyConName _ _ _ _ _ (CaseFunName _ _ pars)) xs) = take (min n pars) xs
113conName a b c d = ConName a b c (get $ snd $ getParams d) d
114 where
115 get (TyCon s _) = s
111 116
112pattern Con x y <- Con_ _ x y where Con x y = Con_ (foldMap maxDB_ y) x y 117pattern Con x n y <- Con_ _ x n y where Con x n y = Con_ (foldMap maxDB_ y) x n y
118pattern ConN s a <- Con (ConName s _ _ _ _) _ a
119pattern TCon s i t a <- Con (ConName s _ i _ t) _ a where TCon s i t a = Con (conName s Nothing i t) 0 a -- todo: don't match on type
113pattern TyCon x y <- TyCon_ _ x y where TyCon x y = TyCon_ (foldMap maxDB_ y) x y 120pattern TyCon x y <- TyCon_ _ x y where TyCon x y = TyCon_ (foldMap maxDB_ y) x y
114pattern Lam v x y <- Lam_ _ v x y where Lam v x y = Lam_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y 121pattern Lam y <- Lam_ _ y where Lam y = Lam_ (lowerDB (maxDB_ y)) y
115pattern Pi v x y <- Pi_ _ v x y where Pi v x y = Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y 122pattern Pi v x y <- Pi_ _ v x y where Pi v x y = Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y
116
117pattern FunN a b <- Fun (FunName a _ _) b 123pattern FunN a b <- Fun (FunName a _ _) b
118pattern TFun a t b <- Fun (FunName a _ t) b where TFun a t b = Fun (FunName a Nothing t) b 124pattern TFun a t b <- Fun (FunName a _ t) b where TFun a t b = Fun (FunName a Nothing t) b
119 125pattern TFun' a t b <- Fun_ (FunName a _ t) b where TFun' a t b = Fun_ (FunName a Nothing t) b
120pattern Lam' b <- Lam _ _ b
121
122pattern CstrT t a b = TFun "'EqCT" (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b]
123pattern ReflCstr x = TFun "reflCstr" (TType :~> CstrT TType (Var 0) (Var 0)) [x]
124pattern Coe a b w x = TFun "coe" (TType :~> TType :~> CstrT TType (Var 1) (Var 0) :~> Var 2 :~> Var 2) [a,b,w,x]
125pattern ParEval t a b = TFun "parEval" (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, a, b]
126pattern Undef t = TFun "undefined" (Pi Hidden TType (Var 0)) [t]
127
128pattern ConN s a <- Con (ConName s _ _ _) a
129pattern TCon s i t a <- Con (ConName s _ i t) a where TCon s i t a = Con (ConName s Nothing i t) a -- todo: don't match on type
130pattern TyConN s a <- TyCon (TyConName s _ _ _ _ _) a 126pattern TyConN s a <- TyCon (TyConName s _ _ _ _ _) a
131pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a where TTyCon s t a = TyCon (TyConName s Nothing (error "todo: inum") t (error "todo: tcn cons 2") $ error "TTyCon") a 127pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a where TTyCon s t a = TyCon (TyConName s Nothing (error "todo: inum") t (error "todo: tcn cons 2") $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a
132pattern TTyCon0 s <- TyCon (TyConName s _ _ TType _ _) [] where TTyCon0 s = TyCon (TyConName s Nothing (error "todo: inum2") TType (error "todo: tcn cons 3") $ error "TTyCon0") [] 128pattern TTyCon0 s <- TyCon (TyConName s _ _ TType _ _) [] where TTyCon0 s = TyCon (TyConName s Nothing 0 TType (error "todo: tcn cons 3") $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) []
133--pattern Sigma a b <- TyConN "Sigma" [a, Lam' b] where Sigma a b = TTyCon "Sigma" (error "sigmatype") [a, Lam Visible a{-todo: don't duplicate-} b] 129pattern a :~> b = Pi Visible a b
130
134pattern Unit = TTyCon0 "'Unit" 131pattern Unit = TTyCon0 "'Unit"
135pattern TT = TCon "TT" 0 Unit []
136pattern T2 a b = TFun "'T2" (TType :~> TType :~> TType) [a, b]
137pattern T2C a b = TFun "t2C" (Unit :~> Unit :~> Unit) [a, b]
138pattern Empty s <- TyCon (TyConName "'Empty" _ _ _ _ _) [EString s] where
139 Empty s = TyCon (TyConName "'Empty" Nothing (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [EString s]
140pattern TInt = TTyCon0 "'Int" 132pattern TInt = TTyCon0 "'Int"
141pattern TNat = TTyCon0 "'Nat" 133pattern TNat = TTyCon0 "'Nat"
142pattern TBool = TTyCon0 "'Bool" 134pattern TBool = TTyCon0 "'Bool"
@@ -144,25 +136,46 @@ pattern TFloat = TTyCon0 "'Float"
144pattern TString = TTyCon0 "'String" 136pattern TString = TTyCon0 "'String"
145pattern TChar = TTyCon0 "'Char" 137pattern TChar = TTyCon0 "'Char"
146pattern TOrdering = TTyCon0 "'Ordering" 138pattern TOrdering = TTyCon0 "'Ordering"
139pattern TTuple2 a b = TTyCon "'Tuple2" (TType :~> TType :~> TType) [a, b]
140pattern TVec a b = TTyCon "'VecS" (TType :~> TNat :~> TType) [b, a]
141pattern Empty s <- TyCon (TyConName "'Empty" _ _ _ _ _) [EString s] where
142 Empty s = TyCon (TyConName "'Empty" Nothing (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [EString s]
143
144pattern TT = TCon "TT" 0 Unit []
147pattern Zero = TCon "Zero" 0 TNat [] 145pattern Zero = TCon "Zero" 0 TNat []
148pattern Succ n = TCon "Succ" 1 (TNat :~> TNat) [n] 146pattern Succ n = TCon "Succ" 1 (TNat :~> TNat) [n]
147
148pattern CstrT t a b = TFun "'EqCT" (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b]
149pattern CstrT' t a b = TFun' "'EqCT" (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b]
150pattern ReflCstr x = TFun "reflCstr" (TType :~> CstrT TType (Var 0) (Var 0)) [x]
151pattern Coe a b w x = TFun "coe" (TType :~> TType :~> CstrT TType (Var 1) (Var 0) :~> Var 2 :~> Var 2) [a,b,w,x]
152pattern ParEval t a b = TFun "parEval" (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, a, b]
153pattern Undef t = TFun "undefined" (Pi Hidden TType (Var 0)) [t]
154pattern T2 a b = TFun "'T2" (TType :~> TType :~> TType) [a, b]
155pattern T2C a b = TFun "t2C" (Unit :~> Unit :~> Unit) [a, b]
156pattern CSplit a b c <- FunN "'Split" [a, b, c]
157
158pattern EInt a = ELit (LInt a)
159pattern EFloat a = ELit (LFloat a)
160pattern EChar a = ELit (LChar a)
161pattern EString a = ELit (LString a)
162pattern EBool a <- (getEBool -> Just a) where EBool = mkBool
163pattern ENat n <- (fromNatE -> Just n) where ENat = toNatE
164
165pattern LCon <- (isCon -> True)
166pattern CFun <- (isCaseFun -> True)
167pattern NoTup <- (noTup -> True)
168
169--pattern Sigma a b <- TyConN "Sigma" [a, Lam b] where Sigma a b = TTyCon "Sigma" (error "sigmatype") [a, Lam Visible a{-todo: don't duplicate-} b]
149--pattern TVec a b = TTyCon "'Vec" (TNat :~> TType :~> TType) [a, b] 170--pattern TVec a b = TTyCon "'Vec" (TNat :~> TType :~> TType) [a, b]
150pattern TVec a b = TTyCon "'VecS" (TType :~> TNat :~> TType) [b, a]
151--pattern Tuple2 a b c d = TCon "Tuple2" 0 Tuple2Type [a, b, c, d] 171--pattern Tuple2 a b c d = TCon "Tuple2" 0 Tuple2Type [a, b, c, d]
152--pattern Tuple0 = TCon "Tuple0" 0 TTuple0 [] 172--pattern Tuple0 = TCon "Tuple0" 0 TTuple0 []
153pattern CSplit a b c <- FunN "'Split" [a, b, c]
154
155--pattern TTuple0 :: Exp 173--pattern TTuple0 :: Exp
156--pattern TTuple0 <- _ where TTuple0 = TTyCon0 "'Tuple0" 174--pattern TTuple0 <- _ where TTuple0 = TTyCon0 "'Tuple0"
157--pattern Tuple2Type :: Exp 175--pattern Tuple2Type :: Exp
158--pattern Tuple2Type <- _ where Tuple2Type = Pi Hidden TType $ Pi Hidden TType $ Var 1 :~> Var 1 :~> tTuple2 (Var 3) (Var 2) 176--pattern Tuple2Type <- _ where Tuple2Type = Pi Hidden TType $ Pi Hidden TType $ Var 1 :~> Var 1 :~> TTuple2 (Var 3) (Var 2)
159
160tTuple2 a b = TTyCon "'Tuple2" (TType :~> TType :~> TType) [a, b]
161--tTuple3 a b c = TTyCon "'Tuple3" (TType :~> TType :~> TType :~> TType) [a, b, c] 177--tTuple3 a b c = TTyCon "'Tuple3" (TType :~> TType :~> TType :~> TType) [a, b, c]
162 178
163pattern NatE :: Int -> Exp
164pattern NatE n <- (fromNatE -> Just n) where NatE = toNatE
165
166toNatE :: Int -> Exp 179toNatE :: Int -> Exp
167toNatE 0 = Zero 180toNatE 0 = Zero
168toNatE n | n > 0 = Succ (toNatE (n - 1)) 181toNatE n | n > 0 = Succ (toNatE (n - 1))
@@ -172,12 +185,6 @@ fromNatE Zero = Just 0
172fromNatE (Succ n) = (1 +) <$> fromNatE n 185fromNatE (Succ n) = (1 +) <$> fromNatE n
173fromNatE _ = Nothing 186fromNatE _ = Nothing
174 187
175pattern EInt a = ELit (LInt a)
176pattern EFloat a = ELit (LFloat a)
177pattern EChar a = ELit (LChar a)
178pattern EString a = ELit (LString a)
179pattern EBool a <- (getEBool -> Just a) where EBool = mkBool
180
181mkBool False = TCon "False" 0 TBool [] 188mkBool False = TCon "False" 0 TBool []
182mkBool True = TCon "True" 1 TBool [] 189mkBool True = TCon "True" 1 TBool []
183 190
@@ -185,11 +192,6 @@ getEBool (ConN "False" []) = Just False
185getEBool (ConN "True" []) = Just True 192getEBool (ConN "True" []) = Just True
186getEBool _ = Nothing 193getEBool _ = Nothing
187 194
188pattern LCon <- (isCon -> True)
189pattern CFun <- (isCaseFun -> True)
190
191pattern a :~> b = Pi Visible a b
192
193isCaseFun (Fun f _) = True 195isCaseFun (Fun f _) = True
194isCaseFun (CaseFun f _) = True 196isCaseFun (CaseFun f _) = True
195isCaseFun (TyCaseFun f _) = True 197isCaseFun (TyCaseFun f _) = True
@@ -197,7 +199,7 @@ isCaseFun _ = False
197 199
198isCon = \case 200isCon = \case
199 TType -> True 201 TType -> True
200 Con _ _ -> True 202 Con _ _ _ -> True
201 TyCon _ _ -> True 203 TyCon _ _ -> True
202 ELit _ -> True 204 ELit _ -> True
203 _ -> False 205 _ -> False
@@ -207,15 +209,11 @@ mkOrdering = \case
207 EQ -> TCon "EQ" 1 TOrdering [] 209 EQ -> TCon "EQ" 1 TOrdering []
208 GT -> TCon "GT" 2 TOrdering [] 210 GT -> TCon "GT" 2 TOrdering []
209 211
210pattern NoTup <- (noTup -> True)
211
212noTup (TyConN s _) = take 6 s /= "'Tuple" -- todo 212noTup (TyConN s _) = take 6 s /= "'Tuple" -- todo
213noTup _ = False 213noTup _ = False
214 214
215conTypeName :: ConName -> TyConName 215conTypeName :: ConName -> TyConName
216conTypeName (ConName _ _ _ t) = case snd (getParams t) of 216conTypeName (ConName _ _ _ t _) = t
217 TyCon n _ -> n
218 _ -> error "impossible"
219 217
220outputType = TTyCon0 "'Output" 218outputType = TTyCon0 "'Output"
221boolType = TBool 219boolType = TBool
@@ -260,6 +258,13 @@ unlabel' a = a
260 258
261-------------------------------------------------------------------------------- low-level toolbox 259-------------------------------------------------------------------------------- low-level toolbox
262 260
261class Up a => Subst b a where
262 subst :: Int -> b -> a -> a
263
264down :: (Subst Exp a) => Int -> a -> Maybe a
265down t x | used t x = Nothing
266 | otherwise = Just $ subst t (error "impossible: down" :: Exp) x
267
263instance Eq Exp where 268instance Eq Exp where
264 PMLabel a _ == PMLabel a' _ = a == a' 269 PMLabel a _ == PMLabel a' _ = a == a'
265 FixLabel a _ == FixLabel a' _ = a == a' 270 FixLabel a _ == FixLabel a' _ = a == a'
@@ -267,13 +272,13 @@ instance Eq Exp where
267 a == FixLabel _ a' = a == a' 272 a == FixLabel _ a' = a == a'
268 LabelEnd_ k a == a' = a == a' 273 LabelEnd_ k a == a' = a == a'
269 a == LabelEnd_ k' a' = a == a' 274 a == LabelEnd_ k' a' = a == a'
270 Lam' a == Lam' a' = a == a' 275 Lam a == Lam a' = a == a'
271 Pi a b c == Pi a' b' c' = (a, b, c) == (a', b', c') 276 Pi a b c == Pi a' b' c' = (a, b, c) == (a', b', c')
272 Con a b == Con a' b' = (a, b) == (a', b') 277 Con a n b == Con a' n' b' = (a, n, b) == (a', n', b')
273 TyCon a b == TyCon a' b' = (a, b) == (a', b') 278 TyCon a b == TyCon a' b' = (a, b) == (a', b')
274 TType == TType = True 279 TType == TType = True
275 ELit l == ELit l' = l == l' 280 ELit l == ELit l' = l == l'
276 Neut _ a == Neut _ a' = a == a' 281 Neut a == Neut a' = a == a'
277 _ == _ = False 282 _ == _ = False
278 283
279instance Eq Neutral where 284instance Eq Neutral where
@@ -284,93 +289,28 @@ instance Eq Neutral where
284 Var_ a == Var_ a' = a == a' 289 Var_ a == Var_ a' = a == a'
285 _ == _ = False 290 _ == _ = False
286 291
287newtype MaxDB = MaxDB {getMaxDB{-, getMaxDB' -} :: Maybe Int} 292isClosed (maxDB_ -> MaxDB x) = isNothing x
288
289instance Monoid MaxDB where
290 mempty = MaxDB Nothing --0 0
291 MaxDB a `mappend` MaxDB a' = MaxDB $ Just $ max (fromMaybe 0 a) (fromMaybe 0 a') -- (max b b')
292
293instance Show MaxDB where show _ = "MaxDB"
294
295varDB i = MaxDB $ Just $ i + 1--) -- (i + 1)
296
297lowerDB (MaxDB i) = MaxDB $ (+ (- 1)) <$> i --(i-1) (j-1)
298lowerDB' l (MaxDB i) = MaxDB $ Just $ 1 + max l (fromMaybe 0 i) -- (1 + max l j)
299combineDB a b = a --(MaxDB a b) ~(MaxDB a' b') = MaxDB a (max b b')
300
301closed = mempty
302
303isClosed (maxDB_ -> MaxDB x) = isNothing x --False
304 293
305-- 0 means that no free variable is used 294-- 0 means that no free variable is used
306-- 1 means that only var 0 is used 295-- 1 means that only var 0 is used
307maxDB :: Exp -> Int
308maxDB = max 0 . fromMaybe 0 . getMaxDB . maxDB_ 296maxDB = max 0 . fromMaybe 0 . getMaxDB . maxDB_
309maxDB' = maxDB --max 0 . fromMaybe 0 . getMaxDB' . maxDB_
310 297
311--assign :: (Int -> Exp -> CEnv Exp -> a) -> (Int -> Exp -> CEnv Exp -> a) -> Int -> Exp -> CEnv Exp -> a 298free x | isClosed x = mempty
312swapAssign _ clet i (Var j, t) b | i > j = clet j (Var (i-1), t) $ subst_ "swapAssign" j (Var (i-1)) $ up1_ i b 299free x = fold (\i k -> Set.fromList [k - i | k >= i]) 0 x
313swapAssign clet _ i a b = clet i a b
314
315assign = swapAssign Assign Assign
316
317freeE x | isClosed x = mempty
318freeE x = fold (\i k -> Set.fromList [k - i | k >= i]) 0 x
319
320class Up a where
321 up_ :: Int -> Int -> a -> a
322 up_ n i = iterateN n $ up1_ i
323 up1_ :: Int -> a -> a
324 up1_ = up_ 1
325
326 subst :: Env -> Int -> Exp -> a -> a
327
328 fold :: Monoid e => (Int -> Int -> e) -> Int -> a -> e
329
330 used :: Int -> a -> Bool
331
332 maxDB_ :: a -> MaxDB
333
334 closedExp :: a -> a
335 closedExp a = a
336
337up n = up_ n 0
338subst_ err = subst (error $ "subst_: todo: environment required in " ++ err) -- todo: remove
339 300
340instance Up Exp where 301instance Up Exp where
341 up_ n = f where 302 up_ n = f where
342 f i e | isClosed e = e 303 f i e | isClosed e = e
343 f i e = case e of 304 f i e = case e of
344 Var k -> Var $ if k >= i then k+n else k 305 Lam b -> Lam (f (i+1) b)
345 Lam h a b -> Lam h (f i a) (f (i+1) b)
346 Pi h a b -> Pi h (f i a) (f (i+1) b) 306 Pi h a b -> Pi h (f i a) (f (i+1) b)
347 Fun s as -> Fun s $ map (f i) as 307 Con s pn as -> Con s pn $ map (f i) as
348 CaseFun s as -> CaseFun s $ map (f i) as
349 TyCaseFun s as -> TyCaseFun s $ map (f i) as
350 Con s as -> Con s $ map (f i) as
351 TyCon s as -> TyCon s $ map (f i) as 308 TyCon s as -> TyCon s $ map (f i) as
352 App a b -> App (f i a) (f i b) 309 Neut x -> Neut $ up_ n i x
353 Label lk x y -> Label lk (f i x) $ f i y 310 Label lk x y -> Label lk (f i x) $ f i y
354 LabelEnd_ k x -> LabelEnd_ k $ f i x 311 LabelEnd_ k x -> LabelEnd_ k $ f i x
355 x@TType{} -> x 312 x@TType{} -> x
356 x@ELit{} -> x 313 x@ELit{} -> x
357-- Neut _ x -> Neut
358
359 subst te i x e | {-i >= maxDB e-} isClosed e = e
360 subst te i x e = case e of
361 Label lk z v -> label lk (subst_ "slab" i x z) $ subst te{-todo: label env?-} i x v
362 Var k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> x
363 Lam h a b -> Lam h (subst te i x a) (subst te (i+1) (up 1 x) b)
364 Pi h a b -> Pi h (subst te i x a) (subst te (i+1) (up 1 x) b)
365 Fun s as -> eval te $ Fun s $ subst te i x <$> as
366 CaseFun s as -> eval te $ CaseFun s $ subst te i x <$> as
367 TyCaseFun s as -> eval te $ TyCaseFun s $ subst te i x <$> as
368 Con s as -> Con s $ subst te i x <$> as
369 TyCon s as -> TyCon s $ subst te i x <$> as
370 TType -> TType
371 ELit l -> ELit l
372 App a b -> app_ (subst te i x a) (subst te i x b) -- todo: precise env?
373 LabelEnd_ k a -> LabelEnd_ k $ subst te i x a
374 314
375 used i e 315 used i e
376 | i >= maxDB e = False 316 | i >= maxDB e = False
@@ -379,58 +319,66 @@ instance Up Exp where
379 fold f i = \case 319 fold f i = \case
380 PMLabel x _ -> fold f i x 320 PMLabel x _ -> fold f i x
381 FixLabel _ x -> fold f i x 321 FixLabel _ x -> fold f i x
382 Lam' b -> {-fold f i t <> todo: explain why this is not needed -} fold f (i+1) b 322 Lam b -> {-fold f i t <> todo: explain why this is not needed -} fold f (i+1) b
383 Pi _ a b -> fold f i a <> fold f (i+1) b 323 Pi _ a b -> fold f i a <> fold f (i+1) b
384 Con _ as -> foldMap (fold f i) as 324 Con _ _ as -> foldMap (fold f i) as
385 TyCon _ as -> foldMap (fold f i) as 325 TyCon _ as -> foldMap (fold f i) as
386 TType -> mempty 326 TType -> mempty
387 ELit _ -> mempty 327 ELit _ -> mempty
388 LabelEnd_ _ x -> fold f i x 328 LabelEnd_ _ x -> fold f i x
389 Neut _ x -> fold f i x 329 Neut x -> fold f i x
390 330
391 maxDB_ = \case 331 maxDB_ = \case
392 332 Lam_ c _ -> c
393 Lam_ c _ _ _ -> c
394 Pi_ c _ _ _ -> c 333 Pi_ c _ _ _ -> c
395 Con_ c _ _ -> c 334 Con_ c _ _ _ -> c
396 TyCon_ c _ _ -> c 335 TyCon_ c _ _ -> c
397 Neut c _ -> c
398 336
399 PMLabel x y -> maxDB_ x `combineDB` maxDB_ y 337 Neut x -> maxDB_ x
338 PMLabel x y -> maxDB_ x -- `combineDB` maxDB_ y
400 FixLabel x y -> maxDB_ x <> maxDB_ y 339 FixLabel x y -> maxDB_ x <> maxDB_ y
401 TType -> mempty 340 TType -> mempty
402 ELit _ -> mempty 341 ELit _ -> mempty
403 LabelEnd_ _ x -> maxDB_ x 342 LabelEnd_ _ x -> maxDB_ x
404 343
405 closedExp = \case 344 closedExp = \case
406 Lam_ _ a b c -> Lam_ closed a b c 345 Lam_ _ c -> Lam_ mempty c
407 Pi_ _ a b c -> Pi_ closed a b c 346 Pi_ _ a b c -> Pi_ mempty a b c
408 Con_ _ a b -> Con_ closed a b 347 Con_ _ a b c -> Con_ mempty a b c
409 TyCon_ _ a b -> TyCon_ closed a b 348 TyCon_ _ a b -> TyCon_ mempty a b
410 Neut _ a -> Neut closed a 349 Neut a -> Neut $ closedExp a
411 e -> e 350 e -> e
412 351
352instance Subst Exp Exp where
353 subst i x e | {-i >= maxDB e-} isClosed e = e
354 subst i x e = case e of
355 Label lk z v -> label lk (subst i x z) $ subst i x v
356 Var k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> x
357 Lam b -> Lam (subst (i+1) (up 1 x) b)
358 Pi h a b -> Pi h (subst i x a) (subst (i+1) (up 1 x) b)
359 Fun s as -> eval $ Fun s $ subst i x <$> as
360 CaseFun s as -> eval $ CaseFun s $ subst i x <$> as
361 TyCaseFun s as -> eval $ TyCaseFun s $ subst i x <$> as
362 Con s n as -> Con s n $ subst i x <$> as
363 TyCon s as -> TyCon s $ subst i x <$> as
364 TType -> TType
365 ELit l -> ELit l
366 App a b -> app_ (subst i x a) (subst i x b)
367 LabelEnd_ k a -> LabelEnd_ k $ subst i x a
368
413instance Up Neutral where 369instance Up Neutral where
414 370
415 up_ n = f where 371 up_ n = f where
416-- f i e | isClosed e = e 372 f i e | isClosed e = e
417 f i e = case e of 373 f i e = case e of
418 Var_ k -> Var_ $ if k >= i then k+n else k 374 Var_ k -> Var_ $ if k >= i then k+n else k
419 Fun_ s as -> Fun_ s $ map (up_ n i) as 375 Fun_ s as -> Fun_ s $ map (up_ n i) as
420 CaseFun_ s as -> CaseFun_ s $ map (up_ n i) as 376 CaseFun_ s as -> CaseFun_ s $ map (up_ n i) as
421 TyCaseFun_ s as -> TyCaseFun_ s $ map (up_ n i) as 377 TyCaseFun_ s as -> TyCaseFun_ s $ map (up_ n i) as
422 App_ a b -> App_ (up_ n i a) (up_ n i b) 378 App_ a b -> App_ (up_ n i a) (up_ n i b)
423{- 379
424-- subst te i x e | {-i >= maxDB e-} isClosed e = e
425 subst te i x e = case e of
426 Var_ k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> x
427 Fun s as -> eval te $ Fun s $ subst te i x <$> as
428 CaseFun s as -> eval te $ CaseFun s $ subst te i x <$> as
429 TyCaseFun s as -> eval te $ TyCaseFun s $ subst te i x <$> as
430 App a b -> app_ (subst te i x a) (subst te i x b) -- todo: precise env?
431-}
432 used i e 380 used i e
433-- | i >= maxDB e = False 381 | i >= maxDB e = False
434 | otherwise = ((getAny .) . fold ((Any .) . (==))) i e 382 | otherwise = ((getAny .) . fold ((Any .) . (==))) i e
435 383
436 fold f i = \case 384 fold f i = \case
@@ -440,123 +388,41 @@ instance Up Neutral where
440 TyCaseFun_ _ as -> foldMap (fold f i) as 388 TyCaseFun_ _ as -> foldMap (fold f i) as
441 App_ a b -> fold f i a <> fold f i b 389 App_ a b -> fold f i a <> fold f i b
442 390
443{- 391 maxDB_ = \case
444data Neutral 392 Var_ k -> varDB k
445 = Fun_ FunName [Exp] 393 Fun__ c _ as -> c
446 | CaseFun_ CaseFunName [Exp] -- todo: neutral at the end 394 CaseFun__ c _ as -> c
447 | TyCaseFun_ TyCaseFunName [Exp] -- todo: neutral at the end 395 TyCaseFun__ c _ as -> c
448 | App_ Exp{-todo: Neutral-} Exp 396 App__ c a b -> c
449 | Var_ !Int -- De Bruijn variable
450 deriving (Show)
451-}
452instance Up a => Up (CEnv a) where
453 up1_ i = \case
454 MEnd a -> MEnd $ up1_ i a
455 Meta a b -> Meta (up1_ i a) (up1_ (i+1) b)
456 Assign j a b -> handleLet i j $ \i' j' -> assign j' (up1_ i' a) (up1_ i' b)
457 where
458 handleLet i j f
459 | i > j = f (i-1) j
460 | i <= j = f i (j+1)
461
462 subst te i x = \case
463 MEnd a -> MEnd $ subst te i x a
464 Meta a b -> Meta (subst te i x a) (subst te (i+1) (up 1 x) b)
465 Assign j a b
466 | j > i, Just a' <- downE i a -> assign (j-1) a' (subst_ "sa" i (subst_ "sa" (j-1) (fst a') x) b)
467 | j > i, Just x' <- downE (j-1) x -> assign (j-1) (subst_ "sa" i x' a) (subst_ "sa" i x' b)
468 | j < i, Just a' <- downE (i-1) a -> assign j a' (subst_ "sa" (i-1) (subst_ "sa" j (fst a') x) b)
469 | j < i, Just x' <- downE j x -> assign j (subst_ "sa" (i-1) x' a) (subst_ "sa" (i-1) x' b)
470 | j == i -> Meta (cstrT (snd a) x $ fst a) $ up1_ 0 b
471
472 used i a = error "used @(CEnv _)"
473
474 fold _ _ _ = error "fold @(CEnv _)"
475 397
476instance (Up a, Up b) => Up (a, b) where 398 closedExp = \case
477 up_ n i (a, b) = (up_ n i a, up_ n i b) 399 x@Var_{} -> error "impossible"
478 subst env i x (a, b) = (subst env i x a, subst env i x b) 400 Fun__ _ a as -> Fun__ mempty a as
479 used i (a, b) = used i a || used i b 401 CaseFun__ _ a as -> CaseFun__ mempty a as
480 fold _ _ _ = error "fold @(_,_)" 402 TyCaseFun__ _ a as -> TyCaseFun__ mempty a as
481 maxDB_ (a, b) = maxDB_ a <> maxDB_ b 403 App__ _ a b -> App__ mempty a b
482 closedExp (a, b) = (closedExp a, closedExp b)
483 404
484downE t x | used t x = Nothing 405instance (Subst x a, Subst x b) => Subst x (a, b) where
485 | otherwise = Just $ subst (error "impossible") t (error "impossible: downE") x 406 subst i x (a, b) = (subst i x a, subst i x b)
486 407
487varType :: String -> Int -> Env -> (Binder, Exp) 408varType :: String -> Int -> Env -> (Binder, Exp)
488varType err n_ env = f n_ env where 409varType err n_ env = f n_ env where
489 f n (EAssign i (x, _) es) = second (subst_ "varType" i x) $ f (if n < i then n else n+1) es 410 f n (EAssign i (x, _) es) = second (subst i x) $ f (if n < i then n else n+1) es
490 f n (EBind2 b t es) = if n == 0 then (b, up 1 t) else second (up 1) $ f (n-1) es 411 f n (EBind2 b t es) = if n == 0 then (b, up 1 t) else second (up 1) $ f (n-1) es
491 f n (ELet2 _ (x, t) es) = if n == 0 then (BLam Visible{-??-}, up 1 t) else second (up 1) $ f (n-1) es 412 f n (ELet2 _ (x, t) es) = if n == 0 then (BLam Visible{-??-}, up 1 t) else second (up 1) $ f (n-1) es
492 f n e = either (error $ "varType: " ++ err ++ "\n" ++ show n_ ++ "\n" ++ ppShow env) (f n) $ parent e 413 f n e = either (error $ "varType: " ++ err ++ "\n" ++ show n_ ++ "\n" ++ ppShow env) (f n) $ parent e
493 414
494trSExp :: SExp -> SExp2
495trSExp = g where
496 g = \case
497 SApp si v a b -> SApp si v (g a) (g b)
498 SLet x a b -> SLet x (g a) (g b)
499 SBind si k si' a b -> SBind si k si' (g a) (g b)
500 SVar sn j -> SVar sn j
501 SGlobal sn -> SGlobal sn
502 SLit si l -> SLit si l
503
504-- todo: review
505substS j x = mapS' f2 ((+1) *** up 1) (j, x)
506 where
507 f2 sn j i = case uncurry (subst_ "substS'") i $ Var j of
508 Var k -> SVar sn k
509 x -> STyped (fst sn) (x, error "type of x"{-todo-})
510
511-------------------------------------------------------------------------------- reduction 415-------------------------------------------------------------------------------- reduction
512 416
513t2C TT TT = TT 417eval = \case
514t2C a b = T2C a b
515
516t2 Unit a = a
517t2 a Unit = a
518t2 (Empty a) (Empty b) = Empty (a <> b)
519t2 (Empty s) _ = Empty s
520t2 _ (Empty s) = Empty s
521t2 a b = T2 a b
522
523app_ :: Exp -> Exp -> Exp
524app_ (Lam' x) a = subst_ "app" 0 a x
525app_ (Con s xs) a = Con s (xs ++ [a])
526app_ (TyCon s xs) a = TyCon s (xs ++ [a])
527app_ (Label lk x e) a = label lk (app_ x a) $ app_ e a
528app_ (LabelEnd_ k x) a = LabelEnd_ k (app_ x a) -- ???
529app_ f a = App f a
530
531oneOp :: (forall a . Num a => a -> a) -> Exp -> Maybe Exp
532oneOp f = oneOp_ f f
533
534oneOp_ f _ (EFloat x) = Just $ EFloat $ f x
535oneOp_ _ f (EInt x) = Just $ EInt $ f x
536oneOp_ _ _ _ = Nothing
537
538twoOp :: (forall a . Num a => a -> a -> a) -> Exp -> Exp -> Maybe Exp
539twoOp f = twoOp_ f f
540
541twoOp_ f _ (EFloat x) (EFloat y) = Just $ EFloat $ f x y
542twoOp_ _ f (EInt x) (EInt y) = Just $ EInt $ f x y
543twoOp_ _ _ _ _ = Nothing
544
545modF x y = x - fromIntegral (floor (x / y)) * y
546
547twoOpBool :: (forall a . Ord a => a -> a -> Bool) -> Exp -> Exp -> Maybe Exp
548twoOpBool f (EFloat x) (EFloat y) = Just $ EBool $ f x y
549twoOpBool f (EInt x) (EInt y) = Just $ EBool $ f x y
550twoOpBool _ _ _ = Nothing
551
552eval te = \case
553 App a b -> app_ a b 418 App a b -> app_ a b
554 CstrT TType a b -> cstr a b 419 CstrT TType a b -> cstrT_ TType a b
555 CstrT t a b -> cstrT t a b 420 CstrT t a b -> cstrT t a b
556 ReflCstr a -> reflCstr te a 421 ReflCstr a -> reflCstr a
557 Coe a b TT d -> d 422 Coe a b TT d -> d
558 423
559 CaseFun (CaseFunName _ t pars) (drop (pars + 1) -> ps@(last -> UL (Con (ConName _ _ i _) (drop pars -> vs)))) | i /= (-1) -> foldl app_ (ps !! i) vs 424 CaseFun (CaseFunName _ t pars) (drop (pars + 1) -> ps@(last -> UL (Con (ConName _ _ i _ _) _ vs))) | i /= (-1) -> foldl app_ (ps !! i) vs
425
560 TyCaseFun (TyCaseFunName n ty) [_, t, UL (TyCon (TyConName n' _ _ _ _ _) vs), f] | n == n' -> foldl app_ t vs 426 TyCaseFun (TyCaseFunName n ty) [_, t, UL (TyCon (TyConName n' _ _ _ _ _) vs), f] | n == n' -> foldl app_ t vs
561 TyCaseFun (TyCaseFunName n ty) [_, t, LCon, f] -> f 427 TyCaseFun (TyCaseFunName n ty) [_, t, LCon, f] -> f
562 T2 a b -> t2 a b 428 T2 a b -> t2 a b
@@ -570,10 +436,10 @@ eval te = \case
570{- todo: generate 436{- todo: generate
571 Fun n@(FunName "natElim" _ _) [a, z, s, Succ x] -> let -- todo: replace let with better abstraction 437 Fun n@(FunName "natElim" _ _) [a, z, s, Succ x] -> let -- todo: replace let with better abstraction
572 sx = s `app_` x 438 sx = s `app_` x
573 in sx `app_` eval te (Fun n [a, z, s, x]) 439 in sx `app_` eval (Fun n [a, z, s, x])
574 FunN "natElim" [_, z, s, Zero] -> z 440 FunN "natElim" [_, z, s, Zero] -> z
575 Fun na@(FunName "finElim" _ _) [m, z, s, n, ConN "FSucc" [i, x]] -> let six = s `app_` i `app_` x-- todo: replace let with better abstraction 441 Fun na@(FunName "finElim" _ _) [m, z, s, n, ConN "FSucc" [i, x]] -> let six = s `app_` i `app_` x-- todo: replace let with better abstraction
576 in six `app_` eval te (Fun na [m, z, s, i, x]) 442 in six `app_` eval (Fun na [m, z, s, i, x])
577 FunN "finElim" [m, z, s, n, ConN "FZero" [i]] -> z `app_` i 443 FunN "finElim" [m, z, s, n, ConN "FZero" [i]] -> z `app_` i
578-} 444-}
579 445
@@ -617,108 +483,189 @@ eval te = \case
617 FunN "PrimNot" [_, _, _, EBool x] -> EBool $ not x 483 FunN "PrimNot" [_, _, _, EBool x] -> EBool $ not x
618 484
619 x -> x 485 x -> x
620 486 where
621reflCstr te = \case 487 cstrT t (UL a) (UL a') | a == a' = Unit
488 cstrT t (ConN "Succ" [a]) (ConN "Succ" [a']) = cstrT TNat a a'
489 cstrT t (FixLabel _ a) a' = cstrT t a a'
490 cstrT t a (FixLabel _ a') = cstrT t a a'
491 cstrT t a a' = CstrT t a a'
492
493 -- todo: use typ
494 cstrT_ typ = cstr__ []
495 where
496 cstr__ = cstr_
497
498 cstr_ [] (UL a) (UL a') | a == a' = Unit
499 cstr_ ns (LabelEnd_ k a) a' = cstr_ ns a a'
500 cstr_ ns a (LabelEnd_ k a') = cstr_ ns a a'
501 cstr_ ns (FixLabel _ a) a' = cstr_ ns a a'
502 cstr_ ns a (FixLabel _ a') = cstr_ ns a a'
503 -- cstr_ ns (PMLabel a _) a' = cstr_ ns a a'
504 -- cstr_ ns a (PMLabel a' _) = cstr_ ns a a'
505 -- cstr_ ns TType TType = Unit
506 cstr_ ns (Con a n xs) (Con a' n' xs') | a == a' && n == n' = foldr t2 Unit $ zipWith (cstr__ ns) xs xs'
507 cstr_ [] (TyConN "'FrameBuffer" [a, b]) (TyConN "'FrameBuffer" [a', b']) = t2 (cstrT TNat a a') (cstr__ [] b b') -- todo: elim
508 cstr_ ns (TyCon a xs) (TyCon a' xs') | a == a' = foldr t2 Unit $ zipWith (cstr__ ns) xs xs'
509 -- cstr_ ns (TyCon a []) (TyCon a' []) | a == a' = Unit
510 cstr_ ns (Var i) (Var i') | i == i', i < length ns = Unit
511 cstr_ (_: ns) (down 0 -> Just a) (down 0 -> Just a') = cstr__ ns a a'
512 -- cstr_ ((t, t'): ns) (UApp (down 0 -> Just a) (Var 0)) (UApp (down 0 -> Just a') (Var 0)) = traceInj2 (a, "V0") (a', "V0") $ cstr__ ns a a'
513 -- cstr_ ((t, t'): ns) a (UApp (down 0 -> Just a') (Var 0)) = traceInj (a', "V0") a $ cstr__ ns (Lam Visible t a) a'
514 -- cstr_ ((t, t'): ns) (UApp (down 0 -> Just a) (Var 0)) a' = traceInj (a, "V0") a' $ cstr__ ns a (Lam Visible t' a')
515-- cstr_ ns (Lam b) (Lam b') = cstr__ ((a, a'): ns) b b' -- todo
516 cstr_ ns (Pi h a b) (Pi h' a' b') | h == h' = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b')
517 -- cstr_ ns (Meta a b) (Meta a' b') = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b')
518 -- cstr_ [] t (Meta a b) = Meta a $ cstr_ [] (up 1 t) b
519 -- cstr_ [] (Meta a b) t = Meta a $ cstr_ [] b (up 1 t)
520 -- cstr_ ns (unApp -> Just (a, b)) (unApp -> Just (a', b')) = traceInj2 (a, show b) (a', show b') $ t2 (cstr__ ns a a') (cstr__ ns b b')
521 -- cstr_ ns (unApp -> Just (a, b)) (unApp -> Just (a', b')) = traceInj2 (a, show b) (a', show b') $ t2 (cstr__ ns a a') (cstr__ ns b b')
522 -- cstr_ ns (Label f xs _) (Label f' xs' _) | f == f' = foldr1 T2 $ zipWith (cstr__ ns) xs xs'
523
524 cstr_ [] (UL (FunN "'VecScalar" [a, b])) (TVec a' b') = t2 (cstrT TNat a a') (cstr__ [] b b')
525 cstr_ [] (UL (FunN "'VecScalar" [a, b])) (UL (FunN "'VecScalar" [a', b'])) = t2 (cstrT TNat a a') (cstr__ [] b b')
526 cstr_ [] (UL (FunN "'VecScalar" [a, b])) t@(TTyCon0 n) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t)
527 cstr_ [] t@(TTyCon0 n) (UL (FunN "'VecScalar" [a, b])) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t)
528
529 cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'FragmentOperation" [x]) = cstr__ ns a x
530 cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = cstr__ ns a $ TTuple2 x y
531
532 cstr_ ns@[] (TyConN "'Tuple2" [x, y]) (UL (FunN "'JoinTupleType" [x', y'])) = t2 (cstr__ ns x x') (cstr__ ns y y')
533 cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) (TyConN "'Tuple2" [x, y]) = t2 (cstr__ ns x' x) (cstr__ ns y' y)
534 cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) x@NoTup = t2 (cstr__ ns x' x) (cstr__ ns y' $ TTyCon0 "'Tuple0")
535
536 cstr_ ns@[] (x@NoTup) (UL (FunN "'InterpolatedType" [x'])) = cstr__ ns (TTyCon "'Interpolated" (TType :~> TType) [x]) x'
537
538 -- cstr_ [] (TyConN "'FrameBuffer" [a, b]) (UL (FunN "'TFFrameBuffer" [TyConN "'Image" [a', b']])) = T2 (cstrT TNat a a') (cstr__ [] b b')
539
540 cstr_ [] a@App{} a'@App{} = CstrT TType a a'
541 cstr_ [] a@CFun a'@CFun = CstrT TType a a'
542 cstr_ [] a@LCon a'@CFun = CstrT TType a a'
543 cstr_ [] a@LCon a'@App{} = CstrT TType a a'
544 cstr_ [] a@CFun a'@LCon = CstrT TType a a'
545 cstr_ [] a@App{} a'@LCon = CstrT TType a a'
546 cstr_ [] a@PMLabel{} a' = CstrT TType a a'
547 cstr_ [] a a'@PMLabel{} = CstrT TType a a'
548 cstr_ [] a a' | isVar a || isVar a' = CstrT TType a a'
549 cstr_ ns a a' = Empty $ unlines [ "can not unify"
550 , ppShow a
551 , "with"
552 , ppShow a'
553 ]
622{- 554{-
623 Unit -> TT 555 -- unApp (UApp a b) | isInjective a = Just (a, b) -- TODO: injectivity check
624 TType -> TT -- ? 556 unApp (Con a xs@(_:_)) = Just (Con a (init xs), last xs)
625 Con n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs 557 unApp (TyCon a xs@(_:_)) = Just (TyCon a (init xs), last xs)
626 TyCon n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs 558 unApp _ = Nothing
627 x -> {-error $ "reflCstr: " ++ show x-} ReflCstr x
628-} 559-}
629 x -> TT 560 isInjective _ = True--False
630 561
631cstrT t (UL a) (UL a') | a == a' = Unit 562 isVar Var{} = True
632cstrT t (ConN "Succ" [a]) (ConN "Succ" [a']) = cstrT TNat a a' 563 isVar (App a b) = isVar a
633cstrT t (FixLabel _ a) a' = cstrT t a a' 564 isVar _ = False
634cstrT t a (FixLabel _ a') = cstrT t a a'
635cstrT t a a' = CstrT t a a'
636 565
637cstr = cstrT_ TType 566 traceInj2 (a, a') (b, b') c | debug && (susp a || susp b) = trace_ (" inj'? " ++ show a ++ " : " ++ a' ++ " ---- " ++ show b ++ " : " ++ b') c
567 traceInj2 _ _ c = c
568 traceInj (x, y) z a | debug && susp x = trace_ (" inj? " ++ show x ++ " : " ++ y ++ " ---- " ++ show z) a
569 traceInj _ _ a = a
570
571 susp Con{} = False
572 susp TyCon{} = False
573 susp _ = True
574
575 isElemTy n = n `elem` ["'Bool", "'Float", "'Int"]
576
577 reflCstr = \case
578 {-
579 Unit -> TT
580 TType -> TT -- ?
581 Con n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs
582 TyCon n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs
583 x -> {-error $ "reflCstr: " ++ show x-} ReflCstr x
584 -}
585 x -> TT
586
587 t2C TT TT = TT
588 t2C a b = T2C a b
589
590 t2 Unit a = a
591 t2 a Unit = a
592 t2 (Empty a) (Empty b) = Empty (a <> b)
593 t2 (Empty s) _ = Empty s
594 t2 _ (Empty s) = Empty s
595 t2 a b = T2 a b
596
597 oneOp :: (forall a . Num a => a -> a) -> Exp -> Maybe Exp
598 oneOp f = oneOp_ f f
599
600 oneOp_ f _ (EFloat x) = Just $ EFloat $ f x
601 oneOp_ _ f (EInt x) = Just $ EInt $ f x
602 oneOp_ _ _ _ = Nothing
603
604 twoOp :: (forall a . Num a => a -> a -> a) -> Exp -> Exp -> Maybe Exp
605 twoOp f = twoOp_ f f
606
607 twoOp_ f _ (EFloat x) (EFloat y) = Just $ EFloat $ f x y
608 twoOp_ _ f (EInt x) (EInt y) = Just $ EInt $ f x y
609 twoOp_ _ _ _ _ = Nothing
610
611 modF x y = x - fromIntegral (floor (x / y)) * y
612
613 twoOpBool :: (forall a . Ord a => a -> a -> Bool) -> Exp -> Exp -> Maybe Exp
614 twoOpBool f (EFloat x) (EFloat y) = Just $ EBool $ f x y
615 twoOpBool f (EInt x) (EInt y) = Just $ EBool $ f x y
616 twoOpBool _ _ _ = Nothing
617
618cstr a b = eval $ CstrT TType a b
619
620app_ :: Exp -> Exp -> Exp
621app_ (Lam x) a = subst 0 a x
622app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a])
623app_ (TyCon s xs) a = TyCon s (xs ++ [a])
624app_ (Label lk x e) a = label lk (app_ x a) $ app_ e a
625app_ (LabelEnd_ k x) a = LabelEnd_ k (app_ x a) -- ???
626app_ (Neut f) a = Neut $ App_ f a
627
628-------------------------------------------------------------------------------- constraints env
629
630data CEnv a
631 = MEnd a
632 | Meta Exp (CEnv a)
633 | Assign !Int ExpType (CEnv a) -- De Bruijn index decreasing assign reservedOp, only for metavariables (non-recursive)
634 deriving (Show, Functor)
635
636instance (Subst Exp a) => Up (CEnv a) where
637 up1_ i = \case
638 MEnd a -> MEnd $ up1_ i a
639 Meta a b -> Meta (up1_ i a) (up1_ (i+1) b)
640 Assign j a b -> handleLet i j $ \i' j' -> assign j' (up1_ i' a) (up1_ i' b)
641 where
642 handleLet i j f
643 | i > j = f (i-1) j
644 | i <= j = f i (j+1)
645
646 used i a = error "used @(CEnv _)"
647
648 fold _ _ _ = error "fold @(CEnv _)"
649
650 maxDB_ _ = error "maxDB_ @(CEnv _)"
651
652instance (Subst Exp a) => Subst Exp (CEnv a) where
653 subst i x = \case
654 MEnd a -> MEnd $ subst i x a
655 Meta a b -> Meta (subst i x a) (subst (i+1) (up 1 x) b)
656 Assign j a b
657 | j > i, Just a' <- down i a -> assign (j-1) a' (subst i (subst (j-1) (fst a') x) b)
658 | j > i, Just x' <- down (j-1) x -> assign (j-1) (subst i x' a) (subst i x' b)
659 | j < i, Just a' <- down (i-1) a -> assign j a' (subst (i-1) (subst j (fst a') x) b)
660 | j < i, Just x' <- down j x -> assign j (subst (i-1) x' a) (subst (i-1) x' b)
661 | j == i -> Meta (eval $ CstrT (snd a) x $ fst a) $ up1_ 0 b
662
663--assign :: (Int -> Exp -> CEnv Exp -> a) -> (Int -> Exp -> CEnv Exp -> a) -> Int -> Exp -> CEnv Exp -> a
664swapAssign _ clet i (Var j, t) b | i > j = clet j (Var (i-1), t) $ subst j (Var (i-1)) $ up1_ i b
665swapAssign clet _ i a b = clet i a b
666
667assign = swapAssign Assign Assign
638 668
639-- todo: use typ
640cstrT_ typ = cstr__ []
641 where
642 cstr__ = cstr_
643
644 cstr_ [] (UL a) (UL a') | a == a' = Unit
645 cstr_ ns (LabelEnd_ k a) a' = cstr_ ns a a'
646 cstr_ ns a (LabelEnd_ k a') = cstr_ ns a a'
647 cstr_ ns (FixLabel _ a) a' = cstr_ ns a a'
648 cstr_ ns a (FixLabel _ a') = cstr_ ns a a'
649-- cstr_ ns (PMLabel a _) a' = cstr_ ns a a'
650-- cstr_ ns a (PMLabel a' _) = cstr_ ns a a'
651-- cstr_ ns TType TType = Unit
652 cstr_ ns (Con a xs) (Con a' xs') | a == a' = foldr t2 Unit $ zipWith (cstr__ ns) xs xs'
653 cstr_ [] (TyConN "'FrameBuffer" [a, b]) (TyConN "'FrameBuffer" [a', b']) = t2 (cstrT TNat a a') (cstr__ [] b b') -- todo: elim
654 cstr_ ns (TyCon a xs) (TyCon a' xs') | a == a' = foldr t2 Unit $ zipWith (cstr__ ns) xs xs'
655-- cstr_ ns (TyCon a []) (TyCon a' []) | a == a' = Unit
656 cstr_ ns (Var i) (Var i') | i == i', i < length ns = Unit
657 cstr_ (_: ns) (downE 0 -> Just a) (downE 0 -> Just a') = cstr__ ns a a'
658-- cstr_ ((t, t'): ns) (UApp (downE 0 -> Just a) (Var 0)) (UApp (downE 0 -> Just a') (Var 0)) = traceInj2 (a, "V0") (a', "V0") $ cstr__ ns a a'
659-- cstr_ ((t, t'): ns) a (UApp (downE 0 -> Just a') (Var 0)) = traceInj (a', "V0") a $ cstr__ ns (Lam Visible t a) a'
660-- cstr_ ((t, t'): ns) (UApp (downE 0 -> Just a) (Var 0)) a' = traceInj (a, "V0") a' $ cstr__ ns a (Lam Visible t' a')
661 cstr_ ns (Lam h a b) (Lam h' a' b') | h == h' = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b')
662 cstr_ ns (Pi h a b) (Pi h' a' b') | h == h' = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b')
663-- cstr_ ns (Meta a b) (Meta a' b') = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b')
664-- cstr_ [] t (Meta a b) = Meta a $ cstr_ [] (up 1 t) b
665-- cstr_ [] (Meta a b) t = Meta a $ cstr_ [] b (up 1 t)
666-- cstr_ ns (unApp -> Just (a, b)) (unApp -> Just (a', b')) = traceInj2 (a, show b) (a', show b') $ t2 (cstr__ ns a a') (cstr__ ns b b')
667-- cstr_ ns (unApp -> Just (a, b)) (unApp -> Just (a', b')) = traceInj2 (a, show b) (a', show b') $ t2 (cstr__ ns a a') (cstr__ ns b b')
668-- cstr_ ns (Label f xs _) (Label f' xs' _) | f == f' = foldr1 T2 $ zipWith (cstr__ ns) xs xs'
669
670 cstr_ [] (UL (FunN "'VecScalar" [a, b])) (TVec a' b') = t2 (cstrT TNat a a') (cstr__ [] b b')
671 cstr_ [] (UL (FunN "'VecScalar" [a, b])) (UL (FunN "'VecScalar" [a', b'])) = t2 (cstrT TNat a a') (cstr__ [] b b')
672 cstr_ [] (UL (FunN "'VecScalar" [a, b])) t@(TTyCon0 n) | isElemTy n = t2 (cstrT TNat a (NatE 1)) (cstr__ [] b t)
673 cstr_ [] t@(TTyCon0 n) (UL (FunN "'VecScalar" [a, b])) | isElemTy n = t2 (cstrT TNat a (NatE 1)) (cstr__ [] b t)
674
675 cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'FragmentOperation" [x]) = cstr__ ns a x
676 cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = cstr__ ns a $ tTuple2 x y
677
678 cstr_ ns@[] (TyConN "'Tuple2" [x, y]) (UL (FunN "'JoinTupleType" [x', y'])) = t2 (cstr__ ns x x') (cstr__ ns y y')
679 cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) (TyConN "'Tuple2" [x, y]) = t2 (cstr__ ns x' x) (cstr__ ns y' y)
680 cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) x@NoTup = t2 (cstr__ ns x' x) (cstr__ ns y' $ TTyCon0 "'Tuple0")
681
682 cstr_ ns@[] (x@NoTup) (UL (FunN "'InterpolatedType" [x'])) = cstr__ ns (TTyCon "'Interpolated" (TType :~> TType) [x]) x'
683
684-- cstr_ [] (TyConN "'FrameBuffer" [a, b]) (UL (FunN "'TFFrameBuffer" [TyConN "'Image" [a', b']])) = T2 (cstrT TNat a a') (cstr__ [] b b')
685
686 cstr_ [] a@App{} a'@App{} = CstrT TType a a'
687 cstr_ [] a@CFun a'@CFun = CstrT TType a a'
688 cstr_ [] a@LCon a'@CFun = CstrT TType a a'
689 cstr_ [] a@LCon a'@App{} = CstrT TType a a'
690 cstr_ [] a@CFun a'@LCon = CstrT TType a a'
691 cstr_ [] a@App{} a'@LCon = CstrT TType a a'
692 cstr_ [] a@PMLabel{} a' = CstrT TType a a'
693 cstr_ [] a a'@PMLabel{} = CstrT TType a a'
694 cstr_ [] a a' | isVar a || isVar a' = CstrT TType a a'
695 cstr_ ns a a' = Empty $ unlines [ "can not unify"
696 , ppShow a
697 , "with"
698 , ppShow a'
699 ]
700
701-- unApp (UApp a b) | isInjective a = Just (a, b) -- TODO: injectivity check
702 unApp (Con a xs@(_:_)) = Just (Con a (init xs), last xs)
703 unApp (TyCon a xs@(_:_)) = Just (TyCon a (init xs), last xs)
704 unApp _ = Nothing
705
706 isInjective _ = True--False
707
708 isVar Var{} = True
709 isVar (App a b) = isVar a
710 isVar _ = False
711
712 traceInj2 (a, a') (b, b') c | debug && (susp a || susp b) = trace_ (" inj'? " ++ show a ++ " : " ++ a' ++ " ---- " ++ show b ++ " : " ++ b') c
713 traceInj2 _ _ c = c
714 traceInj (x, y) z a | debug && susp x = trace_ (" inj? " ++ show x ++ " : " ++ y ++ " ---- " ++ show z) a
715 traceInj _ _ a = a
716
717 susp Con{} = False
718 susp TyCon{} = False
719 susp _ = True
720
721 isElemTy n = n `elem` ["'Bool", "'Float", "'Int"]
722 669
723-------------------------------------------------------------------------------- environments 670-------------------------------------------------------------------------------- environments
724 671
@@ -766,24 +713,22 @@ litType = \case
766 LString _ -> TString 713 LString _ -> TString
767 LChar _ -> TChar 714 LChar _ -> TChar
768 715
769expType_ msg te = \case 716class NType a where nType :: a -> Type
770 Lam h t x -> Pi h t $ expType (EBind2 (BLam h) t te) x 717
771 App f x -> appTy (expType te{-todo: precise env-} f) x 718instance NType FunName where nType (FunName _ _ t) = t
772 Var i -> snd $ varType "C" i te 719instance NType ConName where nType (ConName _ _ _ _ t) = t
773 Pi{} -> TType 720instance NType TyConName where nType (TyConName _ _ _ t _ _) = t
774 Label _ x _ -> expType te x 721instance NType CaseFunName where nType (CaseFunName _ t _) = t
775 TFun _ t ts -> foldl appTy t ts 722instance NType TyCaseFunName where nType (TyCaseFunName _ t) = t
776 CaseFun (CaseFunName _ t _) ts -> foldl appTy t ts 723
777 TyCaseFun (TyCaseFunName _ t) ts -> foldl appTy t ts 724neutType te = \case
778 TCon _ _ t ts -> foldl appTy t ts 725 App_ f x -> appTy (neutType te f) x
779 TTyCon _ t ts -> foldl appTy t ts 726 Var_ i -> snd $ varType "C" i te
780 TType -> TType 727 Fun_ s ts -> foldl appTy (nType s) ts
781 ELit l -> litType l 728 CaseFun_ s ts -> foldl appTy (nType s) ts
782 LabelEnd_ k x -> expType te x 729 TyCaseFun_ s ts -> foldl appTy (nType s) ts
783 where
784 expType = expType_ msg
785 730
786appTy (Pi _ a b) x = subst_ "expType_" 0 x b 731appTy (Pi _ a b) x = subst 0 x b
787appTy t x = error $ "appTy: " ++ show t 732appTy t x = error $ "appTy: " ++ show t
788 733
789-------------------------------------------------------------------------------- inference 734-------------------------------------------------------------------------------- inference
@@ -792,11 +737,11 @@ type TCM m = ExceptT String (WriterT Infos m)
792 737
793--runTCM = either error id . runExcept 738--runTCM = either error id . runExcept
794 739
795expAndType (e, t, si) = (e, t) 740expAndType s (e, t, si) = (e, t)
796 741
797-- todo: do only if NoTypeNamespace extension is not on 742-- todo: do only if NoTypeNamespace extension is not on
798lookupName s@('\'':s') m = expAndType <$> (Map.lookup s m `mplus` Map.lookup s' m) 743lookupName s@('\'':s') m = expAndType s <$> (Map.lookup s m `mplus` Map.lookup s' m)
799lookupName s m = expAndType <$> Map.lookup s m 744lookupName s m = expAndType s <$> Map.lookup s m
800--elemIndex' s@('\'':s') m = elemIndex s m `mplus` elemIndex s' m 745--elemIndex' s@('\'':s') m = elemIndex s m `mplus` elemIndex s' m
801--elemIndex' s m = elemIndex s m 746--elemIndex' s m = elemIndex s m
802 747
@@ -832,14 +777,14 @@ inferN tracelevel = infer where
832 checkN_ te e t 777 checkN_ te e t
833 -- temporal hack 778 -- temporal hack
834 | x@(SGlobal (si, MatchName n)) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e 779 | x@(SGlobal (si, MatchName n)) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e
835 = infer te $ x `SAppV` SLam Visible SType (STyped mempty (subst_ "checkN" (v+1) (Var 0) $ up 1 t, TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b 780 = infer te $ x `SAppV` SLam Visible SType (STyped mempty (subst (v+1) (Var 0) $ up 1 t, TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b
836 -- temporal hack 781 -- temporal hack
837 | x@(SGlobal (si, "'NatCase")) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` b `SAppV` SVar siv v <- e 782 | x@(SGlobal (si, "'NatCase")) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` b `SAppV` SVar siv v <- e
838 = infer te $ x `SAppV` STyped mempty (Lam Visible TNat $ subst_ "checkN" (v+1) (Var 0) $ up 1 t, TNat :~> TType) `SAppV` a `SAppV` b `SAppV` SVar siv v 783 = infer te $ x `SAppV` STyped mempty (Lam $ subst (v+1) (Var 0) $ up 1 t, TNat :~> TType) `SAppV` a `SAppV` b `SAppV` SVar siv v
839{- 784{-
840 -- temporal hack 785 -- temporal hack
841 | x@(SGlobal "'VecSCase") `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v <- e 786 | x@(SGlobal "'VecSCase") `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v <- e
842 = infer te $ x `SAppV` (SLamV (SLamV (STyped (subst_ "checkN" (v+1) (Var 0) $ up 2 t, TType)))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v 787 = infer te $ x `SAppV` (SLamV (SLamV (STyped (subst (v+1) (Var 0) $ up 2 t, TType)))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v
843-} 788-}
844 -- temporal hack 789 -- temporal hack
845 | SGlobal (si, "undefined") <- e = focus_' te e (Undef t, t) 790 | SGlobal (si, "undefined") <- e = focus_' te e (Undef t, t)
@@ -848,15 +793,14 @@ inferN tracelevel = infer where
848 | SLam h a b <- e, Pi h' x y <- t, h == h' = do 793 | SLam h a b <- e, Pi h' x y <- t, h == h' = do
849 tellType te e t 794 tellType te e t
850 let same = checkSame te a x 795 let same = checkSame te a x
851 if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ show a ++ "\nwith\n" ++ showEnvExp te x 796 if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ show a ++ "\nwith\n" ++ showEnvExp te (x, TType)
852 | Pi Hidden a b <- t, notHiddenLam e = checkN (EBind2 (BLam Hidden) a te) (upS e) b 797 | Pi Hidden a b <- t, notHiddenLam e = checkN (EBind2 (BLam Hidden) a te) (up1 e) b
853 | otherwise = infer (CheckType_ (sourceInfo e) t te) e 798 | otherwise = infer (CheckType_ (sourceInfo e) t te) e
854 where 799 where
855 -- todo 800 -- todo
856 notHiddenLam = \case 801 notHiddenLam = \case
857 SLam Visible _ _ -> True 802 SLam Visible _ _ -> True
858 SGlobal (si,s) | Lam Hidden _ _ <- fst $ fromMaybe (error $ "infer: can't find: " ++ s) $ lookupName s $ snd $ extractEnv te -> False 803 SGlobal (si,s) | (Lam _, Pi Hidden _ _) <- fromMaybe (error $ "infer: can't find: " ++ s) $ lookupName s $ snd $ extractEnv te -> False
859 -- todo: use type instead of expr.
860 | otherwise -> True 804 | otherwise -> True
861 _ -> False 805 _ -> False
862{- 806{-
@@ -878,11 +822,11 @@ inferN tracelevel = infer where
878 focus_' env si eet = tellType env si (snd eet) >> focus_ env eet 822 focus_' env si eet = tellType env si (snd eet) >> focus_ env eet
879 823
880 focus_ :: Env -> ExpType -> TCM m ExpType' 824 focus_ :: Env -> ExpType -> TCM m ExpType'
881 focus_ env eet@(e, et) = (if tracelevel >= 1 then trace_ $ "focus: " ++ showEnvExp env e else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "focus" env) else id) $ case env of 825 focus_ env eet@(e, et) = (if tracelevel >= 1 then trace_ $ "focus: " ++ showEnvExp env eet else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "focus" env) else id) $ case env of
882 ELabelEnd te -> focus_ te (LabelEnd e, et) 826 ELabelEnd te -> focus_ te (LabelEnd e, et)
883-- CheckSame x te -> focus_ (EBind2_ (debugSI "focus_ CheckSame") BMeta (cstr x e) te) $ up 1 eet 827-- CheckSame x te -> focus_ (EBind2_ (debugSI "focus_ CheckSame") BMeta (cstr x e) te) $ up 1 eet
884 CheckAppType si h t te b -- App1 h (CheckType t te) b 828 CheckAppType si h t te b -- App1 h (CheckType t te) b
885 | Pi h' x (downE 0 -> Just y) <- et, h == h' -> case t of 829 | Pi h' x (down 0 -> Just y) <- et, h == h' -> case t of
886 Pi Hidden t1 t2 | h == Visible -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet -- <<e>> b : {t1} -> {t2} 830 Pi Hidden t1 t2 | h == Visible -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet -- <<e>> b : {t1} -> {t2}
887 _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr t y) $ EApp1 si h te b) $ up 1 eet 831 _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr t y) $ EApp1 si h te b) $ up 1 eet
888 | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet 832 | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet
@@ -891,10 +835,10 @@ inferN tracelevel = infer where
891 | Pi Hidden x y <- et, h == Visible -> focus_ (EApp1 mempty Hidden env $ Wildcard $ Wildcard SType) eet -- e b --> e _ b 835 | Pi Hidden x y <- et, h == Visible -> focus_ (EApp1 mempty Hidden env $ Wildcard $ Wildcard SType) eet -- e b --> e _ b
892-- | CheckType (Pi Hidden _ _) te' <- te -> error "ok" 836-- | CheckType (Pi Hidden _ _) te' <- te -> error "ok"
893-- | CheckAppType Hidden _ te' _ <- te -> error "ok" 837-- | CheckAppType Hidden _ te' _ <- te -> error "ok"
894 | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (upS__ 0 3 b) 838 | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b)
895 where 839 where
896 cstr' h x y e = EApp2 mempty h (eval (error "cstr'") $ Coe (up 1 x) (up 1 y) (Var 0) (up 1 e), up 1 y) . EBind2_ (sourceInfo b) BMeta (cstr x y) 840 cstr' h x y e = EApp2 mempty h (eval $ Coe (up 1 x) (up 1 y) (Var 0) (up 1 e), up 1 y) . EBind2_ (sourceInfo b) BMeta (cstr x y)
897 ELet2 le (x{-let-}, xt) te -> focus_ te $ subst_ "app2" 0 (mkELet le x xt){-let-} eet{-in-} 841 ELet2 le (x{-let-}, xt) te -> focus_ te $ subst 0 (mkELet le x xt){-let-} eet{-in-}
898 CheckIType x te -> checkN te x e 842 CheckIType x te -> checkN te x e
899 CheckType_ si t te 843 CheckType_ si t te
900 | hArgs et > hArgs t 844 | hArgs et > hArgs t
@@ -912,24 +856,24 @@ inferN tracelevel = infer where
912 focus2 env eet = case env of 856 focus2 env eet = case env of
913 ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-} 857 ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-}
914 EBind2_ si BMeta tt te 858 EBind2_ si BMeta tt te
915 | Unit <- tt -> refocus te $ subst te 0 TT eet 859 | Unit <- tt -> refocus te $ subst 0 TT eet
916 | Empty msg <- tt -> throwError $ "type error: " ++ msg ++ "\nin " ++ showSI te si ++ "\n"-- todo: better error msg 860 | Empty msg <- tt -> throwError $ "type error: " ++ msg ++ "\nin " ++ showSI te si ++ "\n"-- todo: better error msg
917 | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te 861 | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te
918 -> refocus te' $ subst te' 2 (t2C (Var 1) (Var 0)) $ up 2 eet 862 -> refocus te' $ subst 2 (eval $ T2C (Var 1) (Var 0)) $ up 2 eet
919 | CstrT t a b <- tt, a == b -> refocus te $ subst_ "inferN2" 0 TT eet 863 | CstrT t a b <- tt, a == b -> refocus te $ subst 0 TT eet
920 | CstrT t a b <- tt, Just r <- cst (a, t) b -> r 864 | CstrT t a b <- tt, Just r <- cst (a, t) b -> r
921 | CstrT t a b <- tt, Just r <- cst (b, t) a -> r 865 | CstrT t a b <- tt, Just r <- cst (b, t) a -> r
922 | isCstr tt, EBind2 h x te' <- te{-, h /= BMeta todo: remove-}, Just x' <- downE 0 tt, x == x' 866 | isCstr tt, EBind2 h x te' <- te{-, h /= BMeta todo: remove-}, Just x' <- down 0 tt, x == x'
923 -> refocus te $ subst_ "inferN3" 1 (Var 0) eet 867 -> refocus te $ subst 1 (Var 0) eet
924 | EBind2 h x te' <- te, h /= BMeta, Just b' <- downE 0 tt 868 | EBind2 h x te' <- te, h /= BMeta, Just b' <- down 0 tt
925 -> refocus (EBind2_ si h (up 1 x) $ EBind2_ si BMeta b' te') $ subst_ "inferN3" 2 (Var 0) $ up 1 eet 869 -> refocus (EBind2_ si h (up 1 x) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet
926 | ELet2 le (x, xt) te' <- te, Just b' <- downE 0 tt 870 | ELet2 le (x, xt) te' <- te, Just b' <- down 0 tt
927 -> refocus (ELet2 le (up 1 x, up 1 xt) $ EBind2_ si BMeta b' te') $ subst_ "inferN32" 2 (Var 0) $ up 1 eet 871 -> refocus (ELet2 le (up 1 x, up 1 xt) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet
928 | EBind1 si h te' x <- te -> refocus (EBind1 si h (EBind2_ si BMeta tt te') $ upS__ 1 1 x) eet 872 | EBind1 si h te' x <- te -> refocus (EBind1 si h (EBind2_ si BMeta tt te') $ up1_ 1 x) eet
929 | ELet1 le te' x <- te, floatLetMeta $ snd $ replaceMetas' $ Meta tt $ eet 873 | ELet1 le te' x <- te, floatLetMeta $ snd $ replaceMetas' $ Meta tt $ eet
930 -> refocus (ELet1 le (EBind2_ si BMeta tt te') $ upS__ 1 1 x) eet 874 -> refocus (ELet1 le (EBind2_ si BMeta tt te') $ up1_ 1 x) eet
931 | CheckAppType si h t te' x <- te -> refocus (CheckAppType si h (up 1 t) (EBind2_ si BMeta tt te') $ upS x) eet 875 | CheckAppType si h t te' x <- te -> refocus (CheckAppType si h (up 1 t) (EBind2_ si BMeta tt te') $ up1 x) eet
932 | EApp1 si h te' x <- te -> refocus (EApp1 si h (EBind2_ si BMeta tt te') $ upS x) eet 876 | EApp1 si h te' x <- te -> refocus (EApp1 si h (EBind2_ si BMeta tt te') $ up1 x) eet
933 | EApp2 si h x te' <- te -> refocus (EApp2 si h (up 1 x) $ EBind2_ si BMeta tt te') eet 877 | EApp2 si h x te' <- te -> refocus (EApp2 si h (up 1 x) $ EBind2_ si BMeta tt te') eet
934 | CheckType_ si t te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt te') eet 878 | CheckType_ si t te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt te') eet
935-- | CheckIType x te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt te') eet 879-- | CheckIType x te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt te') eet
@@ -940,24 +884,24 @@ inferN tracelevel = infer where
940 cst :: ExpType -> Exp -> Maybe (TCM m ExpType') 884 cst :: ExpType -> Exp -> Maybe (TCM m ExpType')
941 cst x = \case 885 cst x = \case
942 Var i | fst (varType "X" i te) == BMeta 886 Var i | fst (varType "X" i te) == BMeta
943 , Just y <- downE i x 887 , Just y <- down i x
944 -> Just $ join swapAssign (\i x -> refocus $ EAssign i x te) i y $ subst te 0 {-ReflCstr y-}TT $ subst te (i+1) (fst $ up 1 y) eet 888 -> Just $ join swapAssign (\i x -> refocus $ EAssign i x te) i y $ subst 0 {-ReflCstr y-}TT $ subst (i+1) (fst $ up 1 y) eet
945 _ -> Nothing 889 _ -> Nothing
946 890
947 EAssign i b te -> case te of 891 EAssign i b te -> case te of
948 EBind2_ si h x te' | i > 0, Just b' <- downE 0 b 892 EBind2_ si h x te' | i > 0, Just b' <- down 0 b
949 -> refocus' (EBind2_ si h (subst_ "inferN5" (i-1) (fst b') x) (EAssign (i-1) b' te')) eet 893 -> refocus' (EBind2_ si h (subst (i-1) (fst b') x) (EAssign (i-1) b' te')) eet
950 ELet2 le (x, xt) te' | i > 0, Just b' <- downE 0 b 894 ELet2 le (x, xt) te' | i > 0, Just b' <- down 0 b
951 -> refocus' (ELet2 le (subst_ "inferN51" (i-1) (fst b') x, subst_ "inferN52" (i-1) (fst b') xt) (EAssign (i-1) b' te')) eet 895 -> refocus' (ELet2 le (subst (i-1) (fst b') x, subst (i-1) (fst b') xt) (EAssign (i-1) b' te')) eet
952 ELet1 le te' x -> refocus' (ELet1 le (EAssign i b te') $ substS (i+1) (fst $ up 1 b) x) eet 896 ELet1 le te' x -> refocus' (ELet1 le (EAssign i b te') $ substS (i+1) (up 1 b) x) eet
953 EBind1 si h te' x -> refocus' (EBind1 si h (EAssign i b te') $ substS (i+1) (fst $ up 1 b) x) eet 897 EBind1 si h te' x -> refocus' (EBind1 si h (EAssign i b te') $ substS (i+1) (up 1 b) x) eet
954 CheckAppType si h t te' x -> refocus' (CheckAppType si h (subst_ "inferN6" i (fst b) t) (EAssign i b te') $ substS i (fst b) x) eet 898 CheckAppType si h t te' x -> refocus' (CheckAppType si h (subst i (fst b) t) (EAssign i b te') $ substS i b x) eet
955 EApp1 si h te' x -> refocus' (EApp1 si h (EAssign i b te') $ substS i (fst b) x) eet 899 EApp1 si h te' x -> refocus' (EApp1 si h (EAssign i b te') $ substS i b x) eet
956 EApp2 si h x te' -> refocus' (EApp2 si h (subst te'{-todo: precise env-} i (fst b) x) $ EAssign i b te') eet 900 EApp2 si h x te' -> refocus' (EApp2 si h (subst i (fst b) x) $ EAssign i b te') eet
957 CheckType_ si t te' -> refocus' (CheckType_ si (subst_ "inferN8" i (fst b) t) $ EAssign i b te') eet 901 CheckType_ si t te' -> refocus' (CheckType_ si (subst i (fst b) t) $ EAssign i b te') eet
958 ELabelEnd te' -> refocus' (ELabelEnd $ EAssign i b te') eet 902 ELabelEnd te' -> refocus' (ELabelEnd $ EAssign i b te') eet
959 EAssign j a te' | i < j 903 EAssign j a te' | i < j
960 -> refocus' (EAssign (j-1) (subst_ "ea" i (fst b) a) $ EAssign i (up1_ (j-1) b) te') eet 904 -> refocus' (EAssign (j-1) (subst i (fst b) a) $ EAssign i (up1_ (j-1) b) te') eet
961 t | Just te' <- pull i te -> refocus' te' eet 905 t | Just te' <- pull i te -> refocus' te' eet
962 | otherwise -> swapAssign (\i x -> focus2 te . Assign i x) (\i x -> refocus' $ EAssign i x te) i b eet 906 | otherwise -> swapAssign (\i x -> focus2 te . Assign i x) (\i x -> refocus' $ EAssign i x te) i b eet
963 -- todo: CheckSame Exp Env 907 -- todo: CheckSame Exp Env
@@ -965,8 +909,8 @@ inferN tracelevel = infer where
965 refocus' = fix refocus_ 909 refocus' = fix refocus_
966 pull i = \case 910 pull i = \case
967 EBind2 BMeta _ te | i == 0 -> Just te 911 EBind2 BMeta _ te | i == 0 -> Just te
968 EBind2_ si h x te -> EBind2_ si h <$> downE (i-1) x <*> pull (i-1) te 912 EBind2_ si h x te -> EBind2_ si h <$> down (i-1) x <*> pull (i-1) te
969 EAssign j b te -> EAssign (if j <= i then j else j-1) <$> downE i b <*> pull (if j <= i then i+1 else i) te 913 EAssign j b te -> EAssign (if j <= i then j else j-1) <$> down i b <*> pull (if j <= i then i+1 else i) te
970 _ -> Nothing 914 _ -> Nothing
971 915
972 EGlobal{} -> return eet 916 EGlobal{} -> return eet
@@ -981,11 +925,11 @@ inferN tracelevel = infer where
981 925
982 replaceMetas' = replaceMetas $ lamPi Hidden 926 replaceMetas' = replaceMetas $ lamPi Hidden
983 927
984lamPi h = (***) <$> Lam h <*> Pi h 928lamPi h = (***) <$> (\a b -> Lam b) <*> Pi h
985 929
986replaceMetas bind = \case 930replaceMetas bind = \case
987 Meta a t -> bind a $ replaceMetas bind t 931 Meta a t -> bind a $ replaceMetas bind t
988 Assign i x t | x' <- up1_ i x -> bind (cstrT (snd x') (Var i) $ fst x') . up 1 . up1_ i $ replaceMetas bind t 932 Assign i x t | x' <- up1_ i x -> bind (eval $ CstrT (snd x') (Var i) $ fst x') . up 1 . up1_ i $ replaceMetas bind t
989 MEnd t -> t 933 MEnd t -> t
990 934
991 935
@@ -1000,65 +944,46 @@ type Message = String
1000recheck :: Message -> Env -> ExpType -> ExpType 944recheck :: Message -> Env -> ExpType -> ExpType
1001recheck msg e = recheck' msg e 945recheck msg e = recheck' msg e
1002 946
947-- todo: check type also
1003recheck' :: Message -> Env -> ExpType -> ExpType 948recheck' :: Message -> Env -> ExpType -> ExpType
1004recheck' msg' e (x, xt) = (e', xt {-todo-}) 949recheck' msg' e (x, xt) = (recheck_ "main" (checkEnv e) (x, xt), xt)
1005 where 950 where
1006 e' = recheck_ "main" (checkEnv e) x
1007 checkEnv = \case 951 checkEnv = \case
1008 e@EGlobal{} -> e 952 e@EGlobal{} -> e
1009 EBind1 si h e b -> EBind1 si h (checkEnv e) b 953 EBind1 si h e b -> EBind1 si h (checkEnv e) b
1010 EBind2_ si h t e -> EBind2_ si h (recheckEnv e t) $ checkEnv e -- E [\(x :: t) -> e] -> check E [t] 954 EBind2_ si h t e -> EBind2_ si h (checkType e t) $ checkEnv e -- E [\(x :: t) -> e] -> check E [t]
1011 ELet1 le e b -> ELet1 le (checkEnv e) b 955 ELet1 le e b -> ELet1 le (checkEnv e) b
1012 ELet2 le (x, t) e -> ELet2 le (recheckEnv e x, recheckEnv e t{-?-}) $ checkEnv e 956 ELet2 le x e -> ELet2 le (recheck'' "env" e x) $ checkEnv e
1013 EApp1 si h e b -> EApp1 si h (checkEnv e) b 957 EApp1 si h e b -> EApp1 si h (checkEnv e) b
1014 EApp2 si h (a, at) e -> EApp2 si h (recheckEnv {-(EApp1 h e _)-}e a, at) $ checkEnv e -- E [a x] -> check 958 EApp2 si h a e -> EApp2 si h (recheck'' "env" e a) $ checkEnv e -- E [a x] -> check
1015 EAssign i (x, xt) e -> EAssign i (recheckEnv e $ up1_ i x, xt) $ checkEnv e -- __ <i := x> 959 EAssign i x e -> EAssign i (recheck'' "env" e $ up1_ i x) $ checkEnv e -- __ <i := x>
1016 CheckType_ si x e -> CheckType_ si (recheckEnv e x) $ checkEnv e 960 CheckType_ si x e -> CheckType_ si (checkType e x) $ checkEnv e
1017-- CheckSame x e -> CheckSame (recheckEnv e x) $ checkEnv e 961-- CheckSame x e -> CheckSame (recheck'' "env" e x) $ checkEnv e
1018 CheckAppType si h x e y -> CheckAppType si h (recheckEnv e x) (checkEnv e) y 962 CheckAppType si h x e y -> CheckAppType si h (checkType e x) (checkEnv e) y
1019 963
1020 recheckEnv = recheck_ "env" 964 recheck'' msg te a@(x, xt) = (recheck_ msg te a, xt)
965 checkType te e = recheck_ "check" te (e, TType)
1021 966
1022 recheck_ msg te = \case 967 recheck_ msg te = \case
1023 Var k -> Var k 968 (Var k, zt) -> Var k -- todo: check var type
1024 Lam h a b -> Lam h (ch True te{-ok?-} a) $ ch False (EBind2 (BLam h) a te) b 969 (Lam b, Pi h a bt) -> Lam $ recheck_ "9" (EBind2 (BLam h) a te) (b, bt)
1025 Pi h a b -> Pi h (ch True te{-ok?-} a) $ ch True (EBind2 (BPi h) a te) b 970 (Pi h a b, TType) -> Pi h (checkType te a) $ checkType (EBind2 (BPi h) a te) b
1026 App a b -> appf (recheck'' "app1" te{-ok?-} a) (recheck'' "app2" (EApp2 mempty Visible (a, expType_ "7" te a) te) b) 971 (ELit l, zt) -> ELit l -- todo: check literal type
1027 Label lk z x -> Label lk (recheck_ msg te z) x 972 (TType, TType) -> TType
1028 ELit l -> ELit l 973 (Neut (App_ a b), zt)
1029 TType -> TType 974 | (Neut a', at) <- recheck'' "app1" te (Neut a, neutType te a)
1030 Con s [] -> Con s [] 975 -> checkApps [] zt (Neut . App_ a' . head) te at [b]
1031 Con s as -> reApp $ recheck_ "prim" te $ foldl App (Con s []) as 976 (Con s n as, zt) -> checkApps [] zt (Con s n . drop (conParams s)) te (nType s) $ mkConPars n zt ++ as
1032 TyCon s [] -> TyCon s [] 977 (TyCon s as, zt) -> checkApps [] zt (TyCon s) te (nType s) as
1033 TyCon s as -> reApp $ recheck_ "prim" te $ foldl App (TyCon s []) as 978 (Fun s as, zt) -> checkApps [] zt (Fun s) te (nType s) as
1034 CaseFun s [] -> CaseFun s [] 979 (CaseFun s as, zt) -> checkApps [] zt (CaseFun s) te (nType s) as
1035 CaseFun s as -> reApp $ recheck_ "fun" te $ foldl App (CaseFun s []) as 980 (TyCaseFun s as, zt) -> checkApps [] zt (TyCaseFun s) te (nType s) as
1036 TyCaseFun s [] -> TyCaseFun s [] 981 (Label lk a x, zt) -> Label lk (recheck_ msg te (a, zt)) x
1037 TyCaseFun s as -> reApp $ recheck_ "tycfun" te $ foldl App (TyCaseFun s []) as 982 (LabelEnd_ k x, zt) -> LabelEnd_ k $ recheck_ msg te (x, zt)
1038 Fun s [] -> Fun s []
1039 Fun s as -> reApp $ recheck_ "fun" te $ foldl App (Fun s []) as
1040 LabelEnd_ k x -> LabelEnd_ k $ recheck_ msg te x
1041 where 983 where
1042 reApp (App f x) = case reApp f of 984 checkApps acc zt f _ t [] | t == zt = f $ reverse acc
1043 Fun s args -> Fun s $ args ++ [x] 985 checkApps acc zt f te t@(Pi h x y) (b_: xs) = checkApps (b: acc) zt f te (appTy t b) xs where b = recheck_ "checkApps" te (b_, x)
1044 CaseFun s args -> CaseFun s $ args ++ [x] 986 checkApps acc zt f te t _ = error_ $ "checkApps " ++ msg ++ "\n" ++ showEnvExp te{-todo-} (t, TType) ++ "\n\n" ++ showEnvExp e (x, xt)
1045 TyCaseFun s args -> TyCaseFun s $ args ++ [x]
1046 Con s args -> Con s $ args ++ [x]
1047 TyCon s args -> TyCon s $ args ++ [x]
1048 reApp x = x
1049
1050 appf at@(a, Pi h x y) (b, x')
1051 | x == x' = app_ a b
1052 | otherwise = error_ $ "recheck " ++ msg' ++ "; " ++ msg ++ "\nexpected: " ++ showEnvExp te{-todo-} x ++ "\nfound: " ++ showEnvExp te{-todo-} x' ++ "\nin term: " ++ showEnvExp (EApp2 mempty h at te) b ++ "\n" ++ ppShow y
1053 appf (a, t) (b, x')
1054 = error_ $ "recheck " ++ msg' ++ "; " ++ msg ++ "\nnot a pi type: " ++ showEnvExp te{-todo-} t ++ "\n\n" ++ showEnvExp e x
1055
1056 recheck'' msg te a = (b, expType_ "4" te b) where b = recheck_ msg te a
1057
1058 ch False te e = recheck_ "ch" te e
1059 ch True te e = case recheck'' "check" te e of
1060 (e', TType) -> e'
1061 _ -> error_ $ "recheck'':\n" ++ showEnvExp te e
1062 987
1063-- Ambiguous: (Int ~ F a) => Int 988-- Ambiguous: (Int ~ F a) => Int
1064-- Not ambiguous: (Show a, a ~ F b) => b 989-- Not ambiguous: (Show a, a ~ F b) => b
@@ -1068,7 +993,7 @@ ambiguityCheck s ty = case ambigVars ty of
1068 err -> Just $ s ++ " has ambiguous type:\n" ++ ppShow ty ++ "\nproblematic vars:\n" ++ show err 993 err -> Just $ s ++ " has ambiguous type:\n" ++ ppShow ty ++ "\nproblematic vars:\n" ++ show err
1069 994
1070ambigVars :: Exp -> [(Int, Exp)] 995ambigVars :: Exp -> [(Int, Exp)]
1071ambigVars ty = [(n, c) | (n, c) <- hid, not $ any (`Set.member` defined) $ Set.insert n $ freeE c] 996ambigVars ty = [(n, c) | (n, c) <- hid, not $ any (`Set.member` defined) $ Set.insert n $ free c]
1072 where 997 where
1073 (defined, hid, i) = compDefined False ty 998 (defined, hid, i) = compDefined False ty
1074 999
@@ -1079,7 +1004,7 @@ floatLetMeta ty = (i-1) `Set.member` defined
1079 1004
1080compDefined b ty = (defined, hid, i) 1005compDefined b ty = (defined, hid, i)
1081 where 1006 where
1082 defined = dependentVars hid $ Set.map (if b then (+i) else id) $ freeE ty 1007 defined = dependentVars hid $ Set.map (if b then (+i) else id) $ free ty
1083 1008
1084 i = length hid_ 1009 i = length hid_
1085 hid = zipWith (\k t -> (k, up (k+1) t)) (reverse [0..i-1]) hid_ 1010 hid = zipWith (\k t -> (k, up (k+1) t)) (reverse [0..i-1]) hid_
@@ -1093,7 +1018,7 @@ hiddenVars t = ([], t)
1093dependentVars :: [(Int, Exp)] -> Set.Set Int -> Set.Set Int 1018dependentVars :: [(Int, Exp)] -> Set.Set Int -> Set.Set Int
1094dependentVars ie = cycle mempty 1019dependentVars ie = cycle mempty
1095 where 1020 where
1096 freeVars = freeE 1021 freeVars = free
1097 1022
1098 cycle acc s 1023 cycle acc s
1099 | Set.null s = acc 1024 | Set.null s = acc
@@ -1128,22 +1053,22 @@ extractDesugarInfo :: GlobalEnv -> DesugarInfo
1128extractDesugarInfo ge = 1053extractDesugarInfo ge =
1129 ( Map.fromList 1054 ( Map.fromList
1130 [ (n, f) | (n, (d, _, si)) <- Map.toList ge, f <- maybeToList $ case UL' d of 1055 [ (n, f) | (n, (d, _, si)) <- Map.toList ge, f <- maybeToList $ case UL' d of
1131 Con (ConName _ f _ _) [] -> f 1056 Con (ConName _ f _ _ _) 0 [] -> f
1132 TyCon (TyConName _ f _ _ _ _) [] -> f 1057 TyCon (TyConName _ f _ _ _ _) [] -> f
1133 (snd . getLams -> UL (snd . getLams -> Fun (FunName _ f _) _)) -> f 1058 (getLams -> UL (getLams -> Fun (FunName _ f _) _)) -> f
1134 Fun (FunName _ f _) [] -> f 1059 Fun (FunName _ f _) [] -> f
1135 _ -> Nothing 1060 _ -> Nothing
1136 ] 1061 ]
1137 , Map.fromList $ 1062 , Map.fromList $
1138 [ (n, Left ((t, inum), map f cons)) 1063 [ (n, Left ((t, inum), map f cons))
1139 | (n, (UL' (Con cn []), _, si)) <- Map.toList ge, let TyConName t _ inum _ cons _ = conTypeName cn 1064 | (n, (UL' (Con cn 0 []), _, si)) <- Map.toList ge, let TyConName t _ inum _ cons _ = conTypeName cn
1140 ] ++ 1065 ] ++
1141 [ (n, Right $ pars t) 1066 [ (n, Right $ pars t)
1142 | (n, (UL' (TyCon (TyConName _ f _ t _ _) []), _, _)) <- Map.toList ge 1067 | (n, (UL' (TyCon (TyConName _ f _ t _ _) []), _, _)) <- Map.toList ge
1143 ] 1068 ]
1144 ) 1069 )
1145 where 1070 where
1146 f (ConName n _ _ ct) = (n, pars ct) 1071 f (ConName n _ _ _ ct) = (n, pars ct)
1147 pars = length . filter ((==Visible) . fst) . fst . getParams 1072 pars = length . filter ((==Visible) . fst) . fst . getParams
1148 1073
1149-------------------------------------------------------------------------------- infos 1074-------------------------------------------------------------------------------- infos
@@ -1164,19 +1089,19 @@ listInfos (Infos m) = [(r, Set.toList i) | (r, i) <- Map.toList m]
1164 1089
1165handleStmt :: MonadFix m => [Stmt] -> Stmt -> ElabStmtM m () 1090handleStmt :: MonadFix m => [Stmt] -> Stmt -> ElabStmtM m ()
1166handleStmt defs = \case 1091handleStmt defs = \case
1167 Primitive n mf (trSExp -> t_) -> do 1092 Primitive n mf (trSExp' -> t_) -> do
1168 t <- inferType tr =<< ($ t_) <$> addF 1093 t <- inferType tr =<< ($ t_) <$> addF
1169 tellStmtType (fst n) t 1094 tellStmtType (fst n) t
1170 addToEnv n $ flip (,) t $ lamify t $ Fun (FunName (snd n) mf t) 1095 addToEnv n $ flip (,) t $ lamify t $ Fun (FunName (snd n) mf t)
1171 Let n mf mt ar t_ -> do 1096 Let n mf mt ar t_ -> do
1172 af <- addF 1097 af <- addF
1173 let t__ = maybe id (flip SAnn . af) mt t_ 1098 let t__ = maybe id (flip SAnn . af) mt t_
1174 (x, t) <- inferTerm (snd n) tr id $ trSExp $ fromMaybe (SBuiltin "primFix" `SAppV` SLamV t__) $ downS 0 t__ 1099 (x, t) <- inferTerm (snd n) tr id $ trSExp' $ fromMaybe (SBuiltin "primFix" `SAppV` SLamV t__) $ downS 0 t__
1175 tellStmtType (fst n) t 1100 tellStmtType (fst n) t
1176 addToEnv n (mkELet (True, n, SData mf, ar) x t, t) 1101 addToEnv n (mkELet (True, n, SData mf, ar) x t, t)
1177 PrecDef{} -> return () 1102 PrecDef{} -> return ()
1178 TypeFamily s ps t -> handleStmt defs $ Primitive s Nothing $ addParamsS ps t 1103 TypeFamily s ps t -> handleStmt defs $ Primitive s Nothing $ addParamsS ps t
1179 Data s (map (second trSExp) -> ps) (trSExp -> t_) addfa (map (second trSExp) -> cs) -> do 1104 Data s (map (second trSExp') -> ps) (trSExp' -> t_) addfa (map (second trSExp') -> cs) -> do
1180 exs <- asks fst 1105 exs <- asks fst
1181 af <- if addfa then gets $ addForalls exs . (snd s:) . defined' else return id 1106 af <- if addfa then gets $ addForalls exs . (snd s:) . defined' else return id
1182 vty <- inferType tr $ addParamsS ps t_ 1107 vty <- inferType tr $ addParamsS ps t_
@@ -1193,8 +1118,8 @@ handleStmt defs = \case
1193 let pars = zipWith (\x -> second $ STyped (debugSI "mkConstr1") . flip (,) TType . up_ (1+j) x) [0..] $ drop (length ps) $ fst $ getParams cty 1118 let pars = zipWith (\x -> second $ STyped (debugSI "mkConstr1") . flip (,) TType . up_ (1+j) x) [0..] $ drop (length ps) $ fst $ getParams cty
1194 act = length . fst . getParams $ cty 1119 act = length . fst . getParams $ cty
1195 acts = map fst . fst . getParams $ cty 1120 acts = map fst . fst . getParams $ cty
1196 conn = ConName (snd cn) (listToMaybe [f | PrecDef n f <- defs, n == cn]) j cty 1121 conn = conName (snd cn) (listToMaybe [f | PrecDef n f <- defs, n == cn]) j cty
1197 addToEnv cn (Con conn [], cty) 1122 addToEnv cn (Con conn 0 [], cty)
1198 return ( conn 1123 return ( conn
1199 , addParamsS pars 1124 , addParamsS pars
1200 $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (SGlobal cn) (zip acts $ downToS (j+1+length pars) (length ps) ++ downToS 0 (act- length ps))] 1125 $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (SGlobal cn) (zip acts $ downToS (j+1+length pars) (length ps) ++ downToS 0 (act- length ps))]
@@ -1207,7 +1132,8 @@ handleStmt defs = \case
1207 SPi Visible (apps' (SGlobal s) $ zip (map fst ps) (downToS inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum)) SType 1132 SPi Visible (apps' (SGlobal s) $ zip (map fst ps) (downToS inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum)) SType
1208 1133
1209 mdo 1134 mdo
1210 let tcn = TyConName (snd s) Nothing inum vty (map fst cons) ct 1135 let tcn = TyConName (snd s) Nothing inum vty (map fst cons) cfn
1136 let cfn = CaseFunName (snd s) ct $ length ps
1211 addToEnv s (TyCon tcn [], vty) 1137 addToEnv s (TyCon tcn [], vty)
1212 cons <- zipWithM mkConstr [0..] cs 1138 cons <- zipWithM mkConstr [0..] cs
1213 ct <- inferType tr 1139 ct <- inferType tr
@@ -1220,7 +1146,7 @@ handleStmt defs = \case
1220 ) 1146 )
1221 $ foldl SAppV (SVar (debugSI "23", ".ct") $ length cs + inum + 1) $ downToS 1 inum ++ [SVar (debugSI "24", ".24") 0] 1147 $ foldl SAppV (SVar (debugSI "23", ".ct") $ length cs + inum + 1) $ downToS 1 inum ++ [SVar (debugSI "24", ".24") 0]
1222 ) 1148 )
1223 addToEnv (fst s, caseName (snd s)) (lamify ct $ CaseFun (CaseFunName (snd s) ct $ length ps), ct) 1149 addToEnv (fst s, caseName (snd s)) (lamify ct $ CaseFun cfn, ct)
1224 let ps' = fst $ getParams vty 1150 let ps' = fst $ getParams vty
1225 t = (TType :~> TType) 1151 t = (TType :~> TType)
1226 :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps')) 1152 :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps'))
@@ -1237,23 +1163,23 @@ mkELet (True, n, SData mf, ar) x t{-type of x-} = term
1237 term = label LabelPM (addLams' ar t 0) $ par ar t x 0 1163 term = label LabelPM (addLams' ar t 0) $ par ar t x 0
1238 1164
1239 addLams' [] _ i = Fun (FunName (snd n) mf t) $ downTo 0 i 1165 addLams' [] _ i = Fun (FunName (snd n) mf t) $ downTo 0 i
1240 addLams' (h: ar) (Pi h' d t) i | h == h' = Lam h d $ addLams' ar t (i+1) 1166 addLams' (h: ar) (Pi h' d t) i | h == h' = Lam $ addLams' ar t (i+1)
1241 addLams' ar@(Visible: _) (Pi h@Hidden d t) i = Lam h d $ addLams' ar t (i+1) 1167 addLams' ar@(Visible: _) (Pi h@Hidden d t) i = Lam $ addLams' ar t (i+1)
1242 1168
1243 par ar tt (FunN "primFix" [_, f]) i = f `app_` label LabelFix (addLams' ar tt i) (foldl app_ term $ downTo 0 i) 1169 par ar tt (FunN "primFix" [_, f]) i = f `app_` label LabelFix (addLams' ar tt i) (foldl app_ term $ downTo 0 i)
1244 par ar (Pi Hidden _ tt) (Lam Hidden k z) i = Lam Hidden k $ par (dropHidden ar) tt z (i+1) 1170 par ar (Pi Hidden k tt) (Lam z) i = Lam $ par (dropHidden ar) tt z (i+1)
1245 where 1171 where
1246 dropHidden (Hidden: ar) = ar 1172 dropHidden (Hidden: ar) = ar
1247 dropHidden ar = ar 1173 dropHidden ar = ar
1248 par ar t x _ = x 1174 par ar t x _ = x
1249 1175
1250removeHiddenUnit (Pi Hidden Unit (downE 0 -> Just t)) = removeHiddenUnit t 1176removeHiddenUnit (Pi Hidden Unit (down 0 -> Just t)) = removeHiddenUnit t
1251removeHiddenUnit (Pi h a b) = Pi h a $ removeHiddenUnit b 1177removeHiddenUnit (Pi h a b) = Pi h a $ removeHiddenUnit b
1252removeHiddenUnit t = t 1178removeHiddenUnit t = t
1253 1179
1254addParams ps t = foldr (uncurry Pi) t ps 1180addParams ps t = foldr (uncurry Pi) t ps
1255 1181
1256addLams ps t = foldr (uncurry Lam) t ps 1182addLams ps t = foldr (uncurry $ \h a b -> Lam b) t ps
1257 1183
1258lamify t x = addLams (fst $ getParams t) $ x $ downTo 0 $ arity t 1184lamify t x = addLams (fst $ getParams t) $ x $ downTo 0 $ arity t
1259 1185
@@ -1269,8 +1195,8 @@ getParams :: Exp -> ([(Visibility, Exp)], Exp)
1269getParams (UL' (Pi h a b)) = first ((h, a):) $ getParams b 1195getParams (UL' (Pi h a b)) = first ((h, a):) $ getParams b
1270getParams x = ([], x) 1196getParams x = ([], x)
1271 1197
1272getLams (Lam h a b) = first ((h, a):) $ getLams b 1198getLams (Lam b) = getLams b
1273getLams x = ([], x) 1199getLams x = x
1274 1200
1275getGEnv f = do 1201getGEnv f = do
1276 (exs, src) <- ask 1202 (exs, src) <- ask
@@ -1295,7 +1221,7 @@ defined' = Map.keys
1295 1221
1296addF = asks fst >>= \exs -> gets $ addForalls exs . defined' 1222addF = asks fst >>= \exs -> gets $ addForalls exs . defined'
1297 1223
1298tellType te si t = tell $ mkInfoItem (sourceInfo si) $ removeEscs $ showDoc $ expDoc_ True t 1224tellType te si t = tell $ mkInfoItem (sourceInfo si) $ removeEscs $ showDoc $ mkDoc True (t, TType)
1299tellStmtType si t = getGEnv $ \te -> tellType te si t 1225tellStmtType si t = getGEnv $ \te -> tellType te si t
1300 1226
1301 1227
@@ -1318,22 +1244,22 @@ joinPolyEnvs _ = return . foldr mappend' mempty' -- todo
1318-- todo: do this via conversion to SExp 1244-- todo: do this via conversion to SExp
1319 1245
1320instance PShow Exp where 1246instance PShow Exp where
1321 pShowPrec _ = showDoc_ . expDoc 1247 pShowPrec _ = showDoc_ . mkDoc False
1322 1248
1323instance PShow (CEnv Exp) where 1249instance PShow (CEnv Exp) where
1324 pShowPrec _ = showDoc_ . mExpDoc 1250 pShowPrec _ = showDoc_ . mkDoc False
1325 1251
1326instance PShow Env where 1252instance PShow Env where
1327 pShowPrec _ e = showDoc_ $ envDoc e $ pure $ shAtom $ underlined "<<HERE>>" 1253 pShowPrec _ e = showDoc_ $ envDoc e $ pure $ shAtom $ underlined "<<HERE>>"
1328 1254
1329showEnvExp :: Env -> Exp -> String 1255showEnvExp :: Env -> ExpType -> String
1330showEnvExp e c = showDoc $ envDoc e $ epar <$> expDoc c 1256showEnvExp e c = showDoc $ envDoc e $ epar <$> mkDoc False c
1331 1257
1332showEnvSExp :: Env -> SExp' a -> String 1258showEnvSExp :: Up a => Env -> SExp' a -> String
1333showEnvSExp e c = showDoc $ envDoc e $ epar <$> sExpDoc c 1259showEnvSExp e c = showDoc $ envDoc e $ epar <$> sExpDoc c
1334 1260
1335showEnvSExpType :: Env -> SExp' a -> Exp -> String 1261showEnvSExpType :: Up a => Env -> SExp' a -> Exp -> String
1336showEnvSExpType e c t = showDoc $ envDoc e $ epar <$> (shAnn "::" False <$> sExpDoc c <**> expDoc t) 1262showEnvSExpType e c t = showDoc $ envDoc e $ epar <$> (shAnn "::" False <$> sExpDoc c <**> mkDoc False (t, TType))
1337 where 1263 where
1338 infixl 4 <**> 1264 infixl 4 <**>
1339 (<**>) :: NameDB (a -> b) -> NameDB a -> NameDB b 1265 (<**>) :: NameDB (a -> b) -> NameDB a -> NameDB b
@@ -1372,51 +1298,68 @@ nameSExp = \case
1372envDoc :: Env -> Doc -> Doc 1298envDoc :: Env -> Doc -> Doc
1373envDoc x m = case x of 1299envDoc x m = case x of
1374 EGlobal{} -> m 1300 EGlobal{} -> m
1375 EBind1 _ h ts b -> envDoc ts $ join $ shLam (usedS 0 b) h <$> m <*> pure (sExpDoc b) 1301 EBind1 _ h ts b -> envDoc ts $ join $ shLam (used 0 b) h <$> m <*> pure (sExpDoc b)
1376 EBind2 h a ts -> envDoc ts $ join $ shLam True h <$> expDoc a <*> pure m 1302 EBind2 h a ts -> envDoc ts $ join $ shLam True h <$> mkDoc ts' (a, TType) <*> pure m
1377 EApp1 _ h ts b -> envDoc ts $ shApp h <$> m <*> sExpDoc b 1303 EApp1 _ h ts b -> envDoc ts $ shApp h <$> m <*> sExpDoc b
1378 EApp2 _ h (Lam Visible TType (Var 0), _) ts -> envDoc ts $ shApp h (shAtom "tyType") <$> m 1304 EApp2 _ h (Lam (Var 0), Pi Visible TType _) ts -> envDoc ts $ shApp h (shAtom "tyType") <$> m
1379 EApp2 _ h (a, at) ts -> envDoc ts $ shApp h <$> expDoc a <*> m 1305 EApp2 _ h a ts -> envDoc ts $ shApp h <$> mkDoc ts' a <*> m
1380 ELet1 _ ts b -> envDoc ts $ shLet_ m (sExpDoc b) 1306 ELet1 _ ts b -> envDoc ts $ shLet_ m (sExpDoc b)
1381 ELet2 _ (x, _) ts -> envDoc ts $ shLet_ (expDoc x) m 1307 ELet2 _ x ts -> envDoc ts $ shLet_ (mkDoc ts' x) m
1382 EAssign i (x, _) ts -> envDoc ts $ shLet i (expDoc x) m 1308 EAssign i x ts -> envDoc ts $ shLet i (mkDoc ts' x) m
1383 CheckType t ts -> envDoc ts $ shAnn ":" False <$> m <*> expDoc t 1309 CheckType t ts -> envDoc ts $ shAnn ":" False <$> m <*> mkDoc ts' (t, TType)
1384-- CheckSame t ts -> envDoc ts $ shCstr <$> m <*> expDoc t 1310-- CheckSame t ts -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t
1385 CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m 1311 CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m
1386 ELabelEnd ts -> envDoc ts $ shApp Visible (shAtom "labEnd") <$> m 1312 ELabelEnd ts -> envDoc ts $ shApp Visible (shAtom "labEnd") <$> m
1313 where
1314 ts' = False
1387 1315
1388expDoc = expDoc_ False 1316class MkDoc a where
1317 mkDoc :: Bool -> a -> Doc
1389 1318
1390expDoc_ :: Bool -> Exp -> Doc 1319instance MkDoc ExpType where
1391expDoc_ ts e = fmap inGreen <$> f e 1320 mkDoc ts e = mkDoc ts $ fst e
1392 where 1321
1393 f = \case 1322instance MkDoc Exp where
1394 PMLabel x _ -> f x 1323 mkDoc ts e = fmap inGreen <$> f e
1395 FixLabel _ x -> f x 1324 where
1396 Var k -> shAtom <$> shVar k 1325 f = \case
1397 App a b -> shApp Visible <$> f a <*> f b 1326 PMLabel x _ -> f x
1398 Lam h a b -> join $ shLam (used 0 b) (BLam h) <$> f a <*> pure (f b) 1327 FixLabel _ x -> f x
1399 Pi h a b -> join $ shLam (used 0 b) (BPi h) <$> f a <*> pure (f b) 1328 Neut x -> mkDoc ts x
1400 CstrT TType a b -> shCstr <$> f a <*> f b 1329-- Lam h a b -> join $ shLam (used 0 b) (BLam h) <$> f a <*> pure (f b)
1401 FunN s xs -> foldl (shApp Visible) (shAtom_ s) <$> mapM f xs 1330 Lam b -> join $ shLam True (BLam Visible) <$> f TType{-todo-} <*> pure (f b)
1402 CaseFun s xs -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM f xs 1331 Pi h a b -> join $ shLam (used 0 b) (BPi h) <$> f a <*> pure (f b)
1403 TyCaseFun s xs -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM f xs 1332 ENat n -> pure $ shAtom $ show n
1404 NatE n -> pure $ shAtom $ show n 1333 ConN s xs -> foldl (shApp Visible) (shAtom_ s) <$> mapM f xs
1405 ConN s xs -> foldl (shApp Visible) (shAtom_ s) <$> mapM f xs 1334 TyConN s xs -> foldl (shApp Visible) (shAtom_ s) <$> mapM f xs
1406 TyConN s xs -> foldl (shApp Visible) (shAtom_ s) <$> mapM f xs 1335 TType -> pure $ shAtom "Type"
1407 TType -> pure $ shAtom "Type" 1336 ELit l -> pure $ shAtom $ show l
1408 ELit l -> pure $ shAtom $ show l 1337 LabelEnd_ k x -> shApp Visible (shAtom $ "labend" ++ show k) <$> f x
1409 LabelEnd_ k x -> shApp Visible (shAtom $ "labend" ++ show k) <$> f x 1338
1410 1339 shAtom_ = shAtom . if ts then switchTick else id
1411 shAtom_ = shAtom . if ts then switchTick else id 1340
1412 1341instance MkDoc Neutral where
1413mExpDoc e = fmap inGreen <$> f e 1342 mkDoc ts e = fmap inGreen <$> f e
1414 where 1343 where
1415 f :: CEnv Exp -> Doc 1344 g = mkDoc ts
1416 f = \case 1345 f = \case
1417 MEnd a -> expDoc a 1346 Var_ k -> shAtom <$> shVar k
1418 Meta a b -> join $ shLam True BMeta <$> expDoc a <*> pure (f b) 1347 App_ a b -> shApp Visible <$> g a <*> g b
1419 Assign i (x, _) e -> shLet i (expDoc x) (f e) 1348 CstrT' TType a b -> shCstr <$> g a <*> g b
1349 Fun_ s xs -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g xs
1350 CaseFun_ s xs -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g xs
1351 TyCaseFun_ s xs -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g xs
1352
1353 shAtom_ = shAtom . if ts then switchTick else id
1354
1355instance MkDoc (CEnv Exp) where
1356 mkDoc ts e = fmap inGreen <$> f e
1357 where
1358 f :: CEnv Exp -> Doc
1359 f = \case
1360 MEnd a -> mkDoc ts a
1361 Meta a b -> join $ shLam True BMeta <$> mkDoc ts a <*> pure (f b)
1362 Assign i (x, _) e -> shLet i (mkDoc ts x) (f e)
1420 1363
1421-------------------------------------------------------------------------------- main 1364-------------------------------------------------------------------------------- main
1422 1365
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 31012fdd..e7356653 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -15,7 +15,7 @@ module LambdaCube.Compiler.Parser
15 , sourceInfo, SI(..), debugSI 15 , sourceInfo, SI(..), debugSI
16 , Module(..), Visibility(..), Binder(..), SExp'(..), Extension(..), Extensions 16 , Module(..), Visibility(..), Binder(..), SExp'(..), Extension(..), Extensions
17 , pattern SVar, pattern SType, pattern Wildcard, pattern SAppV, pattern SLamV, pattern SAnn 17 , pattern SVar, pattern SType, pattern Wildcard, pattern SAppV, pattern SLamV, pattern SAnn
18 , getParamsS, addParamsS, getApps, apps', downToS, usedS, addForalls 18 , getParamsS, addParamsS, getApps, apps', downToS, used, addForalls
19 , mkDesugarInfo, joinDesugarInfo 19 , mkDesugarInfo, joinDesugarInfo
20 , throwErrorTCM, ErrorMsg(..), ErrorT 20 , throwErrorTCM, ErrorMsg(..), ErrorT
21 , Doc, shLam, shApp, shLet, shLet_, shAtom, shAnn, shVar, epar, showDoc, showDoc_, sExpDoc 21 , Doc, shLam, shApp, shLet, shLet_, shAtom, shAnn, shVar, epar, showDoc, showDoc_, sExpDoc
@@ -202,34 +202,79 @@ instance SetSourceInfo (SExp' a) where
202 202
203-------------------------------------------------------------------------------- low-level toolbox 203-------------------------------------------------------------------------------- low-level toolbox
204 204
205foldS g f i = \case 205newtype MaxDB = MaxDB {getMaxDB :: Maybe Int}
206 SApp _ _ a b -> foldS g f i a <> foldS g f i b
207 SLet _ a b -> foldS g f i a <> foldS g f (i+1) b
208 SBind _ _ _ a b -> foldS g f i a <> foldS g f (i+1) b
209-- STyped si (e, t) -> f si i e <> f si i t
210 SVar sn j -> f sn j i
211 SGlobal sn -> g sn i
212 x@SLit{} -> mempty
213 206
214freeS = nub . foldS (\sn _ -> [sn]) mempty 0 207instance Monoid MaxDB where
215usedS = (getAny .) . foldS mempty (\sn j i -> Any $ j == i) 208 mempty = MaxDB Nothing
209 MaxDB a `mappend` MaxDB a' = MaxDB $ Just $ max (fromMaybe 0 a) (fromMaybe 0 a')
216 210
217mapS' = mapS__ (const . SGlobal) 211instance Show MaxDB where show _ = "MaxDB"
218mapS__ gg f2 h = g where 212
213varDB i = MaxDB $ Just $ i + 1
214
215lowerDB (MaxDB i) = MaxDB $ (+ (- 1)) <$> i
216lowerDB' l (MaxDB i) = MaxDB $ Just $ 1 + max l (fromMaybe 0 i)
217
218class Up a where
219 up_ :: Int -> Int -> a -> a
220 up_ n i = iterateN n $ up1_ i
221 up1_ :: Int -> a -> a
222 up1_ = up_ 1
223
224 fold :: Monoid e => (Int -> Int -> e) -> Int -> a -> e
225
226 used :: Int -> a -> Bool
227 used = (getAny .) . fold ((Any .) . (==))
228
229 maxDB_ :: a -> MaxDB
230
231 closedExp :: a -> a
232 closedExp a = a
233
234instance (Up a, Up b) => Up (a, b) where
235 up_ n i (a, b) = (up_ n i a, up_ n i b)
236 used i (a, b) = used i a || used i b
237 fold _ _ _ = error "fold @(_,_)"
238 maxDB_ (a, b) = maxDB_ a <> maxDB_ b
239 closedExp (a, b) = (closedExp a, closedExp b)
240
241up n = up_ n 0
242up1 = up1_ 0
243
244substS j x = mapS' f2 ((+1) *** up 1) (j, x)
245 where
246 f2 sn i (j, x) = case compare i j of
247 GT -> SVar sn $ i - 1
248 LT -> SVar sn i
249 EQ -> STyped (fst sn) x
250
251foldS h g f = fs
252 where
253 fs i = \case
254 SApp _ _ a b -> fs i a <> fs i b
255 SLet _ a b -> fs i a <> fs (i+1) b
256 SBind _ _ _ a b -> fs i a <> fs (i+1) b
257 STyped si x -> h i si x
258 SVar sn j -> f sn j i
259 SGlobal sn -> g sn i
260 x@SLit{} -> mempty
261
262freeS = nub . foldS (\_ _ _ -> error "freeS") (\sn _ -> [sn]) mempty 0
263
264mapS' = mapS__ (\_ _ _ -> error "mapS'") (const . SGlobal)
265mapS__ hh gg f2 h = g where
219 g i = \case 266 g i = \case
220 SApp si v a b -> SApp si v (g i a) (g i b) 267 SApp si v a b -> SApp si v (g i a) (g i b)
221 SLet x a b -> SLet x (g i a) (g (h i) b) 268 SLet x a b -> SLet x (g i a) (g (h i) b)
222 SBind si k si' a b -> SBind si k si' (g i a) (g (h i) b) 269 SBind si k si' a b -> SBind si k si' (g i a) (g (h i) b)
223 SVar sn j -> f2 sn j i 270 SVar sn j -> f2 sn j i
224 SGlobal sn -> gg sn i 271 SGlobal sn -> gg sn i
272 STyped si x -> hh i si x
225 x@SLit{} -> x 273 x@SLit{} -> x
226 274
227rearrangeS :: (Int -> Int) -> SExp -> SExp 275rearrangeS :: (Int -> Int) -> SExp -> SExp
228rearrangeS f = mapS' (\sn j i -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0 276rearrangeS f = mapS' (\sn j i -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0
229 277
230upS__ i n = mapS' (\sn j i -> SVar sn $ if j < i then j else j+n) (+1) i
231upS = upS__ 0 1
232
233substS'' :: Int -> Int -> SExp' a -> SExp' a 278substS'' :: Int -> Int -> SExp' a -> SExp' a
234substS'' j' x = mapS' f2 (+1) j' 279substS'' j' x = mapS' f2 (+1) j'
235 where 280 where
@@ -238,18 +283,40 @@ substS'' j' x = mapS' f2 (+1) j'
238 | j == i = SVar sn $ x + (j - j') 283 | j == i = SVar sn $ x + (j - j')
239 | j > i = SVar sn $ j - 1 284 | j > i = SVar sn $ j - 1
240 285
241substSG j = mapS__ (\sn x -> if sn == j then SVar sn x else SGlobal sn) (\sn j -> const $ SVar sn j) (+1) 286substSG j = mapS__ (\_ _ _ -> error "substSG") (\sn x -> if sn == j then SVar sn x else SGlobal sn) (\sn j -> const $ SVar sn j) (+1)
242substSG0 n = substSG n 0 . upS 287substSG0 n = substSG n 0 . up1
243 288
244downS t x | usedS t x = Nothing 289downS t x | used t x = Nothing
245 | otherwise = Just $ substS'' t (error "impossible") x 290 | otherwise = Just $ substS'' t (error "impossible") x
246 291
292instance Up Void
293
294instance Up a => Up (SExp' a) where
295 up_ n i = mapS' (\sn j i -> SVar sn $ if j < i then j else j+n) (+1) i
296 fold f = foldS (\_ _ _ -> error "fold @SExp") mempty $ \sn j i -> f j i
297
247dbf' = dbf_ 0 298dbf' = dbf_ 0
248dbf_ j xs e = foldl (\e (i, sn) -> substSG sn i e) e $ zip [j..] xs 299dbf_ j xs e = foldl (\e (i, sn) -> substSG sn i e) e $ zip [j..] xs
249 300
250dbff :: DBNames -> SExp -> SExp 301dbff :: DBNames -> SExp -> SExp
251dbff ns e = foldr substSG0 e ns 302dbff ns e = foldr substSG0 e ns
252 303
304trSExp' = trSExp elimVoid
305
306elimVoid :: Void -> a
307elimVoid _ = error "impossible"
308
309trSExp :: (a -> b) -> SExp' a -> SExp' b
310trSExp f = g where
311 g = \case
312 SApp si v a b -> SApp si v (g a) (g b)
313 SLet x a b -> SLet x (g a) (g b)
314 SBind si k si' a b -> SBind si k si' (g a) (g b)
315 SVar sn j -> SVar sn j
316 SGlobal sn -> SGlobal sn
317 SLit si l -> SLit si l
318 STyped si a -> STyped si $ f a
319
253-------------------------------------------------------------------------------- expression parsing 320-------------------------------------------------------------------------------- expression parsing
254 321
255parseType mb = maybe id option mb (reservedOp "::" *> parseTTerm PrecLam) 322parseType mb = maybe id option mb (reservedOp "::" *> parseTTerm PrecLam)
@@ -339,8 +406,8 @@ parseTerm prec = withRange setSI $ case prec of
339 dcls <- localIndentation Ge $ localAbsoluteIndentation $ parseDefs xSLabelEnd 406 dcls <- localIndentation Ge $ localAbsoluteIndentation $ parseDefs xSLabelEnd
340 mkLets True <$> dsInfo <*> pure dcls <* reserved "in" <*> parseTerm PrecLam 407 mkLets True <$> dsInfo <*> pure dcls <* reserved "in" <*> parseTerm PrecLam
341 where 408 where
342 mkLeftSection (op, e) = SLam Visible (Wildcard SType) $ SGlobal op `SAppV` SVar (mempty, ".ls") 0 `SAppV` upS e 409 mkLeftSection (op, e) = SLam Visible (Wildcard SType) $ SGlobal op `SAppV` SVar (mempty, ".ls") 0 `SAppV` up1 e
343 mkRightSection (e, op) = SLam Visible (Wildcard SType) $ SGlobal op `SAppV` upS e `SAppV` SVar (mempty, ".rs") 0 410 mkRightSection (e, op) = SLam Visible (Wildcard SType) $ SGlobal op `SAppV` up1 e `SAppV` SVar (mempty, ".rs") 0
344 411
345 mkSwizzling term = swizzcall 412 mkSwizzling term = swizzcall
346 where 413 where
@@ -420,7 +487,7 @@ parseTerm prec = withRange setSI $ case prec of
420 mkPi Hidden (getTTuple' -> xs) b = foldr (sNonDepPi Hidden) b xs 487 mkPi Hidden (getTTuple' -> xs) b = foldr (sNonDepPi Hidden) b xs
421 mkPi h a b = sNonDepPi h a b 488 mkPi h a b = sNonDepPi h a b
422 489
423 sNonDepPi h a b = SPi h a $ upS b 490 sNonDepPi h a b = SPi h a $ up1 b
424 491
425getTTuple' (getTTuple -> Just (n, xs)) | n == length xs = xs 492getTTuple' (getTTuple -> Just (n, xs)) | n == length xs = xs
426getTTuple' x = [x] 493getTTuple' x = [x]
@@ -457,7 +524,7 @@ mapP f = \case
457 ViewPat e pp -> ViewPat (f e) (mapPP f pp) 524 ViewPat e pp -> ViewPat (f e) (mapPP f pp)
458 PatType pp e -> PatType (mapPP f pp) (f e) 525 PatType pp e -> PatType (mapPP f pp) (f e)
459 526
460upP i j = mapP (upS__ i j) 527upP i j = mapP (up_ j i)
461 528
462varPP = length . getPPVars_ 529varPP = length . getPPVars_
463varP = length . getPVars_ 530varP = length . getPVars_
@@ -573,7 +640,7 @@ mapGT k i = \case
573 Alts gts -> Alts $ map (mapGT k i) gts 640 Alts gts -> Alts $ map (mapGT k i) gts
574 GuardLeaf e -> GuardLeaf $ i k e 641 GuardLeaf e -> GuardLeaf $ i k e
575 642
576upGT k i = mapGT k $ \k -> upS__ k i 643upGT k i = mapGT k $ \k -> up_ i k
577 644
578substGT i j = mapGT 0 $ \k -> rearrangeS $ \r -> if r == k + i then k + j else if r > k + i then r - 1 else r 645substGT i j = mapGT 0 $ \k -> rearrangeS $ \r -> if r == k + i then k + j else if r > k + i then r - 1 else r
579 646
@@ -628,13 +695,13 @@ compileGuardTree unode node adts t = (\x -> traceD (" ! :" ++ ppShow x) x) $ g
628 Nothing -> error $ "Constructor is not defined: " ++ s 695 Nothing -> error $ "Constructor is not defined: " ++ s
629 Just (Left ((t, inum), cns)) -> 696 Just (Left ((t, inum), cns)) ->
630 foldl SAppV (SGlobal (debugSI "compileGuardTree2", caseName t) `SAppV` iterateN (1 + inum) SLamV (Wildcard SType)) 697 foldl SAppV (SGlobal (debugSI "compileGuardTree2", caseName t) `SAppV` iterateN (1 + inum) SLamV (Wildcard SType))
631 [ iterateN n SLamV $ guardTreeToCases $ Alts $ map (filterGuardTree (upS__ 0 n f) cn 0 n . upGT 0 n) ts 698 [ iterateN n SLamV $ guardTreeToCases $ Alts $ map (filterGuardTree (up n f) cn 0 n . upGT 0 n) ts
632 | (cn, n) <- cns 699 | (cn, n) <- cns
633 ] 700 ]
634 `SAppV` f 701 `SAppV` f
635 Just (Right n) -> SGlobal (debugSI "compileGuardTree3", MatchName s) 702 Just (Right n) -> SGlobal (debugSI "compileGuardTree3", MatchName s)
636 `SAppV` SLamV (Wildcard SType) 703 `SAppV` SLamV (Wildcard SType)
637 `SAppV` iterateN n SLamV (guardTreeToCases $ Alts $ map (filterGuardTree (upS__ 0 n f) s 0 n . upGT 0 n) ts) 704 `SAppV` iterateN n SLamV (guardTreeToCases $ Alts $ map (filterGuardTree (up n f) s 0 n . upGT 0 n) ts)
638 `SAppV` f 705 `SAppV` f
639 `SAppV` guardTreeToCases (Alts $ map (filterGuardTree' f s) ts) 706 `SAppV` guardTreeToCases (Alts $ map (filterGuardTree' f s) ts)
640 707
@@ -643,7 +710,7 @@ compileGuardTree unode node adts t = (\x -> traceD (" ! :" ++ ppShow x) x) $ g
643 GuardLeaf e -> GuardLeaf e 710 GuardLeaf e -> GuardLeaf e
644 Alts ts -> Alts $ map (filterGuardTree f s k ns) ts 711 Alts ts -> Alts $ map (filterGuardTree f s k ns) ts
645 GuardNode f' s' ps gs 712 GuardNode f' s' ps gs
646 | f /= f' -> GuardNode f' s' ps $ filterGuardTree (upS__ 0 su f) s (su + k) ns gs 713 | f /= f' -> GuardNode f' s' ps $ filterGuardTree (up su f) s (su + k) ns gs
647 | s == s' -> filterGuardTree f s k ns $ guardNodes (zips [k+ns-1, k+ns-2..] ps) gs 714 | s == s' -> filterGuardTree f s k ns $ guardNodes (zips [k+ns-1, k+ns-2..] ps) gs
648 | otherwise -> Alts [] 715 | otherwise -> Alts []
649 where 716 where
@@ -656,7 +723,7 @@ compileGuardTree unode node adts t = (\x -> traceD (" ! :" ++ ppShow x) x) $ g
656 GuardLeaf e -> GuardLeaf e 723 GuardLeaf e -> GuardLeaf e
657 Alts ts -> Alts $ map (filterGuardTree' f s) ts 724 Alts ts -> Alts $ map (filterGuardTree' f s) ts
658 GuardNode f' s' ps gs 725 GuardNode f' s' ps gs
659 | f /= f' || s /= s' -> GuardNode f' s' ps $ filterGuardTree' (upS__ 0 su f) s gs 726 | f /= f' || s /= s' -> GuardNode f' s' ps $ filterGuardTree' (up su f) s gs
660 | otherwise -> Alts [] 727 | otherwise -> Alts []
661 where 728 where
662 su = sum $ map varPP ps 729 su = sum $ map varPP ps
@@ -761,7 +828,7 @@ parseDef =
761 where 828 where
762 mkProj (cn, (Just fs, _)) 829 mkProj (cn, (Just fs, _))
763 = [ Let fn Nothing Nothing [Visible] 830 = [ Let fn Nothing Nothing [Visible]
764 $ upS{-non-rec-} $ patLam SLabelEnd ge (PCon cn $ replicate (length fs) $ ParPat [PVar (fst cn, "generated_name1")]) $ SVar (fst cn, ".proj") i 831 $ up1{-non-rec-} $ patLam SLabelEnd ge (PCon cn $ replicate (length fs) $ ParPat [PVar (fst cn, "generated_name1")]) $ SVar (fst cn, ".proj") i
765 | (i, fn) <- zip [0..] fs] 832 | (i, fn) <- zip [0..] fs]
766 mkProj _ = [] 833 mkProj _ = []
767 834
@@ -821,7 +888,7 @@ mkLets True ge (Let n _ mt ar (downS 0 -> Just x): ds) e
821mkLets le ge (ValueDef p x: ds) e = patLam id ge p (dbff (getPVars p) $ mkLets le ge ds e) `SAppV` x -- (p = e; f) --> (\p -> f) e 888mkLets le ge (ValueDef p x: ds) e = patLam id ge p (dbff (getPVars p) $ mkLets le ge ds e) `SAppV` x -- (p = e; f) --> (\p -> f) e
822mkLets _ _ (x: ds) e = error $ "mkLets: " ++ show x 889mkLets _ _ (x: ds) e = error $ "mkLets: " ++ show x
823 890
824addForalls :: Extensions -> [SName] -> SExp' a -> SExp' a 891addForalls :: Up a => Extensions -> [SName] -> SExp' a -> SExp' a
825addForalls exs defined x = foldl f x [v | v@(_, vh:_) <- reverse $ freeS x, snd v `notElem'` defined, isLower vh || NoConstructorNamespace `elem` exs] 892addForalls exs defined x = foldl f x [v | v@(_, vh:_) <- reverse $ freeS x, snd v `notElem'` defined, isLower vh || NoConstructorNamespace `elem` exs]
826 where 893 where
827 f e v = SPi Hidden (Wildcard SType) $ substSG0 v e 894 f e v = SPi Hidden (Wildcard SType) $ substSG0 v e
@@ -852,15 +919,15 @@ compileFunAlts par ulend lend ds xs = dsInfo >>= \ge -> case xs of
852 ++ [ FunAlt n (map noTA ps) $ Right $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'Unit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ] 919 ++ [ FunAlt n (map noTA ps) $ Right $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'Unit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ]
853 ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] 920 ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")]
854 ++ concat 921 ++ concat
855 [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ upS t) 922 [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ up1 t)
856 : [ FunAlt m p $ Right $ {- SLam Hidden (Wildcard SType) $ upS $ -} substS'' 0 ic $ upS__ (ic+1) 1 e 923 : [ FunAlt m p $ Right $ {- SLam Hidden (Wildcard SType) $ up1 $ -} substS'' 0 ic $ up1_ (ic+1) e
857 | Instance n' i cstrs alts <- ds, n' == n 924 | Instance n' i cstrs alts <- ds, n' == n
858 , Let m' ~Nothing ~Nothing ar e <- alts, m' == m 925 , Let m' ~Nothing ~Nothing ar e <- alts, m' == m
859 , let p = zip ((,) Hidden <$> ps) i -- ++ ((Hidden, Wildcard SType), PVar): [] 926 , let p = zip ((,) Hidden <$> ps) i -- ++ ((Hidden, Wildcard SType), PVar): []
860 , let ic = sum $ map varP i 927 , let ic = sum $ map varP i
861 ] 928 ]
862 | (m, t) <- ms 929 | (m, t) <- ms
863-- , let ts = fst $ getParamsS $ upS t 930-- , let ts = fst $ getParamsS $ up1 t
864 ] 931 ]
865 [TypeAnn n t] -> return [Primitive n Nothing t | snd n `notElem` [n' | FunAlt (_, n') _ _ <- ds]] 932 [TypeAnn n t] -> return [Primitive n Nothing t | snd n `notElem` [n' | FunAlt (_, n') _ _ <- ds]]
866 tf@[TypeFamily n ps t] -> case [d | d@(FunAlt n' _ _) <- ds, n' == n] of 933 tf@[TypeFamily n ps t] -> case [d | d@(FunAlt n' _ _) <- ds, n' == n] of
@@ -1015,7 +1082,7 @@ parseLC f str
1015 1082
1016-------------------------------------------------------------------------------- pretty print 1083-------------------------------------------------------------------------------- pretty print
1017 1084
1018instance PShow (SExp' a) where 1085instance Up a => PShow (SExp' a) where
1019 pShowPrec _ = showDoc_ . sExpDoc 1086 pShowPrec _ = showDoc_ . sExpDoc
1020 1087
1021type Doc = NameDB PrecString 1088type Doc = NameDB PrecString
@@ -1029,14 +1096,14 @@ showDoc = str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':
1029showDoc_ :: Doc -> P.Doc 1096showDoc_ :: Doc -> P.Doc
1030showDoc_ = text . str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']) 1097showDoc_ = text . str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z'])
1031 1098
1032sExpDoc :: SExp' a -> Doc 1099sExpDoc :: Up a => SExp' a -> Doc
1033sExpDoc = \case 1100sExpDoc = \case
1034 SGlobal (_,s) -> pure $ shAtom s 1101 SGlobal (_,s) -> pure $ shAtom s
1035 SAnn a b -> shAnn ":" False <$> sExpDoc a <*> sExpDoc b 1102 SAnn a b -> shAnn ":" False <$> sExpDoc a <*> sExpDoc b
1036 TyType a -> shApp Visible (shAtom "tyType") <$> sExpDoc a 1103 TyType a -> shApp Visible (shAtom "tyType") <$> sExpDoc a
1037 SApp _ h a b -> shApp h <$> sExpDoc a <*> sExpDoc b 1104 SApp _ h a b -> shApp h <$> sExpDoc a <*> sExpDoc b
1038 Wildcard t -> shAnn ":" True (shAtom "_") <$> sExpDoc t 1105 Wildcard t -> shAnn ":" True (shAtom "_") <$> sExpDoc t
1039 SBind _ h _ a b -> join $ shLam (usedS 0 b) h <$> sExpDoc a <*> pure (sExpDoc b) 1106 SBind _ h _ a b -> join $ shLam (used 0 b) h <$> sExpDoc a <*> pure (sExpDoc b)
1040 SLet _ a b -> shLet_ (sExpDoc a) (sExpDoc b) 1107 SLet _ a b -> shLet_ (sExpDoc a) (sExpDoc b)
1041 STyped _ _{-(e,t)-} -> pure $ shAtom "<<>>" -- todo: expDoc e 1108 STyped _ _{-(e,t)-} -> pure $ shAtom "<<>>" -- todo: expDoc e
1042 SVar _ i -> shAtom <$> shVar i 1109 SVar _ i -> shAtom <$> shVar i
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 5eee2067..63fd85d4 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -126,11 +126,12 @@ removeEscs [] = []
126 126
127correctEscs :: String -> String 127correctEscs :: String -> String
128correctEscs = (++ "\ESC[K") . f ["39","49"] where 128correctEscs = (++ "\ESC[K") . f ["39","49"] where
129 f acc (ESC i@(_:_) cs) = ESC i $ f (i:acc) cs 129 f acc (ESC i@(_:_) cs) = esc (i /= head acc) i $ f (i: acc) cs
130 f (a: acc) (ESC "" cs) = ESC (compOld (cType a) acc) $ f acc cs 130 f (a: acc) (ESC "" cs) = esc (a /= head acc) (compOld (cType a) acc) $ f acc cs
131 f acc (c: cs) = c: f acc cs 131 f acc (c: cs) = c: f acc cs
132 f acc [] = [] 132 f acc [] = []
133 133
134 esc b i = if b then ESC i else id
134 compOld x xs = head $ filter ((== x) . cType) xs 135 compOld x xs = head $ filter ((== x) . cType) xs
135 136
136 cType n 137 cType n
diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index 479c9883..5c4ff581 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -394,7 +394,7 @@ testdata/Builtins.lc 65:49-65:56 Type
394testdata/Builtins.lc 65:53-65:54 Nat 394testdata/Builtins.lc 65:53-65:54 Nat
395testdata/Builtins.lc 65:55-65:56 Type 395testdata/Builtins.lc 65:55-65:56 Type
396testdata/Builtins.lc 66:1-66:7 {a} -> {b} -> {c:Nat} -> a->b -> VecS a c -> VecS b c 396testdata/Builtins.lc 66:1-66:7 {a} -> {b} -> {c:Nat} -> a->b -> VecS a c -> VecS b c
397testdata/Builtins.lc 66:23-66:32 {a} -> (d : b:Nat -> VecS a b -> Type) -> (e:a -> f:a -> d 2 ('V2 a e f)) -> (h:a -> i:a -> j:a -> d 3 ('V3 a h i j)) -> (l:a -> m:a -> n:a -> o:a -> d 4 ('V4 a l m n o)) -> {q:Nat} -> (r : VecS a q) -> d q r 397testdata/Builtins.lc 66:23-66:32 {a} -> (d : b:Nat -> VecS a b -> Type) -> (e:a -> f:a -> d 2 ('V2 e f)) -> (h:a -> i:a -> j:a -> d 3 ('V3 h i j)) -> (l:a -> m:a -> n:a -> o:a -> d 4 ('V4 l m n o)) -> {q:Nat} -> (r : VecS a q) -> d q r
398testdata/Builtins.lc 66:23-66:51 (V0 -> V1 -> VecS V6 2) -> (V1 -> V2 -> V3 -> VecS V8 3) -> (V2 -> V3 -> V4 -> V5 -> VecS V10 4) -> {m:Nat} -> VecS V4 m -> VecS V9 m 398testdata/Builtins.lc 66:23-66:51 (V0 -> V1 -> VecS V6 2) -> (V1 -> V2 -> V3 -> VecS V8 3) -> (V2 -> V3 -> V4 -> V5 -> VecS V10 4) -> {m:Nat} -> VecS V4 m -> VecS V9 m
399testdata/Builtins.lc 66:23-67:29 (V4 -> V5 -> V6 -> VecS V6 3) -> (V5 -> V6 -> V7 -> V8 -> VecS V8 4) -> {j:Nat} -> VecS V7 j -> VecS V7 j 399testdata/Builtins.lc 66:23-67:29 (V4 -> V5 -> V6 -> VecS V6 3) -> (V5 -> V6 -> V7 -> V8 -> VecS V8 4) -> {j:Nat} -> VecS V7 j -> VecS V7 j
400testdata/Builtins.lc 66:23-68:37 (V4 -> V5 -> V6 -> V7 -> VecS V7 4) -> {f:Nat} -> VecS V6 f -> VecS V6 f 400testdata/Builtins.lc 66:23-68:37 (V4 -> V5 -> V6 -> V7 -> VecS V7 4) -> {f:Nat} -> VecS V6 f -> VecS V6 f
diff --git a/testdata/Prelude.out b/testdata/Prelude.out
index 7966939c..0920bc2d 100644
--- a/testdata/Prelude.out
+++ b/testdata/Prelude.out
@@ -329,7 +329,7 @@ testdata/Prelude.lc 102:6-103:40 Type
329testdata/Prelude.lc 102:22-102:36 Type 329testdata/Prelude.lc 102:22-102:36 Type
330testdata/Prelude.lc 102:23-102:29 Type 330testdata/Prelude.lc 102:23-102:29 Type
331testdata/Prelude.lc 102:31-102:35 Type 331testdata/Prelude.lc 102:31-102:35 Type
332testdata/Prelude.lc 103:7-103:17 RecordC V2 | Type | {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type (\(b : Tuple2 String Type) -> 'snd String Type b) a) -> RecordC a 332testdata/Prelude.lc 103:7-103:17 RecordC V2 | Type | {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) a) -> RecordC a
333testdata/Prelude.lc 103:18-103:40 Type 333testdata/Prelude.lc 103:18-103:40 Type
334testdata/Prelude.lc 103:19-103:26 List Type -> Type 334testdata/Prelude.lc 103:19-103:26 List Type -> Type
335testdata/Prelude.lc 103:27-103:39 List Type 335testdata/Prelude.lc 103:27-103:39 List Type
@@ -434,16 +434,16 @@ testdata/Prelude.lc 169:45-170:164 List V2 -> V2 | V1 -> List V2 -> V2 | V10 |
434testdata/Prelude.lc 169:51-169:52 String 434testdata/Prelude.lc 169:51-169:52 String
435testdata/Prelude.lc 169:51-169:56 String->Bool 435testdata/Prelude.lc 169:51-169:56 String->Bool
436testdata/Prelude.lc 169:51-169:59 Bool 436testdata/Prelude.lc 169:51-169:59 Bool
437testdata/Prelude.lc 169:51-170:164 'tuptype ('map (Tuple2 String Type) Type (\(a : Tuple2 String Type) -> 'snd String Type a) V1) -> V1 | V13 437testdata/Prelude.lc 169:51-170:164 'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V1) -> V1 | V13
438testdata/Prelude.lc 169:53-169:56 {a} -> {b : Eq a} -> a -> a->Bool 438testdata/Prelude.lc 169:53-169:56 {a} -> {b : Eq a} -> a -> a->Bool
439testdata/Prelude.lc 169:57-169:59 V6 439testdata/Prelude.lc 169:57-169:59 V6
440testdata/Prelude.lc 169:62-169:65 {a} -> {b} -> Tuple2 a b -> a 440testdata/Prelude.lc 169:62-169:65 {a} -> {b} -> Tuple2 a b -> a
441testdata/Prelude.lc 169:62-169:113 V15 441testdata/Prelude.lc 169:62-169:113 V15
442testdata/Prelude.lc 169:62-170:164 Bool->V16 442testdata/Prelude.lc 169:62-170:164 Bool->V16
443testdata/Prelude.lc 169:66-169:113 Tuple2 V15 ('tuptype ('map (Tuple2 String Type) Type (\(a : Tuple2 String Type) -> 'snd String Type a) V8)) 443testdata/Prelude.lc 169:66-169:113 Tuple2 V15 ('tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V8))
444testdata/Prelude.lc 169:67-169:79 {a} -> {b} -> a->b 444testdata/Prelude.lc 169:67-169:79 {a} -> {b} -> a->b
445testdata/Prelude.lc 169:67-169:82 {a} -> V1->a 445testdata/Prelude.lc 169:67-169:82 {a} -> V1->a
446testdata/Prelude.lc 169:67-169:109 V0 -> Tuple2 V19 ('tuptype ('map (Tuple2 String Type) Type (\(b : Tuple2 String Type) -> 'snd String Type b) V12)) 446testdata/Prelude.lc 169:67-169:109 V0 -> Tuple2 V19 ('tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) V12))
447testdata/Prelude.lc 169:84-169:109 Type 447testdata/Prelude.lc 169:84-169:109 Type
448testdata/Prelude.lc 169:85-169:86 Type 448testdata/Prelude.lc 169:85-169:86 Type
449testdata/Prelude.lc 169:88-169:95 List Type -> Type 449testdata/Prelude.lc 169:88-169:95 List Type -> Type
@@ -453,7 +453,7 @@ testdata/Prelude.lc 169:97-169:100 {a} -> {b} -> a->b -> List a -> List b
453testdata/Prelude.lc 169:97-169:104 List (Tuple2 V0 V1) -> List V2 453testdata/Prelude.lc 169:97-169:104 List (Tuple2 V0 V1) -> List V2
454testdata/Prelude.lc 169:101-169:104 {a} -> {b} -> Tuple2 a b -> b 454testdata/Prelude.lc 169:101-169:104 {a} -> {b} -> Tuple2 a b -> b
455testdata/Prelude.lc 169:105-169:107 List (Tuple2 String Type) 455testdata/Prelude.lc 169:105-169:107 List (Tuple2 String Type)
456testdata/Prelude.lc 169:110-169:112 'tuptype ('map (Tuple2 String Type) Type (\(a : Tuple2 String Type) -> 'snd String Type a) V3) 456testdata/Prelude.lc 169:110-169:112 'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V3)
457testdata/Prelude.lc 170:51-170:58 {a} -> {b : List (Tuple2 String Type)} -> c:String -> {d : 'isKeyC String 'TT c a b} -> RecordC b -> a 457testdata/Prelude.lc 170:51-170:58 {a} -> {b : List (Tuple2 String Type)} -> c:String -> {d : 'isKeyC String 'TT c a b} -> RecordC b -> a
458testdata/Prelude.lc 170:51-170:61 {a : List (Tuple2 String Type)} -> b:String -> {c : 'isKeyC String 'TT b V19 a} -> RecordC a -> V21 458testdata/Prelude.lc 170:51-170:61 {a : List (Tuple2 String Type)} -> b:String -> {c : 'isKeyC String 'TT b V19 a} -> RecordC a -> V21
459testdata/Prelude.lc 170:51-170:65 a:String -> {b : 'isKeyC String 'TT a V17 V10} -> RecordC V11 -> V19 459testdata/Prelude.lc 170:51-170:65 a:String -> {b : 'isKeyC String 'TT a V17 V10} -> RecordC V11 -> V19
@@ -473,13 +473,13 @@ testdata/Prelude.lc 170:89-170:90 String
473testdata/Prelude.lc 170:91-170:92 Type 473testdata/Prelude.lc 170:91-170:92 Type
474testdata/Prelude.lc 170:93-170:95 List (Tuple2 String Type) 474testdata/Prelude.lc 170:93-170:95 List (Tuple2 String Type)
475testdata/Prelude.lc 170:98-170:164 RecordC V1 475testdata/Prelude.lc 170:98-170:164 RecordC V1
476testdata/Prelude.lc 170:99-170:109 {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type (\(b : Tuple2 String Type) -> 'snd String Type b) a) -> RecordC a 476testdata/Prelude.lc 170:99-170:109 {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) a) -> RecordC a
477testdata/Prelude.lc 170:110-170:163 'tuptype ('map (Tuple2 String Type) Type (\(a : Tuple2 String Type) -> 'snd String Type a) V9) 477testdata/Prelude.lc 170:110-170:163 'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V9)
478testdata/Prelude.lc 170:111-170:114 {a} -> {b} -> Tuple2 a b -> b 478testdata/Prelude.lc 170:111-170:114 {a} -> {b} -> Tuple2 a b -> b
479testdata/Prelude.lc 170:115-170:162 Tuple2 V16 ('tuptype ('map (Tuple2 String Type) Type (\(a : Tuple2 String Type) -> 'snd String Type a) V9)) 479testdata/Prelude.lc 170:115-170:162 Tuple2 V16 ('tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V9))
480testdata/Prelude.lc 170:116-170:128 {a} -> {b} -> a->b 480testdata/Prelude.lc 170:116-170:128 {a} -> {b} -> a->b
481testdata/Prelude.lc 170:116-170:131 {a} -> V1->a 481testdata/Prelude.lc 170:116-170:131 {a} -> V1->a
482testdata/Prelude.lc 170:116-170:158 V0 -> Tuple2 V20 ('tuptype ('map (Tuple2 String Type) Type (\(b : Tuple2 String Type) -> 'snd String Type b) V13)) 482testdata/Prelude.lc 170:116-170:158 V0 -> Tuple2 V20 ('tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) V13))
483testdata/Prelude.lc 170:133-170:158 Type 483testdata/Prelude.lc 170:133-170:158 Type
484testdata/Prelude.lc 170:134-170:135 Type 484testdata/Prelude.lc 170:134-170:135 Type
485testdata/Prelude.lc 170:137-170:144 List Type -> Type 485testdata/Prelude.lc 170:137-170:144 List Type -> Type
@@ -489,7 +489,7 @@ testdata/Prelude.lc 170:146-170:149 {a} -> {b} -> a->b -> List a -> List b
489testdata/Prelude.lc 170:146-170:153 List (Tuple2 V0 V1) -> List V2 489testdata/Prelude.lc 170:146-170:153 List (Tuple2 V0 V1) -> List V2
490testdata/Prelude.lc 170:150-170:153 {a} -> {b} -> Tuple2 a b -> b 490testdata/Prelude.lc 170:150-170:153 {a} -> {b} -> Tuple2 a b -> b
491testdata/Prelude.lc 170:154-170:156 List (Tuple2 String Type) 491testdata/Prelude.lc 170:154-170:156 List (Tuple2 String Type)
492testdata/Prelude.lc 170:159-170:161 'tuptype ('map (Tuple2 String Type) Type (\(a : Tuple2 String Type) -> 'snd String Type a) V4) 492testdata/Prelude.lc 170:159-170:161 'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V4)
493testdata/Prelude.lc 174:1-174:4 Float -> Float -> Float -> VecS Float 4 493testdata/Prelude.lc 174:1-174:4 Float -> Float -> Float -> VecS Float 4
494testdata/Prelude.lc 174:13-174:15 {a} -> a -> a -> a -> a -> VecS a 4 494testdata/Prelude.lc 174:13-174:15 {a} -> a -> a -> a -> a -> VecS a 4
495testdata/Prelude.lc 174:13-174:17 V5 -> V6 -> V7 -> VecS V8 4 495testdata/Prelude.lc 174:13-174:17 V5 -> V6 -> V7 -> VecS V8 4
diff --git a/testdata/language-features/adt/adt05.out b/testdata/language-features/adt/adt05.out
index d596dc9c..97b40b5c 100644
--- a/testdata/language-features/adt/adt05.out
+++ b/testdata/language-features/adt/adt05.out
@@ -1 +1 @@
main \ No newline at end of file main \ No newline at end of file
diff --git a/testdata/record01.reject.out b/testdata/record01.reject.out
index 84a36049..1a5f9539 100644
--- a/testdata/record01.reject.out
+++ b/testdata/record01.reject.out
@@ -1,5 +1,5 @@
1type error: can not unify 1type error: can not unify
2'FrameBuffer V1 V0 2'FrameBuffer V1 V0
3with 3with
4'Float 4'Float
5 5
diff --git a/testdata/typesig.reject.out b/testdata/typesig.reject.out
index 6b643ecd..20a94f96 100644
--- a/testdata/typesig.reject.out
+++ b/testdata/typesig.reject.out
@@ -1,2 +1,2 @@
1focus checkMetas: labEnd \{a}-><<HERE>> 1focus checkMetas: labEnd \{a}-><<HERE>>
2\(a : V0~'X)->X \ No newline at end of file 2\(a : V0~'X)->X \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 16:32:39 +0000