fibonacci05.ctree 4.1 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("plus",FunType([ConstType(Sort("Nat",[])),ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[])))),OpDecl("fibb",FunType([ConstType(Sort("Nat",[]))],ConstType(Sort("Nat",[]))))])]),Strategies([SDefT("eval_0_0",[],[],CallT(SVar("memo_1_0"),[Let([SDefT("p_63",[VarDec("r_63",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[],Seq(All(CallT(SVar("p_63"),[CallT(SVar("r_63"),[],[])],[])),CallT(SVar("r_63"),[],[]))),SDefT("q_63",[],[],GuardedLChoice(GuardedLChoice(Scope(["f_63"],Seq(Match(Anno(Op("plus",[Anno(Op("d0",[]),Wld),Var("f_63")]),Wld)),Build(Var("f_63")))),Id,GuardedLChoice(Scope(["g_63","h_63","i_63","j_63"],Seq(Match(Anno(Op("plus",[Anno(Op("s",[Var("g_63")]),Wld),Var("h_63")]),Wld)),Seq(Match(Var("j_63")),Seq(Build(Anno(Op("plus",[Var("g_63"),Var("h_63")]),Op("Nil",[]))),Seq(CallT(SVar("q_63"),[],[]),Seq(Match(Var("i_63")),Seq(Build(Var("j_63")),Build(Anno(Op("s",[Var("i_63")]),Op("Nil",[])))))))))),Id,GuardedLChoice(Seq(Match(Anno(Op("fibb",[Anno(Op("d0",[]),Wld)]),Wld)),Build(Anno(Op("d0",[]),Op("Nil",[])))),Id,GuardedLChoice(Seq(Match(Anno(Op("fibb",[Anno(Op("s",[Anno(Op("d0",[]),Wld)]),Wld)]),Wld)),Build(Anno(Op("s",[Anno(Op("d0",[]),Op("Nil",[]))]),Op("Nil",[])))),Id,Scope(["k_63","l_63","m_63","n_63","o_63"],Seq(Match(Anno(Op("fibb",[Anno(Op("s",[Anno(Op("s",[Var("k_63")]),Wld)]),Wld)]),Wld)),Seq(Match(Var("m_63")),Seq(Build(Anno(Op("fibb",[Anno(Op("s",[Var("k_63")]),Op("Nil",[]))]),Op("Nil",[]))),Seq(CallT(SVar("q_63"),[],[]),Seq(Match(Var("l_63")),Seq(Build(Var("m_63")),Seq(Seq(Match(Var("o_63")),Seq(Build(Anno(Op("fibb",[Var("k_63")]),Op("Nil",[]))),Seq(CallT(SVar("q_63"),[],[]),Seq(Match(Var("n_63")),Seq(Build(Var("o_63")),Build(Anno(Op("plus",[Var("l_63"),Var("n_63")]),Op("Nil",[])))))))),CallT(SVar("q_63"),[],[]))))))))))))),Id,Id))],CallT(SVar("p_63"),[CallT(SVar("q_63"),[],[])],[]))],[])),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("fibb",[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",[]))),Seq(CallT(SVar("eval_and_print_0_0"),[],[]),Seq(Build(Anno(Op("fibb",[Anno(Op("fibb",[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(Op("fibb",[Anno(Op("fibb",[Anno(Op("fibb",[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(Op("fibb",[Anno(Op("fibb",[Anno(Op("fibb",[Anno(Op("fibb",[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",[]))),Seq(CallT(SVar("eval_and_print_0_0"),[],[]),Seq(Build(Anno(Op("fibb",[Anno(Op("fibb",[Anno(Op("fibb",[Anno(Op("fibb",[Anno(Op("fibb",[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",[]))),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("z_13",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("exit_0_0",[],[]),ExtSDef("memo_1_0",[VarDec("l_22",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[])])])