permutations6.ctree 7.92 KB
Newer Older
1
Specification([Signature([Constructors([ExtOpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),OpDecl("d0",ConstType(Sort("Nat",[]))),OpDecl("s",FunType([ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[])))),OpDecl("nil",ConstType(Sort("NatList",[]))),OpDecl("l",FunType([ConstType(Sort("Nat",[]))],ConstType(Sort("NatList",[])))),OpDecl("ll",FunType([ConstType(Sort("NatList",[])),ConstType(Sort("NatList",[]))],ConstType(Sort("NatList",[])))),OpDecl("nilP",ConstType(Sort("NatListList",[]))),OpDecl("p",FunType([ConstType(Sort("NatList",[]))],ConstType(Sort("NatListList",[])))),OpDecl("pp",FunType([ConstType(Sort("NatListList",[])),ConstType(Sort("NatListList",[]))],ConstType(Sort("NatListList",[])))),OpDecl("perm",FunType([ConstType(Sort("Nat",[]))],ConstType(Sort("NatListList",[])))),OpDecl("insert1",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("NatListList",[]))],ConstType(Sort("NatListList",[])))),OpDecl("insert0",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("NatList",[]))],ConstType(Sort("NatListList",[])))),OpDecl("map_cons",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("NatListList",[]))],ConstType(Sort("NatListList",[])))),OpDecl("ppreduce",FunType([ConstType(Sort("NatListList",[])),ConstType(Sort("NatListList",[]))],ConstType(Sort("NatListList",[])))),OpDecl("ppflat",FunType([ConstType(Sort("NatListList",[])),ConstType(Sort("NatListList",[]))],ConstType(Sort("NatListList",[]))))])]),Strategies([SDefT("eval_0_0",[],[],CallT(SVar("memo_1_0"),[Let([SDefT("m_69",[VarDec("o_69",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(All(CallT(SVar("m_69"),[CallT(SVar("o_69"),[],[])],[])),CallT(SVar("o_69"),[],[]))),SDefT("n_69",[],[],GuardedLChoice(GuardedLChoice(Seq(Match(Anno(Op("perm",[Anno(Op("d0",[]),Wld)]),Wld)),Seq(Build(Anno(Op("ppreduce",[Anno(Op("p",[Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[])),Anno(Op("nilP",[]),Op("Nil",[]))]),Op("Nil",[]))),CallT(SVar("n_69"),[],[]))),Id,GuardedLChoice(Seq(Match(Anno(Op("perm",[Anno(Op("s",[Anno(Op("d0",[]),Wld)]),Wld)]),Wld)),Seq(Build(Anno(Op("ppreduce",[Anno(Op("p",[Anno(Op("ll",[Anno(Op("l",[Anno(Op("s",[Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[])),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[])),Anno(Op("nilP",[]),Op("Nil",[]))]),Op("Nil",[]))),CallT(SVar("n_69"),[],[]))),Id,GuardedLChoice(Scope(["v_67","w_67","x_67"],Seq(Match(Anno(Op("perm",[Anno(Op("s",[Var("v_67")]),Wld)]),Wld)),Seq(Match(Var("x_67")),Seq(Build(Anno(Op("perm",[Var("v_67")]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("w_67")),Seq(Build(Var("x_67")),Seq(Build(Anno(Op("insert1",[Anno(Op("s",[Var("v_67")]),Op("Nil",[])),Var("w_67")]),Op("Nil",[]))),CallT(SVar("n_69"),[],[]))))))))),Id,GuardedLChoice(Scope(["y_67","z_67","a_68","b_68","c_68","d_68","e_68"],Seq(Match(Anno(Op("insert1",[Var("z_67"),Anno(Op("pp",[Anno(Op("p",[Var("y_67")]),Wld),Var("a_68")]),Wld)]),Wld)),Seq(Match(Var("c_68")),Seq(Build(Anno(Op("insert0",[Var("z_67"),Var("y_67")]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("b_68")),Seq(Build(Var("c_68")),Seq(Seq(Match(Var("e_68")),Seq(Build(Anno(Op("insert1",[Var("z_67"),Var("a_68")]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("d_68")),Seq(Build(Var("e_68")),Build(Anno(Op("ppreduce",[Var("b_68"),Var("d_68")]),Op("Nil",[])))))))),CallT(SVar("n_69"),[],[]))))))))),Id,GuardedLChoice(Scope(["f_68","g_68"],Seq(Match(Anno(Op("insert1",[Var("f_68"),Anno(Op("p",[Var("g_68")]),Wld)]),Wld)),Seq(Build(Anno(Op("insert0",[Var("f_68"),Var("g_68")]),Op("Nil",[]))),CallT(SVar("n_69"),[],[])))),Id,GuardedLChoice(Scope(["h_68"],Seq(Match(Anno(Op("insert1",[Var("h_68"),Anno(Op("nilP",[]),Wld)]),Wld)),Build(Anno(Op("nilP",[]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["i_68","j_68","k_68","l_68","m_68","n_68","o_68"],Seq(Match(Anno(Op("insert0",[Var("j_68"),Anno(Op("ll",[Anno(Op("l",[Var("i_68")]),Wld),Var("k_68")]),Wld)]),Wld)),Seq(Match(Var("m_68")),Seq(Match(Var("o_68")),Seq(Build(Anno(Op("insert0",[Var("j_68"),Var("k_68")]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("n_68")),Seq(Build(Var("o_68")),Seq(Build(Anno(Op("map_cons",[Var("i_68"),Var("n_68")]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("l_68")),Seq(Build(Var("m_68")),Seq(Build(Anno(Op("ppreduce",[Anno(Op("p",[Anno(Op("ll",[Anno(Op("l",[Var("j_68")]),Op("Nil",[])),Anno(Op("ll",[Anno(Op("l",[Var("i_68")]),Op("Nil",[])),Var("k_68")]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[])),Var("l_68")]),Op("Nil",[]))),CallT(SVar("n_69"),[],[])))))))))))))),Id,GuardedLChoice(Scope(["p_68"],Seq(Match(Anno(Op("insert0",[Var("p_68"),Anno(Op("nil",[]),Wld)]),Wld)),Seq(Build(Anno(Op("ppreduce",[Anno(Op("p",[Anno(Op("ll",[Anno(Op("l",[Var("p_68")]),Op("Nil",[])),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[])),Anno(Op("nilP",[]),Op("Nil",[]))]),Op("Nil",[]))),CallT(SVar("n_69"),[],[])))),Id,GuardedLChoice(Scope(["q_68","r_68","s_68","t_68","u_68"],Seq(Match(Anno(Op("map_cons",[Var("r_68"),Anno(Op("pp",[Anno(Op("p",[Var("q_68")]),Wld),Var("s_68")]),Wld)]),Wld)),Seq(Match(Var("u_68")),Seq(Build(Anno(Op("map_cons",[Var("r_68"),Var("s_68")]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("t_68")),Seq(Build(Var("u_68")),Seq(Build(Anno(Op("ppreduce",[Anno(Op("p",[Anno(Op("ll",[Anno(Op("l",[Var("r_68")]),Op("Nil",[])),Var("q_68")]),Op("Nil",[]))]),Op("Nil",[])),Var("t_68")]),Op("Nil",[]))),CallT(SVar("n_69"),[],[]))))))))),Id,GuardedLChoice(Scope(["v_68","w_68"],Seq(Match(Anno(Op("map_cons",[Var("v_68"),Anno(Op("p",[Var("w_68")]),Wld)]),Wld)),Build(Anno(Op("p",[Anno(Op("ll",[Anno(Op("l",[Var("v_68")]),Op("Nil",[])),Var("w_68")]),Op("Nil",[]))]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["x_68"],Seq(Match(Anno(Op("map_cons",[Var("x_68"),Anno(Op("nilP",[]),Wld)]),Wld)),Build(Anno(Op("nilP",[]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["y_68"],Seq(Match(Anno(Op("ppreduce",[Anno(Op("nilP",[]),Wld),Var("y_68")]),Wld)),Build(Var("y_68")))),Id,GuardedLChoice(Scope(["z_68"],Seq(Match(Anno(Op("ppreduce",[Var("z_68"),Anno(Op("nilP",[]),Wld)]),Wld)),Build(Var("z_68")))),Id,GuardedLChoice(Scope(["a_69","b_69","c_69","d_69"],Seq(Match(Anno(Op("ppreduce",[Var("a_69"),Var("b_69")]),Wld)),Seq(Match(Var("d_69")),Seq(Build(Anno(Op("ppflat",[Var("b_69"),Anno(Op("nilP",[]),Op("Nil",[]))]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("c_69")),Seq(Build(Var("d_69")),Seq(Build(Anno(Op("ppflat",[Var("a_69"),Var("c_69")]),Op("Nil",[]))),CallT(SVar("n_69"),[],[]))))))))),Id,GuardedLChoice(Scope(["e_69"],Seq(Match(Anno(Op("ppflat",[Anno(Op("nilP",[]),Wld),Var("e_69")]),Wld)),Build(Var("e_69")))),Id,GuardedLChoice(Scope(["f_69","g_69"],Seq(Match(Anno(Op("ppflat",[Anno(Op("p",[Var("f_69")]),Wld),Var("g_69")]),Wld)),Build(Anno(Op("pp",[Anno(Op("p",[Var("f_69")]),Op("Nil",[])),Var("g_69")]),Op("Nil",[]))))),Id,Scope(["h_69","i_69","j_69","k_69","l_69"],Seq(Match(Anno(Op("ppflat",[Anno(Op("pp",[Var("h_69"),Var("i_69")]),Wld),Var("j_69")]),Wld)),Seq(Match(Var("l_69")),Seq(Build(Anno(Op("ppflat",[Var("i_69"),Var("j_69")]),Op("Nil",[]))),Seq(CallT(SVar("n_69"),[],[]),Seq(Match(Var("k_69")),Seq(Build(Var("l_69")),Seq(Build(Anno(Op("ppflat",[Var("h_69"),Var("k_69")]),Op("Nil",[]))),CallT(SVar("n_69"),[],[]))))))))))))))))))))))))),Id,Id))],CallT(SVar("m_69"),[CallT(SVar("n_69"),[],[])],[]))],[])),SDefT("eval_and_print_0_0",[],[],Seq(CallT(SVar("eval_0_0"),[],[]),CallT(SVar("debug_1_0"),[Build(Anno(Str("result = "),Op("Nil",[])))],[]))),SDefT("main_0_0",[],[],Seq(Build(Anno(Op("perm",[Anno(Op("s",[Anno(Op("s",[Anno(Op("s",[Anno(Op("s",[Anno(Op("s",[Anno(Op("s",[Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[]))),Seq(CallT(SVar("eval_and_print_0_0"),[],[]),Seq(Build(Anno(Int("0"),Op("Nil",[]))),CallT(SVar("exit_0_0"),[],[]))))),ExtSDef("debug_1_0",[VarDec("y_15",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("exit_0_0",[],[]),ExtSDef("memo_1_0",[VarDec("k_24",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[])])])