model.test.c (5760B)
1 #include <stdbool.h> 2 #include <assert.h> 3 4 #include "symbol.h" 5 #include "schema.h" 6 #include "model.h" 7 #include "gardener.h" 8 9 #define I intern 10 11 bool 12 test_existence(void) 13 { 14 assert(schema(context)); 15 assert(schema(term)); 16 assert(schema(term_list)); 17 // if ( schema(vars) == NULL) return false; 18 // if ( schema(term_list) == NULL) return false; 19 // if ( schema(proof) == NULL) return false; 20 return true; 21 } 22 23 void 24 test_context(void) 25 { 26 schema *ctx = schema(context); 27 28 assert (has_key (ctx, I("attitude"), I("name") )); 29 assert (has_key (ctx, I("attitude"), I("vars") )); 30 assert (has_key (ctx, I("attitude"), I("pressupositions") )); 31 assert (has_key (ctx, I("assumption"), I("name") )); 32 assert (has_key (ctx, I("assumption"), I("judgment") )); 33 assert (has_key (ctx, I("assumption"), I("proof") )); 34 35 assert (takes_leaf (ctx, I("attitude"), I("name") ) ); 36 assert (get_subschema (ctx, I("attitude"), I("vars") ) == schema(vars) ); 37 assert (get_subschema (ctx, I("attitude"), I("pressupositions") ) == schema(term_list) ); 38 39 assert (takes_leaf (ctx, I("assumption"), I("name") ) ); 40 assert (get_subschema (ctx, I("assumption"), I("judgment") ) == schema(term) ); 41 assert (get_subschema (ctx, I("assumption"), I("proof") ) == schema(proof) ); 42 } 43 44 void 45 test_term(void) 46 { 47 schema *term = schema(term); 48 assert (is_constructor (term, I("term") ) ); 49 assert (has_key (term, I("term"), I("head") ) ); 50 assert (has_key (term, I("term"), I("subterms") ) ); 51 assert (takes_leaf (term, I("term"), I("head") ) ); 52 assert (get_subschema (term, I("term"), I("subterms") ) == schema(term_list) ); 53 } 54 55 void 56 test_term_list(void) 57 { 58 schema *tl = schema(term_list); 59 60 assert (is_constructor (tl, I("cons") ) ); 61 assert (is_constructor (tl, I("nil") ) ); 62 assert (has_key (tl, I("cons"), I("car") ) ); 63 assert (has_key (tl, I("cons"), I("cdr") ) ); 64 assert (get_subschema (tl, I("cons"), I("car") ) == schema(term) ); 65 assert (get_subschema (tl, I("cons"), I("cdr") ) == schema(term_list) ); 66 } 67 68 void 69 test_vars(void) 70 { 71 schema *it = schema(vars); 72 assert (is_constructor (it, I("var") ) ); 73 assert (is_constructor (it, I("nil") ) ); 74 assert (has_key (it, I("var"), I("name") ) ); 75 assert (has_key (it, I("var"), I("rest") ) ); 76 assert (takes_leaf (it, I("var"), I("name") ) ); 77 assert (get_subschema (it, I("var"), I("rest") ) == schema(vars) ); 78 } 79 80 void 81 test_proof(void) 82 { 83 schema *it = schema(proof); 84 assert (is_constructor (it, I("step") ) ); 85 assert (is_constructor (it, I("done") ) ); 86 assert (has_key (it, I("step"), I("tactic") ) ); 87 assert (has_key (it, I("step"), I("args") ) ); 88 assert (takes_leaf (it, I("step"), I("tactic") ) ); 89 assert (get_subschema (it, I("step"), I("args") ) == schema(term_list) ); 90 assert (get_subschema (it, I("step"), I("rest") ) == schema(proof) ); 91 } 92 93 void 94 test_use(void) 95 { 96 gardener *g = new_gardener(schema(context)); 97 98 start (g, I("attitude") ); assert(get_error(g) == OK); 99 fill (g, I("name"), I("wft") ); assert(get_error(g) == OK); 100 sub (g, I("vars"), I("var") ); assert(get_error(g) == OK); 101 fill (g, I("name"), I("a") ); assert(get_error(g) == OK); 102 sub (g, I("rest"), I("nil") ); assert(get_error(g) == OK); 103 done (g ); assert(get_error(g) == OK); 104 done (g ); assert(get_error(g) == OK); 105 sub (g, I("pressupositions"), I("nil") ); assert(get_error(g) == OK); 106 done (g ); assert(get_error(g) == OK); 107 sup (g, I("attitude"), I("prev") ); assert(get_error(g) == OK); 108 fill (g, I("name"), I("is") ); assert(get_error(g) == OK); 109 sub (g, I("vars"), I("var") ); assert(get_error(g) == OK); 110 fill (g, I("name"), I("a") ); assert(get_error(g) == OK); 111 sub (g, I("rest"), I("var") ); assert(get_error(g) == OK); 112 fill (g, I("name"), I("b") ); assert(get_error(g) == OK); 113 sub (g, I("rest"), I("nil") ); assert(get_error(g) == OK); 114 done (g ); assert(get_error(g) == OK); 115 done (g ); assert(get_error(g) == OK); 116 done (g ); assert(get_error(g) == OK); 117 sub (g, I("pressupositions"), I("cons") ); assert(get_error(g) == OK); 118 sub (g, I("car"), I("term") ); assert(get_error(g) == OK); 119 fill (g, I("head"), I("wft") ); assert(get_error(g) == OK); 120 sub (g, I("subterms"), I("nil") ); assert(get_error(g) == OK); 121 done (g ); assert(get_error(g) == OK); 122 done (g ); assert(get_error(g) == OK); 123 sub (g, I("cdr"), I("nil") ); assert(get_error(g) == OK); 124 done (g ); assert(get_error(g) == OK); 125 done (g ); assert(get_error(g) == OK); 126 127 // display_tree(stdout, result(g)); 128 } 129 130 int 131 main() 132 { 133 test_existence(); 134 test_context(); 135 test_term(); 136 test_term_list(); 137 test_vars(); 138 test_proof(); 139 test_use(); 140 return 0; 141 }