diff options
Diffstat (limited to 'tactics/tauto.mli')
| -rw-r--r-- | tactics/tauto.mli | 127 |
1 files changed, 127 insertions, 0 deletions
diff --git a/tactics/tauto.mli b/tactics/tauto.mli new file mode 100644 index 0000000000..27bd8ee43b --- /dev/null +++ b/tactics/tauto.mli @@ -0,0 +1,127 @@ + +(* $Id$ *) + +(* Mars 1993 *) +(* Autor: Cesar A. Munnoz H *) + +open Tacmach +open Term + +(* Prototipo *) +(* Estructuras de Datos *) + +type formula = + | FVar of string + | FAnd of formula*formula + | FOr of formula*formula + | FImp of formula*formula + | FEqu of formula*formula + | FNot of formula + | FEq of formula*formula*formula + | FPred of constr (* Predicado proposicional *) + | FFalse + | FTrue + (* La siguiente no puede aparecer en una formula de entrada *) + (* Representa una formula atomica cuando aparece en un principal de una + regla *) + | FLis of formula list (* Lista de formulas *) + | FAto of string (* Formula atomica *) + | FLisfor of string (* Variable para una lista de formulas *) + (* En el antecedente se llama GAMA, + en el sucedente DELTA *) + +(* Terminos en calculo lambda *) +type termino = + | TVar of string + | TApl of formula*formula*termino*termino + | TFun of string*formula*termino + | TPar of formula*formula*termino*termino + | TInl of formula*formula*termino + | TInr of formula*formula*termino + | TFst of formula*formula*termino + | TSnd of formula*formula*termino + | TCase of formula list * termino list + | TZ of formula * termino + | TExi of string + | TRefl of formula * formula (*Reflexividad de la igualdad *) + | TSim of formula * formula * formula * termino + (*Simetria de la igualdad *) + | TTrue + (* Los siguientes terminos se usan solamente en las sustituciones *) + | TSum of termino*termino (* Suma de terminos *) + | TLis of termino list (* Lista de terminos *) + | TLister of string (* Variable para una lista de terminos *) + (* En el antecendete se llama Gama, + en el sucedente Delta *) + | TZero of formula (* Milagro *) + +(* Es una formula asociada con un termino del calculo lambda, o los + multiconjuntos Gama y Delta *) +type formulaT = termino*formula + +(* La primera componente es el antecedente, la segunda es sucedente *) +type sequente = formulaT list * formulaT list + +(* Substitucion de variable por una formula *) +type subsF = (string*formula) list + +(* Substitucion de variable por un lambda termino *) +type subsT = (string*termino) list + +type regla = { + tip: string; (* Tipo de la formula principal *) + heu: bool; (* Si es una regla heuristica o no *) + ant: bool; (* Si principal es antecedente o sucedente *) + pri: formulaT;(* Formula principal de la regla *) + pre: sequente list; (* Premisas de la regla *) + res: sequente;(* Restricciones para la aplicacion de una regla*) + def: subsT; (* Definicion de los terminos del lado derecho *) + sub: subsT; (* Substitucion que se aplica al lado derecho de la + conclusion para obetener el lambda termino *) + ren: string list; (* Variables que se deben renombrar *) + vardelta:bool; (* Si se usa la variable proposicional DELTA *) + ssi:bool; (* Si la regla es reversible o no *) + rendelta: string list} (* Renombramientos de delta *) + (* Note que si Res = A |- B, entonces la conclusion de la regla es + A,Gama,Pri' |- B, Pri'',Delta + Si ant = true Pri'= Pri + Si ant =false Pri''=Pri*) + +(* Substitucion Formula Termino para aplicar una regla *) +type sFT = { + sReg : regla ref; (*Apuntador a la regla *) + sFor : subsF; (*Substitucion de Formulas *) + sGam : formulaT list; (* Lista de formulas de Gamma *) + sDel : formulaT list; (* Lista de formulas de Delta *) + sRen : (string*subsT) list; (* Renombramientos de variables *) + sTer : subsT; (* Susbstitucion de terminos *) + sDef : subsT } (* Definicion de terminos *) + +type subsFT = SNil | SCons of sFT + +type reglaSub = RNil | RCons of (sFT*regla list*formulaT list*sequente) + +(* De un arbol de demostracion *) +type nodo = { + seq: sequente ref; (* Sequente que se resuelve *) + reg: regla ref; (* Regla usada para resolver *) + sd: subsT; (* Substitucion que define los lambda terminos *) + st: subsT } (* Substitucion que calcula el lambda termino *) + +(* Arbol de demostracion *) +type arbol = Nil | Cons of arbol * nodo * arbol + +(* Demostracion *) +(* Si el secuente es valido Arb es un arbol de demostracion y Lisbut + es vacio, sino Lisbut es un contexto en el cual Arb es valido *) +type demostracion = { arb : arbol; lisbut : formulaT list } + +(* Definicion de excepcion para rescribir terminos *) +exception NoAplica +exception TacticFailure + +val tauto_tac : tactic +val intuition : tactic +val intuition_tac : tactic +val tauto : tactic + |