vm.h (2780B)
1 #ifndef VM_H 2 #define VM_H 3 4 typedef enum { 5 SYMBOL, 6 ATTITUDE, 7 ASSUMPTION, 8 TERM, 9 PROOF, 10 } ref_t; 11 12 struct ref { 13 ref_t type; 14 void *addr; 15 int resolved; 16 }; 17 18 struct symbol { 19 char *name; 20 }; 21 22 struct attitude { 23 struct symbol *marker; 24 size_t nvars; 25 struct symbol **vars; 26 size_t npres; 27 struct term **pressupositions; 28 }; 29 30 struct term { 31 struct symbol *head; 32 size_t nargs; 33 struct term **subterms; 34 }; 35 36 struct assumption { 37 struct symbol *name; 38 struct symbol *marker; 39 size_t nvars; 40 size_t nsub; 41 size_t nproofs; 42 struct proof *proofs; 43 struct term *judgment; 44 struct symbol *vars; 45 struct assumption *sub; 46 struct assumption *prev; 47 }; 48 49 struct proof { 50 struct term *thesis; 51 struct argument *argument; 52 }; 53 54 struct goal { 55 struct goal *next; 56 struct goal *parent; 57 struct goal *sub; 58 ref_t type; 59 void **target; 60 }; 61 62 #define cap(t) c ## t ## s 63 #define num(t) n ## t ## s 64 #define vec(t) t ## s 65 66 #define init(s, t) do { \ 67 s . cap(t) = 1; \ 68 s . num(t) = 0; \ 69 s . vec(t) = calloc(1, sizeof(struct t)); \ 70 } while(0) 71 72 #define push(s, t, x) do { \ 73 if (s -> cap(t) == s -> num(t)) { \ 74 s -> vec(t) = realloc(s -> vec(t), s -> cap(t) *= 2 * sizeof(struct t)); \ 75 } \ 76 (s -> vec(t)[s -> num(t)++] = x); } while(0) 77 78 #define reserve(s, t) ( \ 79 ( \ 80 (s -> cap(t) == s -> num(t)) ? \ 81 (s -> vec(t) = realloc(s -> vec(t), \ 82 (s -> cap(t) *= 2)*sizeof(struct t))) : \ 83 NULL \ 84 ), \ 85 (s -> vec(t) + (s -> num(t)++)) \ 86 ) 87 88 #define list(t) size_t num(t); size_t cap(t); struct t ** vec(t) 89 90 /* The program is a series of values. The possible types are: 91 - A TOP instruction + type of top goal 92 - A value, depending on the current focus 93 94 Types of values: 95 - Symbol 96 - Natural number 97 */ 98 99 enum opcode { 100 TOP, 101 SYM, 102 NUM, 103 HLT 104 }; 105 106 struct op { 107 enum opcode code; 108 union { 109 unsigned int num; 110 struct symbol *sym; 111 ref_t type; 112 }; 113 }; 114 115 struct tape { 116 struct op *code; 117 size_t cur; 118 }; 119 120 struct state { 121 struct goal *focus; 122 struct goal *cursor; 123 struct goal *next; 124 struct assumption *head; 125 126 list(attitude); 127 }; 128 129 130 struct state new_state(void); 131 struct ref *allocate_refs(struct state *st, size_t n, ref_t type); 132 struct term *create_term(struct symbol *head, size_t nargs); 133 struct symbol *create_symbol(char *name); 134 struct attitude *create_attitude(struct symbol *marker, size_t nvars, size_t npres); 135 struct assumption *create_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub); 136 struct proof *create_proof(struct state *st, struct term *thesis); 137 138 void assign(struct state *st, struct ref *ref, void *dest); 139 void add_subgoal(struct state *st, ref_t type, void *target); 140 void commit(struct state *st); 141 void solve(struct state *st, void *dest); 142 struct attitude *lookup_attitude(struct state *st, struct symbol *name); 143 144 #endif