Dlet (Pvar "EVEN") (Fun "v1" (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0))))) Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])] Dlet (Pvar "UNIT") (Fun "v2" (Fun "v1" (Con "Pair" [Var "v2"; Var "v1"]))) Dlet (Pvar "BIND") (Fun "v4" (Fun "v3" (Fun "v5" (Mat (App Opapp (Var "v4") (Var "v5")) [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "v3") (Var "v2")) (Var "v1"))])))) Dletrec [("prob_while_cut","v2", Fun "v3" (Fun "v4" (Fun "v5" (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0)))) (App Opapp (Var "UNIT") (Var "v5")) (If (App Opapp (Var "v2") (Var "v5")) (App Opapp (App Opapp (Var "BIND") (App Opapp (Var "v3") (Var "v5"))) (Fun "v1" (App Opapp (App Opapp (App Opapp (App Opapp (Var "prob_while_cut") (Var "v2")) (Var "v3")) (Let "k" (App (Opn Minus) (Var "v4") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))) (Var "v1")))) (App Opapp (Var "UNIT") (Var "v5")))))))] Dlet (Pvar "K") (Fun "v2" (Fun "v1" (Var "v2"))) Dlet (Pvar "I") (Fun "v1" (Var "v1")) Dlet (Pvar "many") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (App Opapp (Var "prob_while_cut") (Var "I")) (App Opapp (Var "K") (Var "v1"))) (Var "v2")) (Val (Lit (Bool T)))))) Dletrec [("log2","v1", If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (App (Opn Plus) (App Opapp (Var "log2") (App (Opn Divide) (Var "v1") (Val (Lit (IntLit 2))))) (Val (Lit (IntLit 1)))))] Dletrec [("factor_twos","v4", If (Log And (App (Opb Lt) (Val (Lit (IntLit 0))) (Var "v4")) (App Opapp (Var "EVEN") (Var "v4"))) (Let "v3" (App Opapp (Var "factor_twos") (App (Opn Divide) (Var "v4") (Val (Lit (IntLit 2))))) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1))); Var "v1"])])) (Con "Pair" [Val (Lit (IntLit 0)); Var "v4"]))] Dletrec [("modexp","v5", Fun "v3" (Fun "v4" (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 1))) (Let "v2" (App Opapp (App Opapp (App Opapp (Var "modexp") (Var "v5")) (Var "v3")) (App (Opn Divide) (Var "v4") (Val (Lit (IntLit 2))))) (Let "v1" (App (Opn Modulo) (App (Opn Times) (Var "v2") (Var "v2")) (Var "v5")) (If (App Opapp (Var "EVEN") (Var "v4")) (Var "v1") (App (Opn Modulo) (App (Opn Times) (Var "v1") (Var "v3")) (Var "v5"))))))))] Dletrec [("witness_tail","v2", Fun "v3" (Fun "v4" (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0)))) (App Equality (App Equality (Var "v3") (Val (Lit (IntLit 1)))) (Val (Lit (Bool F)))) (Let "v1" (App (Opn Modulo) (App (Opn Times) (Var "v3") (Var "v3")) (Var "v2")) (If (App Equality (Var "v1") (Val (Lit (IntLit 1)))) (Log And (App Equality (App Equality (Var "v3") (Val (Lit (IntLit 1)))) (Val (Lit (Bool F)))) (App Equality (App Equality (Var "v3") (Let "k" (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))) (Val (Lit (Bool F))))) (App Opapp (App Opapp (App Opapp (Var "witness_tail") (Var "v2")) (Var "v1")) (App (Opn Minus) (Var "v4") (Val (Lit (IntLit 1))))))))))] Dlet (Pvar "witness") (Fun "v5" (Fun "v4" (Let "v3" (App Opapp (Var "factor_twos") (Let "k" (App (Opn Minus) (Var "v5") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (App Opapp (Var "witness_tail") (Var "v5")) (App Opapp (App Opapp (App Opapp (Var "modexp") (Var "v5")) (Var "v4")) (Var "v1"))) (Var "v2"))])))) Dlet (Pvar "shd") (Fun "v1" (App Opapp (Var "v1") (Val (Lit (IntLit 0))))) Dlet (Pvar "stl") (Fun "v1" (Fun "v2" (App Opapp (Var "v1") (App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1))))))) Dletrec [("prob_unif","v4", Fun "v5" (If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0)))) (Con "Pair" [Val (Lit (IntLit 0)); Var "v5"]) (Let "v3" (App Opapp (App Opapp (Var "prob_unif") (App (Opn Divide) (Var "v4") (Val (Lit (IntLit 2))))) (Var "v5")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [If (App Opapp (Var "shd") (Var "v1")) (App (Opn Plus) (App (Opn Times) (Val (Lit (IntLit 2))) (Var "v2")) (Val (Lit (IntLit 1)))) (App (Opn Times) (Val (Lit (IntLit 2))) (Var "v2")); App Opapp (Var "stl") (Var "v1")])]))))] Dletrec [("prob_uniform_cut","x", Fun "x1" (Fun "x2" (If (App (Opb Leq) (Var "x") (Val (Lit (IntLit 0)))) (If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0)))) (Raise Bind_error) (Con "Pair" [Val (Lit (IntLit 0)); Var "x2"])) (If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0)))) (Raise Bind_error) (Let "v3" (App Opapp (App Opapp (Var "prob_unif") (App (Opn Minus) (Var "x1") (Val (Lit (IntLit 1))))) (Var "x2")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], If (App (Opb Lt) (Var "v2") (Var "x1")) (Con "Pair" [Var "v2"; Var "v1"]) (App Opapp (App Opapp (App Opapp (Var "prob_uniform_cut") (App (Opn Minus) (Var "x") (Val (Lit (IntLit 1))))) (Var "x1")) (Var "v1")))]))))))] Dlet (Pvar "miller_rabin_1") (Fun "v4" (Fun "v5" (If (App Equality (Var "v4") (Val (Lit (IntLit 2)))) (Con "Pair" [Val (Lit (Bool T)); Var "v5"]) (If (Log Or (App Equality (Var "v4") (Val (Lit (IntLit 1)))) (App Opapp (Var "EVEN") (Var "v4"))) (Con "Pair" [Val (Lit (Bool F)); Var "v5"]) (Let "v3" (App Opapp (App Opapp (App Opapp (Var "prob_uniform_cut") (App (Opn Times) (Val (Lit (IntLit 2))) (App Opapp (Var "log2") (Let "k" (App (Opn Minus) (Var "v4") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))) (Let "k" (App (Opn Minus) (Var "v4") (Val (Lit (IntLit 2)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))) (Var "v5")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Equality (App Opapp (App Opapp (Var "witness") (Var "v4")) (App (Opn Plus) (Var "v2") (Val (Lit (IntLit 2))))) (Val (Lit (Bool F))); Var "v1"])])))))) Dlet (Pvar "miller_rabin") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "many") (App Opapp (Var "miller_rabin_1") (Var "v1"))) (Var "v2"))))