mergesort1000.ctree 11 KB
Newer Older
1
Specification([Signature([Constructors([ExtOpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),OpDecl("true",ConstType(Sort("Bool",[]))),OpDecl("false",ConstType(Sort("Bool",[]))),OpDecl("d0",ConstType(Sort("Nat",[]))),OpDecl("s",FunType([ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[])))),OpDecl("nil",ConstType(Sort("NatList",[]))),OpDecl("cons",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("NatList",[]))],ConstType(Sort("NatList",[])))),OpDecl("pair",FunType([ConstType(Sort("NatList",[])),ConstType(Sort("NatList",[]))],ConstType(Sort("ListPair",[])))),OpDecl("d10",ConstType(Sort("Nat",[]))),OpDecl("lte",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[]))],ConstType(Sort("Bool",[])))),OpDecl("plus",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[])))),OpDecl("times",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[])))),OpDecl("rev",FunType([ConstType(Sort("Nat",[]))],ConstType(Sort("NatList",[])))),OpDecl("split",FunType([ConstType(Sort("NatList",[]))],ConstType(Sort("ListPair",[])))),OpDecl("merge",FunType([ConstType(Sort("NatList",[])),ConstType(Sort("NatList",[]))],ConstType(Sort("NatList",[])))),OpDecl("mergesort",FunType([ConstType(Sort("NatList",[]))],ConstType(Sort("NatList",[])))),OpDecl("p1",FunType([ConstType(Sort("ListPair",[]))],ConstType(Sort("NatList",[])))),OpDecl("p2",FunType([ConstType(Sort("ListPair",[]))],ConstType(Sort("NatList",[]))))])]),Strategies([SDefT("eval_0_0",[],[],CallT(SVar("memo_1_0"),[Let([SDefT("r_72",[VarDec("t_72",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(All(CallT(SVar("r_72"),[CallT(SVar("t_72"),[],[])],[])),CallT(SVar("t_72"),[],[]))),SDefT("s_72",[],[],GuardedLChoice(GuardedLChoice(Seq(Match(Anno(Op("d10",[]),Wld)),Build(Anno(Op("s",[Anno(Op("s",[Anno(Op("s",[Anno(Op("s",[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",[]))]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["w_69"],Seq(Match(Anno(Op("lte",[Anno(Op("d0",[]),Wld),Anno(Op("s",[Var("w_69")]),Wld)]),Wld)),Build(Anno(Op("true",[]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["x_69"],Seq(Match(Anno(Op("lte",[Anno(Op("s",[Var("x_69")]),Wld),Anno(Op("d0",[]),Wld)]),Wld)),Build(Anno(Op("false",[]),Op("Nil",[]))))),Id,GuardedLChoice(Seq(Match(Anno(Op("lte",[Anno(Op("d0",[]),Wld),Anno(Op("d0",[]),Wld)]),Wld)),Build(Anno(Op("true",[]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["y_69","z_69"],Seq(Match(Anno(Op("lte",[Anno(Op("s",[Var("y_69")]),Wld),Anno(Op("s",[Var("z_69")]),Wld)]),Wld)),Seq(Build(Anno(Op("lte",[Var("y_69"),Var("z_69")]),Op("Nil",[]))),CallT(SVar("s_72"),[],[])))),Id,GuardedLChoice(Scope(["a_70"],Seq(Match(Anno(Op("plus",[Anno(Op("d0",[]),Wld),Var("a_70")]),Wld)),Build(Var("a_70")))),Id,GuardedLChoice(Scope(["b_70","c_70","d_70","e_70"],Seq(Match(Anno(Op("plus",[Anno(Op("s",[Var("b_70")]),Wld),Var("c_70")]),Wld)),Seq(Match(Var("e_70")),Seq(Build(Anno(Op("plus",[Var("b_70"),Var("c_70")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("d_70")),Seq(Build(Var("e_70")),Build(Anno(Op("s",[Var("d_70")]),Op("Nil",[])))))))))),Id,GuardedLChoice(Scope(["f_70"],Seq(Match(Anno(Op("times",[Anno(Op("d0",[]),Wld),Var("f_70")]),Wld)),Build(Anno(Op("d0",[]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["g_70","h_70","i_70","j_70"],Seq(Match(Anno(Op("times",[Anno(Op("s",[Var("g_70")]),Wld),Var("h_70")]),Wld)),Seq(Match(Var("j_70")),Seq(Build(Anno(Op("times",[Var("g_70"),Var("h_70")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("i_70")),Seq(Build(Var("j_70")),Seq(Build(Anno(Op("plus",[Var("h_70"),Var("i_70")]),Op("Nil",[]))),CallT(SVar("s_72"),[],[]))))))))),Id,GuardedLChoice(Scope(["k_70","l_70","m_70"],Seq(Match(Anno(Op("rev",[Anno(Op("s",[Var("k_70")]),Wld)]),Wld)),Seq(Match(Var("m_70")),Seq(Build(Anno(Op("rev",[Var("k_70")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("l_70")),Seq(Build(Var("m_70")),Build(Anno(Op("cons",[Anno(Op("s",[Var("k_70")]),Op("Nil",[])),Var("l_70")]),Op("Nil",[])))))))))),Id,GuardedLChoice(Seq(Match(Anno(Op("rev",[Anno(Op("d0",[]),Wld)]),Wld)),Build(Anno(Op("cons",[Anno(Op("d0",[]),Op("Nil",[])),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["n_70"],Seq(Match(Anno(Op("merge",[Anno(Op("nil",[]),Wld),Var("n_70")]),Wld)),Build(Var("n_70")))),Id,GuardedLChoice(Scope(["o_70"],Seq(Match(Anno(Op("merge",[Var("o_70"),Anno(Op("nil",[]),Wld)]),Wld)),Build(Var("o_70")))),Id,GuardedLChoice(Scope(["p_70","q_70","r_70","s_70","t_70","u_70","v_70","w_70","x_70","y_70","z_70"],Seq(Match(Anno(Op("merge",[Anno(Op("cons",[Var("r_70"),Var("p_70")]),Wld),Anno(Op("cons",[Var("s_70"),Var("q_70")]),Wld)]),Wld)),Seq(Match(Var("t_70")),Seq(Match(Var("w_70")),Seq(Build(Anno(Op("lte",[Var("r_70"),Var("s_70")]),Op("Nil",[]))),Seq(Match(Var("u_70")),Seq(Build(Var("w_70")),Seq(Match(Var("x_70")),Seq(Build(Anno(Op("true",[]),Op("Nil",[]))),Seq(Match(Var("v_70")),Seq(Build(Var("x_70")),Seq(CallT(SVar("equal_after_eval_0_2"),[],[Var("u_70"),Var("v_70")]),Seq(Build(Var("t_70")),Seq(Match(Var("z_70")),Seq(Build(Anno(Op("merge",[Var("p_70"),Anno(Op("cons",[Var("s_70"),Var("q_70")]),Op("Nil",[]))]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("y_70")),Seq(Build(Var("z_70")),Build(Anno(Op("cons",[Var("r_70"),Var("y_70")]),Op("Nil",[]))))))))))))))))))))),Id,GuardedLChoice(Scope(["a_71","b_71","c_71","d_71","e_71","f_71","g_71","h_71","i_71","j_71","k_71"],Seq(Match(Anno(Op("merge",[Anno(Op("cons",[Var("c_71"),Var("a_71")]),Wld),Anno(Op("cons",[Var("d_71"),Var("b_71")]),Wld)]),Wld)),Seq(Match(Var("e_71")),Seq(Match(Var("h_71")),Seq(Build(Anno(Op("lte",[Var("c_71"),Var("d_71")]),Op("Nil",[]))),Seq(Match(Var("f_71")),Seq(Build(Var("h_71")),Seq(Match(Var("i_71")),Seq(Build(Anno(Op("false",[]),Op("Nil",[]))),Seq(Match(Var("g_71")),Seq(Build(Var("i_71")),Seq(CallT(SVar("equal_after_eval_0_2"),[],[Var("f_71"),Var("g_71")]),Seq(Build(Var("e_71")),Seq(Match(Var("k_71")),Seq(Build(Anno(Op("merge",[Anno(Op("cons",[Var("c_71"),Var("a_71")]),Op("Nil",[])),Var("b_71")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("j_71")),Seq(Build(Var("k_71")),Build(Anno(Op("cons",[Var("d_71"),Var("j_71")]),Op("Nil",[]))))))))))))))))))))),Id,GuardedLChoice(Scope(["l_71","m_71","n_71","o_71","p_71","q_71","r_71","s_71","t_71","u_71","v_71"],Seq(Match(Anno(Op("split",[Anno(Op("cons",[Var("l_71"),Anno(Op("cons",[Var("m_71"),Var("n_71")]),Wld)]),Wld)]),Wld)),Seq(Match(Var("p_71")),Seq(Match(Var("r_71")),Seq(Build(Anno(Op("split",[Var("n_71")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("q_71")),Seq(Build(Var("r_71")),Seq(Build(Anno(Op("p1",[Var("q_71")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("o_71")),Seq(Build(Var("p_71")),Seq(Match(Var("t_71")),Seq(Match(Var("v_71")),Seq(Build(Anno(Op("split",[Var("n_71")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("u_71")),Seq(Build(Var("v_71")),Seq(Build(Anno(Op("p2",[Var("u_71")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("s_71")),Seq(Build(Var("t_71")),Build(Anno(Op("pair",[Anno(Op("cons",[Var("l_71"),Var("o_71")]),Op("Nil",[])),Anno(Op("cons",[Var("m_71"),Var("s_71")]),Op("Nil",[]))]),Op("Nil",[]))))))))))))))))))))))))),Id,GuardedLChoice(Seq(Match(Anno(Op("split",[Anno(Op("nil",[]),Wld)]),Wld)),Build(Anno(Op("pair",[Anno(Op("nil",[]),Op("Nil",[])),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["w_71"],Seq(Match(Anno(Op("split",[Anno(Op("cons",[Var("w_71"),Anno(Op("nil",[]),Wld)]),Wld)]),Wld)),Build(Anno(Op("pair",[Anno(Op("cons",[Var("w_71"),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[])),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[]))))),Id,GuardedLChoice(Seq(Match(Anno(Op("mergesort",[Anno(Op("nil",[]),Wld)]),Wld)),Build(Anno(Op("nil",[]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["x_71"],Seq(Match(Anno(Op("mergesort",[Anno(Op("cons",[Var("x_71"),Anno(Op("nil",[]),Wld)]),Wld)]),Wld)),Build(Anno(Op("cons",[Var("x_71"),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["y_71","z_71","a_72","b_72","c_72","d_72","e_72","f_72","g_72","h_72","i_72","j_72","k_72","l_72","m_72"],Seq(Match(Anno(Op("mergesort",[Anno(Op("cons",[Var("y_71"),Anno(Op("cons",[Var("z_71"),Var("a_72")]),Wld)]),Wld)]),Wld)),Seq(Match(Var("c_72")),Seq(Match(Var("e_72")),Seq(Match(Var("g_72")),Seq(Build(Anno(Op("split",[Var("a_72")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("f_72")),Seq(Build(Var("g_72")),Seq(Build(Anno(Op("p1",[Var("f_72")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("d_72")),Seq(Build(Var("e_72")),Seq(Build(Anno(Op("mergesort",[Anno(Op("cons",[Var("y_71"),Var("d_72")]),Op("Nil",[]))]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("b_72")),Seq(Build(Var("c_72")),Seq(Seq(Match(Var("i_72")),Seq(Match(Var("k_72")),Seq(Match(Var("m_72")),Seq(Build(Anno(Op("split",[Var("a_72")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("l_72")),Seq(Build(Var("m_72")),Seq(Build(Anno(Op("p2",[Var("l_72")]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("j_72")),Seq(Build(Var("k_72")),Seq(Build(Anno(Op("mergesort",[Anno(Op("cons",[Var("z_71"),Var("j_72")]),Op("Nil",[]))]),Op("Nil",[]))),Seq(CallT(SVar("s_72"),[],[]),Seq(Match(Var("h_72")),Seq(Build(Var("i_72")),Build(Anno(Op("merge",[Var("b_72"),Var("h_72")]),Op("Nil",[])))))))))))))))))),CallT(SVar("s_72"),[],[]))))))))))))))))))),Id,GuardedLChoice(Scope(["n_72","o_72"],Seq(Match(Anno(Op("p1",[Anno(Op("pair",[Var("o_72"),Var("n_72")]),Wld)]),Wld)),Build(Var("o_72")))),Id,Scope(["p_72","q_72"],Seq(Match(Anno(Op("p2",[Anno(Op("pair",[Var("p_72"),Var("q_72")]),Wld)]),Wld)),Build(Var("q_72")))))))))))))))))))))))))),Id,Id))],CallT(SVar("r_72"),[CallT(SVar("s_72"),[],[])],[]))],[])),SDefT("equal_after_eval_0_2",[],[VarDec("k_2",ConstType(Sort("ATerm",[]))),VarDec("l_2",ConstType(Sort("ATerm",[])))],Scope(["m_2","n_2","o_2","p_2"],Seq(Match(Var("o_2")),Seq(Build(Var("k_2")),Seq(CallT(SVar("eval_0_0"),[],[]),Seq(Match(Var("m_2")),Seq(Build(Var("o_2")),Seq(Match(Var("p_2")),Seq(Build(Var("l_2")),Seq(CallT(SVar("eval_0_0"),[],[]),Seq(Match(Var("n_2")),Seq(Build(Var("p_2")),CallT(SVar("equal_0_2"),[],[Var("m_2"),Var("n_2")]))))))))))))),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("mergesort",[Anno(Op("rev",[Anno(Op("times",[Anno(Op("d10",[]),Op("Nil",[])),Anno(Op("times",[Anno(Op("d10",[]),Op("Nil",[])),Anno(Op("d10",[]),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("u_16",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("exit_0_0",[],[]),ExtSDef("memo_1_0",[VarDec("g_25",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("equal_0_2",[],[VarDec("a_26",ConstType(Sort("ATerm",[]))),VarDec("b_26",ConstType(Sort("ATerm",[])))])])])