SLL Arithmetic

sll.ml

type ident = string
type pattern = { pname : ident; pargs : ident list; }
type expr =
  | Var of ident
  | Ctr of ident * expr list
  | FCall of ident * expr list
  | GCall of ident * expr list

type gdef = {
  gname : ident;
  pattern : pattern;
  gargs : ident list;
  gbody : expr;
}
type fdef = { fname : ident; fargs : ident list; fbody : expr; }

type ftable = (ident, fdef) Hashtbl.t
type gtable = (ident * ident, gdef) Hashtbl.t

type program = { ftable : ftable; gtable : gtable; term : expr; }
type env = (ident * expr) list

exception Interpret_error of string

let rec ( // ) expr env =
  let ( //* ) exprs env = List.map (fun e -> e // env) exprs in
  match expr with
  | Var vname -> begin try
        List.assoc vname env
      with Not_found -> raise (Interpret_error ("Unbound variable " ^ vname))
    end
  | Ctr (name, args) -> Ctr (name, args //* env)
  | FCall (name, args) -> FCall (name, args //* env)
  | GCall (name, args) -> GCall (name, args //* env)

let string_of_app name args = name ^ "(" ^ String.concat ", " args ^ ")"

let rec string_of_expr = function
  | Var vname -> vname
  | Ctr (name, args) | FCall (name, args) | GCall (name, args) ->
      string_of_app name (List.map string_of_expr args)

let make_program fdefs gdefs term =
  let (ftable : ftable) = Hashtbl.create (Array.length fdefs) in
  let (gtable : gtable) = Hashtbl.create (Array.length gdefs) in
  Array.iter (fun ({ fname; _ } as fdef) ->
    Hashtbl.replace ftable fname fdef) fdefs;
  Array.iter (fun ({ gname; pattern = { pname; _ }; _ } as gdef) ->
    Hashtbl.replace gtable (gname, pname) gdef) gdefs;
  { ftable; gtable; term; }

let string_of_fdef { fname; fargs; fbody; } =
  string_of_app fname fargs ^ " = " ^ string_of_expr fbody

let string_of_pattern { pname; pargs; } = string_of_app pname pargs

let string_of_gdef { gname; pattern; gargs; gbody; } =
  string_of_app gname (string_of_pattern pattern :: gargs) ^
    " = " ^ string_of_expr gbody

let string_of_program { ftable; gtable; term; } =
  let buffer = Buffer.create 16 in
  let add_defs printer table =
    Hashtbl.iter (fun _ def ->
      Buffer.add_string buffer (printer def ^ "\n")) table
  in
  add_defs string_of_fdef ftable;
  add_defs string_of_gdef gtable;
  Buffer.add_string buffer (string_of_expr term);
  Buffer.contents buffer

let rec make_nat = function
  | 0 -> Ctr ("Z", [])
  | n -> Ctr ("S", [make_nat (n - 1)])

let rec from_nat = function
  | Ctr ("Z", [])  -> 0
  | Ctr ("S", [x]) -> 1 + from_nat x
  | x -> raise (Interpret_error ("(from_nat) bad nat: " ^ string_of_expr x))

let make_int z =
  if z < 0
  then Ctr ("N", [make_nat (-z)])
  else (make_nat z)

let from_int = function
  | Ctr ("N", [x]) -> -(from_nat x)
  | x -> from_nat x

let run { ftable; gtable; term; } =
  let rec intr = function
    | Var name -> raise (Interpret_error ("Undefined variable " ^ name))
    | Ctr (cname, cargs) -> Ctr (cname, List.map intr cargs)
    | FCall (fname, act_args) ->
        let { fname; fargs; fbody; } = begin try
            Hashtbl.find ftable fname
          with Not_found ->
            raise (Interpret_error ("f-definition not found: " ^ fname))
          end
        in
        intr (fbody // List.combine fargs act_args)
    | GCall (gname, pat :: act_args) ->
        begin match intr pat with
        | Ctr (cname, cargs) ->
            let { gname; pattern = { pname; pargs }; gargs; gbody; } = begin try
                Hashtbl.find gtable (gname, cname)
              with Not_found ->
                raise (Interpret_error ("g-definition not found: " ^
                                        gname ^ "(" ^ cname ^ "(...)...)"))
              end
            in
            let env = List.combine pargs cargs @ List.combine gargs act_args in
            intr (gbody // env)
        | _ -> raise (Interpret_error ("FATAL: this code must be unreachable!"))
        end
    | _ -> raise (Interpret_error ("GCall with zero-length argument list"))
  in
  intr term

let ( +> ) pname pargs = { pname; pargs; }
let ( $  ) gname (pattern, gargs) = (gname, pattern, gargs)
let ( => ) (gname, pattern, gargs) gbody = { gname; pattern; gargs; gbody; }

let ( >$ ) fname fargs = (fname, fargs)
let ( >= ) (fname, fargs) fbody = { fname; fargs; fbody; }

let () =
  let gdefs = [|
    (* Subtraction for Non-Negative integers *)
    "snn"  $ ("Z" +> [],    ["y"]) => GCall ("neg", [Var "y"]);
    "snn"  $ ("S" +> ["x"], ["y"]) => GCall ("sud", [Var "y"; Var "x"]);

    (* Subtract from already Decremented second argument Unexplored first one *)
    "sud"  $ ("Z" +> [],    ["x"]) => Ctr ("S", [Var "x"]);
    "sud"  $ ("S" +> ["y"], ["x"]) => GCall ("snn", [Var "x"; Var "y"]);

    (* Negate integer *)
    "neg"  $ ("Z" +> [],    []) => Ctr ("Z", []);
    "neg"  $ ("S" +> ["x"], []) => Ctr ("N", [Ctr ("S", [Var "x"])]);
    "neg"  $ ("N" +> ["x"], []) => Var "x";

    (* Addition *)
    "add"  $ ("Z" +> [],    ["y"]) => Var "y";
    "add"  $ ("S" +> ["x"], ["y"]) =>
      GCall ("aup", [Var "y"; Ctr ("S", [Var "x"])]);
    "add"  $ ("N" +> ["x"], ["y"]) => GCall ("sup", [Var "y"; Var "x"]);

    (* Add Unexplored integer and Positive one *)
    "aup"  $ ("Z" +> [],    ["y"]) => Var "y";
    "aup"  $ ("S" +> ["x"], ["y"]) =>
      Ctr ("S", [GCall ("aup", [Var "x"; Var "y"])]);
    "aup"  $ ("N" +> ["x"], ["y"]) => GCall ("snn", [Var "y"; Var "x"]);

    (* Subtract from Unexplored integer Positive one *)
    "sup"  $ ("Z" +> [],    ["y"]) => Ctr ("N", [Var "y"]);
    "sup"  $ ("S" +> ["x"], ["y"]) => GCall ("sud", [Var "y"; Var "x"]);
    "sup"  $ ("N" +> ["x"], ["y"]) =>
      Ctr ("N", [GCall ("aup", [Var "y"; Var "x"])]);

    (* Multiplication *)
    "mul"  $ ("Z" +> [],    ["y"]) => Ctr ("Z", []);
    "mul"  $ ("S" +> ["x"], ["y"]) =>
      GCall ("add", [Var "y"; GCall ("mul", [Var "x"; Var "y"])]);
    "mul"  $ ("N" +> ["x"], ["y"]) =>
      GCall ("neg", [GCall ("mul", [Var "x"; Var "y"])]);

    (* Is Negative predicate *)
    "isn"  $ ("Z" +> [],    []) => Ctr ("F", []);
    "isn"  $ ("S" +> ["x"], []) => Ctr ("F", []);
    "isn"  $ ("N" +> ["x"], []) => Ctr ("T", []);

    (* Absolute value *)
    "abs"  $ ("Z" +> [],    []) => Ctr ("Z", []);
    "abs"  $ ("S" +> ["x"], []) => Ctr ("S", [Var "x"]);
    "abs"  $ ("N" +> ["x"], []) => Var "x";

    (* Signum function *)
    "sgn"  $ ("Z" +> [],    []) => Ctr ("Z", []);
    "sgn"  $ ("S" +> ["x"], []) => Ctr ("S", [Ctr ("Z", [])]);
    "sgn"  $ ("N" +> ["x"], []) => Ctr ("N", [Ctr ("S", [Ctr ("Z", [])])]);

    (* Condition / if-then-else *)
    "cnd"  $ ("T" +> [], ["t"; "f"]) => Var "t";
    "cnd"  $ ("F" +> [], ["t"; "f"]) => Var "f";
  |] in
  let fdefs = [|
    (* Subtraction *)
    "sub" >$ ["x"; "y"] >= GCall ("add", [Var "x"; GCall ("neg", [Var "y"])]);

    (* Less then predicate *)
    "lss" >$ ["x"; "y"] >= GCall ("isn", [FCall ("sub", [Var "x"; Var "y"])]);

    (* Division for Non-Negative integers *)
    "dnn" >$ ["x"; "y"] >= GCall ("cnd", [
      FCall ("lss", [Var "x"; Var "y"]);
      Ctr ("Z", []);
      Ctr ("S", [FCall ("dnn", [
        FCall ("sub", [Var "x"; Var "y"]);
        Var "y"])])]);

    (* Division *)
    "div" >$ ["x"; "y"] >= GCall ("mul", [
      GCall ("mul", [GCall ("sgn", [Var "x"]); GCall ("sgn", [Var "y"])]);
      FCall ("dnn", [GCall ("abs", [Var "x"]); GCall ("abs", [Var "y"])])]);

    (* signed Modulo *)
    "mod" >$ ["x"; "y"] >= FCall ("sub", [ Var "x";
      GCall ("mul", [FCall ("div", [Var "x"; Var "y"]); Var "y"])]);
  |] in
  let program = make_program fdefs gdefs (Ctr ("Z", [])) in
  print_endline (string_of_program program);
  let tester make_call func control x y =
    let term = make_call func x y in
    let program = { program with term } in
    if run program = make_int (control x y)
    then print_string      " ok"
    else print_endline "\n [FAIL]"
  in
  let test = tester (fun func x y -> GCall (func, [make_int x; make_int y])) in
  test  "snn" ( - )   8    5 ;
  test  "snn" ( - )   5    8 ;
  test  "snn" ( - )   8    0 ;
  test  "snn" ( - )   0    8 ;
  test  "snn" ( - )   0    0 ;
  test  "add" ( + )   0    0 ;
  test  "add" ( + )   0    8 ;
  test  "add" ( + )   0  (-8);
  test  "add" ( + )   5    0 ;
  test  "add" ( + )   5    8 ;
  test  "add" ( + )   5  (-8);
  test  "add" ( + )   8  (-5);
  test  "add" ( + ) (-7)   0 ;
  test  "add" ( + ) (-7)   5 ;
  test  "add" ( + ) (-7)   7 ;
  test  "add" ( + ) (-7)   9 ;
  test  "add" ( + ) (-7) (-5);
  test  "mul" ( * )   0    0 ;
  test  "mul" ( * )   5    0 ;
  test  "mul" ( * )   0    5 ;
  test  "mul" ( * )   5    8 ;
  test  "mul" ( * )   5  (-8);
  test  "mul" ( * ) (-8)   5 ;
  test  "mul" ( * ) (-8) (-5);
  let testf = tester (fun func x y -> FCall (func, [make_int x; make_int y])) in
  testf "sub" ( - )   5  (-8);
  testf "sub" ( - ) (-8)   5 ;
  testf "sub" ( - ) (-8) (-5);
  testf "dnn" ( / )   0    5 ;
  testf "dnn" ( / )   3    5 ;
  testf "dnn" ( / )  40    8 ;
  testf "dnn" ( / )  41    8 ;
  testf "dnn" ( / )  39    8 ;
  testf "div" ( / )   0    5 ;
  testf "div" ( / )   3    5 ;
  testf "div" ( / )  40    8 ;
  testf "div" ( / )  41    8 ;
  testf "div" ( / )  39    8 ;
  testf "div" ( / )   3  (-8);
  testf "div" ( / ) (-8)   3 ;
  testf "div" ( / ) (-8) (-3);
  testf "mod" (mod)   0    5 ;
  testf "mod" (mod)   3    5 ;
  testf "mod" (mod)  40    8 ;
  testf "mod" (mod)  41    8 ;
  testf "mod" (mod)  39    8 ;
  testf "mod" (mod)   3  (-8);
  testf "mod" (mod) (-8)   3 ;
  testf "mod" (mod) (-8) (-3);
  print_endline "";

  print_string "x = ";
  let x = make_int (read_int ()) in
  print_string "y = ";
  let y = make_int (read_int ()) in
  let ratio  = run { program with term = FCall ("div", [x; y]) } in
  let modulo = run { program with term = FCall ("mod", [x; y]) } in
  print_endline ("x / y = " ^ string_of_int (from_int ratio));
  print_endline ("x % y = " ^ string_of_int (from_int modulo));

sll.mli

type ident = string
type pattern = { pname : ident; pargs : ident list; }
type expr =
  | Var of ident
  | Ctr of ident * expr list
  | FCall of ident * expr list
  | GCall of ident * expr list

type gdef = {
  gname : ident;
  pattern : pattern;
  gargs : ident list;
  gbody : expr;
}
type fdef = { fname : ident; fargs : ident list; fbody : expr; }

type ftable = (ident, fdef) Hashtbl.t
type gtable = (ident * ident, gdef) Hashtbl.t

type program = { ftable : ftable; gtable : gtable; term : expr; }

exception Interpret_error of string

val string_of_expr : expr -> string
val string_of_program : program -> string
val run : program -> expr

$ ocamlopt sll.ml -o ints
$ ./ints 
mod(x, y) = sub(x, mul(div(x, y), y))
dnn(x, y) = cnd(lss(x, y), Z(), S(dnn(sub(x, y), y)))
lss(x, y) = isn(sub(x, y))
sub(x, y) = add(x, neg(y))
div(x, y) = mul(mul(sgn(x), sgn(y)), dnn(abs(x), abs(y)))
neg(Z()) = Z()
sud(S(y), x) = snn(x, y)
mul(Z(), y) = Z()
sup(Z(), y) = N(y)
sup(N(x), y) = N(aup(y, x))
abs(Z()) = Z()
aup(N(x), y) = snn(y, x)
sud(Z(), x) = S(x)
abs(N(x)) = x
add(S(x), y) = aup(y, S(x))
sgn(S(x)) = S(Z())
cnd(T(), t, f) = t
mul(S(x), y) = add(y, mul(x, y))
neg(N(x)) = x
isn(N(x)) = T()
isn(Z()) = F()
sup(S(x), y) = sud(y, x)
sgn(N(x)) = N(S(Z()))
add(Z(), y) = y
abs(S(x)) = S(x)
aup(Z(), y) = y
snn(Z(), y) = neg(y)
cnd(F(), t, f) = f
snn(S(x), y) = sud(y, x)
aup(S(x), y) = S(aup(x, y))
sgn(Z()) = Z()
mul(N(x), y) = neg(mul(x, y))
isn(S(x)) = F()
add(N(x), y) = sup(y, x)
neg(S(x)) = N(S(x))
Z()
 ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok ok
x = 415
y = 47
x / y = 8
x % y = 39
$