loa

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

formating.c (2361B)

      1 #include <stdio.h>
      2 #include <stdlib.h>
      3 
      4 #include "formating.h"
      5 
      6 void
      7 print_symbol(FILE *f, struct symbol *s)
      8 {
      9 	if (s == NULL)
     10 		fputc('_', f);
     11 	else
     12 		fprintf(f, "%s", s->name);
     13 }
     14 
     15 void
     16 print_term(FILE *f, struct state *st, struct term *t)
     17 {
     18 	if (t == NULL) {
     19 		fputc('_', f);
     20 	} else {
     21 		if (t->nargs == 0) {
     22 			print_symbol(f, t->head);
     23 		} else {
     24 			fputc('(', f);
     25 			print_symbol(f, t->head);
     26 			for (size_t i = 0; i < t->nargs; i++) {
     27 				fputc(' ', f);
     28 				struct term *s = t->subterms[i];
     29 				if (s)
     30 					print_term(f, st, s);
     31 				else 
     32 					fprintf(f, "%p", (void*)(t->subterms + i));
     33 			}
     34 			fputc(')', f);
     35 		}
     36 	}
     37 }
     38 
     39 void
     40 print_goal(FILE *f, struct goal *g, unsigned int level)
     41 {
     42 	if (!g) {
     43 		fprintf(f, "Nothing to do.");
     44 	} else {
     45 		for (size_t i = 0; i < level; i++) fputc(' ', f);
     46 		fprintf(f, "Build %c at %p", type_variable(g->type), (void*)g->target);
     47 		struct goal *cur = g->sub;
     48 		while (cur) {
     49 			print_goal(f, cur, level + 1);
     50 			cur = cur->next;
     51 		}
     52 	}
     53 }
     54 
     55 
     56 void
     57 print_attitude(FILE *f, struct state *st, struct attitude *a)
     58 {
     59 	if (a == NULL) {
     60 		fprintf(f, "TBD\n");
     61 	} else {
     62 		fputc('(', f);
     63 		print_symbol(f, a->marker);
     64 		for (size_t i = 0; i < a->nvars; i++) {
     65 			fputc(' ', f);
     66 			print_symbol(f, a->vars[i]);
     67 		}
     68 		fputs(")\n", f);
     69 	
     70 		for (size_t i = 0; i < a->npres; i++) {
     71 			fputs("    ", f);
     72 			print_term(f, st, a->pressupositions[i]);
     73 			fputc('\n', f);
     74 		}
     75 	}
     76 }
     77 
     78 /*
     79 void
     80 print_assumption(FILE *f, struct state *st, struct assumption a)
     81 {
     82 	print_symbol(f, *a.name);
     83 	fputc('[', f);
     84 	for (size_t i = 0; i < a.nvars; i++) {
     85 		print_symbol(f, a.vars[i]);
     86 	}
     87 	fputs("]: ", f);
     88 	print_term(f, st, *a.judgment);
     89 	fputc('\n', f);
     90 	for (size_t i = 0; i < a.nsub; i++) {
     91 		fputs("    ", f);
     92 		print_assumption(f, st, a.sub[i]);
     93 		fputc('\n', f);
     94 	}
     95 }
     96 
     97 void
     98 print_proof(FILE *f, struct state *st, struct proof p)
     99 {
    100 	// print_argument(f, st, *p.argument);
    101 	fprintf(f, " |- ");
    102 	print_term(f, st, *p.thesis);
    103 	fputc('\n', f);
    104 }
    105 */
    106 
    107 void
    108 print_state(FILE *f, struct state *st)
    109 {
    110 	// size_t i;
    111 
    112 	fprintf(f, "----------\n");
    113 
    114 	fprintf(f, "ATTITUDES (%ld/%ld)\n", st->nattitudes, st->cattitudes);
    115 	for (size_t i = 0; i < st->nattitudes; i++) {
    116 		print_attitude(f, st, st->attitudes[i]);
    117 	}
    118 	fputc('\n', f);
    119 
    120 	fprintf(f, "GOALS\n");
    121 	for (struct goal *cur = st->focus; cur; cur = cur->next) {
    122 		print_goal(f, cur, 0);
    123 		fputc('\n', f);
    124 	}
    125 }
    126