1. INTRODUCCIÓN

• Crear especificación algebráicas con un lenguaje de especificación recursivo bastante sencillo e intuitivo.
• Probar teoremas con respecto a los tipos creados y evaluar expresiones empleando un motor de reescritura
• Generar código en C, que implementa los tipos especificados

1.1. Nota Legal

1.2. Referencias

[Tam99] TÁMARA, Vladimir.  ManTa: Manejador de Tipos Abstractos de Datos. 
        Tesis de Magister en Ingeniería de Sistemas y Computación.
        Universidad de los Andes. Santafé de Bogotá, Colombia. 1999

[Tam97] TÁMARA, Vladimir.  ManTa: Manejador de Tipos Abstractos de Datos.
        Tesis de Pregrado en Ingeniería de Sistemas y Computación.
        Universidad de los Andes. Santafé de Bogotá, Colombia. 1997

[Apo95] APONTE, Hernán.  MANTA 3.0: Un sistema para la implantación certificada y
        automática de tipos abstractos de datos.  Tesis de Magister en Ingeniería de
        Sistemas y Computación.   Universidad de los Andes. 1995

[Muñ92] MUÑOZ, Cesar.  ManTa: Un sistema para la implantación certificada y
        automática de Tipos Abstractos de Datos.  Tesis de Magister en Ingeniería de
        Sistemas y Computación. Universidad de los Andes. 1992.

[Rui90] RUIZ, Carolina.  ManTa 2. Departamento de Sistemas y Computación.
        Tesis de Magister. Universidad de los Andes. 1990.

2. ESTRUCTURA GENERAL

• Tipos y Representaciones.  Ver [Rui90]
• Teoremas y Prototipos. Ver [Muñ92]
• Interfaz Plana/Emacs. Ver [Apo95]
• Independencia de Plataforma. Ver sección 4.

2.1 Organización de fuentes

La actual organización de fuentes es coherente con la arquitectura:

dmanta3.1b4
        - doc            Documentacion
        - i_plain        Interfaz plana
        - kernel         Kernel
        - m2ocaml        Generador de codigo Ocaml
        - tools          Herramientas para distribucion

kernel
      -d_prot        Modulo de generacion de codigo C
      -d_theo        Modulo del motor de reescritura y del demostrador
      -d_types       Modulo para administracion de tipos
      -plat          Modulos dependientes de plataforma
             -cygnus     Archivos especificos para Cygnus GCC en Windows
             -djgpp      Archivos especificos para DJGPP v2 en Windows
             -unix       Archivos especificos para cc/gcc en UNIX

Las declaraciones globales del proyecto están en el directorio kernel, en los archivos declara.h y definic.h.   Las funciones dependientes de plataforma y sus declaraciones están en os_dep.c y os_dep.h respectivamente.  Las implementaciones para cada plataforma del archivo os_dep.c estan en el directorio d_plat  (Ver sección 4).

Los TADs para acceso ortogonal al núcleo, estan en el directorio kernel en los archivo apimanta.h y apimanta.c.
 

3. TADs PARA ACCEDER EL NÚCLEO

Hay dos constantes para controlar el comportamiento de adiciones a listas (ver funciones adicElemLTipo y adicElemLNombre)

const int ADIC_ADD=0,   /* Si está repetido se adiciona */
          ADIC_REP=1;   /* Si está repetdio se reemplaza */

En el resto de este capítulo se presenta la declaración de las funciones de cada TAD, junto con una corta descripción (puede encontrar más documentación en el código fuente, disponible en el sitio WEB de ManTa http://manta.sourceforge.net)
 
 

3.1 TADs Nombre  y LNombre

Lista de cadenas.  Se usa para mantener los parametros de un tipo

typedef struct nodonombre {
  cad50   nombre;
  struct nodonombre *sig;
} nodo_nombre;

int nuevoNodoNombre(nodo_nombre **n,char *merr);

Crea un nodo nodo_nombre inicializado con 0

Parametros:

n - En este parametro retorna el nuevo nodo (la funcion lozaliza mem);

merr - Buffer para mensajes de error

Retorna:

0 si y sólo  si no hay error

void nombreNodoNombre(nodo_nombre *n, char *nom);

Retorna el nombre de un nodo_nombre

Parametros:

n - nodo del cual retornar nombre

nom - espacio ya localizado donde se retornará el nombre

void elimNodoNombre(nodo_nombre **n);

Libera un nodo_nombre. No elimina el resto de nodos

              Parametros:

n - nodo por liberar

int inicLNombre(nodo_nombre **ln);

Inicializa la lista que recibe como una lista vacia.

Parametros:

         ln - Cabeza de la lista de nombres por inicializar

int copiaLNombre(nodo_nombre **n,nodo_nombre *nf,char *merr);

Saca una copia de una lista de nombres

Parametros:

n - Cabeza de la lista por copiar

nf - Sera la cabeza de la nueva lista (esta funcion localiza memoria);

merr - Buffer para mensajes de error

void adicElemLNombre(nodo_nombre **ln,nodo_nombre *nuevo, int remp);

Agrega en orden alfabetico el nombre nuevo. Reemplaza o agrega segun el valor remp

Parametros:

ln - Cabeza de la lista de nombres

nuevo - Nuevo nodo por agregar

remp - Forma de agregar el nodo ADIC_ADD si existe otro del mismo nombre agrega

el nuevo antes ADIC_REP si existe otro con el mismo nombre lo reemplaza (libera la

memoria del otro)

int cantElemLNombre(nodo_nombre *ln);

Retorna la cantidad de nombres en la lista

Parametros:

          ln - Cabeza de la lista de nombres

nodo_nombre *buscaNombreLNombre(nodo_nombre *n,char *nom);

Retorna un apuntador al noodo_nombre cuyo nombre es nom Si no existe retorna NULL

Parametros:

n - cabeza de la lista de nombres

nom - Nombre buscado

void nombreElemLNombre(nodo_nombre *n,int i, char* nom);

Retorna el nombre del i-esimo nombre de la lista n

Parametros:

n - Cabeza de la lista

i - Indice del cual sacar nombre. Debe ser menor que la cantidad de elementos de la

lista

nom - En este parametro deja el nombre del i-esimo nodo

void reemplazaLNombre(nodo_nombre *n,char *old,char *new);

Reemplaza toda ocurrencia del nombre old por n

Parametros:

n - Cabeza de la lista

old - Nombre antiguo

n - Nombre nuevo

void elimLNombre(nodo_nombre **n);

Libera una lista de nombres

Parametros:

          n - cabeza de la lista

     Modela el dominio de una función e.g En la función A:NATxBOOL->NAT, el dominio es la lista  [BOOL,NAT]
 

Estructura de Datos

typedef struct nododom {
  cad12   nombre;
  short   induccion;
  struct nododom  *sig;
} nodo_dom;

 
int nuevoNodoDominio(nodo_dom **n,char *merr);

Crea un nodo nuevo para un dominio

Parametros:

n - Sera el nuevo nodo (memoria localizada por esta funcion)

merr - Buffer para mensajes de error

void reemplazaLDominio(nodo_dom *n,char *old,char *new);

Reemplaza toda ocurrencia del nombre old por n

Parametros:

n - Cabeza de la lista

old - Nombre antiguo

n - Nombre nuevo

int copiaLDominio(nodo_dom **n,nodo_dom *nf,char *merr);

Crea una lista de dominios nueva copiando otra existente

Parametros:

n - cabeza de la lista existente

nf - Sera la cabeza de la nueva lista (localizada por esta funcion) @para merr

Buffer para manejar mensajes de error

void elimLDominio(nodo_dom **n);

Libera una lista de dominios

Parametros:

           n - cabeza de la lista

Modela las generadoras de un TAD (iniciales y constructoras)

typedef struct nodogeneradora{
  cad12   nombre;
  cad12   nombre_fte; /* Nombre de la selectora de la que se creo */
  nodo_nombre  *dominio;
  struct nodogeneradora *sig;
} nodo_generadora;

int nuevoNodoGeneradora(nodo_generadora **n,char *merr);

Crea un nodo nuevo para una generadora

Parametros:

n - Sera el nuevo nodo (memoria localizada por esta funcion)

merr - Buffer para mensajes de error

int copiaLGeneradora(nodo_generadora **n,nodo_generadora *nf,char *merr);

Crea una lista de generadoras nueva copiando otra existente

Parametros:

n - cabeza de la lista existente

nf - Sera la cabeza de la nueva lista (localizada por esta funcion) @para merr Buffer

para manejar mensajes de error

void elimLGeneradora(nodo_generadora **n);

Libera una lista de generadoras

Parametros:

           n - cabeza de la lista

Modela los argumentos de una expresión.

typedef struct nodoargum {
  nodo_expresion  *expr;
  struct nodoargum *sig;
} nodo_argm;

int nuevoNodoArgumento(nodo_argum **n,char *merr);

Crea un nodo nuevo para un argumento

Parametros:

n - Sera el nuevo nodo (memoria localizada por esta funcion)

merr - Buffer para mensajes de error

int copiaLArgumento(nodo_argum **n,nodo_argum *nf,char *merr);

Crea una lista de argumentos nueva copiando otra existente

Parametros:

n - cabeza de la lista existente

nf - Sera la cabeza de la nueva lista (localizada por esta funcion) @para merr Buffer

para manejar mensajes de error

void elimLArgumento(nodo_argum **n);

Libera una lista de argumentos

Parametros:

          n - cabeza de la lista

Modela una expresión con tipo

typedef struct nodoexpresion {
  cad12   nombre;
  cad20   tipo;
  cad12    clase;
  struct nodoargum *argumentos;
} nodo_expresion;

La clase de una expresion puede ser :

• "VAR"    Variable
• "INIC"   Inicial
• "CONSTR" Constructor
• "SELECT" Selectora
• "EQUAL"  Axioma de igualdad
• "ERROR"  La palabra clave ERROR

int nuevoNodoExpresion(nodo_expresion **n,char *merr);

Crea un nodo nuevo para una expresión

Parametros:

n - Sera el nuevo nodo (memoria localizada por esta funcion)

merr - Buffer para mensajes de error

int copiaNodoExpresion(nodo_expresion **n,nodo_expresion *nf,char *merr);

Crea una expresión nueva copiando otra existente

Parametros:

n - expresión existente

nf - Sera la nueva expresión (localizada por esta funcion) @para merr Buffer para

manejar mensajes de error

void elimNodoExpresion(nodo_expresion **n);

Libera una expresion

Parametros:

          n - cabeza de la lista

Modelan una lista de igualdades entre dos expresiones (puede mantener un axioma)

typedef struct nodoigualdad {
  texpr   li_str,
          ld_str;
  nodo_expresion  *lado_izq,
                  *lado_der;
  struct nodoigualdad *sig;
} nodo_igualdad;

int nuevoNodoIgualdad(nodo_igualdad **n,char *merr);

Crea un nodo nuevo para una igualdad

Parametros:

n - Sera el nuevo nodo (memoria localizada por esta funcion)

merr - Buffer para mensajes de error

int copiaLIgualdad(nodo_igualdad **n,nodo_igualdad *nf,char *merr);

Crea una lista de igualdades nueva copiando otra existente

Parametros:

n - cabeza de la lista existente

nf - Sera la cabeza de la nueva lista (localizada por esta funcion) @para merr Buffer

para manejar mensajes de error

void elimLIgualdad(nodo_igualdad **n);

Crea una lista de igualdades nueva copiando otra existente

Parametros:

n - cabeza de la lista existente

nf - Sera la cabeza de la nueva lista (localizada por esta funcion) @para merr Buffer para manejar mensajes de error

Modela una lista de selectoras.  La signatura y sus axiomas.

typedef struct nodoselect {
   cad12   nombre;
   cad12                   nombre_fte;
   nodo_dom  *dominio;
   cad20   codominio;
   short   caracterizadora;
   nodo_igualdad  *axiomas;
   struct nodoselect *sig;
} nodo_select;

int nuevoNodoSelectora(nodo_select **n,char *merr);

Crea una lista de igualdades nueva copiando otra existente

Parametros:

n - cabeza de la lista existente

nf - Sera la cabeza de la nueva lista (localizada por esta funcion) @para merr Buffer

para manejar mensajes de error

void elimNodoSelectora(nodo_select **n);

Libera un nodo_select.  No libera el resto de la lista

Parametros:

n - nodo por eliminar

int copiaLSelectora(nodo_select **n,nodo_select *nf,char *merr);

Crea una lista de selectoras nueva copiando otra existente

Parametros:

n - cabeza de la lista existente

nf - Sera la cabeza de la nueva lista (localizada por esta funcion) @para merr Buffer

para manejar mensajes de error

nodo_select *buscaNombreLSelectora(nodo_select *sel,char *nombre);

Busca una selectora por nombre en una lista

Parametros:

sel - Cabeza de la lista @paam nombre Nombre de la selectora buscada

Retorna:

Un apuntado al nodo con la selectora o NULL si no esta

nodo_select *buscaFuenteLSelectora(nodo_select *sel,char *nombre_fte);

Busca una selectora por el nombre de la fuente en una lista

Parametros:

sel - Cabeza de la lista

nombre - Nombre de la fuente

Retorna:

Un apuntador al nodo con la selectora o NULL si no esta

void elimLSelectora(nodo_select **n);

Libera una lista de selectoras

Parametros:

          n - cabeza de la lista

Modela un TAD, tanto su signatura como sus axiomas

typedef struct nodotad {
 cad12   nombre;              /*-- Nombre del tad --*/
 short   status,              /*-- 1 = MODIFICABLE,
                                   0 = NO_MODIFICABLE --*/
         tipo;                /*-- NORMAL, PROD_CART,etc --*/
 int     modif;               /*-- Indica si ha sido modificado,
                                   para salvarlo.         --*/
 nodo_nombre  *info_tipo,     /*-- Tipos que los generan --*/
              *parametros;    /*-- Tipos parametros     --*/
 nodo_generadora *iniciales,  /*-- Iniciales --*/
              *constructoras; /*-- Constructoras --*/
 nodo_select  *selectoras;    /*-- Selectoras --*/
 struct nodotad  *sig;        /*-- Siguiente tad --*/
}

int nuevoNodoTipo(nodo_tad **p,char *merr);

Crea un nuevo nodo de un tipo

Parametros:

p - Apuntara al nuevo tipo (localizado por esta funcion)

merr - Buffer de errores

Retorna:

0 si y solo si no hay error

void nombreNodoTipo(nodo_tad *t, int largo, char *nom);

Retorna el nombre del TAD t Si t es NULL retorna un nombre vacio

Parametros:

t - Tad del cual se obtendra el nombre

largo - Indica si se debe retornar el nombre largo

nom - En este buffer queda el nombre (debe venir localizado)

int numParamT(nodo_tad *t);

Retorna la cantidad de parametros del tad que recibe

Parametros:

t - tad por examinar

Retorna:

La cantidad de parametros del tipo

void nombreParamT(nodo_tad *t,int i,char *nom);

Retorna un parametro del tad recibido

Parametros:

t - Tad por examinar

i - Numero de Parametro por devolver

nom - En este buffer deja el nombre (debe venir localizado)

int tipoMalo(nodo_tad *t,char *merr);

Indica si el tipo es inservible

Parametros:

t - El tipo por revisar

Retorna:

Verdadero si el tipo es inservible

int esTipoBasico(nodo_tad *t1);

Indica si un tipo es basico

Parametros:

          t1 - Tipo por revisar @rturn verdadero si y solo si es un tipo básico

int esTipoExtension(nodo_tad *t1,char *merr);

Indica si un tipo es extensión (sin generadoras ni parametros)

Parametros:

t1 - Tipo por revisar

merr - Buffer para mensajes de error

Retorna:

1 si es extension 0 y un mensaje de error en el buffer si no es

int esRepresentacion(nodo_tad *r,char *merr);

Indica si un tipo es una representacion de otro

Parametros:

r - Tipo por verificar

merr - Buffer con mensajes de error

Retorna:

1 si es representacion 0 si no lo es y un mensaje en el buffer merr

void elimNodoTipo(nodo_tad **nt);

Elimina de memoria el TAD que recibe OJO: Si es parte de una lista deja el resto de la lista, y solo

elimina el nodo solicitado

Parametros:

          nt - TAD por eliminar

int copiaNodoTipo(nodo_tad **dest,nodo_tad *fte,char *merr);
         Crea una copia de un tipo

Parametros:

dest - En este quedara la copia (memoria localizada por esta func)

fte - Tad fuente

merr - Buffer para mensajes de error

Retorna - 0 si y solo si no hay errores

int cargaTipo(FILE *fp,nodo_tad **nt,char *merr);

Carga un tipo del archivo bytecode abierto que recibe

Parametros:

fp - Archivo abierto para lectura

nt - En este sitio dejara el tipo cargado (localizado por esta func.)

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay errores

int salvaTipo(FILE *fp,nodo_tad *nt);

Salva un tipo en un archivo en formato bytecode

Parametros:

fp - Archivo abierto para escritura

nt - TAD por escribir

Retorna:

0 si y solo si no hay errores

int cargaTipoTexto(FILE *fp, nodo_tad **tad,char *merr);

Carga del archivo tipo texto abierto que recibe un TAD (hace analisis sintactico) y llena con este el

tad que recibe

Parametros:

fp - Archivo tipo texto abierto

tad - En este sitio dejara el tipo cargado (localizado por esta func.)

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay errores

void salvaTipoTexto(FILE *fp,nodo_tad *tad);

Crea una archivo con la representacion del TAD tad en el lenguaje de ManTa y la pone en el    archivo abierto fp.

Parametros:

fp - Archivo tipo texto abierto para escritura

tad - Tad que se escribira

void muestraTipo(nodo_tad *tad);
           Para depuración, muestra el estado del tipo que recibe

Modela una lista de  TADs

La misma del TAD Tipo

int inicLTipo(nodo_tad **L);
           Inicializa el ambiente vacio

void elimLTipo(nodo_tad **tad);
            Elimina una lista de TADs

Parametros:

tad - Cabeza de la lista de tads

int adicElemLTipo(nodo_tad **tad,nodo_tad *nuevo, int remp,char *merr);

Agrega el elemento nuevo al final de la lista, si ya habia uno con el nombre, el comportamiento

depende del parametro remp.

Parametros:

tad - Cabeza de la lista de Tads

nuevo - Tad por Agregar

remp - Forma de agregar: ADIC_ADD si existe otro del mismo nombre agrega el

nuevo antes ADIC_REP si existe otro con el mismo nombre lo reemplaza (libera la

memoria del otro)

merr - Buffer con mensajes de error

int cantElemLTipo(nodo_tad *tad);

Si existe un tipo con el nombre recibido lo elimina

Parametros:

tad - Cabeza de la lista de TADs

nom - Nombre del tipo por eliminar

nodo_tad *buscaNombreLTipo(nodo_tad *tad,char *nomtad);

Retorna un apuntador al TAD cuyo nombre es nomtad

Retorna:

apuntado al TAD o NULL si no existe

void nombreElemLTipo(nodo_tad *tad,int i, char* nom);

Retorna el nombre del i-esimo Tipo de la lista tad

Parametros:

tad - Cabeza de la lista de tads

i - Indice del elemento

nom - Apuntará al nombre del elemento que está en la pos. i

void elimElemLTipo(nodo_tad **tad,char *nom);

Si existe un tipo con el nombre recibido lo elimina

Parametros:

tad - Cabeza de la lista de TADs

nom - Nombre del tipo por eliminar

void muestraLTipo(nodo_tad *t);

Muestra una lista de tipos en pantalla

Parametros:

          t - Cabeza de la lista

 
int nombreTipoValido(char *nom,int nuevo,char *merr);
           Indica si el nombre de un tipo es valido
           nuevo  es verdadero si el tipo es nuevo
           (en tal caso el nombre no puede estar definido)

int adicTipoAmbiente(nodo_tad **tad,nodo_tad **symtable, nodo_tad *nuevo,char *merr);

Adiciona un tipo al ambiente y actualiza la tabla de simbolos

Parametros:

tad - Cabeza de la lista de tads que conforman el ambiente

symtabl - Cabeza de la tabla de simbolos

nuevo - Nuevo TAD por adicionar

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay error

nodo_tad* tipoAmbiente(nodo_tad **tadAmb,char *nom,char *merr);

Carga un tipo en caso de que no este en el ambiente

Parametros:

tadAmb - Cabeza del ambiente

nom - Nombre del tipo por cargar

merr - Buffera para mensajes de error

 
const int CP_ENC=1,
  CP_CON=2,
  CP_SEL=4,
  CP_INT=8,
  CP_MAKE=16,
  CP_MAIN=32,
  CP_TODO=63;

int generaCProt(nodo_tad *t,int que);

Genera los archivos del prototipo en C del TAD que recibe, los archivo generados se especifican en

que con las constantes CP_CON,CP_SEL,CP_INT,CP_MAKE,CP_MAIN o CP_TODO

@para t Tad por generar

Parametros:

que - Constante que indica que generar

Retorna:

0 si y solo si no hay error

int nuevoInstanciacionT(char *nombre,nodo_tad *p, char *nom_param,
nodo_tad *p_inst, nodo_tad **nuevo,char *merr);

Crea un nuevo nodo de un tipo, por instanciación

Parametros:

nombre - Nombre del nuevo Tipo

p - Tad por instanciar

nomparam - Nombre del parametro de p por instanciar

p_inst - Tad con el cual instanciar

nuevo - Nuevo TAD (localiza memoria)

merr - Buffer para mensajes de error

Retorna:

Retorna 0 si y solo si no hay errores

int nuevoCopiaT(char *nom, nodo_tad *fuente, nodo_tad **nuevo,char *merr);

Crea un nuevo nodo de un tipo, por copia de otro

Parametros:

nom - Nombre del nuevo Tipo

fuente - Nodo del Tad Fuente

nuevo - Nuevo TAD (localiza memoria)

merr - Buffer para mensajes de error

Retorna:

Retorna 0 si y solo si no hay errores

int nuevoProdT(char *nom, nodo_tad *t1, nodo_tad *t2,
        nodo_tad **nuevo ,char *merr);

Crea un nuevo nodo de un tipo como producto cartesiano de 2

Parametros:

nom - Nombre del nuevo Tipo

t1 - Primer Tipo para el producto

t2 - Segundo Tipo para el producto

nuevo - Nuevo TAD (localiza memoria)

merr - Buffer para mensajes de error

Retorna:

Retorna 0 si y solo si no hay errores

void genereAxiomaRestriccionIzquierdo(nodo_select *sel,
          char *tr,
          char *li_str,
          char *trvar);

Genera lados izquierdos de los axiomas para las selectoras de un tipo por restricción

Parametros:

sel - Nodo de selectora

tr - Tipo que se esta restringiendo

li_str - Buffer donde retorna el lado izquierdo del axioma (ya localizado)

trvar - Buffer para retornar una lista de variables del tipo que se restringe separadas

por | (ya localizado)

void genereAxiomaRestriccionDerecho(nodo_select *sel,
        char *trvar,
        char *npred,
        char *li_str,
        char *ld_str);

Genera lados derechos de los axiomas para las selectoras de un tipo por restricción

Parametros:

sel - Nodo de selectora

trvar - Lista de variables del tipo que se restringe separadas por |

npred - Nombre de la funcion de restriccion

li_str - Lado izquierdo lleno

ld_str - Buffer para guardar el lado derecho calculado (ya localizado)

void cambiaParametrosInduccion(nodo_select *sel, short ind);

Cambia todos los parametros de la selectora sel a inductivos o no segun el parametro ind

Parametros:

sel - Selectora cuyo dominio se cambiara

ind - Valor que se pondra al campo induccion de todos los elementos del dominio

int nuevoResT(char *nom, nodo_tad *tf, char *npred, char *pred,
              FILE *fp,nodo_tad **nuevo,char *merr);

Crea un nuevo nodo de un tipo como restriccion de otro por un predicado

Parametros:

nom - Nombre del nuevo Tipo

tf - Tad por restringir

npred - Nombre del Predicado

pred - Predicado para restriccion

fp - Archivo abierto para escritura donde deja la definicion parcial del TAD

nuevo - Apuntara a un nuevo tad (definido parcialmente)

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay error

int nuevoSumT(char *nom, nodo_tad *t1, nodo_tad *t2,
              FILE *fp,nodo_tad **nuevo,char *merr);

Crea un nuevo nodo de un tipo como suma directa de los dos tipos que recibe

Parametros:

nom - Nombre del nuevo Tipo

t1 - Primer TAD por sumar

t2 - Segundo TAD por sumar

fp - Archivo abierto para escritura donde deja la definicion parcial del TAD

nuevo - Apuntara a un nuevo tad (definido parcialmente)

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay error

int nuevoComT(char *nom, nodo_tad *tf, char *ne,
              FILE *fp,nodo_tad **nuevo,char *merr);

Crea un nuevo nodo de un tipo por completacion con un elmento

Parametros:

nom - Nombre del nuevo Tipo

tf - Tad por restringir

ne - Nombre del nuevo elemento

fp - Archivo abierto para escritura donde deja la definicion parcial del TAD

nuevo - Apuntara a un nuevo tad (definido parcialmente)

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay error

int nuevoVarT(char *nom, nodo_tad *t1, nodo_tad *t2,
              FILE *fp,nodo_tad **nuevo,char *merr);

Crea un nuevo nodo de un tipo como variacion de dos existentes

Parametros:

nom - Nombre del nuevo Tipo

t1 - Primer TAD por sumar

t2 - Segundo TAD por sumar

fp - Archivo abierto para escritura donde deja la definicion parcial del TAD

nuevo - Apuntara a un nuevo tad (definido parcialmente)

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay error

int nuevoIndT(char *nom, FILE *fp,nodo_tad **nuevo,char *merr);

Crea un nuevo nodo de un tipo inductivo

Parametros:

nom - Nombre del nuevo Tipo

fp - Archivo abierto para escritura donde deja la definicion parcial del TAD

nuevo - Apuntara a un nuevo tad (definido parcialmente)

merr - Buffer para mensajes de error

Retorna:

0 si y solo si no hay error

int generadorasRep(nodo_tad *rep,nodo_generadora *gen,
     char *antTipo,char *nuevoTipo,char *merr);

Las generadoras del tipo representado se copian como selectoras en un tipo nuevo cambiando los

nombres (agregando como prefijo el nombre de la representacion.) Tambien cambiamos en todo

dominio y codominio las ocurrencias del tad representado con el tad que representa. Ningun

dominio es inductivo en principio

Parametros:

rep - Representacion que se construye

gen - Generadoras del tad que se representa

antTipo - nombre del TAD que se representa

nuevoTipo - Nombre del TAD con el que se representa

merr - Buffer para mensajes de error

Retorna:

codigo de error o 0 si no hay problemas

 
int selectorasRep(nodo_tad *rep,nodo_select *s,
     char *antTipo,char *nuevoTipo,char *merr);

Un conjunto de selectoras sel se copia como selectoras del nuevo tipo rep cambiando los nombres

(agregando como prefijo el nombre de la representacion.) Tambien cambiamos en todo dominio y

codominio las ocurrencias del tad antTipo por nuevoTipo. Ningun dominio es inductivo en principio

Parametros:

rep - TAD al que se agregan selectoras

s - Nuevas selectoras

antTipo - Nombre del tipo antiguo

nuevoTipo - Nombre del nuevo tipo

merr - Buffer para mensajes de error

Retorna:

Codigo de error o 0 si no hay problemas

int creaTADRep(char *nom,nodo_tad *t1,nodo_tad *t2,
        nodo_tad **nuevo,char *merr);

Crea un TAD extensión para representar t1 sobre t2

Parametros:

nom - Nombre del nuevo tipo

t1 - TAD que se representa

t2 - TAD con el que se representa

nuevo - Apuntara al nuevo tad (localizado por esta funcion)

merr - Buffer para mensajes de error

Retorna:

Codigo de error o 0 si no hay problemas

int nuevaRep(char *nom,nodo_tad *t1, nodo_tad *t2,
      FILE *fp,nodo_tad **nuevo,char *merr);

Crea la definicion parcial de una representacion del TAD t1 en el TAD t2

Parametros:

nom - Nombre del nuevo tipo

t1 - TAD que se representa

t2 - TAD con el que se representa

fp - Archivo abierto para escritura donde dejara un TAD por completar

nuevo - Apuntara al nuevo TAD

merr - Buffer para mensajes de error

void cambiaSelectorasExpresion(nodo_expresion *expr,nodo_select *nsel,
          char *oldtype, char *newtype);

Cambia toda ocurrencia de una selectora fuente por la asociada en nsel

Parametros:

expr - Expresion donde se hara el cambio

nsel - Selectoras con las que se remplazarn las antiguas

oldtype - nombre del tipo anterior

ntype - nombre del nuevo tipo

int cambiosRep(nodo_tad **rep,FILE *fp,char *merr);

Analiza cambios a una representacion (despues de intervencion del usuario) y la actualiza con tales

cambios

Parametros:

rep - Representacion original

fp - Archivo abierto para lectura con cambios del usuario

merr - Buffer para mensajes de error

Retorna:

Codigo de error o 0 si no hay problemas

int componeRep(char *nom,nodo_tad *r1, nodo_tad *r2,
        nodo_tad **nuevo,char *merr);

Crea una nueva representacion por composicion (r2 o r1)

Parametros:

nom - Nombre de la nueva representacion

r1 - Representacion por componer

r2 - Representacion por componer

nuevo - Apuntara a la nueva representacion (localizada por esta fun)

merr - Buffer para mensajes de error

Retorna:

0 si y solo no hay problemas

Una tabla modela una sustitución en una expresión y se implementa como una lista de la siguiente forma :
[<tipo,null>,<sel_1,it_1>, <sel_2,it_2> ... <sel_n,it_n>]
 Donde :
    tipo es un identificador de la tabla
    sel_i es una llave ( cadena de caracteres ) del i-esimo item (it_i)
    it_i  es una expresion con el contenido del item i

typedef struct nodoentrada {
        cad12           selector;
        nodo_expresion  *item;
        } nodo_entrada;

typedef struct nodotabla {
        nodo_entrada      *entrada;
        struct nodotabla  *sig;
} nodo_tabla, *Ptr_tabla;

void elimNodoEntrada(nodo_entrada **ne);

Libera una entrada

Parametros:

          n - cabeza de la lista

void elimLTabla(Ptr_tabla *t);

Libera una Tabla

Parametros:

          n - cabeza de la lista

Representa un lista con la historia de una reescritura o de una desmostración de una igualdad

typedef struct nodohistoria {
        nodo_expresion *expr;    /*-- Expresion que se reescrita  --*/
        nodo_igualdad  *regla;   /*-- Regla que la reescribio     --*/
        cad12          nivel;    /*-- Nivel de induccion al que   --*/
                                 /*-- pertenece la expresion.     --*/
        struct nodohistoria *sig;/*-- Siguiente historia.         --*/
} nodo_historia;

typedef struct nododemost {
        nodo_historia *his_li;   /*-- Historia del lado izquierdo --*/
        nodo_historia *ult_li;   /*-- Ultimo   del lado izquierdo --*/
        nodo_historia *his_ld;   /*-- Historia del lado derecho   --*/
        nodo_historia *ult_ld;   /*-- Ultimo   del lado derecho   --*/
        struct nododemost *sig;  /*-- Apuntador sig.  demostracion--*/
} nodo_demost;

int normalizaExpresion(nodo_expresion **expr,char *merr);

Normaliza la expresión que recibe

Parametros:

expr - Expresion que se normaliza

merr - Buffer para mensajes de error

Retorna:

int conjeturasRep(FILE *fp,nodo_tad *rep,char *merr);

Crea las conjeturas necesarias para probar una representacion

Parametros:

fp - Archivo abierto donde dejara las conjeturas

rep - Representacion por probar

merr - Buffer con mensajes de error

Retorna:

Codigo de error o 0 si no hay problemas

int probarConjeturas(FILE *fp,int *nprob,nodo_demost **prob,
                     int *nnoprob,nodo_demost **noprob,char *merr);

Intenta probar las conjeturas que hay en un archivo

Parametros:

fp - Archivo con conjeturas

nprob - Numero de conjeturas probadas

prob - Apuntador a las conjeturas probadas

nnoprob - Numero de conjeturas no probadas

noprob - Apuntador a las conjeturas no probadas

merr - Buffer para mensajes de error

Retorna:

Codigo de error o 0 si no hay problemas

int escribirPrueba(FILE *fp,nodo_demost *prob);

En un archivo escribe demostraciones de teoremas probados

Parametros:

fp - Archivo en el cual escribe

prob - Apuntador a los teoremas probados

Retorna:

Codigo de error o 0 si no hay problemas

int escribirIntentoPrueba(FILE *fp,nodo_demost *noprob);

En un archivo escribe el intento de prueba de una conjetura

Parametros:

fp - Archivo en el cual escribe

noprob - Apuntador a las conjeturas que no logro probar

Retorna:

Codigo de error o 0 si no hay problemas

int esNombreValido(char *nom);

Dice si el nombre que recibe es sintacticamente valido para un TAD o nombre de funcion

Parametros:

nom - Nombre por revisar

Retorna:

Verdadero si y solo es un nombre valido

int strcmp_nocase(char *a,char *b);

Compara dos cadenas sin tener en cuenta capitalizacion. Este es un reemplaza para strcasecmp que

no es ANSI

Parametros:

a - Cadena por comparar

b - Cadena por comparar

Retorna:

Un positivo si a>b, un negativoo si a

char *duplicastr(char *c);

Retorna una copia de la cadena que recibe. Este es un remplazo para strdup que no es ANSI

Parametros:

c - Cadena por duplicar

Retorna:

Un apuntador a un duplicado o NULL si no logra localizar memoria

4. PROTOCOLO PARA PORTAR LAS FUENTES

1. Crear un directorio para la plataforma en kernel/plat
2. Editar el archivo kernel/plat/os_dep.c cambiando las funciones para que operen correctamente en su plataforma (ver 4.1)
3. Editar el archivo makefile.plt (la extension de acuerdo a la plataforma máximo 3 caracteres) para que compile, pruebe e instale bien todo para su plataforma
4. Opcionalmente puede mejorar aumentar el script dsrc31 en el directorio tools para incluir sus cambios automáticamente en nuevas distribuciones.

Si logra portar ManTa a una nueva plataforma y lo desea puede enviarnos estos archivos, para incluir su contribución en futuras versiones de ManTa.
 

4.1. Las funciones dependientes de plataforma

Recuerde que el único archivo que debe modificar es os_dep.c  (eventualmente agregar #ifdef en  os_dep.h), en el directorio de su plataforma, de lo contrario podría perderse la independencia de plataforma de ManTa.