From 527d082cfd3210d9b8841d60d0963c3a7178460a Mon Sep 17 00:00:00 2001 From: Xie Yuheng Date: Sun, 28 Apr 2024 12:30:25 +0800 Subject: [PATCH] `Term` should have `type` and `kind` --- TODO.md | 2 +- docs/langs/lambda-closure.ch | 22 +- docs/langs/lambda-closure.ch.out | 39 ++- docs/langs/lambda-simple-type.ch | 24 +- docs/langs/lambda-simple-type.ch.out | 47 +++- docs/std/nat/Add.ch | 4 +- docs/std/nat/Add.test.ch | 8 +- docs/std/nat/Add.test.ch.out | 4 +- docs/std/nat/Mul.test.ch.out | 258 ++++++++++++++---- docs/std/nat/Nat.ch | 8 +- docs/std/nat/play.ch | 10 +- docs/std/nat/play.ch.out | 4 +- docs/tests/term/my-list.ch | 14 +- docs/tests/term/my-list.ch.out | 18 +- docs/tests/term/term-name-can-be-uppercase.ch | 3 - .../term/term-name-can-be-uppercase.ch.out | 1 - src/lang/equal/equal.ts | 2 +- src/lang/evaluate/evaluate.ts | 8 + src/lang/exp/Exp.ts | 27 +- src/lang/format/formatExp.ts | 4 + src/lang/format/formatValue.ts | 2 +- src/lang/match/match.ts | 2 +- src/lang/quote/quote.ts | 21 +- src/lang/refresh/refresh.ts | 3 +- src/lang/substitution/substitutionDeepWalk.ts | 3 +- src/lang/syntax/grammars/exp.ts | 1 + src/lang/syntax/matchers/exp_matcher.ts | 7 + src/lang/unify/unify.ts | 2 +- src/lang/value/Value.ts | 8 +- .../var-collection/varCollectionFromExp.ts | 4 + 30 files changed, 398 insertions(+), 162 deletions(-) delete mode 100644 docs/tests/term/term-name-can-be-uppercase.ch delete mode 100644 docs/tests/term/term-name-can-be-uppercase.ch.out diff --git a/TODO.md b/TODO.md index fdfbbf84..ceec60d6 100644 --- 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 index 923a5847..55bebb12 100644 --- 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 index c54697b5..d0c87842 100644 --- 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 index 67f688b6..2d8c11a4 100644 --- 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 index 467904c6..0fac40bd 100644 --- 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 index 4572ef98..4e6c38ca 100644 --- 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 index 0a4ded99..18829946 100644 --- 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 index aac8b764..1f2f5856 100644 --- 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())] diff --git a/docs/std/nat/Mul.test.ch.out b/docs/std/nat/Mul.test.ch.out index 332c227e..772472ed 100644 --- a/docs/std/nat/Mul.test.ch.out +++ b/docs/std/nat/Mul.test.ch.out @@ -1,119 +1,259 @@ -[add1(add1(add1(add1(zero()))))] +[Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))] [ - [add1(zero()), add1(add1(zero()))], - [add1(add1(zero())), add1(zero())] + [Nat::Add1(Nat::Zero()), Nat::Add1(Nat::Add1(Nat::Zero()))], + [Nat::Add1(Nat::Add1(Nat::Zero())), Nat::Add1(Nat::Zero())] ] [ - [add1(zero()), add1(add1(add1(add1(zero()))))], - [add1(add1(zero())), add1(add1(zero()))], - [add1(add1(add1(add1(zero())))), add1(zero())] + [ + Nat::Add1(Nat::Zero()), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))) + ], + [ + Nat::Add1(Nat::Add1(Nat::Zero())), + Nat::Add1(Nat::Add1(Nat::Zero())) + ], + [ + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))), + Nat::Add1(Nat::Zero()) + ] ] [ - [add1(zero()), add1(add1(add1(add1(add1(zero())))))], - [add1(add1(add1(add1(add1(zero()))))), add1(zero())] + [ + Nat::Add1(Nat::Zero()), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))) + ], + [ + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + Nat::Add1(Nat::Zero()) + ] ] [ - [add1(zero()), add1(add1(add1(add1(add1(add1(zero()))))))], - [add1(add1(zero())), add1(add1(add1(zero())))], - [add1(add1(add1(zero()))), add1(add1(zero()))], - [add1(add1(add1(add1(add1(add1(zero())))))), add1(zero())] + [ + Nat::Add1(Nat::Zero()), + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ) + ], + [ + Nat::Add1(Nat::Add1(Nat::Zero())), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))) + ], + [ + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))), + Nat::Add1(Nat::Add1(Nat::Zero())) + ], + [ + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + Nat::Add1(Nat::Zero()) + ] ] [ [ - add1(zero()), - add1(add1(add1(add1(add1(add1(add1(zero()))))))) + Nat::Add1(Nat::Zero()), + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ) ], [ - add1(add1(add1(add1(add1(add1(add1(zero()))))))), - add1(zero()) + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + Nat::Add1(Nat::Zero()) ] ] [ [ - add1(zero()), - add1(add1(add1(add1(add1(add1(add1(add1(zero())))))))) + Nat::Add1(Nat::Zero()), + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ) + ], + [ + Nat::Add1(Nat::Add1(Nat::Zero())), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))) ], - [add1(add1(zero())), add1(add1(add1(add1(zero()))))], - [add1(add1(add1(add1(zero())))), add1(add1(zero()))], [ - add1(add1(add1(add1(add1(add1(add1(add1(zero())))))))), - add1(zero()) + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))), + Nat::Add1(Nat::Add1(Nat::Zero())) + ], + [ + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + Nat::Add1(Nat::Zero()) ] ] [ [ - add1(zero()), - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))) + Nat::Add1(Nat::Zero()), + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ) ], - [add1(add1(add1(zero()))), add1(add1(add1(zero())))], [ - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))), - add1(zero()) + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))) + ], + [ + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ), + Nat::Add1(Nat::Zero()) ] ] [ [ - add1(zero()), - add1( - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))), + Nat::Add1(Nat::Zero()), + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ), ) ], - [add1(add1(zero())), add1(add1(add1(add1(add1(zero())))))], - [add1(add1(add1(add1(add1(zero()))))), add1(add1(zero()))], [ - add1( - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))), + Nat::Add1(Nat::Add1(Nat::Zero())), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))) + ], + [ + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + Nat::Add1(Nat::Add1(Nat::Zero())) + ], + [ + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ), ), - add1(zero()) + Nat::Add1(Nat::Zero()) ] ] [ [ - add1(zero()), - add1( - add1( - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))), + Nat::Add1(Nat::Zero()), + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ), ), ) ], [ - add1( - add1( - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))), + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ), ), ), - add1(zero()) + Nat::Add1(Nat::Zero()) ] ] [ [ - add1(zero()), - add1( - add1( - add1( - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))), + Nat::Add1(Nat::Zero()), + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ), ), ), ) ], [ - add1(add1(zero())), - add1(add1(add1(add1(add1(add1(zero())))))) + Nat::Add1(Nat::Add1(Nat::Zero())), + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ) + ], + [ + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))) ], - [add1(add1(add1(zero()))), add1(add1(add1(add1(zero()))))], - [add1(add1(add1(add1(zero())))), add1(add1(add1(zero())))], [ - add1(add1(add1(add1(add1(add1(zero())))))), - add1(add1(zero())) + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))), + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))) + ], + [ + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + Nat::Add1(Nat::Add1(Nat::Zero())) ], [ - add1( - add1( - add1( - add1(add1(add1(add1(add1(add1(add1(add1(add1(zero()))))))))), + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1( + Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero()))))), + ), + ), + ), + ), ), ), ), - add1(zero()) + Nat::Add1(Nat::Zero()) ] ] diff --git a/docs/std/nat/Nat.ch b/docs/std/nat/Nat.ch index 34e62e0f..3f1ebbf4 100644 --- a/docs/std/nat/Nat.ch +++ b/docs/std/nat/Nat.ch @@ -1,7 +1,7 @@ export { Nat, Zero, Add1 } -clause Nat(zero()) -clause Nat(add1(prev)) -- { Nat(prev) } +clause Nat(Nat::Zero()) +clause Nat(Nat::Add1(prev)) -- { Nat(prev) } -clause Zero(zero()) -clause Add1(prev, add1(prev)) +clause Zero(Nat::Zero()) +clause Add1(prev, Nat::Add1(prev)) diff --git a/docs/std/nat/play.ch b/docs/std/nat/play.ch index 398b1759..c9d6267a 100644 --- a/docs/std/nat/play.ch +++ b/docs/std/nat/play.ch @@ -1,6 +1,6 @@ clause LtEqThree(n) -------------- { - NotEqual(n, add1(add1(add1(zero())))) + NotEqual(n, Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))) } print find n { @@ -8,17 +8,17 @@ print find n { } print find _ { - LtEqThree(zero()) + LtEqThree(Nat::Zero()) } print find _ { - LtEqThree(add1(zero())) + LtEqThree(Nat::Add1(Nat::Zero())) } print find _ { - LtEqThree(add1(add1(zero()))) + LtEqThree(Nat::Add1(Nat::Add1(Nat::Zero()))) } print find _ { - LtEqThree(add1(add1(add1(zero())))) + LtEqThree(Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))) } diff --git a/docs/std/nat/play.ch.out b/docs/std/nat/play.ch.out index 138bbfda..d492c15d 100644 --- a/docs/std/nat/play.ch.out +++ b/docs/std/nat/play.ch.out @@ -1,4 +1,6 @@ -[_.0 with { NotEqual(_.0, add1(add1(add1(zero())))) }] +[ + _.0 with { NotEqual(_.0, Nat::Add1(Nat::Add1(Nat::Add1(Nat::Zero())))) } +] [_.0] [_.0] [_.0] diff --git a/docs/tests/term/my-list.ch b/docs/tests/term/my-list.ch index 72da1173..78a3abaf 100644 --- a/docs/tests/term/my-list.ch +++ b/docs/tests/term/my-list.ch @@ -1,16 +1,16 @@ -clause List(null) -clause List(cons(_head, tail)) -- { List(tail) } +clause List(List::Null()) +clause List(List::Cons(_head, tail)) -- { List(tail) } print find _ { - List(null) - List(cons(1, cons(2, cons(3, null)))) + List(List::Null()) + List(List::Cons(1, List::Cons(2, List::Cons(3, List::Null())))) } print find [list, x, y, z] { - Equal(list, cons(1, cons(2, cons(3, null)))) - Equal(list, cons(x, cons(y, cons(z, null)))) + Equal(list, List::Cons(1, List::Cons(2, List::Cons(3, List::Null())))) + Equal(list, List::Cons(x, List::Cons(y, List::Cons(z, List::Null())))) } print find [list, x, y, z] { - Equal(list, cons(x, cons(y, cons(z, null)))) + Equal(list, List::Cons(x, List::Cons(y, List::Cons(z, List::Null())))) } diff --git a/docs/tests/term/my-list.ch.out b/docs/tests/term/my-list.ch.out index 04abbf9c..380c28b2 100644 --- a/docs/tests/term/my-list.ch.out +++ b/docs/tests/term/my-list.ch.out @@ -1,3 +1,17 @@ [_.0] -[[cons(1, cons(2, cons(3, null))), 1, 2, 3]] -[[cons(_.0, cons(_.1, cons(_.2, null))), _.0, _.1, _.2]] +[ + [ + List::Cons(1, List::Cons(2, List::Cons(3, List::Null()))), + 1, + 2, + 3 + ] +] +[ + [ + List::Cons(_.0, List::Cons(_.1, List::Cons(_.2, List::Null()))), + _.0, + _.1, + _.2 + ] +] diff --git a/docs/tests/term/term-name-can-be-uppercase.ch b/docs/tests/term/term-name-can-be-uppercase.ch deleted file mode 100644 index 63fc05ca..00000000 --- a/docs/tests/term/term-name-can-be-uppercase.ch +++ /dev/null @@ -1,3 +0,0 @@ -print find x { - Equal(x, Uppercase()) -} diff --git a/docs/tests/term/term-name-can-be-uppercase.ch.out b/docs/tests/term/term-name-can-be-uppercase.ch.out deleted file mode 100644 index e71830fa..00000000 --- a/docs/tests/term/term-name-can-be-uppercase.ch.out +++ /dev/null @@ -1 +0,0 @@ -[Uppercase()] diff --git a/src/lang/equal/equal.ts b/src/lang/equal/equal.ts index aa745d35..11421d95 100644 --- a/src/lang/equal/equal.ts +++ b/src/lang/equal/equal.ts @@ -64,7 +64,7 @@ export function equal(left: Value, right: Value): boolean { } if (left["@kind"] === "Term" && right["@kind"] === "Term") { - if (left.name !== right.name) return false + if (left.kind !== right.kind) return false if (left.args.length !== right.args.length) return false for (const [i, leftArg] of left.args.entries()) { diff --git a/src/lang/evaluate/evaluate.ts b/src/lang/evaluate/evaluate.ts index a9785e24..ff885843 100644 --- a/src/lang/evaluate/evaluate.ts +++ b/src/lang/evaluate/evaluate.ts @@ -48,6 +48,14 @@ export function evaluate(mod: Mod, env: Env, exp: Exp): Value { return Values.Null() } + case "Term": { + return Values.Term( + exp.type, + exp.kind, + exp.args.map(arg => evaluate(mod, env, arg)) + ) + } + case "ListCons": { return Values.ListCons( evaluate(mod, env, exp.car), diff --git a/src/lang/exp/Exp.ts b/src/lang/exp/Exp.ts index 00dda47e..fd6a4bf9 100644 --- a/src/lang/exp/Exp.ts +++ b/src/lang/exp/Exp.ts @@ -8,6 +8,7 @@ export type Exp = | Number | Boolean | Null + | Term | ListCons | ListNull | Objekt @@ -100,6 +101,31 @@ export function Null(span: Span): Null { } } +export type Term = { + "@type": "Exp" + "@kind": "Term" + type: string + kind: string + args: Array + span: Span +} + +export function Term( + type: string, + kind: string, + args: Array, + span: Span, +): Term { + return { + "@type": "Exp", + "@kind": "Term", + type, + kind, + args, + span, + } +} + export type ListCons = { "@type": "Exp" "@kind": "ListCons" @@ -202,7 +228,6 @@ export function Fn(patterns: Array, stmts: Array, span: Span): Fn { } } - export type Eval = { "@type": "Exp" "@kind": "Eval" diff --git a/src/lang/format/formatExp.ts b/src/lang/format/formatExp.ts index b1a539c3..c2ca703e 100644 --- a/src/lang/format/formatExp.ts +++ b/src/lang/format/formatExp.ts @@ -24,6 +24,10 @@ export function formatExp(exp: Exp): string { return "null" } + case "Term": { + return `${exp.type}::${exp.kind}${formatArgs(exp.args)}` + } + case "ListCons": { const { elements, last } = foldListCons(exp.car, exp.cdr) return formatElements( diff --git a/src/lang/format/formatValue.ts b/src/lang/format/formatValue.ts index b1a03bb5..d581a200 100644 --- a/src/lang/format/formatValue.ts +++ b/src/lang/format/formatValue.ts @@ -56,7 +56,7 @@ export function formatValue(value: Value): string { case "Term": { const args = value.args.map(formatValue) - return `${value.name}${formatArgs(args)}` + return `${value.type}::${value.kind}${formatArgs(args)}` } case "Relation": { diff --git a/src/lang/match/match.ts b/src/lang/match/match.ts index 611ca8b1..5ac60c5e 100644 --- a/src/lang/match/match.ts +++ b/src/lang/match/match.ts @@ -124,7 +124,7 @@ export function match( } if (left["@kind"] === "Term" && right["@kind"] === "Term") { - if (left.name !== right.name) return undefined + if (left.kind !== right.kind) return undefined if (left.args.length !== right.args.length) return undefined for (const [i, leftArg] of left.args.entries()) { diff --git a/src/lang/quote/quote.ts b/src/lang/quote/quote.ts index a1a712ad..2e0a0f89 100644 --- a/src/lang/quote/quote.ts +++ b/src/lang/quote/quote.ts @@ -30,6 +30,14 @@ export function quote(mod: Mod, env: Env, exp: Exp): Value { return Values.Null() } + case "Term": { + return Values.Term( + exp.type, + exp.kind, + exp.args.map((arg) => quote(mod, env, arg)), + ) + } + case "ListCons": { return Values.ListCons(quote(mod, env, exp.car), quote(mod, env, exp.cdr)) } @@ -57,16 +65,9 @@ export function quote(mod: Mod, env: Env, exp: Exp): Value { } case "Ap": { - if (exp.target["@kind"] !== "Var") { - throw new Errors.LangError(`[quote] can not quote: ${formatExp(exp)}`, { - span: exp.span, - }) - } - - return Values.Term( - exp.target.name, - exp.args.map((arg) => quote(mod, env, arg)), - ) + throw new Errors.LangError(`[quote] can not quote: ${formatExp(exp)}`, { + span: exp.span, + }) } case "Fn": { diff --git a/src/lang/refresh/refresh.ts b/src/lang/refresh/refresh.ts index d26fa0a1..b39ac4e2 100644 --- a/src/lang/refresh/refresh.ts +++ b/src/lang/refresh/refresh.ts @@ -61,7 +61,8 @@ export function refresh( case "Term": { return Values.Term( - value.name, + value.type, + value.kind, value.args.map((arg) => refresh(renames, arg)), ) } diff --git a/src/lang/substitution/substitutionDeepWalk.ts b/src/lang/substitution/substitutionDeepWalk.ts index 5bea543f..69077a0c 100644 --- a/src/lang/substitution/substitutionDeepWalk.ts +++ b/src/lang/substitution/substitutionDeepWalk.ts @@ -32,7 +32,8 @@ export function substitutionDeepWalk( case "Term": { return Values.Term( - value.name, + value.type, + value.kind, value.args.map((arg) => substitutionDeepWalk(substitution, arg)), ) } diff --git a/src/lang/syntax/grammars/exp.ts b/src/lang/syntax/grammars/exp.ts index 33b0d406..88a5517b 100644 --- a/src/lang/syntax/grammars/exp.ts +++ b/src/lang/syntax/grammars/exp.ts @@ -24,6 +24,7 @@ export const operand = { "operand:false": ['"false"'], "operand:string": [{ data: { $pattern: ["string"] } }], "operand:number": [{ data: { $pattern: ["number"] } }], + "operand:term": [{ type: "relation_name" }, '":"', '":"', { kind: "relation_name" }, { args: "args" }], "operand:array": [ '"["', { elements: { $ap: ["zero_or_more", "exp", '","'] } }, diff --git a/src/lang/syntax/matchers/exp_matcher.ts b/src/lang/syntax/matchers/exp_matcher.ts index caef3926..5ac03916 100644 --- a/src/lang/syntax/matchers/exp_matcher.ts +++ b/src/lang/syntax/matchers/exp_matcher.ts @@ -31,6 +31,13 @@ export function operand_matcher(tree: pt.Tree): Exp { Exps.String(pt.trim_boundary(pt.str(data), 1), span), "operand:number": ({ data }, { span }) => Exps.Number(Number.parseFloat(pt.str(data)), span), + "operand:term": ({ type, kind, args }, { span }) => + Exps.Term( + pt.str(type), + pt.str(kind), + matchers.args_matcher(args), + span, + ), "operand:null": ({}, { span }) => Exps.Null(span), "operand:true": ({}, { span }) => Exps.Boolean(true, span), "operand:false": ({}, { span }) => Exps.Boolean(false, span), diff --git a/src/lang/unify/unify.ts b/src/lang/unify/unify.ts index 4478f04c..07a31a16 100644 --- a/src/lang/unify/unify.ts +++ b/src/lang/unify/unify.ts @@ -135,7 +135,7 @@ export function unify( } if (left["@kind"] === "Term" && right["@kind"] === "Term") { - if (left.name !== right.name) return undefined + if (left.kind !== right.kind) return undefined if (left.args.length !== right.args.length) return undefined for (const [i, leftArg] of left.args.entries()) { diff --git a/src/lang/value/Value.ts b/src/lang/value/Value.ts index 158a2b1c..c83baf22 100644 --- a/src/lang/value/Value.ts +++ b/src/lang/value/Value.ts @@ -154,15 +154,17 @@ export function Objekt(properties: Record, etc?: Value): Objekt { export type Term = { "@type": "Value" "@kind": "Term" - name: string + type: string + kind: string args: Array } -export function Term(name: string, args: Array): Term { +export function Term(type: string, kind: string, args: Array): Term { return { "@type": "Value", "@kind": "Term", - name, + type, + kind, args, } } diff --git a/src/lang/var-collection/varCollectionFromExp.ts b/src/lang/var-collection/varCollectionFromExp.ts index 96cfad2b..d32f2f39 100644 --- a/src/lang/var-collection/varCollectionFromExp.ts +++ b/src/lang/var-collection/varCollectionFromExp.ts @@ -22,6 +22,10 @@ export function varCollectionFromExp(exp: Exp): VarCollection { return createVarCollection() } + case "Term": { + return varCollectionMerge(exp.args.map(varCollectionFromExp)) + } + case "ListCons": { return varCollectionMerge([ varCollectionFromExp(exp.car),