diff --git a/lit/annex.mim b/lit/annex.mim index a46c12753..a094cdd60 100644 --- a/lit/annex.mim +++ b/lit/annex.mim @@ -4,7 +4,7 @@ plugin math; let %annex.Vec3.xyz = [x: %math.F64, y: %math.F64, z: %math.F64]; let %annex.Vec3.rgb = [r: %math.F64, g: %math.F64, w: %math.F64]; -rec %annex.Vec3.rpi: □ = %annex.Vec3.xyz -> %annex.Vec3.rpi; +rec %annex.Vec3.rpi: □ = %annex.Vec3.xyz → %annex.Vec3.rpi; let %annex.Vec3.zero = 0; // CHECK: zero = 0x8f3c66400000003 diff --git a/lit/autodiff/multiply2_autodiff.mim b/lit/autodiff/multiply2_autodiff.mim index 7c612716a..35a5aa749 100644 --- a/lit/autodiff/multiply2_autodiff.mim +++ b/lit/autodiff/multiply2_autodiff.mim @@ -16,7 +16,7 @@ con extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (I8, 0), 0) let c = 42I32; f_diff_cast (c,ret_cont) where - con ret_cont [r: I32, pb: Fn I32 -> I32] = + con ret_cont [r: I32, pb: Fn I32 → I32] = // return (mem, r) pb(1I32,pb_ret_cont) where diff --git a/lit/autodiff/multiply_autodiff.mim b/lit/autodiff/multiply_autodiff.mim index d8a9e4a4f..8afc9e492 100644 --- a/lit/autodiff/multiply_autodiff.mim +++ b/lit/autodiff/multiply_autodiff.mim @@ -15,7 +15,7 @@ con extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (I8, 0), 0) let c = 42I32; f_diff_cast (c,ret_cont) where - con ret_cont [r: I32, pb: Fn I32 -> I32] = + con ret_cont [r: I32, pb: Fn I32 → I32] = pb(1I32,pb_ret_cont) where con pb_ret_cont [pr:I32] = diff --git a/lit/autodiff/multiply_autodiff_cond.mim b/lit/autodiff/multiply_autodiff_cond.mim index b5670664b..9b3a8374e 100644 --- a/lit/autodiff/multiply_autodiff_cond.mim +++ b/lit/autodiff/multiply_autodiff_cond.mim @@ -23,7 +23,7 @@ con extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (I8, 0), 0) let c = 4I32; // 42 f_diff_cast (c,ret_cont) where - con ret_cont [r: I32, pb: Fn I32 -> I32] = + con ret_cont [r: I32, pb: Fn I32 → I32] = // return (mem, r) pb (1I32, pb_ret_cont) where diff --git a/lit/autodiff/multiply_autodiff_cond2.mim b/lit/autodiff/multiply_autodiff_cond2.mim index 00d292a8a..e1d44bd93 100644 --- a/lit/autodiff/multiply_autodiff_cond2.mim +++ b/lit/autodiff/multiply_autodiff_cond2.mim @@ -23,7 +23,7 @@ con extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (I8, 0), 0) let c = 7I32; // 42 f_diff_cast (c,ret_cont) where - con ret_cont [r: I32, pb: Fn I32 -> I32] = + con ret_cont [r: I32, pb: Fn I32 → I32] = // return (mem, r) pb(1I32,pb_ret_cont) where diff --git a/lit/autodiff/second/snd_order_man.mim b/lit/autodiff/second/snd_order_man.mim index a52a21576..1560a2aa8 100644 --- a/lit/autodiff/second/snd_order_man.mim +++ b/lit/autodiff/second/snd_order_man.mim @@ -5,7 +5,7 @@ plugin core; plugin autodiff; -fun g_diff(a:I32): [I32, Fn I32 -> I32] = +fun g_diff(a:I32): [I32, Fn I32 → I32] = let b = %core.wrap.add 0 (3I32, a); let c = %core.wrap.mul 0 (a, b); return (c, fn (s:I32): I32 = @@ -14,13 +14,13 @@ fun g_diff(a:I32): [I32, Fn I32 -> I32] = return c); fun f(a:I32): I32 = - con ret_cont [r:I32, pb: Fn I32 -> I32] = + con ret_cont [r:I32, pb: Fn I32 → I32] = con pb_ret_cont [pr:I32] = return pr; pb(1I32,pb_ret_cont); g_diff (a, ret_cont); con extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (I8, 0), 0), return : Cn [%mem.M, I32]] = - con ret_cont [r: I32, pb: Fn I32 -> I32] = + con ret_cont [r: I32, pb: Fn I32 → I32] = con pb_ret_cont [pr:I32] = let c = %core.wrap.mul 0 (100I32, r); let d = %core.wrap.add 0 (c, pr); diff --git a/lit/autodiff/simple_autodiff.mim b/lit/autodiff/simple_autodiff.mim index 8ebddeb22..411dd116d 100644 --- a/lit/autodiff/simple_autodiff.mim +++ b/lit/autodiff/simple_autodiff.mim @@ -14,7 +14,7 @@ con extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (I8, 0), 0) let c = 43I32; f_diff_cast (c,ret_cont) where - con ret_cont [r: I32, pb: Fn I32 -> I32] = + con ret_cont [r: I32, pb: Fn I32 → I32] = pb(1I32,pb_ret_cont) where con pb_ret_cont [pr:I32] = return (mem, pr); diff --git a/lit/autodiff/square.mim b/lit/autodiff/square.mim index a34fc1834..79f7ea54c 100644 --- a/lit/autodiff/square.mim +++ b/lit/autodiff/square.mim @@ -15,7 +15,7 @@ con extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (I8, 0), 0) let c = 42I32; f_diff_cast (c,ret_cont) where - con ret_cont [r: I32, pb: Fn I32 -> I32] = + con ret_cont [r: I32, pb: Fn I32 → I32] = // return (mem, r) pb(1I32,pb_ret_cont) where diff --git a/lit/beta_equiv.mim b/lit/beta_equiv.mim index b527886a3..7669f39dd 100644 --- a/lit/beta_equiv.mim +++ b/lit/beta_equiv.mim @@ -3,11 +3,11 @@ plugin core; plugin math; plugin mem; -rec Num = [T: *, add: [T, T] -> T]; +rec Num = [T: *, add: [T, T] → T]; lam my_add {pe: «2; Nat»} (a b: %math.F pe): %math.F pe = %math.arith.add 0 (a, b); let F64 = (%math.F64, my_add @%math.f64); -axm %bug.Arr: Num -> *; +axm %bug.Arr: Num → *; fun test [N: Num] [A: %bug.Arr N]: Nat = return 0; diff --git a/lit/bndr_as_expr.mim b/lit/bndr_as_expr.mim index e5f7e40a2..d372b3a43 100644 --- a/lit/bndr_as_expr.mim +++ b/lit/bndr_as_expr.mim @@ -1,4 +1,4 @@ // RUN: rm -f %t.ll // RUN: %mim %s -axm %foo.bar: [[Nat, Nat] -> Nat]; +axm %foo.bar: [[Nat, Nat] → Nat]; diff --git a/lit/clos/return_higher_order4.mim b/lit/clos/return_higher_order4.mim index 2ea9686ae..02810ec86 100644 --- a/lit/clos/return_higher_order4.mim +++ b/lit/clos/return_higher_order4.mim @@ -3,7 +3,7 @@ /* TODO: investigate and open error -mim: /plug/clos/phase/clos_conv.cpp:64: const mim::Def* mim::clos::clos_pack_dbg(const mim::Def*, const mim::Def*, const mim::Def*, const mim::Def*): Assertion `pi && env->type() == pi->dom(Clos_Env_Param)' failed. +mim: /plug/clos/phase/clos_conv.cpp:64: const mim::Def* mim::clos::clos_pack_dbg(const mim::Def*, const mim::Def*, const mim::Def*, const mim::Def*): Assertion `pi && env→type() == pi→dom(Clos_Env_Param)' failed. */ plugin core; diff --git a/lit/direct/ds2cps_ax_cps2ds_dependent2.mim b/lit/direct/ds2cps_ax_cps2ds_dependent2.mim index 0a1303559..e69b36e99 100644 --- a/lit/direct/ds2cps_ax_cps2ds_dependent2.mim +++ b/lit/direct/ds2cps_ax_cps2ds_dependent2.mim @@ -4,7 +4,7 @@ plugin core; plugin direct; -lam f(n: Nat, w: Nat): Fn Idx n -> Idx n = +lam f(n: Nat, w: Nat): Fn Idx n → Idx n = fn (a: Idx n): Idx n = let b = %core.conv.u n 42I32; let c = %core.wrap.add w (a,b); diff --git a/lit/direct/mut_dom_bug.mim b/lit/direct/mut_dom_bug.mim index 907d57d83..53c8ee283 100644 --- a/lit/direct/mut_dom_bug.mim +++ b/lit/direct/mut_dom_bug.mim @@ -1,7 +1,7 @@ // RUN: %mim %s -p direct -o - plugin core; -lam ForBody [n: Nat] = [%mem.M, Idx n] -> %mem.M; +lam ForBody [n: Nat] = [%mem.M, Idx n] → %mem.M; lam For {n: Nat} (start: Idx n, _end: Idx n) (mem: %mem.M) (it: ForBody n): %mem.M = lam loop [mem: %mem.M, i: Idx n] @(%core.pe.known i) : [%mem.M, Idx n] = diff --git a/lit/error/pi_redef.mim b/lit/error/pi_redef.mim index 6ca20687f..ca61f7b3f 100644 --- a/lit/error/pi_redef.mim +++ b/lit/error/pi_redef.mim @@ -1,4 +1,4 @@ // RUN: (! %mim %s 2>&1) | FileCheck %s -rec F = |~| Nat -> Nat; -rec F = |~| Nat -> Nat; +rec F = |~| Nat → Nat; +rec F = |~| Nat → Nat; // CHECK: error: redeclaration diff --git a/lit/ext_names.mim b/lit/ext_names.mim index 867f3d5f4..795d2e8fd 100644 --- a/lit/ext_names.mim +++ b/lit/ext_names.mim @@ -4,7 +4,7 @@ plugin core; rec %foo.Shape = [n: Nat, S: «n; Nat», T: *]; -axm %foo.len: %foo.Shape -> Nat, normalize_len; +axm %foo.len: %foo.Shape → Nat, normalize_len; lam %foo.Ptr s: %foo.Shape: * = %mem.Ptr0 «%foo.len s; s#T»; lam %fooIdx s: %foo.Shape: * = Idx (%foo.len s); lam get(s: %foo.Shape) (mem: %mem.M, p: %foo.Ptr s, i: %fooIdx s): [%mem.M, s#T] = (mem, bot:(s#T) /* dummy impl */); diff --git a/lit/fun.mim b/lit/fun.mim index 6990e947d..81b50de9d 100644 --- a/lit/fun.mim +++ b/lit/fun.mim @@ -13,17 +13,17 @@ fun extern main(mem: %mem.M, argc: I32, argv: Ptr (Ptr I8)): [%mem.M, I32] = ret (`mem, y) = foo $ (mem, 23I32); return (mem, %core.wrap.add 0 (x, y)); -lam f1(T: *)((x y: T), return: T -> ⊥): ⊥ = return x; +lam f1(T: *)((x y: T), return: T → ⊥): ⊥ = return x; con f2(T: *)((x y: T), return: Cn T) = return x; fun f3(T: *) (x y: T) = return x; -let g1 = lm (T: *)((x y: T), return: T -> ⊥): ⊥ = return x; +let g1 = lm (T: *)((x y: T), return: T → ⊥): ⊥ = return x; let g2 = cn (T: *)((x y: T), return: Cn T) = return x; let g3 = fn (T: *) (x y: T) = return x; -let F1 = [T:*] [T, T] [T -> ⊥] -> ⊥; +let F1 = [T:*] [T, T] [T → ⊥] → ⊥; let F2 =Cn [T:*] [T, T] [Cn T]; -let F3 =Fn [T:*] [T, T] -> T; +let F3 =Fn [T:*] [T, T] → T; fun bar(cond: Bool): Nat = con t() = diff --git a/lit/group.mim b/lit/group.mim index a02e27f46..a31f72857 100644 --- a/lit/group.mim +++ b/lit/group.mim @@ -1,4 +1,4 @@ // RUN: %mim %s -o - lam f(a b: Nat, x: «a; Nat»): Bool = ff; -axm %foo.F: [p e: Nat] -> *; -axm %foo.bar: {p e: Nat}::pe [Nat] [a b: %foo.F pe] -> %foo.F (p, e); +axm %foo.F: [p e: Nat] → *; +axm %foo.bar: {p e: Nat}::pe [Nat] [a b: %foo.F pe] → %foo.F (p, e); diff --git a/lit/let_ptrn.mim b/lit/let_ptrn.mim index 63f01f213..a4b8a3c22 100644 --- a/lit/let_ptrn.mim +++ b/lit/let_ptrn.mim @@ -1,6 +1,6 @@ // RUN: %mim %s -o - -axm %foo.F: * -> *; -axm %foo.f: [T: *] -> Nat -> %foo.F T; +axm %foo.F: * → *; +axm %foo.f: [T: *] → Nat → %foo.F T; fun extern f( T: *, diff --git a/lit/matrix/print_id_mat.mim b/lit/matrix/print_id_mat.mim index 1ba37d07c..d0407194e 100644 --- a/lit/matrix/print_id_mat.mim +++ b/lit/matrix/print_id_mat.mim @@ -21,7 +21,7 @@ con print_double_matrix_wrap [mem: %mem.M, k: Nat, l: Nat, m: %matrix.Mat (2, (k print_double_matrix(mem, k, l, m2, return); // lam extern internal_mapRed_matrix_const -// ![m: Nat, l: Nat, [p: Nat, e:Nat]] -> +// ![m: Nat, l: Nat, [p: Nat, e:Nat]] → // (Cn[ // [mem:%mem.M], // Cn[%mem.M,%matrix.Mat (2,(m, l),%math.F (p,e))] diff --git a/lit/rec_pi.mim b/lit/rec_pi.mim index 5bfca4a92..5e7e91a3f 100644 --- a/lit/rec_pi.mim +++ b/lit/rec_pi.mim @@ -2,11 +2,11 @@ axm %phase.Phase: *; -axm %phase.phase1: Bool -> %phase.Phase; -axm %phase.phase2: [] -> %phase.Phase; -axm %phase.phase3: [Nat, Bool] -> %phase.Phase; +axm %phase.phase1: Bool → %phase.Phase; +axm %phase.phase2: [] → %phase.Phase; +axm %phase.phase3: [Nat, Bool] → %phase.Phase; -rec PiPeline: * = %phase.Phase -> PiPeline; // got the pun? XD +rec PiPeline: * = %phase.Phase → PiPeline; // got the pun? XD axm %phase.pipe: PiPeline; diff --git a/lit/recursive_uniform_bug.mim b/lit/recursive_uniform_bug.mim index 341e822c7..5993192b3 100644 --- a/lit/recursive_uniform_bug.mim +++ b/lit/recursive_uniform_bug.mim @@ -1,6 +1,6 @@ // RUN: %mim %s -o - let Triple = [T: *, U: *, V: *]; -axm %bug.Box: Triple -> *; -axm %bug.test: [n: Nat] [Ss: «n; Triple», X: Triple] -> %bug.Box X; +axm %bug.Box: Triple → *; +axm %bug.test: [n: Nat] [Ss: «n; Triple», X: Triple] → %bug.Box X; lam l3 [S: Triple]: %bug.Box S = %bug.test 3 ((S, S, S), S); diff --git a/lit/regex/dont_compile.mim b/lit/regex/dont_compile.mim index 05b9ccf12..ea3260d77 100644 --- a/lit/regex/dont_compile.mim +++ b/lit/regex/dont_compile.mim @@ -3,7 +3,7 @@ import compile; -// we want to check the normalizer working -> that's much easier not having the lower_regex phase running :) +// we want to check the normalizer working → that's much easier not having the lower_regex phase running :) lam extern _compile(): %compile.Pipeline = %compile.pipe (%compile.single_pass_phase %compile.internal_cleanup_pass) diff --git a/lit/restructre_free_var.mim b/lit/restructre_free_var.mim index 87638561b..ab8694302 100644 --- a/lit/restructre_free_var.mim +++ b/lit/restructre_free_var.mim @@ -3,7 +3,7 @@ plugin core; -axm %foo.Mat: [n: Nat, S: «n; Nat», T: *] -> *; +axm %foo.Mat: [n: Nat, S: «n; Nat», T: *] → *; axm %foo.map_reduce: // out shape depends on in shape but is complex @@ -12,13 +12,13 @@ axm %foo.map_reduce: NI: «m; Nat», // input dimensions TI: «m; *», // input types SI: «i:m; «NI#i; Nat»» // input shapes - ] -> + ] → // for completeness sake // main arguments [ zero: T, // initial value - add: [T, T]->T, // reduction operation - mul: «i: m; TI#i» ->T, // inner combination + add: [T, T]→T, // reduction operation + mul: «i: m; TI#i» →T, // inner combination // out_index not needed => always ij (0 ... n) for n dimensions input: «x:m; @@ -27,7 +27,7 @@ axm %foo.map_reduce: %foo.Mat (NI#x,SI#x,TI#x) ] » - ] -> + ] → %foo.Mat (n,S,T); let test = %foo.map_reduce diff --git a/lit/sigma.mim b/lit/sigma.mim index 8e937afa2..efb1549da 100644 --- a/lit/sigma.mim +++ b/lit/sigma.mim @@ -19,7 +19,7 @@ rec Foo = [ Bar ]; -rec F: * = Nat -> F; // TODO make inference for F work again +rec F: * = Nat → F; // TODO make inference for F work again lam extern f1 v: Vec1: %math.F64 = v#x; lam extern F1 v: vec1: %math.F64 = v#X; diff --git a/src/mim/plug/affine/affine.mim b/src/mim/plug/affine/affine.mim index 4d3a0e29b..174113f1b 100644 --- a/src/mim/plug/affine/affine.mim +++ b/src/mim/plug/affine/affine.mim @@ -10,7 +10,7 @@ import mem; /// /// ## Operations /// -/// ### %affine.For +/// ### %%affine.For /// /// This operation ranges from (including) `begin` to (excluding) `end` using `step` as stride. /// In addition, this loop manages `n` loop accumulators whose initial values `init` must be given. @@ -29,8 +29,8 @@ axm %affine.For: /// /// ## Passes and Phases /// -/// ### %affine.lower_for_pass +/// ### %%affine.lower_for_pass /// -/// Loweres the %affine.For operation to recursive function calls. +/// Loweres the %%%affine.For operation to recursive function calls. /// axm %affine.lower_for_pass: %compile.Pass; diff --git a/src/mim/plug/autodiff/autodiff.mim b/src/mim/plug/autodiff/autodiff.mim index ac0b9fa16..b08fdf051 100644 --- a/src/mim/plug/autodiff/autodiff.mim +++ b/src/mim/plug/autodiff/autodiff.mim @@ -14,36 +14,36 @@ plugin core; /// /// ## Types /// -axm %autodiff.Tangent: * -> *, normalize_Tangent; +axm %autodiff.Tangent: * → *, normalize_Tangent; /// /// ## Operations /// -/// ### %autodiff.ad +/// ### %%autodiff.ad /// /// This axiom operates on functions and types. /// -/// For function types the augmented type is computed: `(T -> U) => (T -> U × (U -> T))` -axm %autodiff.AD: * -> *, normalize_AD; +/// For function types the augmented type is computed: `(T → U) => (T → U × (U → T))` +axm %autodiff.AD: * → *, normalize_AD; /// On closed terms (functions, operators, ho arguments, registered axioms, etc.) the augmented term is returned. /// The augmented term `f'` returns the result together with the pullback. /// `autodiff f = f' = λ args. (f args, f*)` -axm %autodiff.ad: {T: *} -> T -> %autodiff.AD T, normalize_ad; +axm %autodiff.ad: {T: *} → T → %autodiff.AD T, normalize_ad; /// -/// ### %autodiff.zero +/// ### %%autodiff.zero /// /// Represents universal zero such that `(zero T) +_T t = t`. /// -axm %autodiff.zero: [T: *] -> T, normalize_zero; +axm %autodiff.zero: [T: *] → T, normalize_zero; /// -/// ### %autodiff.add +/// ### %%autodiff.add /// /// A universal addition that consumes zeros and defaults to normal addition for scalar types. /// It lifts additions over types with structure and performs special casing for types with do not allow for addition. /// The sum construct performs addition over a list of terms. /// /// TODO: how do we handle summations that need memory? (grab current memory?) -axm %autodiff.add: {T: *} -> [T, T] -> T, normalize_add; -axm %autodiff.sum: [n:Nat, T: *] -> «n; T» -> T, normalize_sum; +axm %autodiff.add: {T: *} → [T, T] → T, normalize_add; +axm %autodiff.sum: [n:Nat, T: *] → «n; T» → T, normalize_sum; /// /// ## Passes and Phases /// @@ -79,20 +79,20 @@ let ad_phase = /// Appropiate cps2ds wrappers are introduced to handle that the augmented axioms are in cps where the original axioms were in ds. /// Example: /// ``` -/// mul' => args -> result*pullback +/// mul' => args → result*pullback /// call: r = mul (m,w) (a,b) /// res : r,r* = mul' (m,w) (a,b) /// ``` /// The types (with `Int` for `(Int w)`) are: /// ``` -/// mul : [m:Nat,w:Nat] -> [a:Int,b:Int] -> Int +/// mul : [m:Nat,w:Nat] → [a:Int,b:Int] → Int /// r : Int /// r* : cn[Int,cn[Int,Int]] /// ``` /// The pullback has to be in cps for compliance. /// ``` /// mul* := λ s. (s*b,s*a) -/// mul'_cps : [m:Nat,w:Nat] -> cn[[Int,Int],cn[Int, cn[Int,cn[Int,Int]]]] +/// mul'_cps : [m:Nat,w:Nat] → cn[[Int,Int],cn[Int, cn[Int,cn[Int,Int]]]] /// r,r* = (cps2ds (mul'_cps (m,w))) (a,b) /// ``` /// @@ -105,21 +105,21 @@ let ad_phase = /// The tuple pullback transports the partial pullbacks of the operands and handles the sums. /// By its nature the pullback of a tuple needs to be a sum. /// -/// ### %core.icmp.xYgLE (eq) +/// ### %%core.icmp.xYgLE (eq) /// /// The comparison pullback exists formally but is not used. /// fun extern internal_diff_core_icmp_xYgLE {s: Nat} (ab: «2; Idx s»)@tt: [Bool, Cn[Bool, Cn«2; Idx s»]] = return (%core.icmp.sle ab, fn [Bool]@tt: «2; Idx s» = return ‹2; 0:(Idx s)›); /// -/// ### %core.wrap.add +/// ### %%core.wrap.add /// /// s ↦ (s, s) /// fun extern internal_diff_core_wrap_add {s: Nat} (m: Nat) (ab: «2; Idx s»)@tt: [Idx s, Cn[Idx s, Cn«2; Idx s»]] = return (%core.wrap.add m ab, fn (i: Idx s)@tt: «2; Idx s» = return ‹2; i›); /// -/// ### %core.wrap.mul +/// ### %%core.wrap.mul /// /// s ↦ (s*b, s*a) /// diff --git a/src/mim/plug/clos/clos.mim b/src/mim/plug/clos/clos.mim index 9e0968173..8196f19fa 100644 --- a/src/mim/plug/clos/clos.mim +++ b/src/mim/plug/clos/clos.mim @@ -11,8 +11,8 @@ plugin core; /// ## Operations related to longjmp /// let %clos.BufPtr = %mem.Ptr0 I8; -axm %clos.alloc_jmpbuf: %mem.M -> [%mem.M, %clos.BufPtr]; -axm %clos.setjmp: [%mem.M, %clos.BufPtr] -> [%mem.M, I32]; +axm %clos.alloc_jmpbuf: %mem.M → [%mem.M, %clos.BufPtr]; +axm %clos.setjmp: [%mem.M, %clos.BufPtr] → [%mem.M, I32]; axm %clos.longjmp: Cn [%mem.M, %clos.BufPtr, I32]; /// /// ## Closure Attribute @@ -25,7 +25,7 @@ axm %clos.longjmp: Cn [%mem.M, %clos.BufPtr, I32]; /// * `esc`: lambda that escapes its parent scope /// * `bot`: no special use /// -axm %clos.attr(returning, freeBB, fstclassBB, esc, bottom): {T: *} [T] -> T, normalize_clos; +axm %clos.attr(returning, freeBB, fstclassBB, esc, bottom): {T: *} [T] → T, normalize_clos; /// /// ## Passes and Phases /// @@ -35,7 +35,7 @@ axm %clos.clos_conv_prep_pass: %compile.Pass; axm %clos.branch_clos_pass: %compile.Pass; axm %clos.lower_typed_clos_prep_pass: %compile.Pass; axm %clos.clos2sjlj_pass: %compile.Pass; -axm %clos.eta_red_bool_pass: Bool -> %compile.Pass; +axm %clos.eta_red_bool_pass: Bool → %compile.Pass; /// /// ### Phases /// diff --git a/src/mim/plug/compile/compile.mim b/src/mim/plug/compile/compile.mim index 2a059ed77..ed738ba3c 100644 --- a/src/mim/plug/compile/compile.mim +++ b/src/mim/plug/compile/compile.mim @@ -6,26 +6,26 @@ /// /// This plugin handles the optimization part of the compilation of Mim programs. /// Plugins can register passes and phases using the axioms from this plugin. -/// The program then can invoke the optimization pipeline by defining a function `_compile: [] -> %compile.Pipeline`. +/// The program then can invoke the optimization pipeline by defining a function `_compile: [] → %%compile.Pipeline`. /// /// ## Types /// -/// ### %compile.Pass -/// ### %compile.Phase +/// ### %%compile.Pass +/// ### %%compile.Phase /// /// Types for compilation passes and phases. /// axm %compile.Pass: *; axm %compile.Phase: *; /// -/// ### %compile.Pipeline -/// ### %compile.PassList +/// ### %%compile.Pipeline +/// ### %%compile.PassList /// /// Types for functions that accept an arbitrary number of phases and passes respectively. /// -rec %compile.Pipeline: □ = %compile.Phase -> %compile.Pipeline; -rec %compile.PassList: □ = %compile.Pass -> %compile.PassList; -rec %compile.CombinedPhase: □ = %compile.Phase -> %compile.CombinedPhase; +rec %compile.Pipeline: □ = %compile.Phase → %compile.Pipeline; +rec %compile.PassList: □ = %compile.Pass → %compile.PassList; +rec %compile.CombinedPhase: □ = %compile.Phase → %compile.CombinedPhase; /// /// (This is a forward declaration for opt.mim.) /// @@ -49,15 +49,15 @@ axm %compile.refly_plugin: %compile.Plugin; axm %compile.regex_plugin: %compile.Plugin; axm %compile.matrix_plugin: %compile.Plugin; /// -/// ### %opt.is_loaded +/// ### %%opt.is_loaded /// /// Indicates whether a plugin is loaded. /// The normalizer will statically evaluate this expression to a constant boolean. /// TODO: find correct point (not at parsing but before compilation) /// -// axm %opt.is_loaded: %opt.Plugin -> Bool; +// axm %opt.is_loaded: %opt.Plugin → Bool; /// -/// ### %compile.pipe +/// ### %%compile.pipe /// /// Given n phases, returns the representation of a pipeline. /// @@ -65,35 +65,35 @@ axm %compile.pipe: %compile.Pipeline; /// /// ## Passes and Phases /// -/// ### %compile.debug_phase +/// ### %%compile.debug_phase /// /// Given a log level, returns a phase that prints the externals (for log level >= 2). /// -axm %compile.debug_phase: Nat -> %compile.Phase; +axm %compile.debug_phase: Nat → %compile.Phase; /// -/// ### %compile.pass_phase +/// ### %%compile.pass_phase /// /// Given n passes, returns a phase that applies them in order. /// /// TODO: combine two pass_list axm %compile.pass_list: %compile.PassList; /// `pass_phase (pass_list pass1 ... passN) = passes_to_phase N (pass1, ..., passN)` -axm %compile.pass_phase: %compile.PassList -> %compile.Phase, normalize_pass_phase; -axm %compile.passes_to_phase: [n: Nat] -> «n; %compile.Pass» -> %compile.Phase; +axm %compile.pass_phase: %compile.PassList → %compile.Phase, normalize_pass_phase; +axm %compile.passes_to_phase: [n: Nat] → «n; %compile.Pass» → %compile.Phase; /// `combine_pass_list K (pass_list pass11 ... pass1N) ... (pass_list passK1 ... passKM) = pass_list pass11 ... p1N ... passK1 ... passKM` -axm %compile.combine_pass_list: [n: Nat] -> «n; %compile.PassList» -> %compile.PassList, normalize_combine_pass_list; +axm %compile.combine_pass_list: [n: Nat] → «n; %compile.PassList» → %compile.PassList, normalize_combine_pass_list; /// `single_pass_phase pass = passes_to_phase 1 pass` // TODO: as let instead of axiom -axm %compile.single_pass_phase: %compile.Pass -> %compile.Phase, normalize_single_pass_phase; +axm %compile.single_pass_phase: %compile.Pass → %compile.Phase, normalize_single_pass_phase; /// -/// ### %compile.combined_phase +/// ### %%compile.combined_phase /// /// Given n phases, returns a phase that applies them in order. /// axm %compile.phase_list: %compile.CombinedPhase; /// `combined_phase (phase_list phase1 ... phaseN) = phases_to_phase N (phase1, ..., phaseN)` -axm %compile.combined_phase: %compile.CombinedPhase -> %compile.Phase, normalize_combined_phase; -axm %compile.phases_to_phase: [n: Nat] -> «n; %compile.Phase» -> %compile.Phase; +axm %compile.combined_phase: %compile.CombinedPhase → %compile.Phase, normalize_combined_phase; +axm %compile.phases_to_phase: [n: Nat] → «n; %compile.Phase» → %compile.Phase; /// /// ### Passes /// @@ -102,11 +102,11 @@ axm %compile.phases_to_phase: [n: Nat] -> «n; %compile.Phase» -> %compile.Phas axm %compile.beta_red_pass: %compile.Pass; axm %compile.eta_red_pass: %compile.Pass; /// Eta expansion expects an instance of eta reduction as argument. -axm %compile.eta_exp_pass: %compile.Pass -> %compile.Pass; +axm %compile.eta_exp_pass: %compile.Pass → %compile.Pass; /// Scalarize expects an instance of eta expansion as argument. -axm %compile.scalarize_pass: %compile.Pass -> %compile.Pass; +axm %compile.scalarize_pass: %compile.Pass → %compile.Pass; /// Tail recursion elimination expects an instance of eta reduction as argument. -axm %compile.tail_rec_elim_pass: %compile.Pass -> %compile.Pass; +axm %compile.tail_rec_elim_pass: %compile.Pass → %compile.Pass; axm %compile.lam_spec_pass: %compile.Pass; axm %compile.ret_wrap_pass: %compile.Pass; /// has to be registered in the pipeline @@ -148,7 +148,7 @@ lam extern _fallback_compile(): %compile.Pipeline = default_core_pipeline; /// let empty_pass = %compile.nullptr_pass; let empty_phase = %compile.passes_to_phase 0 (); -axm %compile.plugin_select: [T: *] -> %compile.Plugin -> T -> T -> T; +axm %compile.plugin_select: [T: *] → %compile.Plugin → T → T → T; let plugin_phase = %compile.plugin_select %compile.Phase; let plugin_pass = %compile.plugin_select %compile.Pass; lam plugin_cond_phase(plug: %compile.Plugin, phase: %compile.Phase): %compile.Phase = plugin_phase plug phase empty_phase; diff --git a/src/mim/plug/core/core.mim b/src/mim/plug/core/core.mim index 33af8126a..8e9c00926 100644 --- a/src/mim/plug/core/core.mim +++ b/src/mim/plug/core/core.mim @@ -10,14 +10,14 @@ plugin mem; /// /// ## Nat Operations /// -/// ### %core.nat +/// ### %%core.nat /// /// Standard arithmetic operations on `Nat`s.
/// `%%core.nat.sub (a, b)` yields `0`, if `a` < `b`. /// -axm %core.nat(add, sub, mul): «2; Nat» -> Nat, normalize_nat; +axm %core.nat(add, sub, mul): «2; Nat» → Nat, normalize_nat; /// -/// ### %core.ncmp +/// ### %%core.ncmp /// /// Nat comparison is made of 3 disjoint relations: /// * `G`reater @@ -37,7 +37,7 @@ axm %core.nat(add, sub, mul): «2; Nat» -> Nat, normalize_nat; /// axm %core.ncmp(gle = f, glE = e, gLe = l, gLE = le, Gle = g, GlE = ge, GLe = ne, GLE = t): - «2; Nat» -> Bool, normalize_ncmp; + «2; Nat» → Bool, normalize_ncmp; /// /// ## Integer Operations /// @@ -58,13 +58,13 @@ let %core.mode.nuw = %core.mode.Us; let %core.mode.nsw = %core.mode.uS; let %core.mode.nusw = %core.mode.US; /// -/// ### %core.idx +/// ### %%core.idx /// /// Creates a literal of type `Idx s` from `l` while obeying mode `m`. /// axm %core.idx: [s: Nat] [m: Nat] [l: Nat] → Idx s, normalize_idx; /// -/// ### %core.bit1 +/// ### %%core.bit1 /// /// This *unary* bitwise operations offers all [4 possible operations](https://en.wikipedia.org/wiki/Truth_table#Unary_operations) as summarized in the following table: /// @@ -75,9 +75,9 @@ axm %core.idx: [s: Nat] [m: Nat] [l: Nat] → Idx s, normalize_idx; /// | id | x | o | identity | /// | t | x | x | always true | /// -axm %core.bit1(f, neg, id, t): {s: Nat} [m: Nat] [Idx s] -> Idx s, normalize_bit1; +axm %core.bit1(f, neg, id, t): {s: Nat} [m: Nat] [Idx s] → Idx s, normalize_bit1; /// -/// ### %core.bit2 +/// ### %%core.bit2 /// /// This *binary* bitwise operations offers all [16 possible operations](https://en.wikipedia.org/wiki/Truth_table#Truth_table_for_all_binary_logical_operators) as summarized in the following table: /// @@ -102,26 +102,26 @@ axm %core.bit1(f, neg, id, t): {s: Nat} [m: Nat] [Idx s] -> Idx s, normalize_bit /// axm %core.bit2( f, nor, nciff, nfst, niff, nsnd, xor_, nand, and_, nxor, snd, iff, fst, ciff, or_, t): - {s: Nat} [m: Nat] [«2; Idx s»] -> Idx s , normalize_bit2; + {s: Nat} [m: Nat] [«2; Idx s»] → Idx s , normalize_bit2; /// -/// ### %core.shr +/// ### %%core.shr /// /// Shift right: /// * [`a`rithmetic shift right](https://en.wikipedia.org/wiki/Arithmetic_shift) /// * [`l`ogical shift right](https://en.wikipedia.org/wiki/Logical_shift) /// -axm %core.shr(a, l): {s: Nat} [«2; Idx s»] -> Idx s, normalize_shr; +axm %core.shr(a, l): {s: Nat} [«2; Idx s»] → Idx s, normalize_shr; /// -/// ### %core.wrap +/// ### %%core.wrap /// /// Integer operations that may overflow. /// You can specify the desired behavior in the case of an overflow with the curried argument just in front of the actual argument by providing a mim::plug::core::Mode as `Nat`. /// -axm %core.wrap(add, sub, mul, shl): {s: Nat} [m: Nat] [«2; Idx s»] -> Idx s, normalize_wrap; +axm %core.wrap(add, sub, mul, shl): {s: Nat} [m: Nat] [«2; Idx s»] → Idx s, normalize_wrap; lam %core.minus {s: Nat} (m: Nat) (a: Idx s): Idx s = %core.wrap.sub m (0:(Idx s), a); /// -/// ### %core.div +/// ### %%core.div /// /// Signed and unsigned Integer division/remainder. /// @@ -129,9 +129,9 @@ lam %core.minus {s: Nat} (m: Nat) (a: Idx s): Idx s = %core.wrap.sub m (0:(Idx s /// For this reason, these axioms expect a `%%mem.M`. /// axm %core.div(sdiv, udiv, srem, urem): - {s: Nat} [%mem.M, «2; Idx s»] -> [%mem.M, Idx s], normalize_div; + {s: Nat} [%mem.M, «2; Idx s»] → [%mem.M, Idx s], normalize_div; /// -/// ### %core.icmp +/// ### %%core.icmp /// /// Integer comparison is made of 5 disjoint relations: /// * `X`: first operand plus, second minus @@ -202,55 +202,55 @@ axm %core.icmp(xygle = f, xyglE = e, xygLe, xygLE, XyGle = sg, XyGlE = sge, XyGLe, XyGLE, XYgle, XYglE, XYgLe, XYgLE, XYGle, XYGlE, XYGLe = ne, XYGLE = t): - {s: Nat} [«2; Idx s»] -> Bool , normalize_icmp; + {s: Nat} [«2; Idx s»] → Bool , normalize_icmp; /// -/// ### %core.extrema +/// ### %%core.extrema /// /// Minimum and Maximum of two Integers /// * un`s`igned or `S`igned /// * `m`inimum or `M`aximum /// -axm %core.extrema(sm=umin, sM=umax, Sm=smin, SM=smax): {s: Nat} [Idx s,Idx s] -> Idx s, normalize_extrema; +axm %core.extrema(sm=umin, sM=umax, Sm=smin, SM=smax): {s: Nat} [Idx s,Idx s] → Idx s, normalize_extrema; /// -/// ### %core.abs +/// ### %%core.abs /// /// Absolute value of an int /// /// @warning Computing the absolute value of an Integer with the lowest possible value leads to *undefined behavior*, which is why this axiom expects a `%%mem.M` /// -axm %core.abs: {s:Nat} [%mem.M, Idx s] -> [%mem.M, Idx s], normalize_abs; +axm %core.abs: {s:Nat} [%mem.M, Idx s] → [%mem.M, Idx s], normalize_abs; /// /// ## Conversions /// -/// ### %core.conv +/// ### %%core.conv /// /// Conversion between index types - both signed and unsigned - of different sizes. /// -axm %core.conv(s, u): {ss: Nat} [ds: Nat] [Idx ss] -> Idx ds, normalize_conv; +axm %core.conv(s, u): {ss: Nat} [ds: Nat] [Idx ss] → Idx ds, normalize_conv; /// -/// ### %core.bitcast +/// ### %%core.bitcast /// /// Bitcast to reinterpret a value as another type. /// Can be used for pointer / integer conversions as well as integer / nat conversions. /// -axm %core.bitcast: {S: *} [D: *] [S] -> D, normalize_bitcast; +axm %core.bitcast: {S: *} [D: *] [S] → D, normalize_bitcast; /// /// ## Other Operations /// -/// ### %core.trait +/// ### %%core.trait /// /// Yields the size or align of a type. /// -axm %core.trait(size, align): * -> Nat, normalize_trait; +axm %core.trait(size, align): * → Nat, normalize_trait; /// -/// ### %core.pe +/// ### %%core.pe /// /// Steers the partial evaluator. /// -axm %core.pe(hlt, run): [T: *] [T] -> T, normalize_pe; -axm %core.pe(known): {T: *} [T] -> Bool, normalize_pe; +axm %core.pe(hlt, run): [T: *] [T] → T, normalize_pe; +axm %core.pe(known): {T: *} [T] → Bool, normalize_pe; /// -/// ### %core.zip +/// ### %%core.zip /// /// [Zips](https://en.wikipedia.org/wiki/Zipping_(computer_science)) several tensors. /// @@ -266,5 +266,5 @@ axm %core.pe(known): {T: *} [T] -> Bool, normalize_pe; /// * `is`: the actual input tensors /// axm %core.zip: [r: Nat, s: «r; Nat»] - [n_i: Nat, Is: «n_i; *», n_o: Nat, Os: «n_o; *», f: «i: n_i; Is#i» -> «o: n_o; Os#o»] - [is: «i: n_i; «s; Is#i»»] -> «o: n_o; «s; Os#o»», normalize_zip; + [n_i: Nat, Is: «n_i; *», n_o: Nat, Os: «n_o; *», f: «i: n_i; Is#i» → «o: n_o; Os#o»] + [is: «i: n_i; «s; Is#i»»] → «o: n_o; «s; Os#o»», normalize_zip; diff --git a/src/mim/plug/demo/demo.mim b/src/mim/plug/demo/demo.mim index 312e48ca4..85e3fca4b 100644 --- a/src/mim/plug/demo/demo.mim +++ b/src/mim/plug/demo/demo.mim @@ -8,7 +8,7 @@ /// /// ## Operations /// -/// ### %democonst +/// ### %%demo.const_idx /// /// The 42 constant, evaluated using a normalizer axm %demo.const_idx: [n: Nat] → Idx n, normalize_const; diff --git a/src/mim/plug/direct/direct.mim b/src/mim/plug/direct/direct.mim index 4d9f2634f..1107fc888 100644 --- a/src/mim/plug/direct/direct.mim +++ b/src/mim/plug/direct/direct.mim @@ -15,17 +15,17 @@ import compile; /// /// ## Operations /// -/// ### %direct.ds2cps +/// ### %%direct.ds2cps /// -// axm %direct.ds2cps: [T: *, U: *] → (T -> U) → Cn [T, Cn U]; +// axm %direct.ds2cps: [T: *, U: *] → (T → U) → Cn [T, Cn U]; /// -/// ### %direct.cps2ds +/// ### %%direct.cps2ds /// /// This axiom lets the user call a cps function in direct style. /// The function is not converted. Only the call site is changed. /// -axm %direct.cps2ds: [T: *, U: *] -> Cn [T, Cn U] -> (T -> U), normalize_cps2ds, 2; -axm %direct.cps2ds_dep: [T: *, U: T -> *] -> Cn [t: T, Cn U t] -> [[t: T] -> U t], 2; +axm %direct.cps2ds: [T: *, U: *] → Cn [T, Cn U] → (T → U), normalize_cps2ds, 2; +axm %direct.cps2ds_dep: [T: *, U: T → *] → Cn [t: T, Cn U t] → [[t: T] → U t], 2; /// /// ## Passes and Phases /// diff --git a/src/mim/plug/math/math.mim b/src/mim/plug/math/math.mim index 9af4d73bc..3225aac30 100644 --- a/src/mim/plug/math/math.mim +++ b/src/mim/plug/math/math.mim @@ -10,12 +10,12 @@ /// /// ## Types /// -/// ### %math.F +/// ### %%math.F /// /// A floating-point type with `p` many bits as precision and `e` many bits as exponent. /// The sign bit is neither included in `p` nor in `e`. /// Thus, the total number of bits occupied by a value of this type is `p + e + 1`. -axm %math.F: «2; Nat» -> *; +axm %math.F: «2; Nat» → *; let %math.f16 = (10, 5); let %math.f32 = (23, 8); @@ -35,16 +35,16 @@ let %math.PXR24 = %math.F %math.pxr24; /// /// ## Numerical Operations /// -/// ### %math.arith +/// ### %%math.arith /// /// Arithmetic operations. axm %math.arith(add, sub, mul, div, rem): - {pe: «2; Nat»} [Nat] [«2; %math.F pe»] -> %math.F pe, normalize_arith; + {pe: «2; Nat»} [Nat] [«2; %math.F pe»] → %math.F pe, normalize_arith; lam %math.minus {pe: «2; Nat»} (m: Nat) (a: %math.F pe): %math.F pe = %math.arith.sub m (0:(%math.F pe), a); /// -/// ### %math.extrema +/// ### %%math.extrema /// /// Minimum and Maximum. /// * `m`in or `M`ax @@ -72,9 +72,9 @@ lam %math.minus {pe: «2; Nat»} (m: Nat) (a: %math.F pe): %math.F pe = /// axm %math.extrema(im = fmin, iM = fmax, Im = ieee754min, IM = ieee754max): - {pe: «2; Nat»} [Nat] [«2; %math.F pe»] -> %math.F pe, normalize_extrema; + {pe: «2; Nat»} [Nat] [«2; %math.F pe»] → %math.F pe, normalize_extrema; /// -/// ### %math.tri +/// ### %%math.tri /// /// [Trigonometric](https://en.wikipedia.org/wiki/Trigonometric_functions) and [hypberbolic](https://en.wikipedia.org/wiki/Hyperbolic_functions) functions. /// @@ -105,15 +105,15 @@ axm %math.tri(ahff = sin , ahfF = cos , ahFf = tan , ahFF, aHff = sinh = h, aHfF = cosh, aHFf = tanh, aHFF, Ahff = asin = a, AhfF = acos , AhFf = atan , AhFF, AHff = asinh , AHfF = acosh, AHFf = atanh, AHFF): - {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_tri; + {pe: «2; Nat»} [Nat] [%math.F pe] → %math.F pe, normalize_tri; /// -/// ### %math.pow +/// ### %%math.pow /// /// Power function: \f$x^y\f$ /// -axm %math.pow: {pe: «2; Nat»} [Nat] [«2; %math.F pe»] -> %math.F pe, normalize_pow; +axm %math.pow: {pe: «2; Nat»} [Nat] [«2; %math.F pe»] → %math.F pe, normalize_pow; /// -/// ### %math.rt +/// ### %%math.rt /// /// [Square](https://en.wikipedia.org/wiki/Square_root) and [cube root](https://en.wikipedia.org/wiki/Cube_root): /// @@ -122,9 +122,9 @@ axm %math.pow: {pe: «2; Nat»} [Nat] [«2; %math.F pe»] -> %math.F pe, normali /// | `%%math.rt.sq` | square root | \f$\sqrt{x}\f$ | /// | `%%math.rt.cb` | cube root |\f$\sqrt[3]{x}\f$ | /// -axm %math.rt(sq, cb): {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_rt; +axm %math.rt(sq, cb): {pe: «2; Nat»} [Nat] [%math.F pe] → %math.F pe, normalize_rt; /// -/// ### %math.exp +/// ### %%math.exp /// /// [Exponential function](https://en.wikipedia.org/wiki/Exponential_function) and [logarithm](https://en.wikipedia.org/wiki/Logarithm): /// * `L`ogarithm @@ -143,9 +143,9 @@ axm %math.rt(sq, cb): {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normali /// axm %math.exp(lbb = exp, lbB = exp2 = bin, lBb = exp10 = dec, lBB, Lbb = log, LbB = log2 , LBb = log10 , LBB): - {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_exp; + {pe: «2; Nat»} [Nat] [%math.F pe] → %math.F pe, normalize_exp; /// -/// ### %math.er +/// ### %%math.er /// /// [Error](https://en.wikipedia.org/wiki/Error_function) and [complementary error function](https://en.wikipedia.org/wiki/Error_function#Complementary_error_function). /// @@ -154,9 +154,9 @@ axm %math.exp(lbb = exp, lbB = exp2 = bin, lBb = exp10 = dec, lBB, /// | `%%math.er.f` | error function | \f$\frac{2}{\sqrt\pi}\int_0^x e^{-t^2}\,dt\f$ | /// | `%%math.er.fc` | complementary error function | \f$\frac{2}{\sqrt\pi}\int_x^\infty e^{-t^2}\,dt = 1 - \textrm{erf}(x)\f$ | /// -axm %math.er(f, fc): {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_er; +axm %math.er(f, fc): {pe: «2; Nat»} [Nat] [%math.F pe] → %math.F pe, normalize_er; /// -/// ### %math.gamma +/// ### %%math.gamma /// /// [Gamma function](https://en.wikipedia.org/wiki/Gamma_function) and its natural [logarithm](https://en.wikipedia.org/wiki/Gamma_function#The_log-gamma_function). /// @@ -165,15 +165,15 @@ axm %math.er(f, fc): {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normaliz /// | `%%math.gamma.t` | gamma function | \f$\Gamma(x) = \int_0^\infty t^{x-1} e^{-t}\,dt\f$ | /// | `%%math.gamma.l` | natural logarithm of gamma function | \f$\ln \mid \int_0^\infty t^{x-1} e^{-t}\,dt \mid\f$ | /// -axm %math.gamma(t, l): {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_gamma; +axm %math.gamma(t, l): {pe: «2; Nat»} [Nat] [%math.F pe] → %math.F pe, normalize_gamma; /// -/// ### %math.abs +/// ### %%math.abs /// /// [Absolute value](https://en.wikipedia.org/wiki/Absolute_value) of a floating point number /// -axm %math.abs: {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_abs; +axm %math.abs: {pe: «2; Nat»} [Nat] [%math.F pe] → %math.F pe, normalize_abs; /// -/// ### %math.round +/// ### %%math.round /// /// Common rounding operations for floating points: /// * `f`loor @@ -188,11 +188,11 @@ axm %math.abs: {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_abs; /// | `%%math.round.r`| [round to nearest integer](https://en.wikipedia.org/wiki/Rounding#Rounding_to_the_nearest_integer) | \f$round (x)\f$ | /// | `%%math.round.t`| [round towards zero](https://en.wikipedia.org/wiki/Rounding#Rounding_toward_zero) | \f$trunc (x)\f$ | /// -axm %math.round(f,c,r,t): {pe: «2; Nat»} [Nat] [%math.F pe] -> %math.F pe, normalize_round; +axm %math.round(f,c,r,t): {pe: «2; Nat»} [Nat] [%math.F pe] → %math.F pe, normalize_round; /// /// ## Other Operations /// -/// ### %math.cmp +/// ### %%math.cmp /// /// Floating point comparison is made of 4 disjoint relations: /// * `U`nordered (yields true if either operand is a QNAN) @@ -223,28 +223,28 @@ axm %math.cmp(ugle = f, uglE = e, ugLe = l, ugLE = le, uGle = g, uGlE = ge, uGLe = ne, uGLE = o, Ugle = u, UglE = ue, UgLe = ul, UgLE = ule, UGle = ug, UGlE = uge, UGLe = une, UGLE = t): - {pe: «2; Nat»} [Nat] [«2; %math.F pe»] -> Bool, normalize_cmp; + {pe: «2; Nat»} [Nat] [«2; %math.F pe»] → Bool, normalize_cmp; /// -/// ### %math.conv +/// ### %%math.conv /// /// Conversion between floating point and index types - both signed and unsigned - of different sizes. /// -axm %math.conv(s2f, u2f): { ss: Nat } [dpe: «2; Nat»] [ Idx ss] -> %math.F dpe, normalize_conv; -axm %math.conv(f2s, f2u): {spe: «2; Nat»} [ ds: Nat ] [%math.F spe] -> Idx ds, normalize_conv; -axm %math.conv(f2f): {spe: «2; Nat»} [dpe: «2; Nat»] [%math.F spe] -> %math.F dpe, normalize_conv; +axm %math.conv(s2f, u2f): { ss: Nat } [dpe: «2; Nat»] [ Idx ss] → %math.F dpe, normalize_conv; +axm %math.conv(f2s, f2u): {spe: «2; Nat»} [ ds: Nat ] [%math.F spe] → Idx ds, normalize_conv; +axm %math.conv(f2f): {spe: «2; Nat»} [dpe: «2; Nat»] [%math.F spe] → %math.F dpe, normalize_conv; /// -/// ### %math.slf +/// ### %%math.slf /// [Standard logistic function](https://en.wikipedia.org/wiki/Logistic_function) of a floating point number (\f$slf(x) = \frac{1}{1+e^{-x}}\f$) /// lam %math.slf {pe : <<2; Nat>>} (m : Nat) (x : %math.F pe): %math.F pe = %math.arith.div m ((%math.conv.f2f pe 1.0:(%math.F64)), %math.arith.add m ((%math.conv.f2f pe 1.0:(%math.F64)), %math.exp.exp m (%math.minus m x))); /// -/// ### %math.sgn +/// ### %%math.sgn /// [Sign function](https://en.wikipedia.org/wiki/Sign_function) lam %math.sgn {pe : <<2; Nat>>} (m : Nat) (x : %math.F pe): %math.F pe = ((%math.conv.f2f pe -1.0:(%math.F64)), ((%math.conv.f2f pe 0.0:(%math.F64)), (%math.conv.f2f pe 1.0:(%math.F64)))#(%math.cmp.g m (x,(%math.conv.f2f pe 0.0:(%math.F64)))))#(%math.cmp.ge m (x, (%math.conv.f2f pe 0.0:(%math.F64)))); /// -/// ### %math.rrt +/// ### %%math.rrt /// [Reciprocal](https://en.wikipedia.org/wiki/Multiplicative_inverse) of the [square root](https://en.wikipedia.org/wiki/Square_root) (\f$rrt(x) = \frac{1}{\sqrt{x}}\f$) lam %math.rrt {pe : <<2; Nat>>} (m : Nat) (x : %math.F pe): %math.F pe = %math.arith.div m (%math.conv.f2f pe 1.0:(%math.F64), %math.rt.sq m x); diff --git a/src/mim/plug/matrix/matrix.mim b/src/mim/plug/matrix/matrix.mim index 8b4138b25..b7c3495da 100644 --- a/src/mim/plug/matrix/matrix.mim +++ b/src/mim/plug/matrix/matrix.mim @@ -14,21 +14,21 @@ plugin affine; /// /// ## Types /// -/// ### %matrix.Mat +/// ### %%matrix.Mat /// /// Matrices are n-dimensional tensors with elements of type T. /// They can be seen as a generalization of Coq's vector type (a container with a fixed number of elements specified on type level). /// ``` -/// matrix = [n: Nat, S: «n; Nat», T: *] -> * +/// matrix = [n: Nat, S: «n; Nat», T: *] → * /// matrix n S T = «S_0; «S_1; ... «S_{n-1}; T» ... »» /// ``` /// => a matrix is a dependend array /// -axm %matrix.Mat: [n: Nat, S: «n; Nat», T: *] -> *; +axm %matrix.Mat: [n: Nat, S: «n; Nat», T: *] → *; /// /// ## Operations /// -/// ### %matrix.shape +/// ### %%matrix.shape /// /// Extracts the size along the i-th dimension from the type. /// For a dependent matrix this is a simple projection to S(i). @@ -36,14 +36,14 @@ axm %matrix.Mat: [n: Nat, S: «n; Nat», T: *] -> *; /// #### Normalization /// * resolve shape calls at construction by replacing them with the size argument /// -axm %matrix.shape: [n: Nat, S: «n; Nat», T: *]::nST [%matrix.Mat nST, i: Idx n] -> Nat, normalize_shape; +axm %matrix.shape: [n: Nat, S: «n; Nat», T: *]::nST [%matrix.Mat nST, i: Idx n] → Nat, normalize_shape; /// -/// ### %matrix.const +/// ### %%matrix.const /// /// a constant matrix -axm %matrix.constMat: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, T] -> [%mem.M, %matrix.Mat nST]; +axm %matrix.constMat: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, T] → [%mem.M, %matrix.Mat nST]; /// -/// ### %matrix.read +/// ### %%matrix.read /// /// read _ (mat, idx) : body_type /// @@ -54,9 +54,9 @@ axm %matrix.constMat: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, T] -> [%mem.M, /// * read(insert) /// * read(const) /// -axm %matrix.read: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, %matrix.Mat nST, idx: «i: n; Idx S#i»] -> [%mem.M, T], normalize_read; +axm %matrix.read: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, %matrix.Mat nST, idx: «i: n; Idx S#i»] → [%mem.M, T], normalize_read; /// -/// ### %matrix.insert +/// ### %%matrix.insert /// /// insert (dims, sizes, type) (mat, idx, val) : mat /// @@ -67,12 +67,12 @@ axm %matrix.read: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, %matrix.Mat nST, i /// * with other inserts /// * with initialization /// -axm %matrix.insert: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, %matrix.Mat nST, idx: «i: n; Idx S#i», val: T] -> [%mem.M, %matrix.Mat nST], normalize_insert; +axm %matrix.insert: [n: Nat, S: «n; Nat», T: *]::nST [%mem.M, %matrix.Mat nST, idx: «i: n; Idx S#i», val: T] → [%mem.M, %matrix.Mat nST], normalize_insert; /// -/// ### %matrix.init +/// ### %%matrix.init /// /// A fresh matrix with uninitialized values. -axm %matrix.init: [n: Nat, S: «n; Nat», T: *, %mem.M] -> [%mem.M, %matrix.Mat (n, S, T)]; +axm %matrix.init: [n: Nat, S: «n; Nat», T: *, %mem.M] → [%mem.M, %matrix.Mat (n, S, T)]; /// /// ### High-level matrix operations /// @@ -108,15 +108,15 @@ axm %matrix.sum: [n: Nat, S: «n; Nat», [p:Nat, e:Nat]] /// * `map f M = map_reduce (0,+, f,[(idx, M)])` (TODO: get rid of reduce step if not needed with dummy values) /// * `reduce acc f M = map_reduce (n=0) (acc, f, id,[(idx, M)])` (TODO: see index problem above) /// einsum application: -/// * `tranpose ij->ji (einsum(,[(1,0), M]))` -/// * `trace ii->` -/// * `sum ij ->` -/// * `col sum ij -> j ` -/// * `mat vec prod ik, k->i` -/// * `mat mat prod ik, kj -> ij` -/// * `dot product i, i ->` -/// * `dot matrix ij, ij ->` -/// * `outer product i, j -> ij` +/// * `tranpose ij→ji (einsum(,[(1,0), M]))` +/// * `trace ii→` +/// * `sum ij →` +/// * `col sum ij → j ` +/// * `mat vec prod ik, k→i` +/// * `mat mat prod ik, kj → ij` +/// * `dot product i, i →` +/// * `dot matrix ij, ij →` +/// * `outer product i, j → ij` /// TODO: introduce dummy values (zero, add, ...) in refly and use these /// dummy = has correct type but can not produce code (should always be eliminated) axm %matrix.map_reduce: @@ -131,10 +131,10 @@ axm %matrix.map_reduce: mem: %mem.M, // memory zero: T, // initial value // TODO: propagate change: no addition but instead take acc as argument (like mlir.linarith.generic) - comb: Fn [%mem.M, T, «i: m; TI#i»] -> [%mem.M, T], // inner combination + comb: Fn [%mem.M, T, «i: m; TI#i»] → [%mem.M, T], // inner combination // out_index not needed => always ij (0 ... n) for n dimensions input: «i: m; [«NI#i; Nat», %matrix.Mat (NI#i, SI#i, TI#i)]» - ] -> [%mem.M, %matrix.Mat (n, S, T)], + ] → [%mem.M, %matrix.Mat (n, S, T)], normalize_map_reduce; /// /// ## Unfolding functions diff --git a/src/mim/plug/mem/mem.mim b/src/mim/plug/mem/mem.mim index 08f49528e..7a48b2722 100644 --- a/src/mim/plug/mem/mem.mim +++ b/src/mim/plug/mem/mem.mim @@ -10,16 +10,16 @@ import compile; /// /// ## Types /// -/// ### %mem.M {#memM} +/// ### %%mem.M {#memM} /// /// This type tracks all kind of side-effects. axm %mem.M: *; /// -/// ### %mem.Ptr +/// ### %%mem.Ptr /// /// Pointer type with *pointee* type `T` and *address space* `as`. /// At the moment, the *address space* is not really used and a placeholder for future work. -axm %mem.Ptr: [*, Nat] -> *; +axm %mem.Ptr: [*, Nat] → *; lam %mem.Ptr0(T: *): * = %mem.Ptr (T, 0); /// @@ -28,59 +28,59 @@ lam %mem.Ptr0(T: *): * = %mem.Ptr (T, 0); /// The following operations have side effects. /// For this reason, they consume a `%%mem.M` and yield a new `%%mem.M`. /// -/// ### %mem.load +/// ### %%mem.load /// /// Loads from a pointer of type `%%mem.Ptr (T, as)` the pointed value of type `T`. -axm %mem.load: {T: *, Nat}::Tas [%mem.M, %mem.Ptr Tas] -> [%mem.M, T], normalize_load; +axm %mem.load: {T: *, Nat}::Tas [%mem.M, %mem.Ptr Tas] → [%mem.M, T], normalize_load; /// -/// ### %mem.store +/// ### %%mem.store /// /// Stores a value of type `T` to the location pointed to by a pointer of type `%%mem.Ptr (T, as)`, -axm %mem.store: {T: *, Nat}::Tas [%mem.M, %mem.Ptr Tas, T] -> %mem.M, normalize_store; +axm %mem.store: {T: *, Nat}::Tas [%mem.M, %mem.Ptr Tas, T] → %mem.M, normalize_store; /// -/// ### %mem.remem +/// ### %%mem.remem /// /// Creates a new dummy `%%mem.M`-typed value in order to acknowledge the fact that some unspecified side-effect happened. -axm %mem.remem: %mem.M -> %mem.M, normalize_remem; +axm %mem.remem: %mem.M → %mem.M, normalize_remem; /// -/// ### %mem.alloc +/// ### %%mem.alloc /// /// Allocates memory of type `T` in address space `as`. -axm %mem.alloc: [*, Nat]::Tas [%mem.M] -> [%mem.M, %mem.Ptr Tas]; +axm %mem.alloc: [*, Nat]::Tas [%mem.M] → [%mem.M, %mem.Ptr Tas]; /// -/// ### %mem.slot +/// ### %%mem.slot /// /// Reserves a memory slot for type `T` in address space `as`. /// `id` has to be provided a unique id. -axm %mem.slot: [*, Nat]::Tas [%mem.M, id: Nat] -> [%mem.M, %mem.Ptr Tas]; +axm %mem.slot: [*, Nat]::Tas [%mem.M, id: Nat] → [%mem.M, %mem.Ptr Tas]; /// -/// ### %mem.malloc +/// ### %%mem.malloc /// /// Allocates memory of type `T` in address space `as`. /// The difference to `%%mem.alloc` is that the `size` is automatically inferred. -axm %mem.malloc: [*, Nat]::Tas [%mem.M, Nat] -> [%mem.M, %mem.Ptr Tas]; +axm %mem.malloc: [*, Nat]::Tas [%mem.M, Nat] → [%mem.M, %mem.Ptr Tas]; /// -/// ### %mem.free +/// ### %%mem.free /// /// Frees memory of type `T` in address space `as`. -axm %mem.free: {*, Nat}::Tas [%mem.M, %mem.Ptr Tas] -> %mem.M; +axm %mem.free: {*, Nat}::Tas [%mem.M, %mem.Ptr Tas] → %mem.M; /// -/// ### %mem.mslot +/// ### %%mem.mslot /// /// Reserves a memory slot for type `T` in address space `as`. /// The reserved slot will be `size` bytes large. /// `id` has to be provided an unique id. -axm %mem.mslot: [*, Nat]::Tas [%mem.M, size: Nat, id: Nat] -> [%mem.M, %mem.Ptr Tas]; +axm %mem.mslot: [*, Nat]::Tas [%mem.M, size: Nat, id: Nat] → [%mem.M, %mem.Ptr Tas]; /// /// ## Operations w/o Side Effects /// -/// ### %mem.lea +/// ### %%mem.lea /// /// Load effective address. /// Performs address computation by offsetting the passed pointer with index `i`. -axm %mem.lea: [n: Nat, Ts: «n; *», as: Nat][%mem.Ptr («j: n; Ts#j», as), i: Idx n] -> %mem.Ptr (Ts#i, as), normalize_lea; +axm %mem.lea: [n: Nat, Ts: «n; *», as: Nat][%mem.Ptr («j: n; Ts#j», as), i: Idx n] → %mem.Ptr (Ts#i, as), normalize_lea; /// -/// ### %mem.create/destroy +/// ### %%mem.create/destroy /// /// Create side effect out of thin or pretend that the side effect does not exists. /// @warning Use with caution since you completely remove the `%%mem.M` dependency. @@ -88,7 +88,7 @@ axm %mem.lea: [n: Nat, Ts: «n; *», as: Nat][%mem.Ptr («j: n; Ts#j», as), i: let %mem.m = ⊤:%mem.M; lam %mem.ignore {O: *} (_: %mem.M, o: O): O = o; lam %mem.rm (n: Nat, Is: «n; *», O: *) - (f: [%mem.M, «i: n; Is#i»] -> [%mem.M, O]) + (f: [%mem.M, «i: n; Is#i»] → [%mem.M, O]) (is: «i: n; Is#i»): O = %mem.ignore (f (%mem.m, is)); /// @@ -105,12 +105,12 @@ axm %mem.reshape_arg: %mem.reshape_mode; /// ### Passes /// /// SSA pass expects eta expansion as argument -axm %mem.ssa_pass: %compile.Pass -> %compile.Pass; +axm %mem.ssa_pass: %compile.Pass → %compile.Pass; /// Copy propagation expects beta reduction and eta expansion as argument. -axm %mem.copy_prop_pass: [%compile.Pass, %compile.Pass, Bool] -> %compile.Pass; +axm %mem.copy_prop_pass: [%compile.Pass, %compile.Pass, Bool] → %compile.Pass; axm %mem.remem_elim_pass: %compile.Pass; axm %mem.alloc2malloc_pass: %compile.Pass; -axm %mem.reshape_pass: %mem.reshape_mode -> %compile.Pass; +axm %mem.reshape_pass: %mem.reshape_mode → %compile.Pass; /// /// ### Phases /// diff --git a/src/mim/plug/refly/refly.mim b/src/mim/plug/refly/refly.mim index f4ba5f002..a13947620 100644 --- a/src/mim/plug/refly/refly.mim +++ b/src/mim/plug/refly/refly.mim @@ -12,28 +12,28 @@ import compile; /// /// ## Types /// -axm %refly.Code: * -> *; +axm %refly.Code: * → *; /// /// ## Reify/Reflect /// -/// ### %refly.reify +/// ### %%refly.reify /// /// Yields the internal MimIR representation of a Mim expression as `%%refly.Code`. -axm %refly.reify: {T: *} [T] -> [%refly.Code T], normalize_reify; +axm %refly.reify: {T: *} [T] → [%refly.Code T], normalize_reify; /// -/// ### %refly.reflect +/// ### %%refly.reflect /// /// Converts a `%%refly.Code` back to a Mim expression. -axm %refly.reflect: {T: *} [%refly.Code T] -> T, normalize_reflect; +axm %refly.reflect: {T: *} [%refly.Code T] → T, normalize_reflect; /// /// ## Inspect /// -/// ### %refly.gid +/// ### %%refly.gid /// /// Retuns the internal mim::Def::gid of the argument. -axm %refly.gid: {T: *} [T] -> Nat, normalize_gid; +axm %refly.gid: {T: *} [T] → Nat, normalize_gid; /// -/// ### %refly.dbg +/// ### %%refly.dbg /// /// Debugs a given expression. /// * `tmp`: Prints debug information of a given expression at construction time and vanishes afterwards. @@ -46,15 +46,15 @@ let %refly.info = 2; let %refly.verbose = 3; let %refly.debug = 4; -axm %refly.dbg(tmp, perm): {T: *} [Nat, T] -> T, normalize_dbg; +axm %refly.dbg(tmp, perm): {T: *} [Nat, T] → T, normalize_dbg; /// /// ## Manipulate /// -/// ### %refly.refine +/// ### %%refly.refine /// /// Sets the `i`th operand of the reified Code `e` to `x`. // TODO type infere - not working right now -axm %refly.refine: [E: *, X: *][e: %refly.Code E, i: Nat, x: %refly.Code X] -> %refly.Code E, normalize_refine; +axm %refly.refine: [E: *, X: *][e: %refly.Code E, i: Nat, x: %refly.Code X] → %refly.Code E, normalize_refine; /// /// ## Passes and Phases /// diff --git a/src/mim/plug/regex/regex.mim b/src/mim/plug/regex/regex.mim index 2a9b653a3..9a105a87b 100644 --- a/src/mim/plug/regex/regex.mim +++ b/src/mim/plug/regex/regex.mim @@ -4,7 +4,7 @@ /// /// [TOC] /// -/// A normalizing regex plugin +/// A normalizing regex plugin. /// /// ## Dependencies /// @@ -22,45 +22,45 @@ let Char = I8; lam Str(n: Nat): * = %mem.Ptr0 «n; Char»; /// A regular expression matcher. lam Res (n: Nat): * = [%mem.M, Bool, Idx n]; -let RE = {n: Nat} [%mem.M, Str n, Idx n] -> Res n; +let RE = {n: Nat} [%mem.M, Str n, Idx n] → Res n; /// /// ## Meta /// -/// ### %regex.conj +/// ### %%regex.conj /// /// A sequence of RE's, e.g. `\d\d\d` matching 3 digits: /// `%%regex.conj (%%regex.cls.d, %%regex.cls.d, %%regex.cls.d)` /// -axm %regex.conj: [n: Nat][«n; RE»] -> RE, normalize_conj, 2; +axm %regex.conj: [n: Nat] [«n; RE»] → RE, normalize_conj, 2; /// -/// ### %regex.disj +/// ### %%regex.disj /// /// Match any of the sub expressions: `[0123456789]` /// -axm %regex.disj: [n: Nat][«n; RE»] -> RE, normalize_disj, 2; +axm %regex.disj: [n: Nat] [«n; RE»] → RE, normalize_disj, 2; /// /// ## Values /// -/// ### %regex.range +/// ### %%regex.range /// /// Wraps a range of literals. /// Use: `%%regex.range ('a', 'z')` to match all lower case letters. /// -axm %regex.range: «2; Char» -> RE, normalize_range, 1; +axm %regex.range: «2; Char» → RE, normalize_range, 1; /// -/// ### %regex.lit +/// ### %%regex.lit /// /// Wraps a literal. /// lam %regex.lit(val: Char) = %regex.range (val, val); /// -/// ### %regex.not +/// ### %%regex.not /// /// Do not match the parameter. /// -axm %regex.not_: RE -> RE, normalize_not, 1; +axm %regex.not_: RE → RE, normalize_not, 1; /// -/// ### %regex.cls.* +/// ### %%regex.cls.* /// /// | Subtag | Matches | /// |--------|--------------------------------| @@ -78,7 +78,7 @@ let %regex.cls.W = %regex.not_ %regex.cls.w; let %regex.cls.s = %regex.disj 3 (%regex.range ('\t', '\n'), %regex.lit '\r', %regex.lit ' '); let %regex.cls.S = %regex.not_ %regex.cls.s; /// -/// ### %regex.any +/// ### %%regex.any /// /// Match any character. /// @@ -86,9 +86,9 @@ axm %regex.any: RE; /// /// ## Quantifiers /// -/// ### %regex.quant.* +/// ### %%regex.quant.* /// -axm %regex.quant(optional,star,plus): RE -> RE, normalize_quant, 1; +axm %regex.quant(optional,star,plus): RE → RE, normalize_quant, 1; /// /// ## Passes and Phases ///