Assistant.Derivation

Definicion de un paso de derivacion. Consiste de un juicio, la regla que fue aplicada en este paso de la derivacion y la posicion que denota a este paso en toda derivacion total.

type DerivationTree = Tree DerivationStep

Definicion de un arbol de derivaciones.

type Derivation = (DerivationTree, DS, [Constraint])

Definicion de una derivacion. La definimos como un arbol de triplas, que almacena la informacion de los juicios que la componen. Ademas contiene informacion referida al conjunto de UNKNOWNs y variables que se pueden generar para esta derivacion como asi tambien la lista de restricciones existentes sobre la derivacion.

type DS = ([Expr], [Id], [GenId])

Almacena un estado interno particular de la derivacion. Mantiene un conteo de las variables e incognitas que se han empleado en la misma.

Constructores

derNew :: DerivationTree -> DS -> [Constraint] -> Derivation

Define explicitamente una derivacion.

derStepNew :: Judgement -> Maybe Rule -> DerivationStep

Construye un nuevo paso para una derivacion, con el juicio que recibe como argumento. La regla indica si hay alguna regla que lo relacione con sus premisas o no y la posicion determina su ubicacion en todo el arbol de derivacion.

dsInit :: DS

Define el estado inicial del generador de variables e incognitas nuevas.

Metodos

derGetTree :: Derivation -> DerivationTree

Dada una derivacion, devuelve el arbol asociada a la misma.

derGetDS :: Derivation -> DS

Dada una derivacion, devuelve el contador de variables y UNKNOWNs.

derGetConstr :: Derivation -> [Constraint]

Dada una derivacion, devuelve el conjunto de restricciones que debe satisfacer la derivacion en cuestion.

derStepFromPos :: DerivationTree -> Pos -> Maybe DerivationStep

Dada una derivacion y una posicion, devuelve el paso de derivacion que se encuentra en esa posicion.

derStepGetJudge :: DerivationStep -> Judgement

Dado un paso de la derivacion, devuelve el juicio asociado al mismo.

derStepGetRule :: DerivationStep -> Maybe Rule

Dado un paso de la derivacion, devuelve la regla asociada al mismo.

derStepIsComp :: DerivationStep -> Bool

Dado un paso de la derivacion, determina si dicha rama ya se encuentra completada, es decir, sin ninguna incognita y con la regla de Axioma aplicada a todas sus hojas.

derDelPremises :: Derivation -> Pos -> Maybe Derivation

Dada una derivacion, devuelve la derivacion con el arbol de juicios modificado, de forma tal que el subarbol ubicado en el camino dado como argumento ha sido removido.

derJudgeFromPos :: Derivation -> Pos -> Maybe Judgement

Dada una derivacion y una posicion, devuelve el juicio que forma parte de la derivacion y se encuentra en esa posicion.

derGetUnkIdsAt :: Derivation -> Pos -> [Integer]

Dada una derivacion y una posicion, devuelve la lista de identificadores de incognitas que se encuentran presentes en la derivacion.

derTreeComplCheck :: DerivationTree -> DerivationTree

Dada una derivacion, efectua el analisis de cada uno de los juicios que la componen, verificando si ya todas las ramas finalizan con axiomas y ya no quedan incognitas por definidir. Dicho de otro modo, verifica si la derivacion ya esta completa.

derTreeFindMinDS :: DerivationTree -> DS

Dado un arbol de derivaciones, retorna el minimo generador de incognitas y variables tal que las variables que genere no ocurran en los juicios que forman parte del arbol de derivaciones.

derTreeRebuildConstr :: PTS -> DerivationTree -> Maybe ([SubstT Integer], [Constraint])

Dada la especificacion de un PTS y un arbol de derivaciones, reconstruye a partir de los mismos la informacion referida a las restricciones que debe satisfacer dicho arbol.

derTreeNoDefSorts :: Maybe PTS -> DerivationTree -> [Sort]

Dada una especificacion de PTS y un arbol de derivaciones, retorna la lista de sorts que ocurren en los juicios que componen la derivacion y no se encuentran definidos como sorts en la especificacion del PTS.

derIsComplete :: Derivation -> Bool

Dada una derivacion, determina si la misma se encuentra completa. Esto es que todas sus hojas son axiomas y que en ningun nodo de la derivacion se encuentran incognitas.

dsSet :: Integer -> Integer -> Integer -> DS

Dado el identificador inicial de incognitas y variables, retorna un nuevo generador de incognitas y variables que generara elementos a partir de los valores que se recibieron como argumento.

dsSetUnnamed :: DS -> Integer -> DS

Dado un generador de incognitas y un contador de variables sin nombre, configura el generador para que la proxima variable sin nombre se corresponda con el valor dado.

dsGetUnnamed :: DS -> Integer

Dado un generador de incognitas, retorna el identificador de la proxima variable sin nombre que deberia de ser utilizada.

dsNew :: DS -> Int -> Int -> Int -> ([Expr], [Id], [GenId], DS)

Dado un generador de variables e incognitas y un par de valores, retorna tantas incognitas y veriables nuevas como se indica en el par dado como argumento, ademas del generador de variables e incognitas actualizado.

Produced by Haddock version 0.8