bubblesort720.ctree 7.62 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("d10",ConstType(Sort("Nat",[]))),OpDecl("lt",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[]))],ConstType(Sort("Bool",[])))),OpDecl("bubsort",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("NatList",[]))],ConstType(Sort("NatList",[])))),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("fact",FunType([ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[]))))])]),Strategies([SDefT("eval_0_0",[],[],CallT(SVar("memo_1_0"),[Let([SDefT("t_68",[VarDec("v_68",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(All(CallT(SVar("t_68"),[CallT(SVar("v_68"),[],[])],[])),CallT(SVar("v_68"),[],[]))),SDefT("u_68",[],[],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(Seq(Match(Anno(Op("lt",[Anno(Op("d0",[]),Wld),Anno(Op("d0",[]),Wld)]),Wld)),Build(Anno(Op("false",[]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["e_67"],Seq(Match(Anno(Op("lt",[Anno(Op("d0",[]),Wld),Anno(Op("s",[Var("e_67")]),Wld)]),Wld)),Build(Anno(Op("true",[]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["f_67"],Seq(Match(Anno(Op("lt",[Anno(Op("s",[Var("f_67")]),Wld),Anno(Op("d0",[]),Wld)]),Wld)),Build(Anno(Op("false",[]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["g_67","h_67"],Seq(Match(Anno(Op("lt",[Anno(Op("s",[Var("g_67")]),Wld),Anno(Op("s",[Var("h_67")]),Wld)]),Wld)),Seq(Build(Anno(Op("lt",[Var("g_67"),Var("h_67")]),Op("Nil",[]))),CallT(SVar("u_68"),[],[])))),Id,GuardedLChoice(Scope(["i_67"],Seq(Match(Anno(Op("plus",[Anno(Op("d0",[]),Wld),Var("i_67")]),Wld)),Build(Var("i_67")))),Id,GuardedLChoice(Scope(["j_67","k_67","l_67","m_67"],Seq(Match(Anno(Op("plus",[Anno(Op("s",[Var("j_67")]),Wld),Var("k_67")]),Wld)),Seq(Match(Var("m_67")),Seq(Build(Anno(Op("plus",[Var("j_67"),Var("k_67")]),Op("Nil",[]))),Seq(CallT(SVar("u_68"),[],[]),Seq(Match(Var("l_67")),Seq(Build(Var("m_67")),Build(Anno(Op("s",[Var("l_67")]),Op("Nil",[])))))))))),Id,GuardedLChoice(Scope(["n_67"],Seq(Match(Anno(Op("times",[Anno(Op("d0",[]),Wld),Var("n_67")]),Wld)),Build(Anno(Op("d0",[]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["o_67","p_67","q_67","r_67"],Seq(Match(Anno(Op("times",[Anno(Op("s",[Var("o_67")]),Wld),Var("p_67")]),Wld)),Seq(Match(Var("r_67")),Seq(Build(Anno(Op("times",[Var("o_67"),Var("p_67")]),Op("Nil",[]))),Seq(CallT(SVar("u_68"),[],[]),Seq(Match(Var("q_67")),Seq(Build(Var("r_67")),Seq(Build(Anno(Op("plus",[Var("p_67"),Var("q_67")]),Op("Nil",[]))),CallT(SVar("u_68"),[],[]))))))))),Id,GuardedLChoice(Seq(Match(Anno(Op("fact",[Anno(Op("d0",[]),Wld)]),Wld)),Build(Anno(Op("s",[Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["s_67","t_67","u_67"],Seq(Match(Anno(Op("fact",[Anno(Op("s",[Var("s_67")]),Wld)]),Wld)),Seq(Match(Var("u_67")),Seq(Build(Anno(Op("fact",[Var("s_67")]),Op("Nil",[]))),Seq(CallT(SVar("u_68"),[],[]),Seq(Match(Var("t_67")),Seq(Build(Var("u_67")),Seq(Build(Anno(Op("times",[Anno(Op("s",[Var("s_67")]),Op("Nil",[])),Var("t_67")]),Op("Nil",[]))),CallT(SVar("u_68"),[],[]))))))))),Id,GuardedLChoice(Scope(["v_67","w_67","x_67"],Seq(Match(Anno(Op("rev",[Anno(Op("s",[Var("v_67")]),Wld)]),Wld)),Seq(Match(Var("x_67")),Seq(Build(Anno(Op("rev",[Var("v_67")]),Op("Nil",[]))),Seq(CallT(SVar("u_68"),[],[]),Seq(Match(Var("w_67")),Seq(Build(Var("x_67")),Seq(Build(Anno(Op("bubsort",[Anno(Op("s",[Var("v_67")]),Op("Nil",[])),Var("w_67")]),Op("Nil",[]))),CallT(SVar("u_68"),[],[]))))))))),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(["y_67"],Seq(Match(Anno(Op("bubsort",[Var("y_67"),Anno(Op("nil",[]),Wld)]),Wld)),Build(Anno(Op("cons",[Var("y_67"),Anno(Op("nil",[]),Op("Nil",[]))]),Op("Nil",[]))))),Id,GuardedLChoice(Scope(["z_67","a_68","b_68","c_68","d_68","e_68","f_68","g_68","h_68","i_68"],Seq(Match(Anno(Op("bubsort",[Var("b_68"),Anno(Op("cons",[Var("a_68"),Var("z_67")]),Wld)]),Wld)),Seq(Match(Var("c_68")),Seq(Match(Var("f_68")),Seq(Build(Anno(Op("lt",[Var("a_68"),Var("b_68")]),Op("Nil",[]))),Seq(Match(Var("d_68")),Seq(Build(Var("f_68")),Seq(Match(Var("g_68")),Seq(Build(Anno(Op("true",[]),Op("Nil",[]))),Seq(Match(Var("e_68")),Seq(Build(Var("g_68")),Seq(CallT(SVar("equal_after_eval_0_2"),[],[Var("d_68"),Var("e_68")]),Seq(Build(Var("c_68")),Seq(Match(Var("i_68")),Seq(Build(Anno(Op("bubsort",[Var("b_68"),Var("z_67")]),Op("Nil",[]))),Seq(CallT(SVar("u_68"),[],[]),Seq(Match(Var("h_68")),Seq(Build(Var("i_68")),Build(Anno(Op("cons",[Var("a_68"),Var("h_68")]),Op("Nil",[]))))))))))))))))))))),Id,Scope(["j_68","k_68","l_68","m_68","n_68","o_68","p_68","q_68","r_68","s_68"],Seq(Match(Anno(Op("bubsort",[Var("l_68"),Anno(Op("cons",[Var("k_68"),Var("j_68")]),Wld)]),Wld)),Seq(Match(Var("m_68")),Seq(Match(Var("p_68")),Seq(Build(Anno(Op("lt",[Var("k_68"),Var("l_68")]),Op("Nil",[]))),Seq(Match(Var("n_68")),Seq(Build(Var("p_68")),Seq(Match(Var("q_68")),Seq(Build(Anno(Op("false",[]),Op("Nil",[]))),Seq(Match(Var("o_68")),Seq(Build(Var("q_68")),Seq(CallT(SVar("equal_after_eval_0_2"),[],[Var("n_68"),Var("o_68")]),Seq(Build(Var("m_68")),Seq(Match(Var("s_68")),Seq(Build(Anno(Op("bubsort",[Var("k_68"),Var("j_68")]),Op("Nil",[]))),Seq(CallT(SVar("u_68"),[],[]),Seq(Match(Var("r_68")),Seq(Build(Var("s_68")),Build(Anno(Op("cons",[Var("l_68"),Var("r_68")]),Op("Nil",[])))))))))))))))))))))))))))))))))))),Id,Id))],CallT(SVar("t_68"),[CallT(SVar("u_68"),[],[])],[]))],[])),SDefT("equal_after_eval_0_2",[],[VarDec("r_1",ConstType(Sort("ATerm",[]))),VarDec("s_1",ConstType(Sort("ATerm",[])))],Scope(["t_1","u_1","v_1","w_1"],Seq(Match(Var("v_1")),Seq(Build(Var("r_1")),Seq(CallT(SVar("eval_0_0"),[],[]),Seq(Match(Var("t_1")),Seq(Build(Var("v_1")),Seq(Match(Var("w_1")),Seq(Build(Var("s_1")),Seq(CallT(SVar("eval_0_0"),[],[]),Seq(Match(Var("u_1")),Seq(Build(Var("w_1")),CallT(SVar("equal_0_2"),[],[Var("t_1"),Var("u_1")]))))))))))))),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("rev",[Anno(Op("fact",[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",[]))),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("w_15",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("exit_0_0",[],[]),ExtSDef("memo_1_0",[VarDec("i_24",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("equal_0_2",[],[VarDec("c_25",ConstType(Sort("ATerm",[]))),VarDec("d_25",ConstType(Sort("ATerm",[])))])])])