This translation extends 'std_prelude'. Certificate theorem for push: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "push") ((LIST_TYPE a --> a --> LIST_TYPE a) push) Certificate theorem for pop: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "pop") ((LIST_TYPE a --> NUM --> LIST_TYPE a) pop) Certificate theorem for take1: |- DeclAssum example_parser_gen_decls env ∧ take1_side x x1 ⇒ Eval env (Var "take1") ((Eq NUM x --> Eq (LIST_TYPE a) x1 --> LIST_TYPE a) take1) Definition of side condition for take1: |- take1_side v1 v2 ⇔ case v1 of 0 => (v2 = []) ∨ ∃v__5 v__4. v2 = v__5::v__4 | SUC v__3 => case v2 of [] => F | v__2::v__1 => take1_side v__3 v__1 Certificate theorem for take: |- DeclAssum example_parser_gen_decls env ∧ take_side v2 v1 ⇒ Eval env (Var "take") ((Eq NUM v2 --> Eq (LIST_TYPE a) v1 --> OPTION_TYPE (LIST_TYPE a)) take) Definition of side condition for take: |- take_side v2 v1 ⇔ LENGTH v1 ≥ v2 ⇒ take1_side v2 v1 Definition of refinement invariant: |- (∀x_2 v. SYMBOL_TYPE (NTS x_2) v ⇔ ∃v2_1. (v = Conv "Nts" [v2_1]) ∧ LIST_TYPE CHAR x_2 v2_1) ∧ ∀x_1 v. SYMBOL_TYPE (TS x_1) v ⇔ ∃v1_1. (v = Conv "Ts" [v1_1]) ∧ LIST_TYPE CHAR x_1 v1_1 Certificate theorem for isNonTmnlSym: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "isNonTmnlSym") ((SYMBOL_TYPE --> BOOL) isNonTmnlSym) Certificate theorem for sym2Str: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "sym2Str") ((SYMBOL_TYPE --> LIST_TYPE CHAR) sym2Str) Definition of refinement invariant: |- ∀x_2 x_1 v. RULE_TYPE (rule x_2 x_1) v ⇔ ∃v1_1 v1_2. (v = Conv "Rule" [v1_1; v1_2]) ∧ LIST_TYPE CHAR x_2 v1_1 ∧ LIST_TYPE SYMBOL_TYPE x_1 v1_2 Certificate theorem for ruleRhs: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "ruleRhs") ((RULE_TYPE --> LIST_TYPE SYMBOL_TYPE) ruleRhs) Certificate theorem for ruleLhs: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "ruleLhs") ((RULE_TYPE --> LIST_TYPE CHAR) ruleLhs) Definition of refinement invariant: |- (PTREE_TYPE (Node x_3 x_2) v ⇔ ∃v2_1 v2_2. (v = Conv "Node" [v2_1; v2_2]) ∧ LIST_TYPE CHAR x_3 v2_1 ∧ LIST_TYPE PTREE_TYPE x_2 v2_2) ∧ (PTREE_TYPE (Leaf x_1) v ⇔ ∃v1_1. (v = Conv "Leaf" [v1_1]) ∧ LIST_TYPE CHAR x_1 v1_1) Certificate theorem for ptree2Sym: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "ptree2Sym") ((PTREE_TYPE --> SYMBOL_TYPE) ptree2Sym) Certificate theorem for buildTree: |- DeclAssum example_parser_gen_decls env ∧ buildTree_side v2 v3 ⇒ Eval env (Var "buildTree") ((Eq (LIST_TYPE (PAIR_TYPE a PTREE_TYPE)) v2 --> Eq (LIST_TYPE SYMBOL_TYPE) v3 --> OPTION_TYPE (LIST_TYPE PTREE_TYPE)) buildTree) Definition of side condition for buildTree: |- buildTree_side v2 v3 ⇔ (take (LENGTH v3) (MAP (ptree2Sym o SND) v2) ≠ NONE ⇒ IS_SOME (take (LENGTH v3) (MAP (ptree2Sym o SND) v2)) ∧ ((v3 = THE (take (LENGTH v3) (MAP (ptree2Sym o SND) v2))) ⇒ take_side (LENGTH (THE (take (LENGTH v3) (MAP (ptree2Sym o SND) v2)))) (MAP SND v2) ∧ IS_SOME (take (LENGTH v3) (MAP (ptree2Sym o SND) v2)))) ∧ take_side (LENGTH v3) (MAP (ptree2Sym o SND) v2) Certificate theorem for addRule: |- DeclAssum example_parser_gen_decls env ∧ addRule_side v4 v5 ∧ EqualityType PTREE_TYPE ⇒ Eval env (Var "addRule") ((Eq (LIST_TYPE (PAIR_TYPE a PTREE_TYPE)) v4 --> Eq RULE_TYPE v5 --> OPTION_TYPE PTREE_TYPE) addRule) Definition of side condition for addRule: |- addRule_side v4 v5 ⇔ ∀v3 v2. (v5 = rule v3 v2) ⇒ (buildTree v4 (REVERSE v2) ≠ NONE ⇒ IS_SOME (buildTree v4 (REVERSE v2))) ∧ buildTree_side v4 (REVERSE v2) Certificate theorem for stackSyms: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "stackSyms") ((LIST_TYPE (PAIR_TYPE (PAIR_TYPE a b) c) --> LIST_TYPE a) stackSyms) Definition of refinement invariant: |- ∀x_2 x_1 v. ITEM_TYPE (item x_2 x_1) v ⇔ ∃v1_1 v1_2. (v = Conv "Item" [v1_1; v1_2]) ∧ LIST_TYPE CHAR x_2 v1_1 ∧ PAIR_TYPE (LIST_TYPE SYMBOL_TYPE) (LIST_TYPE SYMBOL_TYPE) x_1 v1_2 Certificate theorem for findItemInRules: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "findItemInRules") ((ITEM_TYPE --> LIST_TYPE RULE_TYPE --> BOOL) findItemInRules) Certificate theorem for itemEqRuleList: |- DeclAssum example_parser_gen_decls env ∧ itemEqRuleList_side v7 v8 ⇒ Eval env (Var "itemEqRuleList") ((Eq (LIST_TYPE ITEM_TYPE) v7 --> Eq (LIST_TYPE RULE_TYPE) v8 --> BOOL) itemEqRuleList) Definition of side condition for itemEqRuleList: |- itemEqRuleList_side v1 v2 ⇔ case v1 of [] => T | v__4::v__3 => case v2 of [] => T | v__2::v__1 => (LENGTH v__3 = LENGTH v__1) ⇒ findItemInRules v__4 (v__2::v__1) ⇒ itemEqRuleList_side v__3 (v__2::v__1) Definition of refinement invariant: |- (∀v. ACTION_TYPE NA v ⇔ (v = Conv "Na" [])) ∧ (∀x_2 v. ACTION_TYPE (GOTO x_2) v ⇔ ∃v2_1. (v = Conv "Goto" [v2_1]) ∧ LIST_TYPE ITEM_TYPE x_2 v2_1) ∧ ∀x_1 v. ACTION_TYPE (REDUCE x_1) v ⇔ ∃v1_1. (v = Conv "Reduce" [v1_1]) ∧ RULE_TYPE x_1 v1_1 Certificate theorem for getState: |- DeclAssum example_parser_gen_decls env ∧ getState_side v11 v12 v13 ⇒ Eval env (Var "getState") ((Eq (PAIR_TYPE (LIST_TYPE ITEM_TYPE --> SYMBOL_TYPE --> LIST_TYPE ITEM_TYPE) (LIST_TYPE ITEM_TYPE --> LIST_TYPE CHAR --> LIST_TYPE RULE_TYPE)) v11 --> Eq (LIST_TYPE ITEM_TYPE) v12 --> Eq SYMBOL_TYPE v13 --> ACTION_TYPE) getState) Definition of side condition for getState: |- getState_side v11 v12 v13 ⇔ ∀v10 v9. (v11 = (v10,v9)) ⇒ ∀v6 v5. (v10 v12 v13 = v6::v5) ⇒ ∀v4 v3. (v9 v12 (sym2Str v13) = v4::v3) ⇒ itemEqRuleList_side (v6::v5) (v4::v3) Certificate theorem for stackSyms_1: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "stackSyms_1") ((LIST_TYPE (PAIR_TYPE (PAIR_TYPE a b) c) --> LIST_TYPE a) stackSyms) Certificate theorem for exitCond: |- DeclAssum example_parser_gen_decls env ∧ EqualityType PTREE_TYPE ⇒ Eval env (Var "exitCond") ((PAIR_TYPE (LIST_TYPE CHAR) SYMBOL_TYPE --> PAIR_TYPE (LIST_TYPE SYMBOL_TYPE) (PAIR_TYPE (LIST_TYPE (PAIR_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE ITEM_TYPE)) PTREE_TYPE)) a) --> BOOL) exitCond) Certificate theorem for init: |- DeclAssum example_parser_gen_decls env ⇒ Eval env (Var "init") ((b --> a --> PAIR_TYPE a (PAIR_TYPE (LIST_TYPE (PAIR_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE ITEM_TYPE)) PTREE_TYPE)) (LIST_TYPE b))) init) Certificate theorem for doReduce: |- DeclAssum example_parser_gen_decls env ∧ doReduce_side x x1 x2 ∧ EqualityType PTREE_TYPE ∧ EqualityType a ⇒ Eval env (Var "doReduce") ((Eq (PAIR_TYPE (LIST_TYPE a --> SYMBOL_TYPE --> LIST_TYPE a) b) x --> Eq (PAIR_TYPE (LIST_TYPE SYMBOL_TYPE) (PAIR_TYPE (LIST_TYPE (PAIR_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE a)) PTREE_TYPE)) (LIST_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE a))))) x1 --> Eq RULE_TYPE x2 --> OPTION_TYPE (PAIR_TYPE (LIST_TYPE SYMBOL_TYPE) (PAIR_TYPE (LIST_TYPE (PAIR_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE a)) PTREE_TYPE)) (LIST_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE a)))))) doReduce) Definition of side condition for doReduce: |- doReduce_side v9 v8 v7 ⇔ (∃v6 v5 v4 v3 v2 v1. v8 = (v6::v5,v4,(v3,v2)::v1)) ∧ ∀v19 v18. (v8 = (v19,v18)) ⇒ ∀v17 v16. v19 ≠ [] ∧ ((v19 = v17::v16) ⇒ ∀v15 v14. (v18 = (v15,v14)) ⇒ ∀v13 v12. v14 ≠ [] ∧ ((v14 = v13::v12) ⇒ ∀v11 v10. (v13 = (v11,v10)) ⇒ ¬isNonTmnlSym v17 ⇒ addRule_side v15 v7)) Certificate theorem for parse: |- DeclAssum example_parser_gen_decls env ∧ parse_side x x1 ∧ EqualityType PTREE_TYPE ⇒ Eval env (Var "parse") ((Eq (OPTION_TYPE (PAIR_TYPE (LIST_TYPE ITEM_TYPE --> SYMBOL_TYPE --> LIST_TYPE ITEM_TYPE) (LIST_TYPE ITEM_TYPE --> LIST_TYPE CHAR --> LIST_TYPE RULE_TYPE))) x --> Eq (PAIR_TYPE (LIST_TYPE SYMBOL_TYPE) (PAIR_TYPE (LIST_TYPE (PAIR_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE ITEM_TYPE)) PTREE_TYPE)) (LIST_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE ITEM_TYPE))))) x1 --> OPTION_TYPE (PAIR_TYPE (LIST_TYPE SYMBOL_TYPE) (PAIR_TYPE (LIST_TYPE (PAIR_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE ITEM_TYPE)) PTREE_TYPE)) (LIST_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE ITEM_TYPE)))))) parse) Definition of side condition for parse: |- parse_side v7 v6 ⇔ (∃v5 v4 v3 v2 v1. v6 = (v5,v4,(v3,v2)::v1)) ∧ ∀v19 v18. (v6 = (v19,v18)) ⇒ ∀v17 v16. (v18 = (v17,v16)) ⇒ ∀v15 v14. v16 ≠ [] ∧ ((v16 = v15::v14) ⇒ ∀v13 v12. (v15 = (v13,v12)) ⇒ ∀v11. (v7 = SOME v11) ⇒ ∀v10 v9. (v19 = v10::v9) ⇒ ∀v8 v7. ((v9 = []) ⇒ getState_side v11 v12 v10 ∧ ∀v1. (getState v11 v12 v10 = REDUCE v1) ⇒ doReduce_side v11 ([v10],v17,(v13,v12)::v14) v1) ∧ ((v9 = v8::v7) ⇒ getState_side v11 v12 v10 ∧ ∀v4. (getState v11 v12 v10 = REDUCE v4) ⇒ doReduce_side v11 (v10::v8::v7,v17,(v13,v12)::v14) v4)) Certificate theorem for parser: |- DeclAssum example_parser_gen_decls env ∧ parser_side v26 v27 v28 ∧ EqualityType PTREE_TYPE ⇒ Eval env (Var "parser") ((Eq (PAIR_TYPE (PAIR_TYPE SYMBOL_TYPE (LIST_TYPE ITEM_TYPE)) (PAIR_TYPE (LIST_TYPE CHAR) (LIST_TYPE CHAR))) v26 --> Eq (OPTION_TYPE (PAIR_TYPE (LIST_TYPE ITEM_TYPE --> SYMBOL_TYPE --> LIST_TYPE ITEM_TYPE) (LIST_TYPE ITEM_TYPE --> LIST_TYPE CHAR --> LIST_TYPE RULE_TYPE))) v27 --> Eq (LIST_TYPE SYMBOL_TYPE) v28 --> OPTION_TYPE (OPTION_TYPE PTREE_TYPE)) parser) Definition of side condition for parser: |- parser_side v26 v27 v28 ⇔ ∀v25 v24. (v26 = (v25,v24)) ⇒ ∀v23 v22. (v24 = (v23,v22)) ⇒ IS_SOME (OWHILE (option_case FALSE (λv14. ¬exitCond (v23,NTS v22) v14)) (option_case NONE (pair_case (λv19. pair_case (λv17 v16. parse v27 (v19,v17,v16))))) (SOME (init v25 v28))) ∧ ∀v19 v17 v16. parse_side v27 (v19,v17,v16) Definition of declaration list: |- example_parser_gen_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 "push") (Fun "v2" (Fun "v1" (Con "Cons" [Var "v1"; Var "v2"]))); Dletrec [("pop","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0)))) (Con "Cons" [Var "v2"; Var "v1"]) (App Opapp (App Opapp (Var "pop") (Var "v1")) (App (Opn Minus) (Var "v4") (Val (Lit (IntLit 1))))))]))]; Dletrec [("take1","x", Fun "x1" (If (App (Opb Leq) (Var "x") (Val (Lit (IntLit 0)))) (Mat (Var "x1") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Con "Nil" [])]) (Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], If (App (Opb Leq) (Var "x") (Val (Lit (IntLit 0)))) (Con "Nil" []) (Con "Cons" [Var "v4"; App Opapp (App Opapp (Var "take1") (App (Opn Minus) (Var "x") (Val (Lit (IntLit 1))))) (Var "v3")]))])))]; Dlet (Pvar "take") (Fun "v2" (Fun "v1" (If (App (Opb Geq) (App Opapp (Var "LENGTH") (Var "v1")) (Var "v2")) (Con "Some" [App Opapp (App Opapp (Var "take1") (Var "v2")) (Var "v1")]) (Con "None" [])))); Dtype [([],"symbol", [("Nts",[Tapp [Tnum] "list"]); ("Ts",[Tapp [Tnum] "list"])])]; Dlet (Pvar "isNonTmnlSym") (Fun "v3" (Mat (Var "v3") [(Pcon "Ts" [Pvar "v1"],Val (Lit (Bool F))); (Pcon "Nts" [Pvar "v2"],Val (Lit (Bool T)))])); Dlet (Pvar "sym2Str") (Fun "v3" (Mat (Var "v3") [(Pcon "Ts" [Pvar "v1"],Var "v1"); (Pcon "Nts" [Pvar "v2"],Var "v2")])); Dtype [([],"rule", [("Rule", [Tapp [Tnum] "list"; Tapp [Tapp [] "symbol"] "list"])])]; Dlet (Pvar "ruleRhs") (Fun "v3" (Mat (Var "v3") [(Pcon "Rule" [Pvar "v2"; Pvar "v1"],Var "v1")])); Dlet (Pvar "ruleLhs") (Fun "v3" (Mat (Var "v3") [(Pcon "Rule" [Pvar "v2"; Pvar "v1"],Var "v2")])); Dtype [([],"ptree", [("Node",[Tapp [Tnum] "list"; Tapp [Tapp [] "ptree"] "list"]); ("Leaf",[Tapp [Tnum] "list"])])]; Dlet (Pvar "ptree2Sym") (Fun "v4" (Mat (Var "v4") [(Pcon "Leaf" [Pvar "v1"],Con "Ts" [Var "v1"]); (Pcon "Node" [Pvar "v3"; Pvar "v2"], Con "Nts" [Var "v3"])])); Dlet (Pvar "buildTree") (Fun "v2" (Fun "v3" (Let "v1" (App Opapp (App Opapp (Var "take") (App Opapp (Var "LENGTH") (Var "v3"))) (App Opapp (App Opapp (Var "MAP") (App Opapp (App Opapp (Var "o") (Var "ptree2Sym")) (Var "SND"))) (Var "v2"))) (If (App Equality (Var "v1") (Con "None" [])) (Con "None" []) (If (App Equality (Var "v3") (App Opapp (Var "THE") (Var "v1"))) (App Opapp (App Opapp (Var "take") (App Opapp (Var "LENGTH") (App Opapp (Var "THE") (Var "v1")))) (App Opapp (App Opapp (Var "MAP") (Var "SND")) (Var "v2"))) (Con "None" [])))))); Dlet (Pvar "addRule") (Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Rule" [Pvar "v3"; Pvar "v2"], Let "v1" (App Opapp (App Opapp (Var "buildTree") (Var "v4")) (App Opapp (Var "REVERSE") (Var "v2"))) (If (App Equality (Var "v1") (Con "None" [])) (Con "None" []) (Con "Some" [Con "Node" [Var "v3"; App Opapp (Var "REVERSE") (App Opapp (Var "THE") (Var "v1"))]])))]))); Dlet (Pvar "stackSyms") (Fun "v1" (App Opapp (Var "REVERSE") (App Opapp (App Opapp (Var "MAP") (Var "FST")) (App Opapp (App Opapp (Var "MAP") (Var "FST")) (Var "v1"))))); Dtype [([],"item", [("Item", [Tapp [Tnum] "list"; Tapp [Tapp [Tapp [] "symbol"] "list"; Tapp [Tapp [] "symbol"] "list"] "prod"])])]; Dlet (Pvar "findItemInRules") (Fun "v11" (Fun "v12" (Mat (Var "v11") [(Pcon "Item" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Nil" [], Mat (Var "v12") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Mat (Var "v4") [(Pcon "Rule" [Pvar "v2"; Pvar "v1"], Val (Lit (Bool T)))])]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Val (Lit (Bool F)))])])]))); Dletrec [("itemEqRuleList","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Nil" [], Mat (Var "v8") [(Pcon "Nil" [],Val (Lit (Bool T))); (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"], If (App Equality (App Equality (App Opapp (Var "LENGTH") (Con "Cons" [Var "v6"; Var "v5"])) (App Opapp (Var "LENGTH") (Con "Cons" [Var "v4"; Var "v3"]))) (Val (Lit (Bool F)))) (Val (Lit (Bool F))) (If (App Opapp (App Opapp (Var "findItemInRules") (App Opapp (Var "HD") (Con "Cons" [Var "v6"; Var "v5"]))) (Con "Cons" [Var "v4"; Var "v3"])) (App Opapp (App Opapp (Var "itemEqRuleList") (App Opapp (Var "TL") (Con "Cons" [Var "v6"; Var "v5"]))) (Con "Cons" [Var "v4"; Var "v3"])) (Val (Lit (Bool F)))))])]))]; Dtype [([],"action", [("Na",[]); ("Goto",[Tapp [Tapp [] "item"] "list"]); ("Reduce",[Tapp [] "rule"])])]; Dlet (Pvar "getState") (Fun "v11" (Fun "v12" (Fun "v13" (Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Let "v8" (App Opapp (App Opapp (Var "v10") (Var "v12")) (Var "v13")) (Let "v7" (App Opapp (App Opapp (Var "v9") (Var "v12")) (App Opapp (Var "sym2Str") (Var "v13"))) (Mat (Var "v8") [(Pcon "Nil" [], Mat (Var "v7") [(Pcon "Nil" [],Con "Na" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Equality (App Opapp (Var "LENGTH") (Var "v7")) (Val (Lit (IntLit 1)))) (Con "Reduce" [App Opapp (Var "HD") (Var "v7")]) (Con "Na" []))]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v7") [(Pcon "Nil" [],Con "Goto" [Var "v8"]); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], If (App Opapp (App Opapp (Var "itemEqRuleList") (Con "Cons" [Var "v6"; Var "v5"])) (Con "Cons" [Var "v4"; Var "v3"])) (Con "Reduce" [App Opapp (Var "HD") (Var "v7")]) (Con "Na" []))])])))])))); Dlet (Pvar "stackSyms_1") (Fun "v1" (App Opapp (Var "REVERSE") (App Opapp (App Opapp (Var "MAP") (Var "FST")) (App Opapp (App Opapp (Var "MAP") (Var "FST")) (Var "v1"))))); Dlet (Pvar "exitCond") (Fun "v7" (Fun "v8" (Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v8") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Log And (Log And (App Equality (App Equality (Var "v2") (Con "Nil" [])) (Val (Lit (Bool F)))) (App Equality (App Opapp (Var "stackSyms_1") (Var "v2")) (Con "Cons" [Var "v5"; Con "Nil" []]))) (App Equality (Var "v4") (Con "Cons" [Con "Ts" [Var "v6"]; Con "Nil" []])))])])]))); Dlet (Pvar "init") (Fun "v1" (Fun "v2" (Con "Pair" [Var "v2"; Con "Pair" [Con "Nil" []; Con "Cons" [Var "v1"; Con "Nil" []]]]))); Dlet (Pvar "doReduce") (Fun "x" (Fun "x1" (Fun "x2" (Mat (Var "x1") [(Pcon "Pair" [Pvar "v19"; Pvar "v18"], Mat (Var "v19") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v17"; Pvar "v16"], Mat (Var "v18") [(Pcon "Pair" [Pvar "v15"; Pvar "v14"], Mat (Var "v14") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v13"; Pvar "v12"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v11"; Pvar "v10"], If (App Opapp (Var "isNonTmnlSym") (Var "v17")) (Con "None" []) (Let "v9" (App Opapp (Var "ruleLhs") (Var "x2")) (Let "v8" (App Opapp (Var "ruleRhs") (Var "x2")) (Let "v7" (App Opapp (App Opapp (Var "addRule") (Var "v15")) (Var "x2")) (Mat (Var "v7") [(Pcon "None" [], Con "None" []); (Pcon "Some" [Pvar "v6"], Let "v5" (App Opapp (App Opapp (Var "pop") (Var "v15")) (App Opapp (Var "LENGTH") (Var "v8"))) (Let "v4" (App Opapp (App Opapp (Var "pop") (Con "Cons" [Con "Pair" [Var "v11"; Var "v10"]; Var "v12"])) (App Opapp (Var "LENGTH") (Var "v8"))) (If (App Equality (Var "v4") (Con "Nil" [])) (Con "None" []) (Let "v3" (App Opapp (Var "SND") (App Opapp (Var "HD") (Var "v4"))) (Let "v2" (App Opapp (App Opapp (App Opapp (Var "FST") (Var "x")) (Var "v3")) (Con "Nts" [Var "v9"])) (If (App Equality (Var "v2") (Con "Nil" [])) (Con "None" []) (Let "v1" (Con "Pair" [Con "Nts" [Var "v9"]; Var "v2"]) (Con "Some" [Con "Pair" [Con "Cons" [Var "v17"; Var "v16"]; Con "Pair" [App Opapp (App Opapp (Var "APPEND") (Con "Cons" [Con "Pair" [Var "v1"; Var "v6"]; Con "Nil" []])) (Var "v5"); App Opapp (App Opapp (Var "push") (Var "v4")) (Var "v1")]]]))))))))])))))])])])])])))); Dlet (Pvar "parse") (Fun "x" (Fun "x1" (Mat (Var "x1") [(Pcon "Pair" [Pvar "v19"; Pvar "v18"], Mat (Var "v18") [(Pcon "Pair" [Pvar "v17"; Pvar "v16"], Mat (Var "v16") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v15"; Pvar "v14"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v13"; Pvar "v12"], Mat (Var "x") [(Pcon "None" [],Con "None" []); (Pcon "Some" [Pvar "v11"], Mat (Var "v19") [(Pcon "Nil" [],Con "None" []); (Pcon "Cons" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Nil" [], Let "v3" (App Opapp (App Opapp (App Opapp (Var "getState") (Var "v11")) (Var "v12")) (Var "v10")) (Mat (Var "v3") [(Pcon "Reduce" [Pvar "v1"], App Opapp (App Opapp (App Opapp (Var "doReduce") (Var "v11")) (Con "Pair" [Con "Cons" [Var "v10"; Con "Nil" []]; Con "Pair" [Var "v17"; Con "Cons" [Con "Pair" [Var "v13"; Var "v12"]; Var "v14"]]])) (Var "v1")); (Pcon "Goto" [Pvar "v2"], Con "None" []); (Pcon "Na" [], Con "None" [])])); (Pcon "Cons" [Pvar "v8"; Pvar "v7"], Let "v6" (App Opapp (App Opapp (App Opapp (Var "getState") (Var "v11")) (Var "v12")) (Var "v10")) (Mat (Var "v6") [(Pcon "Reduce" [Pvar "v4"], App Opapp (App Opapp (App Opapp (Var "doReduce") (Var "v11")) (Con "Pair" [Con "Cons" [Var "v10"; Con "Cons" [Var "v8"; Var "v7"]]; Con "Pair" [Var "v17"; Con "Cons" [Con "Pair" [Var "v13"; Var "v12"]; Var "v14"]]])) (Var "v4")); (Pcon "Goto" [Pvar "v5"], If (App Opapp (Var "isNonTmnlSym") (Var "v10")) (Con "None" []) (Con "Some" [Con "Pair" [Con "Cons" [Var "v8"; Var "v7"]; Con "Pair" [Con "Cons" [Con "Pair" [Con "Pair" [Var "v10"; Var "v5"]; Con "Leaf" [App Opapp (Var "sym2Str") (Var "v10")]]; Var "v17"]; App Opapp (App Opapp (Var "push") (Con "Cons" [Con "Pair" [Var "v13"; Var "v12"]; Var "v14"])) (Con "Pair" [Var "v10"; Var "v5"])]]])); (Pcon "Na" [], Con "None" [])]))])])])])])])]))); Dlet (Pvar "parser") (Fun "v26" (Fun "v27" (Fun "v28" (Mat (Var "v26") [(Pcon "Pair" [Pvar "v25"; Pvar "v24"], Mat (Var "v24") [(Pcon "Pair" [Pvar "v23"; Pvar "v22"], Let "v13" (App Opapp (App Opapp (App Opapp (Letrec [("owhile","g", Fun "f" (Fun "x" (If (App Opapp (Var "g") (Var "x")) (App Opapp (App Opapp (App Opapp (Var "owhile") (Var "g")) (Var "f")) (App Opapp (Var "f") (Var "x"))) (Con "Some" [Var "x"]))))] (Var "owhile")) (Fun "v15" (Mat (Var "v15") [(Pcon "None" [], Val (Lit (Bool F))); (Pcon "Some" [Pvar "v14"], App Equality (App Opapp (App Opapp (Var "exitCond") (Con "Pair" [Var "v23"; Con "Nts" [Var "v22"]])) (Var "v14")) (Val (Lit (Bool F))))]))) (Fun "v21" (Mat (Var "v21") [(Pcon "None" [],Con "None" []); (Pcon "Some" [Pvar "v20"], Mat (Var "v20") [(Pcon "Pair" [Pvar "v19"; Pvar "v18"], Mat (Var "v18") [(Pcon "Pair" [Pvar "v17"; Pvar "v16"], App Opapp (App Opapp (Var "parse") (Var "v27")) (Con "Pair" [Var "v19"; Con "Pair" [Var "v17"; Var "v16"]]))])])]))) (Con "Some" [App Opapp (App Opapp (Var "init") (Var "v25")) (Var "v28")])) (Mat (Var "v13") [(Pcon "None" [],Con "None" []); (Pcon "Some" [Pvar "v12"], Mat (Var "v12") [(Pcon "None" [], Con "Some" [Con "None" []]); (Pcon "Some" [Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v8") [(Pcon "Nil" [], Con "Some" [Con "None" []]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v6") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v5") [(Pcon "Nil" [], Con "Some" [Con "Some" [Var "v3"]]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Some" [Con "None" []])])])])])])])]))])]))))]