From 8fb14f6b3785c01b06bcd01ec314d2571a613e17 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Tue, 29 Oct 2024 23:34:41 -0300 Subject: [PATCH] Revert "Merge branch 'master' of github.com:higherorderco/kind" This reverts commit f8985f880ab634a9824dd3f544b61ee37059895f, reversing changes made to c459a64d70f00fb626db97adcee460d21917b810. --- src/Kind/API.hs | 4 +- src/Kind/Check.hs | 69 ++++++++------------------- src/Kind/Equal.hs | 25 ---------- src/Kind/Parse.hs | 116 +++++++++++++++------------------------------ src/Kind/Reduce.hs | 33 ------------- src/Kind/Show.hs | 13 ----- src/Kind/Type.hs | 14 ------ src/Kind/Util.hs | 78 +++++++++++------------------- 8 files changed, 90 insertions(+), 262 deletions(-) diff --git a/src/Kind/API.hs b/src/Kind/API.hs index 1b4026c04..9279e98b9 100644 --- a/src/Kind/API.hs +++ b/src/Kind/API.hs @@ -96,9 +96,9 @@ apiCheck bookPath (book, defs, _) defName defPath = do case M.lookup fileDefName book of Just term -> do case envRun (doCheck term) book of - Done state chkTerm -> do + Done state _ -> do apiPrintLogs state - apiPrintWarn chkTerm state + apiPrintWarn term state putStrLn $ "\x1b[32m✓ " ++ fileDefName ++ "\x1b[0m" return $ Right () Fail state -> do diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index efd3bd786..279c0b3ba 100644 --- a/src/Kind/Check.hs +++ b/src/Kind/Check.hs @@ -80,9 +80,6 @@ infer sus src term dep = debug ("infer:" ++ (if sus then "* " else " ") ++ showT go U64 = do return $ Ann False U64 Set - go I64 = do - return $ Ann False I64 Set - go F64 = do return $ Ann False F64 Set @@ -92,17 +89,29 @@ infer sus src term dep = debug ("infer:" ++ (if sus then "* " else " ") ++ showT go (Flt num) = do return $ Ann False (Flt num) F64 - go (Int num) = do - return $ Ann False (Int num) I64 go (Op2 opr fst snd) = do - envLog (Error src (Ref "annotation") (Ref "Op2") (Op2 opr fst snd) dep) - envFail - - go (Op1 opr fst) = do - envLog (Error src (Ref "annotation") (Ref "Op1") (Op1 opr fst) dep) - envFail + fstT <- infer sus src fst dep + sndT <- infer sus src snd dep + + let validTypes = [F64, U64] + isValidType <- checkValidType (getType fstT) validTypes dep + if not isValidType then do + envLog (Error src (Ref "Valid numeric type") (getType fstT) (Op2 opr fst snd) dep) + envFail + else do + typesEqual <- equal (getType fstT) (getType sndT) dep + if not typesEqual then do + envLog (Error src (getType fstT) (getType sndT) (Op2 opr fst snd) dep) + envFail + else do + book <- envGetBook + fill <- envGetFill + let reducedFst = reduce book fill 1 (getType fstT) + let returnType = getOpReturnType opr reducedFst + return $ Ann False (Op2 opr fstT sndT) returnType + go (Swi zer suc) = do envLog (Error src (Ref "annotation") (Ref "switch") (Swi zer suc) dep) envFail @@ -279,42 +288,6 @@ check sus src term typx dep = debug ("check:" ++ (if sus then "* " else " ") ++ otherwise -> infer sus src (Mat cse) dep otherwise -> infer sus src (Mat cse) dep - go (Op2 opr fst snd) = do - fstT <- infer sus src fst dep - sndT <- infer sus src snd dep - - t1 <- equal (getType fstT) typx dep - t2 <- equal (getType fstT) (getType sndT) dep - - if not t1 then do - envLog (Error src typx (getType fstT) (Op2 opr fst snd) dep) - envFail - else if not t2 then do - envLog (Error src (getType fstT) (getType sndT) (Op2 opr fst snd) dep) - envFail - else do - book <- envGetBook - fill <- envGetFill - let reducedFst = reduce book fill 1 (getType fstT) - let reducedSnd = reduce book fill 1 (getType sndT) - let returnType = getOpReturnType opr reducedFst reducedSnd - - return $ Ann False (Op2 opr fst snd) returnType - - go (Op1 opr fst) = do - fstT <- infer sus src fst dep - - t1 <- equal (getType fstT) typx dep - if not t1 then do - envLog (Error src typx (getType fstT) (Op1 opr fst) dep) - envFail - else do - book <- envGetBook - fill <- envGetFill - let reducedFst = reduce book fill 1 (getType fstT) - let returnType = getOp1ReturnType opr reducedFst - return $ Ann False (Op1 opr fst) returnType - go (Swi zer suc) = do book <- envGetBook fill <- envGetFill @@ -417,7 +390,7 @@ checkUnreachable src cNam term dep = go src cNam term dep where checkLater :: Bool -> Maybe Cod -> Term -> Term -> Int -> Env Term checkLater False src term typx dep = check False src term typx dep -checkLater True src term typx dep = envSusp (Check src term typx dep) >> return term +checkLater True src term typx dep = envSusp (Check src term typx dep) >> return (Met 0 []) doCheckMode :: Bool -> Term -> Env Term doCheckMode sus (Ann _ val typ) = do diff --git a/src/Kind/Equal.hs b/src/Kind/Equal.hs index 15247b119..595f7e747 100644 --- a/src/Kind/Equal.hs +++ b/src/Kind/Equal.hs @@ -114,21 +114,14 @@ identical a b dep = do return True go F64 F64 dep = return True - go I64 I64 dep = - return True go (Num aVal) (Num bVal) dep = return (aVal == bVal) go (Flt aVal) (Flt bVal) dep = return (aVal == bVal) - go (Int aVal) (Int bVal) dep = - return (aVal == bVal) go (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep = do iFst <- identical aFst bFst dep iSnd <- identical aSnd bSnd dep return (iFst && iSnd) - go (Op1 aOpr aFst) (Op1 bOpr bFst) dep = do - iFst <- identical aFst bFst dep - return iFst go (Swi aZer aSuc) (Swi bZer bSuc) dep = do iZer <- identical aZer bZer dep iSuc <- identical aSuc bSuc dep @@ -205,9 +198,6 @@ similar a b dep = go a b dep where eFst <- equal aFst bFst dep eSnd <- equal aSnd bSnd dep return (eFst && eSnd) - go (Op1 aOpr aFst) (Op1 bOpr bFst) dep = do - eFst <- equal aFst bFst dep - return eFst go (Swi aZer aSuc) (Swi bZer bSuc) dep = do eZer <- equal aZer bZer dep eSuc <- equal aSuc bSuc dep @@ -328,9 +318,6 @@ occur book fill uid term dep = go term dep where let o_fst = go fst dep o_snd = go snd dep in o_fst || o_snd - go (Op1 opr fst) dep = - let o_fst = go fst dep - in o_fst go (Swi zer suc) dep = let o_zer = go zer dep o_suc = go suc dep @@ -420,18 +407,12 @@ same U64 U64 dep = True same F64 F64 dep = True -same I64 I64 dep = - True same (Num aVal) (Num bVal) dep = aVal == bVal same (Flt aVal) (Flt bVal) dep = aVal == bVal -same (Int aVal) (Int bVal) dep = - aVal == bVal same (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep = same aFst bFst dep && same aSnd bSnd dep -same (Op1 aOpr aFst) (Op1 bOpr bFst) dep = - same aFst bFst dep same (Swi aZer aSuc) (Swi bZer bSuc) dep = same aZer bZer dep && same aSuc bSuc dep same (Txt aTxt) (Txt bTxt) dep = @@ -493,12 +474,9 @@ subst lvl neo term = go term where go Set = Set go U64 = U64 go F64 = F64 - go I64 = I64 go (Num n) = Num n go (Flt n) = Flt n - go (Int n) = Int n go (Op2 opr fst snd) = Op2 opr (go fst) (go snd) - go (Op1 opr fst) = Op1 opr (go fst) go (Txt txt) = Txt txt go (Lst lst) = Lst (map go lst) go (Nat val) = Nat val @@ -531,13 +509,10 @@ replace old neo term dep = if same old term dep then neo else go term where go (Hol nam ctx) = Hol nam (map (\x -> replace old neo x (dep+1)) ctx) go Set = Set go U64 = U64 - go I64 = I64 go F64 = F64 go (Num n) = Num n - go (Int n) = Int n go (Flt n) = Flt n go (Op2 opr fst snd) = Op2 opr (replace old neo fst dep) (replace old neo snd dep) - go (Op1 opr fst) = Op1 opr (replace old neo fst dep) go (Txt txt) = Txt txt go (Lst lst) = Lst (map (\x -> replace old neo x dep) lst) go (Nat val) = Nat val diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index f1af94dff..67ab73b56 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -3,7 +3,6 @@ module Kind.Parse where import Data.Char (ord) -import Data.Int (Int64) import Data.Functor.Identity (Identity) import Data.List (intercalate, isPrefixOf, uncons, find, transpose) import Data.Maybe (catMaybes, fromJust, isJust) @@ -71,15 +70,6 @@ name_end = do name_skp :: Parser String name_skp = name_end <* skip -kw_end :: String -> Parser String -kw_end s = do - x <- string_end s - P.notFollowedBy name_char - return x - -kw_skp :: String -> Parser String -kw_skp s = kw_end s <* skip - digit :: Parser Char digit = P.digit @@ -164,7 +154,6 @@ parseTerm = (do , parseMat , parseLam , parseEra - , parseOp1 , parseOp2 , parseApp , parseAnn @@ -182,7 +171,6 @@ parseTerm = (do , parseDo , parseSet , parseFloat - , parseInt , parseNum , parseTxt , parseLst @@ -224,7 +212,7 @@ parseApp = withSrc $ do fun <- parseTerm args <- P.many $ do P.notFollowedBy (char_end ')') - era <- P.optionMaybe (char_skp '~') + era <- P.optionMaybe (char_skp '-') arg <- parseTerm return (era, arg) char_end ')' @@ -385,7 +373,6 @@ parseRef = withSrc $ do return $ case name' of "U64" -> U64 "F64" -> F64 - "I64" -> I64 "Set" -> Set "_" -> Met 0 [] _ -> Ref name' @@ -428,28 +415,31 @@ parseSet = withSrc $ char_end '*' >> return Set parseFloat = withSrc $ P.try $ do + -- Parse optional negative sign sign <- P.option id $ P.char '-' >> return negate + + -- Parse integer part intPart <- P.many1 digit + + -- Parse decimal part (this must succeed, or we fail the whole parser) decPart <- do char_end '.' P.many1 digit + + -- Parse optional exponent expPart <- P.option 0 $ P.try $ do oneOf "eE" expSign <- P.option '+' (oneOf "+-") exp <- read <$> P.many1 digit return $ if expSign == '-' then -exp else exp + -- Combine parts into final float let floatStr = intPart ++ "." ++ decPart let value = (read floatStr :: Double) * (10 ^^ expPart) + -- Apply the sign to the final value return $ Flt (sign value) -parseInt = withSrc $ P.try $ do - sign <- P.choice [P.char '+' >> return id, P.char '-' >> return negate] - intPart <- P.many1 P.digit - let value = sign (read intPart :: Int64) - return $ Int value - parseNum = withSrc $ Num . read <$> P.many1 digit parseOp2 = withSrc $ do @@ -461,14 +451,6 @@ parseOp2 = withSrc $ do char_end ')' return $ Op2 opr fst snd -parseOp1 = withSrc $ do - opr <- P.try $ do - char_skp '(' - parseOper1 - fst <- parseTerm - char_end ')' - return $ Op1 opr fst - parseLst = withSrc $ do char_skp '[' elems <- P.many parseTerm @@ -521,7 +503,7 @@ parseHol = withSrc $ do return $ Hol nam ctx parseLog parseBody = withSrc $ do - P.try $ kw_skp "log" + P.try $ string_skp "log" msg <- parseTerm val <- parseBody return $ Log msg val @@ -545,12 +527,6 @@ parseOper = P.choice , P.try (string_skp "^") >> return XOR ] -parseOper1 = P.choice - [ P.try (string_skp "cos") >> return COS - , P.try (string_skp "sin") >> return SIN - , P.try (string_skp "tan") >> return TAN - ] - parseSuffix :: Term -> Parser Term parseSuffix term = P.choice [ parseSuffArr term @@ -594,7 +570,7 @@ parseDef = P.choice parseDefADT :: Parser (String, Term) parseDefADT = do - P.try $ kw_skp "data" + P.try $ string_skp "data " name <- name_skp params <- P.many $ do P.try $ char_skp '(' @@ -675,7 +651,7 @@ parseRule dep = P.try $ do pats <- P.many parsePattern with <- P.choice [ P.try $ do - kw_skp "with" + string_skp "with" wth <- P.many1 $ P.notFollowedBy (char_skp '.') >> parseTerm rul <- P.many1 $ parseRule (dep + 1) return $ WWit wth rul @@ -688,10 +664,9 @@ parseRule dep = P.try $ do parsePattern :: Parser Pattern parsePattern = do - P.notFollowedBy $ kw_skp "with" + P.notFollowedBy $ string_skp "with" P.choice [ parsePatternNat, - parsePatternLst, parsePatternCtr, parsePatternVar ] @@ -705,13 +680,6 @@ parsePatternNat = do let n = read num return $ (foldr (\_ acc -> PCtr "Succ" [acc]) (PCtr "Zero" []) [1..n]) -parsePatternLst :: Parser Pattern -parsePatternLst = do - P.try $ char_skp '[' - elems <- P.many parsePattern - char_skp ']' - return $ foldr (\x acc -> PCtr "Cons" [x, acc]) (PCtr "Nil" []) elems - parsePatternCtr :: Parser Pattern parsePatternCtr = do name <- P.try $ do @@ -731,25 +699,24 @@ parsePatternVar = do parseUses :: Parser Uses parseUses = P.many $ P.try $ do - kw_skp "use" + string_skp "use " long <- name_skp - kw_skp "as" + string_skp "as " short <- name_skp - return (short, long) + return (short ++ "/", long ++ "/") expandUses :: Uses -> String -> String -expandUses ((short, long):uses) name - | short == name = long - | (short ++ "/") `isPrefixOf` name = long ++ drop (length short) name - | otherwise = expandUses uses name -expandUses [] name = name +expandUses uses name = + case filter (\(short, _) -> short `isPrefixOf` name) uses of + (short, long):_ -> long ++ drop (length short) name + [] -> name -- Syntax Sugars -- ------------- parseDo :: Parser Term parseDo = withSrc $ do - P.try $ kw_skp "do" + P.try $ string_skp "do " monad <- name_skp char_skp '{' skip @@ -777,9 +744,7 @@ parseDoAsk monad = P.choice parseDoAskMch :: String -> Parser Term parseDoAskMch monad = do - P.try $ do - kw_skp "ask" - string_skp "#" + P.try $ string_skp "ask #" cnam <- name_skp char_skp '{' args <- P.many name_skp @@ -802,7 +767,7 @@ parseDoAskVal monad = P.choice parseDoAskValNamed :: String -> Parser Term parseDoAskValNamed monad = do nam <- P.try $ do - kw_skp "ask" + string_skp "ask " nam <- name_skp char_skp '=' return nam @@ -815,7 +780,7 @@ parseDoAskValNamed monad = do parseDoAskValAnon :: String -> Parser Term parseDoAskValAnon monad = do - P.try $ kw_skp "ask" + P.try $ string_skp "ask " exp <- parseTerm next <- parseStmt monad (_, _, uses) <- P.getState @@ -825,7 +790,7 @@ parseDoAskValAnon monad = do parseDoRet :: String -> Parser Term parseDoRet monad = do - P.try $ kw_skp "ret" + P.try $ string_skp "ret " exp <- parseTerm (_, _, uses) <- P.getState return $ App (App (Ref (monad ++ "/pure")) (Met 0 [])) exp @@ -835,13 +800,13 @@ parseDoFor monad = do (stt, nam, lst, loop, body) <- P.choice [ do stt <- P.try $ do - kw_skp "ask" + string_skp "ask " stt <- name_skp string_skp "=" - kw_skp "for" + string_skp "for" return stt nam <- name_skp - kw_skp "in" + string_skp "in" lst <- parseTerm char_skp '{' loop <- parseStmt monad @@ -849,9 +814,9 @@ parseDoFor monad = do body <- parseStmt monad return (Just stt, nam, lst, loop, body) , do - P.try $ kw_skp "for" + P.try $ string_skp "for " nam <- name_skp - kw_skp "in" + string_skp "in" lst <- parseTerm char_skp '{' loop <- parseStmt monad @@ -881,16 +846,16 @@ parseDoFor monad = do -- match cond { #True: t #False: f } parseIf = withSrc $ do - P.try $ kw_skp "if" + P.try $ string_skp "if " cond <- parseTerm t <- parseBranch True - kw_skp "else" + string_skp "else" f <- P.choice [parseBranch False, parseIf] return $ App (Mat [("True", t), ("False", f)]) cond where parseBranch isIf = P.choice [ do - kw_skp "do" + string_skp "do " monad <- name_skp char_skp '{' t <- parseStmt monad @@ -911,7 +876,7 @@ parseIf = withSrc $ do -- if (fn x c0) { v0 } else if (fn x c1) { v1 } else { df } parseWhen = withSrc $ do - P.try $ kw_skp "when" + P.try $ string_skp "when " fun <- parseTerm val <- parseTerm char_skp '{' @@ -939,7 +904,7 @@ parseWhen = withSrc $ do parseMatInl :: Parser Term parseMatInl = withSrc $ do - P.try $ kw_skp "match" + P.try $ string_skp "match " x <- parseTerm char_skp '{' cse <- parseMatCases @@ -948,7 +913,7 @@ parseMatInl = withSrc $ do parseSwiInl :: Parser Term parseSwiInl = withSrc $ do - P.try $ kw_skp "switch" + P.try $ string_skp "switch " x <- parseTerm char_skp '{' P.choice @@ -996,11 +961,8 @@ flattenDef rules depth = flattenWith :: Int -> With -> Term flattenWith dep (WBod bod) = bod flattenWith dep (WWit wth rul) = - -- Wrap the 'with' arguments and patterns in Pairs since the type checker only takes one match argument. - let wthA = foldr1 (\x acc -> Con "Pair" [(Nothing, x), (Nothing, acc)]) wth - rulA = map (\(pat, wth) -> ([foldr1 (\x acc -> PCtr "Pair" [x, acc]) pat], wth)) rul - bod = flattenDef rulA (dep + 1) - in App bod wthA + let bod = flattenDef rul (dep + 1) + in foldl App bod wth flattenRules :: [[Pattern]] -> [Term] -> Int -> Term flattenRules ([]:mat) (bod:bods) depth = bod diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index 6b681444e..359063abd 100644 --- a/src/Kind/Reduce.hs +++ b/src/Kind/Reduce.hs @@ -31,7 +31,6 @@ reduce book fill lv term = red term where red (Ref nam) = ref nam red (Let nam val bod) = red (bod (red val)) red (Use nam val bod) = red (bod (red val)) - red (Op1 opr fst) = op1 opr (red fst) red (Op2 opr fst snd) = op2 opr (red fst) (red snd) red (Txt val) = txt val red (Lst val) = lst val @@ -100,27 +99,8 @@ reduce book fill lv term = red term where op2 AND (Flt _) (Flt _) = error "Bitwise AND not supported for floating-point numbers" op2 OR (Flt _) (Flt _) = error "Bitwise OR not supported for floating-point numbers" op2 XOR (Flt _) (Flt _) = error "Bitwise XOR not supported for floating-point numbers" - op2 op (Ref nam) (Int snd) | lv > 0 = op2 op (ref nam) (Int snd) - op2 op (Int fst) (Ref nam) | lv > 0 = op2 op (Int fst) (ref nam) - op2 ADD (Int fst) (Int snd) = Int (fst + snd) - op2 SUB (Int fst) (Int snd) = Int (fst - snd) - op2 MUL (Int fst) (Int snd) = Int (fst * snd) - op2 DIV (Int fst) (Int snd) = Int (div fst snd) - op2 MOD (Int fst) (Int snd) = Int (mod fst snd) - op2 EQ (Int fst) (Int snd) = Num (if fst == snd then 1 else 0) - op2 NE (Int fst) (Int snd) = Num (if fst /= snd then 1 else 0) - op2 LT (Int fst) (Int snd) = Num (if fst < snd then 1 else 0) - op2 GT (Int fst) (Int snd) = Num (if fst > snd then 1 else 0) - op2 LTE (Int fst) (Int snd) = Num (if fst <= snd then 1 else 0) - op2 GTE (Int fst) (Int snd) = Num (if fst >= snd then 1 else 0) op2 opr fst snd = Op2 opr fst snd - op1 op (Ref nam) | lv > 0 = op1 op (ref nam) - op1 COS (Flt fst) = Flt (cos fst) - op1 SIN (Flt fst) = Flt (sin fst) - op1 TAN (Flt fst) = Flt (tan fst) - op1 opr fst = Op1 opr fst - ref nam | lv > 0 = case M.lookup nam book of Just val -> red val Nothing -> Con ("undefined-reference:"++nam) [] @@ -208,17 +188,12 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where go Set dep = Set go U64 dep = U64 go F64 dep = F64 - go I64 dep = I64 go (Num val) dep = Num val go (Flt val) dep = Flt val - go (Int val) dep = Int val go (Op2 opr fst snd) dep = let nf_fst = normal book fill lv fst dep in let nf_snd = normal book fill lv snd dep in Op2 opr nf_fst nf_snd - go (Op1 opr fst) dep = - let nf_fst = normal book fill lv fst dep in - Op1 opr nf_fst go (Txt val) dep = Txt val go (Lst val) dep = let nf_val = map (\x -> normal book fill lv x dep) val in @@ -305,17 +280,12 @@ bind (Use nam val bod) ctx = bind Set ctx = Set bind U64 ctx = U64 bind F64 ctx = F64 -bind I64 ctx = I64 bind (Num val) ctx = Num val bind (Flt val) ctx = Flt val -bind (Int val) ctx = Int val bind (Op2 opr fst snd) ctx = let fst' = bind fst ctx in let snd' = bind snd ctx in Op2 opr fst' snd' -bind (Op1 opr fst) ctx = - let fst' = bind fst ctx in - Op1 opr fst' bind (Txt txt) ctx = Txt txt bind (Lst lst) ctx = let lst' = map (\x -> bind x ctx) lst in @@ -391,9 +361,6 @@ genMetasGo (Op2 opr fst snd) c = let (fst', c1) = genMetasGo fst c (snd', c2) = genMetasGo snd c1 in (Op2 opr fst' snd', c2) -genMetasGo (Op1 opr fst) c = - let (fst', c1) = genMetasGo fst c - in (Op1 opr fst', c1) genMetasGo (Lst lst) c = let (lst', c1) = foldr (\t (acc, c') -> let (t', c'') = genMetasGo t c' in (t':acc, c'')) ([], c) lst in (Lst lst', c1) diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs index 8cfe99c4d..fbbad46fa 100644 --- a/src/Kind/Show.hs +++ b/src/Kind/Show.hs @@ -83,7 +83,6 @@ showTermGo small term dep = in concat ["use " , nam' , " = " , val' , " " , bod'] Set -> "*" U64 -> "U64" - I64 -> "I64" F64 -> "F64" Num val -> let val' = show val @@ -91,13 +90,6 @@ showTermGo small term dep = Flt val -> let val' = show val in concat [val'] - Int val -> - let val' = show val - in concat [val'] - Op1 opr fst -> - let opr' = showOper1 opr - fst' = showTermGo small fst dep - in concat ["(" , opr' , " ", fst', ")"] Op2 opr fst snd -> let opr' = showOper opr fst' = showTermGo small fst dep @@ -161,11 +153,6 @@ showOper XOR = "^" showOper LSH = "<<" showOper RSH = ">>" -showOper1 :: Oper1 -> String -showOper1 COS = "cos" -showOper1 SIN = "sin" -showOper1 TAN = "tan" - -- Pretty Printing (Sugars) -- ------------------------ diff --git a/src/Kind/Type.hs b/src/Kind/Type.hs index 54d315dd9..dbb238fba 100644 --- a/src/Kind/Type.hs +++ b/src/Kind/Type.hs @@ -5,7 +5,6 @@ import qualified Data.Map.Strict as M import Debug.Trace import Data.Word (Word64) -import Data.Int (Int64) -- Kind's AST data Term @@ -54,24 +53,15 @@ data Term -- F64 Type | F64 - -- I64 Type - | I64 - -- U64 Value | Num Word64 -- F64 Value | Flt Double - -- I64 Value - | Int Int64 - -- Binary Operation | Op2 Oper Term Term - -- Unary Operation - | Op1 Oper1 Term - -- U64 Elimination (updated to use splitting lambda) | Swi Term Term @@ -106,10 +96,6 @@ data Term data Loc = Loc String Int Int data Cod = Cod Loc Loc -data Oper1 - = COS | SIN | TAN - deriving Show - -- Numeric Operators data Oper = ADD | SUB | MUL | DIV diff --git a/src/Kind/Util.hs b/src/Kind/Util.hs index f298b91a2..a268e0a48 100644 --- a/src/Kind/Util.hs +++ b/src/Kind/Util.hs @@ -29,7 +29,6 @@ getDeps term = case term of Let _ val bod -> getDeps val ++ getDeps (bod Set) Use _ val bod -> getDeps val ++ getDeps (bod Set) Op2 _ fst snd -> getDeps fst ++ getDeps snd - Op1 _ fst -> getDeps fst Swi zer suc -> getDeps zer ++ getDeps suc Src _ val -> getDeps val Hol _ args -> concatMap getDeps args @@ -39,10 +38,8 @@ getDeps term = case term of Set -> [] U64 -> [] F64 -> [] - I64 -> [] Num _ -> [] Flt _ -> [] - Int _ -> [] Txt _ -> [] Lst elems -> concatMap getDeps elems Nat _ -> [] @@ -147,51 +144,32 @@ getForallNames (All nam _ bod) = nam : getForallNames (bod Set) getForallNames (Src _ val) = getForallNames val getForallNames _ = [] --- Returns the type of a numeric operation given its operands. -getOpReturnType :: Oper -> Term -> Term -> Term -getOpReturnType ADD U64 _ = U64 -getOpReturnType ADD F64 _ = F64 -getOpReturnType ADD I64 _ = I64 -getOpReturnType ADD _ U64 = U64 -getOpReturnType ADD _ F64 = F64 -getOpReturnType ADD _ I64 = F64 -getOpReturnType SUB U64 _ = U64 -getOpReturnType SUB F64 _ = F64 -getOpReturnType SUB I64 _ = I64 -getOpReturnType SUB _ U64 = U64 -getOpReturnType SUB _ F64 = F64 -getOpReturnType SUB _ I64 = I64 -getOpReturnType MUL U64 _ = U64 -getOpReturnType MUL F64 _ = F64 -getOpReturnType MUL I64 _ = I64 -getOpReturnType MUL _ U64 = U64 -getOpReturnType MUL _ F64 = F64 -getOpReturnType MUL _ I64 = I64 -getOpReturnType DIV U64 _ = U64 -getOpReturnType DIV F64 _ = F64 -getOpReturnType DIV I64 _ = I64 -getOpReturnType DIV _ U64 = U64 -getOpReturnType DIV _ F64 = F64 -getOpReturnType DIV _ I64 = I64 -getOpReturnType MOD U64 _ = U64 -getOpReturnType MOD I64 _ = I64 -getOpReturnType EQ _ _ = U64 -getOpReturnType NE _ _ = U64 -getOpReturnType LT _ _ = U64 -getOpReturnType GT _ _ = U64 -getOpReturnType LTE _ _ = U64 -getOpReturnType GTE _ _ = U64 -getOpReturnType AND U64 _ = U64 -getOpReturnType OR U64 _ = U64 -getOpReturnType XOR U64 _ = U64 -getOpReturnType LSH U64 _ = U64 -getOpReturnType RSH U64 _ = U64 -getOpReturnType opr t1 t2 = error ("Invalid operator: " ++ (show opr) ++ " Invalid operand types: " ++ (showTerm t1) ++ ", " ++ (showTerm t2)) - - -getOp1ReturnType :: Oper1 -> Term -> Term -getOp1ReturnType COS F64 = F64 -getOp1ReturnType SIN F64 = F64 -getOp1ReturnType TAN F64 = F64 -getOp1ReturnType opr t = error ("Invalid operator: " ++ (show opr) ++ " Invalid operand type: " ++ (showTerm t)) +getOpReturnType :: Oper -> Term -> Term +getOpReturnType ADD U64 = U64 +getOpReturnType ADD F64 = F64 +getOpReturnType SUB U64 = U64 +getOpReturnType SUB F64 = F64 +getOpReturnType MUL U64 = U64 +getOpReturnType MUL F64 = F64 +getOpReturnType DIV U64 = U64 +getOpReturnType DIV F64 = F64 +getOpReturnType MOD U64 = U64 +getOpReturnType EQ _ = U64 +getOpReturnType NE _ = U64 +getOpReturnType LT _ = U64 +getOpReturnType GT _ = U64 +getOpReturnType LTE _ = U64 +getOpReturnType GTE _ = U64 +getOpReturnType AND U64 = U64 +getOpReturnType OR U64 = U64 +getOpReturnType XOR U64 = U64 +getOpReturnType LSH U64 = U64 +getOpReturnType RSH U64 = U64 +getOpReturnType opr trm = error ("Invalid opertor: " ++ (show opr) ++ " Invalid operand type: " ++ (showTerm trm)) + +checkValidType :: Term -> [Term] -> Int -> Env Bool +checkValidType typ validTypes dep = foldr (\t acc -> do + isEqual <- equal typ t dep + if isEqual then return True else acc + ) (return False) validTypes