This translation extends 'word_prelude'. Certificate theorem for ShiftXor: |- DeclAssum example_tea_decls env ⇒ Eval env (Var "ShiftXor") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> WORD) ShiftXor) Certificate theorem for Round: |- DeclAssum example_tea_decls env ⇒ Eval env (Var "Round") ((PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD) --> PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD)) Round) Certificate theorem for InvRound: |- DeclAssum example_tea_decls env ⇒ Eval env (Var "InvRound") ((PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD) --> PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD)) InvRound) Certificate theorem for Rounds: |- DeclAssum example_tea_decls env ⇒ Eval env (Var "Rounds") ((PAIR_TYPE WORD (PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD)) --> PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD)) Rounds) Certificate theorem for InvRounds: |- DeclAssum example_tea_decls env ⇒ Eval env (Var "InvRounds") ((PAIR_TYPE WORD (PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD)) --> PAIR_TYPE (PAIR_TYPE WORD WORD) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) WORD)) InvRounds) Certificate theorem for teaEncrypt: |- DeclAssum example_tea_decls env ⇒ Eval env (Var "teaEncrypt") ((PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) (PAIR_TYPE WORD WORD) --> PAIR_TYPE WORD WORD) teaEncrypt) Certificate theorem for teaDecrypt: |- DeclAssum example_tea_decls env ⇒ Eval env (Var "teaDecrypt") ((PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) (PAIR_TYPE WORD WORD) --> PAIR_TYPE WORD WORD) teaDecrypt) Definition of declaration list: |- example_tea_decls = [Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])]; Dtype [(["a"],"list", [("Cons",[Tvar "a"; Tapp [Tvar "a"] "list"]); ("Nil",[])])]; Dlet (Pvar "HD") (Fun "x1" (Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")])); Dlet (Pvar "TL") (Fun "x1" (Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v1")])); Dletrec [("APPEND","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "APPEND") (Var "v1")) (Var "v4")])]))]; Dletrec [("REV","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Cons" [Var "v2"; Var "v4"]))]))]; Dlet (Pvar "REVERSE") (Fun "v1" (App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Nil" []))); Dlet (Pvar "FST") (Fun "v3" (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v2")])); Dlet (Pvar "SND") (Fun "v3" (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v1")])); Dlet (Pvar "CURRY") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (Var "v1") (Con "Pair" [Var "v2"; Var "v3"]))))); Dlet (Pvar "UNCURRY") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "v1") (App Opapp (Var "FST") (Var "v2"))) (App Opapp (Var "SND") (Var "v2"))))); Dlet (Pvar "o") (Fun "v2" (Fun "v3" (Fun "v1" (App Opapp (Var "v2") (App Opapp (Var "v3") (Var "v1")))))); Dlet (Pvar "I") (Fun "v1" (Var "v1")); Dlet (Pvar "C") (Fun "v3" (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v3") (Var "v1")) (Var "v2"))))); Dlet (Pvar "K") (Fun "v2" (Fun "v1" (Var "v2"))); Dlet (Pvar "S") (Fun "v3" (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v3") (Var "v1")) (App Opapp (Var "v2") (Var "v1")))))); Dlet (Pvar "UPDATE") (Fun "v3" (Fun "v4" (Fun "v2" (Fun "v1" (If (App Equality (Var "v3") (Var "v1")) (Var "v4") (App Opapp (Var "v2") (Var "v1"))))))); Dlet (Pvar "W") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v2") (Var "v1")) (Var "v1")))); Dtype [([],"one",[("One",[])])]; Dtype [(["a"],"option",[("Some",[Tvar "a"]); ("None",[])])]; Dlet (Pvar "THE") (Fun "x1" (Mat (Var "x1") [(Pcon "None" [],Raise Bind_error); (Pcon "Some" [Pvar "v1"],Var "v1")])); Dlet (Pvar "IS_NONE") (Fun "v2" (Mat (Var "v2") [(Pcon "None" [],Val (Lit (Bool T))); (Pcon "Some" [Pvar "v1"],Val (Lit (Bool F)))])); Dlet (Pvar "IS_SOME") (Fun "v2" (Mat (Var "v2") [(Pcon "None" [],Val (Lit (Bool F))); (Pcon "Some" [Pvar "v1"],Val (Lit (Bool T)))])); Dlet (Pvar "OPTION_MAP") (Fun "v2" (Fun "v3" (Mat (Var "v3") [(Pcon "None" [],Con "None" []); (Pcon "Some" [Pvar "v1"], Con "Some" [App Opapp (Var "v2") (Var "v1")])]))); Dlet (Pvar "OPTION_MAP2") (Fun "v1" (Fun "v2" (Fun "v3" (If (Log And (App Opapp (Var "IS_SOME") (Var "v2")) (App Opapp (Var "IS_SOME") (Var "v3"))) (Con "Some" [App Opapp (App Opapp (Var "v1") (App Opapp (Var "THE") (Var "v2"))) (App Opapp (Var "THE") (Var "v3"))]) (Con "None" []))))); Dtype [(["a"; "b"],"sum",[("Inr",[Tvar "b"]); ("Inl",[Tvar "a"])])]; Dlet (Pvar "ISL") (Fun "v3" (Mat (Var "v3") [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool T))); (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool F)))])); Dlet (Pvar "ISR") (Fun "v3" (Mat (Var "v3") [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool F))); (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool T)))])); Dlet (Pvar "OUTL") (Fun "x1" (Mat (Var "x1") [(Pcon "Inl" [Pvar "v1"],Var "v1"); (Pcon "Inr" [Pvar "v2"],Raise Bind_error)])); Dlet (Pvar "OUTR") (Fun "x1" (Mat (Var "x1") [(Pcon "Inl" [Pvar "v1"],Raise Bind_error); (Pcon "Inr" [Pvar "v2"],Var "v2")])); Dlet (Pvar "++") (Fun "v3" (Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Inl" [Pvar "v1"], Con "Inl" [App Opapp (Var "v3") (Var "v1")]); (Pcon "Inr" [Pvar "v2"], Con "Inr" [App Opapp (Var "v4") (Var "v2")])])))); Dletrec [("LENGTH_AUX","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1")) (App (Opn Plus) (Var "v4") (Val (Lit (IntLit 1)))))]))]; Dlet (Pvar "LENGTH") (Fun "v1" (App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1")) (Val (Lit (IntLit 0))))); Dletrec [("MAP","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [App Opapp (Var "v3") (Var "v2"); App Opapp (App Opapp (Var "MAP") (Var "v3")) (Var "v1")])]))]; Dletrec [("FILTER","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Opapp (Var "v3") (Var "v2")) (Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "FILTER") (Var "v3")) (Var "v1")]) (App Opapp (App Opapp (Var "FILTER") (Var "v3")) (Var "v1")))]))]; Dletrec [("FOLDR","v3", Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (App Opapp (Var "FOLDR") (Var "v3")) (Var "v4")) (Var "v1")))])))]; Dletrec [("FOLDL","v3", Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (App Opapp (Var "FOLDL") (Var "v3")) (App Opapp (App Opapp (Var "v3") (Var "v4")) (Var "v2"))) (Var "v1"))])))]; Dletrec [("SUM","v3", Mat (Var "v3") [(Pcon "Nil" [],Val (Lit (IntLit 0))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App (Opn Plus) (Var "v2") (App Opapp (Var "SUM") (Var "v1")))])]; Dletrec [("UNZIP","v3", Mat (Var "v3") [(Pcon "Nil" [],Con "Pair" [Con "Nil" []; Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Pair" [Con "Cons" [App Opapp (Var "FST") (Var "v2"); App Opapp (Var "FST") (App Opapp (Var "UNZIP") (Var "v1"))]; Con "Cons" [App Opapp (Var "SND") (Var "v2"); App Opapp (Var "SND") (App Opapp (Var "UNZIP") (Var "v1"))]])])]; Dletrec [("FLAT","v3", Mat (Var "v3") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "APPEND") (Var "v2")) (App Opapp (Var "FLAT") (Var "v1")))])]; Dletrec [("TAKE","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Con "Nil" []) (Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "TAKE") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (Var "v1")]))]))]; Dletrec [("DROP","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Con "Cons" [Var "v2"; Var "v1"]) (App Opapp (App Opapp (Var "DROP") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (Var "v1")))]))]; Dletrec [("SNOC","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Cons" [Var "v3"; Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "SNOC") (Var "v3")) (Var "v1")])]))]; Dletrec [("EVERY","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "EVERY") (Var "v3")) (Var "v1")))]))]; Dletrec [("EXISTS","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log Or (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "EXISTS") (Var "v3")) (Var "v1")))]))]; Dletrec [("GENLIST","v1", Fun "v2" (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0)))) (Con "Nil" []) (App Opapp (App Opapp (Var "SNOC") (App Opapp (Var "v1") (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1)))))) (App Opapp (App Opapp (Var "GENLIST") (Var "v1")) (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1))))))))]; Dlet (Pvar "PAD_RIGHT") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (App Opapp (Var "APPEND") (Var "v3")) (App Opapp (App Opapp (Var "GENLIST") (App Opapp (Var "K") (Var "v1"))) (Let "k" (App (Opn Minus) (Var "v2") (App Opapp (Var "LENGTH") (Var "v3"))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))))); Dlet (Pvar "PAD_LEFT") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "GENLIST") (App Opapp (Var "K") (Var "v1"))) (Let "k" (App (Opn Minus) (Var "v2") (App Opapp (Var "LENGTH") (Var "v3"))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (Var "v3"))))); Dletrec [("MEM","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log Or (App Equality (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "MEM") (Var "v3")) (Var "v1")))]))]; Dletrec [("ALL_DISTINCT","v3", Mat (Var "v3") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Equality (App Opapp (App Opapp (Var "MEM") (Var "v2")) (Var "v1")) (Val (Lit (Bool F)))) (App Opapp (Var "ALL_DISTINCT") (Var "v1")))])]; Dletrec [("isPREFIX","v5", Fun "v6" (Mat (Var "v5") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Mat (Var "v6") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Equality (Var "v4") (Var "v2")) (App Opapp (App Opapp (Var "isPREFIX") (Var "v3")) (Var "v1")))])]))]; Dletrec [("FRONT","x1", Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v1") (Con "Nil" [])) (Con "Nil" []) (Con "Cons" [Var "v2"; App Opapp (Var "FRONT") (Var "v1")]))])]; Dletrec [("ZIP","x1", Mat (Var "x1") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v8") [(Pcon "Nil" [], Mat (Var "v7") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Raise Bind_error)]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v7") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Con "Cons" [Con "Pair" [Var "v6"; Var "v4"]; App Opapp (Var "ZIP") (Con "Pair" [Var "v5"; Var "v3"])])])])])]; Dletrec [("EL","v1", Fun "v2" (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0)))) (App Opapp (Var "HD") (Var "v2")) (App Opapp (App Opapp (Var "EL") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (App Opapp (Var "TL") (Var "v2")))))]; Dletrec [("PART","v3", Fun "v4" (Fun "v5" (Fun "v6" (Mat (Var "v4") [(Pcon "Nil" [],Con "Pair" [Var "v5"; Var "v6"]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Con "Cons" [Var "v2"; Var "v5"])) (Var "v6")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Var "v5")) (Con "Cons" [Var "v2"; Var "v6"])))]))))]; Dlet (Pvar "PARTITION") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v1")) (Var "v2")) (Con "Nil" [])) (Con "Nil" [])))); Dletrec [("QSORT","v7", Fun "v8" (Mat (Var "v8") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Let "v3" (App Opapp (App Opapp (Var "PARTITION") (Fun "v4" (App Opapp (App Opapp (Var "v7") (Var "v4")) (Var "v6")))) (Var "v5")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v2"))) (Con "Cons" [Var "v6"; Con "Nil" []]))) (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v1")))]))]))]; Dletrec [("EXP_AUX","v2", Fun "v3" (Fun "v1" (If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Var "v1") (App Opapp (App Opapp (App Opapp (Var "EXP_AUX") (Var "v2")) (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (App (Opn Times) (Var "v2") (Var "v1"))))))]; Dlet (Pvar "EXP") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (Var "EXP_AUX") (Var "v1")) (Var "v2")) (Val (Lit (IntLit 1)))))); Dlet (Pvar "MIN") (Fun "v1" (Fun "v2" (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v1") (Var "v2")))); Dlet (Pvar "MAX") (Fun "v1" (Fun "v2" (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v2") (Var "v1")))); Dlet (Pvar "EVEN") (Fun "v1" (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0))))); Dlet (Pvar "ODD") (Fun "v1" (App (Opb Lt) (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))))); Dletrec [("FUNPOW","v1", Fun "v2" (Fun "v3" (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0)))) (Var "v3") (App Opapp (App Opapp (App Opapp (Var "FUNPOW") (Var "v1")) (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1))))) (App Opapp (Var "v1") (Var "v3"))))))]; Dlet (Pvar "MOD_2EXP") (Fun "v2" (Fun "v1" (App (Opn Modulo) (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2"))))); Dlet (Pvar "DIV_2EXP") (Fun "v2" (Fun "v1" (App (Opn Divide) (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2"))))); Dlet (Pvar "PRE") (Fun "v1" (Let "k" (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))); Dlet (Pvar "ABS_DIFF") (Fun "v2" (Fun "v1" (If (App (Opb Lt) (Var "v2") (Var "v1")) (Let "k" (App (Opn Minus) (Var "v1") (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (Let "k" (App (Opn Minus) (Var "v2") (Var "v1")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))); Dlet (Pvar "DIV2") (Fun "v1" (App (Opn Divide) (Var "v1") (Val (Lit (IntLit 2))))); Dletrec [("string_lt","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Nil" [], Mat (Var "v8") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Val (Lit (Bool T)))]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v8") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Log Or (App Opapp (Let "m" (Var "v6") (Fun "n" (App (Opb Lt) (Var "m") (Var "n")))) (Var "v4")) (Log And (App Equality (Var "v6") (Var "v4")) (App Opapp (App Opapp (Var "string_lt") (Var "v5")) (Var "v3"))))])]))]; Dlet (Pvar "string_le") (Fun "v1" (Fun "v2" (Log Or (App Equality (Var "v1") (Var "v2")) (App Opapp (App Opapp (Var "string_lt") (Var "v1")) (Var "v2"))))); Dlet (Pvar "string_gt") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "string_lt") (Var "v2")) (Var "v1")))); Dlet (Pvar "string_ge") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "string_le") (Var "v2")) (Var "v1")))); Dlet (Pvar "BITS") (Fun "v1" (Fun "v2" (Fun "v3" (App (Opn Divide) (App (Opn Modulo) (Var "v3") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (App (Opn Plus) (Var "v1") (Val (Lit (IntLit 1)))))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")))))); Dlet (Pvar "BIT") (Fun "v1" (Fun "v2" (App Equality (App (Opn Modulo) (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 1)))))); Dlet (Pvar "SBIT") (Fun "v1" (Fun "v2" (If (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (Val (Lit (IntLit 0)))))); Dtype [(["a"],"ptree", [("Branch", [Tnum; Tnum; Tapp [Tvar "a"] "ptree"; Tapp [Tvar "a"] "ptree"]); ("Leaf",[Tnum; Tvar "a"]); ("Empty",[])])]; Dletrec [("BRANCHING_BIT","v1", Fun "v2" (If (Log Or (App Equality (App Opapp (Var "ODD") (Var "v1")) (App Opapp (Var "EVEN") (Var "v2"))) (App Equality (Var "v1") (Var "v2"))) (Val (Lit (IntLit 0))) (App (Opn Plus) (App Opapp (App Opapp (Var "BRANCHING_BIT") (App Opapp (Var "DIV2") (Var "v1"))) (App Opapp (Var "DIV2") (Var "v2"))) (Val (Lit (IntLit 1))))))]; Dletrec [("PEEK","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Empty" [],Con "None" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v8") (Var "v2")) (Con "Some" [Var "v1"]) (Con "None" [])); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], App Opapp (App Opapp (Var "PEEK") (If (App Opapp (App Opapp (Var "BIT") (Var "v5")) (Var "v8")) (Var "v4") (Var "v3"))) (Var "v8"))]))]; Dlet (Pvar "MOD_2EXP_EQ") (Fun "v3" (Fun "v1" (Fun "v2" (App Equality (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3")) (Var "v1")) (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3")) (Var "v2")))))); Dlet (Pvar "JOIN") (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v7"; Pvar "v6"], Mat (Var "v6") [(Pcon "Pair" [Pvar "v5"; Pvar "v4"], Mat (Var "v4") [(Pcon "Pair" [Pvar "v3"; Pvar "v2"], Let "v1" (App Opapp (App Opapp (Var "BRANCHING_BIT") (Var "v7")) (Var "v3")) (If (App Opapp (App Opapp (Var "BIT") (Var "v1")) (Var "v7")) (Con "Branch" [App Opapp (App Opapp (Var "MOD_2EXP") (Var "v1")) (Var "v7"); Var "v1"; Var "v5"; Var "v2"]) (Con "Branch" [App Opapp (App Opapp (Var "MOD_2EXP") (Var "v1")) (Var "v7"); Var "v1"; Var "v2"; Var "v5"])))])])])); Dletrec [("ADD","v13", Fun "v14" (Mat (Var "v13") [(Pcon "Empty" [], Mat (Var "v14") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Leaf" [Var "v2"; Var "v1"])]); (Pcon "Leaf" [Pvar "v6"; Pvar "v5"], Mat (Var "v14") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], If (App Equality (Var "v6") (Var "v4")) (Con "Leaf" [Var "v4"; Var "v3"]) (App Opapp (Var "JOIN") (Con "Pair" [Var "v4"; Con "Pair" [Con "Leaf" [Var "v4"; Var "v3"]; Con "Pair" [Var "v6"; Con "Leaf" [Var "v6"; Var "v5"]]]])))]); (Pcon "Branch" [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"], Mat (Var "v14") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], If (App Opapp (App Opapp (App Opapp (Var "MOD_2EXP_EQ") (Var "v11")) (Var "v8")) (Var "v12")) (If (App Opapp (App Opapp (Var "BIT") (Var "v11")) (Var "v8")) (Con "Branch" [Var "v12"; Var "v11"; App Opapp (App Opapp (Var "ADD") (Var "v10")) (Con "Pair" [Var "v8"; Var "v7"]); Var "v9"]) (Con "Branch" [Var "v12"; Var "v11"; Var "v10"; App Opapp (App Opapp (Var "ADD") (Var "v9")) (Con "Pair" [Var "v8"; Var "v7"])])) (App Opapp (Var "JOIN") (Con "Pair" [Var "v8"; Con "Pair" [Con "Leaf" [Var "v8"; Var "v7"]; Con "Pair" [Var "v12"; Con "Branch" [Var "v12"; Var "v11"; Var "v10"; Var "v9"]]]])))])]))]; Dlet (Pvar "BRANCH") (Fun "v31" (Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v26") [(Pcon "Empty" [], Mat (Var "v25") [(Pcon "Empty" [],Con "Empty" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], Con "Leaf" [Var "v2"; Var "v1"]); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], Con "Branch" [Var "v6"; Var "v5"; Var "v4"; Var "v3"])]); (Pcon "Leaf" [Pvar "v14"; Pvar "v13"], Mat (Var "v25") [(Pcon "Empty" [], Con "Leaf" [Var "v14"; Var "v13"]); (Pcon "Leaf" [Pvar "v8"; Pvar "v7"], Con "Branch" [Var "v30"; Var "v28"; Con "Leaf" [Var "v14"; Var "v13"]; Con "Leaf" [Var "v8"; Var "v7"]]); (Pcon "Branch" [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"], Con "Branch" [Var "v30"; Var "v28"; Con "Leaf" [Var "v14"; Var "v13"]; Con "Branch" [Var "v12"; Var "v11"; Var "v10"; Var "v9"]])]); (Pcon "Branch" [Pvar "v24"; Pvar "v23"; Pvar "v22"; Pvar "v21"], Mat (Var "v25") [(Pcon "Empty" [], Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]); (Pcon "Leaf" [Pvar "v16"; Pvar "v15"], Con "Branch" [Var "v30"; Var "v28"; Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]; Con "Leaf" [Var "v16"; Var "v15"]]); (Pcon "Branch" [Pvar "v20"; Pvar "v19"; Pvar "v18"; Pvar "v17"], Con "Branch" [Var "v30"; Var "v28"; Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]; Con "Branch" [Var "v20"; Var "v19"; Var "v18"; Var "v17"]])])])])])])); Dletrec [("REMOVE","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Empty" [],Con "Empty" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v2") (Var "v8")) (Con "Empty" []) (Con "Leaf" [Var "v2"; Var "v1"])); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], If (App Opapp (App Opapp (App Opapp (Var "MOD_2EXP_EQ") (Var "v5")) (Var "v8")) (Var "v6")) (If (App Opapp (App Opapp (Var "BIT") (Var "v5")) (Var "v8")) (App Opapp (Var "BRANCH") (Con "Pair" [Var "v6"; Con "Pair" [Var "v5"; Con "Pair" [App Opapp (App Opapp (Var "REMOVE") (Var "v4")) (Var "v8"); Var "v3"]]])) (App Opapp (Var "BRANCH") (Con "Pair" [Var "v6"; Con "Pair" [Var "v5"; Con "Pair" [Var "v4"; App Opapp (App Opapp (Var "REMOVE") (Var "v3")) (Var "v8")]]]))) (Con "Branch" [Var "v6"; Var "v5"; Var "v4"; Var "v3"]))]))]; Dlet (Pvar "word_add") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_mul") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_add_1") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_mul_1") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_add_2") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_mul_2") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dletrec [("BITWISE","v1", Fun "v2" (Fun "v3" (Fun "v4" (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (App (Opn Plus) (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v2")) (Var "v3")) (Var "v4")) (App Opapp (App Opapp (Var "SBIT") (App Opapp (App Opapp (Var "v2") (App Opapp (App Opapp (Var "BIT") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v3"))) (App Opapp (App Opapp (Var "BIT") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v4")))) (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))))))))]; Dlet (Pvar "word_xor") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_xor_1") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 8)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_xor_2") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_or") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (Log Or (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_or_1") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16)))) (Fun "v2" (Fun "v1" (Log Or (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_and") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (Log And (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_lsl") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (Var "v1")))); Dlet (Pvar "word_lsl_1") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul_1") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))) (Var "v1")))); Dlet (Pvar "word_lsl_2") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul_2") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1")))); Dlet (Pvar "word_lsr") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_lsr_1") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_lsr_2") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_msb") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 31)))) (Var "v1"))); Dlet (Pvar "word_msb_1") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 15)))) (Var "v1"))); Dlet (Pvar "word_msb_2") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 7)))) (Var "v1"))); Dlet (Pvar "word_lsb") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_lsb_1") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_lsb_2") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_asr") (Fun "v2" (Fun "v1" (If (App Opapp (Var "word_msb") (Var "v2")) (App Opapp (App Opapp (Var "word_or") (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 4294967296))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 32))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (App Opapp (App Opapp (Var "word_lsr") (Var "v2")) (Var "v1"))) (App Opapp (App Opapp (Var "word_lsr") (Var "v2")) (Var "v1"))))); Dlet (Pvar "word_asr_1") (Fun "v2" (Fun "v1" (If (App Opapp (Var "word_msb_1") (Var "v2")) (App Opapp (App Opapp (Var "word_or_1") (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 65536))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 16))) (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 16))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))) (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2")) (Var "v1"))) (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2")) (Var "v1"))))); Dlet (Pvar "word_sub") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 4294967296))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))))); Dlet (Pvar "word_sub_1") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add_1") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 65536))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))); Dlet (Pvar "word_sub_2") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add_2") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 256))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))); Dlet (Pvar "word_bits") (Fun "v1" (Fun "v2" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (Var "BITS") (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 31))))) (Var "v2")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))))); Dlet (Pvar "word_ror") (Fun "v3" (Fun "v2" (Let "v1" (App (Opn Modulo) (Var "v2") (Val (Lit (IntLit 32)))) (App Opapp (App Opapp (Var "word_or") (App Opapp (App Opapp (App Opapp (Var "word_bits") (Val (Lit (IntLit 31)))) (Var "v1")) (Var "v3"))) (App Opapp (App Opapp (Var "word_lsl") (App Opapp (App Opapp (App Opapp (Var "word_bits") (Let "k" (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))) (Val (Lit (IntLit 0)))) (Var "v3"))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (Var "v1")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))))); Dlet (Pvar "word_rol") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "word_ror") (Var "v2")) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 32))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))); Dlet (Pvar "ShiftXor") (Fun "v7" (Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "word_xor") (App Opapp (App Opapp (Var "word_add") (App Opapp (App Opapp (Var "word_lsl") (Var "v6")) (Val (Lit (IntLit 4))))) (Var "v2"))) (App Opapp (App Opapp (Var "word_xor") (App Opapp (App Opapp (Var "word_add") (Var "v6")) (Var "v4"))) (App Opapp (App Opapp (Var "word_add") (App Opapp (App Opapp (Var "word_asr") (Var "v6")) (Val (Lit (IntLit 5))))) (Var "v1"))))])])])); Dlet (Pvar "Round") (Fun "v15" (Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v14") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v10") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Let "v2" (App Opapp (App Opapp (Var "word_add") (Var "v9")) (Let "x" (Val (Lit (IntLit 2654435769))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (Let "v1" (App Opapp (App Opapp (Var "word_add") (Var "v12")) (App Opapp (Var "ShiftXor") (Con "Pair" [Var "v11"; Con "Pair" [Var "v2"; Con "Pair" [Var "v8"; Var "v6"]]]))) (Con "Pair" [Con "Pair" [Var "v1"; App Opapp (App Opapp (Var "word_add") (Var "v11")) (App Opapp (Var "ShiftXor") (Con "Pair" [Var "v1"; Con "Pair" [Var "v2"; Con "Pair" [Var "v4"; Var "v3"]]]))]; Con "Pair" [Con "Pair" [Var "v8"; Con "Pair" [Var "v6"; Con "Pair" [Var "v4"; Var "v3"]]]; Var "v2"]])))])])])])])])); Dlet (Pvar "InvRound") (Fun "v13" (Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v12") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v8") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Con "Pair" [App Opapp (App Opapp (Var "word_sub") (Var "v10")) (App Opapp (Var "ShiftXor") (Con "Pair" [App Opapp (App Opapp (Var "word_sub") (Var "v9")) (App Opapp (Var "ShiftXor") (Con "Pair" [Var "v10"; Con "Pair" [Var "v7"; Con "Pair" [Var "v2"; Var "v1"]]])); Con "Pair" [Var "v7"; Con "Pair" [Var "v6"; Var "v4"]]])); App Opapp (App Opapp (Var "word_sub") (Var "v9")) (App Opapp (Var "ShiftXor") (Con "Pair" [Var "v10"; Con "Pair" [Var "v7"; Con "Pair" [Var "v2"; Var "v1"]]]))]; Con "Pair" [Con "Pair" [Var "v6"; Con "Pair" [Var "v4"; Con "Pair" [Var "v2"; Var "v1"]]]; App Opapp (App Opapp (Var "word_sub") (Var "v7")) (Let "x" (Val (Lit (IntLit 2654435769))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))]])])])])])])])); Dletrec [("Rounds","v3", Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v2") (Let "x" (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (Var "v1") (App Opapp (Var "Rounds") (Con "Pair" [App Opapp (App Opapp (Var "word_sub") (Var "v2")) (Let "x" (Val (Lit (IntLit 1))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))); App Opapp (Var "Round") (Var "v1")])))])]; Dletrec [("InvRounds","v3", Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v2") (Let "x" (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (Var "v1") (App Opapp (Var "InvRounds") (Con "Pair" [App Opapp (App Opapp (Var "word_sub") (Var "v2")) (Let "x" (Val (Lit (IntLit 1))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))); App Opapp (Var "InvRound") (Var "v1")])))])]; Dlet (Pvar "teaEncrypt") (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v7"; Pvar "v6"], Let "v5" (App Opapp (Var "Rounds") (Con "Pair" [Let "x" (Val (Lit (IntLit 32))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))); Con "Pair" [Var "v6"; Con "Pair" [Var "v7"; Let "x" (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))]]])) (Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Var "v4")])]))])); Dlet (Pvar "teaDecrypt") (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v7"; Pvar "v6"], Let "v5" (App Opapp (Var "InvRounds") (Con "Pair" [Let "x" (Val (Lit (IntLit 32))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))); Con "Pair" [Var "v6"; Con "Pair" [Var "v7"; App Opapp (App Opapp (Var "word_lsl") (Let "x" (Val (Lit (IntLit 2654435769))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (Val (Lit (IntLit 5)))]]])) (Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Var "v4")])]))]))]