/* (C) Copyright International Business Machines Corporation 23 January */
/* 1990.  All Rights Reserved. */
/*  */
/* See the file USERAGREEMENT distributed with this software for full */
/* terms and conditions of use. */
/* File: texutil.c */
/* Author: Andy Lowry */
/* SCCS Info: @(#)texutil.c	1.5 3/19/90 */

/* The following routines act on a parsed checking table entries by */
/* generating Tex source code to produce a typeset representation of */
/* the entry */


#include "gentab.h"
#include <stdio.h>
#include <assert.h>

void
init_checking_table()
{
}

void
add_operation(opname, operands, selectpos, qualname, typerules,
	      tsrules, exceptions)
char *opname, *qualname;
stringlist *operands;
int selectpos;
typerule *typerules;
typestaterules *tsrules;
stringlist *exceptions;
{
  void gen_operands(), gen_exceptions(), gen_typerules(), gen_tsrules();

  printf("\\operator{%s}", opname);
  gen_operands(operands);
  gen_exceptions(tsrules, exceptions);
  printf("\n");
  gen_typerules(typerules, operands);
  gen_tsrules(tsrules, operands);
  printf("\\qualtype %s\\endqualtype\n",qualname);
  printf("\\endoperator\n");
}

void
done_checking_table()
{
}

static void
gen_operands(operands)
stringlist *operands;
{
  stringlist *firstop;

  if (operands == nil)
    printf("{()}");
  else if (operands == &variable_operands)
    printf("{(\\variableoperands)}");
  else {
    printf("{(");
    firstop = operands;
    while (operands != nil) {
      if (operands != firstop)
	printf(", ");
      printf("\\operand{%s}", operands->value);
      operands = operands->next;
    }
    printf(")}");
  }
}

static void
gen_exceptions(tsrules,exceptions)
typestaterules *tsrules;
stringlist *exceptions;
{
  void gen_otherexceptions();
  stringlist *firstexcep;

  firstexcep = exceptions;
  printf("{");
  while (exceptions != nil) {
    if (exceptions != firstexcep)
      printf(", ");
    printf("\\exception{%s}", exceptions->value);
    exceptions = exceptions->next;
  }
  gen_otherexceptions(tsrules->preconditions, firstexcep != nil);
  printf("}");
}

static void
gen_otherexceptions(preconditions, initialcomma)
tsrule *preconditions;
boolean initialcomma;
{
  boolean first = TRUE;
  char *exception;
  char *rangeerror, *uncopyable, *duplicatekey;

  rangeerror = "RangeError";
  uncopyable = "Uncopyable";
  duplicatekey = "DuplicateKey";

  while (preconditions != nil) {
    if (strcmp(preconditions->func, "rangeerror?") == 0) {
      exception = rangeerror;
      rangeerror = nil;
    }
    else if (strcmp(preconditions->func, "uncopyable?") == 0) {
      exception = uncopyable;
      uncopyable = nil;
    }
    else if (strcmp(preconditions->func, "duplicatekey?") == 0) {
      exception = duplicatekey;
      duplicatekey = nil;
    }
    else {
      assert(preconditions->func[strlen(preconditions->func)-1] != '?');
      exception = nil;
    }

    if (exception != nil) {
      if (!first || initialcomma )
	printf(", ");
      first = FALSE;
      printf("\\optexception{%s}", exception);
    }
    preconditions = preconditions->next;
  }
  if (first && !initialcomma)
    printf("\\noexceptions");
}


static void
gen_typerules(typerules, operands)
typerule *typerules;
stringlist *operands;
{
  void gen_fam_rule(), gen_asgn_rule(), gen_inf_rule();
  char *opname(), *safe_malloc();
  int stringlist_size();

  typerule *rule;
  int *sameasclass;
  int opcount;
  int class, nextclass;
  int i;
  boolean firstinclass;

  printf("\\typerules\n");
  if (typerules == nil) {
    printf("\\notyperules\n");
    printf("\\endtyperules\n");
    return;
  }
  for (rule = typerules; rule != nil; rule = rule->next)
    if (rule->type == FAMILY)
      gen_fam_rule(&rule->rule.fam, operands);
  for (rule = typerules; rule != nil; rule = rule->next)
    if (rule->type == ASSIGNMENT)
      gen_asgn_rule(&rule->rule.asgn, operands);
  for (rule = typerules; rule != nil; rule = rule->next)
    if (rule->type == INFERENCE
	&& strcmp(rule->rule.inf.func,"sameas") != 0)
      gen_inf_rule(&rule->rule.inf, operands);
  opcount = stringlist_size(operands);
  if (opcount != 0) {
    sameasclass = (int *) safe_malloc(opcount*sizeof(int));
    for (i = 0; i < opcount; i++)
      sameasclass[i] = 0;
    nextclass = 1;
    for (rule = typerules; rule != nil; rule = rule->next)
      if (rule->type == INFERENCE
	  && strcmp(rule->rule.inf.func, "sameas") == 0) {
	class = 0;
	if (sameasclass[rule->rule.inf.source] != 0)
	  class = sameasclass[rule->rule.inf.source];
	else if (sameasclass[rule->rule.inf.target] != 0)
	  class = sameasclass[rule->rule.inf.target];
	if (class == 0)
	  class = nextclass++;
	sameasclass[rule->rule.inf.source] = class;
	if (sameasclass[rule->rule.inf.target] == 0)
	  sameasclass[rule->rule.inf.target] = class;
	else
	  assert(sameasclass[rule->rule.inf.target] == class);
      }
    if (nextclass > 1)
      for (class = 1; class < nextclass; class++) {
	firstinclass = TRUE;
	for (i = 0; i < opcount; i++)
	  if (sameasclass[i] == class) {
	    if (firstinclass) {
	      printf("\\sameas{");
	      firstinclass = FALSE;
	    }
	    else
	      printf(", ");
	    printf("%s", opname(i, operands));
	  }
	printf("}\n");
      }
    free(sameasclass);
  }
  printf("\\endtyperules\n");
}

static void
gen_fam_rule(rule, operands)
familyrule *rule;
stringlist *operands;
{
  char *opname();

  printf("\\classrule{%s}{%s}\n",
	 opname(rule->target, operands), rule->family);
}


static void
gen_asgn_rule(rule, operands)
assignmentrule *rule;
stringlist *operands;
{
  char *opname();
  char *type;

  
  static char predef[] = "predefined";
  assert(strncmp(rule->func, predef, strlen(predef)) == 0);
  type = &rule->func[strlen("predefined")];
  if (strcmp(type, "attribute_name") == 0)
    ;
  else if (strcmp(type, "definitionsmodule") == 0)
    type = "definitions_module";
  else if (strcmp(type, "definitionsmodules") == 0)
    type = "definitions_modules";
  else if (strcmp(type, "program") == 0)
    ;
  else if (strcmp(type, "integer") == 0)
    ;
  else if (strcmp(type, "typename") == 0)
    ;
  else if (strcmp(type, "typeofvalue") == 0)
    type = "typeof_value";
  else if (strcmp(type, "typestateofvalue") == 0)
    type = "typestateof_value";
  else
    assert(FALSE);
  printf("\\asgnrule{%s}{%s}\n", opname(rule->target, operands), type);
}


static void
gen_inf_rule(rule, operands)
inferencerule *rule;
stringlist *operands;
{
  char *opname();

  printf("\\infrule{%s}{%s}{%s}\n",
	 opname(rule->target, operands), rule->func,
	 opname(rule->source, operands));
}


static void
gen_tsrules(tsrules, operands)
typestaterules *tsrules;
stringlist *operands;
{
  void gen_preconditions(), gen_normal_post(), gen_special_post();

  printf("\\preconditions\n");
  gen_preconditions(tsrules->preconditions, operands);
  printf("\\endpreconditions\n");
  
  printf("\\postconditions\n");
  switch (tsrules->type) {
  case NORMAL:
    gen_normal_post(tsrules->post.postconditions, operands);
    break;
  case SPECIAL:
    gen_special_post(tsrules->post.special);
    break;
  }
  printf("\\endpostconditions\n");
}

static void
gen_preconditions(preconditions, operands)
tsrule *preconditions;
stringlist *operands;
{
  void gen_tsrule();

  if (preconditions == nil)
    printf("\\nopreconditions\n");
  else
    while (preconditions != nil) {
      gen_tsrule("\\precondition", preconditions, operands);
      preconditions = preconditions->next;
    }
}

static void 
gen_normal_post(postconditions, operands)
tsrule *postconditions;
stringlist *operands;
{
  void gen_tsrule();

  if (postconditions == nil)
    printf("\\nopostconditions\n");
  else
    while (postconditions != nil) {
      gen_tsrule("\\postcondition", postconditions, operands);
      postconditions = postconditions->next;
    }
}

static void
gen_special_post(name)
char *name;
{
  printf("\\specialpostcondition{%s}\n", name);
}

static void
gen_tsrule(csname, rule, operands)
char *csname;
tsrule *rule;
stringlist *operands;
{
  char *opname();
  intlist *ops, *firstop;

  printf("%s{%s}{(", csname, rule->func);
  ops = rule->operands;
  firstop = ops;
  while (ops != nil) {
    if (ops != firstop)
      printf(", ");
    printf("%s", opname(ops->value, operands));
    ops = ops->next;
  }
  printf(")}\n");
}

static char *
opname(pos, operands)
int pos;
stringlist *operands;
{
  char *safe_malloc();
  char *buf;

  while (pos-- > 0)
    operands = operands->next;
  buf = safe_malloc(strlen(operands->value)+strlen("\\operand{}")+1);
  sprintf(buf, "\\operand{%s}", operands->value);
  return(buf);
}

static int
stringlist_size(strings)
stringlist *strings;
{
  int count;

  count = 0;
  while (strings != nil) {
    count++;
    strings = strings->next;
  }
  return(count);
}

static char *
safe_malloc(size)
int size;
{
  char *malloc();
  char *stg;

  stg = malloc(size);
  assert(stg != nil);
  return(stg);
}


