Revert "Merge branch 'master' of github.com:higherorderco/kind"

This reverts commit f8985f8, reversing
changes made to c459a64.

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

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

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