loa

Virtual machine for the Logic of Assumptions
git clone git://juanmeleiro.mat.br/loa
Log | Files | Refs

model.c (2647B)


      1 #include "model.h"
      2 
      3 #include "schema.h"
      4 
      5 #define I intern
      6 
      7 #define start_schema(NAME) \
      8 	schema * _ ## NAME ## _schema = NULL; \
      9 	schema* \
     10 	NAME ## _schema() { \
     11 		if (_ ## NAME ## _schema != NULL) return _ ## NAME ## _schema; \
     12 		schema *it = new_schema(intern(#NAME)); \
     13 		_ ## NAME ## _schema = it; \
     14 
     15 #define end_schema(NAME) \
     16 	return it; \
     17 	}
     18 
     19 #define schema(NAME) NAME ## _schema()
     20 
     21 start_schema(context)
     22 	add_constructor  (it, I("attitude")                                             );
     23 	mark_as_leaf     (it, I("attitude"),   I("name")                                );
     24 	assign_subschema (it, I("attitude"),   I("vars"),            schema(vars)       );
     25 	assign_subschema (it, I("attitude"),   I("pressupositions"), schema(term_list)  );
     26 	assign_subschema (it, I("attitude"),   I("precontext"),      schema(context)    );
     27 
     28 	add_constructor  (it, I("assumption")                                           );
     29 	mark_as_leaf     (it, I("assumption"), I("name")                                );
     30 	assign_subschema (it, I("assumption"), I("judgment"),        schema(term)       );
     31 	assign_subschema (it, I("assumption"), I("proof"),           schema(proof)      );
     32 	assign_subschema (it, I("assumption"), I("precontext"),      schema(context)    );
     33 	assign_subschema (it, I("assumption"), I("subcontext"),      schema(context)    );
     34 
     35 	add_constructor  (it, I("being")                                                );
     36 end_schema(context);
     37 
     38 start_schema(term)
     39 	add_constructor  (it, I("term")                                    );
     40 	mark_as_leaf     (it, I("term"), I("head")                         );
     41 	assign_subschema (it, I("term"), I("subterms"), schema(term_list)  );
     42 end_schema(term)
     43 
     44 start_schema(term_list)
     45 	add_constructor  (it, I("cons")                              );
     46 	add_constructor  (it, I("nil")                               );
     47 	assign_subschema (it, I("cons"), I("car"), schema(term)      );
     48 	assign_subschema (it, I("cons"), I("cdr"), schema(term_list) );
     49 end_schema(term_list)
     50 
     51 start_schema(vars)
     52 	add_constructor  (it, I("var")                          );
     53 	add_constructor  (it, I("nil")                          );
     54 	assign_subschema (it, I("var"), I("rest"), schema(vars) );
     55 	mark_as_leaf     (it, I("var"), I("name")               );
     56 end_schema(vars)
     57 
     58 start_schema(proof)
     59 	add_constructor  (it, I("done")                               );
     60 	add_constructor  (it, I("step")                               );
     61 	mark_as_leaf     (it, I("step"), I("tactic")                  );
     62 	assign_subschema (it, I("step"), I("args"), schema(term_list) );
     63 	assign_subschema (it, I("step"), I("rest"), schema(proof)     );
     64 end_schema(proof)