Use symantic-document to write docType.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Bool / Test.hs

diff --git a/symantic-lib/Language/Symantic/Lib/Bool/Test.hs b/symantic-lib/Language/Symantic/Lib/Bool/Test.hs
index 032083acfb21d360f43951c1e01ea339777d1209..51ab1e9daa0b8901a029b0595cf3b35a64f24475 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Bool/Test.hs
+++ b/symantic-lib/Language/Symantic/Lib/Bool/Test.hs
@@ -6,57 +6,52 @@ import Test.Tasty
 import Data.Proxy (Proxy(..))
 import Prelude hiding ((&&), not, (||))
 
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Lib.Bool
-import Language.Symantic.Lib.Lambda ((~>))
-import Compiling.Term.Test
+import Language.Symantic
+import Language.Symantic.Lib
+-- import Language.Symantic.Lib.Lambda ((~>))
+import Compiling.Test
 
-type Ifaces =
+type SS =
  [ Proxy Bool
  , Proxy (->)
  , Proxy Integer
+ , Proxy []
+ , Proxy Char
  ]
-(==>) = test_compile @Ifaces
+(==>) = test_readTerm @() @SS
 
 tests :: TestTree
 tests = testGroup "Bool" $
- [ "True" ==> Right (ty @Bool, True, "True")
- , "xor True True" ==> Right (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
- , "xor False True" ==> Right (ty @Bool, True, "((\\x0 -> (\\x1 -> x0 `xor` x1)) False) True")
- , "True `xor` True" ==> Right (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
- , "(\\(x:Bool) -> x) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
- , "(\\(False:Bool) -> False) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
- , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right
-        (ty @Bool, True, "(\\x0 -> x0) (((\\x0 -> (\\x1 -> x0 `xor` x1)) False) True)")
- , "(\\(lett:Bool) -> lett) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
- , "(\\(x:Bool) -> xor x x) True" ==> Right
-        (ty @Bool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) x0) True")
- , "let x = True in xor x True" ==> Right
-        (ty @Bool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
+ [ "True"                           ==> Right (tyBool, True , "True")
+ , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")
+ , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")
+ , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")
+ , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")
+ , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")
+ , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")
+ , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")
+ , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")
+ , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")
  , testGroup "Error_Term"
-        [ "True True" ==> Left (ty @Bool,
-               Right $ Error_Term_Con_Type $
-               Right $ Con_TyApp $
-               At (maybeRight $ test_tokenizer "True") $
-               EType $ ty @Bool)
-        , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (ty @Bool,
-               Right $ Error_Term_unbound $ Term_Name "Bool")
-        , "(\\(x:Bool) -> x) True True" ==> Left (ty @Bool,
-               Right $ Error_Term_Con_Type $
-               Right $ Con_TyApp $
-               At (maybeRight $ test_tokenizer "(\\(x:Bool) -> x) True") $
-               EType $ ty @Bool)
-        , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (ty @Bool,
-               Right $ Error_Term_Con_Type $ Right $
-               Con_TyEq
-                (Right $ At (maybeRight $ test_tokenizer "(\\(x:Bool -> Bool) -> x True)") $
-                       EType $ (ty @Bool ~> ty @Bool))
-                (At (maybeRight $ test_tokenizer "True") $
-                       EType $ ty @Bool)
-                )
+        [ "True True" ==> Left (tyBool,
+               Right $ Error_Term_Beta $
+               Error_Beta_Term_not_a_function $
+               TypeVT $ tyBool @_ @'[])
+        , "x" ==> Left (tyBool,
+               Right $ Error_Term_unknown $ NameTe "x")
+        , "x `xor` True" ==> Left (tyBool,
+               Right $ Error_Term_unknown $ NameTe "x")
+        , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,
+               Right $ Error_Term_unknown $ NameTe "Bool")
+        , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,
+               Right $ Error_Term_Beta $
+               Error_Beta_Term_not_a_function $
+               TypeVT $ tyBool @_ @'[])
+        , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,
+               Right $ Error_Term_Beta $ Error_Beta_Unify $
+               Error_Unify_Const_mismatch
+                (TypeVT $ tyFun @_ @'[])
+                (TypeVT $ tyBool @_ @'[]))
         ]
  ]
 
@@ -66,10 +61,10 @@ class Sym_Bool_Vars repr where
        x :: repr Bool
        y :: repr Bool
        z :: repr Bool
-instance Sym_Bool_Vars TextI where
-       x = TextI $ \_p _v -> "x"
-       y = TextI $ \_p _v -> "y"
-       z = TextI $ \_p _v -> "z"
+instance Sym_Bool_Vars View where
+       x = View $ \_p _v -> "x"
+       y = View $ \_p _v -> "y"
+       z = View $ \_p _v -> "z"
 {-
 instance -- Trans_Boo_Const
  ( Sym_Bool repr