ContentsIndex
GlobalPW
Portability portable
Stability experimental
Maintainer jproenca@di.uminho.pt
Contents
Data Type
Conversion of an haskell expression to a GlobalPW term
Conversion of a GlobalPW term to a PWCore term
Description

A global pointwise syntax and its relation with:

  • An expression in programatica's abstract syntax tree;
  • A pointwise core - PWCore.
Synopsis
data GLTerm
= Star
| V String
| (:-:) GLTerm GLTerm
| Lam String GLTerm
| (:&:) GLTerm GLTerm
| Pi1 GLTerm
| Pi2 GLTerm
| Inl' GLTerm
| Inr' GLTerm
| Case' GLTerm (String, GLTerm) (String, GLTerm)
| In' HsExpP GLTerm
| Out' HsExpP GLTerm
| Fix' GLTerm
| T'
| F'
| Z'
| Suc GLTerm
| Pred GLTerm
| IsZ GLTerm
| Ite GLTerm GLTerm GLTerm
| N'
| (:::) GLTerm GLTerm
| Hd GLTerm
| Tl GLTerm
| IsN GLTerm
| Letrec String GLTerm GLTerm
| RecNat GLTerm GLTerm GLTerm
| RecList GLTerm GLTerm GLTerm
exp2Global :: Monad m => HsExpI PNT -> m GLTerm
global2core :: GLTerm -> PWTerm
Data Type

Represents a pointwise language that:

  1. is very similar to the way we are used to program in haskell;
  2. not the most general one, since it only deals with booleans, natural numbers and lists.
data GLTerm
Constructors
StarUnit
V StringVariable
(:-:) GLTerm GLTermAplication
Lam String GLTermAbstraction
(:&:) GLTerm GLTermPair
Pi1 GLTermPoint-wise first
Pi2 GLTermPoint-wise second
Inl' GLTermPoint-wise left injection
Inr' GLTermPoint-wise right injection
Case' GLTerm (String, GLTerm) (String, GLTerm)Case of
In' HsExpP GLTermInjection on a specified type
Out' HsExpP GLTermExtraction of the functor of a specified type
Fix' GLTermFixed-point
T'Constant True
F'Constant False
Z'Constant Zero
Suc GLTermSuccessor
Pred GLTermPredecessor
IsZ GLTermis zero?
Ite GLTerm GLTerm GLTermif then else
N'Empty list
(:::) GLTerm GLTermConstructor for lists
Hd GLTermHead of a list
Tl GLTermTail of a list
IsN GLTermis the list empty?
Letrec String GLTerm GLTermrecursive let
RecNat GLTerm GLTerm GLTermPrimitive recursion on Nat's
RecList GLTerm GLTerm GLTermPrimitive recursion on List's
Instances
Show GLTerm
Conversion of an haskell expression to a GlobalPW term
exp2Global :: Monad m => HsExpI PNT -> m GLTerm

Applies a simple transformation from an expression of programatica's abstract syntax tree to GLTerm.

The recognized grammar is:

G, G1, G2, G3 ::=
(G) | undefined | () | _L | inN (_L::type) G | ouT (_L::type) | True | False | 0 | [] | n, n>0 | [G1, G2, ... ] | G1 : G2 | succ G | pred G | (==0) G | G == 0 | head G | tail G | null | recNat G1 G2 G3 | recList G1 G2 G3 | fix G | if G1 then G2 else G3 | var | (G1,G2) | fst | snd | Left | Right | G1 infixOp G2 | \var1 var2 ... -> G | case G1 of Left var1 -> G2; Right var2 ->G3 | let var = G1 in G2

where types are read as the pretty print string, and var, var1 and var2 are variables that are read as strings also.

Conversion of a GlobalPW term to a PWCore term
global2core :: GLTerm -> PWTerm
Converts a GLTerm to a PWTerm, which is a more general representation for pointwise terms, but with less pratical constructors (in PWCore).
Produced by Haddock version 0.6