Term should have type and kind

cicada-lang · Apr 28, 2024 · 527d082 · 527d082
1 parent 397398b
commit 527d082
Show file tree

Hide file tree

Showing 30 changed files with 398 additions and 162 deletions.
diff --git a/TODO.md b/TODO.md
@@ -1,4 +1,4 @@
-`datatype` -- `Data` should have `type` and `kind`
+`Data` instead of `Term` -- only defined by `datatype`
 
 [maybe] remove eval
 [maybe] remove print -- find should print

diff --git a/docs/langs/lambda-closure.ch b/docs/langs/lambda-closure.ch
@@ -1,12 +1,12 @@
-clause Exp(var(name)) -- { String(name) }
-clause Exp(fn(name, ret)) -- { String(name) Exp(ret) }
-clause Exp(ap(target, arg)) -- { Exp(target) Exp(arg) }
+clause Exp(Exp::Var(name)) -- { String(name) }
+clause Exp(Exp::Fn(name, ret)) -- { String(name) Exp(ret) }
+clause Exp(Exp::Ap(target, arg)) -- { Exp(target) Exp(arg) }
 
 print find exp limit 10 {
   Exp(exp)
 }
 
-clause Value(closure(name, ret, env)) -- {
+clause Value(Value::Closure(name, ret, env)) -- {
   String(name)
   Exp(ret)
   Env(env)
@@ -26,26 +26,26 @@ clause Lookup([[key, _value] | rest], name, found)
   Lookup(rest, name, found)
 }
 
-clause Eval(env, var(name), value)
+clause Eval(env, Exp::Var(name), value)
 ---------------------------- var {
   Lookup(env, name, value)
 }
 
-clause Eval(env, fn(name, ret), value)
+clause Eval(env, Exp::Fn(name, ret), value)
 ---------------------------------- fn {
-  Equal(value, closure(name, ret, env))
+  Equal(value, Value::Closure(name, ret, env))
 }
 
-clause Eval(env, ap(target, arg), value)
+clause Eval(env, Exp::Ap(target, arg), value)
 ---------------------------------------- ap {
-  Eval(env, target, closure(name, ret, env2))
+  Eval(env, target, Value::Closure(name, ret, env2))
   Eval(env, arg, argValue)
   Eval([[name, argValue] | env2], ret, value)
 }
 
 print find exp limit 3 {
-  Equal(value, closure("y", var("x"), [
-    ["x", closure("z", var("z"), [])]
+  Equal(value, Value::Closure("y", Exp::Var("x"), [
+    ["x", Value::Closure("z", Exp::Var("z"), [])]
   ]))
   Eval([], exp, value)
 }
diff --git a/docs/langs/lambda-closure.ch.out b/docs/langs/lambda-closure.ch.out
@@ -1,20 +1,29 @@
 [ 
-  var(_.0) with { String(_.0) },
-  fn(_.0, var(_.1)) with { String(_.1) String(_.0) },
-  ap(var(_.0), var(_.1)) with { String(_.1) String(_.0) },
-  fn(_.0, fn(_.1, var(_.2))) with { String(_.2) String(_.1) String(_.0) },
-  fn(_.0, ap(var(_.1), var(_.2))) with { String(_.2) String(_.1) String(_.0) },
-  ap(var(_.0), fn(_.1, var(_.2))) with { String(_.2) String(_.1) String(_.0) },
-  ap(fn(_.0, var(_.1)), var(_.2)) with { String(_.2) String(_.1) String(_.0) },
-  fn(_.0, fn(_.1, fn(_.2, var(_.3)))) with { String(_.3) String(_.2) String(_.1) String(_.0) },
-  ap(var(_.0), ap(var(_.1), var(_.2))) with { String(_.2) String(_.1) String(_.0) },
-  ap(ap(var(_.0), var(_.1)), var(_.2)) with { String(_.2) String(_.1) String(_.0) }
+  Exp::Var(_.0) with { String(_.0) },
+  Exp::Fn(_.0, Exp::Var(_.1)) with { String(_.1) String(_.0) },
+  Exp::Ap(Exp::Var(_.0), Exp::Var(_.1)) with { String(_.1) String(_.0) },
+  Exp::Fn(_.0, Exp::Fn(_.1, Exp::Var(_.2))) with { String(_.2) String(_.1) String(_.0) },
+  Exp::Fn(_.0, Exp::Ap(Exp::Var(_.1), Exp::Var(_.2))) with { String(_.2) String(_.1) String(_.0) },
+  Exp::Ap(Exp::Var(_.0), Exp::Fn(_.1, Exp::Var(_.2))) with { String(_.2) String(_.1) String(_.0) },
+  Exp::Ap(Exp::Fn(_.0, Exp::Var(_.1)), Exp::Var(_.2)) with { String(_.2) String(_.1) String(_.0) },
+  Exp::Fn(_.0, Exp::Fn(_.1, Exp::Fn(_.2, Exp::Var(_.3)))) with { String(_.3) String(_.2) String(_.1) String(_.0) },
+  Exp::Ap(Exp::Var(_.0), Exp::Ap(Exp::Var(_.1), Exp::Var(_.2))) with { String(_.2) String(_.1) String(_.0) },
+  Exp::Ap(Exp::Ap(Exp::Var(_.0), Exp::Var(_.1)), Exp::Var(_.2)) with { String(_.2) String(_.1) String(_.0) }
 ]
 [ 
-  ap(fn("x", fn("y", var("x"))), fn("z", var("z"))),
-  ap(fn("x", ap(var("x"), fn("y", var("x")))), fn("z", var("z"))),
-  ap(
-    fn("x", ap(fn(_.0, var(_.0)), fn("y", var("x")))),
-    fn("z", var("z")),
+  Exp::Ap(
+    Exp::Fn("x", Exp::Fn("y", Exp::Var("x"))),
+    Exp::Fn("z", Exp::Var("z")),
+  ),
+  Exp::Ap(
+    Exp::Fn("x", Exp::Ap(Exp::Var("x"), Exp::Fn("y", Exp::Var("x")))),
+    Exp::Fn("z", Exp::Var("z")),
+  ),
+  Exp::Ap(
+    Exp::Fn(
+      "x",
+      Exp::Ap(Exp::Fn(_.0, Exp::Var(_.0)), Exp::Fn("y", Exp::Var("x"))),
+    ),
+    Exp::Fn("z", Exp::Var("z")),
   )
 ]
diff --git a/docs/langs/lambda-simple-type.ch b/docs/langs/lambda-simple-type.ch
@@ -1,9 +1,9 @@
-clause Exp(var(name)) -- { String(name) }
-clause Exp(fn(name, ret)) -- { String(name) Exp(ret) }
-clause Exp(ap(target, arg)) -- { Exp(target) Exp(arg) }
+clause Exp(Exp::Var(name)) -- { String(name) }
+clause Exp(Exp::Fn(name, ret)) -- { String(name) Exp(ret) }
+clause Exp(Exp::Ap(target, arg)) -- { Exp(target) Exp(arg) }
 
-clause Type(atom(name)) -- { String(name) }
-clause Type(arrow(argType, retType)) -- { Type(argType) Type(retType) }
+clause Type(Type::Atom(name)) -- { String(name) }
+clause Type(Type::Arrow(argType, retType)) -- { Type(argType) Type(retType) }
 
 clause Ctx([])
 clause Ctx([[name, type] | rest]) -- { String(name) Type(type) Ctx(rest) }
@@ -15,31 +15,31 @@ clause Lookup([[key, _value] | rest], name, found)
   Lookup(rest, name, found)
 }
 
-clause Check(ctx, var(name), type)
+clause Check(ctx, Exp::Var(name), type)
 ---------------------------- {
   Lookup(ctx, name, type)
 }
 
-clause Check(ctx, fn(name, ret), arrow(argType, retType))
+clause Check(ctx, Exp::Fn(name, ret), Type::Arrow(argType, retType))
 --------------------------------------------------- {
   Check([[name, argType] | ctx], ret, retType)
 }
 
-clause Check(ctx, ap(target, arg), retType)
+clause Check(ctx, Exp::Ap(target, arg), retType)
 ------------------------------------- {
-  Check(ctx, target, arrow(argType, retType))
+  Check(ctx, target, Type::Arrow(argType, retType))
   Check(ctx, arg, argType)
 }
 
 print find type {
   Equal(ctx, [])
-  Equal(exp, fn("x", var("x")))
+  Equal(exp, Exp::Fn("x", Exp::Var("x")))
   Check(ctx, exp, type)
 }
 
 print find exp limit 10 {
   Equal(ctx, [])
-  Equal(type, arrow("A", "A"))
+  Equal(type, Type::Arrow("A", "A"))
   Check(ctx, exp, type)
 }
 
@@ -51,6 +51,6 @@ print find exp limit 10 {
 
 print find type {
   Equal(ctx, [])
-  Equal(exp, fn("f", ap(var("f"), var("f"))))
+  Equal(exp, Exp::Fn("f", Exp::Ap(Exp::Var("f"), Exp::Var("f"))))
   Check(ctx, exp, type)
 }
diff --git a/docs/langs/lambda-simple-type.ch.out b/docs/langs/lambda-simple-type.ch.out
@@ -1,17 +1,38 @@
-[arrow(_.0, _.0)]
+[Type::Arrow(_.0, _.0)]
 [ 
-  fn(_.0, var(_.0)),
-  fn(_.0, ap(fn(_.1, var(_.1)), var(_.0))),
-  ap(fn(_.0, var(_.0)), fn(_.1, var(_.1))),
-  ap(fn(_.0, fn(_.1, var(_.1))), fn(_.2, var(_.2))),
-  fn(_.0, ap(fn(_.1, var(_.0)), var(_.0))) with { NotEqual(_.1, _.0) },
-  ap(fn(_.0, fn(_.1, var(_.1))), fn(_.2, fn(_.3, var(_.3)))),
-  fn(_.0, ap(fn(_.1, var(_.0)), fn(_.2, var(_.2)))) with { NotEqual(_.1, _.0) },
-  ap(
-    fn(_.0, fn(_.1, var(_.1))),
-    fn(_.2, fn(_.3, fn(_.4, var(_.4)))),
+  Exp::Fn(_.0, Exp::Var(_.0)),
+  Exp::Fn(_.0, Exp::Ap(Exp::Fn(_.1, Exp::Var(_.1)), Exp::Var(_.0))),
+  Exp::Ap(Exp::Fn(_.0, Exp::Var(_.0)), Exp::Fn(_.1, Exp::Var(_.1))),
+  Exp::Ap(
+    Exp::Fn(_.0, Exp::Fn(_.1, Exp::Var(_.1))),
+    Exp::Fn(_.2, Exp::Var(_.2)),
   ),
-  fn(_.0, ap(fn(_.1, var(_.1)), ap(fn(_.2, var(_.2)), var(_.0)))),
-  fn(_.0, ap(fn(_.1, var(_.0)), fn(_.2, fn(_.3, var(_.3))))) with { NotEqual(_.1, _.0) }
+  Exp::Fn(_.0, Exp::Ap(Exp::Fn(_.1, Exp::Var(_.0)), Exp::Var(_.0))) with { NotEqual(_.1, _.0) },
+  Exp::Ap(
+    Exp::Fn(_.0, Exp::Fn(_.1, Exp::Var(_.1))),
+    Exp::Fn(_.2, Exp::Fn(_.3, Exp::Var(_.3))),
+  ),
+  Exp::Fn(
+    _.0,
+    Exp::Ap(Exp::Fn(_.1, Exp::Var(_.0)), Exp::Fn(_.2, Exp::Var(_.2))),
+  ) with { NotEqual(_.1, _.0) },
+  Exp::Ap(
+    Exp::Fn(_.0, Exp::Fn(_.1, Exp::Var(_.1))),
+    Exp::Fn(_.2, Exp::Fn(_.3, Exp::Fn(_.4, Exp::Var(_.4)))),
+  ),
+  Exp::Fn(
+    _.0,
+    Exp::Ap(
+      Exp::Fn(_.1, Exp::Var(_.1)),
+      Exp::Ap(Exp::Fn(_.2, Exp::Var(_.2)), Exp::Var(_.0)),
+    ),
+  ),
+  Exp::Fn(
+    _.0,
+    Exp::Ap(
+      Exp::Fn(_.1, Exp::Var(_.0)),
+      Exp::Fn(_.2, Exp::Fn(_.3, Exp::Var(_.3))),
+    ),
+  ) with { NotEqual(_.1, _.0) }
 ]
 []
diff --git a/docs/std/nat/Add.ch b/docs/std/nat/Add.ch
@@ -2,8 +2,8 @@ import { Zero, Add1, Nat } from "Nat.ch"
 
 export { Add }
 
-clause Add(zero(), y, y)
-clause Add(add1(prev), y, add1(res))
+clause Add(Nat::Zero(), y, y)
+clause Add(Nat::Add1(prev), y, Nat::Add1(res))
 --------------------------- {
   Add(prev, y, res)
 }
diff --git a/docs/std/nat/Add.test.ch b/docs/std/nat/Add.test.ch
@@ -2,20 +2,20 @@ import { Zero, Add1, Nat } from "Nat.ch"
 import { Add } from "Add.ch"
 
 // trace steps 5 {
-//   Add1(add1(zero()), _x)
+//   Add1(Nat::Add1(Nat::Zero()), _x)
 // }
 
 print find x {
-  Add(x, x, zero())
+  Add(x, x, Nat::Zero())
 }
 
 print find x {
-  Add(x, x, add1(add1(zero())))
+  Add(x, x, Nat::Add1(Nat::Add1(Nat::Zero())))
 }
 
 // The following query diverges.
 
 // trace steps 5 {
 //   Add(x, y, z)
-//   Add(x, y, add1(z))
+//   Add(x, y, Nat::Add1(z))
 // }
diff --git a/docs/std/nat/Add.test.ch.out b/docs/std/nat/Add.test.ch.out
@@ -1,2 +1,2 @@
-[zero()]
-[add1(zero())]
+[Nat::Zero()]
+[Nat::Add1(Nat::Zero())]