a4

(* ****** ****** *)
//
// Title:
// Principles of
// Programming Languages
// Course: CAS CS 520
//
// Semester: Spring, 2018
//
// Classroom: MCS B25
// Class Time: TR 2:00-3:15
//
// Instructor: Hongwei Xi (hwxiATcsDOTbuDOTedu)
//
(* ****** ****** *)
//
// Due date: Tuesday, the 20th of February
//
(* ****** ****** *)

#include
"share/atspre_staload.hats"
#include
"share/atspre_staload_libats_ML.hats"

(* ****** ****** *)

datatype term =
//
  | TMint of (int)
  | TMstr of string
//
  | TMtup of termlst
  | TMproj of (term, int)
//
  | TMvar of string
//
  | TMlam of (string, term(*body*))
  | TMapp of (term(*fun*), term(*arg*))
  | TMfix of (string(*f*), string(*x*), term)
//
  | TMopr of (string(*opr*), termlst)
  | TMifnz of (term(*test*), term(*then*), term(*else*))

where termlst = list0(term)

(* ****** ****** *)

datatype value =
  | VALint of int
  | VALstr of string
  | VALtup of valuelst
  | VALfix of (term, envir)
  | VALlam of (term, envir)

where

envir =
list0($tup(string, value))

and valuelst = list0(value)


(* ****** ****** *)

extern
fun
print_value(t0: value): void
extern
fun
fprint_value(out: FILEref, t0: value): void

overload print with print_value
overload fprint with fprint_value

(* ****** ****** *)

implement
fprint_val<value> = fprint_value

(* ****** ****** *)

implement
print_value
(t0) = fprint_value(stdout_ref, t0)

implement
fprint_value(out, t0) =
(
case+ t0 of
//
| VALint(i) => fprint!(out, "VALint(", i, ")")
| VALstr(s) => fprint!(out, "VALstr(", s, ")")
//
| VALtup(vs) => fprint!(out, "VALtup(", vs, ")")
//
| VALlam(_, _) => fprint!(out, "VALlam(_, _)")
| VALfix(_, _) => fprint!(out, "VALfix(_, _)")
//
)

(* ****** ****** *)
//
// HX-2018-02-08:
// please implement the
// following one on your own:
//
extern
fun interp1(t0: term): value
//

extern
fun
interp2 : (term, envir) -> value

overload interp with interp1
overload interp with interp2

(* ****** ****** *)

implement
interp1(src) =
interp2(src, list0_nil())

(* ****** ****** *)

extern
fun
envir_find :
(envir, string) -> value
implement
envir_find(env, x0) =
(
case- env of
| list0_cons(xv, env) =>
  if x0 = xv.0
    then xv.1 else envir_find(env, x0)
  // end of [if]
)

fun
interp2_list
(ts: termlst, env: envir): valuelst =
list0_map<term><value>(ts, lam(t) => interp2(t, env))

implement
interp2(t0, env) =
(
case t0 of
//
| TMint(i) => VALint(i)
| TMstr(s) => VALstr(s)
//
| TMvar(x) => envir_find(env, x)
//
| TMlam _ => VALlam(t0, env)
| TMfix _ => VALfix(t0, env)
//
| TMtup(ts) =>
  VALtup(interp2_list(ts, env))
//
| TMproj
    (t_tup, i) => let
    val v_tup = interp2(t_tup, env)
  in
    case- v_tup of
    | VALtup(vs) => vs[i] // = list0_get_at_exn(vs, i)
  end
//
| TMapp(t1, t2) => let
    val v1 = interp2(t1, env)
  in
    case- v1 of
    | VALlam
      (t_lam, env_lam) => let
        val v2 = interp2(t2, env)
        val-TMlam(x, t_body) = t_lam
        val env_lam = list0_cons($tup(x, v2), env_lam)
      in
        interp2(t_body, env_lam)
      end
    | VALfix
      (t_fix, env_fix) => let
        val v2 = interp2(t2, env)
        val-TMfix(f, x, t_body) = t_fix
        val env_fix = list0_cons($tup(x, v2), env_fix)
        val env_fix = list0_cons($tup(f, v1), env_fix)
      in
        interp2(t_body, env_fix)
      end
  end // end of [TMapp]
//
| TMopr _ => interp2_opr(t0, env)
//
| TMifnz
    (t1, t2, t3) => let
    val v1 = interp2(t1, env)
  in
    case- v1 of
    | VALint(i) =>
      interp2(if i != 0 then t2 else t3, env)
  end
) where
{
//
fun
interp2_opr
( t0: term
, env: envir): value = let
//
#define :: list0_cons
#define nil list0_nil
//
val-TMopr(opr, ts) = t0
//
val vs =
list0_map<term><value>(ts, lam(t) => interp2(t, env))
//
in
case- opr of
| "+" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => VALint(i1+i2)
  )
| "-" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => VALint(i1-i2)
  )
| "*" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => VALint(i1*i2)
  )
| "/" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => VALint(i1/i2)
  )
| "~" =>
  (
    case- vs of VALint(i1)::nil() => VALint(~i1)
  )
| "abs" =>
  (
    case- vs of VALint(i1)::nil() => VALint(abs(i1))
  )
| ">=" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => if i1 >= i2 then VALint(1) else VALint(0)
  )
| "<=" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => if i1 <= i2 then VALint(1) else VALint(0)
  )
| ">" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => if i1 > i2 then VALint(1) else VALint(0)
  )
| "<" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => if i1 < i2 then VALint(1) else VALint(0)
  )
| "print" =>
  (
    case- vs of
    | VALstr(s1)::nil() =>
    let
    val ()=print(s1)
    in
    VALstr(s1)
    end
    | VALint(i1)::nil() =>
    let
    val ()=print(i1)
    in
    VALint(i1)
    end
  )
| "==" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => if i1 = i2 then VALint(1) else VALint(0)
  )
| "!=" =>
  (
    case- vs of
    | VALint(i1)::VALint(i2)::nil() => if i1 != i2 then VALint(1) else VALint(0)
  )
end // end of [interp2_opr]

} (* end of [interp2] *)

(* ****** ****** *)
//
val x = TMvar("x")
val f = TMvar("f")
//
(* ****** ****** *)

fun
sub_term_int
(t1: term, i2: int): term =
TMopr
( "-"
, list0_tuple(t1, TMint(i2)))

fun
sub_int_term
(i1: int, t2: term): term =
TMopr
( "-"
, list0_tuple(TMint(i1), t2))

fun
add_term_term
(t1: term, t2: term): term =
TMopr("+", list0_tuple(t1, t2))

fun
add_term_int
(t1: term, i2: int): term =
TMopr("+", list0_tuple(t1, TMint(i2)))

fun
mul_term_term
(t1: term, t2: term): term =
TMopr("*", list0_tuple(t1, t2))

fun
equal_term_int
(t1: term, i2: int): term =
TMopr("==", list0_tuple(t1, TMint(i2)))

overload - with sub_term_int
overload + with add_term_term
overload * with mul_term_term

#define N 8

fun bd(t0: term, t1: term, t2: term, t3: term, t4: term, t5: term, t6: term, t7: term): term =
TMtup(cons0(t0, cons0(t1, cons0(t2,cons0(t3,cons0(t4,cons0(t5,cons0(t6,cons0(t7,nil0())))))))))
fun pair(t0: term, t1: term): term = TMtup(cons0(t0, cons0(t1, nil0())))

fun fst(t0: term): term = TMproj(t0, 0)
fun snd(t0: term): term = TMproj(t0, 1)
fun trd(t0: term): term = TMproj(t0, 2)
fun fur(t0: term): term = TMproj(t0, 3)
fun fiv(t0: term): term = TMproj(t0, 4)
fun six(t0: term): term = TMproj(t0, 5)
fun sev(t0: term): term = TMproj(t0, 6)
fun eig(t0: term): term = TMproj(t0, 7)

val i = TMvar("i")
val f = TMvar("f")
val board=TMvar("board")

val print_dots = TMfix("f","i",TMifnz(TMopr(">",list0_tuple(i,TMint(0))),pair(TMopr("print",list0_tuple(TMstr(". "))),TMapp(f,i-1)),TMstr("")))

val print_row =
TMlam("i",TMtup(cons0(TMapp(print_dots,i),cons0(TMopr("print",list0_tuple(TMstr("Q "))),cons0(TMapp(print_dots,sub_int_term(N,i)-1),
cons0(TMopr("print",list0_tuple(TMstr("\n"))),nil0()))))))

val print_board=TMlam
(
  "board",
  TMtup(cons0(TMapp(print_row,fst(board)),
  cons0(TMapp(print_row,snd(board)),
  cons0(TMapp(print_row,trd(board)),
  cons0(TMapp(print_row,fur(board)),
  cons0(TMapp(print_row,fiv(board)),
  cons0(TMapp(print_row,six(board)),
  cons0(TMapp(print_row,sev(board)),
  cons0(TMapp(print_row,eig(board)),
  cons0(TMopr("print",list0_tuple(TMstr("\n"))),
  nil0()))))))))))
)

val bd_i=TMvar("bd_i")

val board_get=TMlam
(
  "bd_i",
  TMifnz
  (
    equal_term_int(snd(bd_i),0),
    fst(fst(bd_i)),
    TMifnz
    (
      equal_term_int(snd(bd_i),1),
      snd(fst(bd_i)),
      TMifnz
      (
        equal_term_int(snd(bd_i),2),
        trd(fst(bd_i)),
        TMifnz
        (
          equal_term_int(snd(bd_i),3),
          fur(fst(bd_i)),
          TMifnz
          (
            equal_term_int(snd(bd_i),4),
            fiv(fst(bd_i)),
            TMifnz
            (
              equal_term_int(snd(bd_i),5),
              six(fst(bd_i)),
              TMifnz
              (
                equal_term_int(snd(bd_i),6),
                sev(fst(bd_i)),
                TMifnz
                (
                  equal_term_int(snd(bd_i),7),
                  eig(fst(bd_i)),
                  TMint(~1)
                )
              )
            )
          )
        )
      )
    )
  )
)

val bd_i_j=TMvar("bd_i_j")

val board_set=TMlam
(
  "bd_i_j",
  TMifnz
  (
    equal_term_int(snd(bd_i_j),0),
    TMtup(cons0(trd(bd_i_j), cons0(snd(fst(bd_i_j)), cons0(trd(fst(bd_i_j)),cons0(fur(fst(bd_i_j)),cons0(fiv(fst(bd_i_j)),cons0(six(fst(bd_i_j)),cons0(sev(fst(bd_i_j)),cons0(eig(fst(bd_i_j)),nil0()))))))))),
    TMifnz
    (
      equal_term_int(snd(bd_i_j),1),
      TMtup(cons0(fst(fst(bd_i_j)), cons0(trd(bd_i_j), cons0(trd(fst(bd_i_j)),cons0(fur(fst(bd_i_j)),cons0(fiv(fst(bd_i_j)),cons0(six(fst(bd_i_j)),cons0(sev(fst(bd_i_j)),cons0(eig(fst(bd_i_j)),nil0()))))))))),
      TMifnz
      (
        equal_term_int(snd(bd_i_j),2),
        TMtup(cons0(fst(fst(bd_i_j)), cons0(snd(fst(bd_i_j)), cons0(trd(bd_i_j),cons0(fur(fst(bd_i_j)),cons0(fiv(fst(bd_i_j)),cons0(six(fst(bd_i_j)),cons0(sev(fst(bd_i_j)),cons0(eig(fst(bd_i_j)),nil0()))))))))),
        TMifnz
        (
          equal_term_int(snd(bd_i_j),3),
          TMtup(cons0(fst(fst(bd_i_j)), cons0(snd(fst(bd_i_j)), cons0(trd(fst(bd_i_j)),cons0(trd(bd_i_j),cons0(fiv(fst(bd_i_j)),cons0(six(fst(bd_i_j)),cons0(sev(fst(bd_i_j)),cons0(eig(fst(bd_i_j)),nil0()))))))))),
          TMifnz
          (
            equal_term_int(snd(bd_i_j),4),
            TMtup(cons0(fst(fst(bd_i_j)), cons0(snd(fst(bd_i_j)), cons0(trd(fst(bd_i_j)),cons0(fur(fst(bd_i_j)),cons0(trd(bd_i_j),cons0(six(fst(bd_i_j)),cons0(sev(fst(bd_i_j)),cons0(eig(fst(bd_i_j)),nil0()))))))))),
            TMifnz
            (
              equal_term_int(snd(bd_i_j),5),
              TMtup(cons0(fst(fst(bd_i_j)), cons0(snd(fst(bd_i_j)), cons0(trd(fst(bd_i_j)),cons0(fur(fst(bd_i_j)),cons0(fiv(fst(bd_i_j)),cons0(trd(bd_i_j),cons0(sev(fst(bd_i_j)),cons0(eig(fst(bd_i_j)),nil0()))))))))),
              TMifnz
              (
                equal_term_int(snd(bd_i_j),6),
                TMtup(cons0(fst(fst(bd_i_j)), cons0(snd(fst(bd_i_j)), cons0(trd(fst(bd_i_j)),cons0(fur(fst(bd_i_j)),cons0(fiv(fst(bd_i_j)),cons0(six(fst(bd_i_j)),cons0(trd(bd_i_j),cons0(eig(fst(bd_i_j)),nil0()))))))))),
                TMifnz
                (
                  equal_term_int(snd(bd_i_j),7),
                  TMtup(cons0(fst(fst(bd_i_j)), cons0(snd(fst(bd_i_j)), cons0(trd(fst(bd_i_j)),cons0(fur(fst(bd_i_j)),cons0(fiv(fst(bd_i_j)),cons0(six(fst(bd_i_j)),cons0(sev(fst(bd_i_j)),cons0(trd(bd_i_j),nil0()))))))))),
                  fst(bd_i_j)
                )
              )
            )
          )
        )
      )
    )
  )
)

val TMtrue=TMint(1)
val TMfalse=TMint(0)
val i0_j0_i1_j1=TMvar("i0_j0_i1_j1")

val safety_test1=TMlam
(
  "i0_j0_i1_j1",
  TMifnz
  (
    TMopr("!=", list0_tuple(snd(i0_j0_i1_j1),fur(i0_j0_i1_j1))),
    TMifnz
    (
      TMopr("!=", list0_tuple(
        TMopr("abs",list0_tuple(TMopr("-",list0_tuple(fst(i0_j0_i1_j1),trd(i0_j0_i1_j1))))),
        TMopr("abs",list0_tuple(TMopr("-",list0_tuple(snd(i0_j0_i1_j1),fur(i0_j0_i1_j1))))))),
      TMtrue,
      TMfalse
    ),
    TMfalse
  )
)

val i0_j0_bd_i=TMvar("i0_j0_bd_i")
fun fourpara(t0: term, t1: term, t2: term, t3: term): term = TMtup(cons0(t0, cons0(t1, cons0(t2, cons0(t3, nil0())))))

val safety_test2=TMfix
(
  "f","i0_j0_bd_i",
  TMifnz
  (
    TMopr(">=",list0_tuple(fur(i0_j0_bd_i),TMint(0))),
    TMifnz
    (
      TMapp(safety_test1,fourpara(fst(i0_j0_bd_i),snd(i0_j0_bd_i),fur(i0_j0_bd_i),TMapp(board_get,pair(trd(i0_j0_bd_i),fur(i0_j0_bd_i))))),
      TMapp(f,fourpara(fst(i0_j0_bd_i),snd(i0_j0_bd_i),trd(i0_j0_bd_i),fur(i0_j0_bd_i)-1)),
      TMfalse
    ),
    TMtrue
  )
)

var bd_i_j_nsol=TMvar("bd_i_j_nsol")
fun threepara(t0: term, t1: term, t2: term): term = TMtup(cons0(t0, cons0(t1, cons0(t2, nil0()))))

val search=TMfix
(
  "f","bd_i_j_nsol",
  TMifnz
  (
    TMopr("<",list0_tuple(trd(bd_i_j_nsol),TMint(N))),
    TMifnz
    (
      TMapp(safety_test2,fourpara(snd(bd_i_j_nsol),trd(bd_i_j_nsol),fst(bd_i_j_nsol),snd(bd_i_j_nsol)-1)),
      TMifnz
      (
        equal_term_int(add_term_int(snd(bd_i_j_nsol),1),N),
        TMtup
        (cons0(TMopr("print",list0_tuple(TMstr("Solution #"))),
        cons0(TMopr("print",list0_tuple(add_term_int(fur(bd_i_j_nsol),1))),
        cons0(TMopr("print",list0_tuple(TMstr(":\n\n"))),
        cons0(TMapp(print_board,TMapp(board_set,threepara(fst(bd_i_j_nsol),snd(bd_i_j_nsol),trd(bd_i_j_nsol)))),
        cons0(TMapp(f,fourpara(fst(bd_i_j_nsol),snd(bd_i_j_nsol),add_term_int(trd(bd_i_j_nsol),1),add_term_int(fur(bd_i_j_nsol),1))),
        nil0())))))
        ),
        TMapp(f,fourpara(TMapp(board_set,threepara(fst(bd_i_j_nsol),snd(bd_i_j_nsol),trd(bd_i_j_nsol))),add_term_int(snd(bd_i_j_nsol),1),TMint(0),fur(bd_i_j_nsol)))
      ),
      TMapp(f,fourpara(fst(bd_i_j_nsol),snd(bd_i_j_nsol),add_term_int(trd(bd_i_j_nsol),1),fur(bd_i_j_nsol)))
    ),
    TMifnz
    (
      TMopr(">",list0_tuple(snd(bd_i_j_nsol),TMint(0))),
      TMapp(f,fourpara(fst(bd_i_j_nsol),snd(bd_i_j_nsol)-1,add_term_int(TMapp(board_get,pair(fst(bd_i_j_nsol),snd(bd_i_j_nsol)-1)),1),fur(bd_i_j_nsol))),
      fur(bd_i_j_nsol)
    )
  )
)

val bdpara=bd(TMint(0),TMint(0),TMint(0),TMint(0),TMint(0),TMint(0),TMint(0),TMint(0))

val nsol = TMapp(search,fourpara(bdpara,TMint(0),TMint(0),TMint(0)))

(* ****** ****** *)

implement main0()=
{
  val ()= println!("nsol = ",interp(nsol))
}

(* end of [assign04.dats] *)