module M = import "data/map.ml"
module S = import "data/set.ml"
module Str = import "data/set.ml"

open import "prelude.ml"
open import "./lang.ml"
open import "./lib/monads.ml"

type addr =
  | Combinator of string
  | Local of int
  | Arg of int
  | Int of int

type gm_code =
  | Push of addr
  | Update of int
  | Pop of int
  | Slide of int
  | Alloc of int
  | Unwind
  | Mkap
  | Add | Sub | Mul | Div | Eval
  | Iszero of list gm_code * list gm_code
  | Pack of int * int
  | Casejump of list (int * list gm_code)

instance show gm_code begin
  let show = function
    | Mkap -> "Mkap"
    | Unwind -> "Unwind"
    | Push (Combinator k) -> "Push " ^ k
    | Push (Arg i) -> "Pusharg " ^ show i
    | Push (Local i) -> "Pushlocal " ^ show i
    | Push (Int i) -> "Pushint " ^ show i
    | Update n -> "Update " ^ show n
    | Pop n   -> "Pop " ^ show n
    | Slide n -> "Slide " ^ show n
    | Alloc n -> "Alloc " ^ show n
    | Add  -> "Add"
    | Mul  -> "Mul"
    | Sub  -> "Sub"
    | Div  -> "Div"
    | Eval -> "Eval"
    | Pack (arity, tag) -> "Pack{" ^ show arity ^ "," ^ show tag ^ "}"
    | Casejump xs -> "Casejump " ^ show xs
    | Iszero xs -> "Iszero " ^ show xs
end

type program_item =
  | Sc of string * int * list gm_code
  | Fd of fdecl

instance show program_item begin
  let show = function
    | Sc p -> show p
    | Fd _ -> "<foreign item>"
end

let rec lambda_lift strict = function
  | Ref v -> pure (Ref v)
  | Lit v -> pure (Lit v)
  | App (f, x) -> (| app (lambda_lift false f) (lambda_lift false x) |)
  | Lam (v, x) ->
    let! body = lambda_lift true x
    let! (i, defs, known_sc) = get

    let vars =
      x |> free_vars
        |> S.delete v
        |> flip S.difference known_sc
        |> S.members

    let def = ("Lam" ^ show i, vars ++ [v], body)
    let app = foldl (fun f -> app f # Ref) (Ref ("Lam" ^ show i)) vars

    put (i + 1, Decl def :: defs, known_sc)
      |> map (const app)
  | Case (sc, alts) ->
    let! sc = lambda_lift true sc
    let! alts = traverse (fun (c, args, e) -> (c,args,) <$> lambda_lift true e) alts
    let case = Case (sc, alts)
    if strict then
      pure case
    else
      let! (i, defs, known_sc) = get
      let vars =
        case
          |> free_vars
          |> flip S.difference known_sc
          |> S.members
      let def = ("Case" ^ show i, vars, case)
      let app = foldl (fun f -> app f # Ref) (Ref ("Case" ^ show i)) vars
      put (i + 1, Decl def :: defs, known_sc)
        |> map (const app)
  | Let (vs, e) ->
    let! vs = flip traverse vs @@ fun (v, e) ->
      (v,) <$> lambda_lift false e
    let! e = lambda_lift true e
    pure (Let (vs, e))
  | If _ -> error "if expression in lambda-lifting"

let rec eta_contract = function
  | Decl (n, a, e) as dec ->
    match a, e with
    | [], _ -> dec
    | xs, App (f, Ref v) ->
      if v == last xs && not (S.member v (free_vars f)) then
        eta_contract (Decl (n, init a, f))
      else
        dec
    | _, _ -> dec
  | Data c -> Data c
  | Foreign i -> Foreign i

let rec lambda_lift_sc = function
  | Decl (n, a, e) ->
    match e with
    | Lam (v, e) -> lambda_lift_sc (Decl (n, a ++ [v], e))
    | _ ->
      let! e = lambda_lift true e
      let! _ = modify (fun (a, b, s) -> (a, b, S.insert n s))
      pure (Decl (n, a, e))
  | Data c -> Data c |> pure
  | Foreign (Fimport { var } as i) ->
      let! _ = modify (second (second (S.insert var)))
      Foreign i |> pure

type dlist 'a <- list 'a -> list 'a

let cg_prim (Fimport { var, fent }) =
  let prim_math_op x =
    [ Push (Arg 0), Eval, Push (Arg 2), Eval, x, Update 2, Pop 2, Unwind ]
  let prim_equality =
    [ Push (Arg 0), Eval (* x, arg0, arg1, arg2, arg3 *)
    , Push (Arg 2), Eval (* y, x, arg0, arg1, arg2, arg3 *)
    , Sub                (* y - x, arg0, arg1, arg2, arg3 *)
    , Iszero ([ Pack (0, 0) ], [ Pack (0, 1) ])
    , Update 2, Pop 2, Unwind ]
  match fent with
  | "add" -> (Sc (var, 2, prim_math_op Add), Add)
  | "sub" -> (Sc (var, 2, prim_math_op Sub), Sub)
  | "mul" -> (Sc (var, 2, prim_math_op Mul), Mul)
  | "div" -> (Sc (var, 2, prim_math_op Div), Div)
  | "equ" -> (Sc (var, 2, prim_equality), Unwind)
  | "seq" -> (Sc (var, 2, [ Push (Arg 0), Eval, Update 0, Push (Arg 2), Update 2, Pop 2, Unwind]), Eval)
  | e -> error @@ "No such primitive " ^ e

type slot = As of int | Ls of int

let offs n = function
  | As x -> As (x + n)
  | Ls x -> Ls (x + n)

let incr = offs 1

let private prim_scs : ref (M.t string gm_code) = ref M.empty

let private is_arith_op = function
  | Add | Sub | Mul | Div | Iszero _ -> true
  | _ -> false

let rec compile_lazy (env : M.t string slot) = function
  | Ref v ->
    match M.lookup v env with
    | Some (As i) -> (Push (Arg i) ::)
    | Some (Ls i) -> (Push (Local i) ::)
    | None -> (Push (Combinator v) ::)

  | App (f, x) ->
    let f = compile_lazy env f
    let x = compile_lazy (map incr env) x
    f # x # (Mkap ::)
  | Lam _ ->
      error "Can not compile lambda expression, did you forget to lift?"
  | If _ ->
      error "Can not compile if expression, did you forget to TC?"
  | Case _ ->
      error "Case expression in lazy context"
  | Lit i -> (Push (Int i) ::)
  | Let (vs, e) ->
      compile_let compile_lazy env vs e

and compile_strict (env : M.t string slot) = function
  | Case (sc, alts) ->
    let rec go_alts = function
      | [] -> []
      | Cons ((_, args, exp), rest) ->
        let c_arity = length args
        let env =
          args
            |> flip zip [Ls k | with k <- [c_arity - 1, c_arity - 2 .. 0]]
            |> M.from_list
            |> M.union (offs (c_arity + 1) <$> env)
        (c_arity, compile_strict env exp [Slide (c_arity + 1)]) :: go_alts rest
    compile_strict env sc # (Casejump (go_alts alts) ::)
  | App (App (Ref f, x), y) as e ->
      match M.lookup f !prim_scs with
      | Some op when is_arith_op op ->
          compile_strict env x
            # compile_strict (incr <$> env) y
            # (op ::)
      | _ -> compile_lazy env e # (Eval ::)
  | e -> compile_lazy env e # (Eval ::)

and compile_tail (env : M.t string slot) = function
  | Ref v ->
    match M.lookup v env with
    | Some (As i) -> (Push (Arg i) ::)
    | Some (Ls i) -> (Push (Local i) ::)
    | None -> (Push (Combinator v) ::)
  | App (f, x) ->
    let f = compile_tail env f
    let x = compile_lazy (map incr env) x
    f # x # (Mkap ::)
  | e -> compile_strict env e

and compile_let cont env vs e =
  let n = length vs
  let env =
    vs
      |> map (fun (x, _) -> x)
      |> flip zip [Ls x | with x <- [n - 1, n - 2 .. 0]]
      |> M.from_list
      |> M.union (offs n <$> env)
  let defs = zip [1..n] vs
  let rec go : list (int * string * expr) -> dlist gm_code = function
    | [] -> id
    | Cons ((k, (_, exp)), rest) ->
        compile_lazy env exp # (Update (n - k) ::) # go rest
  (Alloc n ::) # go defs # cont env e # (Slide n ::)

let supercomb (_, args, exp) =
  let env = M.from_list (zip args [0..length args])
  let k = compile_tail (M.from_list (zip args (As <$> [0..length args]))) exp
  k [Update (length env), Pop (length env), Unwind]

let compile_cons =
  let rec go i = function
    | [] -> []
    | Cons (Constr (n, args), rest) ->
      let arity = length args
      let rec pushargs i =
        if i < arity then
          Push (Arg (2 * i)) :: pushargs (i + 1)
        else
          []
      Sc (n, arity, pushargs 0 ++ [ Pack (arity, i), Update (2 * arity), Pop (2 * arity), Unwind ])
        :: go (i + 1) rest
  go 0

let program decs =
  let rec globals s = function
    | [] -> s
    | Cons (Decl (n, _, _), r) -> globals (S.insert n s) r
    | Cons (Data (_, _, c), r) ->
        globals (foldl (fun s (Constr (n, _)) -> S.insert n s) s c) r
    | Cons (Foreign (Fimport {var=n}), r) ->
        globals (S.insert n s) r

  let (decs, (_, lams, _)) =
    run_state (traverse (map eta_contract # lambda_lift_sc) decs)
      (0, [], globals S.empty decs)

  let define nm k =
    let! x = get
    if nm `S.member` x then
      pure []
    else
      let! _ = modify (S.insert nm)
      k

  let go =
    flip traverse (lams ++ decs) @@ function
      | Decl ((nm, args, _) as sc) ->
        define nm (
          let code = supercomb sc
          [Sc (nm, length args, code)] |> pure
        )
      | Data (_, _, cs) -> pure (compile_cons cs)
      | Foreign (Fimport { cc = Prim, var } as fi) ->
        define var (
          let (code, h) = cg_prim fi
          prim_scs := M.insert var h !prim_scs
          pure [code]
        )
      | Foreign f -> pure [Fd f]
  let (out, _) = run_state go S.empty
  join out