Method forestExample

examples/java/JavaGenericExample.java:1525–1638

(Context ctx)

    // / tree ::= nil | cons(forest, forest)
    // / </remarks>
    @SuppressWarnings({"unchecked", "unused", "UnusedAssignment"})
    public <Tree, Forest> void forestExample(Context ctx) throws TestFailedException
    {
        System.out.println("ForestExample");
        Log.append("ForestExample");

        DatatypeSort<Forest> forest;
        DatatypeSort<Tree> tree;
        FuncDecl<DatatypeSort<Forest>> nil1_decl, cons1_decl, cdr1_decl, car2_decl, cdr2_decl;
        FuncDecl<DatatypeSort<Tree>> car1_decl, nil2_decl, cons2_decl;
        FuncDecl<BoolSort> is_nil1_decl, is_nil2_decl, is_cons1_decl, is_cons2_decl;

        //
        // 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<Forest> nil1_con, cons1_con;
        Constructor<Tree> nil2_con, cons2_con;
        Constructor<Forest>[] constructors1 = new Constructor[2];
        Constructor<Tree>[] constructors2 = new Constructor[2];
        Symbol[] sort_names = { ctx.mkSymbol("forest"), ctx.mkSymbol("tree") };

        /* build a forest */
        nil1_con = ctx.mkConstructor(ctx.mkSymbol("nil1"),
                ctx.mkSymbol("is_nil1"), 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<Object>[][] clists = new Constructor[][] { constructors1,
                constructors2 };