-
Notifications
You must be signed in to change notification settings - Fork 2
/
Go_Setup.thy
149 lines (121 loc) · 4.59 KB
/
Go_Setup.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
theory Go_Setup
imports "Main"
begin
ML_file \<open>code_go.ML\<close>
code_identifier
code_module Code_Target_Nat \<rightharpoonup> (Go) Arith
| code_module Code_Target_Int \<rightharpoonup> (Go) Arith
| code_module Code_Numeral \<rightharpoonup> (Go) Arith
code_printing
constant Code.abort \<rightharpoonup>
(Go) "panic( _ )"
(* Bools *)
code_printing
type_constructor bool \<rightharpoonup> (Go) "bool"
| constant "False::bool" \<rightharpoonup> (Go) "false"
| constant "True::bool" \<rightharpoonup> (Go) "true"
code_printing
constant HOL.Not \<rightharpoonup> (Go) "'! _"
| constant HOL.conj \<rightharpoonup> (Go) infixl 1 "&&"
| constant HOL.disj \<rightharpoonup> (Go) infixl 0 "||"
| constant HOL.implies \<rightharpoonup> (Go) "!('!((_)) || (_))"
| constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (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 \<rightharpoonup> (Go) "string"
| constant "STR ''''" \<rightharpoonup> (Go) "\"\""
| constant "Groups.plus_class.plus :: String.literal \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
(Go) infix 6 "+"
| constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
(Go) infix 4 "=="
| constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
(Go) infix 4 "<="
| constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
(Go) infix 4 "<"
setup \<open>
fold Literal.add_code ["Go"]
\<close>
(* Integers via big/math *)
code_printing
code_module "Bigint" \<rightharpoonup> (Go) \<open>
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
}
\<close> for constant "uminus :: integer \<Rightarrow> _" "minus :: integer \<Rightarrow> _" "Code_Numeral.dup" "Code_Numeral.sub"
"(*) :: integer \<Rightarrow> _" "(+) :: integer \<Rightarrow> _" "Code_Numeral.divmod_abs" "HOL.equal :: integer \<Rightarrow> _"
"less_eq :: integer \<Rightarrow> _" "less :: integer \<Rightarrow> _" "abs :: integer \<Rightarrow> _"
"String.literal_of_asciis" "String.asciis_of_literal"
| type_constructor "integer" \<rightharpoonup> (Go) "Bigint.Int"
| constant "uminus :: integer \<Rightarrow> integer" \<rightharpoonup> (Go) "Bigint.Uminus( _ )"
| constant "minus :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup> (Go) "Bigint.Minus( _, _)"
| constant "Code_Numeral.dup" \<rightharpoonup> (Go) "!(Bigint.MkInt(\"2\") * _)"
| constant "Code_Numeral.sub" \<rightharpoonup> (Go) "panic(\"sub\")"
| constant "(+) :: integer \<Rightarrow> _ " \<rightharpoonup> (Go) "Bigint.Plus( _, _)"
| constant "(*) :: integer \<Rightarrow> _ \<Rightarrow> _ " \<rightharpoonup> (Go) "Bigint.Times( _, _)"
| constant Code_Numeral.divmod_abs \<rightharpoonup>
(Go) "func () Prod[Bigint.Int, Bigint.Int] { a, b := Bigint.Divmod'_abs( _, _); return Prod[Bigint.Int, Bigint.Int]{a, b}; }()"
| constant "HOL.equal :: integer \<Rightarrow> _" \<rightharpoonup> (Go) "Bigint.Equal( _, _)"
| constant "less_eq :: integer \<Rightarrow> integer \<Rightarrow> bool " \<rightharpoonup> (Go) "Bigint.Less'_eq( _, _)"
| constant "less :: integer \<Rightarrow> _ " \<rightharpoonup> (Go) "Bigint.Less( _, _)"
| constant "abs :: integer \<Rightarrow> _" \<rightharpoonup> (Go) "Bigint.Abs( _ )"
code_printing
constant "0::integer" \<rightharpoonup> (Go) "Bigint.MkInt(\"0\")"
setup \<open>
Numeral.add_code \<^const_name>\<open>Code_Numeral.Pos\<close> I Code_Printer.literal_numeral "Go"
#> Numeral.add_code \<^const_name>\<open>Code_Numeral.Neg\<close> (~) Code_Printer.literal_numeral "Go"
\<close>
end