apple 0.1.0.0 → 0.2.0.0
raw patch · 38 files changed
+782/−532 lines, 38 filesdep +fast-arithmeticdep +tasty-quickcheckPVP ok
version bump matches the API change (PVP)
Dependencies added: fast-arithmetic, tasty-quickcheck
API changes (from Hackage documentation)
+ A: InitM :: Builtin
+ A: IsEq :: C
+ A: TailM :: Builtin
+ C: instance GHC.Internal.Show.Show C.BTemp
+ C: instance GHC.Internal.Show.Show C.FTemp
+ C: instance GHC.Internal.Show.Show C.Temp
+ IR: Cpy1 :: AE -> AE -> Exp -> Stmt
+ L: BuiltinBool :: Builtin
+ L: IDiv :: Sym
+ L: Ice :: Sym
+ L: InitM :: Sym
+ L: TailM :: Sym
+ Ty: instance Prettyprinter.Internal.Pretty Ty.Focus
Files
- CHANGELOG.md +9/−0
- apple.cabal +5/−2
- include/apple_p.h +10/−0
- of/Test.hs +2/−0
- run/Main.hs +24/−6
- src/A.hs +11/−2
- src/A/Eta.hs +2/−0
- src/Asm/Aarch64/Byte.hs +9/−6
- src/Asm/Aarch64/T.hs +25/−4
- src/Asm/G.hs +1/−1
- src/Asm/X86/Trans.hs +1/−1
- src/C.hs +4/−0
- src/C/Alloc.hs +30/−18
- src/C/CF.hs +14/−8
- src/C/Trans.hs +215/−132
- src/IR.hs +2/−0
- src/IR/C.hs +1/−0
- src/IR/CF.hs +23/−21
- src/IR/Hoist.hs +22/−21
- src/IR/Opt.hs +4/−2
- src/L.x +15/−4
- src/Parser.y +11/−6
- src/Parser/Rw.hs +3/−0
- src/Ty.hs +282/−259
- test/Spec.cpphs +19/−13
- test/data/const.apple +0/−4
- test/data/filt.apple +1/−0
- test/data/pf.apple +8/−0
- test/data/twoSum.apple +0/−5
- test/examples/ffact.apple +0/−1
- test/examples/neuralNetwork.apple +0/−10
- test/examples/partition.apple +1/−1
- test/examples/perimeter.apple +2/−3
- test/examples/primes.apple +5/−0
- test/examples/sum.apple +0/−1
- test/examples/xor.apple +1/−1
- test/harness/ia_harness.c +10/−0
- test/harness/ii_harness.c +10/−0
CHANGELOG.md view
@@ -1,5 +1,14 @@ # apple +## 0.2.0.0++ * Add `:delete` to REPL+ * Some cases no longer crash the compiler+ * Fix `free` insertion in branches+ * Implement filter (`§`) and 'indices of' (`⩪`)+ * Add `{:?` (tailM) and `}:?` (initM)+ * Existentials are handled better+ ## 0.1.0.0 Initial release
apple.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.0 name: apple-version: 0.1.0.0+version: 0.2.0.0 license: AGPL-3 license-file: LICENSE copyright: Copyright: (c) 2022 Vanessa McHale@@ -284,7 +284,10 @@ tasty, tasty-hunit, bytestring,- hypergeometric >=0.1.4.0+ hypergeometric >=0.1.4.0,+ fast-arithmetic,+ QuickCheck,+ tasty-quickcheck if impl(ghc >=8.10) ghc-options: -Wunused-packages
include/apple_p.h view
@@ -14,3 +14,13 @@ F* e=xs+(rnk+1)*sizeof(F); PA("%f",t,e); }++void pai(U xs) {+ J* dims=xs;+ J rnk=dims[0];dims+=1;+ pj(rnk);pf(" ");+ J t=1;J d;+ DO(i,rnk,{d=dims[i];t*=d;pj(d);if (i!=rnk-1) {pf(",");}}) nl;+ J* e=xs+(rnk+1)*sizeof(J);+ PA("%lld",t,e);+}
of/Test.hs view
@@ -46,6 +46,8 @@ , ccOut pwd "test/data/sin.🍏" "ff" sys "-1.000000\n" , ccOut pwd "test/data/conv.🍏" "conv" sys "2 3,3\n9.000000,9.000000,9.000000,9.000000,9.000000,9.000000,9.000000,9.000000,9.000000\n" , ccOut pwd "math/hypergeometric.🍏" "hyper" sys "2.030078"+ , ccOut pwd "math/numbertheory/radical.🍎" "ii" sys "30"+ , ccOut pwd "test/data/pf.🍎" "ia" sys "1 3\n2,3,5\n" ] where sys = case arch of {"x86_64" -> X64; "aarch64" -> Aarch64}
run/Main.hs view
@@ -24,7 +24,7 @@ import Data.Tuple.Extra (first3) import Data.Word (Word8) import Dbg-import Foreign.LibFFI (argPtr, callFFI, retCDouble, retCUChar, retInt64, retPtr, retWord8)+import Foreign.LibFFI (callFFI, retCDouble, retCUChar, retInt64, retPtr, retWord8) import Foreign.Marshal.Alloc (free) import Foreign.Marshal.Array (peekArray) import Foreign.Ptr (Ptr, castPtr, plusPtr)@@ -60,6 +60,8 @@ aEe :: Nm AlexPosn -> E AlexPosn -> Env -> Env aEe n e (Env l ees mm a) = Env l ((n,e):ees) mm a +mE f (Env l ees mm a) = Env l (f ees) mm a+ setL :: AlexUserState -> Env -> Env setL lSt (Env _ ees mm a) = Env lSt ees mm a @@ -107,7 +109,7 @@ appleCompletions ("ay:", "") = pure ("ay:", cyclicSimple ["nk"]) appleCompletions ("nay:", "") = pure ("nay:", cyclicSimple ["k"]) appleCompletions ("knay:", "") = pure ("knay:", cyclicSimple [""])-appleCompletions ("d:", "") = pure ("d:", [simpleCompletion "isasm"])+appleCompletions ("d:", "") = pure ("d:", [simpleCompletion "isasm", simpleCompletion "elete"]) appleCompletions ("id:", "") = pure ("id:", [simpleCompletion "sasm"]) appleCompletions ("sid:", "") = pure ("sid:", [simpleCompletion "asm"]) appleCompletions ("asid:", "") = pure ("asid:", [simpleCompletion "sm"])@@ -131,6 +133,12 @@ appleCompletions ("eh:", "") = pure ("eh:", [simpleCompletion "lp"]) appleCompletions ("leh:", "") = pure ("leh:", [simpleCompletion "p"]) appleCompletions ("pleh:", "") = pure ("pleh:", [simpleCompletion ""])+appleCompletions ("ed:", "") = pure ("ed:", [simpleCompletion "lete"])+appleCompletions ("led:", "") = pure ("led:", [simpleCompletion "ete"])+appleCompletions ("eled:", "") = pure ("eled:", [simpleCompletion "te"])+appleCompletions ("teled:", "") = pure ("teled:", [simpleCompletion "e"])+appleCompletions ("eteled:", "") = pure ("eteled:", [simpleCompletion ""])+appleCompletions (" eteled:", "") = do { ns <- namesStr ; pure (" eteled:", cyclicSimple ns) } appleCompletions (" yt:", "") = do { ns <- namesStr ; pure (" yt:", cyclicSimple ns) } appleCompletions (" t:", "") = do { ns <- namesStr ; pure (" t:", cyclicSimple ns) } appleCompletions ("", "") = ("",) . cyclicSimple <$> namesStr@@ -167,9 +175,13 @@ Just (":graph":e) -> graph (unwords e) *> loop Just (":qc":e) -> qc (unwords e) *> loop Just (":quickcheck":e) -> qc (unwords e) *> loop+ Just (":delete":[n]) -> del n *> loop Just e -> printExpr (unwords e) *> loop Nothing -> pure () +del :: String -> Repl AlexPosn ()+del s = lift $ modify (mE (filter (\((Nm n _ _),_) -> n /= st))) where st=T.pack s+ listCtx :: Repl AlexPosn () listCtx = do bs <- lift $ gets ee@@ -190,6 +202,7 @@ , helpOption ":qc" "<proposition>" "Property test" , helpOption ":quit, :q" "" "Quit REPL" , helpOption ":yank, :y" "<fn> <file>" "Read file"+ , helpOption ":delete" "<name>" "Delete from REPL environment" , helpOption "\\l" "" "Reference card" -- TODO: dump debug state ]@@ -199,7 +212,7 @@ [ lOption "Λ" "scan" "√" "sqrt" , lOption "⋉" "max" "⋊" "min" , lOption "⍳" "integer range" "⌊" "floor"- , lOption "ℯ" "exp" "⨳ {m,n}" "convolve"+ , lOption "e:" "exp" "⨳ {m,n}" "convolve" , lOption "\\~" "successive application" "\\`n" "dyadic infix" , lOption "_." "log" "'n" "map" , lOption "`" "zip" "`{i,j∘[k,l]}" "rank"@@ -210,7 +223,7 @@ , lOption "re:" "repeat" "}." "typesafe last" , lOption "⊲" "cons" "⊳" "snoc" , lOption "^:" "iterate" "%." "matmul"- , lOption "⊗" "outer product" "|:" "transpose"+ , lOption "⊗" "outer product" "⍉, |:" "transpose" , lOption "{.?" "head" "{." "typesafe head" , lOption "}.?" "last" "}:" "typesafe init" , lOption "⟨z,w⟩" "array literal" "?p,.e1,.e2" "conditional"@@ -225,7 +238,7 @@ , lOption "%:" "vector mul" "odd." "parity" , lOption "~" "reverse" "¬,⊻,∧,∨" "logical" , lOption "♭" "flatten" "♮" "add dimension"- , lOption "℘" "indices of" "§" "filter"+ , lOption "⩪" "indices of" "§, #." "filter" , lOption "👁️" "identity m" "(i × j)" "dimensions" , lOption "gen." "generate" "{x⟜y;z}" "no inline" ]@@ -434,6 +447,11 @@ asm@(_, fp, _) <- efp eC benchmark (nfIO $ callFFI fp retCDouble []) freeAsm asm+ A.B -> do+ liftIO $ do+ asm@(_, fp, _) <- efp eC+ benchmark (nfIO $ callFFI fp retCUChar [])+ freeAsm asm P [A.F,A.F] -> error "Haskell support for float ABI is poor :(" (Arr _ _) -> do liftIO $ do@@ -458,7 +476,7 @@ pR I p = do {i <- peek (castPtr p :: Ptr Int64); pure (pretty i)} pR A.F p = do {f <- peek (castPtr p :: Ptr Double); pure (pretty f)} pR A.B p = do {b <- peek (castPtr p :: Ptr AB); pure (pretty b)}-pR (P ts) p = tupledBy "*" <$> traverse (`pR` p) ts+pR (P ts) p = tupledBy "*" <$> let pds = offs ts in zipWithM pR ts ((p `plusPtr`) <$> pds) peekInterpret :: T a -> Ptr b -> IO (Doc ann) peekInterpret (Arr _ t) p = do
src/A.hs view
@@ -44,12 +44,16 @@ instance Show (I a) where show = show . pretty -data C = IsNum | IsOrd -- implies eq+data C = IsNum | IsOrd | IsEq | HasBits deriving (Generic, Eq, Ord) instance NFData C where -instance Pretty C where pretty IsNum = "IsNum"; pretty IsOrd = "IsOrd"; pretty HasBits = "HasBits"+instance Pretty C where+ pretty IsNum = "IsNum"+ pretty IsOrd = "IsOrd"+ pretty IsEq = "IsEq"+ pretty HasBits = "HasBits" instance Show C where show=show.pretty @@ -165,7 +169,9 @@ pretty Head = "{." pretty HeadM = "{.?" pretty Tail = "{:"+ pretty TailM = "{:?" pretty Init = "}:"+ pretty InitM = "}:?" pretty ConsE = "⊲" pretty Snoc = "⊳" pretty Mul = "%."@@ -220,6 +226,7 @@ | DI !Int -- dyadic infix | Conv [Int] | TAt !Int | Last | LastM | ConsE | Snoc | Mul | VMul | Outer | R | Head | HeadM | Tail | Init | RevE+ | TailM | InitM | Sin | Cos | Rot | Tan | Cyc | A1 | Even | Odd | IOf | Abs | And | Or | Xor | N | Sr | Sl deriving (Generic)@@ -266,6 +273,8 @@ mPrec Mod = Just 7 mPrec Succ = Just 9 mPrec Fold = Just 9+mPrec Ices = Just 6+mPrec Filt = Just 6 mPrec Map = Just 5 mPrec ConsE = Just 4 mPrec Snoc = Just 4
src/A/Eta.hs view
@@ -43,6 +43,8 @@ ηAt (EApp t ho@(Builtin _ Fold) op) = EApp t ho <$> η op ηAt (EApp t ho@(Builtin _ FoldA) op) = EApp t ho <$> η op ηAt (EApp t ho@(Builtin _ Foldl) op) = EApp t ho <$> η op+ηAt (EApp t ho@(Builtin _ Filt{}) f) = EApp t ho <$> η f+ηAt (EApp t ho@(Builtin _ Ices{}) p) = EApp t ho <$> η p ηAt (EApp t ho@(Builtin _ Map{}) op) = EApp t ho <$> η op ηAt (EApp t ho@(Builtin _ Rank{}) op) = EApp t ho <$> η op ηAt (EApp t ho@(Builtin _ DI{}) op) = EApp t ho <$> η op
src/Asm/Aarch64/Byte.hs view
@@ -137,6 +137,7 @@ asm ix st (Ldr _ r (RP rb u):asms) | (uϵ, 0) <- u `quotRem` 8 = [0b11111001, 0x1 `shiftL` 6 .|. fromIntegral (uϵ `shiftR` 6), fromIntegral (0b111111 .&. uϵ) `shiftL` 2 .|. be rb `shiftR` 3, lb rb r]:asm (ix+4) st asms asm ix st (Ldr _ r (R rb):asms) = [0xf9, 0x1 `shiftL` 6, be rb `shiftR` 3, lb rb r]:asm (ix+4) st asms asm ix st (Ldr _ r (BI rb ri s):asms) = [0b11111000, 0x3 `shiftL` 5 .|. be ri, 0x3 `shiftL` 5 .|. bs s `shiftL` 4 .|. 0x2 `shiftL` 2 .|. (be rb `shiftR` 3), lb rb r]:asm (ix+4) st asms+asm ix st (LdrB x r (R rb):asms) = asm ix st (LdrB x r (RP rb 0):asms) asm ix st (LdrB _ r (RP rb u):asms) | u <= 4095 = [0b00111001, 0x1 `shiftL` 6 .|. (fromIntegral u `shiftR` 6), fromIntegral (0b111111 .&. u) `shiftL` 2 .|. be rb `shiftR` 3, lb rb r]:asm (ix+4) st asms asm ix st (LdrB _ r (BI rb ri s):asms) = [0b00111000, 0x3 `shiftL` 5 .|. be ri, 0x3 `shiftL` 5 .|. bs s `shiftL` 4 .|. 0x2 `shiftL` 2 .|. (be rb `shiftR` 3), lb rb r]:asm (ix+4) st asms asm ix st (Ldp x r0 r1 (R rb):asms) = asm ix st (Ldp x r0 r1 (RP rb 0):asms)@@ -144,6 +145,8 @@ asm ix st (Str x r (R rb):asms) = asm ix st (Str x r (RP rb 0):asms) asm ix st (Str _ r (RP rb u):asms) | (uu, 0) <- u `quotRem` 8 = [0xf9, fromIntegral (uu `shiftR` 6), fromIntegral (0b111111 .&. uu) `shiftL` 2 .|. be rb `shiftR` 3, lb rb r]:asm (ix+4) st asms asm ix st (Str _ r (BI rb ri s):asms) = [0b11111000, 0x1 `shiftL` 5 .|. be ri, 0x3 `shiftL` 5 .|. bs s `shiftL` 4 .|. 0x2 `shiftL` 2 .|. be rb `shiftR` 3, lb rb r]:asm (ix+4) st asms+asm ix st (StrB x r (R rb):asms) = asm ix st (StrB x r (RP rb 0):asms)+asm ix st (StrB _ r (RP rb u):asms) | u <= 4095 = [0b00111001, fromIntegral (u `shiftR` 6), fromIntegral (0b111111 .&. u) `shiftL` 2 .|. be rb `shiftR` 3, lb rb r]:asm (ix+4) st asms asm ix st (StrB _ r (BI rb ri s):asms) = [0b00111000, 0x1 `shiftL` 5 .|. be ri, 0x3 `shiftL` 5 .|. bs s `shiftL` 4 .|. 0x2 `shiftL` 2 .|. be rb `shiftR` 3, lb rb r]:asm (ix+4) st asms asm ix st (StrD _ d (BI rb ri s):asms) = [0xfc, 0x1 `shiftL` 5 .|. be ri, 0x3 `shiftL` 5 .|. bs s `shiftL` 4 .|. 0x2 `shiftL` 2 .|. be rb `shiftR` 3, lb rb d]:asm (ix+4) st asms asm ix st (StrD _ d (R rb):asms) = [0b11111101, 0x0, be rb `shiftR` 3, lb rb d]:asm (ix+4) st asms@@ -203,16 +206,16 @@ asm ix st (m4 r m++asms) asm ix st@(_, (Just (_, f, _, _), _), _) (MovRCf _ r Free:asms) = asm ix st (m4 r f++asms)-asm ix st@(_, (_, Just (_, l, _)),_) (MovRCf _ r Log:asms) =- asm ix st (m4 r l++asms)-asm ix st@(_, (_, Just (e, _, _)),_) (MovRCf _ r Exp:asms) =- asm ix st (m4 r e++asms)-asm ix st@(_, (_, Just (_, _, p)),_) (MovRCf _ r Pow:asms) =- asm ix st (m4 r p++asms) asm ix st@(_, (Just (_, _, d, _), _),_) (MovRCf _ r DR:asms) = asm ix st (m4 r d++asms) asm ix st@(_, (Just (_, _, _, j), _),_) (MovRCf _ r JR:asms) = asm ix st (m4 r j++asms)+asm ix st@(_, (_, Just (e, _, _)),_) (MovRCf _ r Exp:asms) =+ asm ix st (m4 r e++asms)+asm ix st@(_, (_, Just (_, l, _)),_) (MovRCf _ r Log:asms) =+ asm ix st (m4 r l++asms)+asm ix st@(_, (_, Just (_, _, p)),_) (MovRCf _ r Pow:asms) =+ asm ix st (m4 r p++asms) asm ix st (LdrRL _ r l:asms) = let p = pI$arr l st w0=p .&. 0xffff; w1=(p .&. 0xffff0000) `lsr` 16; w2=(p .&. 0xFFFF00000000) `lsr` 32; w3=(p .&. 0xFFFF000000000000) `lsr` 48
src/Asm/Aarch64/T.hs view
@@ -30,6 +30,7 @@ mIop Op.IPlus = Just AddRR mIop Op.IMinus = Just SubRR mIop Op.ITimes = Just MulRR+mIop Op.IDiv = Just Sdiv mIop (Op.BI b) = Just$mB b mIop _ = Nothing @@ -233,14 +234,28 @@ let li=fromIntegral$(n-1)*8 pure $ plED ++ plES ++ concat [ [Ldp () t0 t1 (RP (IReg rS) (i*16)), Stp () t0 t1 (RP (IReg rD) (i*16))] | i <- fromIntegral<$>[0..(n'-1)] ] ++ [Ldr () t0 (RP (IReg rS) li), Str () t0 (RP (IReg rD) li)] ir (IR.Cpy (IR.AP tD eD _) (IR.AP tS eS _) eN) = do- rD <- nextI; rS <- nextI; rN <- nextI; i <- nextR+ rD <- nextI; rS <- nextI; i <- nextR t0 <- nextR; t1 <- nextR plED <- eval (maybe id (+) eD$IR.Reg tD) (IR.ITemp rD) plES <- eval (maybe id (+) eS$IR.Reg tS) (IR.ITemp rS)- plEN <- eval eN (IR.ITemp rN)- let rDA=IReg rD; rSA=IReg rS; rNA=IReg rN+ (plEN, rN) <- plI eN+ let rDA=IReg rD; rSA=IReg rS l <- nextL; eL <- nextL- pure $ plED ++ plES ++ plEN ++ [MovRC () i 0, CmpRR () i rNA, Bc () Geq eL, Tbz () rNA 0 l, Ldr () t0 (R rSA), Str () t0 (R rDA), MovRC () i 1, AddRC () rSA rSA 8, AddRC () rDA rDA 8, Label () l, Ldp () t0 t1 (R rSA), Stp () t0 t1 (R rDA), AddRC () rSA rSA 16, AddRC () rDA rDA 16, AddRC () i i 2, CmpRR () i rNA, Bc () Lt l, Label () eL]+ pure $ plED ++ plES ++ plEN [ZeroR () i, CmpRR () i rN, Bc () Geq eL, Tbz () rN 0 l, Ldr () t0 (R rSA), Str () t0 (R rDA), MovRC () i 1, AddRC () rSA rSA 8, AddRC () rDA rDA 8, Label () l, Ldp () t0 t1 (R rSA), Stp () t0 t1 (R rDA), AddRC () rSA rSA 16, AddRC () rDA rDA 16, AddRC () i i 2, CmpRR () i rN, Bc () Lt l, Label () eL]+ir (IR.Cpy1 (IR.AP tD (Just (IR.ConstI di)) _) (IR.AP tS (Just (IR.ConstI si)) _) eN) | Just du <- mu16 di, Just su <- mu16 si = do+ rD <- nextI; rS <- nextI; i <- nextR; t <- nextR+ (plEN, rN) <- plI eN+ l <- nextL; eL <- nextL+ let rDA=IReg rD; rSA=IReg rS+ pure $ plEN [MovRR () rDA (absReg tD), MovRR () rSA (absReg tS), ZeroR () i, CmpRR () i rN, Bc () Geq eL, Label () l, LdrB () t (RP rSA du), StrB () t (RP rDA su), AddRC () rSA rSA 1, AddRC () rDA rDA 1, AddRC () i i 1, CmpRR () i rN, Bc () Lt l, Label () eL]+ir (IR.Cpy1 (IR.AP tD eD _) (IR.AP tS eS _) eN) = do+ rD <- nextI; rS <- nextI; i <- nextR; t <- nextR+ plED <- eval (maybe id (+) eD$IR.Reg tD) (IR.ITemp rD)+ plES <- eval (maybe id (+) eS$IR.Reg tS) (IR.ITemp rS)+ (plEN, rN) <- plI eN+ l <- nextL; eL <- nextL+ let rDA=IReg rD; rSA=IReg rS+ pure $ plED ++ plES ++ plEN [ZeroR () i, CmpRR () i rN, Bc () Geq eL, Label () l, LdrB () t (BI rSA i Zero), StrB () t (BI rDA i Zero), AddRC () i i 1, CmpRR () i rN, Bc () Lt l, Label () eL] -- ir (IR.IRnd t) = pure [MrsR () (absReg t)] ir (IR.IRnd t) = do r <- nextR@@ -404,6 +419,12 @@ eval (IR.IB Op.IPlus (IR.IB Op.ITimes e0 e1) e2) t = do (plE0,r0) <- plI e0; (plE1,r1) <- plI e1; (plE2,r2) <- plI e2 pure $ plE0 $ plE1 $ plE2 [Madd () (absReg t) r0 r1 r2]+eval (IR.IB Op.IMin e0 e1) t = do+ (plE0,r0) <- plI e0; (plE1,r1) <- plI e1+ pure $ plE0 $ plE1 [CmpRR () r0 r1, Csel () (absReg t) r0 r1 Leq]+eval (IR.IB Op.IMax e0 e1) t = do+ (plE0,r0) <- plI e0; (plE1,r1) <- plI e1+ pure $ plE0 $ plE1 [CmpRR () r0 r1, Csel () (absReg t) r0 r1 Geq] eval (IR.IB op e0 e1) t | Just isn <- mIop op = do (plE0,r0) <- plI e0; (plE1,r1) <- plI e1 pure $ plE0 $ plE1 [isn () (absReg t) r0 r1]
src/Asm/G.hs view
@@ -42,7 +42,7 @@ mapColN f ns = ns { colN = f (colN ns) } mapSpN f ns = ns { spN = f (spN ns) } -data St = St { mvs :: Movs, aS :: GS, aL :: GL, mvS :: Mv, ɴs :: Ns, degs :: !(IM.IntMap Int), initial :: [Int], wkls :: Wk, stack :: [Int], alias :: IM.IntMap Int }+data St = St { mvs :: Movs, aS :: GS, aL :: GL, mvS :: Mv, ɴs :: Ns, degs :: !(IM.IntMap Int), initial :: [Int], wkls :: Wk, stack :: [Int], alias :: !(IM.IntMap Int) } mapMv f st = st { mvS = f (mvS st) }; mapWk f st = st { wkls = f (wkls st) }; mapNs f st = st { ɴs = f (ɴs st) }
src/Asm/X86/Trans.hs view
@@ -227,7 +227,7 @@ (plN,nR) <- plI n t <- nextR; i <- nextR l <- nextL; eL <- nextL- pure $ plN $ plD $ plS $ [IAddRR () diR (absReg tD), IAddRR () siR (absReg tS), MovRI () i 0, CmpRR () i nR, Jge () eL, Label () l, MovRA () t (RSD siR Eight i ds8), MovAR () (RSD diR Eight i sS8) t, IAddRI () i 1, CmpRR () i nR, Jl () l, Label () eL]+ pure $ plN $ plD $ plS [IAddRR () diR (absReg tD), IAddRR () siR (absReg tS), MovRI () i 0, CmpRR () i nR, Jge () eL, Label () l, MovRA () t (RSD siR Eight i ds8), MovAR () (RSD diR Eight i sS8) t, IAddRI () i 1, CmpRR () i nR, Jl () l, Label () eL] ir (IR.Cpy (IR.AP tD (Just (IR.IB Op.IAsl eid (IR.ConstI 3))) _) (IR.AP tS (Just (IR.IB Op.IAsl eis (IR.ConstI 3))) _) (IR.ConstI n)) | n <= 4 = do (plD,diR) <- plI eid; (plS,siR) <- plI eis t <- nextR
src/C.hs view
@@ -57,6 +57,10 @@ pretty FRet0 = "FRet0" pretty FRet1 = "FRet1" +instance Show Temp where show=show.pretty+instance Show FTemp where show=show.pretty+instance Show BTemp where show=show.pretty+ data ArrAcc = AElem Temp CE CE (Maybe AL) Int64 -- pointer, rank, elem., label for tracking liveness, elem. size (bytes) -- TODO: more robust way to handle rank (often statically known) | ARnk Temp (Maybe AL)
src/C/Alloc.hs view
@@ -14,26 +14,38 @@ live :: [CS ()] -> [CS Liveness] live = fmap (fmap liveness) . (\(is,isns,lm) -> reconstruct is lm isns) . cfC +sus = error "Array only freed at the beginning of one branch of the conditional."+ iF :: IM.IntMap Temp -> [CS Liveness] -> [CS Liveness] iF a = gg where- gg (RA{}:cs) = gg cs- gg [s@(For l _ _ _ _ cs)] = s { body = gg cs }:fs0 l- gg [s@(While l _ _ _ cs)] = s { body = gg cs }:fs0 l- gg [s@(For1 l _ _ _ _ cs)] = s { body = gg cs }:fs0 l- gg [s@(If l _ b0 b1)] = s { iBranch = gg b0, eBranch = gg b1 }:fs0 l- gg [s@(Ifn't l _ b)] = s { branch = gg b }:fs0 l- gg [s@(Def _ _ cs)] = [s { body = gg cs }]- gg (s@(For l _ _ _ _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss- gg (s@(While l _ _ _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss- gg (s@(For1 l _ _ _ _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss- gg (s@(If l _ b0 b1):ss@(s0:_)) = s { iBranch = gg b0, eBranch = gg b1 }:fs l s0++gg ss- gg (s@(Ifn't l _ b):ss@(s0:_)) = s { branch = gg b }:fs l s0++gg ss- gg (s@(Def l _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss- gg [s] = s:fs0 (lann s)- gg (s:ss@(s0:_)) = s:fs (lann s) s0++gg ss- gg [] = []+ gg (RA{}:cs) = gg cs+ gg [s@(For l _ _ _ _ cs)] = s { body = gg cs }:fss l+ gg [s@(While l _ _ _ cs)] = s { body = gg cs }:fss l+ gg [s@(For1 l _ _ _ _ cs)] = s { body = gg cs }:fss l+ gg [s@(Ifn't l _ b@(b0:_))] = gEs l b0 [s { branch = gg b }]+ gg [s@(Ifn't l _ [])] = s:fss l+ gg [s@(If l _ [] [])] = s:fss l+ gg [s@(If l _ b0@(b00:_) [])] = gEs l b00 [s { iBranch = gg b0 }]+ gg [s@(If l _ [] b1@(b10:_))] = gEs l b10 [s { eBranch = gg b1 }]+ gg [s@(Def _ _ cs)] = [s { body = gg cs }]+ gg (s@(For l _ _ _ _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss+ gg (s@(While l _ _ _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss+ gg (s@(For1 l _ _ _ _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss+ gg (s@(If l _ b0@(b00:_) b1@(b10:_)):ss) = s { iBranch = fs l b00++gg b0, eBranch = fs l b10++gg b1 }:gg ss+ gg (s@(If l _ b0@(b00:_) _):ss@(s0:_)) = gEs l b00 $ s { iBranch = gg b0 }:fs l s0++gg ss+ gg (s@(If l _ _ b1@(b10:_)):ss@(s0:_)) = gEs l b10 $ s { eBranch = gg b1 }:fs l s0++gg ss+ gg (s@(If l _ _ _):ss@(s0:_)) = s:fs l s0++gg ss+ gg (s@(Ifn't l _ b@(b0:_)):ss@(s0:_)) = gEs l b0 $ s { branch = gg b }:fs l s0++gg ss+ gg (s@(Ifn't l _ _):ss@(s0:_)) = s:fs l s0 ++ gg ss+ gg (s@(Def l _ cs):ss@(s0:_)) = s { body = gg cs }:fs l s0++gg ss+ gg [s] = s:fss (lann s)+ gg (s:ss@(s0:_)) = s:fs (lann s) s0++gg ss+ gg [] = [] - fs0 l = [ Free t | t <- ts0 l ]- ts0 l = mapMaybe (`IM.lookup` a) (IS.toList (ins l `IS.difference` out l))+ es l s = null$ts l s+ gEs l s x = if es l s then x else sus++ fss l = [ Free t | t <- tss l ]+ tss l = mapMaybe (`IM.lookup` a) (IS.toList (ins l `IS.difference` out l)) fs l0 s1 = [ Free t | t <- ts l0 s1 ] ts l0 s1 = mapMaybe (`IM.lookup` a) (IS.toList (ins l0 `IS.difference` ins (lann s1)))
src/C/CF.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE TupleSections #-}+ module C.CF ( cfC ) where import C@@ -48,6 +50,8 @@ mC :: ([N] -> [N]) -> ControlAnn -> ControlAnn mC f (ControlAnn l ds udϵ) = ControlAnn l (f ds) udϵ +addH n = mC (n:)+ unsnoc :: [a] -> ([a], a) unsnoc [x] = ([], x) unsnoc (x:xs) = first (x:) $ unsnoc xs@@ -77,16 +81,17 @@ inspectOrder (c:cs) = node (lann c):inspectOrder cs inspectOrder [] = [] -tieBranch :: ([N] -> [N]) -> [CS ()] -> FreshM ([N] -> [N], [CS ControlAnn])-tieBranch f ss = do+tieBranch :: N -> ([N] -> [N]) -> [CS ()] -> FreshM ([N] -> [N], [CS ControlAnn])+tieBranch i f ss = do preSs <- addCF ss pure $ case uncons preSs of Just (i1, _) -> let hi=node (lann i1) (ss',l) = unsnoc preSs l' = fmap (mC f) l- ss'' = ss'++[l']- in ((hi:), ss'')+ in ((hi:),) $ case uncons ss' of+ Nothing -> ss'++[l']+ Just (hh, bs) -> let h' = fmap (addH i) hh in h':bs++[l'] Nothing -> (id, preSs) tieBody :: N -> ([N] -> [N]) -> [CS ()] -> FreshM ([N] -> [N], [CS ControlAnn])@@ -148,15 +153,16 @@ addCF (If _ p b0 b1:stmts) = do i <- getFresh (f, stmts') <- next stmts- (h0, b0') <- tieBranch f b0- (h1, b1') <- tieBranch f b1- pure $ If (ControlAnn i (f (h0 (h1 []))) udϵ) p b0' b1':stmts'+ (h0, b0') <- tieBranch i f b0+ (h1, b1') <- tieBranch i f b1+ let fnext = if null b0 || null b1 then f else id+ pure $ If (ControlAnn i (fnext (h0 (h1 []))) udϵ) p b0' b1':stmts' where udϵ = UD (uB p) IS.empty IS.empty IS.empty addCF (Ifn't _ p b:stmts) = do i <- getFresh (f, stmts') <- next stmts- (h, b') <- tieBranch f b+ (h, b') <- tieBranch i f b pure $ Ifn't (ControlAnn i (f (h [])) udϵ) p b':stmts' where udϵ = UD (uB p) IS.empty IS.empty IS.empty
src/C/Trans.hs view
@@ -104,12 +104,6 @@ mIF :: T a -> Maybe (T a) mIF (Arr _ F)=Just F; mIF (Arr _ I)=Just I; mIF _=Nothing -if1 :: T a -> Maybe (T a)-if1 (Arr (_ `Cons` Nil) I) = Just I; if1 (Arr (_ `Cons` Nil) F) = Just F; if1 _ = Nothing--if1p :: T a -> Bool-if1p t | Just{} <- if1 t = True | otherwise = False- mAA :: T a -> Maybe ((T a, Int64), (T a, Int64)) mAA (Arrow t0 t1) = (,) <$> tRnk t0 <*> tRnk t1 mAA _ = Nothing@@ -120,10 +114,18 @@ bT :: Integral b => T a -> b bT (P ts)=sum (bT<$>ts); bT F=8; bT I=8; bT B=1; bT Arr{}=8 -bSz, rSz :: Integral b => T a -> Maybe b+bSz, rSz, nSz :: Integral b => T a -> Maybe b bSz (P ts)=sum<$>traverse bSz ts; bSz F=Just 8; bSz I=Just 8; bSz B=Just 1; bSz _=Nothing rSz F=Just 8; rSz I=Just 8; rSz B=Just 1; rSz _=Nothing+nSz F=Just 8; nSz I=Just 8; nSz B=Just 1; nSz (P ts)=sum<$>traverse nSz ts; nSz _=Nothing +aB :: Integral b => T a -> Maybe b+aB (Arr (_ `Cons` Nil) t) = nSz t; aB _ = Nothing+aRr (Arr (_ `Cons` Nil) t) = rr t; aRr _ = Nothing++rr :: Integral b => T a -> Maybe (T a, b)+rr I=Just (I,8); rr F=Just (F,8); rr B=Just (B,1); rr _=Nothing+ szT = scanl' (\off ty -> off+bT ty::Int64) 0 staRnk :: Integral b => Sh a -> Maybe b@@ -135,6 +137,14 @@ eRnk sh (xR, lX) | Just i <- staRnk sh = ConstI i | otherwise = EAt (ARnk xR lX) +ev :: T a -> (Temp, Maybe AL) -> CE+ev (Arr (Ix _ i `Cons` _) _) _ = ConstI$fromIntegral i+ev _ (xR, lX) = EAt (ADim xR 0 lX)++ec :: T a -> (Temp, Maybe AL) -> CE+ec (Arr (_ `Cons` Ix _ j `Cons` _) _) _ = ConstI$fromIntegral j+ec _ (xR, lX) = EAt (ADim xR 1 lX)+ tRnk :: T a -> Maybe (T a, Int64) tRnk (Arr sh t) = (t,) <$> staRnk sh tRnk _ = Nothing@@ -164,11 +174,13 @@ ne, n1 :: T a -> Bool ne (Arr (i `Cons` _) _) = nz i; ne _=False n1 (Arr (i `Cons` _) _) = ni1 i; n1 _=False+nec (Arr (_ `Cons` i `Cons` _) _) = nz i; nec _=False nee :: T a -> Bool nee (Arr sh _) = nzSh sh; nee _=False for t = if ne t then For1 () else For (); for1 t = if n1 t then For1 () else For ()+forc t = if nec t then For1 () else For () fors t = if nee t then For1 () else For () staR :: Sh a -> [Int64]@@ -380,6 +392,12 @@ let rnk=fromIntegral$length ixs; n=product ixs loop = fors ty k 0 ILt (ConstI i) [Wr () (At td [ConstI i, 1] [Tmp k, Tmp k] (Just a) 8) (ConstI 1)] pure (Just a, Ma () a t rnk (ConstI n) 8:diml (t, Just a) (ConstI<$>ixs)++[td=:DP t rnk, loop])+aeval (Builtin ty Eye) t | (F, ixs@[i,_]) <- tRnd ty = do+ a <- nextArr t+ td <- newITemp; k <- newITemp+ let rnk=fromIntegral$length ixs; n=product ixs+ loop = fors ty k 0 ILt (ConstI i) [WrF () (At td [ConstI i, 1] [Tmp k, Tmp k] (Just a) 8) (ConstF 1)]+ pure (Just a, Ma () a t rnk (ConstI n) 8:diml (t, Just a) (ConstI<$>ixs)++[td=:DP t rnk, loop]) aeval (EApp _ (Builtin _ AddDim) x) t | F <- eAnn x = do xR <- newFTemp plX <- feval x xR@@ -396,31 +414,59 @@ let sz=last szs (a,aV) <- vSz t 1 sz pure (Just a, m'sa xR mS++plX++aV++[CpyE () (AElem t 1 0 (Just a) sz) (TupM xR Nothing) 1 sz]++m'pop mS)-aeval (EApp _ (Builtin _ AddDim) xs) t | (Arr sh ty) <- eAnn xs, nind ty = do+aeval (EApp _ (Builtin _ AddDim) xs) t | (Arr sh ty) <- eAnn xs, Just sz <- nSz ty = do (plX, (lX, xR)) <- plA xs- let sz=bT ty xRnk <- newITemp; szR <- newITemp; rnk <- newITemp a <- nextArr t pure (Just a, plX$xRnk=:eRnk sh (xR,lX):SZ () szR xR (Tmp xRnk) lX:rnk =: (Tmp xRnk+1):Ma () a t (Tmp rnk) (Tmp szR) sz: [Wr () (ADim t 0 (Just a)) 1, CpyD () (ADim t 1 (Just a)) (ADim xR 0 lX) (Tmp xRnk), CpyE () (AElem t (Tmp rnk) 0 (Just a) sz) (AElem xR (Tmp xRnk) 0 lX sz) (Tmp szR) sz])-aeval (EApp _ (Builtin _ Flat) xs) t | (Arr sh ty) <- eAnn xs, nind ty = do+aeval (EApp _ (Builtin _ Flat) xs) t | (Arr sh ty) <- eAnn xs, Just sz <- nSz ty = do (plX, (lX, xR)) <- plA xs- let sz=bT ty xRnk <- newITemp; szR <- newITemp (a,aV) <- vSz t (Tmp szR) sz pure (Just a, plX$xRnk=:eRnk sh (xR,lX):SZ () szR xR (Tmp xRnk) lX:aV++[CpyE () (AElem t 1 0 (Just a) sz) (AElem xR (Tmp xRnk) 0 lX sz) (Tmp szR) sz])-aeval (EApp _ (EApp _ (Builtin _ Map) op) e) t | (Arrow tD tC) <- eAnn op, nind tD && nind tC = do+aeval (EApp _ (EApp _ (Builtin _ Map) op) e) t | (Arrow tD tC) <- eAnn op, Just sz <- nSz tC, nind tD = do (plE, (l, xR)) <- plA e iR <- newITemp; szR <- newITemp- let sz=bT tC (a,aV) <- vSz t (Tmp szR) sz (step, pinches) <- aS op [(tD, AElem xR 1 (Tmp iR) l)] tC (AElem t 1 (Tmp iR) (Just a)) let loop=for (eAnn e) iR 0 ILt (Tmp szR) step pure (Just a, plE$- szR=:EAt (ADim xR 0 l):aV+ szR=:ev (eAnn e) (xR,l):aV ++sas pinches [loop])+aeval (EApp _ (EApp _ (Builtin _ Filt) p) xs) t | tXs@(Arr (_ `Cons` Nil) tX) <- eAnn xs, Just sz <- nSz tX = do+ a <- nextArr t+ szR <- newITemp; nR <- newITemp; b <- nBT+ (plX, (lX, xsR)) <- plA xs+ k <- newITemp+ (xR, rX, pinch) <- arg tX (AElem xsR 1 (Tmp k) lX sz)+ ss <- writeRF p [xR] (PT b)+ let step = rX:ss++[If () (Is b) [w tX (AElem t 1 (Tmp nR) (Just a) sz) xR, nR+=1] []]+ loop = for (eAnn xs) k 0 ILt (Tmp szR) step+ pure (Just a,+ plX$+ szR =: ev tXs (xsR,lX)+ :Ma () a t 1 (Tmp szR) sz+ :m'p pinch [nR=:0, loop, Wr () (ADim t 0 (Just a)) (Tmp nR)])+ where+ w ty at tt | isR ty = wt at tt+ w ty at (IT tt) | isΠ ty = CpyE () at (TupM tt Nothing) 1 (bT ty)+aeval (EApp _ (EApp _ (Builtin _ Ices) p) xs) t | tXs@(Arr (_ `Cons` Nil) tX) <- eAnn xs, Just sz <- nSz tX = do+ a <- nextArr t+ szR <- newITemp; nR <- newITemp; b <- nBT+ (plX, (lX, xsR)) <- plA xs+ k <- newITemp+ (xR, rX, pinch) <- arg tX (AElem xsR 1 (Tmp k) lX sz)+ ss <- writeRF p [xR] (PT b)+ let step = rX:ss++[If () (Is b) [Wr () (AElem t 1 (Tmp nR) (Just a) 8) (Tmp k), nR+=1] []]+ loop = for (eAnn xs) k 0 ILt (Tmp szR) step+ pure (Just a,+ plX$+ szR=:ev tXs (xsR,lX)+ :Ma () a t 1 (Tmp szR) 8+ :m'p pinch [nR=:0, loop, Wr () (ADim t 0 (Just a)) (Tmp nR)]) aeval (EApp _ (EApp _ (Builtin _ Map) f) xs) t | (Arrow tD tC) <- eAnn f, Just (_, xRnk) <- tRnk (eAnn xs), Just (ta, rnk) <- tRnk tD, Just szD <- bSz ta, Just sz <- bSz tC = do a <- nextArr t slopP <- newITemp; szR <- newITemp; slopSz <- newITemp@@ -442,7 +488,7 @@ :CpyD () (ADim t 0 (Just a)) (ADim xR 0 lX) dimsFromIn :xd=:DP xR (ConstI xRnk):i=:0 :m'p pinch- (For () k 0 ILt (Tmp szR) step:[Pop () slopE]))+ (fors (eAnn xs) k 0 ILt (Tmp szR) step:[Pop () slopE])) aeval (EApp _ (EApp _ (Builtin _ Map) f) xs) t | (Arrow tD tC) <- eAnn f, Just (_, xRnk) <- tRnk (eAnn xs), Just (ta, rnk) <- tRnk tC, Just szO <- bSz ta, isIF tD = do a <- nextArr t x <- rtemp tD; y <- newITemp; y0 <- newITemp; szX <- newITemp; szY <- newITemp@@ -465,8 +511,8 @@ :CpyD () (ADim t (ConstI xRnk) (Just a)) (ADim y0 0 lY0) (ConstI rnk) :td=:DP t (ConstI$xRnk+rnk) :j=:0- :[For () k 0 ILt (Tmp szX) step])-aeval (EApp _ (EApp _ (Builtin _ Map) f) xs) t | Just (_, xRnk) <- tRnk (eAnn xs), Just ((ta0, rnk0), (ta1, rnk1)) <- mAA (eAnn f), Just sz0 <- bSz ta0, Just sz1 <- bSz ta1 = do+ :[fors (eAnn xs) k 0 ILt (Tmp szX) step])+aeval (EApp _ (EApp _ (Builtin _ Map) f) xs) t | tX <- eAnn xs, Just (_, xRnk) <- tRnk tX, Just ((ta0, rnk0), (ta1, rnk1)) <- mAA (eAnn f), Just sz0 <- bSz ta0, Just sz1 <- bSz ta1 = do a <- nextArr t slopP <- newITemp; y <- newITemp; y0 <- newITemp szR <- newITemp; slopSz <- newITemp; szY <- newITemp@@ -494,23 +540,21 @@ :td=:DP t (ConstI oRnk) :PlProd () szY yDims :PlProd () kL xDims:i =: 0:j =: 0- :For () k 0 ILt (Tmp kL) step+ :fors tX k 0 ILt (Tmp kL) step :[Pop () slopE])-aeval (EApp _ (EApp _ (Builtin _ (Rank [(0, _)])) f) xs) t | Arr sh _ <- eAnn xs, (Arrow tX tY) <- eAnn f, nind tX && nind tY = do+aeval (EApp _ (EApp _ (Builtin _ (Rank [(0, _)])) f) xs) t | Arr sh _ <- eAnn xs, (Arrow tX tY) <- eAnn f, Just szY <- nSz tY, nind tX = do a <- nextArr t rnkR <- newITemp; szR <- newITemp i <- newITemp; xRd <- newITemp; tD <- newITemp- let szY=bT tY (plX, (lX, xR)) <- plA xs (step, pinches) <- aS f [(tX, Raw xRd (Tmp i) lX)] tY (Raw tD (Tmp i) (Just a)) let loop=for (eAnn xs) i 0 ILt (Tmp szR) step pure (Just a, plX$rnkR =: eRnk sh (xR,lX):SZ () szR xR (Tmp rnkR) lX:Ma () a t (Tmp rnkR) (Tmp szR) szY:CpyD () (ADim t 0 (Just a)) (ADim xR 0 lX) (Tmp rnkR):xRd =: DP xR (Tmp rnkR):tD =: DP t (Tmp rnkR):sas pinches [loop])-aeval (EApp _ (EApp _ (EApp _ (Builtin _ (Rank [(0, _), (0, _)])) op) xs) ys) t | Arr sh _ <- eAnn xs, Arrow tX (Arrow tY tC) <- eAnn op, nind tX && nind tY && nind tC = do+aeval (EApp _ (EApp _ (EApp _ (Builtin _ (Rank [(0, _), (0, _)])) op) xs) ys) t | Arr sh _ <- eAnn xs, Arrow tX (Arrow tY tC) <- eAnn op, Just szC <- nSz tC, nind tX && nind tY = do a <- nextArr t rnkR <- newITemp; szR <- newITemp xRd <- newITemp; yRd <- newITemp; tD <- newITemp (plX, (lX, xR)) <- plA xs; (plY, (lY, yR)) <- plA ys- let szC=bT tC i <- newITemp (step, pinches) <- aS op [(tX, Raw xRd (Tmp i) lX), (tY, Raw yRd (Tmp i) lY)] tC (Raw tD (Tmp i) (Just a)) let loop=for (eAnn xs) i 0 ILt (Tmp szR) step@@ -519,7 +563,8 @@ , Just (_, xRnk) <- tRnk (eAnn xs) , (Arrow tX (Arrow _ tCod)) <- eAnn op , Just (tC, opRnk) <- tRnk tCod- , nind tX && isIF yT && isIF tC = do+ , Just xSz <- nSz tX+ , isIF yT && isIF tC = do a <- nextArr t zR <- newITemp (plX, (lX, xR)) <- plA xs; (plY, (lY, yR)) <- plA ys@@ -534,7 +579,6 @@ allDims = zipWith (\ixϵ dt -> case ixϵ of {Cell{} -> Cell dt; Index{} -> Index dt}) allIx dts ~(oDims, complDims) = part allDims slopRnk=fromIntegral cr::Int64; oRnk=yRnk+opRnk-slopRnk- xSz=bT tX (x, pAX, pinch) <- arg tX (AElem xR (ConstI xRnk) (Tmp ix) lX xSz) (lZ, ss) <- writeF op [ra x, AA slopP Nothing] (IT zR) let ecArg = zipWith (\d tt -> case (d,tt) of (dϵ,Index{}) -> Bound dϵ; (_,Cell{}) -> Fixed) dts allIx@@ -565,7 +609,7 @@ ++[Pop () (Tmp slopE)]) aeval (EApp _ (EApp _ (Builtin _ (Rank [(cr, Just ixs)])) f) xs) t | Just (tA, rnk) <- tRnk (eAnn xs) , (Arrow _ tC) <- eAnn f- , nind tC && isIF tA = do+ , Just ySz <- nSz tC, isIF tA = do a <- nextArr t (plX, (lX, xR)) <- plA xs slopP <- newITemp@@ -578,7 +622,6 @@ allDims = zipWith (\ix dt -> case ix of {Cell{} -> Cell dt; Index{} -> Index dt}) allIx dts ~(oDims, complDims) = part allDims oRnk=rnk-fromIntegral cr; slopRnk=fromIntegral cr::Int64- ySz=bT tC (y, wY, pinch) <- rW tC (AElem t (ConstI oRnk) (Tmp di) Nothing ySz) (_, ss) <- writeF f [AA slopP Nothing] y let ecArg = zipWith (\d tt -> case (d,tt) of (dϵ,Index{}) -> Bound dϵ; (_,Cell{}) -> Fixed) dts allIx@@ -642,12 +685,12 @@ ++it=:0:loop ++[Pop () (Tmp slopE)] )-aeval (EApp _ (EApp _ (Builtin _ CatE) x) y) t | Just (ty, 1) <- tRnk (eAnn x) = do+aeval (EApp _ (EApp _ (Builtin _ CatE) x) y) t | tX <- eAnn x, Just (ty, 1) <- tRnk tX = do xnR <- newITemp; ynR <- newITemp; tn <- newITemp- (a,aV) <- v8 t (Tmp tn) let tyN=bT ty+ (a,aV) <- vSz t (Tmp tn) tyN (plX, (lX, xR)) <- plA x; (plY, (lY, yR)) <- plA y- pure (Just a, plX $ plY $ xnR =: EAt (ADim xR 0 lX):ynR =: EAt (ADim yR 0 lY):tn =: (Tmp xnR+Tmp ynR):aV++CpyE () (AElem t 1 0 (Just a) tyN) (AElem xR 1 0 lX tyN) (Tmp xnR) tyN:[CpyE () (AElem t 1 (Tmp xnR) (Just a) tyN) (AElem yR 1 0 lY tyN) (Tmp ynR) tyN])+ pure (Just a, plX $ plY $ xnR =: ev tX (xR,lX):ynR =: ev (eAnn y) (yR,lY):tn =: (Tmp xnR+Tmp ynR):aV++CpyE () (AElem t 1 0 (Just a) tyN) (AElem xR 1 0 lX tyN) (Tmp xnR) tyN:[CpyE () (AElem t 1 (Tmp xnR) (Just a) tyN) (AElem yR 1 0 lY tyN) (Tmp ynR) tyN]) aeval (EApp ty (EApp _ (EApp _ (Builtin _ IRange) start) end) (ILit _ 1)) t = do n <- newITemp; startR <- newITemp; endR <- newITemp (a,aV) <- v8 t (Tmp n)@@ -672,14 +715,14 @@ putIncr <- feval ((end `eMinus` start) `eDiv` (EApp F (Builtin (Arrow I F) ItoF) steps `eMinus` FLit F 1)) incrR let loop=for ty i 0 ILt (Tmp n) [WrF () (AElem t 1 (Tmp i) (Just a) 8) (FTmp startR), MX () startR (FTmp startR+FTmp incrR)] pure (Just a, putStart++putIncr++putN++aV++[loop])-aeval (EApp res (EApp _ (Builtin _ Cyc) xs) n) t | if1p res = do+aeval (EApp res (EApp _ (Builtin _ Cyc) xs) n) t | Just sz <- aB res = do i <- newITemp; nR <- newITemp; nO <- newITemp; szR <- newITemp- (a,aV) <- v8 t (Tmp nO)+ (a,aV) <- vSz t (Tmp nO) sz (plX, (lX, xR)) <- plA xs plN <- eval n nR ix <- newITemp- let loop=for res i 0 ILt (Tmp nR) [CpyE () (AElem t 1 (Tmp ix) (Just a) 8) (AElem xR 1 0 lX 8) (Tmp szR) 8, ix+=Tmp szR]- pure (Just a, plX $ plN ++ szR =: EAt (ADim xR 0 lX):nO =: (Tmp szR*Tmp nR):aV++ix =: 0:[loop])+ let loop=for res i 0 ILt (Tmp nR) [CpyE () (AElem t 1 (Tmp ix) (Just a) sz) (AElem xR 1 0 lX sz) (Tmp szR) sz, ix+=Tmp szR]+ pure (Just a, plX $ plN ++ szR =: ev (eAnn xs) (xR,lX):nO =: (Tmp szR*Tmp nR):aV++ix =: 0:[loop]) aeval (EApp _ (EApp _ (Builtin _ VMul) a) x) t | Just (F, [m,n]) <- tIx$eAnn a, Just s <- cLog n = do i <- newITemp; j <- newITemp; mR <- newITemp; nR <- newITemp; z <- newFTemp (aL,aV) <- v8 t (Tmp mR)@@ -697,104 +740,112 @@ :aV ++nR=:ConstI n :[loop])-aeval (EApp _ (EApp _ (Builtin _ VMul) (EApp _ (Builtin _ T) a)) x) t | f1 (eAnn x) = do+aeval (EApp _ (EApp _ (Builtin _ VMul) (EApp _ (Builtin _ T) a)) x) t | f1 tX = do i <- newITemp; j <- newITemp; m <- newITemp; n <- newITemp; z <- newFTemp (aL,aV) <- v8 t (Tmp m) (plAA, (lA, aR)) <- plA a; (plX, (lX, xR)) <- plA x- let loop = For () i 0 ILt (Tmp m)+ let loop = forc (eAnn a) i 0 ILt (Tmp m) [ MX () z 0,- for (eAnn x) j 0 ILt (Tmp n)+ for tX j 0 ILt (Tmp n) [ MX () z (FTmp z+FAt (AElem aR 2 (Tmp m*Tmp j+Tmp i) lA 8)*FAt (AElem xR 1 (Tmp j) lX 8)) ] , WrF () (AElem t 1 (Tmp i) (Just aL) 8) (FTmp z) ] pure (Just aL, plAA$ plX$- m=:EAt (ADim aR 1 lA)+ m=:ec tA (aR,lA) :aV- ++n=:EAt (ADim xR 0 lX)+ ++n=:ev tX (xR,lX) :[loop])-aeval (EApp _ (EApp _ (Builtin _ VMul) a) x) t | f1 (eAnn x) = do+ where+ tA=eAnn a; tX=eAnn x+aeval (EApp _ (EApp _ (Builtin _ VMul) a) x) t | f1 tX = do i <- newITemp; j <- newITemp; m <- newITemp; n <- newITemp; z <- newFTemp (aL,aV) <- v8 t (Tmp m) (plAA, (lA, aR)) <- plA a; (plX, (lX, xR)) <- plA x- let loop = For () i 0 ILt (Tmp m)+ let loop = for tA i 0 ILt (Tmp m) [ MX () z 0,- for (eAnn x) j 0 ILt (Tmp n)+ for tX j 0 ILt (Tmp n) [ MX () z (FTmp z+FAt (AElem aR 2 (Tmp n*Tmp i+Tmp j) lA 8)*FAt (AElem xR 1 (Tmp j) lX 8)) ] , WrF () (AElem t 1 (Tmp i) (Just aL) 8) (FTmp z) ] pure (Just aL, plAA$ plX$- m=:EAt (ADim aR 0 lA)+ m=:ev tA (aR,lA) :aV- ++n=:EAt (ADim xR 0 lX)+ ++n=:ev tX (xR,lX) :[loop])-aeval (EApp _ (EApp _ (Builtin _ Mul) (EApp _ (Builtin _ T) a)) b) t | Just (F, _) <- tRnk (eAnn a) = do+ where+ tA=eAnn a; tX=eAnn x+aeval (EApp _ (EApp _ (Builtin _ Mul) (EApp _ (Builtin _ T) a)) b) t | Just (F, _) <- tRnk tA = do aL <- nextArr t i <- newITemp; j <- newITemp; k <- newITemp; m <- newITemp; n <- newITemp; o <- newITemp; z <- newFTemp (plAA, (lA, aR)) <- plA a (plB, (lB, bR)) <- plA b- let loop=For () i 0 ILt (Tmp m)- [For () j 0 ILt (Tmp o)- [ MX () z 0, For () k 0 ILt (Tmp n)+ let loop=forc tA i 0 ILt (Tmp m)+ [forc (eAnn b) j 0 ILt (Tmp o)+ [ MX () z 0, for tA k 0 ILt (Tmp n) [MX () z (FTmp z+FAt (AElem aR 2 (Tmp k*Tmp m+Tmp i) lA 8)*FAt (AElem bR 2 (Tmp k*Tmp o+Tmp j) lB 8))] , WrF () (AElem t 2 (Tmp i*Tmp o+Tmp j) (Just aL) 8) (FTmp z)] ] pure (Just aL, plAA$ plB$- m=:EAt (ADim aR 1 lA):o=:EAt (ADim bR 1 lB)+ m=:ec tA (aR,lA):o=:ec tB (bR,lB) :Ma () aL t 2 (Tmp m*Tmp o) 8:diml (t, Just aL) [Tmp m, Tmp o]- ++n=:EAt (ADim aR 0 lA)+ ++n=:ev tA (aR,lA) :[loop])-aeval (EApp _ (EApp _ (Builtin _ Mul) a) b) t | Just (F, _) <- tRnk (eAnn a) = do+ where+ tA=eAnn a; tB=eAnn b+aeval (EApp _ (EApp _ (Builtin _ Mul) a) b) t | Just (F, _) <- tRnk tA = do aL <- nextArr t i <- newITemp; j <- newITemp; k <- newITemp; m <- newITemp; n <- newITemp; o <- newITemp; z <- newFTemp (plAA, (lA, aR)) <- plA a (plB, (lB, bR)) <- plA b- let loop=For () i 0 ILt (Tmp m)- [For () j 0 ILt (Tmp o)- [ MX () z 0, For () k 0 ILt (Tmp n)+ let loop=for tA i 0 ILt (Tmp m)+ [forc tB j 0 ILt (Tmp o)+ [ MX () z 0, for tB k 0 ILt (Tmp n) [MX () z (FTmp z+FAt (AElem aR 2 (Tmp n*Tmp i+Tmp k) lA 8)*FAt (AElem bR 2 (Tmp k*Tmp o+Tmp j) lB 8))] , WrF () (AElem t 2 (Tmp i*Tmp o+Tmp j) (Just aL) 8) (FTmp z)] ] pure (Just aL, plAA$ plB$- m=:EAt (ADim aR 0 lA):o=:EAt (ADim bR 1 lB)+ m=:ev tA (aR,lA):o=:ec tB (bR,lB) :Ma () aL t 2 (Tmp m*Tmp o) 8:diml (t, Just aL) [Tmp m, Tmp o]- ++n=:EAt (ADim bR 0 lB)+ ++n=:ev tB (bR,lB) :[loop])-aeval (EApp _ (EApp _ (Builtin _ ConsE) x) xs) t | tX <- eAnn x, isIF tX = do+ where+ tA=eAnn a; tB=eAnn b+aeval (EApp _ (EApp _ (Builtin _ ConsE) x) xs) t | tX <- eAnn x, Just sz <- rSz tX = do xR <- rtemp tX nR <- newITemp; nϵR <- newITemp- (a,aV) <- v8 t (Tmp nR)+ (a,aV) <- vSz t (Tmp nR) sz plX <- eeval x xR (plXs, (l, xsR)) <- plA xs- pure (Just a, plXs$plX++nϵR =: EAt (ADim xsR 0 l):nR =: (Tmp nϵR+1):aV++wt (AElem t 1 0 (Just a) 8) xR:[CpyE () (AElem t 1 1 (Just a) 8) (AElem xsR 1 0 l 8) (Tmp nϵR) 8])+ pure (Just a, plXs$plX++nϵR =: ev (eAnn xs) (xsR,l):nR =: (Tmp nϵR+1):aV++wt (AElem t 1 0 (Just a) sz) xR:[CpyE () (AElem t 1 1 (Just a) sz) (AElem xsR 1 0 l sz) (Tmp nϵR) sz]) aeval (EApp _ (EApp _ (Builtin _ ConsE) x) xs) t | tX <- eAnn x, isΠ tX, sz <- bT tX = do xR <- newITemp nR <- newITemp; nϵR <- newITemp (_, mSz, _, plX) <- πe x xR (plXs, (lX, xsR)) <- plA xs (a,aV) <- vSz t (Tmp nR) sz- pure (Just a, plXs$m'sa xR mSz++plX++nϵR =: EAt (ADim xsR 0 lX):nR =: (Tmp nϵR+1):aV++[CpyE () (AElem t 1 0 (Just a) sz) (TupM xR Nothing) 1 sz, CpyE () (AElem t 1 1 (Just a) sz) (AElem xsR 1 0 lX sz) (Tmp nϵR) sz]++m'pop mSz)-aeval (EApp _ (EApp _ (Builtin _ Snoc) x) xs) t | tX <- eAnn x, isIF tX = do+ pure (Just a, plXs$m'sa xR mSz++plX++nϵR =: ev (eAnn xs) (xsR,lX):nR =: (Tmp nϵR+1):aV++[CpyE () (AElem t 1 0 (Just a) sz) (TupM xR Nothing) 1 sz, CpyE () (AElem t 1 1 (Just a) sz) (AElem xsR 1 0 lX sz) (Tmp nϵR) sz]++m'pop mSz)+aeval (EApp _ (EApp _ (Builtin _ Snoc) x) xs) t | tX <- eAnn x, Just sz <- rSz tX = do xR <- rtemp tX nR <- newITemp; nϵR <- newITemp- (a,aV) <- v8 t (Tmp nR)+ (a,aV) <- vSz t (Tmp nR) sz plX <- eeval x xR (plXs, (l, xsR)) <- plA xs- pure (Just a, plXs$plX++nϵR =: EAt (ADim xsR 0 l):nR =: (Tmp nϵR+1):aV++wt (AElem t 1 (Tmp nϵR) (Just a) 8) xR:[CpyE () (AElem t 1 0 (Just a) 8) (AElem xsR 1 0 l 8) (Tmp nϵR) 8])+ pure (Just a, plXs$plX++nϵR =: ev (eAnn xs) (xsR,l):nR =: (Tmp nϵR+1):aV++wt (AElem t 1 (Tmp nϵR) (Just a) sz) xR:[CpyE () (AElem t 1 0 (Just a) sz) (AElem xsR 1 0 l sz) (Tmp nϵR) sz]) aeval (EApp _ (EApp _ (Builtin _ Snoc) x) xs) t | tX <- eAnn x, isΠ tX, sz <- bT tX = do xR <- newITemp nR <- newITemp; nϵR <- newITemp (_, mSz, _, plX) <- πe x xR (plXs, (lX, xsR)) <- plA xs (a,aV) <- vSz t (Tmp nR) sz- pure (Just a, plXs$m'sa xR mSz++plX++nϵR =: EAt (ADim xsR 0 lX):nR =: (Tmp nϵR+1):aV++[CpyE () (AElem t 1 (Tmp nϵR) (Just a) sz) (TupM xR Nothing) 1 sz, CpyE () (AElem t 1 0 (Just a) sz) (AElem xsR 1 0 lX sz) (Tmp nϵR) sz]++m'pop mSz)+ pure (Just a, plXs$m'sa xR mSz++plX++nϵR =: ev (eAnn xs) (xsR,lX):nR =: (Tmp nϵR+1):aV++[CpyE () (AElem t 1 (Tmp nϵR) (Just a) sz) (TupM xR Nothing) 1 sz, CpyE () (AElem t 1 0 (Just a) sz) (AElem xsR 1 0 lX sz) (Tmp nϵR) sz]++m'pop mSz) aeval (EApp ty (EApp _ (Builtin _ Re) n) x) t | tX <- eAnn x, Just xSz <- rSz tX = do xR <- rtemp tX; nR <- newITemp (a,aV) <- vSz t (Tmp nR) xSz@@ -823,24 +874,31 @@ :plN ++Ma () a t (Tmp oRnk) (Tmp szX*Tmp nR) sz:Wr () (ADim t 0 (Just a)) (Tmp nR):CpyD () (ADim t 1 (Just a)) (ADim xR 0 lX) (Tmp xRnk) :[loop])-aeval (EApp oTy (Builtin _ Init) x) t | if1p oTy = do+aeval (EApp oTy (Builtin _ Init) x) t | Just sz <- aB oTy = do nR <- newITemp- (a,aV) <- v8 t (Tmp nR)+ (a,aV) <- vSz t (Tmp nR) sz (plX, (lX, xR)) <- plA x- pure (Just a, plX$nR =: (EAt (ADim xR 0 lX)-1):aV++[CpyE () (AElem t 1 0 (Just a) 8) (AElem xR 1 0 lX 8) (Tmp nR) 8])-aeval (EApp oTy (Builtin _ Tail) x) t | if1p oTy = do+ pure (Just a, plX$nR =: (ev (eAnn x) (xR,lX)-1):aV++[CpyE () (AElem t 1 0 (Just a) sz) (AElem xR 1 0 lX sz) (Tmp nR) sz])+aeval (EApp oTy (Builtin _ InitM) x) t | Just sz <- aB oTy = do nR <- newITemp- (a,aV) <- v8 t (Tmp nR)+ (a,aV) <- vSz t (Bin IMax (Tmp nR) 0) sz (plX, (lX, xR)) <- plA x- pure (Just a, plX$nR =: (EAt (ADim xR 0 lX)-1):aV++[CpyE () (AElem t 1 0 (Just a) 8) (AElem xR 1 1 lX 8) (Tmp nR) 8])-aeval (EApp ty (EApp _ (EApp _ (Builtin _ Zip) op) xs) ys) t | (Arrow tX (Arrow tY tC)) <- eAnn op, nind tX && nind tY && nind tC = do+ pure (Just a,+ plX$+ nR =: (ev (eAnn x) (xR,lX)-1)+ :aV++[CpyE () (AElem t 1 0 (Just a) sz) (AElem xR 1 0 lX sz) (Tmp nR) sz])+aeval (EApp oTy (Builtin _ Tail) x) t | Just sz <- aB oTy = do+ nR <- newITemp+ (a,aV) <- vSz t (Tmp nR) sz+ (plX, (lX, xR)) <- plA x+ pure (Just a, plX$nR =: (ev (eAnn x) (xR,lX)-1):aV++[CpyE () (AElem t 1 0 (Just a) sz) (AElem xR 1 1 lX sz) (Tmp nR) sz])+aeval (EApp ty (EApp _ (EApp _ (Builtin _ Zip) op) xs) ys) t | (Arrow tX (Arrow tY tC)) <- eAnn op, Just zSz <- nSz tC, nind tX && nind tY = do nR <- newITemp; i <- newITemp- let zSz=bT tC (a,aV) <- vSz t (Tmp nR) zSz (plEX, (lX, aPX)) <- plA xs; (plEY, (lY, aPY)) <- plA ys (step, pinches) <- aS op [(tX, AElem aPX 1 (Tmp i) lX), (tY, AElem aPY 1 (Tmp i) lY)] tC (AElem t 1 (Tmp i) (Just a)) let loop=for ty i 0 ILt (Tmp nR) step- pure (Just a, plEX$plEY$nR =: EAt (ADim aPX 0 lX):aV++sas pinches [loop])+ pure (Just a, plEX$plEY$nR =: ev (eAnn xs) (aPX,lX):aV++sas pinches [loop]) aeval (EApp _ (EApp _ (EApp _ (Builtin _ ScanS) op) seed) e) t | (Arrow tX (Arrow tY _)) <- eAnn op, isIF tX && isIF tY = do acc <- rtemp tX; x <- rtemp tY i <- newITemp; n <- newITemp@@ -850,7 +908,7 @@ ss <- writeRF op [acc, x] acc let loopBody=wt (AElem t 1 (Tmp i) (Just a) 8) acc:mt (AElem aP 1 (Tmp i) l 8) x:ss loop=for (eAnn e) i 0 ILt (Tmp n) loopBody- pure (Just a, plE$plS++n =: (EAt (ADim aP 0 l)+1):aV++[loop])+ pure (Just a, plE$plS++n =: (ev (eAnn e) (aP,l)+1):aV++[loop]) aeval (EApp _ (EApp _ (Builtin _ Scan) op) xs) t | (Arrow tAcc (Arrow tX _)) <- eAnn op, isIF tAcc && isIF tX = do acc <- rtemp tAcc; x <- rtemp tX i <- newITemp; n <- newITemp@@ -859,30 +917,32 @@ ss <- writeRF op [acc, x] acc let loopBody=wt (AElem t 1 (Tmp i-1) (Just a) 8) acc:mt (AElem aP 1 (Tmp i) l 8) x:ss loop=for1 (eAnn xs) i 1 ILeq (Tmp n) loopBody- pure (Just a, plE$n =: EAt (ADim aP 0 l):aV++mt (AElem aP 1 0 l 8) acc:[loop])-aeval (EApp oTy (EApp _ (Builtin _ (DI n)) op) xs) t | Just ot <- if1 oTy, if1p (eAnn xs) = do+ pure (Just a, plE$n =: ev (eAnn xs) (aP,l):aV++mt (AElem aP 1 0 l 8) acc:[loop])+aeval (EApp oTy (EApp _ (Builtin _ (DI n)) op) xs) t | Just (ot, oSz) <- aRr oTy, Just xSz <- aB (eAnn xs) = do slopP <- newITemp szR <- newITemp; sz'R <- newITemp; i <- newITemp fR <- rtemp ot- (a,aV) <- v8 t (Tmp sz'R)+ (a,aV) <- vSz t (Tmp sz'R) xSz (_, ss) <- writeF op [AA slopP Nothing] fR- let szSlop=fromIntegral$16+8*n+ let szSlop=fromIntegral$16+fromIntegral oSz*n (plX, (lX, aP)) <- plA xs let sz'=Tmp szR-fromIntegral(n-1)- let loopBody=CpyE () (AElem slopP 1 0 Nothing 8) (AElem aP 1 (Tmp i) lX 8) (fromIntegral n) 8:ss++[wt (AElem t 1 (Tmp i) (Just a) 8) fR]+ let loopBody=CpyE () (AElem slopP 1 0 Nothing xSz) (AElem aP 1 (Tmp i) lX xSz) (fromIntegral n) xSz:ss++[wt (AElem t 1 (Tmp i) (Just a) oSz) fR] loop=for oTy i 0 ILt (Tmp sz'R) loopBody- pure (Just a, plX$szR =: EAt (ADim aP 0 lX):sz'R =: sz':aV++Sa () slopP szSlop:Wr () (ARnk slopP Nothing) 1:Wr () (ADim slopP 0 Nothing) (fromIntegral n):loop:[Pop () szSlop])-aeval (EApp _ (EApp _ (Builtin _ Rot) n) xs) t | if1p (eAnn xs) = do+ pure (Just a, plX$szR =: ev (eAnn xs) (aP,lX):sz'R =: sz':aV++Sa () slopP szSlop:Wr () (ARnk slopP Nothing) 1:Wr () (ADim slopP 0 Nothing) (fromIntegral n):loop:[Pop () szSlop])+ -- TODO: not just I,F+aeval (EApp _ (EApp _ (Builtin _ Rot) n) xs) t | tXs <- eAnn xs, Just sz <- aB tXs = do nR <- newITemp; c <- newITemp; szR <- newITemp plN <- eval n nR (plX, (lX, xsR)) <- plA xs- (a, aV) <- v8 t (Tmp szR)- pure (Just a, plX$plN++szR =: EAt (ADim xsR 0 lX):aV++Ifn't () (IRel IGeq (Tmp nR) 0) [nR+=Tmp szR]:c =: (Tmp szR-Tmp nR):[CpyE () (AElem t 1 0 (Just a) 8) (AElem xsR 1 (Tmp nR) lX 8) (Tmp c) 8, CpyE () (AElem t 1 (Tmp c) (Just a) 8) (AElem xsR 1 0 lX 8) (Tmp nR) 8])+ (a, aV) <- vSz t (Tmp szR) sz+ pure (Just a, plX$plN++szR =: ev tXs (xsR,lX):aV++Ifn't () (IRel IGeq (Tmp nR) 0) [nR+=Tmp szR]:c =: (Tmp szR-Tmp nR):[CpyE () (AElem t 1 0 (Just a) sz) (AElem xsR 1 (Tmp nR) lX sz) (Tmp c) sz, CpyE () (AElem t 1 (Tmp c) (Just a) sz) (AElem xsR 1 0 lX sz) (Tmp nR) sz]) aeval (Id _ (AShLit ns es)) t | Just ws <- mIFs es = do let rnk=fromIntegral$length ns n <- nextAA modify (addAA n (rnk:fmap fromIntegral ns++ws)) pure (Nothing, [t =: LA n])+ -- TODO: boolean lits aeval (EApp _ (Builtin _ T) x) t | Just (ty, ixes) <- tIx (eAnn x), rnk <- fromIntegral$length ixes, any (isJust.cLog) ixes = do a <- nextArr t let sze=bT ty; rnkE=ConstI rnk@@ -905,19 +965,17 @@ is <- traverse (\_ -> newITemp) [1..rnk] let loop=thread (zipWith (\i tt -> (:[]) . For () i 0 ILt (Tmp tt)) is dts) [CpyE () (At td (Tmp<$>dstrides) (Tmp<$>reverse is) (Just a) sze) (At xd (Tmp<$>sstrides) (Tmp<$>is) l sze) 1 sze] pure (Just a, plX$plDs++plSs++Ma () a t (ConstI rnk) (Tmp n) sze:diml (t, Just a) (Tmp<$>reverse dts)++init plSd++xd =: (Tmp xR+dO):td =: (Tmp t+dO):loop)-aeval (EApp _ (EApp _ (EApp _ (Builtin _ Outer) op) xs) ys) t | (Arrow tX (Arrow tY tC)) <- eAnn op, nind tX && nind tY && nind tC = do+aeval (EApp _ (EApp _ (EApp _ (Builtin _ Outer) op) xs) ys) t | (Arrow tX (Arrow tY tC)) <- eAnn op, Just zSz <- nSz tC, nind tX && nind tY = do a <- nextArr t szX <- newITemp; szY <- newITemp; i <- newITemp; j <- newITemp; k <- newITemp- let zSz=bT tC (plX, (lX, xR)) <- plA xs; (plY, (lY, yR)) <- plA ys (step, pinches) <- aS op [(tX ,AElem xR 1 (Tmp i) lX), (tY, AElem yR 1 (Tmp j) lY)] tC (AElem t 2 (Tmp k) (Just a)) let loop=for (eAnn xs) i 0 ILt (Tmp szX) [for (eAnn ys) j 0 ILt (Tmp szY) (step++[k+=1])]- pure (Just a, plX$plY$szX =: EAt (ADim xR 0 lX):szY =: EAt (ADim yR 0 lY):Ma () a t 2 (Tmp szX*Tmp szY) zSz:diml (t, Just a) [Tmp szX, Tmp szY]++k=:0:sas pinches [loop])-aeval (EApp _ (EApp _ (EApp _ (Builtin _ Outer) op) xs) ys) t | (Arrow tX (Arrow tY tC)) <- eAnn op, Arr sh tEC <- tC, nind tX && nind tY && nind tEC = do+ pure (Just a, plX$plY$szX =: ev (eAnn xs) (xR,lX):szY =: ev (eAnn ys) (yR,lY):Ma () a t 2 (Tmp szX*Tmp szY) zSz:diml (t, Just a) [Tmp szX, Tmp szY]++k=:0:sas pinches [loop])+aeval (EApp _ (EApp _ (EApp _ (Builtin _ Outer) op) xs) ys) t | (Arrow tX (Arrow tY tC)) <- eAnn op, Arr sh tEC <- tC, Just szXT <- nSz tX, Just szYT <- nSz tY, Just szZT <- nSz tEC = do a <- nextArr t szX <- newITemp; szY <- newITemp; szZ <- newITemp; i <- newITemp; j <- newITemp; k <- newITemp rnkZ <- newITemp; rnkO <- newITemp- let szXT=bT tX; szYT=bT tY; szZT=bT tEC z <- newITemp; z0 <- newITemp (plX, (lX, xR)) <- plA xs; (plY, (lY, yR)) <- plA ys (x, wX, pinchX) <- arg tX (AElem xR 1 (Tmp i) lX szXT)@@ -935,34 +993,41 @@ ++rnkZ=:eRnk sh (z0,lZ0) :rnkO=:(Tmp rnkZ+2) :SZ () szZ z0 (Tmp rnkZ) lZ0- :szX=:EAt (ADim xR 0 lX)- :szY=:EAt (ADim yR 0 lY)+ :szX=:ev (eAnn xs) (xR,lX)+ :szY=:ev (eAnn ys) (yR,lY) :Ma () a t (Tmp rnkO) (Tmp szX*Tmp szY*Tmp szZ) szZT :diml (t, Just a) [Tmp szX, Tmp szY] ++[CpyD () (ADim t 2 (Just a)) (ADim z0 0 lZ0) (Tmp rnkZ), k=:0, loop] ))-aeval (EApp ty (EApp _ (Builtin _ Succ) op) xs) t | Arrow tX (Arrow _ tZ) <- eAnn op, nind tX && nind tZ = do+aeval (EApp ty (EApp _ (Builtin _ Succ) op) xs) t | Arrow tX (Arrow _ tZ) <- eAnn op, Just zSz <- nSz tZ, nind tX = do szR <- newITemp; sz'R <- newITemp- let zSz=bT tZ (a,aV) <- vSz t (Tmp sz'R) zSz (plX, (lX, xR)) <- plA xs i <- newITemp (step, pinches) <- aS op [(tX, AElem xR 1 (Tmp i+1) lX), (tX, AElem xR 1 (Tmp i) lX)] tZ (AElem t 1 (Tmp i) (Just a)) let loop=for ty i 0 ILt (Tmp sz'R) step- pure (Just a, plX$szR =: EAt (ADim xR 0 lX):sz'R =: (Tmp szR-1):aV++sas pinches [loop])-aeval (EApp oTy (Builtin _ RevE) e) t | Just ty <- if1 oTy = do- n <- newITemp; i <- newITemp; o <- rtemp ty- (a,aV) <- v8 t (Tmp n)+ pure (Just a, plX$szR =: ev (eAnn xs) (xR,lX):sz'R =: (Tmp szR-1):aV++sas pinches [loop])+aeval (EApp oTy (Builtin _ RevE) e) t | Just sz <- aB oTy = do+ n <- newITemp; i <- newITemp+ (a,aV) <- vSz t (Tmp n) sz (plE, (lE, eR)) <- plA e- let loop=for oTy i 0 ILt (Tmp n) [mt (AElem eR 1 (Tmp n-Tmp i-1) lE 8) o, wt (AElem t 1 (Tmp i) (Just a) 8) o]- pure (Just a, plE$n =: EAt (ADim eR 0 lE):aV++[loop])-aeval (EApp oTy (EApp _ (EApp _ (Builtin _ Gen) seed) op) n) t | Just ty <- if1 oTy = do+ let loop=for oTy i 0 ILt (Tmp n) [CpyE () (AElem t 1 (Tmp i) (Just a) sz) (AElem eR 1 (Tmp n-Tmp i-1) lE sz) 1 sz]+ pure (Just a, plE$n =: ev oTy (eR,lE):aV++[loop])+aeval (EApp _ (Builtin _ RevE) e) t | tys <- eAnn e, Just (ty, rnk) <- tRnk tys = do+ a <- nextArr t+ n <- newITemp; i <- newITemp; szA <- newITemp+ (plE, (lE, eR)) <- plA e+ let sz=bT ty; rnkE=ConstI rnk+ (dts, plDs) <- plDim rnk (eR, lE)+ let loop = for ty i 0 ILt (Tmp n) [CpyE () (AElem t rnkE (Tmp i*Tmp szA) (Just a) sz) (AElem eR rnkE ((Tmp n-Tmp i-1)*Tmp szA) lE sz) (Tmp szA) sz]+ pure (Just a, plE$n=:ev ty (eR,lE):tail plDs++PlProd () szA (Tmp<$>tail dts):Ma () a t rnkE (Tmp n*Tmp szA) sz:CpyD () (ADim t 0 (Just a)) (ADim eR 0 lE) rnkE:[loop])+aeval (EApp oTy (EApp _ (EApp _ (Builtin _ Gen) seed) op) n) t | tyS <- eAnn seed, Just sz <- rSz tyS = do nR <- newITemp; plN <- eval n nR; i <- newITemp- acc <- rtemp ty+ acc <- rtemp tyS plS <- eeval seed acc- (a,aV) <- v8 t (Tmp nR)+ (a,aV) <- vSz t (Tmp nR) sz ss <- writeRF op [acc] acc- let loop=for oTy i 0 ILt (Tmp nR) (wt (AElem t 1 (Tmp i) (Just a) 8) acc:ss)+ let loop=for oTy i 0 ILt (Tmp nR) (wt (AElem t 1 (Tmp i) (Just a) sz) acc:ss) pure (Just a, plS++plN++aV++[loop]) aeval (EApp ty (EApp _ (EApp _ (Builtin _ Gen) seed) op) n) t | isΠR (eAnn seed) = do nR <- newITemp; plN <- eval n nR; i <- newITemp@@ -1044,6 +1109,9 @@ plA e = do {t <- newITemp; (lX,plX) <- aeval e t; pure ((plX++), (lX, t))} peval :: E (T ()) -> BTemp -> CM [CS ()]+peval (LLet _ b e) t = do+ ss <- llet b+ (ss++) <$> peval e t peval (BLit _ b) t = pure [MB () t (BConst b)] peval (EApp _ (Builtin _ Odd) e0) t = do (pl,eR) <- plEV e0@@ -1071,7 +1139,7 @@ ss <- writeRF op [PT acc, PT x] (PT acc) let loopBody=MB () x (PAt (AElem aP 1 (Tmp i) l 1)):ss loop=for1 (eAnn e) i 1 ILt (Tmp szR) loopBody- pure $ plE$szR =: EAt (ADim aP 0 l):MB () acc (PAt (AElem aP 1 0 l 1)):[loop]+ pure $ plE$szR =: ev (eAnn e) (aP,l):MB () acc (PAt (AElem aP 1 0 l 1)):[loop] peval (EApp _ (EApp _ (EApp _ (Builtin _ FoldS) op) seed) e) acc | (Arrow _ (Arrow tY _)) <- eAnn op, Just szY <- rSz tY = do x <- rtemp tY szR <- newITemp@@ -1081,7 +1149,14 @@ ss <- writeRF op [PT acc, x] (PT acc) let loopBody=mt (AElem aP 1 (Tmp i) l szY) x:ss loop=for (eAnn e) i 0 ILt (Tmp szR) loopBody- pure $ plE $ plAcc++szR=:EAt (ADim aP 0 l):[loop]+ pure $ plE $ plAcc++szR=:ev (eAnn e) (aP,l):[loop]+peval (EApp _ (Builtin _ Head) xs) t = do+ (plX, (l, a)) <- plA xs+ pure $ plX [MB () t (PAt (AElem a 1 0 l 1))]+peval (EApp _ (Builtin _ Last) xs) t = do+ (plX, (l, a)) <- plA xs+ pure $ plX [MB () t (PAt (AElem a 1 (ev (eAnn xs) (a,l)-1) l 1))]+peval e _ = error (show e) eval :: E (T ()) -> Temp -> CM [CS ()] eval (LLet _ b e) t = do@@ -1094,6 +1169,15 @@ eval (EApp _ (EApp _ (Builtin _ A.R) e0) e1) t = do (plE0,e0e) <- plC e0; (plE1,e1e) <- plC e1 pure $ plE0 $ plE1 [Rnd () t, t =: (Bin IRem (Tmp t) (e1e-e0e+1) + e0e)]+eval (EApp _ (EApp _ (Builtin _ Fold) op) e) acc | (Arrow tX _) <- eAnn op, isI tX = do+ x <- newITemp+ szR <- newITemp+ i <- newITemp+ (plE, (l, aP)) <- plA e+ ss <- writeRF op [IT acc, IT x] (IT acc)+ let loopBody=x=:EAt (AElem aP 1 (Tmp i) l 8):ss+ loop=for1 (eAnn e) i 1 ILt (Tmp szR) loopBody+ pure $ plE$szR =: ev (eAnn e) (aP,l):acc =: EAt (AElem aP 1 0 l 8):[loop] eval (EApp _ (EApp _ (EApp _ (Builtin _ FoldS) op) seed) e) acc | (Arrow _ (Arrow tX _)) <- eAnn op, Just xSz <- rSz tX = do x <- rtemp tX szR <- newITemp@@ -1103,7 +1187,7 @@ ss <- writeRF op [IT acc, x] (IT acc) let loopBody=mt (AElem eR 1 (Tmp i) l xSz) x:ss loop=for (eAnn e) i 0 ILt (Tmp szR) loopBody- pure $ plE$plAcc++szR =: EAt (ADim eR 0 l):[loop]+ pure $ plE$plAcc++szR =: ev (eAnn e) (eR,l):[loop] eval (EApp I (EApp _ (Builtin _ op) e0) e1) t | Just cop <- mOp op = do (pl0,e0e) <- plC e0; (pl1,e1e) <- plC e1 pure $ pl0 $ pl1 [t =: Bin cop e0e e1e]@@ -1128,7 +1212,7 @@ pure $ plX [t =: EAt (AElem a 1 0 l 8)] eval (EApp _ (Builtin _ Last) xs) t = do (plX, (l, a)) <- plA xs- pure $ plX [t =: EAt (AElem a 1 (EAt (ADim a 0 l)-1) l 8)]+ pure $ plX [t =: EAt (AElem a 1 (ev (eAnn xs) (a,l)-1) l 8)] eval (EApp _ (Builtin _ Size) xs) t | Just (_, 1) <- tRnk (eAnn xs) = do (plE, (l, xsR)) <- plA xs pure $ plE [t =: EAt (ADim xsR 0 l)]@@ -1149,15 +1233,14 @@ k <- newITemp (offs, a, _, plT) <- πe e k pure $ m'sa t a++plT ++ t =: EAt (Raw k (ConstI$offs!!(i-1)) Nothing 1):m'pop a-eval (EApp _ (EApp _ (Builtin _ IOf) p) xs) t | (Arrow tD _) <- eAnn p, nind tD = do+eval (EApp _ (EApp _ (Builtin _ IOf) p) xs) t | (Arrow tD _) <- eAnn p, Just szX <- nSz tD = do pR <- nBT szR <- newITemp; i <- newITemp; done <- newITemp (plX, (lX, xsR)) <- plA xs- let szX=bT tD (x, wX, pinch) <- arg tD (AElem xsR 1 (Tmp i) lX szX) ss <- writeRF p [x] (PT pR) let loop=While () done INeq 1 (wX:ss++[If () (Is pR) [t=:Tmp i, done=:1] [], i+=1, Cmov () (IRel IGeq (Tmp i) (Tmp szR)) done 1])- pure $ plX $ szR=:EAt (ADim xsR 0 lX):t=:(-1):done=:0:i=:0:m'p pinch [loop]+ pure $ plX $ szR=:ev (eAnn xs) (xsR,lX):t=:(-1):done=:0:i=:0:m'p pinch [loop] eval (EApp _ (EApp _ (EApp _ (Builtin _ Iter) f) n) x) t = do (plN,nR) <- plC n plX <- eval x t@@ -1166,26 +1249,26 @@ let loop=For () i 0 ILt nR ss pure $ plX++plN [loop] eval (Cond _ p e0 e1) t = snd <$> cond p e0 e1 (IT t)-eval (Id _ (FoldOfZip zop op [p])) acc | Just tP <- if1 (eAnn p) = do+eval (Id _ (FoldOfZip zop op [p])) acc | Just (tP, pSz) <- aRr (eAnn p) = do x <- rtemp tP szR <- newITemp i <- newITemp (plPP, (lP, pR)) <- plA p ss <- writeRF op [IT acc, x] (IT acc)- let step = mt (AElem pR 1 (Tmp i) lP 8) x:ss+ let step = mt (AElem pR 1 (Tmp i) lP pSz) x:ss loop = for1 (eAnn p) i 1 ILt (Tmp szR) step sseed <- writeRF zop [x] (IT acc)- pure $ plPP$szR =: EAt (ADim pR 0 lP):mt (AElem pR 1 0 lP 8) x:sseed++[loop]-eval (Id _ (FoldOfZip zop op [p, q])) acc | Just tP <- if1 (eAnn p), Just tQ <- if1 (eAnn q) = do+ pure $ plPP$szR =:ev (eAnn p) (pR,lP):mt (AElem pR 1 0 lP pSz) x:sseed++[loop]+eval (Id _ (FoldOfZip zop op [p, q])) acc | tPs <- eAnn p, Just (tP, pSz) <- aRr tPs, Just (tQ, qSz) <- aRr (eAnn q) = do x <- rtemp tP; y <- rtemp tQ szR <- newITemp i <- newITemp (plPP, (lP, pR)) <- plA p; (plQ, (lQ, qR)) <- plA q ss <- writeRF op [IT acc, x, y] (IT acc)- let step = mt (AElem pR 1 (Tmp i) lP 8) x:mt (AElem qR 1 (Tmp i) lQ 8) y:ss+ let step = mt (AElem pR 1 (Tmp i) lP pSz) x:mt (AElem qR 1 (Tmp i) lQ qSz) y:ss loop = for1 (eAnn p) i 1 ILt (Tmp szR) step seed <- writeRF zop [x,y] (IT acc)- pure $ plPP$plQ$szR =: EAt (ADim pR 0 lP):mt (AElem pR 1 0 lP 8) x:mt (AElem qR 1 0 lQ 8) y:seed++[loop]+ pure $ plPP$plQ$szR =: ev tPs (pR,lP):mt (AElem pR 1 0 lP pSz) x:mt (AElem qR 1 0 lQ qSz) y:seed++[loop] eval e _ = error (show e) frel :: Builtin -> Maybe FRel@@ -1198,7 +1281,7 @@ mB And=Just AndB;mB Or=Just OrB;mB Xor=Just XorB; mB _=Nothing mOp :: Builtin -> Maybe IBin-mOp Plus=Just IPlus;mOp Times=Just ITimes;mOp Minus=Just IMinus; mOp Mod=Just IRem; mOp Sl=Just IAsl;mOp Sr=Just IAsr;mOp a=BI<$>mB a+mOp Plus=Just IPlus;mOp Times=Just ITimes;mOp Minus=Just IMinus; mOp Mod=Just IRem; mOp Sl=Just IAsl;mOp Sr=Just IAsr;mOp A.IDiv=Just Op.IDiv;mOp a=BI<$>mB a mFun :: Builtin -> Maybe FUn mFun Sqrt=Just FSqrt; mFun Log=Just FLog; mFun Sin=Just FSin; mFun Cos=Just FCos; mFun Abs=Just FAbs; mFun _=Nothing@@ -1286,18 +1369,18 @@ pure $ plE $ plI [MX () t (FAt (AElem eR 1 iR lE 8))] feval (EApp _ (Builtin _ Last) xs) t = do (plX, (l, a)) <- plA xs- pure $ plX [MX () t (FAt (AElem a 1 (EAt (ADim a 0 l)-1) l 8))]-feval (Id _ (FoldOfZip zop op [p])) acc | Just tP <- if1 (eAnn p) = do+ pure $ plX [MX () t (FAt (AElem a 1 (ev (eAnn xs) (a,l)-1) l 8))]+feval (Id _ (FoldOfZip zop op [p])) acc | tPs <- eAnn p, Just (tP, pSz) <- aRr tPs = do x <- rtemp tP szR <- newITemp i <- newITemp (plPP, (lP, pR)) <- plA p ss <- writeRF op [FT acc, x] (FT acc)- let step = mt (AElem pR 1 (Tmp i) lP 8) x:ss+ let step = mt (AElem pR 1 (Tmp i) lP pSz) x:ss loop = for1 (eAnn p) i 1 ILt (Tmp szR) step sseed <- writeRF zop [x] (FT acc)- pure $ plPP$szR =: EAt (ADim pR 0 lP):mt (AElem pR 1 0 lP 8) x:sseed++[loop]-feval (Id _ (FoldOfZip zop op [EApp _ (EApp _ (EApp _ (Builtin _ FRange) (FLit _ start)) (FLit _ end)) (ILit _ steps), ys])) acc | Just tQ <- if1 (eAnn ys) = do+ pure $ plPP$szR =: ev tPs (pR,lP):mt (AElem pR 1 0 lP pSz) x:sseed++[loop]+feval (Id _ (FoldOfZip zop op [EApp _ (EApp _ (EApp _ (Builtin _ FRange) (FLit _ start)) (FLit _ end)) (ILit _ steps), ys])) acc | Just (tQ, qSz) <- aRr (eAnn ys) = do x <- newFTemp; y <- rtemp tQ incrR <- newFTemp; i <- newITemp plY <- eeval (EApp tQ (Builtin undefined Head) ys) y@@ -1305,8 +1388,8 @@ plIncr <- feval (FLit F$(end-start)/realToFrac (steps-1)) incrR seed <- writeRF zop [FT x, y] (FT acc) ss <- writeRF op [FT acc, FT x, y] (FT acc)- pure $ plYs $ plY ++ MX () x (ConstF start):seed ++ plIncr ++ [for1 (eAnn ys) i 1 ILt (ConstI$fromIntegral steps) (mt (AElem yR 1 (Tmp i) lY 8) y:MX () x (FTmp x+FTmp incrR):ss)]-feval (Id _ (FoldOfZip zop op [EApp _ (EApp _ (EApp _ (Builtin _ FRange) start) end) steps, ys])) acc | Just tQ <- if1 (eAnn ys) = do+ pure $ plYs $ plY ++ MX () x (ConstF start):seed ++ plIncr ++ [for1 (eAnn ys) i 1 ILt (ConstI$fromIntegral steps) (mt (AElem yR 1 (Tmp i) lY qSz) y:MX () x (FTmp x+FTmp incrR):ss)]+feval (Id _ (FoldOfZip zop op [EApp _ (EApp _ (EApp _ (Builtin _ FRange) start) end) steps, ys])) acc | Just (tQ, qSz) <- aRr (eAnn ys) = do x <- newFTemp; y <- rtemp tQ incrR <- newFTemp; n <- newITemp; i <- newITemp plX <- feval start x; plY <- eeval (EApp tQ (Builtin undefined Head) ys) y@@ -1315,8 +1398,8 @@ plIncr <- feval ((end `eMinus` start) `eDiv` (EApp F (Builtin (Arrow I F) ItoF) steps `eMinus` FLit F 1)) incrR seed <- writeRF zop [FT x, y] (FT acc) ss <- writeRF op [FT acc, FT x, y] (FT acc)- pure $ plYs $ plY ++ plX ++ seed ++ plIncr ++ plN ++ [for1 (eAnn ys) i 1 ILt (Tmp n) (mt (AElem yR 1 (Tmp i) lY 8) y:MX () x (FTmp x+FTmp incrR):ss)]-feval (Id _ (FoldOfZip zop op [EApp _ (EApp _ (EApp _ (Builtin _ IRange) start) _) incr, ys])) acc | Just tQ <- if1 (eAnn ys) = do+ pure $ plYs $ plY ++ plX ++ seed ++ plIncr ++ plN ++ [for1 (eAnn ys) i 1 ILt (Tmp n) (mt (AElem yR 1 (Tmp i) lY qSz) y:MX () x (FTmp x+FTmp incrR):ss)]+feval (Id _ (FoldOfZip zop op [EApp _ (EApp _ (EApp _ (Builtin _ IRange) start) _) incr, ys])) acc | Just (tQ, qSz) <- aRr (eAnn ys) = do x <- newITemp; y <- rtemp tQ szR <- newITemp; i <- newITemp plX <- eval start x; plY <- eeval (EApp tQ (Builtin undefined Head) ys) y@@ -1324,17 +1407,17 @@ (plI,iE) <- plC incr seed <- writeRF zop [IT x, y] (FT acc) ss <- writeRF op [FT acc, IT x, y] (FT acc)- pure $ plYs $ plY ++ plX ++ seed ++ plI (szR =: EAt (ADim yR 0 lY):[for1 (eAnn ys) i 1 ILt (Tmp szR) (mt (AElem yR 1 (Tmp i) lY 8) y:x+=iE:ss)])-feval (Id _ (FoldOfZip zop op [p, q])) acc | Just tP <- if1 (eAnn p), Just tQ <- if1 (eAnn q) = do+ pure $ plYs $ plY ++ plX ++ seed ++ plI (szR =: ev (eAnn ys) (yR,lY):[for1 (eAnn ys) i 1 ILt (Tmp szR) (mt (AElem yR 1 (Tmp i) lY qSz) y:x+=iE:ss)])+feval (Id _ (FoldOfZip zop op [p, q])) acc | tPs <- eAnn p, Just (tP, pSz) <- aRr tPs, Just (tQ, qSz) <- aRr (eAnn q) = do x <- rtemp tP; y <- rtemp tQ szR <- newITemp i <- newITemp (plPP, (lP, pR)) <- plA p; (plQ, (lQ, qR)) <- plA q ss <- writeRF op [FT acc, x, y] (FT acc)- let step = mt (AElem pR 1 (Tmp i) lP 8) x:mt (AElem qR 1 (Tmp i) lQ 8) y:ss+ let step = mt (AElem pR 1 (Tmp i) lP pSz) x:mt (AElem qR 1 (Tmp i) lQ qSz) y:ss loop = for1 tP i 1 ILt (Tmp szR) step seed <- writeRF zop [x,y] (FT acc)- pure $ plPP$plQ$szR =: EAt (ADim pR 0 lP):mt (AElem pR 1 0 lP 8) x:mt (AElem qR 1 0 lQ 8) y:seed++[loop]+ pure $ plPP$plQ$szR =: ev tPs (pR,lP):mt (AElem pR 1 0 lP pSz) x:mt (AElem qR 1 0 lQ qSz) y:seed++[loop] feval (EApp _ (EApp _ (Builtin _ Fold) op) e) acc | (Arrow tX _) <- eAnn op, isF tX = do x <- newFTemp szR <- newITemp@@ -1343,7 +1426,7 @@ ss <- writeRF op [FT acc, FT x] (FT acc) let loopBody=MX () x (FAt (AElem aP 1 (Tmp i) l 8)):ss loop=for1 (eAnn e) i 1 ILt (Tmp szR) loopBody- pure $ plE$szR =: EAt (ADim aP 0 l):MX () acc (FAt (AElem aP 1 0 l 8)):[loop]+ pure $ plE$szR =: ev (eAnn e) (aP,l):MX () acc (FAt (AElem aP 1 0 l 8)):[loop] feval (EApp _ (EApp _ (EApp _ (Builtin _ Foldl) op) seed) e) acc | (Arrow _ (Arrow tX _)) <- eAnn op, isIF tX = do x <- rtemp tX i <- newITemp@@ -1352,7 +1435,7 @@ ss <- writeRF op [x, FT acc] (FT acc) let loopBody=mt (AElem eR 1 (Tmp i) l 8) x:ss++[i =: (Tmp i-1)] loop=While () i IGeq 0 loopBody- pure $ plE $ plAcc++i =: (EAt (ADim eR 0 l)-1):[loop]+ pure $ plE $ plAcc++i =: (ev (eAnn e) (eR,l)-1):[loop] feval (EApp _ (EApp _ (EApp _ (Builtin _ FoldA) op) seed) xs) acc | Arr sh _ <- eAnn xs, (Arrow _ (Arrow tX _)) <- eAnn op, isIF tX = do x <- rtemp tX rnkR <- newITemp; szR <- newITemp; k <- newITemp@@ -1387,7 +1470,7 @@ ss <- writeRF op [FT acc, x] (FT acc) let loopBody=mt (AElem eR 1 (Tmp i) l xSz) x:ss loop=for (eAnn e) i 0 ILt (Tmp szR) loopBody- pure $ plE $ plAcc++szR =: EAt (ADim eR 0 l):[loop]+ pure $ plE $ plAcc++szR =: ev (eAnn e) (eR,l):[loop] feval (EApp _ (EApp _ (EApp _ (Builtin _ Iter) f) n) x) t = do (plN,nR) <- plC n plX <- feval x t@@ -1429,7 +1512,7 @@ πe (EApp (P tys) (Builtin _ Last) xs) t | offs <- szT tys, sz <- last offs, szE <- ConstI sz = do xR <- newITemp (lX, plX) <- aeval xs xR- pure (offs, Just szE, [], plX++[CpyE () (TupM t Nothing) (AElem xR 1 (EAt (ADim xR 0 lX)-1) lX sz) 1 sz])+ pure (offs, Just szE, [], plX++[CpyE () (TupM t Nothing) (AElem xR 1 (ev (eAnn xs) (xR,lX)-1) lX sz) 1 sz]) πe (Tup (P tys) es) t | offs <- szT tys, sz <- last offs, szE <- ConstI sz = do (ls, ss) <- unzip <$> zipWithM (\e off ->
src/IR.hs view
@@ -72,6 +72,7 @@ | Sa Temp Exp -- register, size | Pop Exp -- pop salloc | Cpy AE AE Exp+ | Cpy1 AE AE Exp | C Label | R Label | IRnd Temp | FRnd FTemp @@ -92,6 +93,7 @@ pretty (Sa t e) = parens ("salloc" <+> pretty t <+> ":" <+> pretty e) pretty (Pop e) = parens ("spop" <+> pretty e) pretty (Cpy p p' e) = parens ("cpy" <+> pretty p <> "," <+> pretty p' <+> pretty e)+ pretty (Cpy1 p p' e) = parens ("cpy-byte" <+> pretty p <> "," <+> pretty p' <+> pretty e) pretty (C l) = parens ("call" <+> prettyLabel l) pretty R{} = parens "ret" <> hardline pretty (IRnd t) = parens (pretty t <+> "<- rnd")
src/IR/C.hs view
@@ -81,6 +81,7 @@ cToIRM (CpyD _ a0 a1 e) = pure [Cpy (irAt a0) (irAt a1) (irE e)] cToIRM (CpyE _ a0 a1 e 8) = pure [Cpy (irAt a0) (irAt a1) (irE e)] cToIRM (CpyE _ a0 a1 e sz) | (s,0) <- sz `quotRem` 8 = pure [Cpy (irAt a0) (irAt a1) (irE e*IR.ConstI s)]+cToIRM (CpyE _ a0 a1 e sz) = pure [Cpy1 (irAt a0) (irAt a1) (irE e*IR.ConstI sz)] cToIRM (C.Sa _ t e) = pure [IR.Sa (ctemp t) (irE e)] cToIRM (C.Pop _ e) = pure [IR.Pop (irE e)] cToIRM (Ifn't _ p s) = do
src/IR/CF.hs view
@@ -170,6 +170,7 @@ uses C{} = IS.empty uses (Cset _ e) = uE e uses (Cpy a0 a1 e) = uA a0<>uA a1<>uE e+uses (Cpy1 a0 a1 e) = uA a0<>uA a1<>uE e defs (MT t _) = singleton t defs (IRnd t) = singleton t@@ -180,27 +181,28 @@ defs _ = IS.empty usesF, defsF :: Stmt -> IS.IntSet-usesF IRnd{} = IS.empty-usesF FRnd{} = IS.empty-usesF (MX _ e) = uF e-usesF L{} = IS.empty-usesF J{} = IS.empty-usesF MJ{} = IS.empty-usesF (MT _ e) = uFF e-usesF (Ma _ _ e) = uFF e-usesF Free{} = IS.empty-usesF RA{} = IS.empty-usesF (Cmov e _ e') = uFF e<>uFF e'-usesF (Fcmov e _ x) = uFF e<>uF x-usesF (Wr a e) = uAF a<>uFF e-usesF (WrF a x) = uAF a<>uF x-usesF (WrB a e) = uAF a<>uFF e-usesF (Cset _ e) = uFF e-usesF (Sa _ e) = uFF e-usesF (Pop e) = uFF e-usesF C{} = IS.empty-usesF R{} = IS.empty-usesF (Cpy a0 a1 e) = uAF a0<>uAF a1<>uFF e+usesF IRnd{} = IS.empty+usesF FRnd{} = IS.empty+usesF (MX _ e) = uF e+usesF L{} = IS.empty+usesF J{} = IS.empty+usesF MJ{} = IS.empty+usesF (MT _ e) = uFF e+usesF (Ma _ _ e) = uFF e+usesF Free{} = IS.empty+usesF RA{} = IS.empty+usesF (Cmov e _ e') = uFF e<>uFF e'+usesF (Fcmov e _ x) = uFF e<>uF x+usesF (Wr a e) = uAF a<>uFF e+usesF (WrF a x) = uAF a<>uF x+usesF (WrB a e) = uAF a<>uFF e+usesF (Cset _ e) = uFF e+usesF (Sa _ e) = uFF e+usesF (Pop e) = uFF e+usesF C{} = IS.empty+usesF R{} = IS.empty+usesF (Cpy a0 a1 e) = uAF a0<>uAF a1<>uFF e+usesF (Cpy1 a0 a1 e) = uAF a0<>uAF a1<>uFF e defsF (MX t _) = fsingleton t defsF (Fcmov _ x _) = fsingleton x
src/IR/Hoist.hs view
@@ -48,27 +48,28 @@ mapFF f (FConv e) = FConv (mapFE f e) mapF :: (FTemp -> FTemp) -> Stmt -> Stmt-mapF f (MX t e) = MX (f t) (mapFF f e)-mapF _ s@L{} = s-mapF _ s@C{} = s-mapF _ s@R{} = s-mapF _ s@IRnd{} = s-mapF f (FRnd t) = FRnd (f t)-mapF _ s@J{} = s-mapF _ s@Free{} = s-mapF _ s@RA{} = s-mapF f (MT t e) = MT t (mapFE f e)-mapF f (Wr a e) = Wr (mapFA f a) (mapFE f e)-mapF f (WrF a x) = WrF (mapFA f a) (mapFF f x)-mapF f (WrB a e) = WrB (mapFA f a) (mapFE f e)-mapF f (Fcmov e t x) = Fcmov (mapFE f e) (f t) (mapFF f x)-mapF f (MJ e l) = MJ (mapFE f e) l-mapF f (Ma l t e) = Ma l t (mapFE f e)-mapF f (Sa t e) = Sa t (mapFE f e)-mapF f (Pop e) = Pop (mapFE f e)-mapF f (Cpy a0 a1 e) = Cpy (mapFA f a0) (mapFA f a1) (mapFE f e)-mapF f (Cmov p t e) = Cmov (mapFE f p) t (mapFE f e)-mapF f (Cset t p) = Cset t (mapFE f p)+mapF f (MX t e) = MX (f t) (mapFF f e)+mapF _ s@L{} = s+mapF _ s@C{} = s+mapF _ s@R{} = s+mapF _ s@IRnd{} = s+mapF f (FRnd t) = FRnd (f t)+mapF _ s@J{} = s+mapF _ s@Free{} = s+mapF _ s@RA{} = s+mapF f (MT t e) = MT t (mapFE f e)+mapF f (Wr a e) = Wr (mapFA f a) (mapFE f e)+mapF f (WrF a x) = WrF (mapFA f a) (mapFF f x)+mapF f (WrB a e) = WrB (mapFA f a) (mapFE f e)+mapF f (Fcmov e t x) = Fcmov (mapFE f e) (f t) (mapFF f x)+mapF f (MJ e l) = MJ (mapFE f e) l+mapF f (Ma l t e) = Ma l t (mapFE f e)+mapF f (Sa t e) = Sa t (mapFE f e)+mapF f (Pop e) = Pop (mapFE f e)+mapF f (Cpy a0 a1 e) = Cpy (mapFA f a0) (mapFA f a1) (mapFE f e)+mapF f (Cpy1 a0 a1 e) = Cpy1 (mapFA f a0) (mapFA f a1) (mapFE f e)+mapF f (Cmov p t e) = Cmov (mapFE f p) t (mapFE f e)+mapF f (Cset t p) = Cset t (mapFE f p) type Loop = (N, IS.IntSet)
src/IR/Opt.hs view
@@ -27,8 +27,9 @@ (e0', e1') -> IB IPlus e0' e1' optE (IB IMinus e0 e1) = case (optE e0, optE e1) of- (e0', ConstI 0) -> e0'- (e0', e1') -> IB IMinus e0' e1'+ (ConstI i0, ConstI i1) -> ConstI$i0-i1+ (e0', ConstI 0) -> e0'+ (e0', e1') -> IB IMinus e0' e1' optE (IB IAsl e0 e1) = case (optE e0, optE e1) of (ConstI i0, ConstI i1) -> ConstI$i0 `shiftL` fromIntegral i1@@ -82,6 +83,7 @@ opt :: Stmt -> Stmt opt (Cpy s d n) = Cpy (optP s) (optP d) (optE n)+opt (Cpy1 s d n) = Cpy1 (optP s) (optP d) (optE n) opt (MT r e) = MT r (optE e) opt (Ma l t e) = Ma l t (optE e) opt (Wr p e) = Wr (optP p) (optE e)
src/L.x view
@@ -104,6 +104,7 @@ "+" { mkSym Plus } "-" { mkSym Minus } "^" { mkSym Caret }+ "/." { mkSym IDiv } "/" { mkSym Fold } "/ₒ" { mkSym FoldS }@@ -149,7 +150,9 @@ "}." { mkSym Last } "}.?" { mkSym LastM } "{:" { mkSym Tail }+ "{:?" { mkSym TailM } "}:" { mkSym Init }+ "}:?" { mkSym InitM } ⊲ { mkSym Cons } "<|" { mkSym Cons } ⊳ { mkSym Snoc }@@ -178,7 +181,9 @@ "|" { mkSym Mod } "@." { mkSym AtDot } ℘ { mkSym Weier }+ ⩪ { mkSym Ice } § { mkSym Para }+ "#." { mkSym Para } 👁️ { mkSym Eye } "eye." { mkSym Eye } ♭ { mkSym B }@@ -223,6 +228,7 @@ M { mkBuiltin BuiltinM } float { mkBuiltin BuiltinFloat } int { mkBuiltin BuiltinInt }+ bool { mkBuiltin BuiltinBool } 𝔯 { mkBuiltin BuiltinR } "rand." { mkBuiltin BuiltinR } "sin." { mkBuiltin BuiltinSin }@@ -300,17 +306,18 @@ | CondSplit | Cor | ArrL | ArrR | SymLog | LBind | PolyBind | LRank | Compose | Arrow | Sig | MaxS | MinS | DIS | Succ | Conv | Access { iat :: !Int } | TSig | Cons | Snoc | Do | Tensor | Transp | PlusPlus | Rotate- | Last | LastM | Head | HeadM | Tail | Init+ | Last | LastM | Head | HeadM | Tail | TailM | Init | InitM | Geq | Gt | Eq | Neq | Leq | Lt | FoldA | FoldS | Tilde | Cyc | A1 | Mod- | AtDot | Eye | Para | Weier | B | Sharp- | And | Or | Xor | Not | Sr | Sl+ | AtDot | Eye | Para | Weier | Ice | B | Sharp+ | And | Or | Xor | Not | Sr | Sl | IDiv deriving (Generic, NFData) instance Pretty Sym where pretty Plus = "+" pretty Minus = "-" pretty Percent = "%"+ pretty IDiv = "/." pretty Fold = "/" pretty FoldS = "/ₒ" pretty Foldl = "/l"@@ -370,7 +377,9 @@ pretty Tilde = "~" pretty PlusPlus = "⧺" pretty Tail = "{:"+ pretty TailM = "{:?" pretty Init = "}:"+ pretty InitM = "}:?" pretty Rotate = "⊖" pretty Cyc = "⊙" pretty A1 = "˙"@@ -384,6 +393,7 @@ pretty Or = "∨" pretty Not = "¬" pretty Weier = "℘"+ pretty Ice = "⩪" pretty Para = "§" pretty IxTimes = "×" pretty Sr = ">>"@@ -402,7 +412,7 @@ | BuiltinMMul | BuiltinArr | BuiltinInt | BuiltinFloat | BuiltinT | BuiltinR | BuiltinSin | BuiltinCos | BuiltinScanS | BuiltinTan | BuiltinVMul | BuiltinCyc | BuiltinOdd | BuiltinEven | BuiltinAbs- | BuiltinD | BuiltinVec | BuiltinM+ | BuiltinD | BuiltinVec | BuiltinM | BuiltinBool deriving (Generic, NFData) instance Pretty Builtin where@@ -429,6 +439,7 @@ pretty BuiltinM = "M" pretty BuiltinInt = "int" pretty BuiltinFloat = "float"+ pretty BuiltinBool = "bool" pretty BuiltinT = "𝓉" pretty BuiltinR = "𝔯" pretty BuiltinSin = "sin."
src/Parser.y view
@@ -65,7 +65,9 @@ head { TokSym $$ L.Head } headM { TokSym $$ L.HeadM } tail { TokSym $$ L.Tail }+ tailM { TokSym $$ L.TailM } init { TokSym $$ L.Init }+ initM { TokSym $$ L.InitM } do { TokSym $$ Do } tensor { TokSym $$ Tensor } geq { TokSym $$ Geq }@@ -88,6 +90,7 @@ minus { TokSym $$ L.Minus } times { TokSym $$ L.Times } percent { TokSym $$ Percent }+ idiv { TokSym $$ L.IDiv } caret { TokSym $$ Caret } max { TokSym $$ MaxS } min { TokSym $$ MinS }@@ -100,7 +103,8 @@ iat { TokSym $$ L.A1 } mod { TokSym $$ L.Mod } atDot { TokSym $$ AtDot }- weier { TokSym $$ Weier }+ -- weier { TokSym $$ Weier }+ ice { TokSym $$ Ice } para { TokSym $$ Para } eye { TokSym $$ L.Eye } @@ -146,6 +150,7 @@ vec { TokB $$ BuiltinVec } matrix { TokB $$ BuiltinM } int { TokB $$ BuiltinInt }+ bool { TokB $$ BuiltinBool } float { TokB $$ BuiltinFloat } scanS { TokB $$ BuiltinScanS } scan { TokB $$ BuiltinScan }@@ -206,8 +211,7 @@ | vec I T { Arr ($2 `A.Cons` Nil) $3 } | matrix six comma six T { Arr ((Ix (loc $2) (six $2)) `A.Cons` (Ix (loc $4) (six $4)) `A.Cons` Nil) $5 } | matrix T {% do {i <- lift $ freshName "i"; j <- lift $ freshName "j"; pure $ Arr (IVar $1 i `A.Cons` IVar $1 j `A.Cons` Nil) $2 } }- | int { I }- | float { F }+ | int { I } | bool { A.B } | float { F } | parens(T) { $1 } | T arrow T { A.Arrow $1 $3 } @@ -219,6 +223,7 @@ BBin :: { E AlexPosn } : plus { Builtin $1 A.Plus } | minus { Builtin $1 A.Minus } | times { Builtin $1 A.Times } | percent { Builtin $1 Div }+ | idiv { Builtin $1 A.IDiv } | caret { Builtin $1 IntExp } | max { Builtin $1 Max } | min { Builtin $1 Min } | scan { Builtin $1 Scan }@@ -245,7 +250,7 @@ | atDot { Builtin $1 IOf } | and { Builtin $1 A.And } | or { Builtin $1 A.Or } | xor { Builtin $1 A.Xor }- | weier { Builtin $1 Ices }+ | ice { Builtin $1 Ices } | para { Builtin $1 Filt } | sr { Builtin $1 A.Sr } | sl { Builtin $1 A.Sl } @@ -290,8 +295,8 @@ | f { Builtin $1 Fib } | last { Builtin $1 A.Last } | lastM { Builtin $1 A.LastM } | head { Builtin $1 A.Head } | headM { Builtin $1 A.HeadM }- | tail { Builtin $1 A.Tail }- | init { Builtin $1 A.Init }+ | tail { Builtin $1 A.Tail } | tailM { Builtin $1 A.TailM }+ | init { Builtin $1 A.Init } | initM { Builtin $1 A.InitM } | re { Builtin $1 Re } | diag { Builtin $1 Di } | question E condSplit E condSplit E { Cond $1 $2 $4 $6 }
src/Parser/Rw.hs view
@@ -26,7 +26,9 @@ isBinOp Outer = False isBinOp R = False isBinOp Tail = False+isBinOp TailM = False isBinOp Init = False+isBinOp InitM = False isBinOp Even = False isBinOp Odd = False isBinOp Abs = False@@ -43,6 +45,7 @@ fi Mul =7 fi Plus = 6; fi Minus = 6 fi And = 3; fi Or = 2; fi Xor = 6+fi Ices = 6; fi Filt=6 fi Map{} = 5 fi ConsE = 4; fi Snoc = 4 fi Eq = 4; fi Neq = 4; fi Gt = 4
src/Ty.hs view
@@ -15,7 +15,7 @@ import Control.Exception (Exception, throw) import Control.Monad (zipWithM) import Control.Monad.Except (liftEither, throwError)-import Control.Monad.State.Strict (StateT (runStateT), gets, modify)+import Control.Monad.State.Strict (StateT (runStateT), gets, modify, state) import Data.Bifunctor (first, second) import Data.Containers.ListUtils (nubOrd) import Data.Foldable (traverse_)@@ -53,8 +53,8 @@ | OI a (I a) (I a) | ExistentialArg (T ()) | MatchFailed (T ()) (T ())- | MatchShFailed (Sh ()) (Sh ())- | MatchIFailed a (I a) (I a)+ | MatchShFailed (Sh a) (Sh a)+ | MatchIFailed (I a) (I a) | Doesn'tSatisfy a (T a) C deriving (Generic) @@ -78,7 +78,7 @@ pretty (ExistentialArg ty) = "Existential occurs as an argument in" <+> squotes (pretty ty) pretty (MatchFailed t t') = "Failed to match" <+> squotes (pretty t) <+> "against type" <+> squotes (pretty t') pretty (MatchShFailed sh sh') = "Failed to match" <+> squotes (pretty sh) <+> "against shape" <+> squotes (pretty sh')- pretty (MatchIFailed l i i') = pretty l <> ":" <+> "failed to match" <+> squotes (pretty i) <+> "against index" <+> squotes (pretty i')+ pretty (MatchIFailed i i') = "Failed to match" <+> squotes (pretty i) <+> "against index" <+> squotes (pretty i') pretty (Doesn'tSatisfy l ty c) = pretty l <+> squotes (pretty ty) <+> "is not a member of class" <+> pretty c instance (Pretty a) => Show (TyE a) where@@ -98,43 +98,56 @@ (<#*>) x y = x <> hardline <> indent 2 y type TyM a = StateT (TySt a) (Either (TyE a))+type UM a = StateT Int (Either (TyE a)) -mI :: I a -> I a -> Either (TyE a) (Subst a)-mI i0@(Ix l i) i1@(Ix _ j) | i == j = Right mempty- | otherwise = Left $ MatchIFailed l i0 i1-mI (IVar _ (Nm _ (U i) _)) ix = Right $ Subst IM.empty (IM.singleton i ix) IM.empty-mI ix (IVar _ (Nm _ (U i) _)) = Right $ Subst IM.empty (IM.singleton i ix) IM.empty-mI (IEVar _ n) (IEVar _ n') | n == n' = Right mempty-mI (StaPlus _ i (Ix _ iϵ)) (Ix l j) | j >= iϵ = mI i (Ix l (j-iϵ))-mI (Ix l iϵ) (StaPlus _ i (Ix _ j)) | iϵ >= j = mI i (Ix l (iϵ-j))-mI (StaPlus _ i j) (StaPlus _ i' j') = (<>) <$> mI i i' <*> mI j j' -- FIXME: too stringent-mI (StaMul _ i j) (StaMul _ i' j') = (<>) <$> mI i i' <*> mI j j' -- FIXME: too stringent+nI :: a -> UM b (I a)+nI l = state (\i -> let j=i+1 in (IEVar l (Nm "m" (U j) l), j)) -mSh :: Sh a -> Sh a -> Either (TyE a) (Subst a)-mSh (SVar (Nm _ (U i) _)) sh = Right $ Subst IM.empty IM.empty (IM.singleton i sh)-mSh Nil Nil = Right mempty-mSh (Cons i sh) (Cons i' sh') = (<>) <$> mI i i' <*> mSh sh sh'-mSh (Cat sh0 sh1) (Cat sh0' sh1') = (<>) <$> mSh sh0 sh0' <*> mSh sh1 sh1'-mSh (Rev sh) (Rev sh') = mSh sh sh'-mSh sh sh' = Left $ MatchShFailed (void sh) (void sh')+liftU :: UM a x -> TyM a x+liftU a = do+ i <- gets maxU+ (b, j) <- liftEither$runStateT a i+ modify (setMaxU j) $> b +mI :: Focus -> I a -> I a -> Either (TyE a) (Subst a)+mI _ i0@(Ix _ i) i1@(Ix _ j) | i == j = Right mempty+ | otherwise = Left $ MatchIFailed i0 i1+mI _ (IVar _ (Nm _ (U i) _)) ix = Right $ Subst IM.empty (IM.singleton i ix) IM.empty+mI _ ix (IVar _ (Nm _ (U i) _)) = Right $ Subst IM.empty (IM.singleton i ix) IM.empty+mI _ (IEVar _ n) (IEVar _ n') | n == n' = Right mempty+mI RF IEVar{} IEVar{} = Right mempty+-- TODO: Ix should match against ∃+mI _ i0@IEVar{} i1@IEVar{} = Left $ MatchIFailed i0 i1+mI f (StaPlus _ i (Ix _ iϵ)) (Ix l j) | j >= iϵ = mI f i (Ix l (j-iϵ))+mI f (Ix l iϵ) (StaPlus _ i (Ix _ j)) | iϵ >= j = mI f i (Ix l (iϵ-j))+mI f (StaPlus _ i j) (StaPlus _ i' j') = (<>) <$> mI f i i' <*> mI f j j' -- FIXME: too stringent+mI f (StaMul _ i j) (StaMul _ i' j') = (<>) <$> mI f i i' <*> mI f j j' -- FIXME: too stringent++mSh :: Focus -> Sh a -> Sh a -> Either (TyE a) (Subst a)+mSh _ (SVar (Nm _ (U i) _)) sh = Right $ Subst IM.empty IM.empty (IM.singleton i sh)+mSh _ Nil Nil = Right mempty+mSh f (Cons i sh) (Cons i' sh') = (<>) <$> mI f i i' <*> mSh f sh sh'+mSh f (Cat sh0 sh1) (Cat sh0' sh1') = (<>) <$> mSh f sh0 sh0' <*> mSh f sh1 sh1'+mSh f (Rev sh) (Rev sh') = mSh f sh sh'+mSh _ sh sh' = Left $ MatchShFailed sh sh'+ match :: (Typeable a, Pretty a) => T a -> T a -> Subst a-match t t' = either throw id (maM t t')+match t t' = either throw id (maM LF t t') -maM :: T a -> T a -> Either (TyE a) (Subst a)-maM I I = Right mempty-maM F F = Right mempty-maM B B = Right mempty-maM (TVar n) (TVar n') | n == n' = Right mempty-maM (TVar (Nm _ (U i) _)) t = Right $ Subst (IM.singleton i t) IM.empty IM.empty-maM (Arrow t0 t1) (Arrow t0' t1') = (<>) <$> maM t0 t0' <*> maM t1 t1' -- FIXME: use <\> over <>-maM (Arr sh t) (Arr sh' t') = (<>) <$> mSh sh sh' <*> maM t t'-maM (Arr sh t) t' = (<>) <$> mSh sh Nil <*> maM t t'-maM (P ts) (P ts') = mconcat <$> zipWithM maM ts ts'-maM (Ρ n _) (Ρ n' _) | n == n' = Right mempty-maM (Ρ n rs) t@(Ρ _ rs') | IM.keysSet rs' `IS.isSubsetOf` IM.keysSet rs = mapTySubst (insert n t) . mconcat <$> traverse (uncurry maM) (IM.elems (IM.intersectionWith (,) rs rs'))-maM (Ρ n rs) t@(P ts) | length ts >= fst (IM.findMax rs) = mapTySubst (IM.insert (unU$unique n) t) . mconcat <$> traverse (uncurry maM) [ (ts!!(i-1),tϵ) | (i,tϵ) <- IM.toList rs ]-maM t t' = Left $ MatchFailed (void t) (void t')+maM :: Focus -> T a -> T a -> Either (TyE a) (Subst a)+maM _ I I = Right mempty+maM _ F F = Right mempty+maM _ B B = Right mempty+maM _ (TVar n) (TVar n') | n == n' = Right mempty+maM _ (TVar (Nm _ (U i) _)) t = Right $ Subst (IM.singleton i t) IM.empty IM.empty+maM _ (Arrow t0 t1) (Arrow t0' t1') = (<>) <$> maM LF t0 t0' <*> maM RF t1 t1' -- FIXME: use <\> over <>+maM f (Arr sh t) (Arr sh' t') = (<>) <$> mSh f sh sh' <*> maM f t t'+maM f (Arr sh t) t' = (<>) <$> mSh f sh Nil <*> maM f t t'+maM f (P ts) (P ts') = mconcat <$> zipWithM (maM f) ts ts'+maM _ (Ρ n _) (Ρ n' _) | n == n' = Right mempty+maM f (Ρ n rs) t@(Ρ _ rs') | IM.keysSet rs' `IS.isSubsetOf` IM.keysSet rs = mapTySubst (insert n t) . mconcat <$> traverse (uncurry (maM f)) (IM.elems (IM.intersectionWith (,) rs rs'))+maM f (Ρ n rs) t@(P ts) | length ts >= fst (IM.findMax rs) = mapTySubst (IM.insert (unU$unique n) t) . mconcat <$> traverse (uncurry (maM f)) [ (ts!!(i-1),tϵ) | (i,tϵ) <- IM.toList rs ]+maM _ t t' = Left $ MatchFailed (void t) (void t') shSubst :: Subst a -> Sh a -> Sh a shSubst _ Nil = Nil@@ -219,73 +232,96 @@ ftv :: T.Text -> TyM a (T ()) ftv n = ft n () +fti :: T.Text -> TyM a (I ())+fti n = IVar () <$> freshN n ()++ftie :: TyM a (I ())+ftie = IEVar () <$> freshN "n" ()+ mapTySubst f (Subst t i sh) = Subst (f t) i sh mapShSubst f (Subst t i sh) = Subst t i (f sh) -mguIPrep :: IM.IntMap (I a) -> I a -> I a -> Either (TyE a) (IM.IntMap (I a))-mguIPrep is i0 i1 =+data Focus = LF | RF++instance Pretty Focus where pretty LF="⦠"; pretty RF="∢"++mguIPrep :: Focus -> IM.IntMap (I a) -> I a -> I a -> UM a (I a, IM.IntMap (I a))+mguIPrep f is i0 i1 = let i0' = is !> i0 i1' = is !> i1- in mguI is (rwI i0') (rwI i1')+ in mguI f is (rwI i0') (rwI i1') -mguI :: IM.IntMap (I a) -> I a -> I a -> Either (TyE a) (IM.IntMap (I a))-mguI inp i0@(Ix l i) i1@(Ix _ j) | i == j = Right inp- | otherwise = Left$ UI l i0 i1-mguI inp i0@(IEVar l i) i1@(IEVar _ j) | i == j = Right inp- | otherwise = Left $ UI l i0 i1-mguI inp (IVar _ i) (IVar _ j) | i == j = Right inp-mguI inp iix@(IVar l (Nm _ (U i) _)) ix | i `IS.member` occI ix = Left $ OI l iix ix- | otherwise = Right $ IM.insert i ix inp-mguI inp ix iix@(IVar l (Nm _ (U i) _)) | i `IS.member` occI ix = Left$ OI l ix iix- | otherwise = Right $ IM.insert i ix inp-mguI inp (StaPlus _ i0 (Ix _ k0)) (StaPlus _ i1 (Ix _ k1)) | k0 == k1 = mguIPrep inp i0 i1-mguI inp (StaMul _ i0 (Ix _ k0)) (StaMul _ i1 (Ix _ k1)) | k0 == k1 = mguIPrep inp i0 i1-mguI inp i0@(StaPlus l i (Ix _ k)) i1@(Ix lk j) | j >= k = mguIPrep inp i (Ix lk (j-k))- | otherwise = Left $ UI l i0 i1-mguI inp i0@Ix{} i1@(StaPlus _ _ Ix{}) = mguIPrep inp i1 i0-mguI inp (StaMul _ i0 i1) (StaMul _ j0 j1) = do+mguI :: Focus -> IM.IntMap (I a) -> I a -> I a -> UM a (I a, IM.IntMap (I a))+mguI _ inp i0@(Ix _ i) (Ix _ j) | i == j = pure (i0, inp)+mguI RF inp (Ix l _) Ix{} = do {m <- nI l; pure (m, inp)}+mguI _ _ i0@(Ix l _) i1@Ix{} = throwError $ UI l i0 i1+mguI _ inp i0@(IEVar _ i) (IEVar _ j) | i == j = pure (i0, inp)+mguI RF inp (IEVar l _) (IEVar _ _) = do {m <- nI l; pure (m, inp)}+mguI _ _ i0@(IEVar l _) i1@IEVar{} = throwError $ UI l i0 i1+mguI _ inp i0@(IVar _ i) (IVar _ j) | i == j = pure (i0, inp)+mguI _ inp iix@(IVar l (Nm _ (U i) _)) ix | i `IS.member` occI ix = throwError $ OI l iix ix+ | otherwise = pure (ix, IM.insert i ix inp)+mguI _ inp ix iix@(IVar l (Nm _ (U i) _)) | i `IS.member` occI ix = throwError $ OI l ix iix+ | otherwise = pure (ix, IM.insert i ix inp)+mguI f inp (StaPlus _ i0 (Ix _ k0)) (StaPlus _ i1 (Ix _ k1)) | k0 == k1 = mguIPrep f inp i0 i1+mguI f inp (StaMul _ i0 (Ix _ k0)) (StaMul _ i1 (Ix _ k1)) | k0 == k1 = mguIPrep f inp i0 i1+mguI f inp i0@(StaPlus l i (Ix _ k)) i1@(Ix lk j) | j >= k = mguIPrep f inp i (Ix lk (j-k))+ | otherwise = throwError $ UI l i0 i1+mguI f inp i0@Ix{} i1@(StaPlus _ _ Ix{}) = mguIPrep f inp i1 i0+mguI f inp (StaPlus l i0 i1) (StaPlus _ j0 j1) = do -- FIXME: too stringent- s <- mguIPrep inp i0 j0- mguIPrep s i1 j1-mguI _ i0@(IEVar l _) i1@Ix{} = Left $ UI l i0 i1-mguI _ i0@(Ix l _) i1@IEVar{} = Left $ UI l i0 i1-mguI _ i0@(IEVar l _) i1@StaPlus{} = Left $ UI l i0 i1-mguI _ i0@(StaPlus l _ _) i1@IEVar{} = Left $ UI l i0 i1-mguI _ i0 i1 = error (show (i0,i1))+ (k, s) <- mguIPrep f inp i0 j0+ (m, s') <- mguIPrep f s i1 j1+ pure (StaPlus l k m, s')+mguI f inp (StaMul l i0 i1) (StaMul _ j0 j1) = do+ -- FIXME: too stringent+ (k, s) <- mguIPrep f inp i0 j0+ (m, s') <- mguIPrep f s i1 j1+ pure (StaMul l k m, s')+mguI _ _ i0@(IEVar l _) i1@Ix{} = throwError $ UI l i0 i1+mguI _ _ i0@(Ix l _) i1@IEVar{} = throwError $ UI l i0 i1+mguI _ _ i0@(IEVar l _) i1@StaPlus{} = throwError $ UI l i0 i1 -- TODO: focus case+mguI _ _ i0@(StaPlus l _ _) i1@IEVar{} = throwError $ UI l i0 i1+mguI _ _ i0 i1 = error (show (i0,i1)) -mgShPrep :: a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)-mgShPrep l s sh0 sh1 =+mgShPrep :: Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)+mgShPrep f l s sh0 sh1 = let sh0' = shSubst s sh0 sh1' = shSubst s sh1- in mgSh l s (rwSh sh0') (rwSh sh1')+ in mgSh f l s (rwSh sh0') (rwSh sh1') -mgSh :: a -> Subst a -> Sh a -> Sh a -> Either (TyE a) (Subst a)-mgSh _ inp Nil Nil = Right inp-mgSh l inp (Cons i sh) (Cons i' sh') = do- sI <- mguIPrep (iSubst inp) i i'- mgShPrep l (inp { iSubst = sI }) sh sh'-mgSh _ inp (SVar sh) (SVar sh') | sh == sh' = Right inp-mgSh l inp s@(SVar (Nm _ (U i) _)) sh | i `IS.member` occSh sh = Left$ OSh l s sh- | otherwise = Right$ mapShSubst (IM.insert i sh) inp-mgSh l inp sh s@(SVar (Nm _ (U i) _)) | i `IS.member` occSh sh = Left$ OSh l sh s- | otherwise = Right$ mapShSubst (IM.insert i sh) inp-mgSh l _ sh@Nil sh'@Cons{} = Left $ USh l sh sh'-mgSh l _ sh@Cons{} sh'@Nil{} = Left $ USh l sh' sh-mgSh l inp (Rev sh) (Rev sh') = mgShPrep l inp sh sh'-mgSh l inp (Cat sh0 sh0') (Cat sh1 sh1') = do- s <- mgShPrep l inp sh0 sh1- mgShPrep l s sh0' sh1'-mgSh l inp (Rev sh) sh' | (is, Nil) <- unroll sh' = do- mgShPrep l inp sh (roll Nil$reverse is)-mgSh l inp sh (Rev sh') | (is, Nil) <- unroll sh' = do- mgShPrep l inp (roll Nil$reverse is) sh+mgSh :: Focus -> a -> Subst a -> Sh a -> Sh a -> UM a (Sh a, Subst a)+mgSh _ _ inp Nil Nil = pure (Nil, inp)+mgSh f l inp (Cons i sh) (Cons i' sh') = do+ (i'', sI) <- mguIPrep f (iSubst inp) i i'+ (sh'', s2) <- mgShPrep f l (inp { iSubst = sI }) sh sh'+ pure (Cons i'' sh'', s2)+mgSh _ _ inp s@(SVar sh) (SVar sh') | sh == sh' = pure (s, inp)+mgSh _ l inp s@(SVar (Nm _ (U i) _)) sh | i `IS.member` occSh sh = throwError $ OSh l s sh+ | otherwise = pure (sh, mapShSubst (IM.insert i sh) inp)+mgSh _ l inp sh s@(SVar (Nm _ (U i) _)) | i `IS.member` occSh sh = throwError $ OSh l sh s+ | otherwise = pure (sh, mapShSubst (IM.insert i sh) inp)+mgSh _ l _ sh@Nil sh'@Cons{} = throwError $ USh l sh sh'+mgSh _ l _ sh@Cons{} sh'@Nil{} = throwError $ USh l sh' sh+mgSh f l inp (Rev sh) (Rev sh') = mgShPrep f l inp sh sh'+mgSh f l inp (Cat sh0 sh0') (Cat sh1 sh1') = do+ (sh', s) <- mgShPrep f l inp sh0 sh1+ (sh'', s') <- mgShPrep f l s sh0' sh1'+ pure (Cat sh' sh'', s')+mgSh f l inp (Rev sh) sh' | (is, Nil) <- unroll sh' = do+ mgShPrep f l inp sh (roll Nil$reverse is)+mgSh f l inp sh (Rev sh') | (is, Nil) <- unroll sh' = do+ mgShPrep f l inp (roll Nil$reverse is) sh -mguPrep :: (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)-mguPrep l s t0 t1 =+mguPrep :: Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)+mguPrep f l s t0 t1 = let t0' = aT s t0 t1' = aT s t1- in mgu l s ({-# SCC "rwArr" #-} rwArr t0') ({-# SCC "rwArr" #-} rwArr t1')+ in mgu f l s ({-# SCC "rwArr" #-} rwArr t0') ({-# SCC "rwArr" #-} rwArr t1') +mp :: (a, E a) -> Subst a -> T a -> T a -> UM a (Subst a)+mp l s t0 t1 = snd <$> mguPrep LF l s t0 t1+ occSh :: Sh a -> IS.IntSet occSh (SVar (Nm _ (U i) _)) = IS.singleton i occSh (Cat sh0 sh1) = occSh sh0 <> occSh sh1@@ -310,74 +346,83 @@ occ (P ts) = foldMap occ ts occ (Ρ (Nm _ (U i) _) rs) = IS.insert i $ foldMap occ rs -mgu :: (a, E a) -> Subst a -> T a -> T a -> Either (TyE a) (Subst a)-mgu l s (Arrow t0 t1) (Arrow t0' t1') = do- s0 <- mguPrep l s t0 t0'- mguPrep l s0 t1 t1'-mgu _ s I I = Right s-mgu _ s F F = Right s-mgu _ s B B = Right s-mgu _ s Li{} I = Right s-mgu _ s I Li{} = Right s-mgu _ s (Li i0) (Li i1) = do {iS <- mguIPrep (iSubst s) i0 i1; pure $ Subst mempty iS mempty <> s}-mgu _ s (TVar n) (TVar n') | n == n' = Right s-mgu (l, _) s t'@(TVar (Nm _ (U i) _)) t | i `IS.member` occ t = Left$ OT l t' t- | otherwise = Right $ mapTySubst (IM.insert i t) s-mgu (l, _) s t t'@(TVar (Nm _ (U i) _)) | i `IS.member` occ t = Left$ OT l t' t- | otherwise = Right $ mapTySubst (IM.insert i t) s-mgu (l, e) _ t0@Arrow{} t1 = Left $ UF l e t0 t1-mgu (l, e) _ t0 t1@Arrow{} = Left $ UF l e t0 t1-mgu l s (Arr sh t) (Arr sh' t') = do- s0 <- mguPrep l s t t'- mgShPrep (fst l) s0 sh sh'-mgu (l, e) _ F I = Left$ UF l e F I-mgu (l, e) _ I F = Left$ UF l e I F-mgu (l, e) _ F t@Li{} = Left$ UF l e F t-mgu (l, e) _ t@Li{} F = Left$ UF l e t F-mgu l s (Arr (SVar n) t) F = mapShSubst (insert n Nil) <$> mguPrep l s t F-mgu l s (Arr (SVar n) t) I = mapShSubst (insert n Nil) <$> mguPrep l s t I-mgu l s F (Arr (SVar n) t) = mapShSubst (insert n Nil) <$> mguPrep l s F t-mgu l s I (Arr (SVar n) t) = mapShSubst (insert n Nil) <$> mguPrep l s I t-mgu l s (Arr (SVar n) t) t'@P{} = mapShSubst (insert n Nil) <$> mguPrep l s t t'-mgu l s t'@P{} (Arr (SVar n) t) = mapShSubst (insert n Nil) <$> mguPrep l s t' t-mgu l s (P ts) (P ts') | length ts == length ts' = zS (mguPrep l) s ts ts'+mgu :: Focus -> (a, E a) -> Subst a -> T a -> T a -> UM a (T a, Subst a)+mgu f l s (Arrow t0 t1) (Arrow t0' t1') = do+ (t0'', s0) <- mguPrep LF l s t0 t0'+ (t1'', s1) <- mguPrep f l s0 t1 t1'+ pure (Arrow t0'' t1'', s1)+mgu _ _ s I I = pure (I, s)+mgu _ _ s F F = pure (F, s)+mgu _ _ s B B = pure (B, s)+mgu _ _ s t@Li{} I = pure (t, s)+mgu _ _ s I t@Li{} = pure (t, s)+mgu f _ s (Li i0) (Li i1) = do {(i', iS) <- mguIPrep f (iSubst s) i0 i1; pure (Li i', Subst mempty iS mempty <> s)}+mgu _ _ s t@(TVar n) (TVar n') | n == n' = pure (t, s)+mgu _ (l, _) s t'@(TVar (Nm _ (U i) _)) t | i `IS.member` occ t = throwError $ OT l t' t+ | otherwise = pure (t, mapTySubst (IM.insert i t) s)+mgu _ (l, _) s t t'@(TVar (Nm _ (U i) _)) | i `IS.member` occ t = throwError $ OT l t' t+ | otherwise = pure (t, mapTySubst (IM.insert i t) s)+mgu _ (l, e) _ t0@Arrow{} t1 = throwError $ UF l e t0 t1+mgu _ (l, e) _ t0 t1@Arrow{} = throwError $ UF l e t0 t1+mgu f l s (Arr sh t) (Arr sh' t') = do+ (t'', s0) <- mguPrep f l s t t'+ (sh'', s1) <- mgShPrep f (fst l) s0 sh sh'+ pure (Arr sh'' t'', s1)+mgu _ (l, e) _ F I = throwError $ UF l e F I+mgu _ (l, e) _ I F = throwError $ UF l e I F+mgu _ (l, e) _ F t@Li{} = throwError $ UF l e F t+mgu _ (l, e) _ t@Li{} F = throwError $ UF l e t F+mgu f l s (Arr (SVar n) t) F = second (mapShSubst (insert n Nil)) <$> mguPrep f l s t F+mgu f l s (Arr (SVar n) t) I = second (mapShSubst (insert n Nil)) <$> mguPrep f l s t I+mgu f l s F (Arr (SVar n) t) = second (mapShSubst (insert n Nil)) <$> mguPrep f l s F t+mgu f l s I (Arr (SVar n) t) = second (mapShSubst (insert n Nil)) <$> mguPrep f l s I t+mgu f l s (Arr (SVar n) t) B = second (mapShSubst (insert n Nil)) <$> mguPrep f l s t B+mgu f l s B (Arr (SVar n) t) = second (mapShSubst (insert n Nil)) <$> mguPrep f l s B t+mgu f l s (Arr (SVar n) t) t'@P{} = second (mapShSubst (insert n Nil)) <$> mguPrep f l s t t'+mgu f l s t'@P{} (Arr (SVar n) t) = second (mapShSubst (insert n Nil)) <$> mguPrep f l s t' t+mgu f l s (P ts) (P ts') | length ts == length ts' = first P <$> zSt (mguPrep f l) s ts ts' -- TODO: rho occurs check-mgu l@(lϵ, e) s t@(Ρ n rs) t'@(P ts) | length ts >= fst (IM.findMax rs) && fst (IM.findMin rs) > 0 = tS (\sϵ (i, tϵ) -> mapTySubst (insert n t') <$> mguPrep l sϵ (ts!!(i-1)) tϵ) s (IM.toList rs)- | otherwise = Left$UF lϵ e t t'-mgu l s t@P{} t'@Ρ{} = mgu l s t' t-mgu l s (Ρ n rs) (Ρ n' rs') = do- rss <- tS (\sϵ (t0,t1) -> mguPrep l sϵ t0 t1) s $ IM.elems $ IM.intersectionWith (,) rs rs'- pure $ mapTySubst (insert n (Ρ n' (rs<>rs'))) rss-mgu (l, e) _ F t@Arr{} = Left $ UF l e F t-mgu (l, e) _ t@Arr{} F = Left $ UF l e t F-mgu (l, e) _ B t@Arr{} = Left $ UF l e B t-mgu (l, e) _ t@Arr{} B = Left $ UF l e t B-mgu (l, e) _ I t@Arr{} = Left $ UF l e I t-mgu (l, e) _ t@Arr{} I = Left $ UF l e t I-mgu (l, e) _ t@Li{} t'@Arr{} = Left $ UF l e t t'-mgu (l, e) _ t@Arr{} t'@Li{} = Left $ UF l e t t'-mgu (l, e) _ F t@P{} = Left $ UF l e F t-mgu (l, e) _ t@P{} F = Left $ UF l e t F-mgu (l, e) _ I t@P{} = Left $ UF l e I t-mgu (l, e) _ t@P{} I = Left $ UF l e t I-mgu (l, e) _ B t@P{} = Left $ UF l e B t-mgu (l, e) _ t@P{} B = Left $ UF l e t B-mgu (l, e) _ t@P{} t'@Arr{} = Left $ UF l e t t'-mgu (l, e) _ t@Arr{} t'@P{} = Left $ UF l e t t'-mgu (l, e) _ I B= Left $ UF l e I B-mgu (l, e) _ B I = Left $ UF l e B I-mgu (l, e) _ t@Li{} B = Left $ UF l e t B-mgu (l, e) _ B t@Li{} = Left $ UF l e B t+mgu f l@(lϵ, e) s t@(Ρ n rs) t'@(P ts) | length ts >= fst (IM.findMax rs) && fst (IM.findMin rs) > 0 = first P <$> tS (\sϵ (i, tϵ) -> second (mapTySubst (insert n t')) <$> mguPrep f l sϵ (ts!!(i-1)) tϵ) s (IM.toList rs)+ | otherwise = throwError $ UF lϵ e t t'+mgu f l s t@P{} t'@Ρ{} = mgu f l s t' t+mgu f l s (Ρ n rs) (Ρ n' rs') = do+ (_, rss) <- tS (\sϵ (t0,t1) -> mguPrep LF l sϵ t0 t1) s $ IM.elems $ IM.intersectionWith (,) rs rs'+ let t=Ρ n' (rs<>rs') in pure (t, mapTySubst (insert n t) rss)+mgu _ (l, e) _ F t@Arr{} = throwError $ UF l e F t+mgu _ (l, e) _ t@Arr{} F = throwError $ UF l e t F+mgu _ (l, e) _ B t@Arr{} = throwError $ UF l e B t+mgu _ (l, e) _ t@Arr{} B = throwError $ UF l e t B+mgu _ (l, e) _ I t@Arr{} = throwError $ UF l e I t+mgu _ (l, e) _ t@Arr{} I = throwError $ UF l e t I+mgu _ (l, e) _ t@Li{} t'@Arr{} = throwError $ UF l e t t'+mgu _ (l, e) _ t@Arr{} t'@Li{} = throwError $ UF l e t t'+mgu _ (l, e) _ F t@P{} = throwError $ UF l e F t+mgu _ (l, e) _ t@P{} F = throwError $ UF l e t F+mgu _ (l, e) _ I t@P{} = throwError $ UF l e I t+mgu _ (l, e) _ t@P{} I = throwError $ UF l e t I+mgu _ (l, e) _ B t@P{} = throwError $ UF l e B t+mgu _ (l, e) _ t@P{} B = throwError $ UF l e t B+mgu _ (l, e) _ t@P{} t'@Arr{} = throwError $ UF l e t t'+mgu _ (l, e) _ t@Arr{} t'@P{} = throwError $ UF l e t t'+mgu _ (l, e) _ I B= throwError $ UF l e I B+mgu _ (l, e) _ B I = throwError $ UF l e B I+mgu _ (l, e) _ t@Li{} B = throwError $ UF l e t B+mgu _ (l, e) _ B t@Li{} = throwError $ UF l e B t +zSt _ s [] _ = pure ([], s)+zSt _ s _ [] = pure ([], s)+zSt op s (x:xs) (y:ys) = do{(t, next) <- op s x y; first (t:) <$> zSt op next xs ys}+ zS _ s [] _ = pure s zS _ s _ [] = pure s-zS op s (x:xs) (y:ys) = do{next <- op s x y; zS op next xs ys}+zS op s (x:xs) (y:ys) = do {next <- op s x y; zS op next xs ys} -tS :: Monad m => (Subst a -> b -> m (Subst a)) -> Subst a -> [b] -> m (Subst a)-tS _ s [] = pure s-tS f s (t:ts) = do{next <- f s t; tS f next ts}+tS :: Monad m => (Subst a -> b -> m (x, Subst a)) -> Subst a -> [b] -> m ([x], Subst a)+tS _ s [] = pure ([], s)+tS f s (t:ts) = do{(tϵ, next) <- f s t; first (tϵ:) <$> tS f next ts} -vx i = Cons i Nil+vx = (`Cons` Nil)+vV i = Arr (vx i) tyNumBinOp :: a -> TyM a (T (), Subst a) tyNumBinOp l = do@@ -407,6 +452,13 @@ pushVarConstraint n l IsOrd pure (n' ~> n' ~> B, mempty) +tyEqBinRel :: a -> TyM a (T (), Subst a)+tyEqBinRel l = do+ n <- freshN "e" l+ let n'=TVar (void n)+ pushVarConstraint n l IsEq+ pure (n' ~> n' ~> B, mempty)+ sel :: [Int] -> Sh a -> Sh a sel axes sh = roll Nil (fmap snd (filter ((`elem` axes) . fst) (zip [1..] unrolled))) where (unrolled, _) = unroll sh@@ -443,77 +495,63 @@ pure (n' ~> n' ~> Arr (SVar sh) n', mempty) tyB _ Iter = do{a <- ftv "a"; let s = Arrow a a in pure (s ~> I ~> s, mempty)} tyB _ ConsE = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (a ~> Arr (i `Cons` Nil) a ~> Arr (StaPlus () i (Ix()1) `Cons` Nil) a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (a ~> vV i a ~> vV (StaPlus () i (Ix()1)) a, mempty) tyB l Snoc = tyB l ConsE tyB _ A1 = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()+ a <- ftv "a"; i <- fti "i" sh <- fsh "sh" pure (Arr (i `Cons` sh) a ~> I ~> Arr sh a, mempty) tyB _ IOf = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure ((a ~> B) ~> Arr (i `Cons` Nil) a ~> I, mempty)+ a <- ftv "a"; i <- fti "i"+ pure ((a ~> B) ~> vV i a ~> I, mempty) tyB _ Di = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (Arr (i `Cons` i `Cons` Nil) a ~> Arr (i `Cons` Nil) a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (Arr (i `Cons` i `Cons` Nil) a ~> vV i a, mempty) tyB _ LastM = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (Arr (i `Cons` Nil) a ~> a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (vV i a ~> a, mempty) tyB _ Last = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (vV (StaPlus () i (Ix()1)) a ~> a, mempty) tyB _ Head = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (vV (StaPlus () i (Ix()1)) a ~> a, mempty) tyB _ Init = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> Arr (i `Cons` Nil) a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (vV (StaPlus () i (Ix()1)) a ~> vV i a, mempty)+tyB _ InitM = do+ a <- ftv "a"; i <- fti "i"; n <- ftie+ pure (vV i a ~> vV n a, mempty) tyB _ Tail = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (Arr (StaPlus () i (Ix()1) `Cons` Nil) a ~> Arr (i `Cons` Nil) a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (vV (StaPlus () i (Ix()1)) a ~> vV i a, mempty)+tyB _ TailM = do+ a <- ftv "a"; i <- fti "i"; n <- ftie+ pure (vV i a ~> vV n a, mempty) tyB _ Rot = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (I ~> Arr (i `Cons` Nil) a ~> Arr (i `Cons` Nil) a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (I ~> vV i a ~> vV i a, mempty) tyB _ Cyc = do- sh <- fsh "sh"- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- n <- IEVar () <$> freshN "n" ()+ sh <- fsh "sh"; a <- ftv "a"; i <- fti "i"; n <- ftie pure (Arr (i `Cons` sh) a ~> I ~> Arr (n `Cons` sh) a, mempty) tyB _ HeadM = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- pure (Arr (i `Cons` Nil) a ~> a, mempty)+ a <- ftv "a"; i <- fti "i"+ pure (vV i a ~> a, mempty) tyB _ Re = do- a <- ftv "a"- n <- IEVar () <$> freshN "n" ()+ a <- ftv "a"; n <- ftie pure (I ~> a ~> Arr (n `Cons` Nil) a, mempty)-tyB _ FRange = do- n <- IEVar () <$> freshN "n" ()- pure (F ~> F ~> I ~> Arr (n `Cons` Nil) F, mempty)+tyB _ FRange = do {n <- ftie; pure (F ~> F ~> I ~> Arr (n `Cons` Nil) F, mempty)} tyB _ Fib = do- n <- IEVar () <$> freshN "n" ()- a <- freshN "a" ()+ n <- ftie; a <- freshN "a" () let a' = TVar a arrTy = Arr (n `Cons` Nil) a' pure (a' ~> a' ~> (a' ~> a' ~> a') ~> I ~> arrTy, mempty)-tyB _ IRange = do- n <- IEVar () <$> freshN "n" ()- pure (I ~> I ~> I ~> Arr (n `Cons` Nil) I, mempty)+tyB _ IRange = do {n <- ftie; pure (I ~> I ~> I ~> Arr (n `Cons` Nil) I, mempty)} tyB l Plus = tyNumBinOp l; tyB l Minus = tyNumBinOp l tyB l Times = tyNumBinOp l tyB l Gte = tyOrdBinRel l; tyB l Gt = tyOrdBinRel l; tyB l Lt = tyOrdBinRel l-tyB l Lte = tyOrdBinRel l; tyB l Eq = tyOrdBinRel l; tyB l Neq = tyOrdBinRel l+tyB l Lte = tyOrdBinRel l; tyB l Eq = tyEqBinRel l; tyB l Neq = tyEqBinRel l tyB l And = tyBoo l; tyB l Or = tyBoo l; tyB l Xor = tyBoo l tyB l N = do n <- freshN "b" l@@ -559,18 +597,15 @@ i <- freshN "i" (); j <- freshN "j" () n <- freshN "a" () let i' = IVar () i; j' = IVar () j; n' = TVar n- pure (Arr (vx i') n' ~> Arr (vx j') n' ~> Arr (vx $ StaPlus () i' j') n', mempty)+ pure (vV i' n' ~> vV j' n' ~> vV (StaPlus () i' j') n', mempty) tyB _ Scan = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- sh <- fsh "sh"+ a <- ftv "a"; i <- fti "i"; sh <- fsh "sh" let i1 = StaPlus () i (Ix()1) arrTy = Arr (Cons i1 sh) a pure ((a ~> a ~> a) ~> arrTy ~> arrTy, mempty) tyB _ ScanS = do a <- ftv "a"; b <- ftv "b"- i <- IVar () <$> freshN "i" ()- sh <- fsh "sh"+ i <- fti "i"; sh <- fsh "sh" let opTy = b ~> a ~> b arrTy = Arr (Cons i sh); rarrTy = Arr (Cons (StaPlus () i (Ix()1)) sh) -- FIXME: 1+1?@@ -578,7 +613,7 @@ tyB l (DI n) = tyB l (Conv [n]) tyB _ (Conv ns) = do sh <- fsh "sh"- is <- zipWithM (\_ t -> IVar () <$> freshN (T.singleton t) ()) ns ['i'..]+ is <- zipWithM (\_ t -> fti (T.singleton t)) ns ['i'..] a <- ftv "a"; b <- ftv "b" let nx = Ix () <$> ns opTy = Arr (foldr Cons sh nx) a ~> b@@ -586,7 +621,7 @@ pure (opTy ~> t, mempty) tyB _ Succ = do sh <- fsh "sh"- i <- IVar () <$> freshN "i" ()+ i <- fti "i" a <- ftv "a"; b <- ftv "b" let opTy = a ~> (a ~> b) pure (opTy ~> (Arr (StaPlus () i (Ix () 1) `Cons` sh) a ~> Arr (i `Cons` sh) b), mempty)@@ -607,7 +642,7 @@ tyB _ Zip = do i <- freshN "i" () a <- freshN "a" (); b <- freshN "b" (); c <- freshN "c" ()- let arrSh = IVar () i `Cons` Nil+ let arrSh = vx (IVar () i) a' = TVar a; b' = TVar b; c' = TVar c fTy = a' ~> b' ~> c' gTy = Arr arrSh a' ~> Arr arrSh b' ~> Arr arrSh c'@@ -623,27 +658,23 @@ fTy = foldr (~>) cod $ zipWith3 (\ax sh t -> case ax of {(_,Nothing) -> Arr (trim sh) t;(_,Just axs) -> Arr (sel axs sh) t}) as shs vs rTy = foldr (~>) codTy mArrs shsU = zipWith (\ax sh -> case ax of {(n,Nothing) -> tydrop n sh;(_,Just axs) -> del axs sh}) as shs- shUHere sh sh' = liftEither $ mgShPrep l mempty (sh$>l) (sh'$>l)+ shUHere sh sh' = fmap snd (liftU $ mgShPrep LF l mempty (sh$>l) (sh'$>l)) s <- zipWithM shUHere shsU (tail shsU++[SVar codSh]) pure (fTy ~> rTy, mconcat s) tyB _ Fold = do- ix <- IVar () <$> freshN "i" ()- sh <- fsh "sh"+ ix <- fti "i"; sh <- fsh "sh" a <- freshN "a" () let sh1 = StaPlus () ix (Ix()1) `Cons` sh a' = TVar a pure ((a' ~> a' ~> a') ~> Arr sh1 a' ~> Arr sh a', mempty) tyB _ FoldS = do- ix <- IVar () <$> freshN "i" ()- sh <- fsh "sh"+ ix <- fti "i"; sh <- fsh "sh"; a <- freshN "a" () let sh1 = ix `Cons` sh a' = TVar a pure ((a' ~> a' ~> a') ~> a' ~> Arr sh1 a' ~> Arr sh a', mempty) tyB _ Foldl = do- ix <- IVar () <$> freshN "i" ()- sh <- fsh "sh"- a <- ftv "a"+ ix <- fti "i"; sh <- fsh "sh"; a <- ftv "a" let sh1 = ix `Cons` sh pure ((a ~> a ~> a) ~> a ~> Arr sh1 a ~> Arr sh a, mempty) tyB _ FoldA = do@@ -651,14 +682,10 @@ a <- ftv "a" pure ((a ~> a ~> a) ~> a ~> Arr sh a ~> a, mempty) tyB _ Dim = do- iV <- IVar () <$> freshN "i" ()- shV <- fsh "sh"- a <- ftv "a"+ iV <- fti "i"; shV <- fsh "sh"; a <- ftv "a" pure (Arr (iV `Cons` shV) a ~> Li iV, mempty) tyB _ RevE = do- iV <- IVar () <$> freshN "i" ()- shV <- fsh "sh"- a <- ftv "a"+ iV <- fti "i"; shV <- fsh "sh"; a <- ftv "a" let aTy = Arr (iV `Cons` shV) a pure (aTy ~> aTy, mempty) tyB _ Size = do@@ -666,25 +693,23 @@ a <- ftv "a" pure (Arr shV a ~> I, mempty) tyB _ Gen = do- a <- ftv "a"- n <- IEVar () <$> freshN "n" ()+ a <- ftv "a"; n <- ftie let arrTy = Arr (n `Cons` Nil) a pure (a ~> (a ~> a) ~> I ~> arrTy, mempty) tyB l Mul = do a <- freshN "a" l- i <- IVar () <$> freshN "i" (); j <- IVar () <$> freshN "j" (); k <- IVar () <$> freshN "k" ()+ i <- fti "i"; j <- fti "j"; k <- fti "k" pushVarConstraint a l IsNum let a' = TVar (void a) pure (Arr (i `Cons` j `Cons` Nil) a' ~> Arr (j `Cons` k `Cons` Nil) a' ~> Arr (i `Cons` k `Cons` Nil) a', mempty) tyB l VMul = do a <- freshN "a" l- i <- IVar () <$> freshN "i" (); j <- IVar () <$> freshN "j" ()+ i <- fti "i"; j <- fti "j" pushVarConstraint a l IsNum let a' = TVar (void a)- pure (Arr (i `Cons` j `Cons` Nil) a' ~> Arr (j `Cons` Nil) a' ~> Arr (i `Cons` Nil) a', mempty)+ pure (Arr (i `Cons` j `Cons` Nil) a' ~> vV j a' ~> vV i a', mempty) tyB l Eye = do- a <- freshN "a" l- i <- IVar () <$> freshN "i" ()+ a <- freshN "a" l; i <- fti "i" pushVarConstraint a l IsNum let a'=TVar (void a) pure (Arr (i `Cons` i `Cons` Nil) a', mempty)@@ -692,15 +717,11 @@ tyB _ Cos = pure (F ~> F, mempty) tyB _ Tan = pure (F ~> F, mempty) tyB _ Ices = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- n <- IEVar () <$> freshN "n" ()- pure ((a ~> B) ~> Arr (vx i) a ~> Arr (vx n) I, mempty)+ a <- ftv "a"; i <- fti "i"; n <- ftie+ pure ((a ~> B) ~> vV i a ~> vV n I, mempty) tyB _ Filt = do- a <- ftv "a"- i <- IVar () <$> freshN "i" ()- n <- IEVar () <$> freshN "n" ()- pure ((a ~> B) ~> Arr (vx i) a ~> Arr (vx n) I, mempty)+ a <- ftv "a"; i <- fti "i"; n <- ftie+ pure ((a ~> B) ~> vV i a ~> vV n a, mempty) liftCloneTy :: T b -> TyM a (T b, IM.IntMap Int) liftCloneTy t = do@@ -782,6 +803,8 @@ checkTy I (HasBits, _) = pure Nothing checkTy B (HasBits, _) = pure Nothing checkTy F (IsOrd, _) = pure Nothing+checkTy I (IsEq, _) = pure Nothing+checkTy F (IsEq, _) = pure Nothing checkTy t (c@IsNum, l) = Left$ Doesn'tSatisfy l t c checkTy t (c@HasBits, l) = Left$ Doesn'tSatisfy l t c @@ -807,14 +830,14 @@ tyE :: Subst a -> E a -> TyM a (E (T ()), Subst a) tyE s (EApp _ (Builtin _ Re) (ILit _ n)) = do a <- ftv "a"- let arrTy = a ~> Arr (vx $ Ix () (fromInteger n)) a+ let arrTy = a ~> vV (Ix () (fromInteger n)) a pure (EApp arrTy (Builtin (I ~> arrTy) Re) (ILit I n), s) tyE s (EApp _ (EApp _ (EApp _ (Builtin _ FRange) e0) e1) (ILit _ n)) = do (e0',s0) <- tyE s e0; (e1',s1) <- tyE s0 e1 let tyE0 = eAnn e0'; tyE1 = eAnn e1'- arrTy = Arr (vx (Ix () (fromInteger n))) F+ arrTy = vV (Ix () (fromInteger n)) F l0 = eAnn e0; l1 = eAnn e1- s0' <- liftEither $ mguPrep (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftEither $ mguPrep (l1,e1) s0' F (eAnn e1' $> l1)+ s0' <- liftU $ mp (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftU $ mp (l1,e1) s0' F (eAnn e1' $> l1) pure (EApp arrTy (EApp (I ~> arrTy) (EApp (tyE1 ~> I ~> arrTy) (Builtin (tyE0 ~> tyE1 ~> I ~> arrTy) FRange) e0') e1') (ILit I n), s1') tyE s (EApp l eϵ@(EApp _ (EApp _ (Builtin _ FRange) e0) e1) n) = do (nA, sϵ) <- tyE s n@@ -822,23 +845,23 @@ iT@(Li ix) -> do (e0',s0) <- tyE sϵ e0; (e1',s1) <- tyE s0 e1 let tyE0 = eAnn e0'; tyE1 = eAnn e1'- arrTy = Arr (vx ix) F+ arrTy = vV ix F l0 = eAnn e0; l1 = eAnn e1- s0' <- liftEither $ mguPrep (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftEither $ mguPrep (l1,e1) s0' F (eAnn e1' $> l1)+ s0' <- liftU $ mp (l0,e0) s1 F (eAnn e0' $> l0); s1' <- liftU $ mp (l1,e1) s0' F (eAnn e1' $> l1) pure (EApp arrTy (EApp (iT ~> arrTy) (EApp (tyE1 ~> iT ~> arrTy) (Builtin (tyE0 ~> tyE1 ~> iT ~> arrTy) FRange) e0') e1') nA, s1') _ -> do a <- ft "a" l; b <- ft "b" l (eϵ', s0) <- tyE sϵ eϵ let eϵTy = a ~> b- s1 <- liftEither $ mguPrep (l,eϵ) s0 (eAnn eϵ'$>l) eϵTy- s2 <- liftEither $ mguPrep (l,n) s1 (eAnn nA$>l) a+ s1 <- liftU $ mp (l,eϵ) s0 (eAnn eϵ'$>l) eϵTy+ s2 <- liftU $ mp (l,n) s1 (eAnn nA$>l) a pure (EApp (void b) eϵ' nA, s2) tyE s (EApp _ (EApp _ (EApp _ (Builtin _ Gen) x) f) (ILit _ n)) = do (x',s0) <- tyE s x; (f',s1) <- tyE s0 f let tyX = eAnn x'; tyF = eAnn f'- arrTy = Arr (vx $ Ix () (fromInteger n)) tyX+ arrTy = vV (Ix () (fromInteger n)) tyX lX = eAnn x; lF = eAnn f- s1' <- liftEither $ mguPrep (lF, f) s1 ((tyX $> lX) ~> (tyX $> lX)) (tyF $> lF)+ s1' <- liftU $ mp (lF, f) s1 ((tyX $> lX) ~> (tyX $> lX)) (tyF $> lF) pure (EApp arrTy (EApp (I ~> arrTy) (EApp (tyF ~> I ~> arrTy) (Builtin (tyX ~> tyF ~> I ~> arrTy) Gen) x') f') (ILit I n), s1') tyE s (EApp l e@(EApp _ (EApp _ (Builtin _ Gen) x) f) n) = do (nA, sϵ) <- tyE s n@@ -846,28 +869,28 @@ iT@(Li ix) -> do (x',s0) <- tyE sϵ x; (f',s1) <- tyE s0 f let tyX = eAnn x'; tyF = eAnn f'- arrTy = Arr (vx ix) tyX+ arrTy = vV ix tyX lX = eAnn x; lF = eAnn f- s1' <- liftEither $ mguPrep (lF, f) s1 ((tyX $> lX) ~> (tyX $> lX)) (tyF $> lF)+ s1' <- liftU $ mp (lF, f) s1 ((tyX $> lX) ~> (tyX $> lX)) (tyF $> lF) pure (EApp arrTy (EApp (iT ~> arrTy) (EApp (tyF ~> iT ~> arrTy) (Builtin (tyX ~> tyF ~> iT ~> arrTy) Gen) x') f') nA, s1') _ -> do a <- ft "a" l; b <- ft "b" l (e', s0) <- tyE sϵ e let eT = Arrow a b- s1 <- liftEither $ mguPrep (l,e) s0 (eAnn e'$>l) eT- s2 <- liftEither $ mguPrep (l,n) s1 (eAnn nA$>l) a+ s1 <- liftU $ mp (l,e) s0 (eAnn e'$>l) eT+ s2 <- liftU $ mp (l,n) s1 (eAnn nA$>l) a pure (EApp (void b) e' nA, s2) tyE s eC@(EApp lC (EApp _ (Builtin _ Cyc) e) (ILit _ m)) = do (e0, s0) <- tyE s e- ix <- IVar () <$> freshN "ix" ()+ ix <- fti "ix" a <- ftv "a" let t=Arr (ix `Cons` Nil) a arrTy = Arr (StaMul () ix (Ix () (fromIntegral m)) `Cons` Nil) a lE=eAnn e- s1 <- liftEither $ mguPrep (lC,eC) s0 (eAnn e0$>lE) (t$>lE)+ s1 <- liftU $ mp (lC,eC) s0 (eAnn e0$>lE) (t$>lE) pure (EApp arrTy (EApp (I ~> arrTy) (Builtin (t ~> I ~> arrTy) Cyc) e0) (ILit I m), s1) tyE s (EApp _ (EApp _ (EApp _ (Builtin _ IRange) (ILit _ b)) (ILit _ e)) (ILit _ si)) = do- let arrTy = Arr (vx (Ix () (fromInteger ((e-b+si) `quot` si)))) I+ let arrTy = vV (Ix () (fromInteger ((e-b+si) `quot` si))) I pure (EApp arrTy (EApp (I ~> arrTy) (EApp (I ~> I ~> arrTy) (Builtin (I ~> I ~> I ~> arrTy) IRange) (ILit I b)) (ILit I e)) (ILit I si), s) tyE s (FLit _ x) = pure (FLit F x, s) tyE s (BLit _ x) = pure (BLit B x, s)@@ -904,23 +927,23 @@ a <- ftv "a" (es', s') <- sSt s es let eTys = a : fmap eAnn es'- uHere sϵ t t' = mguPrep (l,e) sϵ (t$>l) (t'$>l)- ss' <- liftEither $ zS uHere s' eTys (tail eTys)- pure (ALit (Arr (vx (Ix () $ length es)) a) es', ss')+ uHere sϵ t t' = mp (l,e) sϵ (t$>l) (t'$>l)+ ss' <- liftU $ zS uHere s' eTys (tail eTys)+ pure (ALit (vV (Ix () $ length es) a) es', ss') tyE s (EApp l e0 e1) = do a <- ft "a" l; b <- ft "b" l (e0', s0) <- tyE s e0 (e1', s1) <- tyE s0 e1 let e0Ty = a ~> b- s2 <- liftEither $ mguPrep (l,e0) s1 (eAnn e0'$>l) e0Ty- s3 <- liftEither $ mguPrep (l,e1) s2 (eAnn e1'$>l) a+ s2 <- liftU $ mp (l,e0) s1 (eAnn e0'$>l) e0Ty+ s3 <- liftU $ mp (l,e1) s2 (eAnn e1'$>l) a pure (EApp (void b) e0' e1', s3) tyE s (Cond l p e0 e1) = do (p',sP) <- tyE s p (e0',s0) <- tyE sP e0 (e1',s1) <- tyE s0 e1- sP' <- liftEither $ mguPrep (eAnn p,p) s1 B (eAnn p'$>eAnn p); s0' <- liftEither $ mguPrep (l,e0) sP' (eAnn e0'$>l) (eAnn e1'$>eAnn e1)- pure (Cond (eAnn e0') p' e0' e1', s0')+ sP' <- liftU $ mp (eAnn p,p) s1 B (eAnn p'$>eAnn p); (tB, s0') <- liftU $ mguPrep RF (l,e0) sP' (eAnn e0'$>l) (eAnn e1'$>eAnn e1)+ pure (Cond (void tB) p' e0' e1', s0') tyE s (Var l n@(Nm _ (U u) _)) = do lSt<- gets staEnv case IM.lookup u lSt of@@ -936,7 +959,7 @@ pure (Tup (P eTys) es', s') tyE s (Ann l e t) = do (e', s') <- tyE s e- s'' <- liftEither $ maM (aT s'$fmap ($>l) eAnn e') (aT s' (t$>l))+ s'' <- liftEither $ maM LF (aT s'$fmap ($>l) eAnn e') (aT s' (t$>l)) pure (e', s'<>s'') sSt :: Subst a -> [E a] -> TyM a ([E (T ())], Subst a)
test/Spec.cpphs view
@@ -14,10 +14,13 @@ import Hs.FFI import Math.Hypergeometric (erf, hypergeometric, ncdf) import Math.SpecialFunction (agm, bessel1, chisqcdf, completeElliptic, gamma, tcdf)+import Numeric.NumberTheory (isPrime) import P import System.Info (arch)+import Test.QuickCheck (property) import Test.Tasty import Test.Tasty.HUnit+import Test.Tasty.QuickCheck (testProperty) kl :: Floating a => [a] -> [a] -> a kl xs ys = sum [ x * log (x/y) | x <- xs, y <- ys ]@@ -28,13 +31,21 @@ x .?= y = assertBool ("expected " ++ show y ++ ", got " ++ show x) ((x-y)/y<1e-15&&(y-x)/y<1e-15) main :: IO ()-main = defaultMain $ testGroup "All" $ rTy:tyT:allT:+main = do+ pjit <- fpn =<< BSL.readFile "test/examples/isPrime.apple"+ defaultMain $ testGroup "All" $ pTest pjit:rTy:tyT:allT: #ifdef x86_64_HOST_ARCH- [x64T]+ [x64T] #else- []+ [] #endif +pTest :: FunPtr (Int64 -> CUChar) -> TestTree+pTest pfn = testGroup "property tests" $+ [ testProperty "isPrime" $ property $ \n -> n < 2 || isPrime n == cb (ib pfn (fromIntegral n)) ]+ where+ cb 0=False; cb 1=True+ rTy :: TestTree rTy = testGroup "Regression tests" [ tyF "test/data/polymorphic.apple"@@ -55,8 +66,7 @@ , testCase "ncdf" $ do { res <- ncdfJit 2 ; res .?= ncdf 2 } , testCase "erf" $ do { res <- erfJit 2 ; res .?= erf 2 } , testCase "primes" $ do { res <- fpIa "test/data/primes.apple" 30; res @?= [T,T,F,T,F,T,F,F,F,T,F,T,F,F,F,T,F,T,F,F,F,T,F,F,F,F,F,T,F] }- , testCase "twoSum" $ do { res <- fpAaf "test/data/twoSum.apple" [1,2,3] [2,4,5] ; res @?= 17 }- , testCase "Floats?" $ do { res <- jitFact 50 ; res @?= 3.0414093201713376e64 }+ , testCase "primes-up-to" $ do { res <- fpIa "test/examples/primes.apple" 100; res @?= [2::Int64,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97] } , testCase "shoelace" $ do { res <- fpAaf "test/examples/shoelace.apple" [0,1,1] [0,0,1] ; res @?= 0.5 } , testCase "maxscan" $ do { res <- aaFp "bench/apple/scanmax.apple" [4::Int,6,1] ; res @?= [0::Int,4,6,6] } , testCase "b" $ do { res <- jitB [1,2,3] [2,4,6] ; res @?= 2 }@@ -90,12 +100,12 @@ c @?= 0.9999999999999999 last coeffs @?= (-0.28876537338066266,-0.02632401569273178,0.10638724282445484,0.342212204005514) , testCase "ℯ_" $ do { fp <- fpn "[e:(_x)]"; ff fp 1 @?= exp (-1) }- , testCase "ℯ" $ do { res <- jitE 2.5 ; res @?= exp 2.5 }+ , testCase "ℯ" $ do { f <- fpn "e:"; ff f 2.5 @?= exp 2.5 } , testCase "k-l" $ do { res <- jitKl [0.25, 0.25, 0.5] [0.66, 0.33, 0] ; res @?= kl [0.25, 0.25, 0.5] [0.66, 0.33, 0] } , testCase "fizzbuzz" $ do { (AA 1 [10] res) <- fpAa "test/examples/fizzbuzz.apple" (AA 1 [10] [0..9::Double]); res @?= [15.0,3.0,0.0,3.0,5.0,3.0,0.0,0.0,3.0,0.0::Double] }- , testCase "filt" $ do { (AA 1 [10] res) <- fpAa "test/examples/partition.apple" (AA 1 [10] [0..9::Double]); res @?= [0.0,0.0,0.0,0.0,0.0,0.0,1.0,1.0,1.0,1.0::Double] }+ , testCase "filt" $ do { (AA 1 [10] res) <- fpAa "test/examples/partition.apple" (AA 1 [10] [0..9::Double]); res @?= [F,F,F,F,F,F,T,T,T,T] } , testCase "gamma" $ do { res <- gammaJit (-3.5) ; res @?= gamma (-3.5) }- , testCase "tcdf" $ do { res <- fpFff "math/tcdf.apple" 2 12 ; res @?= tcdf 12 2 }+ , testCase "tcdf" $ do { res <- fpFff "math/tcdf.apple" 2 12 ; res ≈ tcdf 12 2 } , testCase "fcdf" $ do { res <- fpFfff "math/fcdf.apple" 5 2 2 ; res @?= 0.6339381452606089 } , testCase "chi-squared cdf" $ do { res <- fpFff "math/chisqcdf.apple" 2 2 ; res @?= chisqcdf 2 2 } , testCase "ramanujan" $ do { res <- fpFf "test/examples/ramanujanFact.apple" 7 ; res ≈ 5040 }@@ -214,11 +224,6 @@ (fp,_) <- bsFp code pure $ af fp p -jitE :: Double -> IO Double-jitE x = do- fp <- fpn "[e:x]"- pure $ ff fp x- jitExp :: Int64 -> Double -> IO Double jitExp = fpIff "test/examples/exp.apple" @@ -273,6 +278,7 @@ bytesE = either throw id . bytes +foreign import ccall "dynamic" ib :: FunPtr (Int64 -> CUChar) -> Int64 -> CUChar foreign import ccall "dynamic" ia :: FunPtr (Int64 -> U a) -> Int64 -> U a foreign import ccall "dynamic" ai :: FunPtr (U a -> Int64) -> U a -> Int64 foreign import ccall "dynamic" af :: FunPtr (U a -> Double) -> U a -> Double
− test/data/const.apple
@@ -1,4 +0,0 @@-{- fact ⟜ [(*)/ₒ 1 (𝒻 1 (x-1) (⌊x))];- fact 6+fact 7-}
+ test/data/filt.apple view
@@ -0,0 +1,1 @@+\p.\xs. (xs˙)'p⩪xs
+ test/data/pf.apple view
@@ -0,0 +1,8 @@+λn.+ { ni ⟜ ⌊(√(ℝn))+ ; pns ← (⍳ 2 ni 1)+ ; isPrime ← λn.¬((∨)/ₒ #f ([(n|x)=0]'(⍳ 2 (⌊(√(ℝn))) 1))); pf ⇐ (isPrime #.)+ ; pps ⟜ pf ((λk. ((n|k)=0)) #. pns)+ -- prime factors of n+ ; (pf (n⊲(n/.)'pps))⧺pps+ }
− test/data/twoSum.apple
@@ -1,5 +0,0 @@-\xs.\ys.-{- Σ ← [(+)/ₒ 0.0 x];- (Σ xs) + (Σ ys) + 0.0-}
− test/examples/ffact.apple
@@ -1,1 +0,0 @@-[(*)/ₒ 1 (frange 1 x (|.x))]
− test/examples/neuralNetwork.apple
@@ -1,10 +0,0 @@-{- softmax ← λx. {- -- TODO: softmax... what's the key for max?- xs ⟜ [ℯ(_x)]'1 x;- avg ← (+)/ 0 xs;- (%avg)'1 xs- };- sigmoid ← [1+ℯ(_x)];- sigmoid-}
test/examples/partition.apple view
@@ -1,1 +1,1 @@-([?x>5.0,.1.0,.0.0]')+((>5.0)')
test/examples/perimeter.apple view
@@ -1,5 +1,4 @@ λxs.λys.- { sum ← [(+)/ 0 x]- ; succDiff ← ((-)\~)- ; sum ([√(x^2+y^2)]`(succDiff xs) (succDiff ys))+ { succDiff ← ((-)\~)+ ; (+)/([√(x^2+y^2)]`(succDiff xs) (succDiff ys)) }
+ test/examples/primes.apple view
@@ -0,0 +1,5 @@+λN.+{+ isPrime ← λn.¬((∨)/ₒ #f ([(n|x)=0]'(⍳ 2 (⌊(√(ℝn))) 1)));+ isPrime § (irange 2 N 1)+}
− test/examples/sum.apple
@@ -1,1 +0,0 @@-[(+)/ x]
test/examples/xor.apple view
@@ -26,6 +26,6 @@ ; boa ← bo + sum l1Δ ; (wha,woa,bha,boa) };- wh ← (𝔯_1 1)::Arr (2 × 2) float;wo ← 𝔯_1 1;bh ← 𝔯_1 1;bo ← 𝔯_1 1;+ wh ⟜ 𝔯_1 1;wo ⟜ 𝔯_1 1;bh ⟜ 𝔯_1 1;bo ⟜ 𝔯_1 1; train^:10000 (wh,wo,bh,bo) }
+ test/harness/ia_harness.c view
@@ -0,0 +1,10 @@+#include <stdio.h>+#include <stdlib.h>++#include"../../include/apple_p.h"++extern U ia(J);++int main(int argc, char *argv[]) {+ pai(ia(30));+}
+ test/harness/ii_harness.c view
@@ -0,0 +1,10 @@+#include <stdio.h>+#include <stdlib.h>++#include"../../include/apple_p.h"++extern J ii(J);++int main(int argc, char *argv[]) {+ printf("%lld",ii(30));+}