loa

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

tactics.h (795B)

      1 #include <stdlib.h>
      2 #include <assert.h>
      3 
      4 #include "vm.h"
      5 
      6 // struct term_args {
      7 // 	address head;
      8 // 	size_t arity;
      9 // };
     10 // 
     11 // struct attitude_args {
     12 // 	address marker;
     13 // 	size_t nvars;
     14 // 	size_t npres;
     15 // };
     16 // 
     17 // struct tactic_args {
     18 // 	ref_t type;
     19 // 	union {
     20 // 		struct term_args term;
     21 // 		struct attitude_args attitude;
     22 // 	};
     23 // };
     24 // 
     25 // void tactic(struct state *st, struct tactic_args);
     26 void tactic_term(struct state *st, struct symbol *head, size_t arity);
     27 void tactic_symbol(struct state *st, struct symbol *s);
     28 void tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t npres);
     29 void tactic_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub);
     30 void tactic_proof(struct state *st, struct term *thesis);
     31