Theory Go_Setup

theory Go_Setup
  imports "Main"
begin

ML_file ‹code_go.ML›

code_identifier
  code_module Code_Target_Nat ⇀ (Go) Arith
| code_module Code_Target_Int ⇀ (Go) Arith
| code_module Code_Numeral ⇀ (Go) Arith

code_printing
  constant Code.abort ⇀
    (Go) "panic( _ )"

(* Bools *)
code_printing
  type_constructor bool ⇀ (Go) "bool"
| constant "False::bool" ⇀ (Go) "false"
| constant "True::bool" ⇀ (Go) "true"

code_printing
  constant HOL.Not ⇀ (Go) "'! _"
| constant HOL.conj ⇀ (Go) infixl 1 "&&"
| constant HOL.disj ⇀ (Go) infixl 0 "||"
| constant HOL.implies ⇀ (Go) "!('!((_)) || (_))"
| constant "HOL.equal :: bool ⇒ bool ⇒ bool" ⇀ (Go) infix 4 "=="


(* Strings *)

(* definitions to make these functions available *)
definition "go_private_map_list" where
  "go_private_map_list f a = map f a"
definition "go_private_fold_list" where
  "go_private_fold_list f a b = fold f a b"


code_printing
  type_constructor String.literal ⇀ (Go) "string"
| constant "STR ''''" ⇀ (Go) "\"\""
| constant "Groups.plus_class.plus :: String.literal ⇒ _ ⇒ _" ⇀
    (Go) infix 6 "+"
| constant "HOL.equal :: String.literal ⇒ String.literal ⇒ bool" ⇀
    (Go) infix 4 "=="
| constant "(≤) :: String.literal ⇒ String.literal ⇒ bool" ⇀
    (Go) infix 4 "<="
| constant "(<) :: String.literal ⇒ String.literal ⇒ bool" ⇀
    (Go) infix 4 "<"

setup ‹
  fold Literal.add_code ["Go"]
›


(* Integers via big/math *)
code_printing
  code_module "Bigint" ⇀ (Go) ‹
package Bigint

import "math/big"

type Int = big.Int;

func MkInt(s string) Int {
  var i Int;
  _, e := i.SetString(s, 10);
  if (e) {
    return i;
  } else {
    panic("invalid integer literal")
  }
}

func Uminus(a Int) Int {
  var b Int
  b.Neg(&a)
  return b
}

func Minus(a, b Int) Int {
  var c Int
  c.Sub(&a, &b)
  return c
}

func Plus(a, b Int) Int {
  var c Int
  c.Add(&a, &b)
  return c
}

func Times (a, b Int) Int {
  var c Int
  c.Mul(&a, &b)
  return c
}

func Divmod_abs(a, b Int) (Int, Int) {
  var div, mod Int
  div.DivMod(&a, &b, &mod)
  div.Abs(&div)
  return div, mod
}

func Equal(a, b Int) bool {
  return a.Cmp(&b) == 0
}

func Less_eq(a, b Int) bool {
  return a.Cmp(&b) != 1
}

func Less(a, b Int) bool {
  return a.Cmp(&b) == -1
}

func Abs(a Int) Int {
  var b Int
  b.Abs(&a)
  return b
}
› for constant "uminus :: integer ⇒ _" "minus :: integer ⇒ _" "Code_Numeral.dup" "Code_Numeral.sub"
  "(*) :: integer ⇒ _" "(+) :: integer ⇒ _" "Code_Numeral.divmod_abs" "HOL.equal :: integer ⇒ _"
  "less_eq :: integer ⇒ _" "less :: integer ⇒ _" "abs :: integer ⇒ _"
  "String.literal_of_asciis" "String.asciis_of_literal"
  | type_constructor "integer" ⇀ (Go) "Bigint.Int"
  | constant "uminus :: integer ⇒ integer" ⇀ (Go) "Bigint.Uminus( _ )"
  | constant "minus :: integer ⇒ integer ⇒ integer" ⇀ (Go) "Bigint.Minus( _, _)"
  | constant "Code_Numeral.dup" ⇀ (Go) "!(Bigint.MkInt(\"2\") * _)"
  | constant "Code_Numeral.sub" ⇀ (Go) "panic(\"sub\")"
  | constant "(+) :: integer ⇒ _ " ⇀ (Go) "Bigint.Plus( _, _)"
  | constant "(*) :: integer ⇒ _ ⇒ _ " ⇀ (Go) "Bigint.Times( _, _)"
  | constant Code_Numeral.divmod_abs ⇀
     (Go) "func () Prod[Bigint.Int, Bigint.Int] { a, b := Bigint.Divmod'_abs( _, _); return Prod[Bigint.Int, Bigint.Int]{a, b}; }()"
  | constant "HOL.equal :: integer ⇒ _" ⇀ (Go) "Bigint.Equal( _, _)"
  | constant "less_eq :: integer ⇒ integer ⇒ bool " ⇀ (Go) "Bigint.Less'_eq( _, _)"
  | constant "less :: integer ⇒ _ " ⇀ (Go) "Bigint.Less( _, _)"
  | constant "abs :: integer ⇒ _" ⇀ (Go) "Bigint.Abs( _ )"


code_printing
  constant "0::integer" ⇀ (Go) "Bigint.MkInt(\"0\")"
setup ‹
Numeral.add_code \<^const_name>‹Code_Numeral.Pos› I Code_Printer.literal_numeral "Go"
#> Numeral.add_code \<^const_name>‹Code_Numeral.Neg› (~) Code_Printer.literal_numeral "Go"
›

end