use UTF8 arrow consistently

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

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

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] =

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

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

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);

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);

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

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;
 

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];

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;

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);

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] =

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

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 */);

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() =

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);

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: *,

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))]

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;
 

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);

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)

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

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;

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;

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)
 ///