tactics.c (1715B)
1 #include "tactics.h" 2 3 void 4 tactic_term(struct state *st, struct symbol *head, size_t arity) 5 { 6 assert(!st->focus || st->focus->type == TERM); 7 8 struct term *t = create_term(head, arity); 9 10 if (st->focus) solve(st, t); 11 12 for (size_t i = 0; i < arity; i++) { 13 add_subgoal(st, TERM, t->subterms + i); 14 } 15 16 commit(st); 17 } 18 19 void 20 tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t npres) 21 { 22 assert(st->focus && st->focus->type == ATTITUDE); 23 24 struct attitude *a = create_attitude(marker, nvars, npres); 25 26 for (size_t i = 0; i < nvars; i++) 27 add_subgoal(st, SYMBOL, a->vars + i); 28 29 for (size_t i = 0; i < npres; i++) 30 add_subgoal(st, TERM, a->pressupositions + i); 31 32 solve(st, a); 33 commit(st); 34 } 35 36 void 37 tactic_symbol(struct state *st, struct symbol *s) 38 { 39 assert(st->focus && st->focus->type == SYMBOL); 40 solve(st, s); 41 commit(st); 42 } 43 44 // void 45 // tactic_proof(struct state *st, struct term *thesis) 46 // { 47 // assert(!st->focus || st->focus->type == PROOF); 48 // 49 // struct proof *p = create_proof(st, thesis); 50 // 51 // if (st->focus) solve(st, p); 52 // 53 // add_subgoal(st, ASSUMPTION, p->argument); 54 // 55 // commit(st); 56 // } 57 58 /* 59 void 60 tactic_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub) 61 { 62 assert(!st->focus || st->focus->type == ASSUMPTION); 63 64 struct assumption *a = create_assumption(st, name, marker, nvars, nsub); 65 66 if (st->focus) solve(st, a); 67 68 for (size_t i = 0; i < nvars; i++) 69 add_subgoal(st, SYMBOL, a->vars + i); 70 71 add_subgoal(st, TERM, a->judgment); 72 73 for (size_t i = 0; i < nsub; i++) 74 add_subgoal(st, ASSUMPTION, a->sub + i); 75 76 for (size_t i = 0; i < a->nproofs; i++) 77 add_subgoal(st, PROOF, a->proofs + i); 78 79 commit(st); 80 } 81 */