diff --git a/thys/Go/Go_Setup.thy b/thys/Go/Go_Setup.thy new file mode 100644 --- /dev/null +++ b/thys/Go/Go_Setup.thy @@ -0,0 +1,149 @@ +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_name>\Code_Numeral.Pos\ I Code_Printer.literal_numeral "Go" +#> Numeral.add_code \<^const_name>\Code_Numeral.Neg\ (~) Code_Printer.literal_numeral "Go" +\ + +end \ No newline at end of file diff --git a/thys/Go/ROOT b/thys/Go/ROOT new file mode 100644 --- /dev/null +++ b/thys/Go/ROOT @@ -0,0 +1,32 @@ +chapter AFP + +session Go = HOL + + description "A Go frontend for the code generator." + options [timeout = 300] + theories + Go_Setup + document_files + "root.tex" + +session Go_Test_Quick in "test/quick" = Go + + description "Quick test session with BigInts and RBTs" + options [timeout = 300] + sessions + "HOL-Data_Structures" + theories [document = false] + RBT_Test + export_files [3] + "*:code/export1/**" + +session Go_Test_Slow in "test/slow" = "HOL-Library" + + description "Slow test session for (almost) the entire HOL-Library" + options [timeout = 1200] + sessions + Go + "HOL-Number_Theory" + "HOL-Data_Structures" + "HOL-Examples" + theories [document = false] + Candidates + Generate + Generate_Binary_Nat diff --git a/thys/Go/code_go.ML b/thys/Go/code_go.ML new file mode 100644 --- /dev/null +++ b/thys/Go/code_go.ML @@ -0,0 +1,752 @@ + +signature CODE_GO = +sig + val target: string +end; + +structure Code_Go : CODE_GO = +struct + +open Basic_Code_Symbol; +open Basic_Code_Thingol; +open Code_Printer; + +infixr 5 @@; +infixr 5 @|; + +val target = "Go"; + +fun map_terms_bottom_up f (t as IConst _) = f t + | map_terms_bottom_up f (t as IVar _) = f t + | map_terms_bottom_up f (t1 `$ t2) = f + (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) + | map_terms_bottom_up f ((v, ty) `|=> (t, rty)) = f + ((v, ty) `|=> (map_terms_bottom_up f t, rty)) + | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f + (ICase { term = map_terms_bottom_up f t, typ = ty, + clauses = (map o apply2) (map_terms_bottom_up f) clauses, + primitive = map_terms_bottom_up f t0 }); + +fun range_of_head t = + case fst (Code_Thingol.unfold_app t) of + IConst {range, ...} => range + +val print_go_string = + let + fun unicode i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i) + fun char "\"" = "\\\"" + | char "\\" = "\\\\" + | char c = + let val i = ord c + in if i < 32 orelse i > 126 + then unicode i + else if i >= 128 + then error "non-ASCII byte in Go string literal" + else c + end; + in quote o translate_string char end; + + +fun block_enclose (prt1, prt2) prts = (* Pretty.block_enclose (prt1, prt2) prts*) + Pretty.chunks [Pretty.block (Pretty.fbreaks ((Pretty.unbreakable prt1) :: prts)), Pretty.unbreakable prt2]; + +fun print_go_numeral num = "Bigint.MkInt(\"" ^ signed_string_of_int num ^ "\")"; + +val literals = Literals { + literal_string = print_go_string, + literal_numeral = print_go_numeral, + literal_list = enum "," "[" "]", + infix_cons = (6, "") (* TODO: this will go wrong if ever used *) +}; + + + +(* the subset of thingol we actually need for Go *) +datatype go_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list + | Datatype of vname list * ((string * vname list) * itype list) list + | Class of (vname * ((class * class) list * (string * itype) list)) + | Datatypecons of string + | Instance of { class: string, tyco: string, vs: (vname * sort) list, + superinsts: (class * (itype * dict list) list) list, + inst_params: ((string * (const * int)) * (thm * bool)) list, + superinst_params: ((string * (const * int)) * (thm * bool)) list }; + +fun print_go_stmt gen_stringer undefineds infinite_types tyco_syntax const_syntax reserved + args_num is_sum_type is_class_param is_constr (deresolve, deresolve_full) = + let + fun lookup_tyvar tyvars = lookup_var tyvars; + fun intro_tyvars vs = intro_vars (map fst vs); + val deresolve_const = deresolve o Constant; + val deresolve_class = deresolve o Type_Class; + val deresolve_classrel = deresolve o Class_Relation; + val deresolve_inst = deresolve o Class_Instance; + val deresolve_tyco = deresolve o Type_Constructor; + val oneline = Pretty.unbreakable o semicolon; + val block = Pretty.unbreakable o Pretty.block; + val spaced = Pretty.unbreakable o concat; + + fun mk_dest_name name = Long_Name.map_base_name (fn s => s^"_dest") name + fun applify_constraints _ head [] = head + | applify_constraints tyvars head vs = let + val anys = (block o commas o map (str o lookup_tyvar tyvars)) vs + in block [head, str "[", anys, Pretty.brk 1, str "any", str "]"] end + + fun print_go_typ tyvars (tyco `%% tys) = (case tyco_syntax tyco of + NONE => apply_constraints tyvars ((str o deresolve_tyco) tyco) tys + | SOME (_, print) => print (K (print_go_typ tyvars)) NOBR tys) + | print_go_typ tyvars (ITyVar v) = (str o lookup_tyvar tyvars) v + and apply_constraints tyvars head vs = + gen_applify false "[" "]" (print_go_typ tyvars) NOBR head vs + + (* uncurried types of functions in type classes are special-cased here *) + fun print_go_typ_uncurried_toplevel tyvars (typ as "fun" `%% _) = let + val (args, rtyp) = Code_Thingol.unfold_fun typ + val head = applify "(" ")" (print_go_typ tyvars) NOBR (str "func") args; + in concat [head, print_go_typ tyvars rtyp] end + | print_go_typ_uncurried_toplevel tyvars typ = + block [str "func () ", print_go_typ tyvars typ] + + (* wrap a statement into an immediately called function to make it an expression *) + fun wrap_into_lambda tyvars typ body = + block_enclose + (concat [str "func ()", print_go_typ tyvars typ, str "{"], str "}()") body + fun wrap_in_return t = oneline [str "return", t] + fun wrap_if true = wrap_in_return + | wrap_if false = I + + fun print_func head body = block_enclose + (block [str "func ", head, str " {"], str "}") + [body]; + fun print_func_head tyvars vars const tvs extras params tys rty = let + val args = params ~~ tys + |> map (fn (param, ty) => let + val name = case param of + NONE => "_" | SOME n => lookup_var vars n; + in Pretty.block [str name, Pretty.brk 1, print_go_typ tyvars ty] end) + |> (curry op @ extras) + |> enum "," "(" ")" + val sym = case const of + SOME name => (str o deresolve) name + | NONE => str "" + val func_head = concat (applify_constraints tyvars sym tvs :: [args, rty]); + in func_head + end; + + (* a definition of a datatype *) + fun print_go_typedef tyco vs cos reserved = let + val [p,m] = Name.invent (snd reserved) "p" 2 + val ctxt = Name.declare p (Name.declare m (snd reserved)) + val tyargs = map ITyVar vs + val self = tyco `%% tyargs + val tyvars = intro_tyvars (map (rpair []) vs) reserved; + val allowed_infinite = List.exists (fn n => n = tyco) infinite_types + + fun print_constructor m type_name ((name,_), tys) = let + val named_fields = Name.invent_names ctxt "A" tys + val fields = named_fields + |> map (fn (name, arg) => oneline [str name, print_go_typ tyvars arg]) + val head = applify_constraints tyvars (str name) vs + val typ = apply_constraints tyvars (str name) tyargs + val elim_body = if type_name = NONE + then let + val case_branch = block + [str "return ", (Pretty.block o commas) (map (fn (field,_) => str (p^"."^field)) named_fields)] + in (*Pretty.chunks + [oneline [str ((if null named_fields then "_ = " else m^" := ")^p^".("), typ , str ")"] + ,*) case_branch end + else Pretty.block [oneline [str "return ", (Pretty.block o commas) (map (fn (field,_) => str (p^"."^field)) named_fields)]] + val elim_name = mk_dest_name (case type_name of + NONE => name + | SOME name' => name') + val eliminator = if null tys then str "" else print_func + (applify "(" ")" I NOBR (Pretty.block [applify_constraints tyvars (str elim_name) vs, str ("("^p^" "), typ, str ")"]) (map (print_go_typ tyvars o snd) named_fields)) + elim_body + val pretty = name ^ "(" ^ (fold (curry (op ^)) (map (K "%v") fields) "") ^ ")" + val constr = oneline [block_enclose (concat [str "type", head, str "struct {"], str "}") + fields] + in (constr, eliminator) end + in if not allowed_infinite andalso length cos = 1 then case cos of + [((name,_),tys)] => let + val name = deresolve_const name + val tname = deresolve_tyco tyco + val (constr, dest) = print_constructor m (SOME name) ((tname, []), tys) + in Pretty.chunks [constr, dest] end + else let + val (constrs, destrs) = cos + |> map (fn ((name,_),tys) => ((deresolve_const name, []),tys)) + |> map (print_constructor m NONE) + |> split_list + val names = map (fn ((name,_),_) => (str o deresolve_const) name) cos + val comment = block (str "// sum type which can be " :: Pretty.commas names) + val any = oneline [str "type", applify_constraints tyvars ((str o deresolve_tyco) tyco) vs, str "any"] + in Pretty.chunks (comment :: any :: constrs @ destrs) end + end; + + + fun print_classrels [] ps = Pretty.block ps + | print_classrels rels ps = let + val postfix = rels + |> map (fn (self, super) => (Long_Name.base_name o deresolve_classrel) (self, super)) + |> rev + |> String.concatWith "." + in block (ps @ [str ".", str postfix]) end + fun print_dict tyvars (Dict (classrels, x)) = + print_classrels classrels (print_plain_dict tyvars x) + and print_plain_dict tyvars (Dict_Const (inst, args)) = let + val needs_mono = true (* not (length args = 0)*) + val (typargs, dss) = split_list args + val wrap = if needs_mono + then fn head => apply_constraints tyvars head typargs + else I + in wrap ((str o deresolve_inst) inst) + :: (if needs_mono then [((enum "," "(" ")") o map (print_dict tyvars) o flat) dss] else []) end + | print_plain_dict tyvars (Dict_Var { var, index, length, ... }) = + [str (if length = 1 then var ^ "_" + else var ^ string_of_int (index + 1) ^ "_")] + + fun wrap_new_scope term = + block_enclose (str "{", str "};") [term] + + fun type_of_primitive_pattern t = + let + val destructor = case fst (Code_Thingol.unfold_app t) of + IConst const => const + val extras = drop (args_num (#sym destructor)) (#dom destructor) + in extras `--> (#range destructor) + end + + fun print_app_expr const_syntax tyvars some_thm vars + (app as ({ sym, dicts, dom, range, typargs, ... }, ts)) = let + val k = length dom + val l = args_num sym + in if length ts = k then + let + val is_constr = is_constr sym + val is_sum_type = is_sum_type sym + val is_class_param = is_class_param sym + val dict_args = map (print_dict tyvars) (flat dicts) + val typ = case snd (Code_Thingol.unfold_fun range) of + name `%% _ => name | ITyVar name => name + val allowed_infinite = List.exists (fn n => n = typ) infinite_types + andalso is_constr + val _ = if is_class_param andalso not (length dict_args = 1) + then warning "bug in print_app" else () + val applify' = if is_constr + then gen_applify true "{" "}" + else gen_applify true "(" ")" + val (immediate, curried) = chop l ts + val symbol = if is_constr + then (if is_sum_type orelse allowed_infinite then sym else Type_Constructor typ) + else sym + val func_name = if is_class_param + then Pretty.block [hd dict_args, str ".", (str o deresolve) symbol] + else (str o deresolve) symbol + fun wrap_type_args s = if is_sum_type orelse allowed_infinite + then applify "(" ")" I APP (apply_constraints tyvars ((str o deresolve_tyco) typ) typargs) [s] + else s + fun wrap_type_conversion name = + let + val typargs = if is_constr + (* these typargs are always the same set as the outer ones, but sometimes in different order *) + then case range of _ `%% typargs => typargs | _ => [] + else typargs + in if is_class_param then name + else apply_constraints tyvars name typargs + end + val immediate_args = immediate + |> map (print_go_expr const_syntax tyvars some_thm vars BR) + val invocation = (if is_class_param orelse is_constr then immediate_args else dict_args @ immediate_args) + |> applify' I APP (wrap_type_conversion func_name) + |> wrap_type_args + val curried_args = curried + |> map (enclose "(" ")" o single o print_go_expr const_syntax tyvars some_thm vars NOBR) + in invocation :: curried_args + end + else + [print_go_expr const_syntax tyvars some_thm vars BR (Code_Thingol.saturated_application k app)] + end + and print_clause _ _ _ _ [] _ = + raise Fail "there's a bug in the pattern-match translator" + | print_clause tyvars some_thm vars p ((target, pattern) :: subps) term = + let + fun print_condition vars conds (constr, typargs, range, args) p q target body = let + val destructor = (mk_dest_name o deresolve) constr + val (tyco, typargs) = case snd (Code_Thingol.unfold_fun range) of + a `%% typargs => (a, typargs) + val is_boxed = is_sum_type constr orelse List.exists (fn n => n = tyco) infinite_types + val names = map (fn (SOME n) => (str o lookup_var vars) n | NONE => str "_") args + val any_names = exists is_some args + val checks = conds + |> map (fn (var,const) => concat [ + str var, + str "==", + enclose "(" ")" [print_app false const_syntax tyvars some_thm vars NOBR (const, [])] + ]) + |> separate (str "&&") + |> concat + in Pretty.chunks + ((if is_boxed then [oneline [(block o commas) [str (if any_names then q else "_"), str p], str ":=", + applify ".(" ")" I NOBR (str target) [apply_constraints tyvars ((str o deresolve) constr) typargs]]] + else [oneline [str "_ =", str target]]) + @ [(if is_boxed then block_enclose (spaced [str "if", str p, str "{"], str "}") else Pretty.chunks) + ((if any_names then [oneline ((Pretty.block o commas) names :: [str ":=", applify "(" ")" str NOBR (str destructor) [if is_boxed then q else target]])] + else []) + @ [(if null conds then Pretty.chunks else (block_enclose ((spaced [str "if", checks, str "{"]), str "}"))) + [body]])]) + end + in case pattern + of IConst c => + let + val checks = concat + [str target, str "==", enclose "(" ")" [print_app false const_syntax tyvars some_thm vars NOBR (c, [])]] + val body = (if subps = [] + then print_go_term const_syntax tyvars some_thm vars NOBR term + else print_clause tyvars some_thm vars p subps term) + in block_enclose ((spaced [str "if", checks, str "{"]), str "}") + [body] + end + | _ `$ _ => (case Code_Thingol.unfold_const_app pattern of + NONE => raise Fail "bad application in pattern match" + | SOME (constr, args) => let + val ((arg_names, subpatterns, conds), vars') = + fold_rev (fn term => fn ((ts, rs, cs), vars) => case term of + IConst c => let + val [name] = Name.invent (snd vars) "c" 1 + in ((SOME name :: ts, rs,(name,c) :: cs), intro_vars [name] vars) end + | IVar NONE => ((NONE :: ts, rs, cs), vars) + | IVar (SOME v) => ((SOME v :: ts, rs, cs), intro_vars [v] vars) + | _ `$ _ => let + val [name] = Name.invent (snd vars) "p" 1 + in ((SOME name :: ts, (name, term) :: rs, cs), intro_vars [name] vars) end) + args (([],[],[]), vars) + val [q] = Name.invent (snd vars) "q" 1 + val vars = intro_vars [q] vars + val wrapper = print_condition vars' conds (#sym constr, #typargs constr, #range constr, arg_names) p q target + val subpatterns' = subpatterns @ subps + in wrapper (if subpatterns' = [] + then print_go_term const_syntax tyvars some_thm vars' NOBR term + else print_clause tyvars some_thm vars' p subpatterns' term) + end) + | IVar v => let + val vars' = intro_vars (the_list v) vars + val name_printed = case v of + NONE => str "_" | SOME name => (str o lookup_var vars') name + val binding = oneline [name_printed, str ":=", str target] + val usage = case v of + SOME _ => oneline [str "_ =", name_printed] + | NONE => str "" + val body = if subps = [] + then print_go_term const_syntax tyvars some_thm vars' NOBR term + else print_clause tyvars some_thm vars' p subps term + in + Pretty.chunks [binding, body] + end + | _ => raise Fail "bad term in pattern" + end + and print_pattern_match is_stmt tyvars some_thm vars rtyp target clauses = + let + val [target_var] = Name.invent (snd vars) "target" 1 + val vars = intro_vars [target_var] vars + val [p] = Name.invent (snd vars) "m" 1 + val vars = intro_vars [p] vars + val target = print_go_expr const_syntax tyvars some_thm vars NOBR target + val assignment = oneline [str target_var, str ":=", target] + val body = assignment + :: map (fn (pattern,term) => + wrap_new_scope (print_clause tyvars some_thm vars p [(target_var, pattern)] term)) + clauses @ [oneline [str "panic(\"match failed\")"]] + in if is_stmt + then Pretty.chunks body + else wrap_into_lambda tyvars rtyp body + end + and print_app is_stmt const_syntax tyvars some_thm vars fxy (app as (const, args)) = + if List.exists (fn name => #sym const = Constant name) undefineds then + args + (* the arguments may use otherwise-unused variables, so just print somewhere to make Go happy *) + |> map (print_go_expr const_syntax tyvars some_thm vars fxy) + |> map (fn p => oneline [ str "_ = ", p]) + |> curry (op @) [ str ("panic(\"encountered undefined function: \" + "^print_go_string (Code_Symbol.default_base (#sym const))^")") ] + |> Pretty.chunks + else wrap_if is_stmt (gen_print_app (print_app_expr const_syntax tyvars) + (print_go_expr const_syntax tyvars) const_syntax some_thm vars fxy app) + (* go has a distinction between expressions and statements which Thingol doesn't, so we just + periodically have to wrap things into a lambda & return *) + and print_go_term const_syntax tyvars some_thm vars fxy iterm = + print_go_term_gen true const_syntax tyvars some_thm vars fxy iterm + and print_go_expr const_syntax tyvars some_thm vars fxy t = + print_go_term_gen false const_syntax tyvars some_thm vars fxy t + and print_go_term_gen is_stmt const_syntax tyvars some_thm vars fxy t = case t of + IConst (const as {sym,...}) => let + in (print_app is_stmt const_syntax tyvars some_thm vars fxy (const, [])) end + | t1 `$ t2 => (case Code_Thingol.unfold_const_app t of + SOME app => + (print_app is_stmt const_syntax tyvars some_thm vars fxy app) + | _ => wrap_if is_stmt + (applify "(" ")" (print_go_expr const_syntax tyvars some_thm vars NOBR) fxy + (print_go_expr const_syntax tyvars some_thm vars BR t1) [t2])) + | IVar NONE => raise Fail "can't return a variable with no name!" + | IVar (SOME v) => wrap_if is_stmt (str (lookup_var vars v)) + | (params, tys) `|=> (t, rty) => let + (* horrible workaround, please fix me upstream *) + val rty = case t of + ICase c => type_of_primitive_pattern (#primitive c) + | _ => rty + val vars' = intro_vars (map_filter I [params]) vars; + val func_head = print_func_head tyvars vars' NONE [] [] [params] [tys] (print_go_typ tyvars rty) + val body = print_go_term const_syntax tyvars some_thm vars' fxy t + in wrap_if is_stmt (print_func func_head body) end + | ICase { clauses = [], ... } => let + val _ = warning "empty case statement; generating call to panic() ..."; + in str "panic(\"empty case\");" end + (* this is a let-binding, represented as a case *) + | ICase (cases as { clauses = [_], ...}) => + let + val (binds, body) = Code_Thingol.unfold_let (ICase cases); + val does_not_pattern_match = List.all (Code_Thingol.is_IVar o fst o fst) binds + in if does_not_pattern_match then + let + fun print_call t vars = + (print_go_expr const_syntax tyvars some_thm vars fxy t, vars); + fun print_bind tyvars some_thm fxy p = + gen_print_bind (print_go_expr const_syntax tyvars) some_thm fxy p + fun print_assignment ((pat, _), t) vars = vars + |> print_bind tyvars some_thm BR pat + |>> (fn p => (oneline [p, str ":=", + fst (print_call t vars)])) + fun print_left ((IVar NONE, _), t) = + print_call t (* evaluate and discard the result; go does not allow declaring to blank *) + | print_left ((pat as IVar (SOME _), ty), t) = + print_assignment ((pat, ty), t) + val (seps_ps, vars') = + fold_map print_left binds vars; + val term = print_go_term const_syntax tyvars some_thm vars' fxy body + in if is_stmt then Pretty.chunks (seps_ps @ [term]) + else wrap_into_lambda tyvars (type_of_primitive_pattern (#primitive cases)) (seps_ps @ [term]) + end + else + print_pattern_match is_stmt tyvars some_thm vars + (type_of_primitive_pattern (#primitive cases)) (#term cases) (#clauses cases) + end + | ICase cases => print_pattern_match is_stmt tyvars some_thm vars + (type_of_primitive_pattern (#primitive cases)) (#term cases) (#clauses cases); + + fun print_dict_args tyvars vs = + let + fun print_single_arg length v (index, class) = + let + val name = if length = 1 then v^"_" else v ^ string_of_int (index + 1) ^ "_" + val ty = apply_constraints tyvars ((str o deresolve_class) class) [ITyVar v] + in concat [str name, ty] end + fun print_single_dict (v, sort) = let + val args = map_index (print_single_arg (length sort) v) sort + in args end + in (flat (map print_single_dict vs)) + end; + + + fun print_go_func const_syntax reserved const vs ty [] = + let + val (tys, ty') = Code_Thingol.unfold_fun ty; + val params = Name.invent (snd reserved) "a" (length tys); + val tyvars = intro_tyvars vs reserved; + val vars = intro_vars params tyvars; + val dict_args = print_dict_args tyvars vs + val head = print_func_head tyvars vars ((SOME o Constant) const) (map fst vs) dict_args (map SOME params) tys (print_go_typ tyvars ty'); + val _ = warning ("you appear to have defined a function "^const^" with no body; generating a call to panic() ...") + in + print_func head (oneline [str ("panic("^print_go_string const^")")]) + end + | print_go_func const_syntax reserved const vs ty eqs = + let + val tycos = build (fold (fn ((ts, t), _) => + fold Code_Thingol.add_tyconames (t :: ts)) eqs); + val tyvars = reserved + |> intro_base_names + (is_none o tyco_syntax) deresolve_tyco tycos + |> intro_tyvars vs; + val simple = case eqs + of [((ts, _), _)] => forall Code_Thingol.is_IVar ts + | _ => false; + val vars1 = reserved + |> intro_tyvars vs + |> intro_base_names_for (is_none o const_syntax) + deresolve (map (snd o fst) eqs); + val params = if simple + then (map (fn IVar x => x) o fst o fst o hd) eqs + else map SOME (aux_params vars1 (map (fst o fst) eqs)); + val vars2 = intro_vars (map_filter I params) vars1; + val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty; + fun print_rhs is_stmt vars' ((_, t), (some_thm, _)) = + print_go_term_gen is_stmt const_syntax tyvars some_thm vars' NOBR t; + val [p] = Name.invent (snd vars2) "m" 1 + val vars3 = intro_vars [p] vars2 + fun print_fun_clause ((targets, t), (some_thm, _)) = + let + val used = Code_Thingol.add_varnames t [] + val vars' = + intro_vars (build (fold Code_Thingol.add_varnames targets)) vars2; + fun remove_unused (IVar (SOME name)) = IVar + (if member (op =) used name then SOME name else NONE) + | remove_unused t = t + val clauses = params ~~ targets + |> map (apsnd (map_terms_bottom_up remove_unused)) + |> filter (fn (_, IVar NONE) => false | _ => true) + |> map_filter (fn (NONE, _) => NONE | (SOME v, t) => SOME (v,t)) + val clause = print_clause tyvars some_thm vars' p clauses t + in + wrap_new_scope clause + end; + val dict_args = print_dict_args tyvars vs + val head = print_func_head tyvars vars3 ((SOME o Constant) const) (map fst vs) dict_args params tys' (print_go_typ tyvars ty'); + in (*if null params andalso null vs then + print_var ((str o deresolve_const) const) (print_rhs false vars2 (hd eqs)) + else*) + if simple then + print_func head (print_rhs true vars2 (hd eqs)) + else + print_func head (Pretty.chunks + (map print_fun_clause eqs @ [oneline [str "panic(\"match failed\")"]])) + end; + fun print_typeclass tyvars sym ((target, (super, params))) = + let + val tyvars = intro_vars [target] tyvars + val super_fields = super + |> map (fn (self, super) => block [ + (str o Long_Name.base_name o deresolve_classrel) (self, super), + Pretty.brk 1, + apply_constraints tyvars ((str o deresolve_class) super) [ITyVar target] + ]) + val fields = params + |> map (fn (name,typ) => block [ + (str o deresolve_const) name, Pretty.brk 1, + print_go_typ_uncurried_toplevel tyvars typ + ]) + |> (curry op @) super_fields + val head = applify_constraints tyvars ((str o deresolve_class) sym) [target] + in block_enclose (concat [str "type", head, str "struct {"], str "}") fields + end; + fun print_instance tyvars (target, class) {vs, inst_params, superinsts, tyco, ...} = + let + val class_name = deresolve_class class + val tyvars = intro_tyvars vs tyvars + val tyargs = map fst vs + val class_head = apply_constraints tyvars (str class_name) [tyco `%% (map ITyVar tyargs)] + val sym = Class_Instance (target, class) + val instance_name = deresolve_inst (target, class) + val superinsts_fields = superinsts + |> map (fn (super, dicts) => block [ + (str o Long_Name.base_name o deresolve_classrel) (class, super), + str ":", Pretty.brk 1, + print_dict tyvars (Dict ([], Dict_Const ((tyco, super), dicts))), str "," + ]) + fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) = + let + val aux_dom = Name.invent_names (snd reserved) "A" dom; + val auxs = map fst aux_dom; + val vars = intro_vars auxs tyvars; + val (aux_dom1, aux_dom2) = chop dom_length aux_dom; + fun abstract_using [] _ _ body = body + | abstract_using aux_dom should_wrap rty body = let + val params = aux_dom + |> map (fn (aux, ty) => + block [(str o lookup_var vars) aux, Pretty.brk 1, print_go_typ tyvars ty]) + val head = print_func_head tyvars vars NONE [] params [] [] + ((if should_wrap then print_go_typ_uncurried_toplevel else print_go_typ) tyvars rty) + in print_func head (wrap_if should_wrap body) end; + val aux_abstract = if not (null aux_dom1) andalso not (null aux_dom2) + then abstract_using aux_dom1 true (map snd aux_dom2 `--> #range const) o abstract_using aux_dom2 false (#range const) + else abstract_using aux_dom1 false (#range const) o abstract_using aux_dom2 false (#range const) + val wrap_in_func = if null aux_dom1 andalso null aux_dom2 + then print_func (print_func_head tyvars vars NONE [] [] [] [] (print_go_typ tyvars (#range const))) else I + val wrap_aux = case (null aux_dom1, null aux_dom2) of + (true, true) => print_func (print_func_head tyvars vars NONE [] [] [] [] (print_go_typ tyvars (#range const))) + | (false, false) => abstract_using aux_dom1 true (map snd aux_dom2 `--> #range const) o abstract_using aux_dom2 false (#range const) + | _ => abstract_using aux_dom1 false (#range const) o abstract_using aux_dom2 false (#range const) + in block [ + (str o Long_Name.base_name o deresolve_const) classparam, + str ":", Pretty.brk 1, + (wrap_aux o wrap_in_return o print_app false const_syntax tyvars (SOME thm) vars NOBR) + (const, map (IVar o SOME) auxs), + str "," + ] end; + in let + val body = block_enclose (concat [str "return", class_head, str "{"],str "}") + (superinsts_fields + @ map print_classparam_instance inst_params) + val head = print_func_head tyvars reserved (SOME sym) tyargs (print_dict_args tyvars vs) + [] [] class_head + in print_func head body end + end; + fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) = + print_go_func const_syntax reserved const vs ty (filter (snd o snd) raw_eqs) + | print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) = + print_go_typedef tyco vs cos reserved + | print_stmt (Type_Class sym, (_, Class class)) = + print_typeclass reserved sym class + | print_stmt (Class_Instance sym, (_, Instance instance)) = + print_instance reserved sym instance + | print_stmt (_, _) = str "" (*raise Fail "whatever this is, it's not yet supported";*) + in print_stmt + end; + + + +fun variant_capitalize s ctxt = + let + val cs = Symbol.explode s; + val s_lower = case cs of + c :: cs => Symbol.to_ascii_upper c :: cs + in ctxt + |> Name.variant (implode s_lower) + end; + +fun go_program_of_program ctxt module_name reserved identifiers exports program = + let + val variant = variant_capitalize + fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) = + let + val declare = Name.declare name_fragment; + in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end; + fun namify_common base ((nsp_class, nsp_object), nsp_common) = + let + val (base', nsp_common') = variant base nsp_common + in + (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) + end; + fun namify_stmt (Code_Thingol.Fun _) = namify_common + | namify_stmt (Code_Thingol.Datatype _) = namify_common + | namify_stmt (Code_Thingol.Datatypecons _) = namify_common + | namify_stmt (Code_Thingol.Class _) = namify_common + | namify_stmt (Code_Thingol.Classrel _) = namify_common + | namify_stmt (Code_Thingol.Classparam _) = namify_common + | namify_stmt (Code_Thingol.Classinst _) = namify_common; + + fun modify_stmt (_, (_, Code_Thingol.Fun (_, SOME _))) = NONE + | modify_stmt (_, (export, Code_Thingol.Fun (x, _))) = SOME (export, Fun x) + | modify_stmt (_, (export, Code_Thingol.Datatype x)) = SOME (export, Datatype x) + | modify_stmt (_, (_, Code_Thingol.Datatypecons _)) = NONE + | modify_stmt (Type_Class class, (export, Code_Thingol.Class x)) = + SOME (export, Class x) + | modify_stmt (_, (_, Code_Thingol.Classrel x)) = NONE + | modify_stmt (_, (_, Code_Thingol.Classparam x)) = NONE + | modify_stmt (_, (export, Code_Thingol.Classinst inst)) = + SOME (export, Instance inst); + in + Code_Namespace.hierarchical_program ctxt + { module_name = module_name, reserved = reserved, identifiers = identifiers, + empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, + namify_stmt = namify_stmt, cyclic_modules = false, + class_transitive = true, class_relation_public = true, empty_data = (), + memorize_data = K I, modify_stmts = map modify_stmt } + exports program + end; + + + + +fun serialize_go gen_stringer go_module undefineds infinite_types ctxt { module_name, reserved_syms, + identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports = + let + (* build program *) + val { deresolver, hierarchical_program = go_program } = + go_program_of_program ctxt module_name (Name.make_context reserved_syms) + identifiers exports program; + + val go_module = if go_module = "" then "isabelle/exported" else go_module; + + (* helper functions that need access to the entire program *) + fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco) + of Code_Thingol.Datatype (_, constrs) => + (AList.lookup (op = o apsnd fst) constrs constr) + | _ => NONE; + fun is_sum_type sym = case Code_Symbol.Graph.get_node program sym of + Code_Thingol.Datatypecons tyco => (case Code_Symbol.Graph.get_node program (Type_Constructor tyco) + of Code_Thingol.Datatype (_, []) => false + | Code_Thingol.Datatype (_, [_]) => false + | Code_Thingol.Datatype _ => true + | _ => false) + | _ => false; + + fun is_class_param (sym as Constant const) = case Code_Symbol.Graph.get_node program sym + of Code_Thingol.Classparam _ => true + | _ => false + fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class) + of Code_Thingol.Class (_, (_, classparams)) => classparams; + fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym + of Code_Thingol.Fun (((_, ty), []), _) => + (length o fst o Code_Thingol.unfold_fun) ty + | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts + | Code_Thingol.Datatypecons tyco => length (the (lookup_constr tyco const)) + | Code_Thingol.Classparam class => + (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) + (classparams_of_class class)) const; + (* print the go code *) + fun print_stmt prefix_fragments b = ("", print_go_stmt gen_stringer undefineds infinite_types + tyco_syntax const_syntax (make_vars reserved_syms) args_num is_sum_type is_class_param + (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver) b); + + fun get_imports module_name = Module module_name + |> Code_Symbol.Graph.immediate_succs go_program + |> map (fn (Module a) => a) + |> (curry op @) (map fst includes) + |> map (fn (a) => go_module ^ "/" ^ a) + + (* print modules *) + fun print_module _ base _ ps = (base, Pretty.chunks2 + (str ("package " ^ base) + :: block_enclose (str "import (", str ")") + (map (str o print_go_string) (get_imports base)) + :: (map snd ps) )) + + + (* serialization *) + val p = Code_Namespace.print_hierarchical { + print_module = print_module, print_stmt = print_stmt, + lift_markup = K I } go_program + |> curry (op @) includes + |> map (apfst (fn a => [a, "exported.go"])) + + val is_single_module = length p = 1 + in ( + if is_single_module + then Code_Target.Singleton ("go", snd (hd p)) + else Code_Target.Hierarchy ((["go.mod"], Pretty.chunks2 [ + concat [str "module",(str o print_go_string) go_module], + str "go 1.18" + ]) :: p), + try (deresolver []) + ) end; + + +val serializer : Code_Target.serializer = + Code_Target.parse_args ((Scan.optional (Args.$$$ "go_module" |-- Args.name) "" + -- Scan.optional (Args.$$$ "gen_stringer" >> K true) false + -- Scan.optional (Args.$$$ "panic_on" |-- (Scan.repeat Parse.term)) [] + -- Scan.optional (Args.$$$ "infinite_type" |-- (Scan.repeat Parse.term)) []) + >> (fn (((go_module, gen_stringer), undef_terms), infinite_types) => fn lthy => let + val undefineds = map (fst o dest_Const o Syntax.read_term lthy) undef_terms + val infinite_types = map (fst o dest_Type o Syntax.parse_typ lthy) infinite_types + in serialize_go gen_stringer go_module undefineds infinite_types lthy end)) + + +val _ = Theory.setup + (Code_Target.add_language + (target, { serializer = serializer, literals = literals, + check = { env_var = "ISABELLE_GO", + make_destination = fn p => p + Path.explode "export.go", + make_command = fn p => "test -d export.go && cd export.go && $ISABELLE_GO build ./"^p^" || $ISABELLE_GO build ./export.go"}, + evaluation_args = []}) + #> Code_Target.set_printings (Type_Constructor ("fun", + [(target, SOME (2, fn print_go_typ => fn fxy => fn [arg, rtyp] => let + val head = applify "(" ")" (print_go_typ fxy) NOBR (str "func") [arg]; + in concat [head, print_go_typ fxy rtyp] end) + )])) + #> fold (Code_Target.add_reserved target) [ + "any", "break", "default", "func", "interface", "select", "case", "defer", + "go", "map", "struct", "chan", "else", "goto", "package", "switch", + "const", "fallthrough", "if", "range", "type", "continue", "for", + "import", "return", "var" + ]); + + +end; (*struct*) diff --git a/thys/Go/document/root.tex b/thys/Go/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Go/document/root.tex @@ -0,0 +1,24 @@ +\documentclass[11pt,a4paper]{report} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{pdfsetup} +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Go Code Generation for Isabelle} +\author{Terru Stübinger, Lars Hupel} +\maketitle + +\begin{abstract} + This entry contains a standalone code generation target for the Go programming language. + Unlike the previous targets, Go is not a functional language and encourages code in an imperative style, thus many of the features of Isabelle's language (particularly data types, pattern matching, and type classes) have to be emulated using imperative language constructs in Go. + To generate Go code, users can simply import this entry, which makes the Go target available. +\end{abstract} + +\parindent 0pt\parskip 0.5ex + +\input{session} + +\end{document} diff --git a/thys/Go/test/quick/RBT_Test.thy b/thys/Go/test/quick/RBT_Test.thy new file mode 100644 --- /dev/null +++ b/thys/Go/test/quick/RBT_Test.thy @@ -0,0 +1,26 @@ +theory RBT_Test imports + "HOL-Data_Structures.RBT_Set" + "Go.Go_Setup" +begin + + + +definition t1 :: "integer rbt" where + "t1 = fold insert [1,2,3,4,5] empty" + +fun tree_from_list :: "'a::linorder list \ 'a rbt" where + "tree_from_list xs = fold insert xs empty" + +fun delete_list :: "'a::linorder list \ 'a rbt \ 'a rbt" where + "delete_list xs a = fold del xs a" + +fun trees_equal :: "'a::equal rbt \ 'a rbt \ bool" where + "trees_equal a b = (a = b)" + +export_code delete_list tree_from_list join invc trees_equal t1 in Go + module_name RbtTest + + +export_code delete_list tree_from_list join invc trees_equal t1 checking Go? + +end diff --git a/thys/Go/test/quick/export/Bigint/exported.go b/thys/Go/test/quick/export/Bigint/exported.go new file mode 100644 --- /dev/null +++ b/thys/Go/test/quick/export/Bigint/exported.go @@ -0,0 +1,66 @@ + +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 +} + diff --git a/thys/Go/test/quick/export/RbtTest/exported.go b/thys/Go/test/quick/export/RbtTest/exported.go new file mode 100644 --- /dev/null +++ b/thys/Go/test/quick/export/RbtTest/exported.go @@ -0,0 +1,1404 @@ +package RbtTest + +import ( + "isabelle/exported/Bigint" +) + +// sum type which can be Red, Black +type Color any; +type Red struct { }; +type Black struct { }; + + + +func Equal_colora (x0 Color, x1 Color) bool { + { + if x0 == (Color(Red{})) { + if x1 == (Color(Black{})) { + return false; + } + } + }; + { + if x0 == (Color(Black{})) { + if x1 == (Color(Red{})) { + return false; + } + } + }; + { + if x0 == (Color(Black{})) { + if x1 == (Color(Black{})) { + return true; + } + } + }; + { + if x0 == (Color(Red{})) { + if x1 == (Color(Red{})) { + return true; + } + } + }; + panic("match failed"); +} + +type Equal[a any] struct { + Equala func(a, a) bool +} + +func Equal_color () Equal[Color] { + return Equal[Color] { + Equala: func (A Color, Aa Color) bool { return Equal_colora(A, Aa); }, + } +} + +type Prod[a, b any] struct { A a; Aa b; }; +func Pair_dest[a, b any](p Prod[a, b])(a, b) { + return p.A, p.Aa; +} + +func Eq[a any] (a_ Equal[a], aa a, b a) bool { + return a_.Equala(aa, b); +} + +func Equal_proda[a, b any] (a_ Equal[a], b_ Equal[b], x0 Prod[a, b], x1 Prod[a, b]) bool { + { + _ = x0; + x1b, x2a := Pair_dest(x0); + _ = x1; + y1a, y2a := Pair_dest(x1); + return Eq[a](a_, x1b, y1a) && Eq[b](b_, x2a, y2a); + }; + panic("match failed"); +} + +func Equal_prod[a, b any] (a_ Equal[a], b_ Equal[b]) Equal[Prod[a, b]] { + return Equal[Prod[a, b]] { + Equala: func (A Prod[a, b], Aa Prod[a, b]) bool { return Equal_proda[a, b](a_, b_, A, Aa); }, + } +} + +func Equal_integer () Equal[Bigint.Int] { + return Equal[Bigint.Int] { + Equala: func (A Bigint.Int, Aa Bigint.Int) bool { return Bigint.Equal( A, Aa); }, + } +} + +type Ord[a any] struct { + Less_eq func(a, a) bool + Less func(a, a) bool +} + +func Ord_integer () Ord[Bigint.Int] { + return Ord[Bigint.Int] { + Less_eq: func (A Bigint.Int, Aa Bigint.Int) bool { return Bigint.Less_eq( A, Aa); }, + Less: func (A Bigint.Int, Aa Bigint.Int) bool { return Bigint.Less( A, Aa); }, + } +} + +type Preorder[a any] struct { + Ord_preorder Ord[a] +} + +type Order[a any] struct { + Preorder_order Preorder[a] +} + +func Preorder_integer () Preorder[Bigint.Int] { + return Preorder[Bigint.Int] { + Ord_preorder: Ord_integer(), + } +} + +func Order_integer () Order[Bigint.Int] { + return Order[Bigint.Int] { + Preorder_order: Preorder_integer(), + } +} + +type Linorder[a any] struct { + Order_linorder Order[a] +} + +func Linorder_integer () Linorder[Bigint.Int] { + return Linorder[Bigint.Int] { + Order_linorder: Order_integer(), + } +} + +// sum type which can be One, Bit0, Bit1 +type Num any; +type One struct { }; +type Bit0 struct { A Num; }; +type Bit1 struct { A Num; }; + +func Bit0_dest(p Bit0)(Num) { + return p.A +} +func Bit1_dest(p Bit1)(Num) { + return p.A +} + +// sum type which can be Nil, Cons +type List[a any] any; +type Nil[a any] struct { }; +type Cons[a any] struct { A a; Aa List[a]; }; + +func Cons_dest[a any](p Cons[a])(a, List[a]) { + return p.A, p.Aa +} + +// sum type which can be Leaf, Node +type Tree[a any] any; +type Leaf[a any] struct { }; +type Node[a any] struct { A Tree[a]; Aa a; Ab Tree[a]; }; + +func Node_dest[a any](p Node[a])(Tree[a], a, Tree[a]) { + return p.A, p.Aa, p.Ab +} + +// sum type which can be LT, EQ, GT +type Cmp_val any; +type LT struct { }; +type EQ struct { }; +type GT struct { }; + + + + +func Cmp[a any] (a1_ Equal[a], a2_ Linorder[a], x a, y a) Cmp_val { + target := a2_.Order_linorder.Preorder_order.Ord_preorder.Less(x, y); + { + if target == (true) { + return Cmp_val(LT{}); + } + }; + { + if target == (false) { + targeu := Eq[a](a1_, x, y); + { + if targeu == (true) { + return Cmp_val(EQ{}); + } + }; + { + if targeu == (false) { + return Cmp_val(GT{}); + } + }; + panic("match failed"); + } + }; + panic("match failed"); +} + +func Paint[a any] (c Color, x1 Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + if x1 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}); + } + }; + { + cb := c; + q, m := x1.(Node[Prod[a, Color]]); + if m { + la, p, ra := Node_dest(q); + _ = p; + ab, _ := Pair_dest(p); + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{la, Prod[a, Color]{ab, cb}, ra}); + } + }; + panic("match failed"); +} + +func BaliR[a any] (t1 Tree[Prod[a, Color]], aa a, x2 Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + t2a, q, p := Node_dest(q); + _ = q; + ba, d := Pair_dest(q); + if d == (Color(Red{})) { + r, m := p.(Node[Prod[a, Color]]); + if m { + t3a, r, t4a := Node_dest(r); + _ = r; + ca, e := Pair_dest(r); + if e == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, t2a}), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{ca, Color(Black{})}, t4a})}); + } + } + } + } + }; + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + q, p, d := Node_dest(q); + if d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + r, m := q.(Node[Prod[a, Color]]); + if m { + t2a, r, t3a := Node_dest(r); + _ = r; + ba, e := Pair_dest(r); + if e == (Color(Red{})) { + _ = p; + ca, f := Pair_dest(p); + if f == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, t2a}), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{ca, Color(Black{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})})}); + } + } + } + } + } + }; + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + r, q, p := Node_dest(q); + s, m := r.(Node[Prod[a, Color]]); + if m { + t2a, s, t3a := Node_dest(s); + _ = s; + ba, d := Pair_dest(s); + if d == (Color(Red{})) { + _ = q; + ca, e := Pair_dest(q); + if e == (Color(Red{})) { + t, m := p.(Node[Prod[a, Color]]); + if m { + va, t, vba := Node_dest(t); + _ = t; + vca, f := Pair_dest(t); + if f == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, t2a}), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{ca, Color(Black{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba})})}); + } + } + } + } + } + } + }; + { + t1b := t1; + ac := aa; + if x2 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}); + } + }; + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, c := Pair_dest(p); + if c == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba})}); + } + } + }; + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + d, vaa, c := Node_dest(q); + if d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) && c == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), vaa, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})})}); + } + } + }; + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + p, vaa, c := Node_dest(q); + if c == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + q, m := p.(Node[Prod[a, Color]]); + if m { + vba, q, vda := Node_dest(q); + _ = q; + vea, d := Pair_dest(q); + if d == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vba, Prod[a, Color]{vea, Color(Black{})}, vda}), vaa, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})})}); + } + } + } + } + }; + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + c, vaa, p := Node_dest(q); + if c == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + q, m := p.(Node[Prod[a, Color]]); + if m { + vca, q, vea := Node_dest(q); + _ = q; + vfa, d := Pair_dest(q); + if d == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), vaa, Tree[Prod[a, Color]](Node[Prod[a, Color]]{vca, Prod[a, Color]{vfa, Color(Black{})}, vea})})}); + } + } + } + } + }; + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + q, vaa, p := Node_dest(q); + r, m := q.(Node[Prod[a, Color]]); + if m { + vba, r, vga := Node_dest(r); + _ = r; + vha, c := Pair_dest(r); + if c == (Color(Black{})) { + s, m := p.(Node[Prod[a, Color]]); + if m { + vca, s, vea := Node_dest(s); + _ = s; + vfa, d := Pair_dest(s); + if d == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Black{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vba, Prod[a, Color]{vha, Color(Black{})}, vga}), vaa, Tree[Prod[a, Color]](Node[Prod[a, Color]]{vca, Prod[a, Color]{vfa, Color(Black{})}, vea})})}); + } + } + } + } + } + }; + panic("match failed"); +} + +func BaldL[a any] (x0 Tree[Prod[a, Color]], b a, t3 Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + t1a, p, t2a := Node_dest(q); + _ = p; + ab, c := Pair_dest(p); + if c == (Color(Red{})) { + bb := b; + t3b := t3; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1a, Prod[a, Color]{ab, Color(Black{})}, t2a}), Prod[a, Color]{bb, Color(Red{})}, t3b}); + } + } + }; + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + t2a, p, t3b := Node_dest(q); + _ = p; + bb, c := Pair_dest(p); + if c == (Color(Black{})) { + return BaliR[a](Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), ab, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t2a, Prod[a, Color]{bb, Color(Red{})}, t3b})); + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, c := Pair_dest(p); + if c == (Color(Black{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + t2a, q, t3b := Node_dest(q); + _ = q; + bb, d := Pair_dest(q); + if d == (Color(Black{})) { + return BaliR[a](Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), ab, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t2a, Prod[a, Color]{bb, Color(Red{})}, t3b})); + } + } + } + } + }; + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + q, p, t4a := Node_dest(q); + r, m := q.(Node[Prod[a, Color]]); + if m { + t2a, r, t3b := Node_dest(r); + _ = r; + bb, d := Pair_dest(r); + if d == (Color(Black{})) { + _ = p; + ca, e := Pair_dest(p); + if e == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ab, Color(Black{})}, t2a}), Prod[a, Color]{bb, Color(Red{})}, BaliR[a](t3b, ca, Paint[a](Color(Red{}), t4a))}); + } + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, d := Pair_dest(p); + if d == (Color(Black{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + r, q, t4a := Node_dest(q); + s, m := r.(Node[Prod[a, Color]]); + if m { + t2a, s, t3b := Node_dest(s); + _ = s; + bb, e := Pair_dest(s); + if e == (Color(Black{})) { + _ = q; + ca, f := Pair_dest(q); + if f == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Black{})}, t2a}), Prod[a, Color]{bb, Color(Red{})}, BaliR[a](t3b, ca, Paint[a](Color(Red{}), t4a))}); + } + } + } + } + } + } + }; + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ab := b; + if t3 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}); + } + } + }; + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + c, p, vba := Node_dest(q); + if c == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + _ = p; + vca, d := Pair_dest(p); + if d == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{vca, Color(Red{})}, vba})}); + } + } + } + } + }; + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + q, p, vba := Node_dest(q); + r, m := q.(Node[Prod[a, Color]]); + if m { + vaa, r, vea := Node_dest(r); + _ = r; + vfa, c := Pair_dest(r); + if c == (Color(Red{})) { + _ = p; + vca, d := Pair_dest(p); + if d == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vaa, Prod[a, Color]{vfa, Color(Red{})}, vea}), Prod[a, Color]{vca, Color(Red{})}, vba})}); + } + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, c := Pair_dest(p); + if c == (Color(Black{})) { + ab := b; + if t3 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}); + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, c := Pair_dest(p); + if c == (Color(Black{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + d, q, vea := Node_dest(q); + if d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + _ = q; + vfa, e := Pair_dest(q); + if e == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{vfa, Color(Red{})}, vea})}); + } + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, c := Pair_dest(p); + if c == (Color(Black{})) { + ab := b; + q, m := t3.(Node[Prod[a, Color]]); + if m { + r, q, vea := Node_dest(q); + s, m := r.(Node[Prod[a, Color]]); + if m { + vda, s, vha := Node_dest(s); + _ = s; + via, d := Pair_dest(s); + if d == (Color(Red{})) { + _ = q; + vfa, e := Pair_dest(q); + if e == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vda, Prod[a, Color]{via, Color(Red{})}, vha}), Prod[a, Color]{vfa, Color(Red{})}, vea})}); + } + } + } + } + } + } + }; + panic("match failed"); +} + +func Join[a any] (x0 Tree[Prod[a, Color]], t Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + tb := t; + return tb; + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + vc, vaa, vba := Node_dest(q); + if t == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{vc, vaa, vba}); + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + t1a, p, t2a := Node_dest(q); + _ = p; + ab, d := Pair_dest(p); + if d == (Color(Red{})) { + q, m := t.(Node[Prod[a, Color]]); + if m { + t3a, q, t4a := Node_dest(q); + _ = q; + ca, e := Pair_dest(q); + if e == (Color(Red{})) { + target := Join[a](t2a, t3a); + { + if target == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1a, Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ca, Color(Red{})}, t4a})}); + } + }; + { + r, m := target.(Node[Prod[a, Color]]); + if m { + u2, r, u3 := Node_dest(r); + _ = r; + b, f := Pair_dest(r); + if f == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1a, Prod[a, Color]{ab, Color(Red{})}, u2}), Prod[a, Color]{b, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{u3, Prod[a, Color]{ca, Color(Red{})}, t4a})}); + } + } + }; + { + r, m := target.(Node[Prod[a, Color]]); + if m { + u2, r, u3 := Node_dest(r); + _ = r; + b, f := Pair_dest(r); + if f == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1a, Prod[a, Color]{ab, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{u2, Prod[a, Color]{b, Color(Black{})}, u3}), Prod[a, Color]{ca, Color(Red{})}, t4a})}); + } + } + }; + panic("match failed"); + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + t1a, p, t2a := Node_dest(q); + _ = p; + ab, d := Pair_dest(p); + if d == (Color(Black{})) { + q, m := t.(Node[Prod[a, Color]]); + if m { + t3a, q, t4a := Node_dest(q); + _ = q; + ca, e := Pair_dest(q); + if e == (Color(Black{})) { + target := Join[a](t2a, t3a); + { + if target == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return BaldL[a](t1a, ab, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ca, Color(Black{})}, t4a})); + } + }; + { + r, m := target.(Node[Prod[a, Color]]); + if m { + u2, r, u3 := Node_dest(r); + _ = r; + b, f := Pair_dest(r); + if f == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1a, Prod[a, Color]{ab, Color(Black{})}, u2}), Prod[a, Color]{b, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{u3, Prod[a, Color]{ca, Color(Black{})}, t4a})}); + } + } + }; + { + r, m := target.(Node[Prod[a, Color]]); + if m { + u2, r, u3 := Node_dest(r); + _ = r; + b, f := Pair_dest(r); + if f == (Color(Black{})) { + return BaldL[a](t1a, ab, Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{u2, Prod[a, Color]{b, Color(Black{})}, u3}), Prod[a, Color]{ca, Color(Black{})}, t4a})); + } + } + }; + panic("match failed"); + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, c := Pair_dest(p); + if c == (Color(Black{})) { + q, m := t.(Node[Prod[a, Color]]); + if m { + t2a, q, t3a := Node_dest(q); + _ = q; + ab, d := Pair_dest(q); + if d == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Join[a](Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), t2a), Prod[a, Color]{ab, Color(Red{})}, t3a}); + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + t1a, p, t2a := Node_dest(q); + _ = p; + ab, c := Pair_dest(p); + if c == (Color(Red{})) { + q, m := t.(Node[Prod[a, Color]]); + if m { + va, q, vba := Node_dest(q); + _ = q; + vca, d := Pair_dest(q); + if d == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1a, Prod[a, Color]{ab, Color(Red{})}, Join[a](t2a, Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}))}); + } + } + } + } + }; + panic("match failed"); +} + +func Fold[a, b any] (f func(a) func(b) b, x1 List[a], s b) b { + { + fb := f; + q, m := x1.(Cons[a]); + if m { + xa, xsa := Cons_dest(q); + sb := s; + return Fold[a, b](fb, xsa, ((fb(xa))(sb))); + } + }; + { + if x1 == (List[a](Nil[a]{})) { + sb := s; + return sb; + } + }; + panic("match failed"); +} + +func BaliL[a any] (x0 Tree[Prod[a, Color]], c a, t4 Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + q, p, t3a := Node_dest(q); + r, m := q.(Node[Prod[a, Color]]); + if m { + t1a, r, t2a := Node_dest(r); + _ = r; + ab, d := Pair_dest(r); + if d == (Color(Red{})) { + _ = p; + ba, e := Pair_dest(p); + if e == (Color(Red{})) { + cb := c; + t4b := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1a, Prod[a, Color]{ab, Color(Black{})}, t2a}), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{cb, Color(Black{})}, t4b})}); + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + d, q, p := Node_dest(q); + if d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + _ = q; + ab, e := Pair_dest(q); + if e == (Color(Red{})) { + r, m := p.(Node[Prod[a, Color]]); + if m { + t2a, r, t3a := Node_dest(r); + _ = r; + ba, f := Pair_dest(r); + if f == (Color(Red{})) { + cb := c; + t4b := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ab, Color(Black{})}, t2a}), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{cb, Color(Black{})}, t4b})}); + } + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + r, q, p := Node_dest(q); + s, m := r.(Node[Prod[a, Color]]); + if m { + va, s, vba := Node_dest(s); + _ = s; + vca, d := Pair_dest(s); + if d == (Color(Black{})) { + _ = q; + ab, e := Pair_dest(q); + if e == (Color(Red{})) { + t, m := p.(Node[Prod[a, Color]]); + if m { + t2a, t, t3a := Node_dest(t); + _ = t; + ba, f := Pair_dest(t); + if f == (Color(Red{})) { + cb := c; + t4b := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Black{})}, t2a}), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{cb, Color(Black{})}, t4b})}); + } + } + } + } + } + } + }; + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + d, p, vba := Node_dest(q); + if d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + _ = p; + va, e := Pair_dest(p); + if e == (Color(Black{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{va, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + e, vaa, d := Node_dest(q); + if e == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) && d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), vaa, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + d, vaa, p := Node_dest(q); + if d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + q, m := p.(Node[Prod[a, Color]]); + if m { + vb, q, vda := Node_dest(q); + _ = q; + vea, e := Pair_dest(q); + if e == (Color(Black{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), vaa, Tree[Prod[a, Color]](Node[Prod[a, Color]]{vb, Prod[a, Color]{vea, Color(Black{})}, vda})}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + q, p, vba := Node_dest(q); + r, m := q.(Node[Prod[a, Color]]); + if m { + vca, r, vea := Node_dest(r); + _ = r; + vfa, d := Pair_dest(r); + if d == (Color(Black{})) { + _ = p; + va, e := Pair_dest(p); + if e == (Color(Black{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vca, Prod[a, Color]{vfa, Color(Black{})}, vea}), Prod[a, Color]{va, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + p, vaa, d := Node_dest(q); + if d == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + q, m := p.(Node[Prod[a, Color]]); + if m { + vca, q, vea := Node_dest(q); + _ = q; + vfa, e := Pair_dest(q); + if e == (Color(Black{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vca, Prod[a, Color]{vfa, Color(Black{})}, vea}), vaa, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + q, vaa, p := Node_dest(q); + r, m := q.(Node[Prod[a, Color]]); + if m { + vca, r, vea := Node_dest(r); + _ = r; + vfa, d := Pair_dest(r); + if d == (Color(Black{})) { + s, m := p.(Node[Prod[a, Color]]); + if m { + vb, s, vga := Node_dest(s); + _ = s; + vha, e := Pair_dest(s); + if e == (Color(Black{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vca, Prod[a, Color]{vfa, Color(Black{})}, vea}), vaa, Tree[Prod[a, Color]](Node[Prod[a, Color]]{vb, Prod[a, Color]{vha, Color(Black{})}, vga})}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + } + } + } + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, d := Pair_dest(p); + if d == (Color(Black{})) { + ab := c; + t2a := t4; + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba}), Prod[a, Color]{ab, Color(Black{})}, t2a}); + } + } + }; + panic("match failed"); +} + +func BaldR[a any] (t1 Tree[Prod[a, Color]], aa a, x2 Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + t1b := t1; + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + t2a, p, t3a := Node_dest(q); + _ = p; + ba, c := Pair_dest(p); + if c == (Color(Red{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t2a, Prod[a, Color]{ba, Color(Black{})}, t3a})}); + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + t1b, p, t2a := Node_dest(q); + _ = p; + ac, c := Pair_dest(p); + if c == (Color(Black{})) { + ba := aa; + if x2 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return BaliL[a](Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Red{})}, t2a}), ba, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})); + } + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + t1b, p, t2a := Node_dest(q); + _ = p; + ac, c := Pair_dest(p); + if c == (Color(Black{})) { + ba := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + va, q, vba := Node_dest(q); + _ = q; + vca, d := Pair_dest(q); + if d == (Color(Black{})) { + return BaliL[a](Tree[Prod[a, Color]](Node[Prod[a, Color]]{t1b, Prod[a, Color]{ac, Color(Red{})}, t2a}), ba, Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba})); + } + } + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + t1b, q, p := Node_dest(q); + _ = q; + ac, d := Pair_dest(q); + if d == (Color(Red{})) { + r, m := p.(Node[Prod[a, Color]]); + if m { + t2a, r, t3a := Node_dest(r); + _ = r; + ba, e := Pair_dest(r); + if e == (Color(Black{})) { + ca := aa; + if x2 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{BaliL[a](Paint[a](Color(Red{}), t1b), ac, t2a), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{ca, Color(Black{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})})}); + } + } + } + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + t1b, q, p := Node_dest(q); + _ = q; + ac, d := Pair_dest(q); + if d == (Color(Red{})) { + r, m := p.(Node[Prod[a, Color]]); + if m { + t2a, r, t3a := Node_dest(r); + _ = r; + ba, e := Pair_dest(r); + if e == (Color(Black{})) { + ca := aa; + s, m := x2.(Node[Prod[a, Color]]); + if m { + va, s, vba := Node_dest(s); + _ = s; + vca, f := Pair_dest(s); + if f == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{BaliL[a](Paint[a](Color(Red{}), t1b), ac, t2a), Prod[a, Color]{ba, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{t3a, Prod[a, Color]{ca, Color(Black{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba})})}); + } + } + } + } + } + } + }; + { + if t1 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ac := aa; + if x2 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ac, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}); + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + va, p, c := Node_dest(q); + if c == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + _ = p; + vca, d := Pair_dest(p); + if d == (Color(Red{})) { + ac := aa; + if x2 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}), Prod[a, Color]{ac, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}); + } + } + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + vb, q, p := Node_dest(q); + _ = q; + vca, c := Pair_dest(q); + if c == (Color(Red{})) { + r, m := p.(Node[Prod[a, Color]]); + if m { + vaa, r, vea := Node_dest(r); + _ = r; + vfa, d := Pair_dest(r); + if d == (Color(Red{})) { + ac := aa; + if x2 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vb, Prod[a, Color]{vca, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{vaa, Prod[a, Color]{vfa, Color(Red{})}, vea})}), Prod[a, Color]{ac, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}); + } + } + } + } + } + }; + { + if t1 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + va, p, vba := Node_dest(q); + _ = p; + vca, c := Pair_dest(p); + if c == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{ac, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{va, Prod[a, Color]{vca, Color(Black{})}, vba})}); + } + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + vaa, p, c := Node_dest(q); + if c == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + _ = p; + vfa, d := Pair_dest(p); + if d == (Color(Red{})) { + ac := aa; + q, m := x2.(Node[Prod[a, Color]]); + if m { + vd, q, vba := Node_dest(q); + _ = q; + vca, e := Pair_dest(q); + if e == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vaa, Prod[a, Color]{vfa, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}), Prod[a, Color]{ac, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{vd, Prod[a, Color]{vca, Color(Black{})}, vba})}); + } + } + } + } + } + }; + { + q, m := t1.(Node[Prod[a, Color]]); + if m { + vaa, q, p := Node_dest(q); + _ = q; + vfa, c := Pair_dest(q); + if c == (Color(Red{})) { + r, m := p.(Node[Prod[a, Color]]); + if m { + vda, r, vha := Node_dest(r); + _ = r; + via, d := Pair_dest(r); + if d == (Color(Red{})) { + ac := aa; + s, m := x2.(Node[Prod[a, Color]]); + if m { + ve, s, vba := Node_dest(s); + _ = s; + vca, e := Pair_dest(s); + if e == (Color(Black{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Node[Prod[a, Color]]{vaa, Prod[a, Color]{vfa, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{vda, Prod[a, Color]{via, Color(Red{})}, vha})}), Prod[a, Color]{ac, Color(Red{})}, Tree[Prod[a, Color]](Node[Prod[a, Color]]{ve, Prod[a, Color]{vca, Color(Black{})}, vba})}); + } + } + } + } + } + } + }; + panic("match failed"); +} + +func Equal_tree[a any] (a_ Equal[a], x0 Tree[a], x1 Tree[a]) bool { + { + if x0 == (Tree[a](Leaf[a]{})) { + _, m := x1.(Node[a]); + if m { + return false; + } + } + }; + { + _, m := x0.(Node[a]); + if m { + if x1 == (Tree[a](Leaf[a]{})) { + return false; + } + } + }; + { + q, m := x0.(Node[a]); + if m { + x21a, x22a, x23a := Node_dest(q); + q, m := x1.(Node[a]); + if m { + y21a, y22a, y23a := Node_dest(q); + return Equal_tree[a](a_, x21a, y21a) && (Eq[a](a_, x22a, y22a) && Equal_tree[a](a_, x23a, y23a)); + } + } + }; + { + if x0 == (Tree[a](Leaf[a]{})) { + if x1 == (Tree[a](Leaf[a]{})) { + return true; + } + } + }; + panic("match failed"); +} + +func Colora[a any] (x0 Tree[Prod[a, Color]]) Color { + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Color(Black{}); + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + _, p, _ := Node_dest(q); + _ = p; + _, ca := Pair_dest(p); + return ca; + } + }; + panic("match failed"); +} + +func Del[a any] (a1_ Equal[a], a2_ Linorder[a], x a, xa1 Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + if xa1 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}); + } + }; + { + xb := x; + q, m := xa1.(Node[Prod[a, Color]]); + if m { + la, p, ra := Node_dest(q); + _ = p; + ab, _ := Pair_dest(p); + target := Cmp[a](a1_, a2_, xb, ab); + { + if target == (Cmp_val(LT{})) { + targeu := ! Equal_tree[Prod[a, Color]](Equal_prod[a, Color](a1_, Equal_color()), la, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) && Equal_colora(Colora[a](la), Color(Black{})); + { + if targeu == (true) { + return BaldL[a](Del[a](a1_, a2_, xb, la), ab, ra); + } + }; + { + if targeu == (false) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Del[a](a1_, a2_, xb, la), Prod[a, Color]{ab, Color(Red{})}, ra}); + } + }; + panic("match failed"); + } + }; + { + if target == (Cmp_val(EQ{})) { + return Join[a](la, ra); + } + }; + { + if target == (Cmp_val(GT{})) { + targeu := ! Equal_tree[Prod[a, Color]](Equal_prod[a, Color](a1_, Equal_color()), ra, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) && Equal_colora(Colora[a](ra), Color(Black{})); + { + if targeu == (true) { + return BaldR[a](la, ab, Del[a](a1_, a2_, xb, ra)); + } + }; + { + if targeu == (false) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{la, Prod[a, Color]{ab, Color(Red{})}, Del[a](a1_, a2_, xb, ra)}); + } + }; + panic("match failed"); + } + }; + panic("match failed"); + } + }; + panic("match failed"); +} + +func Ins[a any] (a1_ Equal[a], a2_ Linorder[a], x a, xa1 Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + { + xb := x; + if xa1 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}), Prod[a, Color]{xb, Color(Red{})}, Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})}); + } + }; + { + xb := x; + q, m := xa1.(Node[Prod[a, Color]]); + if m { + la, p, ra := Node_dest(q); + _ = p; + ab, c := Pair_dest(p); + if c == (Color(Black{})) { + target := Cmp[a](a1_, a2_, xb, ab); + { + if target == (Cmp_val(LT{})) { + return BaliL[a](Ins[a](a1_, a2_, xb, la), ab, ra); + } + }; + { + if target == (Cmp_val(EQ{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{la, Prod[a, Color]{ab, Color(Black{})}, ra}); + } + }; + { + if target == (Cmp_val(GT{})) { + return BaliR[a](la, ab, Ins[a](a1_, a2_, xb, ra)); + } + }; + panic("match failed"); + } + } + }; + { + xb := x; + q, m := xa1.(Node[Prod[a, Color]]); + if m { + la, p, ra := Node_dest(q); + _ = p; + ab, c := Pair_dest(p); + if c == (Color(Red{})) { + target := Cmp[a](a1_, a2_, xb, ab); + { + if target == (Cmp_val(LT{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{Ins[a](a1_, a2_, xb, la), Prod[a, Color]{ab, Color(Red{})}, ra}); + } + }; + { + if target == (Cmp_val(EQ{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{la, Prod[a, Color]{ab, Color(Red{})}, ra}); + } + }; + { + if target == (Cmp_val(GT{})) { + return Tree[Prod[a, Color]](Node[Prod[a, Color]]{la, Prod[a, Color]{ab, Color(Red{})}, Ins[a](a1_, a2_, xb, ra)}); + } + }; + panic("match failed"); + } + } + }; + panic("match failed"); +} + +func Insert[a any] (a1_ Equal[a], a2_ Linorder[a], x a, t Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + return Paint[a](Color(Black{}), Ins[a](a1_, a2_, x, t)); +} + +func Empty[a any] () Tree[Prod[a, Color]] { + return Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{}); +} + +func T1 () Tree[Prod[Bigint.Int, Color]] { + return Fold[Bigint.Int, Tree[Prod[Bigint.Int, Color]]](func (a Bigint.Int) func(Tree[Prod[Bigint.Int, Color]]) Tree[Prod[Bigint.Int, Color]] { return func (b Tree[Prod[Bigint.Int, Color]]) Tree[Prod[Bigint.Int, Color]] { return Insert[Bigint.Int](Equal_integer(), Linorder_integer(), a, b); }; }, List[Bigint.Int](Cons[Bigint.Int]{Bigint.MkInt("1"), List[Bigint.Int](Cons[Bigint.Int]{Bigint.MkInt("2"), List[Bigint.Int](Cons[Bigint.Int]{Bigint.MkInt("3"), List[Bigint.Int](Cons[Bigint.Int]{Bigint.MkInt("4"), List[Bigint.Int](Cons[Bigint.Int]{Bigint.MkInt("5"), List[Bigint.Int](Nil[Bigint.Int]{})})})})})}), Empty[Bigint.Int]()); +} + +func Invc[a any] (x0 Tree[Prod[a, Color]]) bool { + { + if x0 == (Tree[Prod[a, Color]](Leaf[Prod[a, Color]]{})) { + return true; + } + }; + { + q, m := x0.(Node[Prod[a, Color]]); + if m { + la, p, ra := Node_dest(q); + _ = p; + _, ca := Pair_dest(p); + return (!(Equal_colora(ca, Color(Red{}))) || Equal_colora(Colora[a](la), Color(Black{})) && Equal_colora(Colora[a](ra), Color(Black{}))) && (Invc[a](la) && Invc[a](ra)); + } + }; + panic("match failed"); +} + +func Delete_list[a any] (a1_ Equal[a], a2_ Linorder[a], xs List[a], aa Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { + return Fold[a, Tree[Prod[a, Color]]](func (ab a) func(Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { return func (b Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { return Del[a](a1_, a2_, ab, b); }; }, xs, aa); +} + +func Trees_equal[a any] (a_ Equal[a], aa Tree[Prod[a, Color]], b Tree[Prod[a, Color]]) bool { + return Equal_tree[Prod[a, Color]](Equal_prod[a, Color](a_, Equal_color()), aa, b); +} + +func Tree_from_list[a any] (a1_ Equal[a], a2_ Linorder[a], xs List[a]) Tree[Prod[a, Color]] { + return Fold[a, Tree[Prod[a, Color]]](func (aa a) func(Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { return func (b Tree[Prod[a, Color]]) Tree[Prod[a, Color]] { return Insert[a](a1_, a2_, aa, b); }; }, xs, Empty[a]()); +} diff --git a/thys/Go/test/quick/export/go.mod b/thys/Go/test/quick/export/go.mod new file mode 100644 --- /dev/null +++ b/thys/Go/test/quick/export/go.mod @@ -0,0 +1,3 @@ +module "isabelle/exported" + +go 1.18 diff --git a/thys/Go/test/quick/go/Bigint b/thys/Go/test/quick/go/Bigint new file mode 120000 --- /dev/null +++ b/thys/Go/test/quick/go/Bigint @@ -0,0 +1,1 @@ +../export/Bigint/ \ No newline at end of file diff --git a/thys/Go/test/quick/go/Interface/rbt.go b/thys/Go/test/quick/go/Interface/rbt.go new file mode 100644 --- /dev/null +++ b/thys/Go/test/quick/go/Interface/rbt.go @@ -0,0 +1,42 @@ +package rbt + +import "isabelle/exported/RbtTest" + +var T1 = RbtTest.T1() + +var LinorderInt = RbtTest.Linorder_integer() +var EqualInt = RbtTest.Equal_integer() + +func EmptyTree[a any]() RbtTest.Tree[RbtTest.Prod[a, RbtTest.Color]] { + return RbtTest.Empty[a]() +} + +func JoinAndCheck[a any](a_ RbtTest.Linorder[a], x, y RbtTest.Tree[RbtTest.Prod[a, RbtTest.Color]]) (RbtTest.Tree[RbtTest.Prod[a, RbtTest.Color]], bool) { + b := RbtTest.Join(x, y) + ok := RbtTest.Invc(b) + return b, ok +} + +func DelAndCheck[a any](eq RbtTest.Equal[a], lin RbtTest.Linorder[a], list RbtTest.List[a], x RbtTest.Tree[RbtTest.Prod[a, RbtTest.Color]]) (RbtTest.Tree[RbtTest.Prod[a, RbtTest.Color]], bool) { + b := RbtTest.Delete_list(eq, lin, list, x) + ok := RbtTest.Invc(b) + return b, ok +} + +func TreeFromList[a any](eq RbtTest.Equal[a], lin RbtTest.Linorder[a], xs RbtTest.List[a]) (RbtTest.Tree[RbtTest.Prod[a, RbtTest.Color]], bool) { + tree := RbtTest.Tree_from_list(eq, lin, xs) + ok := RbtTest.Invc(tree) + return tree, ok +} + +func MkList[a any](vec []a) RbtTest.List[a] { + list := RbtTest.List[a](RbtTest.Nil[a]{}) + for _, v := range vec { + list = RbtTest.List[a](RbtTest.Cons[a]{v, list}) + } + return list +} + +func TreesEqual[a any](eq RbtTest.Equal[a], x, y RbtTest.Tree[RbtTest.Prod[a, RbtTest.Color]]) bool { + return RbtTest.Trees_equal(eq, x, y) +} diff --git a/thys/Go/test/quick/go/Interface/rbt_test.go b/thys/Go/test/quick/go/Interface/rbt_test.go new file mode 100644 --- /dev/null +++ b/thys/Go/test/quick/go/Interface/rbt_test.go @@ -0,0 +1,90 @@ +package rbt + +import ( + "reflect" + "testing" + + "isabelle/exported/Bigint" + "isabelle/exported/RbtTest" +) + +type RBTBigInt = RbtTest.Prod[Bigint.Int, RbtTest.Color] + +func TestTreeFromList(t *testing.T) { + array := [5]Bigint.Int{Bigint.MkInt("1"), Bigint.MkInt("2"), Bigint.MkInt("3"), Bigint.MkInt("4"), Bigint.MkInt("5")} + elements := MkList(array[:]) + + got, ok := TreeFromList(EqualInt, LinorderInt, elements) + if !ok { + t.Fatal("new tree does not satisfy invariant") + } + + want := RbtTest.Node[RBTBigInt]{ + A: RbtTest.Node[RBTBigInt]{ + A: RbtTest.Node[RBTBigInt]{ + A: RbtTest.Leaf[RBTBigInt]{}, + Aa: RBTBigInt{A: Bigint.MkInt("1"), + Aa: RbtTest.Black{}, + }, + Ab: RbtTest.Leaf[RBTBigInt]{}, + }, + Aa: RBTBigInt{ + A: Bigint.MkInt("2"), + Aa: RbtTest.Red{}, + }, + Ab: RbtTest.Node[RBTBigInt]{ + A: RbtTest.Leaf[RBTBigInt]{}, + Aa: RBTBigInt{A: Bigint.MkInt("3"), + Aa: RbtTest.Black{}}, + Ab: RbtTest.Leaf[RBTBigInt]{}, + }, + }, + Aa: RBTBigInt{ + A: Bigint.MkInt("4"), + Aa: RbtTest.Black{}, + }, + Ab: RbtTest.Node[RBTBigInt]{ + A: RbtTest.Leaf[RBTBigInt]{}, + Aa: RBTBigInt{ + A: Bigint.MkInt("5"), + Aa: RbtTest.Black{}, + }, + Ab: RbtTest.Leaf[RBTBigInt]{}, + }, + } + + if !reflect.DeepEqual(got, want) { + t.Fatalf("got tree does not equal want tree") + } +} + +func TestJoinAndCheck(t *testing.T) { + list := MkList([]Bigint.Int{Bigint.MkInt("1"), Bigint.MkInt("2"), Bigint.MkInt("3"), Bigint.MkInt("4"), Bigint.MkInt("5")}) + + tree, ok := TreeFromList(EqualInt, LinorderInt, list) + if !ok { + t.Fatal("new tree does not satisfy invariant") + } + _, ok = JoinAndCheck(LinorderInt, tree, tree) + if !ok { + t.Fatal("joining trees violated invariant") + } +} + +func TestDelAndCheck(t *testing.T) { + list := MkList([]Bigint.Int{Bigint.MkInt("1"), Bigint.MkInt("2"), Bigint.MkInt("3"), Bigint.MkInt("4"), Bigint.MkInt("5")}) + + tree, ok := TreeFromList(EqualInt, LinorderInt, list) + if !ok { + t.Fatal("new tree does not satisfy invariant") + } + got, ok := DelAndCheck(EqualInt, LinorderInt, list, tree) + if !ok { + t.Fatal("deletion violated invariant") + } + want := EmptyTree[Bigint.Int]() + ok = TreesEqual(EqualInt, got, want) + if !ok { + t.Fatal("tree not empty after deletion") + } +} diff --git a/thys/Go/test/quick/go/RbtTest b/thys/Go/test/quick/go/RbtTest new file mode 120000 --- /dev/null +++ b/thys/Go/test/quick/go/RbtTest @@ -0,0 +1,1 @@ +../export/RbtTest \ No newline at end of file diff --git a/thys/Go/test/quick/go/go.mod b/thys/Go/test/quick/go/go.mod new file mode 100644 --- /dev/null +++ b/thys/Go/test/quick/go/go.mod @@ -0,0 +1,3 @@ +module "isabelle/exported" + +go 1.18 diff --git a/thys/Go/test/slow/Candidates.thy b/thys/Go/test/slow/Candidates.thy new file mode 100644 --- /dev/null +++ b/thys/Go/test/slow/Candidates.thy @@ -0,0 +1,82 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +section \A huge collection of equations to generate code from\ + +theory Candidates +imports + Complex_Main + "HOL-Library.Library" + "HOL-Library.Sorting_Algorithms" + "HOL-Library.Subseq_Order" + "HOL-Library.RBT" + "HOL-Data_Structures.Tree_Map" + "HOL-Data_Structures.Tree_Set" + "HOL-Computational_Algebra.Computational_Algebra" + "HOL-Computational_Algebra.Polynomial_Factorial" + "HOL-Number_Theory.Eratosthenes" + "HOL-Examples.Records" + "HOL-Examples.Gauss_Numbers" +begin + +text \Drop technical stuff from \<^theory>\HOL.Quickcheck_Narrowing\ which is tailored towards Haskell\ + +setup \ +fn thy => +let + val tycos = Sign.logical_types thy; + val consts = map_filter (try (curry (Axclass.param_of_inst thy) + \<^const_name>\Quickcheck_Narrowing.partial_term_of\)) tycos; +in fold Code.declare_unimplemented_global consts thy end +\ + +text \Simple example for the predicate compiler.\ + +inductive sublist :: "'a list \ 'a list \ bool" +where + empty: "sublist [] xs" +| drop: "sublist ys xs \ sublist ys (x # xs)" +| take: "sublist ys xs \ sublist (x # ys) (x # xs)" + +code_pred sublist . + +text \Avoid popular infix.\ + +code_reserved SML upto + +text \Explicit check in \OCaml\ for correct precedence of let expressions in list expressions\ + +definition funny_list :: "bool list" +where + "funny_list = [let b = True in b, False]" + +definition funny_list' :: "bool list" +where + "funny_list' = funny_list" + +lemma [code]: + "funny_list' = [True, False]" + by (simp add: funny_list_def funny_list'_def) + +definition check_list :: unit +where + "check_list = (if funny_list = funny_list' then () else undefined)" + +text \Explicit check in \Scala\ for correct bracketing of abstractions\ + +definition funny_funs :: "(bool \ bool) list \ (bool \ bool) list" +where + "funny_funs fs = (\x. x \ True) # (\x. x \ False) # fs" + +(* +text \Explicit checks for strings etc.\ + +definition \hello = ''Hello, world!''\ + +definition \hello2 = String.explode (String.implode hello)\ + +definition \which_hello \ hello \ hello2\ +*) + +declare [[code abort: String.literal_of_asciis String.asciis_of_literal]] + +end diff --git a/thys/Go/test/slow/Generate.thy b/thys/Go/test/slow/Generate.thy new file mode 100644 --- /dev/null +++ b/thys/Go/test/slow/Generate.thy @@ -0,0 +1,21 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +section \Pervasive test of code generator\ + +theory Generate +imports + "Candidates" + "HOL-Library.AList_Mapping" + "HOL-Library.Finite_Lattice" + "Go.Go_Setup" +begin + +text \ + If any of the checks fails, inspect the code generated + by a corresponding \export_code\ command. +\ + + +export_code _ checking Go? (infinite_type "stream") + +end diff --git a/thys/Go/test/slow/Generate_Binary_Nat.thy b/thys/Go/test/slow/Generate_Binary_Nat.thy new file mode 100644 --- /dev/null +++ b/thys/Go/test/slow/Generate_Binary_Nat.thy @@ -0,0 +1,14 @@ +theory Generate_Binary_Nat +imports + "Candidates" + "HOL-Library.AList_Mapping" + "HOL-Library.Finite_Lattice" + "HOL-Library.Code_Binary_Nat" + "Go.Go_Setup" +begin + + + +export_code _ checking Go? (infinite_type "stream") + +end diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,804 +1,805 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel Concentration_Inequalities CRDT CRYSTALS-Kyber CRYSTALS-Kyber_Security CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cardinality_Continuum Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Catoids Cauchy Cayley_Hamilton Certification_Monads Ceva Chandy_Lamport Chebyshev_Polynomials Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots Coupledsim_Contrasim CryptHOL CryptoBasedCompositionalProperties Crypto_Standards CubicalCategories Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation Disintegration DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Earley_Parser Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elimination_Of_Repeated_Factors Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Euler_Polyhedron_Formula Eudoxus_Reals Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Fixed_Length_Vector Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops +Go GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOL-CSPM HOL-CSP_OpSem HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual Hypergraph_Basics Hypergraph_Colourings IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse Interval_Analysis IO_Language_Conformance IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry IMP_Noninterference Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_hoops Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD Karatsuba KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt KnuthMorrisPratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_Series Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lovasz_Local Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Martingales Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc ML_Unification Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Nominal_Myhill_Nerode Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OmegaCatoidsQuantales OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect_Fields Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polygonal_Number_Theorem Polylog Polynomial_Crit_Geometry Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic Q0_Metatheory Q0_Soundness QBF_Solver_Verification QHLProver QR_Decomposition Quantales Quantales_Converse Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Region_Quadtrees Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Cardinality Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 S_Finite_Measure_Monad Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Standard_Borel_Spaces Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras Sumcheck_Protocol SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Transport Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Wieferich_Kempner Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL Labeled_Transition_Systems Pushdown_Systems