Method forestExample

examples/java/JavaExample.java:1718–1833

(Context ctx)

    // / tree ::= nil | cons(forest, forest)
    // / </remarks>
    public void forestExample(Context ctx) throws TestFailedException
    {
        System.out.println("ForestExample");
        Log.append("ForestExample");

        Sort tree, forest;
        @SuppressWarnings("unused")
        FuncDecl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl;
        @SuppressWarnings("unused")
        FuncDecl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl;
        @SuppressWarnings("unused")
        Expr nil1, nil2, t1, t2, t3, t4, f1, f2, f3, l1, l2, x, y, u, v;

        //
        // Declare the names of the accessors for cons.
        // Then declare the sorts of the accessors.
        // For this example, all sorts refer to the new types 'forest' and
        // 'tree'
        // being declared, so we pass in null for both sorts1 and sorts2.
        // On the other hand, the sort_refs arrays contain the indices of the
        // two new sorts being declared. The first element in sort1_refs
        // points to 'tree', which has index 1, the second element in sort1_refs
        // array
        // points to 'forest', which has index 0.
        //
        Symbol[] head_tail1 = new Symbol[] { ctx.mkSymbol("head"),
                ctx.mkSymbol("tail") };
        Sort[] sorts1 = new Sort[] { null, null };
        int[] sort1_refs = new int[] { 1, 0 }; // the first item points to a
                                               // tree, the second to a forest

        Symbol[] head_tail2 = new Symbol[] { ctx.mkSymbol("car"),
                ctx.mkSymbol("cdr") };
        Sort[] sorts2 = new Sort[] { null, null };
        int[] sort2_refs = new int[] { 0, 0 }; // both items point to the forest
                                               // datatype.
        Constructor nil1_con, cons1_con, nil2_con, cons2_con;
        Constructor[] constructors1 = new Constructor[2], constructors2 = new Constructor[2];
        Symbol[] sort_names = { ctx.mkSymbol("forest"), ctx.mkSymbol("tree") };

        /* build a forest */
        nil1_con = ctx.mkConstructor(ctx.mkSymbol("nil"),
                ctx.mkSymbol("is_nil"), null, null, null);
        cons1_con = ctx.mkConstructor(ctx.mkSymbol("cons1"),
                ctx.mkSymbol("is_cons1"), head_tail1, sorts1, sort1_refs);
        constructors1[0] = nil1_con;
        constructors1[1] = cons1_con;

        /* build a tree */
        nil2_con = ctx.mkConstructor(ctx.mkSymbol("nil2"),
                ctx.mkSymbol("is_nil2"), null, null, null);
        cons2_con = ctx.mkConstructor(ctx.mkSymbol("cons2"),
                ctx.mkSymbol("is_cons2"), head_tail2, sorts2, sort2_refs);
        constructors2[0] = nil2_con;
        constructors2[1] = cons2_con;

        Constructor[][] clists = new Constructor[][] { constructors1,
                constructors2 };