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( _ )"
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 "=="
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"]
›
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