Skip to content

Commit

Permalink
remove some code printing for strings
Browse files Browse the repository at this point in the history
This avoids issues with dependency management in code printing.
  • Loading branch information
larsrh committed Jan 22, 2024
1 parent f0a4768 commit 5fba2ef
Showing 1 changed file with 0 additions and 18 deletions.
18 changes: 0 additions & 18 deletions Go_Setup.thy
Original file line number Diff line number Diff line change
Expand Up @@ -38,27 +38,9 @@ definition "go_private_fold_list" where

code_printing
type_constructor String.literal \<rightharpoonup> (Go) "string"
| code_module "StrLiteral" \<rightharpoonup> (Go) \<open>package StrLiteral
import "math/big"
func CharOfAscii (i big.Int) rune {
return rune(i.Int64())
}
func AsciiOfChar (r rune) big.Int {
var i big.Int
i.SetInt64(int64(r))
return i
}
\<close> for constant String.asciis_of_literal String.literal_of_asciis
| constant "STR ''''" \<rightharpoonup> (Go) "\"\""
| constant "Groups.plus_class.plus :: String.literal \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
(Go) infix 6 "+"
| constant String.literal_of_asciis \<rightharpoonup>
(Go) "Go'_private'_fold'_list[rune, string](func(r rune) func(string) string { return func(acc string) string { return string(r) + acc; } } , Go'_private'_map'_list[Bigint.Int, rune](StrLiteral.CharOfAscii, _ ), \"\")"
| constant String.asciis_of_literal \<rightharpoonup>
(Go) "func () List[Bigint.Int] { var a string = _ ; list := List[Bigint.Int](Nil[Bigint.Int]{}); for '_, c := range a { list = List[Bigint.Int](Cons[Bigint.Int]{StrLiteral.AsciiOfChar(c), list}) }; return list; }()"
| constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
(Go) infix 4 "=="
| constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
Expand Down

0 comments on commit 5fba2ef

Please sign in to comment.