diff --git a/core/tests/core_eval_integration_test.rs b/core/tests/core_eval_integration_test.rs index f544d24..746dad1 100644 --- a/core/tests/core_eval_integration_test.rs +++ b/core/tests/core_eval_integration_test.rs @@ -33,7 +33,7 @@ type Nat { succ (n : Nat) } -@[terminating] +#[terminating] def length (xs : Stack) : Nat := match xs { cons _ tail => Nat.succ (length tail), diff --git a/core/tests/core_eval_native_integration_test.rs b/core/tests/core_eval_native_integration_test.rs index 1146f7e..796ccac 100644 --- a/core/tests/core_eval_native_integration_test.rs +++ b/core/tests/core_eval_native_integration_test.rs @@ -35,7 +35,7 @@ fn as_i64(v: &monad_core::core_value::Value) -> i64 { const FIB: &str = r#" use init -@[terminating] +#[terminating] def fib (n : I64) : I64 := if n == 0 then 0 @@ -60,13 +60,13 @@ fn phase5_evaluates_real_arithmetic_end_to_end() { const CLASS_DISPATCH: &str = r#" use init -@[terminating] +#[terminating] def build_list (n : I64) : List I64 := if n == 0 then List.empty else List.cons n (build_list (n - 1)) -@[terminating] +#[terminating] def count_eq (target : I64) (xs : List I64) : I64 := match xs { List.cons hd tl => @@ -90,7 +90,7 @@ fn phase5_evaluates_list_class_dispatch_end_to_end() { const STRING_OPS: &str = r#" use init -@[terminating] +#[terminating] def count_down (s : String) : I64 := if String.beq s "" then 0 @@ -126,19 +126,19 @@ type Step { stop (rest : String) } -@[partial] +#[partial] def skip_one (s : String) : String := if String.beq s "" then s else String.drop 1 s -@[partial] +#[partial] def step (label : I64) (s : String) : Step := if String.beq s "" then Step.stop s else Step.ok (skip_one s) label -@[terminating] +#[terminating] def chain (n : I64) (s : String) : I64 := match step n s { Step.ok rest label => label + (chain (label + 1) rest), diff --git a/wasm/web/examples.json b/wasm/web/examples.json index 37244f2..85381f6 100644 --- a/wasm/web/examples.json +++ b/wasm/web/examples.json @@ -9,7 +9,7 @@ }, { "name": "factorial", - "code": "use init\n\nuse math\n\n@[terminating]\ndef factorial (n : I64) : I64 :=\n if n == 0\n then 1\n else n * factorial (n - 1)\n\ndef main (args : List String) : I64 := factorial 5" + "code": "use init\n\nuse math\n\n#[terminating]\ndef factorial (n : I64) : I64 :=\n if n == 0\n then 1\n else n * factorial (n - 1)\n\ndef main (args : List String) : I64 := factorial 5" }, { "name": "list is_empty",