diff options
Diffstat (limited to 'src/LambdaCube/Compiler')
-rw-r--r-- | src/LambdaCube/Compiler/CoreToIR.hs | 4 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 44 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Parser.hs | 53 |
3 files changed, 65 insertions, 36 deletions
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs index 06b08038..62d6ba5c 100644 --- a/src/LambdaCube/Compiler/CoreToIR.hs +++ b/src/LambdaCube/Compiler/CoreToIR.hs | |||
@@ -33,7 +33,7 @@ import LambdaCube.Compiler.Pretty | |||
33 | import Text.PrettyPrint.Compact (nest) | 33 | import Text.PrettyPrint.Compact (nest) |
34 | import LambdaCube.Compiler.Infer hiding (Con, Lam, Pi, TType, Var, ELit, Func) | 34 | import LambdaCube.Compiler.Infer hiding (Con, Lam, Pi, TType, Var, ELit, Func) |
35 | import qualified LambdaCube.Compiler.Infer as I | 35 | import qualified LambdaCube.Compiler.Infer as I |
36 | import LambdaCube.Compiler.Parser (up, Up (..)) | 36 | import LambdaCube.Compiler.Parser (up, Up (..), upDB) |
37 | 37 | ||
38 | import Data.Version | 38 | import Data.Version |
39 | import Paths_lambdacube_compiler (version) | 39 | import Paths_lambdacube_compiler (version) |
@@ -892,7 +892,7 @@ unFunc' (LabelEnd x) = unFunc' x | |||
892 | unFunc' x = x | 892 | unFunc' x = x |
893 | 893 | ||
894 | instance Subst Exp ExpTV where | 894 | instance Subst Exp ExpTV where |
895 | subst i0 x (ExpTV a at vs) = ExpTV (subst i0 x a) (subst i0 x at) (zipWith (\i -> subst (i0+i) $ up i x{-todo: review-}) [1..] vs) | 895 | subst_ i0 dx x (ExpTV a at vs) = ExpTV (subst_ i0 dx x a) (subst_ i0 dx x at) (zipWith (\i -> subst_ (i0+i) (upDB i dx) $ up i x{-todo: review-}) [1..] vs) |
896 | 896 | ||
897 | addToEnv x xs = x: xs | 897 | addToEnv x xs = x: xs |
898 | mkEnv xs = {-trace_ ("mk " ++ show (length xs)) $ -} zipWith up [1..] xs | 898 | mkEnv xs = {-trace_ ("mk " ++ show (length xs)) $ -} zipWith up [1..] xs |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 16381ba4..977b8f9b 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -20,7 +20,7 @@ module LambdaCube.Compiler.Infer | |||
20 | , pattern Var, pattern CaseFun, pattern TyCaseFun, pattern App_, app_ | 20 | , pattern Var, pattern CaseFun, pattern TyCaseFun, pattern App_, app_ |
21 | , pattern Con, pattern TyCon, pattern Pi, pattern Lam, pattern Fun, pattern ELit, pattern Func, pattern LabelEnd, pattern FL, pattern UFL, unFunc_ | 21 | , pattern Con, pattern TyCon, pattern Pi, pattern Lam, pattern Fun, pattern ELit, pattern Func, pattern LabelEnd, pattern FL, pattern UFL, unFunc_ |
22 | , outputType, boolType, trueExp | 22 | , outputType, boolType, trueExp |
23 | , down, Subst (..), free | 23 | , down, Subst (..), free, subst |
24 | , initEnv, Env(..), pattern EBind2 | 24 | , initEnv, Env(..), pattern EBind2 |
25 | , SI(..), Range(..) -- todo: remove | 25 | , SI(..), Range(..) -- todo: remove |
26 | , Info(..), Infos, listAllInfos, listTypeInfos, listTraceInfos | 26 | , Info(..), Infos, listAllInfos, listTypeInfos, listTraceInfos |
@@ -360,11 +360,13 @@ unfixlabel a = a | |||
360 | -------------------------------------------------------------------------------- low-level toolbox | 360 | -------------------------------------------------------------------------------- low-level toolbox |
361 | 361 | ||
362 | class Subst b a where | 362 | class Subst b a where |
363 | subst :: Int -> b -> a -> a | 363 | subst_ :: Int -> MaxDB -> b -> a -> a |
364 | |||
365 | subst i x a = subst_ i (maxDB_ x) x a | ||
364 | 366 | ||
365 | down :: (Subst Exp a, Up a{-used-}) => Int -> a -> Maybe a | 367 | down :: (Subst Exp a, Up a{-used-}) => Int -> a -> Maybe a |
366 | down t x | used t x = Nothing | 368 | down t x | used t x = Nothing |
367 | | otherwise = Just $ subst t (error "impossible: down" :: Exp) x | 369 | | otherwise = Just $ subst_ t mempty (error "impossible: down" :: Exp) x |
368 | 370 | ||
369 | instance Eq Exp where | 371 | instance Eq Exp where |
370 | FL a == a' = a == a' | 372 | FL a == a' = a == a' |
@@ -408,12 +410,12 @@ instance Up Exp where | |||
408 | | otherwise = ((getAny .) . fold ((Any .) . (==))) i e | 410 | | otherwise = ((getAny .) . fold ((Any .) . (==))) i e |
409 | 411 | ||
410 | fold f i = \case | 412 | fold f i = \case |
411 | Lam b -> {-fold f i t <> todo: explain why this is not needed -} fold f (i+1) b | 413 | Lam b -> fold f (i+1) b |
412 | Pi _ a b -> fold f i a <> fold f (i+1) b | 414 | Pi _ a b -> fold f i a <> fold f (i+1) b |
413 | Con _ _ as -> foldMap (fold f i) as | 415 | Con _ _ as -> foldMap (fold f i) as |
414 | TyCon _ as -> foldMap (fold f i) as | 416 | TyCon _ as -> foldMap (fold f i) as |
415 | TType -> mempty | 417 | TType -> mempty |
416 | ELit _ -> mempty | 418 | ELit{} -> mempty |
417 | Neut x -> fold f i x | 419 | Neut x -> fold f i x |
418 | 420 | ||
419 | maxDB_ = \case | 421 | maxDB_ = \case |
@@ -423,7 +425,7 @@ instance Up Exp where | |||
423 | TyCon_ c _ _ -> c | 425 | TyCon_ c _ _ -> c |
424 | 426 | ||
425 | TType -> mempty | 427 | TType -> mempty |
426 | ELit _ -> mempty | 428 | ELit{} -> mempty |
427 | Neut x -> maxDB_ x | 429 | Neut x -> maxDB_ x |
428 | 430 | ||
429 | closedExp = \case | 431 | closedExp = \case |
@@ -436,9 +438,8 @@ instance Up Exp where | |||
436 | Neut a -> Neut $ closedExp a | 438 | Neut a -> Neut $ closedExp a |
437 | 439 | ||
438 | instance Subst Exp Exp where | 440 | instance Subst Exp Exp where |
439 | subst i0 x = f i0 | 441 | subst_ i0 dx x = f i0 |
440 | where | 442 | where |
441 | dx = maxDB_ x | ||
442 | f i (Neut n) = substNeut n | 443 | f i (Neut n) = substNeut n |
443 | where | 444 | where |
444 | substNeut e | cmpDB i e = Neut e | 445 | substNeut e | cmpDB i e = Neut e |
@@ -503,7 +504,7 @@ instance Up Neutral where | |||
503 | d@Delta{} -> d | 504 | d@Delta{} -> d |
504 | 505 | ||
505 | instance (Subst x a, Subst x b) => Subst x (a, b) where | 506 | instance (Subst x a, Subst x b) => Subst x (a, b) where |
506 | subst i x (a, b) = (subst i x a, subst i x b) | 507 | subst_ i dx x (a, b) = (subst_ i dx x a, subst_ i dx x b) |
507 | 508 | ||
508 | varType' :: Int -> [Exp] -> Exp | 509 | varType' :: Int -> [Exp] -> Exp |
509 | varType' i vs = vs !! i | 510 | varType' i vs = vs !! i |
@@ -558,7 +559,7 @@ getFunDef s f = case s of | |||
558 | parEval _ _ (LabelEnd x) = LabelEnd x | 559 | parEval _ _ (LabelEnd x) = LabelEnd x |
559 | parEval t a b = ParEval t a b | 560 | parEval t a b = ParEval t a b |
560 | CFName _ (SData s) -> case s of | 561 | CFName _ (SData s) -> case s of |
561 | "unsafeCoerce" -> \case xs@(_: _: x: _) -> case x of x@FL{} -> x; Neut{} -> f xs; _ -> x | 562 | "unsafeCoerce" -> \case xs@(_: _: x@NonNeut: _) -> x; xs -> f xs |
562 | "reflCstr" -> \case (a: _) -> TT | 563 | "reflCstr" -> \case (a: _) -> TT |
563 | 564 | ||
564 | "hlistNilCase" -> \case (_: x: (unfixlabel -> Con n@(ConName _ 0 _) _ _): _) -> x; xs -> f xs | 565 | "hlistNilCase" -> \case (_: x: (unfixlabel -> Con n@(ConName _ 0 _) _ _): _) -> x; xs -> f xs |
@@ -621,24 +622,23 @@ cstr = f [] | |||
621 | 622 | ||
622 | f_ [] TType (UFunN FVecScalar [a, b]) (UFunN FVecScalar [a', b']) = t2 (f [] TNat a a') (f [] TType b b') | 623 | f_ [] TType (UFunN FVecScalar [a, b]) (UFunN FVecScalar [a', b']) = t2 (f [] TNat a a') (f [] TType b b') |
623 | f_ [] TType (UFunN FVecScalar [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b') | 624 | f_ [] TType (UFunN FVecScalar [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b') |
624 | f_ [] TType (UFunN FVecScalar [a, b]) t@(TTyCon0 n) | isElemTy n = t2 (f [] TNat a (ENat 1)) (f [] TType b t) | 625 | f_ [] TType (UFunN FVecScalar [a, b]) t@NonNeut = t2 (f [] TNat a (ENat 1)) (f [] TType b t) |
625 | f_ [] TType (TVec a' b') (UFunN FVecScalar [a, b]) = t2 (f [] TNat a' a) (f [] TType b' b) | 626 | f_ [] TType (TVec a' b') (UFunN FVecScalar [a, b]) = t2 (f [] TNat a' a) (f [] TType b' b) |
626 | f_ [] TType t@(TTyCon0 n) (UFunN FVecScalar [a, b]) | isElemTy n = t2 (f [] TNat a (ENat 1)) (f [] TType b t) | 627 | f_ [] TType t@NonNeut (UFunN FVecScalar [a, b]) = t2 (f [] TNat a (ENat 1)) (f [] TType b t) |
627 | 628 | ||
628 | f_ [] typ a@Neut{} a' = CstrT typ a a' | 629 | f_ [] typ a@Neut{} a' = CstrT typ a a' |
629 | f_ [] typ a a'@Neut{} = CstrT typ a a' | 630 | f_ [] typ a a'@Neut{} = CstrT typ a a' |
630 | 631 | f_ ns typ a a' = Empty $ unlines [ "can not unify", ppShow a, "with", ppShow a' ] | |
631 | f_ ns typ a a' = Empty $ unlines [ "can not unify" | ||
632 | , ppShow a | ||
633 | , "with" | ||
634 | , ppShow a' | ||
635 | ] | ||
636 | 632 | ||
637 | ff _ _ [] = Unit | 633 | ff _ _ [] = Unit |
638 | ff ns tt@(Pi v t _) ((t1, t2'): ts) = t2 (f ns t t1 t2') $ ff ns (appTy tt t1) ts | 634 | ff ns tt@(Pi v t _) ((t1, t2'): ts) = t2 (f ns t t1 t2') $ ff ns (appTy tt t1) ts |
639 | ff ns t zs = error $ "ff: " -- ++ show (a, n, length xs', length $ mkConPars n typ) ++ "\n" ++ ppShow (nType a) ++ "\n" ++ ppShow (foldl appTy (nType a) $ mkConPars n typ) ++ "\n" ++ ppShow (zip xs xs') ++ "\n" ++ ppShow zs ++ "\n" ++ ppShow t | 635 | ff ns t zs = error $ "ff: " -- ++ show (a, n, length xs', length $ mkConPars n typ) ++ "\n" ++ ppShow (nType a) ++ "\n" ++ ppShow (foldl appTy (nType a) $ mkConPars n typ) ++ "\n" ++ ppShow (zip xs xs') ++ "\n" ++ ppShow zs ++ "\n" ++ ppShow t |
640 | 636 | ||
641 | isElemTy n = n `elem` [FBool, FFloat, FInt] | 637 | pattern NonNeut <- (nonNeut -> True) |
638 | |||
639 | nonNeut FL{} = True | ||
640 | nonNeut Neut{} = False | ||
641 | nonNeut _ = True | ||
642 | 642 | ||
643 | t2C (unfixlabel -> TT) (unfixlabel -> TT) = TT | 643 | t2C (unfixlabel -> TT) (unfixlabel -> TT) = TT |
644 | t2C a b = TFun Ft2C (Unit :~> Unit :~> Unit) [a, b] | 644 | t2C a b = TFun Ft2C (Unit :~> Unit :~> Unit) [a, b] |
@@ -710,9 +710,9 @@ instance (Subst Exp a, Up a) => Up (CEnv a) where | |||
710 | maxDB_ _ = error "maxDB_ @(CEnv _)" | 710 | maxDB_ _ = error "maxDB_ @(CEnv _)" |
711 | 711 | ||
712 | instance (Subst Exp a, Up a) => Subst Exp (CEnv a) where | 712 | instance (Subst Exp a, Up a) => Subst Exp (CEnv a) where |
713 | subst i x = \case | 713 | subst_ i dx x = \case |
714 | MEnd a -> MEnd $ subst i x a | 714 | MEnd a -> MEnd $ subst_ i dx x a |
715 | Meta a b -> Meta (subst i x a) (subst (i+1) (up 1 x) b) | 715 | Meta a b -> Meta (subst_ i dx x a) (subst_ (i+1) (upDB 1 dx) (up 1 x) b) |
716 | Assign j a b | 716 | Assign j a b |
717 | | j > i, Just a' <- down i a -> assign (j-1) a' (subst i (subst (j-1) (fst a') x) b) | 717 | | j > i, Just a' <- down i a -> assign (j-1) a' (subst i (subst (j-1) (fst a') x) b) |
718 | | j > i, Just x' <- down (j-1) x -> assign (j-1) (subst i x' a) (subst i x' b) | 718 | | j > i, Just x' <- down (j-1) x -> assign (j-1) (subst i x' a) (subst i x' b) |
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index 8430caa7..277f67b1 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs | |||
@@ -15,7 +15,7 @@ module LambdaCube.Compiler.Parser | |||
15 | , pattern SVar, pattern SType, pattern Wildcard, pattern SAppV, pattern SLamV, pattern SAnn | 15 | , pattern SVar, pattern SType, pattern Wildcard, pattern SAppV, pattern SLamV, pattern SAnn |
16 | , pattern SBuiltin, pattern SPi, pattern Primitive, pattern SLabelEnd, pattern SLam, pattern Parens | 16 | , pattern SBuiltin, pattern SPi, pattern Primitive, pattern SLabelEnd, pattern SLam, pattern Parens |
17 | , pattern TyType, pattern Wildcard_ | 17 | , pattern TyType, pattern Wildcard_ |
18 | , debug, isPi, varDB, lowerDB, upDB, notClosed, cmpDB, MaxDB(..), iterateN, traceD | 18 | , debug, isPi, varDB, lowerDB, upDB, cmpDB, MaxDB(..), iterateN, traceD |
19 | , parseLC, runDefParser | 19 | , parseLC, runDefParser |
20 | , getParamsS, addParamsS, getApps, apps', downToS, addForalls | 20 | , getParamsS, addParamsS, getApps, apps', downToS, addForalls |
21 | , Up (..), up1, up | 21 | , Up (..), up1, up |
@@ -176,27 +176,56 @@ instance SetSourceInfo (SExp' a) where | |||
176 | 176 | ||
177 | -------------------------------------------------------------------------------- De-Bruijn limit | 177 | -------------------------------------------------------------------------------- De-Bruijn limit |
178 | 178 | ||
179 | newtype MaxDB = MaxDB {getMaxDB :: Bool} -- True: closed | 179 | newtype MaxDB = MaxDB {getMaxDB :: Int} -- True: closed |
180 | 180 | ||
181 | instance Monoid MaxDB where | 181 | instance Monoid MaxDB where |
182 | mempty = MaxDB True | 182 | mempty = MaxDB 0 |
183 | MaxDB a `mappend` MaxDB a' = MaxDB $ a && a' -- $ Just $ max (fromMaybe 0 a) (fromMaybe 0 a') | 183 | MaxDB a `mappend` MaxDB a' = MaxDB $ max a a' |
184 | where | ||
185 | max 0 x = x | ||
186 | max _ _ = 1 -- | ||
184 | 187 | ||
185 | instance Show MaxDB where show _ = "MaxDB" | 188 | instance Show MaxDB where show _ = "MaxDB" |
186 | 189 | ||
187 | varDB i = MaxDB False | 190 | varDB i = MaxDB 1 -- |
191 | |||
192 | lowerDB = id -- | ||
193 | |||
194 | cmpDB _ (maxDB_ -> MaxDB x) = x == 0 | ||
195 | |||
196 | upDB _ (MaxDB 0) = MaxDB 0 | ||
197 | upDB x (MaxDB i) = MaxDB $ x + i | ||
198 | {- | ||
199 | data Na = Ze | Su Na | ||
200 | |||
201 | newtype MaxDB = MaxDB {getMaxDB :: Na} -- True: closed | ||
188 | 202 | ||
189 | lowerDB = id | 203 | instance Monoid MaxDB where |
204 | mempty = MaxDB Ze | ||
205 | MaxDB a `mappend` MaxDB a' = MaxDB $ max a a' | ||
206 | where | ||
207 | max Ze x = x | ||
208 | max (Su i) x = Su $ case x of | ||
209 | Ze -> i | ||
210 | Su j -> max i j | ||
211 | |||
212 | instance Show MaxDB where show _ = "MaxDB" | ||
190 | 213 | ||
191 | -- 0 means that no free variable is used | 214 | varDB i = MaxDB $ Su $ fr i |
192 | -- 1 means that only var 0 is used | 215 | where |
193 | --cmpDB i e = i >= maxDB e | 216 | fr 0 = Ze |
194 | cmpDB _ (maxDB_ -> MaxDB x) = x --isNothing x | 217 | fr i = Su $ fr $ i-1 |
195 | 218 | ||
196 | upDB n = id --(MaxDB i) = MaxDB $ (\x -> if x == 0 then x else x+n) $ i | 219 | lowerDB (MaxDB Ze) = MaxDB Ze |
220 | lowerDB (MaxDB (Su i)) = MaxDB i | ||
197 | 221 | ||
198 | notClosed = MaxDB False | 222 | cmpDB _ (maxDB_ -> MaxDB x) = case x of Ze -> True; _ -> False -- == 0 |
199 | 223 | ||
224 | upDB _ (MaxDB Ze) = MaxDB Ze | ||
225 | upDB x (MaxDB i) = MaxDB $ ad x i where | ||
226 | ad 0 i = i | ||
227 | ad n i = Su $ ad (n-1) i | ||
228 | -} | ||
200 | -------------------------------------------------------------------------------- low-level toolbox | 229 | -------------------------------------------------------------------------------- low-level toolbox |
201 | 230 | ||
202 | class Up a where | 231 | class Up a where |