|
| Assistant.Judgement | | Portability | portable (depende de GHC - GTK2HS) | | Stability | Version de juguete. |
|
|
|
|
|
| Description |
| Definicion de un juicio
|
|
| Synopsis |
|
|
|
|
| Tipos
|
|
| type Judgement = (Context, Expr, Expr) |
| Definicion de un juicio. Lo definimos como una terna, donde la primer
componente es el contexto del juicio, el segundo es el termino y el
tercero es el tipo de dicho termino en ese juicio.
|
|
| Constructores
|
|
| judgementNew :: Context -> Expr -> Expr -> Judgement |
| Dado un contexto, y dos expresiones para el termino y el tipo, devuleve
un nuevo juicio con dichos valores.
|
|
| Metodos
|
|
| judgementToStr :: Judgement -> String |
| Dado un juicio, devuelve una representacion en caracteres del mismo.
|
|
| judgementContext :: Judgement -> Context |
| Dado un juicio con Choices, devuelve el contexto asociado con el mismo.
|
|
| judgementTerm :: Judgement -> Expr |
| Dado un juicio con Choices, devuelve el termino asociado con el mismo.
|
|
| judgementType :: Judgement -> Expr |
| Dado un juicio con Choices, devuelve el tipo asociado con el mismo.
|
|
| judgementUnkIds :: Judgement -> [Integer] |
| Dado un juicio, retorna la lista de identificadore de incognitas que
ocurren en dicho juicio.
|
|
| judgementUnnVars :: Judgement -> [Integer] |
| Dado un juicio, retorna la lista de identificadores de variables sin nombre
que ocurren en dicho juicio.
|
|
| judgementGenVars :: Judgement -> [Integer] |
| Dado un juicio, retorna la lista de identificadores de variables generadas
por el sistema que ocurren en dicho juicio.
|
|
| judgementIsAllDef :: Judgement -> Bool |
| Dado un juicio, determina si el mismo ya no contiene incognitas.
|
|
| judgementIsWellFormed :: Judgement -> Bool |
| Dado un juicio determina si el mismo esta bien formado de acuerdo a la
definicion de un PTS. Esto es que toda variable libre que ocurre en el
termino o la formula, aparezca en el contexto.
|
|
| judgementNoDefSorts :: Maybe PTS -> Judgement -> [Sort] |
| Dada una posible especificacion de PTS y un juicio, retorna la lista de
sorts que ocurren en el juicio, pero que no se encuentran definidos en la
especificacion del PTS.
|
|
| Produced by Haddock version 0.8 |
