Quelle  Go_Setup.thy

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) ‹
  Bigint

  "math/big"

  Int = big.Int;

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

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

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

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

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

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

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

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

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

  Abs(a Int) Int {
 var b Int
 b.Abs(&a)
 return b
 

  And(a, b Int) Int {
 var c Int
 c.And(&a, &b)
 return c
 

  Or(a, b Int) Int {
 var c Int
 c.Or(&a, &b)
 return c
 

  Xor(a, b Int) Int {
 var c Int
 c.Xor(&a, &b)
 return c
 
 › 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 → _"
  "and :: integer → _" "or :: integer → _" "xor :: 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( _ )"
  | constant "and :: integer → _" ⇀ (Go) "Bigint.And( _, _ )"
  | constant "or :: integer → _" ⇀ (Go) "Bigint.Or( _, _ )"
  | constant "xor :: integer → _" ⇀ (Go) "Bigint.Xor( _, _ )"

code_printing
  constant "0::integer" ⇀ (Go) "Bigint.MkInt(\"0\")"
setup ‹
 .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