garbagecollection.ctree 5.82 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("p",ConstType(Sort("Nat",[]))),OpDecl("n",ConstType(Sort("Nat",[]))),OpDecl("d1",ConstType(Sort("Nat",[]))),OpDecl("f",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[])))),OpDecl("c",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[]))))])]),Strategies([SDefT("eval_0_0",[],[],CallT(SVar("memo_1_0"),[Let([SDefT("c_67",[VarDec("e_67",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(All(CallT(SVar("c_67"),[CallT(SVar("e_67"),[],[])],[])),CallT(SVar("e_67"),[],[]))),SDefT("d_67",[],[],GuardedLChoice(GuardedLChoice(Seq(Match(Anno(Op("d1",[]),Wld)),Build(Anno(Op("s",[Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[])))),Id,GuardedLChoice(Scope(["t_65"],Seq(Match(Anno(Op("c",[Anno(Op("d0",[]),Wld),Var("t_65")]),Wld)),Build(Var("t_65")))),Id,GuardedLChoice(Scope(["u_65","v_65","w_65","x_65"],Seq(Match(Anno(Op("c",[Anno(Op("s",[Var("u_65")]),Wld),Var("v_65")]),Wld)),Seq(Match(Var("x_65")),Seq(Build(Anno(Op("c",[Var("u_65"),Var("v_65")]),Op("Nil",[]))),Seq(CallT(SVar("d_67"),[],[]),Seq(Match(Var("w_65")),Seq(Build(Var("x_65")),Build(Anno(Op("s",[Var("w_65")]),Op("Nil",[])))))))))),Id,GuardedLChoice(Scope(["y_65","z_65","a_66","b_66","c_66","d_66","e_66"],Seq(Match(Anno(Op("f",[Var("y_65"),Var("z_65"),Anno(Op("s",[Var("a_66")]),Wld),Var("b_66"),Var("c_66")]),Wld)),Seq(Match(Var("e_66")),Seq(Build(Anno(Op("c",[Var("b_66"),Var("b_66")]),Op("Nil",[]))),Seq(CallT(SVar("d_67"),[],[]),Seq(Match(Var("d_66")),Seq(Build(Var("e_66")),Seq(Build(Anno(Op("f",[Var("y_65"),Var("z_65"),Var("a_66"),Var("d_66"),Var("c_66")]),Op("Nil",[]))),CallT(SVar("d_67"),[],[]))))))))),Id,GuardedLChoice(Scope(["f_66","g_66","h_66","i_66"],Seq(Match(Anno(Op("f",[Var("g_66"),Anno(Op("s",[Var("h_66")]),Wld),Anno(Op("d0",[]),Wld),Var("i_66"),Var("f_66")]),Wld)),Seq(Build(Anno(Op("f",[Var("g_66"),Var("h_66"),Anno(Op("p",[]),Op("Nil",[])),Var("i_66"),Var("i_66")]),Op("Nil",[]))),CallT(SVar("d_67"),[],[])))),Id,GuardedLChoice(Scope(["j_66","k_66","l_66","m_66","n_66"],Seq(Match(Anno(Op("f",[Anno(Op("s",[Var("l_66")]),Wld),Anno(Op("d0",[]),Wld),Anno(Op("d0",[]),Wld),Var("j_66"),Var("k_66")]),Wld)),Seq(Match(Var("n_66")),Seq(Build(Anno(Op("d1",[]),Op("Nil",[]))),Seq(CallT(SVar("d_67"),[],[]),Seq(Match(Var("m_66")),Seq(Build(Var("n_66")),Seq(Build(Anno(Op("f",[Var("l_66"),Anno(Op("n",[]),Op("Nil",[])),Anno(Op("p",[]),Op("Nil",[])),Var("m_66"),Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[]))),CallT(SVar("d_67"),[],[]))))))))),Id,GuardedLChoice(Scope(["o_66","p_66"],Seq(Match(Anno(Op("f",[Anno(Op("d0",[]),Wld),Anno(Op("d0",[]),Wld),Anno(Op("d0",[]),Wld),Var("p_66"),Var("o_66")]),Wld)),Build(Var("p_66")))),Id,GuardedLChoice(Scope(["q_66","r_66","s_66","t_66"],Seq(Match(Anno(Op("f",[Var("q_66"),Anno(Op("s",[Var("r_66")]),Wld),Anno(Op("p",[]),Wld),Var("s_66"),Var("t_66")]),Wld)),Seq(Build(Anno(Op("f",[Var("q_66"),Var("r_66"),Anno(Op("p",[]),Op("Nil",[])),Var("s_66"),Anno(Op("s",[Var("t_66")]),Op("Nil",[]))]),Op("Nil",[]))),CallT(SVar("d_67"),[],[])))),Id,GuardedLChoice(Scope(["u_66","v_66","w_66"],Seq(Match(Anno(Op("f",[Var("u_66"),Anno(Op("d0",[]),Wld),Anno(Op("p",[]),Wld),Var("v_66"),Var("w_66")]),Wld)),Seq(Build(Anno(Op("f",[Var("u_66"),Anno(Op("n",[]),Op("Nil",[])),Anno(Op("p",[]),Op("Nil",[])),Anno(Op("s",[Var("v_66")]),Op("Nil",[])),Var("w_66")]),Op("Nil",[]))),CallT(SVar("d_67"),[],[])))),Id,GuardedLChoice(Scope(["x_66","y_66","z_66"],Seq(Match(Anno(Op("f",[Anno(Op("s",[Var("x_66")]),Wld),Anno(Op("n",[]),Wld),Anno(Op("p",[]),Wld),Var("y_66"),Var("z_66")]),Wld)),Seq(Build(Anno(Op("f",[Var("x_66"),Anno(Op("n",[]),Op("Nil",[])),Anno(Op("p",[]),Op("Nil",[])),Var("y_66"),Var("z_66")]),Op("Nil",[]))),CallT(SVar("d_67"),[],[])))),Id,Scope(["a_67","b_67"],Seq(Match(Anno(Op("f",[Anno(Op("d0",[]),Wld),Anno(Op("n",[]),Wld),Anno(Op("p",[]),Wld),Var("a_67"),Var("b_67")]),Wld)),Build(Var("b_67")))))))))))))),Id,Id))],CallT(SVar("c_67"),[CallT(SVar("d_67"),[],[])],[]))],[])),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("f",[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",[])),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",[])),Anno(Op("s",[Anno(Op("s",[Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[])),Anno(Op("d0",[]),Op("Nil",[])),Anno(Op("d1",[]),Op("Nil",[]))]),Op("Nil",[]))),Seq(CallT(SVar("eval_and_print_0_0"),[],[]),Seq(Build(Anno(Op("f",[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",[])),Anno(Op("s",[Anno(Op("s",[Anno(Op("s",[Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[]))]),Op("Nil",[])),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",[])),Anno(Op("d0",[]),Op("Nil",[])),Anno(Op("d1",[]),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("g_15",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("exit_0_0",[],[]),ExtSDef("memo_1_0",[VarDec("s_23",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[])])])