diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 60 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/DesugaredSource.hs | 34 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 47 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Parser.hs | 8 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Pretty.hs | 5 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Statements.hs | 8 |
6 files changed, 81 insertions, 81 deletions
diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 377cd164..9fc61888 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs | |||
@@ -216,13 +216,14 @@ pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a | |||
216 | pattern TTyCon s t a <- TyCon (TyConName s _ t _ _) a | 216 | pattern TTyCon s t a <- TyCon (TyConName s _ t _ _) a |
217 | pattern TFun' a t b = DFun (FunName' a t) b | 217 | pattern TFun' a t b = DFun (FunName' a t) b |
218 | 218 | ||
219 | 219 | pattern TTyCon0 s <- TyCon (TyConName s _ _ _ _) [] | |
220 | pattern TTyCon0 s <- TyCon (TyConName s _ TType _ _) [] | ||
221 | 220 | ||
222 | tTyCon s t a cs = TyCon (TyConName s (error "todo: inum") t (map ((,) (error "tTyCon")) cs) $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a | 221 | tTyCon s t a cs = TyCon (TyConName s (error "todo: inum") t (map ((,) (error "tTyCon")) cs) $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a |
223 | tTyCon0 s cs = Closed $ TyCon (TyConName s 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) [] | 222 | tTyCon0 s cs = Closed $ TyCon (TyConName s 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) [] |
223 | |||
224 | pattern a :~> b = Pi Visible a b | 224 | pattern a :~> b = Pi Visible a b |
225 | 225 | ||
226 | pattern TConstraint <- TTyCon0 FConstraint where TConstraint = tTyCon0 FConstraint $ error "cs 1" | ||
226 | pattern Unit <- TTyCon0 FUnit where Unit = tTyCon0 FUnit [Unit] | 227 | pattern Unit <- TTyCon0 FUnit where Unit = tTyCon0 FUnit [Unit] |
227 | pattern TInt <- TTyCon0 FInt where TInt = tTyCon0 FInt $ error "cs 1" | 228 | pattern TInt <- TTyCon0 FInt where TInt = tTyCon0 FInt $ error "cs 1" |
228 | pattern TNat <- TTyCon0 FNat where TNat = tTyCon0 FNat $ error "cs 3" | 229 | pattern TNat <- TTyCon0 FNat where TNat = tTyCon0 FNat $ error "cs 3" |
@@ -233,8 +234,8 @@ pattern TChar <- TTyCon0 FChar where TChar = tTyCon0 FChar $ er | |||
233 | pattern TOrdering <- TTyCon0 FOrdering where TOrdering = tTyCon0 FOrdering $ error "cs 8" | 234 | pattern TOrdering <- TTyCon0 FOrdering where TOrdering = tTyCon0 FOrdering $ error "cs 8" |
234 | pattern TVec a b <- TyConN FVecS [b, a] | 235 | pattern TVec a b <- TyConN FVecS [b, a] |
235 | 236 | ||
236 | pattern Empty s <- TyCon (TyConName FEmpty _ _ _ _) [HString{-hnf?-} s] where | 237 | pattern Empty s <- TyCon (TyConName FEmpty _ _ _ _) [HString{-hnf?-} s] |
237 | Empty s = TyCon (TyConName FEmpty (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [HString s] | 238 | where Empty s = TyCon (TyConName FEmpty (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [HString s] |
238 | 239 | ||
239 | pattern TT <- ConN' _ _ | 240 | pattern TT <- ConN' _ _ |
240 | where TT = Closed (tCon FTT 0 Unit []) | 241 | where TT = Closed (tCon FTT 0 Unit []) |
@@ -243,11 +244,17 @@ pattern Zero <- ConN FZero _ | |||
243 | pattern Succ n <- ConN FSucc (n:_) | 244 | pattern Succ n <- ConN FSucc (n:_) |
244 | where Succ n = tCon FSucc 1 (TNat :~> TNat) [n] | 245 | where Succ n = tCon FSucc 1 (TNat :~> TNat) [n] |
245 | 246 | ||
247 | pattern CUnit <- ConN FCUnit _ | ||
248 | where CUnit = tCon FCUnit 0 TConstraint [] | ||
249 | pattern CEmpty s <- ConN FCEmpty (HString s: _) | ||
250 | where CEmpty s = tCon FCEmpty 1 (TString :~> TConstraint) [HString s] | ||
251 | |||
246 | pattern CstrT t a b = Neut (CstrT' t a b) | 252 | pattern CstrT t a b = Neut (CstrT' t a b) |
247 | pattern CstrT' t a b = TFun' FEqCT (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b] | 253 | pattern CstrT' t a b = TFun' FEqCT (TType :~> Var 0 :~> Var 1 :~> TConstraint) [t, a, b] |
248 | pattern Coe a b w x = TFun Fcoe (TType :~> TType :~> CstrT TType (Var 1) (Var 0) :~> Var 2 :~> Var 2) [a,b,w,x] | 254 | pattern Coe a b w x = TFun Fcoe (TType :~> TType :~> CW (CstrT TType (Var 1) (Var 0)) :~> Var 2 :~> Var 2) [a,b,w,x] |
249 | pattern ParEval t a b = TFun FparEval (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, a, b] | 255 | pattern ParEval t a b = TFun FparEval (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, a, b] |
250 | pattern T2 a b = TFun FT2 (TType :~> TType :~> TType) [a, b] | 256 | pattern T2 a b = TFun FT2 (TConstraint :~> TConstraint :~> TConstraint) [a, b] |
257 | pattern CW a = TFun FCW (TConstraint :~> TType) [a] | ||
251 | pattern CSplit a b c <- UFunN FSplit [a, b, c] | 258 | pattern CSplit a b c <- UFunN FSplit [a, b, c] |
252 | 259 | ||
253 | pattern HLit a <- (hnf -> ELit a) | 260 | pattern HLit a <- (hnf -> ELit a) |
@@ -422,7 +429,7 @@ instance Up Exp where | |||
422 | Pi _ a b -> foldVar f i a <> foldVar f (i+1) b | 429 | Pi _ a b -> foldVar f i a <> foldVar f (i+1) b |
423 | Con _ _ as -> foldMap (foldVar f i) as | 430 | Con _ _ as -> foldMap (foldVar f i) as |
424 | TyCon _ as -> foldMap (foldVar f i) as | 431 | TyCon _ as -> foldMap (foldVar f i) as |
425 | TType -> mempty | 432 | TType_ _ -> mempty |
426 | ELit{} -> mempty | 433 | ELit{} -> mempty |
427 | Neut x -> foldVar f i x | 434 | Neut x -> foldVar f i x |
428 | Delta -> mempty | 435 | Delta -> mempty |
@@ -451,7 +458,7 @@ instance HasMaxDB Exp where | |||
451 | Con_ c _ _ _ -> c | 458 | Con_ c _ _ _ -> c |
452 | TyCon_ c _ _ -> c | 459 | TyCon_ c _ _ -> c |
453 | 460 | ||
454 | TType -> mempty | 461 | TType_ _ -> mempty |
455 | ELit{} -> mempty | 462 | ELit{} -> mempty |
456 | Neut x -> maxDB_ x | 463 | Neut x -> maxDB_ x |
457 | Delta -> mempty | 464 | Delta -> mempty |
@@ -484,7 +491,7 @@ instance ClosedExp Exp where | |||
484 | Pi_ _ a b c -> Pi_ mempty a (closedExp b) c | 491 | Pi_ _ a b c -> Pi_ mempty a (closedExp b) c |
485 | Con_ _ a b c -> Con_ mempty a b (closedExp <$> c) | 492 | Con_ _ a b c -> Con_ mempty a b (closedExp <$> c) |
486 | TyCon_ _ a b -> TyCon_ mempty a (closedExp <$> b) | 493 | TyCon_ _ a b -> TyCon_ mempty a (closedExp <$> b) |
487 | e@TType{} -> e | 494 | e@TType_{} -> e |
488 | e@ELit{} -> e | 495 | e@ELit{} -> e |
489 | Neut a -> Neut $ closedExp a | 496 | Neut a -> Neut $ closedExp a |
490 | Delta -> Delta | 497 | Delta -> Delta |
@@ -574,6 +581,7 @@ pattern FunName' a t <- FunName a _ t | |||
574 | getFunDef s f = case show s of | 581 | getFunDef s f = case show s of |
575 | "'EqCT" -> \case (t: a: b: _) -> cstr t a b | 582 | "'EqCT" -> \case (t: a: b: _) -> cstr t a b |
576 | "'T2" -> \case (a: b: _) -> t2 a b | 583 | "'T2" -> \case (a: b: _) -> t2 a b |
584 | "'CW" -> \case (a: _) -> cw a | ||
577 | "t2C" -> \case (a: b: _) -> t2C a b | 585 | "t2C" -> \case (a: b: _) -> t2C a b |
578 | "coe" -> \case (a: b: t: d: _) -> evalCoe a b t d | 586 | "coe" -> \case (a: b: t: d: _) -> evalCoe a b t d |
579 | "parEval" -> \case (t: a: b: _) -> parEval t a b | 587 | "parEval" -> \case (t: a: b: _) -> parEval t a b |
@@ -672,13 +680,13 @@ evalCoe a b (Reduced x) d = evalCoe a b x d | |||
672 | evalCoe a b TT d = d | 680 | evalCoe a b TT d = d |
673 | evalCoe a b t d = Coe a b t d | 681 | evalCoe a b t d = Coe a b t d |
674 | 682 | ||
675 | 683 | cstr_ t a b = cw $ cstr t a b | |
676 | 684 | ||
677 | cstr = f [] | 685 | cstr = f [] |
678 | where | 686 | where |
679 | f z ty a a' = f_ z (hnf ty) (hnf a) (hnf a') | 687 | f z ty a a' = f_ z (hnf ty) (hnf a) (hnf a') |
680 | 688 | ||
681 | f_ _ _ a a' | a == a' = Unit | 689 | f_ _ _ a a' | a == a' = CUnit |
682 | f_ ns typ (RHS a) (RHS a') = f ns typ a a' | 690 | f_ ns typ (RHS a) (RHS a') = f ns typ a a' |
683 | f_ ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = | 691 | f_ ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = |
684 | ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ zip xs xs' | 692 | ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ zip xs xs' |
@@ -687,17 +695,17 @@ cstr = f [] | |||
687 | f_ (_: ns) typ{-down?-} (down 0 -> Just a) (down 0 -> Just a') = f ns typ a a' | 695 | f_ (_: ns) typ{-down?-} (down 0 -> Just a) (down 0 -> Just a') = f ns typ a a' |
688 | f_ ns TType (Pi h a b) (Pi h' a' b') | h == h' = t2 (f ns TType a a') (f ((a, a'): ns) TType b b') | 696 | f_ ns TType (Pi h a b) (Pi h' a' b') | h == h' = t2 (f ns TType a a') (f ((a, a'): ns) TType b b') |
689 | 697 | ||
690 | f_ [] TType (hnf -> UFunN FVecScalar [a, b]) (hnf -> UFunN FVecScalar [a', b']) = t2 (f [] TNat a a') (f [] TType b b') | 698 | f_ [] TType (UFunN FVecScalar [a, b]) (UFunN FVecScalar [a', b']) = t2 (f [] TNat a a') (f [] TType b b') |
691 | f_ [] TType (hnf -> UFunN FVecScalar [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b') | 699 | f_ [] TType (UFunN FVecScalar [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b') |
692 | f_ [] TType (hnf -> UFunN FVecScalar [a, b]) t@NonNeut = t2 (f [] TNat a (ENat 1)) (f [] TType b t) | 700 | f_ [] TType (UFunN FVecScalar [a, b]) t@NonNeut = t2 (f [] TNat a (ENat 1)) (f [] TType b t) |
693 | f_ [] TType (TVec a' b') (hnf -> UFunN FVecScalar [a, b]) = t2 (f [] TNat a' a) (f [] TType b' b) | 701 | f_ [] TType (TVec a' b') (UFunN FVecScalar [a, b]) = t2 (f [] TNat a' a) (f [] TType b' b) |
694 | f_ [] TType t@NonNeut (hnf -> UFunN FVecScalar [a, b]) = t2 (f [] TNat a (ENat 1)) (f [] TType b t) | 702 | f_ [] TType t@NonNeut (UFunN FVecScalar [a, b]) = t2 (f [] TNat a (ENat 1)) (f [] TType b t) |
695 | 703 | ||
696 | f_ [] typ a@Neut{} a' = CstrT typ a a' | 704 | f_ [] typ a@Neut{} a' = CstrT typ a a' |
697 | f_ [] typ a a'@Neut{} = CstrT typ a a' | 705 | f_ [] typ a a'@Neut{} = CstrT typ a a' |
698 | f_ ns typ a a' = Empty $ unlines [ "can not unify", ppShow a, "with", ppShow a' ] | 706 | f_ ns typ a a' = CEmpty $ unlines [ "can not unify", ppShow a, "with", ppShow a' ] |
699 | 707 | ||
700 | ff _ _ [] = Unit | 708 | ff _ _ [] = CUnit |
701 | ff ns tt@(Pi v t _) ((t1, t2'): ts) = t2 (f ns t t1 t2') $ ff ns (appTy tt t1) ts | 709 | ff ns tt@(Pi v t _) ((t1, t2'): ts) = t2 (f ns t t1 t2') $ ff ns (appTy tt t1) ts |
702 | 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 | 710 | 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 |
703 | 711 | ||
@@ -710,11 +718,15 @@ nonNeut _ = True | |||
710 | t2C (hnf -> TT) (hnf -> TT) = TT | 718 | t2C (hnf -> TT) (hnf -> TT) = TT |
711 | t2C a b = TFun Ft2C (Unit :~> Unit :~> Unit) [a, b] | 719 | t2C a b = TFun Ft2C (Unit :~> Unit :~> Unit) [a, b] |
712 | 720 | ||
713 | t2 (hnf -> Unit) a = a | 721 | cw (hnf -> CUnit) = Unit |
714 | t2 a (hnf -> Unit) = a | 722 | cw (hnf -> CEmpty a) = Empty a |
715 | t2 (hnf -> Empty a) (hnf -> Empty b) = Empty (a <> b) | 723 | cw a = CW a |
716 | t2 (hnf -> Empty s) _ = Empty s | 724 | |
717 | t2 _ (hnf -> Empty s) = Empty s | 725 | t2 (hnf -> CUnit) a = a |
726 | t2 a (hnf -> CUnit) = a | ||
727 | t2 (hnf -> CEmpty a) (hnf -> CEmpty b) = CEmpty (a <> b) | ||
728 | t2 (hnf -> CEmpty s) _ = CEmpty s | ||
729 | t2 _ (hnf -> CEmpty s) = CEmpty s | ||
718 | t2 a b = T2 a b | 730 | t2 a b = T2 a b |
719 | 731 | ||
720 | app_ :: Exp -> Exp -> Exp | 732 | app_ :: Exp -> Exp -> Exp |
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs index 8f192c3c..271c678e 100644 --- a/src/LambdaCube/Compiler/DesugaredSource.hs +++ b/src/LambdaCube/Compiler/DesugaredSource.hs | |||
@@ -173,12 +173,10 @@ instance SetSourceInfo SIName where | |||
173 | -- TODO: simplify this | 173 | -- TODO: simplify this |
174 | data FName | 174 | data FName |
175 | = CFName !Int (SData SIName) | 175 | = CFName !Int (SData SIName) |
176 | | FEqCT | FT2 | Fcoe | FparEval | Ft2C | FprimFix | 176 | | FEqCT | FT2 | Fcoe | FparEval | Ft2C | FprimFix | FCW |
177 | | FType | FUnit | FInt | FWord | FNat | FBool | FFloat | FString | FChar | FOrdering | FVecS | FEmpty | FHList | FOutput | 177 | | FType | FConstraint | FUnit | FInt | FWord | FNat | FBool | FFloat | FString | FChar | FOrdering | FVecS | FEmpty | FHList | FOutput |
178 | | FHCons | FHNil | FZero | FSucc | FFalse | FTrue | FLT | FGT | FEQ | FTT | FNil | FCons | 178 | | FHCons | FHNil | FZero | FSucc | FFalse | FTrue | FLT | FGT | FEQ | FTT | FNil | FCons | FCUnit | FCEmpty |
179 | | FSplit | FVecScalar | 179 | | FSplit | FVecScalar |
180 | -- todo: elim | ||
181 | | FEq | FOrd | FNum | FSigned | FComponent | FIntegral | FFloating | ||
182 | deriving (Eq, Ord) | 180 | deriving (Eq, Ord) |
183 | 181 | ||
184 | mkFName' (RangeSI (Range fn p _)) s = fromMaybe (hashPos fn p) $ lookup s $ zipWith (\i (s, _) -> (s, i)) [0..] fntable | 182 | mkFName' (RangeSI (Range fn p _)) s = fromMaybe (hashPos fn p) $ lookup s $ zipWith (\i (s, _) -> (s, i)) [0..] fntable |
@@ -196,6 +194,10 @@ fntable = | |||
196 | , (,) "coe" Fcoe | 194 | , (,) "coe" Fcoe |
197 | , (,) "parEval" FparEval | 195 | , (,) "parEval" FparEval |
198 | , (,) "t2C" Ft2C | 196 | , (,) "t2C" Ft2C |
197 | , (,) "'CW" FCW | ||
198 | , (,) "'Constraint" FConstraint | ||
199 | , (,) "CEmpty" FCEmpty | ||
200 | , (,) "CUnit" FCUnit | ||
199 | , (,) "primFix" FprimFix | 201 | , (,) "primFix" FprimFix |
200 | , (,) "'Unit" FUnit | 202 | , (,) "'Unit" FUnit |
201 | , (,) "'Int" FInt | 203 | , (,) "'Int" FInt |
@@ -209,13 +211,6 @@ fntable = | |||
209 | , (,) "'VecS" FVecS | 211 | , (,) "'VecS" FVecS |
210 | , (,) "'Empty" FEmpty | 212 | , (,) "'Empty" FEmpty |
211 | , (,) "'HList" FHList | 213 | , (,) "'HList" FHList |
212 | , (,) "'Eq" FEq | ||
213 | , (,) "'Ord" FOrd | ||
214 | , (,) "'Num" FNum | ||
215 | , (,) "'Signed" FSigned | ||
216 | , (,) "'Component" FComponent | ||
217 | , (,) "'Integral" FIntegral | ||
218 | , (,) "'Floating" FFloating | ||
219 | , (,) "'Output" FOutput | 214 | , (,) "'Output" FOutput |
220 | , (,) "'Type" FType | 215 | , (,) "'Type" FType |
221 | , (,) "HCons" FHCons | 216 | , (,) "HCons" FHCons |
@@ -317,9 +312,11 @@ pattern ConsName <- SIName _ ":" | |||
317 | pattern SRHS a = SBuiltin "_rhs" `SAppV` a | 312 | pattern SRHS a = SBuiltin "_rhs" `SAppV` a |
318 | pattern Section e = SBuiltin "^section" `SAppV` e | 313 | pattern Section e = SBuiltin "^section" `SAppV` e |
319 | pattern SType = SBuiltin "'Type" | 314 | pattern SType = SBuiltin "'Type" |
315 | pattern SConstraint = SBuiltin "'Constraint" | ||
320 | pattern Parens e = SBuiltin "parens" `SAppV` e | 316 | pattern Parens e = SBuiltin "parens" `SAppV` e |
321 | pattern SAnn a t = SBuiltin "typeAnn" `SAppH` t `SAppV` a | 317 | pattern SAnn a t = SBuiltin "typeAnn" `SAppH` t `SAppV` a |
322 | pattern TyType a = SAnn a SType | 318 | pattern TyType a = SAnn a SType |
319 | pattern SCW a = SBuiltin "'CW" `SAppV` a | ||
323 | 320 | ||
324 | -- builtin heterogenous list | 321 | -- builtin heterogenous list |
325 | pattern HList a = SBuiltin "'HList" `SAppV` a | 322 | pattern HList a = SBuiltin "'HList" `SAppV` a |
@@ -455,8 +452,7 @@ instance (Up a, PShow a) => PShow (SExp' a) where | |||
455 | SGlobal ns -> pShow ns | 452 | SGlobal ns -> pShow ns |
456 | Parens x -> pShow x -- TODO: remove | 453 | Parens x -> pShow x -- TODO: remove |
457 | SAnn a b -> shAnn (pShow a) (pShow b) | 454 | SAnn a b -> shAnn (pShow a) (pShow b) |
458 | TyType a -> text "tyType" `dApp` pShow a | 455 | TyType a -> text "tyType" `DApp` pShow a |
459 | SAppV a b -> pShow a `dApp` pShow b | ||
460 | SApp h a b -> shApp h (pShow a) (pShow b) | 456 | SApp h a b -> shApp h (pShow a) (pShow b) |
461 | Wildcard SType -> text "_" | 457 | Wildcard SType -> text "_" |
462 | Wildcard t -> shAnn (text "_") (pShow t) | 458 | Wildcard t -> shAnn (text "_") (pShow t) |
@@ -472,6 +468,13 @@ shApp Hidden a b = DApp a (DAt b) | |||
472 | 468 | ||
473 | shLam usedVar h a b = shLam_ usedVar h (Just a) b | 469 | shLam usedVar h a b = shLam_ usedVar h (Just a) b |
474 | 470 | ||
471 | shLam_ False (BPi Hidden) (Just (DText "'CW" `DApp` a)) b = DFreshName False $ showContext (DUp 0 a) b | ||
472 | where | ||
473 | showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d | ||
474 | showContext x (DParContext xs y) = DParContext (DComma x xs) y | ||
475 | showContext x (DContext xs y) = DParContext (DComma x xs) y | ||
476 | showContext x y = DContext x y | ||
477 | |||
475 | shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b | 478 | shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b |
476 | where | 479 | where |
477 | lam = case h of | 480 | lam = case h of |
@@ -497,6 +500,7 @@ shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b | |||
497 | showForall s x (DForall s' xs y) | s == s' = DForall s (DSep (InfixR 11) x xs) y | 500 | showForall s x (DForall s' xs y) | s == s' = DForall s (DSep (InfixR 11) x xs) y |
498 | showForall s x y = DForall s x y | 501 | showForall s x y = DForall s x y |
499 | 502 | ||
503 | -- TODO: use other sign instead of (=>) | ||
500 | showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d | 504 | showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d |
501 | showContext x (DParContext xs y) = DParContext (DComma x xs) y | 505 | showContext x (DParContext xs y) = DParContext (DComma x xs) y |
502 | showContext x (DContext xs y) = DParContext (DComma x xs) y | 506 | showContext x (DContext xs y) = DParContext (DComma x xs) y |
@@ -522,7 +526,7 @@ instance PShow Stmt where | |||
522 | pShow stmt = vcat . map DResetFreshNames $ case stmt of | 526 | pShow stmt = vcat . map DResetFreshNames $ case stmt of |
523 | Primitive n t -> pure $ shAnn (pShow n) (pShow t) | 527 | Primitive n t -> pure $ shAnn (pShow n) (pShow t) |
524 | Let n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)] | 528 | Let n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)] |
525 | Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl dApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs]) | 529 | Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl DApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs]) |
526 | PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i | 530 | PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i |
527 | 531 | ||
528 | instance DeBruijnify SIName Stmt where | 532 | instance DeBruijnify SIName Stmt where |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 5ff71a52..6b2bece3 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -86,20 +86,20 @@ showEnvSExp :: (PShow a, Up a) => Env -> SExp' a -> String | |||
86 | showEnvSExp e c = show $ envDoc e $ underline $ pShow c | 86 | showEnvSExp e c = show $ envDoc e $ underline $ pShow c |
87 | 87 | ||
88 | showEnvSExpType :: (PShow a, Up a) => Env -> SExp' a -> Exp -> String | 88 | showEnvSExpType :: (PShow a, Up a) => Env -> SExp' a -> Exp -> String |
89 | showEnvSExpType e c t = show $ envDoc e $ underline $ (shAnn (pShow c) (mkDoc False (ET t TType))) | 89 | showEnvSExpType e c t = show $ envDoc e $ underline $ (shAnn (pShow c) (mkDoc False t)) |
90 | 90 | ||
91 | envDoc :: Env -> Doc -> Doc | 91 | envDoc :: Env -> Doc -> Doc |
92 | envDoc x m = case x of | 92 | envDoc x m = case x of |
93 | EGlobal{} -> m | 93 | EGlobal{} -> m |
94 | EBind1 _ h ts b -> envDoc ts $ shLam (usedVar 0 b) h m (pShow b) | 94 | EBind1 _ h ts b -> envDoc ts $ shLam (usedVar 0 b) h m (pShow b) |
95 | EBind2 h a ts -> envDoc ts $ shLam True h (mkDoc False (ET a TType)) m | 95 | EBind2 h a ts -> envDoc ts $ shLam True h (mkDoc False a) m |
96 | EApp1 _ h ts b -> envDoc ts $ shApp h m (pShow b) | 96 | EApp1 _ h ts b -> envDoc ts $ shApp h m (pShow b) |
97 | EApp2 _ h (ET (Lam (Var 0)) (Pi Visible TType _)) ts -> envDoc ts $ shApp h (text "tyType") m | 97 | EApp2 _ h (ET (Lam (Var 0)) (Pi Visible TType _)) ts -> envDoc ts $ shApp h (text "tyType") m |
98 | EApp2 _ h a ts -> envDoc ts $ shApp h (mkDoc False a) m | 98 | EApp2 _ h a ts -> envDoc ts $ shApp h (mkDoc False a) m |
99 | ELet1 _ ts b -> envDoc ts $ shLet_ m (pShow b) | 99 | ELet1 _ ts b -> envDoc ts $ shLet_ m (pShow b) |
100 | ELet2 _ x ts -> envDoc ts $ shLet_ (mkDoc False x) m | 100 | ELet2 _ x ts -> envDoc ts $ shLet_ (mkDoc False x) m |
101 | EAssign i x ts -> envDoc ts $ shLet i (mkDoc False x) m | 101 | EAssign i x ts -> envDoc ts $ shLet i (mkDoc False x) m |
102 | CheckType t ts -> envDoc ts $ shAnn m $ mkDoc False (ET t TType) | 102 | CheckType t ts -> envDoc ts $ shAnn m $ mkDoc False t |
103 | CheckIType t ts -> envDoc ts $ shAnn m (text "??") -- mkDoc ts' t | 103 | CheckIType t ts -> envDoc ts $ shAnn m (text "??") -- mkDoc ts' t |
104 | -- CheckSame t ts -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t | 104 | -- CheckSame t ts -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t |
105 | CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m | 105 | CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m |
@@ -149,7 +149,7 @@ instance (Subst Exp a, Rearrange a) => Subst Exp (CEnv a) where | |||
149 | | j > i, Just x' <- down (j-1) x -> assign (j-1) (subst i x' a) (subst i x' b) | 149 | | j > i, Just x' <- down (j-1) x -> assign (j-1) (subst i x' a) (subst i x' b) |
150 | | j < i, Just a' <- down (i-1) a -> assign j a' (subst (i-1) (subst j (expr a') x) b) | 150 | | j < i, Just a' <- down (i-1) a -> assign j a' (subst (i-1) (subst j (expr a') x) b) |
151 | | j < i, Just x' <- down j x -> assign j (subst (i-1) x' a) (subst (i-1) x' b) | 151 | | j < i, Just x' <- down j x -> assign j (subst (i-1) x' a) (subst (i-1) x' b) |
152 | | j == i -> Meta (cstr (ty a) x $ expr a) $ up1_ 0 b | 152 | | j == i -> Meta (cstr_ (ty a) x $ expr a) $ up1_ 0 b |
153 | 153 | ||
154 | --swapAssign :: (Int -> Exp -> CEnv Exp -> a) -> (Int -> Exp -> CEnv Exp -> a) -> Int -> Exp -> CEnv Exp -> a | 154 | --swapAssign :: (Int -> Exp -> CEnv Exp -> a) -> (Int -> Exp -> CEnv Exp -> a) -> Int -> Exp -> CEnv Exp -> a |
155 | swapAssign _ clet i (ET (Var j) t) b | i > j = clet j (ET (Var (i-1)) t) $ subst j (Var (i-1)) $ up1_ i b | 155 | swapAssign _ clet i (ET (Var j) t) b | i > j = clet j (ET (Var (i-1)) t) $ subst j (Var (i-1)) $ up1_ i b |
@@ -338,7 +338,6 @@ inferN_ tellTrace = infer where | |||
338 | return $ ex == y | 338 | return $ ex == y |
339 | -} | 339 | -} |
340 | checkSame te (Wildcard _) a = True | 340 | checkSame te (Wildcard _) a = True |
341 | checkSame te (SGlobal (sName -> "'Type")) TType = True | ||
342 | checkSame te SType TType = True | 341 | checkSame te SType TType = True |
343 | checkSame te (SBind_ _ BMeta _ SType (STyped (ET (Var 0) _))) a = True | 342 | checkSame te (SBind_ _ BMeta _ SType (STyped (ET (Var 0) _))) a = True |
344 | checkSame te a b = error $ "checkSame: " ++ ppShow (a, b) | 343 | checkSame te a b = error $ "checkSame: " ++ ppShow (a, b) |
@@ -356,7 +355,7 @@ inferN_ tellTrace = infer where | |||
356 | CheckAppType si h t te b -- App1 h (CheckType t te) b | 355 | CheckAppType si h t te b -- App1 h (CheckType t te) b |
357 | | Pi h' x (down 0 -> Just y) <- et, h == h' -> case t of | 356 | | Pi h' x (down 0 -> Just y) <- et, h == h' -> case t of |
358 | Pi Hidden t1 t2 | h == Visible -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet -- <<e>> b : {t1} -> {t2} | 357 | Pi Hidden t1 t2 | h == Visible -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet -- <<e>> b : {t1} -> {t2} |
359 | _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr TType t y) $ EApp1 si h te b) $ up 1 eet | 358 | _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr_ TType t y) $ EApp1 si h te b) $ up 1 eet |
360 | | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet | 359 | | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet |
361 | EApp1 si h te b | 360 | EApp1 si h te b |
362 | | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b x | 361 | | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b x |
@@ -365,7 +364,7 @@ inferN_ tellTrace = infer where | |||
365 | -- | CheckAppType Hidden _ te' _ <- te -> error "ok" | 364 | -- | CheckAppType Hidden _ te' _ <- te -> error "ok" |
366 | | 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) | 365 | | 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) |
367 | where | 366 | where |
368 | cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr TType x y) | 367 | cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr_ TType x y) |
369 | ELet2 ln (ET x{-let-} xt) te -> focus_ te $ subst 0 (mkELet ln x xt){-let-} eet{-in-} | 368 | ELet2 ln (ET x{-let-} xt) te -> focus_ te $ subst 0 (mkELet ln x xt){-let-} eet{-in-} |
370 | CheckIType x te -> checkN te x e | 369 | CheckIType x te -> checkN te x e |
371 | CheckType_ si t te | 370 | CheckType_ si t te |
@@ -373,7 +372,7 @@ inferN_ tellTrace = infer where | |||
373 | -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet | 372 | -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet |
374 | | hArgs et < hArgs t, Pi Hidden t1 t2 <- t | 373 | | hArgs et < hArgs t, Pi Hidden t1 t2 <- t |
375 | -> focus_ (CheckType_ si t2 $ EBind2 (BLam Hidden) t1 te) eet | 374 | -> focus_ (CheckType_ si t2 $ EBind2 (BLam Hidden) t1 te) eet |
376 | | otherwise -> focus_ (EBind2_ si BMeta (cstr TType t et) te) $ up 1 eet | 375 | | otherwise -> focus_ (EBind2_ si BMeta (cstr_ TType t et) te) $ up 1 eet |
377 | EApp2 si h (ET a at) te -> focusTell te si $ ET (app_ a e) (appTy at e) -- h?? | 376 | EApp2 si h (ET a at) te -> focusTell te si $ ET (app_ a e) (appTy at e) -- h?? |
378 | EBind1 si h te b -> infer (EBind2_ (sourceInfo b) h e te) b | 377 | EBind1 si h te b -> infer (EBind2_ (sourceInfo b) h e te) b |
379 | EBind2_ si (BLam h) a te -> focus_ te $ lamPi h a eet | 378 | EBind2_ si (BLam h) a te -> focus_ te $ lamPi h a eet |
@@ -386,13 +385,14 @@ inferN_ tellTrace = infer where | |||
386 | ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-} | 385 | ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-} |
387 | EBind2_ si BMeta tt_ te | 386 | EBind2_ si BMeta tt_ te |
388 | | ERHS te' <- te -> refocus (ERHS $ EBind2_ si BMeta tt_ te') eet | 387 | | ERHS te' <- te -> refocus (ERHS $ EBind2_ si BMeta tt_ te') eet |
389 | | (hnf -> Unit) <- tt -> refocus te $ subst 0 TT eet | 388 | | Unit <- tt -> refocus te $ subst 0 TT eet |
389 | -- | CW (hnf -> CUnit) <- tt -> error "okk"--, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te | ||
390 | | Empty msg <- tt -> throwError' $ ETypeError (text msg) si | 390 | | Empty msg <- tt -> throwError' $ ETypeError (text msg) si |
391 | | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te | 391 | | CW (hnf -> T2 x y) <- tt, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te |
392 | -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet | 392 | -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet |
393 | | CstrT t a b <- tt, Just r <- cst (ET a t) b -> r | 393 | | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET a t) b -> r |
394 | | CstrT t a b <- tt, Just r <- cst (ET b t) a -> r | 394 | | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET b t) a -> r |
395 | | isCstr tt, EBind2 h x te' <- te{-, h /= BMeta todo: remove-}, Just x' <- down 0 tt, x == x' | 395 | | CW _ <- tt, EBind2 h x te' <- te, Just x' <- down 0 tt, x == x' |
396 | -> refocus te $ subst 1 (Var 0) eet | 396 | -> refocus te $ subst 1 (Var 0) eet |
397 | | EBind2_ si' h x te' <- te, h /= BMeta, Just b' <- down 0 tt | 397 | | EBind2_ si' h x te' <- te, h /= BMeta, Just b' <- down 0 tt |
398 | -> refocus (EBind2_ si' h (up 1 x) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet | 398 | -> refocus (EBind2_ si' h (up 1 x) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet |
@@ -467,14 +467,9 @@ lamPi h t (ET x y) = ET (Lam x) (Pi h t y) | |||
467 | 467 | ||
468 | replaceMetas bind = \case | 468 | replaceMetas bind = \case |
469 | Meta a t -> bind a $ replaceMetas bind t | 469 | Meta a t -> bind a $ replaceMetas bind t |
470 | Assign i x t | x' <- up1_ i x -> bind (cstr (ty x') (Var i) $ expr x') . up 1 . up1_ i $ replaceMetas bind t | 470 | Assign i x t | x' <- up1_ i x -> bind (cstr_ (ty x') (Var i) $ expr x') . up 1 . up1_ i $ replaceMetas bind t |
471 | MEnd t -> t | 471 | MEnd t -> t |
472 | 472 | ||
473 | |||
474 | isCstr CstrT{} = True | ||
475 | isCstr (UFunN s [_]) = s `elem` [FEq, FOrd, FNum, FSigned, FComponent, FIntegral, FFloating] -- todo: use Constraint type to decide this | ||
476 | isCstr _ = {- trace_ (ppShow c ++ show c) $ -} False | ||
477 | |||
478 | -------------------------------------------------------------------------------- re-checking | 473 | -------------------------------------------------------------------------------- re-checking |
479 | 474 | ||
480 | type Message = String | 475 | type Message = String |
@@ -570,7 +565,7 @@ dependentVars ie = cycle mempty | |||
570 | 565 | ||
571 | grow = flip foldMap ie $ \case | 566 | grow = flip foldMap ie $ \case |
572 | (n, t) -> (Set.singleton n <-> freeVars t) <> case t of | 567 | (n, t) -> (Set.singleton n <-> freeVars t) <> case t of |
573 | CstrT _{-todo-} ty f -> freeVars ty <-> freeVars f | 568 | (hnf -> CW (hnf -> CstrT _{-todo-} ty f)) -> freeVars ty <-> freeVars f |
574 | (hnf -> CSplit a b c) -> freeVars a <-> (freeVars b <> freeVars c) | 569 | (hnf -> CSplit a b c) -> freeVars a <-> (freeVars b <> freeVars c) |
575 | _ -> mempty | 570 | _ -> mempty |
576 | where | 571 | where |
@@ -746,12 +741,6 @@ lamify t x = addLams (fst $ getParams t) $ x $ downTo 0 $ arity t | |||
746 | arity :: Exp -> Int | 741 | arity :: Exp -> Int |
747 | arity = length . fst . getParams | 742 | arity = length . fst . getParams |
748 | 743 | ||
749 | {- | ||
750 | getApps' = second reverse . run where | ||
751 | run (App a b) = second (b:) $ run a | ||
752 | run x = (x, []) | ||
753 | -} | ||
754 | |||
755 | inferTerm :: Monad m => String -> SExp2 -> IM m ExpType | 744 | inferTerm :: Monad m => String -> SExp2 -> IM m ExpType |
756 | inferTerm msg t = | 745 | inferTerm msg t = |
757 | fmap (closedExp . recheck msg EGlobal . replaceMetas (lamPi Hidden)) $ inferN EGlobal t | 746 | fmap (closedExp . recheck msg EGlobal . replaceMetas (lamPi Hidden)) $ inferN EGlobal t |
@@ -767,13 +756,9 @@ addToEnv sn@(SIName si s) (ET x t) = do | |||
767 | case v of | 756 | case v of |
768 | Nothing -> return $ Map.singleton s (closedExp x, closedExp t, si) | 757 | Nothing -> return $ Map.singleton s (closedExp x, closedExp t, si) |
769 | Just (_, _, si') -> throwError' $ ERedefined s si si' | 758 | Just (_, _, si') -> throwError' $ ERedefined s si si' |
770 | {- | ||
771 | joinEnv :: Monad m => GlobalEnv -> GlobalEnv -> IM m GlobalEnv | ||
772 | joinEnv e1 e2 = do | ||
773 | -} | ||
774 | 759 | ||
775 | downTo n m = map Var [n+m-1, n+m-2..n] | 760 | downTo n m = map Var [n+m-1, n+m-2..n] |
776 | 761 | ||
777 | tellType si t = tell $ mkInfoItem (sourceInfo si) $ DTypeNamespace True $ mkDoc False (ET t TType) | 762 | tellType si t = tell $ mkInfoItem (sourceInfo si) $ DTypeNamespace True $ mkDoc False t |
778 | 763 | ||
779 | 764 | ||
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index eee794f9..cd118768 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs | |||
@@ -187,10 +187,8 @@ parseTermLam = | |||
187 | where | 187 | where |
188 | mkIf b t f = SBuiltin "primIfThenElse" `SAppV` b `SAppV` t `SAppV` f | 188 | mkIf b t f = SBuiltin "primIfThenElse" `SAppV` b `SAppV` t `SAppV` f |
189 | 189 | ||
190 | mkPi Hidden xs b = foldr (sNonDepPi Hidden) b $ getTTuple xs | 190 | mkPi Hidden xs b = foldr (\a b -> SPi Hidden a $ up1 b) b $ map SCW $ getTTuple xs |
191 | mkPi h a b = sNonDepPi h a b | 191 | mkPi Visible a b = SPi Visible a $ up1 b |
192 | |||
193 | sNonDepPi h a b = SPi h a $ up1 b | ||
194 | 192 | ||
195 | parseTermAnn = level parseTermOp $ \t -> SAnn t <$> parseType Nothing | 193 | parseTermAnn = level parseTermOp $ \t -> SAnn t <$> parseType Nothing |
196 | 194 | ||
@@ -423,7 +421,7 @@ parseDef = | |||
423 | return $ pure $ Class x (map snd ts) cs | 421 | return $ pure $ Class x (map snd ts) cs |
424 | <|> do reserved "instance" *> do | 422 | <|> do reserved "instance" *> do |
425 | typeNS $ do | 423 | typeNS $ do |
426 | constraints <- option [] $ try_ "constraint" $ getTTuple <$> setR parseTermOp <* reservedOp "=>" | 424 | constraints <- option [] $ try_ "constraint" $ map SCW . getTTuple <$> setR parseTermOp <* reservedOp "=>" |
427 | x <- upperCase | 425 | x <- upperCase |
428 | (nps, args) <- telescopePat | 426 | (nps, args) <- telescopePat |
429 | cs <- expNS $ option [] $ reserved "where" *> identation False ({-deBruijnify nps <$> -} funAltDef (Just lhsOperator) varId) | 427 | cs <- expNS $ option [] $ reserved "where" *> identation False ({-deBruijnify nps <$> -} funAltDef (Just lhsOperator) varId) |
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs index c2651cba..f9702b94 100644 --- a/src/LambdaCube/Compiler/Pretty.hs +++ b/src/LambdaCube/Compiler/Pretty.hs | |||
@@ -311,8 +311,6 @@ pattern DArr x y = DArr_ "->" x y | |||
311 | braces = DBrace | 311 | braces = DBrace |
312 | parens = DParen | 312 | parens = DParen |
313 | 313 | ||
314 | dApp x y = DApp x y | ||
315 | |||
316 | shCstr = DCstr | 314 | shCstr = DCstr |
317 | 315 | ||
318 | shTuple [] = "()" | 316 | shTuple [] = "()" |
@@ -338,6 +336,9 @@ class PShow a where | |||
338 | ppShow :: PShow a => a -> String | 336 | ppShow :: PShow a => a -> String |
339 | ppShow = show . pShow | 337 | ppShow = show . pShow |
340 | 338 | ||
339 | tracePShow :: PShow a => a -> b -> b | ||
340 | tracePShow a b = trace (ppShow a) b | ||
341 | |||
341 | instance PShow Doc where pShow = id | 342 | instance PShow Doc where pShow = id |
342 | instance PShow Int where pShow = fromString . show | 343 | instance PShow Int where pShow = fromString . show |
343 | instance PShow Integer where pShow = fromString . show | 344 | instance PShow Integer where pShow = fromString . show |
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs index 0046eb27..42f02b07 100644 --- a/src/LambdaCube/Compiler/Statements.hs +++ b/src/LambdaCube/Compiler/Statements.hs | |||
@@ -86,12 +86,12 @@ compileStmt compilegt ds = \case | |||
86 | [Instance{}] -> return [] | 86 | [Instance{}] -> return [] |
87 | [Class n ps ms] -> do | 87 | [Class n ps ms] -> do |
88 | cd <- compileStmt' $ | 88 | cd <- compileStmt' $ |
89 | [ TypeAnn n $ foldr (SPi Visible) SType ps ] | 89 | [ TypeAnn n $ foldr (SPi Visible) SConstraint ps ] |
90 | ++ [ funAlt n (map noTA ps) $ noGuards $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'Unit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ] | 90 | ++ [ funAlt n (map noTA ps) $ noGuards $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'CUnit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ] |
91 | ++ [ funAlt n (replicate (length ps) (noTA $ PVarSimp $ dummyName "cst0")) $ noGuards $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ sName n ++ " on ???"{-TODO-})] | 91 | ++ [ funAlt n (replicate (length ps) (noTA $ PVarSimp $ dummyName "cst0")) $ noGuards $ SBuiltin "'CEmpty" `SAppV` sLit (LString $ "no instance of " ++ sName n ++ " on ???"{-TODO-})] |
92 | cds <- sequence | 92 | cds <- sequence |
93 | [ compileStmt'_ SRHS SRHS{-id-} | 93 | [ compileStmt'_ SRHS SRHS{-id-} |
94 | $ TypeAnn m (UncurryS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS "a2" 0 $ length ps) $ up1 t) | 94 | $ TypeAnn m (UncurryS (map ((,) Hidden) ps) $ SPi Hidden (SCW $ foldl SAppV (SGlobal n) $ downToS "a2" 0 $ length ps) $ up1 t) |
95 | : as | 95 | : as |
96 | | (m, t) <- ms | 96 | | (m, t) <- ms |
97 | -- , let ts = fst $ getParamsS $ up1 t | 97 | -- , let ts = fst $ getParamsS $ up1 t |