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_nameCode_Numeral.Pos I Code_Printer.literal_numeral "Go"
#> Numeral.add_code const_nameCode_Numeral.Neg (~) Code_Printer.literal_numeral "Go"

end