open HolKernel Parse boolLib bossLib

open ParserHelpers
open TypeParser
open ValueParser
open CodeParser
open wordsTheory
open sumMonadTheory
open uvmTypesTheory
open uvmValuesTheory
open uvmMemoryTheory
open uvmIRTheory

val _ = new_theory "codeTest"

fun assert_parse_inst(s, i) =
  let val i' = uir_inst mock_context [QUOTE ("(* *)" ^ s)]
        handle HOL_ERR e => raise ParseError(
          "failed to parse inst '" ^ s ^ "': " ^ #message e)
  in
    prove(mk_eq(i', mk_return i),
      simp[lift_left_def, ap_left_def, mapM_left_def, sequence_left_def])
    handle HOL_ERR e => raise ParseError(
      "inst '" ^ s ^ "' did not parse as (" ^ term_to_string i ^ "): " ^ #message e)
  end

fun assert_parse_terminst(s, i) =
  let val i' = uir_terminst mock_context [QUOTE ("(* *)" ^ s)]
        handle HOL_ERR e => raise ParseError(
          "failed to parse terminst '" ^ s ^ "': " ^ #message e)
  in
    prove(mk_eq(i', mk_return i),
      rw[get_callee_def] >> simp[lift_left_def, ap_left_def, mapM_left_def, sequence_left_def])
    handle HOL_ERR e => (
      print (type_to_string (type_of i') ^ "; " ^ type_to_string (type_of i));
      raise ParseError(
        "terminst '" ^ s ^ "' did not parse as (" ^ term_to_string i ^ "): " ^ #message e))
  end

val _ =
  assert_parse_inst("ID <int<8>> %bar",
    ``Assign [] (Id (Int 8) (Var %"bar"))``);
  assert_parse_inst("%foo = ID <int<8>> %bar",
    ``Assign [%"foo"] (Id (Int 8) (Var %"bar"))``);
  assert_parse_inst("(%foo %bar) = ID <int<8>> %baz",
    ``Assign [%"foo"; %"bar"] (Id (Int 8) (Var %"baz"))``);
  assert_parse_inst("ADD <int<8>> %a %b",
    ``Assign [] (BinOp ADD (Int 8) (Var %"a") (Var %"b"))``);
  assert_parse_inst("UGT <int<8>> %a %b",
    ``Assign [] (CmpOp UGT (Int 8) (Var %"a") (Var %"b"))``);
  assert_parse_inst("TRUNC <int<8> int<16>> %a",
    ``Assign [] (ConvOp TRUNC (Int 8) (Int 16) (Var %"a"))``);
  assert_parse_inst("%th = NEWTHREAD %st THROW_EXC %ex",
    ``NewThread (%"th") (Var %"st") (Const (RefV Void NONE))
        (ThrowExc (Var %"ex"))``);
  assert_parse_inst("%th = NEWTHREAD %st PASS_VALUES <int<8> int<16>> (%a %b)",
    ``NewThread (%"th") (Var %"st") (Const (RefV Void NONE))
        (PassValues [(Var %"a", Int 8); (Var %"b", Int 16)])``);
  assert_parse_terminst("RET (%foo %bar)", ``Ret [Var %"foo"; Var %"bar"]``);
  assert_parse_terminst("THROW %foo", ``Throw (Var %"foo")``);
  assert_parse_terminst("BRANCH %label(%a %b)",
    ``Branch1 (BlockLabel "label", [Var %"a"; Var %"b"])``);
  assert_parse_terminst("BRANCH2 %cond %t() %f()",
    ``Branch2 (Var %"cond") (BlockLabel "t", []) (BlockLabel "f", [])``);
  assert_parse_terminst("TAILCALL <(int<8>) -> ()> %fn (%arg)",
    ``TailCall <|
        name := INL %"fn";
        args := [Var %"arg"];
        signature := <|arg_types := [Int 8]; return_types := []|>;
        convention := Mu
      |>``);
  assert_parse_terminst("CALL <(int<8>) -> ()> %fn (%arg) EXC (%n() %e())",
    ``Call [] <|
        name := INL %"fn";
        args := [Var %"arg"];
        signature := <|arg_types := [Int 8]; return_types := []|>;
        convention := Mu
      |> <|
        normal_dest := (BlockLabel "n", []);
        exceptional_dest := SOME (BlockLabel "e", [])
      |>``);
  assert_parse_terminst("%x = CALL <(int<8>) -> (int<8>)> %fn (%arg) EXC (%n(%x) %e())",
    ``Call [%"x"] <|
        name := INL %"fn";
        args := [Var %"arg"];
        signature := <|arg_types := [Int 8]; return_types := [Int 8]|>;
        convention := Mu
      |> <|
        normal_dest := (BlockLabel "n", [Var %"x"]);
        exceptional_dest := SOME (BlockLabel "e", [])
      |>``);
  assert_parse_terminst("%x = COMMINST @uvm.new_stack <[@sig]> (%st) EXC (%n(%x))",
    ``CommInst [%"x"] (NewStack <|arg_types := []; return_types := []|> (Var %"st"))
      <| normal_dest := (BlockLabel "n", [Var %"x"]);
         exceptional_dest := NONE
      |>``);
  assert_parse_terminst("COMMINST @uvm.current_stack EXC (%n() %e())",
    ``CommInst [] CurrentStack <|
        normal_dest := (BlockLabel "n", []);
        exceptional_dest := SOME (BlockLabel "e", [])
      |> : ssavar terminst``);
    

(* Equality testing for basic blocks and functions is nigh-impossible, so
   instead just run the parsing functions and make sure they don't throw.
*)
val _ =
  print "parsing basic block\n";
  uir_block mock_context `
    %add(<int<8>> %a <int<8>> %b):
      %res = ADD <int<8>> %a %b
      RET (%res)
  `;

val _ =
  print "parsing function\n";
  uir_func mock_context (uir_funcsig mock_context `(int<8>) -> (int<8>)`) `
    %entry(<int<8>> %n):
      %is1 = ULE <int<8>> %n %one
      BRANCH2 %is1 %done() %recur(%n)
    %recur(<int<8>> %n):
      %minus1 = SUB <int<8>> %n %one
      %x = CALL <(int<8>) -> (int<8>)> %fact (%minus1) EXC (%mul(%n %x) %done())
    %mul(<int<8>> %m <int<8>> %n):
      %result = MUL <int<8>> %m %n
      RET (%result)
    %done():
      RET (%one)
  `;

val _ = export_theory()