(* Simple ML code for the paper *) open Print_code let genlet x = Print_code.code_of_val_code (Print_code. genlet x) let genletrec : (('a->'b) code -> 'a code -> 'b code) -> ('a->'b) code = fun f -> genlet .. ..) in g>. let fib x y n = let rec loop n = if n = 0 then x else if n = 1 then y else loop (n-1) + loop (n-2) in loop n let 8 = fib 1 1 5;; (* The same fib, but in the open recursion style *) let fibnr plus x y self n = if n = 0 then x else if n = 1 then y else plus (self (n-1)) (self (n-2)) let rec fix f x = f (fix f) x (* Tying the knot using the ordinary fixpoint *) let 8 = fix (fibnr (+) 1 1) 5;; let splus : int code -> int code -> int code = fun x y -> .<.~x + .~y>. let _ = . .~(fix (fibnr splus .. ..) 5)>. (* - : (int -> int -> int) code = .< fun x_1 -> fun y_2 -> (((y_2 + x_1) + y_2) + (y_2 + x_1)) + ((y_2 + x_1) + y_2)>. *) let mfix' : (('a -> 'b code) -> ('a -> 'b code)) -> ('a -> 'b code) = fun f x -> let memo = ref [] in let rec loop n = match List.assoc n !memo with | x -> x | exception Not_found -> let v = (f loop n) in memo := (n,v) :: !memo; v in loop x let _ = . .~(mfix' (fibnr splus .. ..) 5)>. (* No memoization: why? - : (int -> int -> int) code = .< fun x_3 -> fun y_4 -> (((y_4 + x_3) + y_4) + (y_4 + x_3)) + ((y_4 + x_3) + y_4)>. *) let mfix : (('a -> 'b code) -> ('a -> 'b code)) -> ('a -> 'b code) = fun f x -> let memo = ref [] in let rec loop n = match List.assoc n !memo with | x -> x | exception Not_found -> let v = genlet (f loop n) in memo := (n,v) :: !memo; v in loop x let _ = . .~(mfix (fibnr splus .. ..) 5)>. (* - : (int -> int -> int) code = .< fun x_5 -> fun y_6 -> let lv_7 = y_6 + x_5 in let lv_8 = lv_7 + y_6 in let lv_9 = lv_8 + lv_7 in let lv_10 = lv_9 + lv_8 in lv_10>. *) (* Another example: power *) let rec power : int -> int -> int = fun n x -> if n = 0 then 1 else x * power (n-1) x (* turning 'power' into a generator, which given x, produces the code computing power n x for some fixed n. specializing to n is easy: write the desired type signature and put the staging annotations so to eliminate all type errors. in the process described in MetaOCaml tutorial. *) let 128 = power 7 2 (* one can attempt the similar procedure when specializing to the given x *) let rec tpower : int code -> int -> int code = fun n x -> .. x)>. (* Alas, attempring to . (tpower .. 2)>. will diverge trying to build the infinite expression . if n = 0 then 1 else 2 * (if n-1 = 0 then 1 else 2 * ...)>. Indeed, nothing limits the recursion in tpower any more *) let tpower : int -> (int -> int) code = fun x -> genletrec (fun loop n -> ..) let _ = tpower 2;; (* More interesting: specializing Ackermann *) let rec ack m n = if m = 0 then n+1 else if n = 0 then ack (m-1) 1 else ack (m-1) (ack m (n-1)) ;; let 9 = ack 2 3;; (* A(2,y) = 2y+3 A(1,y)=y+2 A(3,y)=2^(n+3)-3 *) let tack self m n = if m = 0 then .<.~n+1>. else .. ;; (* val tack : (int -> (int -> int) code) -> int -> int code -> int code = *) (* Divereges! let _ = mfix (fun self m -> . .~(tack self m ..)>.) 2;; *) let mrfix : (('a -> ('b->'c) code) -> ('a -> 'b code ->'c code)) -> ('a -> ('b->'c) code) = fun f x -> let memo = ref ([],[]) in let rec loop n = match List.assoc n (fst !memo @ snd !memo) with | x -> x | exception Not_found -> let v = genletrec (fun g y -> let old = snd !memo in memo := (fst !memo, (n,g) :: old); let v = (f loop n y) in memo := (fst !memo, old); v) in memo := ((n,v) :: fst !memo, snd !memo); v in loop x let _ = mrfix (fun self m x -> tack self m x) 1;; (* - : (int -> int) code = .< let lv_5 = let rec g_3 x_4 = x_4 + 1 in g_3 in let lv_6 = let rec g_1 x_2 = if x_2 = 0 then lv_5 1 else lv_5 (g_1 (x_2 - 1)) in g_1 in lv_6>. *) let ack2 = mrfix (fun self m x -> tack self m x) 2;; (* val ack2 : (int -> int) code = .< let lv_13 = let rec g_11 x_12 = x_12 + 1 in g_11 in let lv_14 = let rec g_9 x_10 = if x_10 = 0 then lv_13 1 else lv_13 (g_9 (x_10 - 1)) in g_9 in let lv_15 = let rec g_7 x_8 = if x_8 = 0 then lv_14 1 else lv_14 (g_7 (x_8 - 1)) in g_7 in lv_15>. *) let 9 = Runcode.run ack2 3;; (* let%staged rec ack m = .< fun n -> .~(if m = 0 then .. else .< if n = 0 then .~(ack (m - 1)) 1 else .~(ack (m - 1)) (.~(ack m) (n - 1)) >.)>. in ack x *) (* Mutually-recursive definitions *) (* First, a complicated and contrived version of the even-odd example, made to look somewhat like the ack above: [even m n] tells the parity of [m + n] *) let rec even m n = if n>0 then odd m (n-1) else if m>0 then odd (m-1) n else true and odd m n = if n>0 then even m (n-1) else if m>0 then even (m-1) n else false ;; let true = even 10 42;; let true = odd 42 41;; (* Index *) type evod = Even | Odd let rec evodf self idx m n = match idx with | Even -> if n>0 then self Odd m (n-1) else if m>0 then self Odd (m-1) n else true | Odd -> if n>0 then self Even m (n-1) else if m>0 then self Even (m-1) n else false ;; let true = fix evodf Even 10 42;; let true = fix evodf Odd 42 41;; let rec sevodf self idx m n = match idx with | Even -> .0 then .~(self Odd m) (.~n-1) else .~(if m>0 then .<.~(self Odd (m-1)) .~n>. else ..)>. | Odd -> .0 then .~(self Even m) (.~n-1) else .~(if m>0 then .<.~(self Even (m-1)) .~n>. else ..)>. ;; let _ = mrfix (fun self (idx,m) x -> sevodf (fun idx m -> self (idx,m)) idx m x) (Even,0);; (* - : (int -> bool) code = .< let lv_6 = let rec g_1 = let lv_5 = let rec g_3 x_4 = if x_4 > 0 then g_1 (x_4 - 1) else false in g_3 in fun x_2 -> if x_2 > 0 then lv_5 (x_2 - 1) else true in g_1 in lv_6>. *) (* let _ = mrfix (fun self (idx,m) x -> sevodf (fun idx m -> self (idx,m)) idx m x) (Even,1);; Exception: Failure "Scope extrusion detected at Characters 254-277:\n for code built at File \"_none_\", line 1:\n for the identifier g_9 bound at Characters 102-103:\n ". *) (* The state automaton example from the paper *) type token = A | B let rec s = function A :: r -> s r | B :: r -> t r | [] -> true and t = function A :: r -> s r | B :: r -> u r | [] -> false and u = function A :: r -> t r | B :: r -> u r | [] -> false let true = s [A;A;A;B;B;B;A;A;A];; (* Open recursion style, index *) type state = S | T | U open Token let au self state stream = match state with | S -> . .~(self S) r | B :: r -> .~(self T) r | [] -> true>. | T -> . .~(self S) r | B :: r -> .~(self U) r | [] -> false>. | U -> . .~(self T) r | B :: r -> .~(self U) r | [] -> false>. ;; let _ = mrfix au S;; (* - : (Token.token list -> bool) code = .< let lv_15 = let rec g_1 = let lv_14 = let rec g_5 = let lv_13 = let rec g_9 x_10 = match x_10 with | (Token.A )::r_11 -> g_5 r_11 | (Token.B )::r_12 -> g_9 r_12 | [] -> false in g_9 in fun x_6 -> match x_6 with | (Token.A )::r_7 -> g_1 r_7 | (Token.B )::r_8 -> lv_13 r_8 | [] -> false in g_5 in fun x_2 -> match x_2 with | (Token.A )::r_3 -> g_1 r_3 | (Token.B )::r_4 -> lv_14 r_4 | [] -> true in g_1 in lv_15>. *) (* A better reprsentation *) type ('alph,'state) automaton = {finals : 'state list; trans : ('state * ('alph * 'state) list) list } let makeau {finals;trans} self state stream = let accept = List.mem state finals in let next token = List.assoc token (List.assoc state trans) in . .~(self (next A)) r | B :: r -> .~(self (next B)) r | [] -> accept>. ;; let au1 = {finals = [S]; trans = [ (S, [(A, S); (B, T)]); (T, [(A, S); (B, U)]); (U, [(A, T); (B, U)]); ] } ;; let auc = mrfix (makeau au1) S;; (* val auc : (Token.token list -> bool) code = .< let lv_15 = let rec g_1 = let lv_14 = let rec g_5 = let lv_13 = let rec g_9 x_10 = match x_10 with | (Token.A )::r_11 -> g_5 r_11 | (Token.B )::r_12 -> g_9 r_12 | [] -> false in g_9 in fun x_6 -> match x_6 with | (Token.A )::r_7 -> g_1 r_7 | (Token.B )::r_8 -> lv_13 r_8 | [] -> false in g_5 in fun x_2 -> match x_2 with | (Token.A )::r_3 -> g_1 r_3 | (Token.B )::r_4 -> lv_14 r_4 | [] -> true in g_1 in lv_15>. *) let true = Runcode.run auc [A;A;A;B;B;B;A;A;A];; (* An example with more complex recursion, for which the simple genletrec/mrfix fails *) type state2 = S1 | S2 | S3 | S4 let au3 = {finals = [S1; S2; S3; S4]; trans = [S1, [A, S2; B, S3]; S2, [A, S3; B, S4]; S3, [A, S4; B, S1]; S4, [A, S1; B, S2]; ] } ;; (* Scope extrusion! *) let auc3 = mrfix (makeau au3) S1;;