| Copyright | (c) Michael Hanus 2003 Martin Engelke 2004 Bernd Brassel 2005 |
|---|---|
| License | BSD-3-clause |
| Maintainer | bjp@informatik.uni-kiel.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Curry.FlatCurry.Type
Description
This module contains a definition for representing FlatCurry programs
in Haskell in type Prog.
- type QName = (String, String)
- type VarIndex = Int
- type TVarIndex = Int
- data Visibility
- data Prog = Prog String [String] [TypeDecl] [FuncDecl] [OpDecl]
- data TypeDecl
- data TypeExpr
- data ConsDecl = Cons QName Int Visibility [TypeExpr]
- data OpDecl = Op QName Fixity Integer
- data Fixity
- data FuncDecl = Func QName Int Visibility TypeExpr Rule
- data Rule
- data Expr
- data Literal
- data CombType
- data CaseType
- data BranchExpr = Branch Pattern Expr
- data Pattern
Representation of qualified names and (type) variables
type QName = (String, String) Source #
Qualified names.
In FlatCurry all names are qualified to avoid name clashes. The first component is the module name and the second component the unqualified name as it occurs in the source program.
Type variables are represented by (TVar i) where i is a
type variable index.
Data types for FlatCurry
A FlatCurry module.
A value of this data type has the form
Prog modname imports typedecls functions opdecls
where
modname- Name of this module
imports- List of modules names that are imported
typedecls- Type declarations
funcdecls- Function declarations
opdecls- Operator declarations
Declaration of algebraic data type or type synonym.
A data type declaration of the form
data t x1...xn = ...| c t1....tkc |...
is represented by the FlatCurry term
Type t [i1,...,in] [...(Cons c kc [t1,...,tkc])...]
where each ij is the index of the type variable xj
Note: The type variable indices are unique inside each type declaration and are usually numbered from 0.
Thus, a data type declaration consists of the name of the data type, a list of type parameters and a list of constructor declarations.
Constructors
| Type QName Visibility [TVarIndex] [ConsDecl] | |
| TypeSyn QName Visibility [TVarIndex] TypeExpr |
Type expressions.
A type expression is either a type variable, a function type, or a type constructor application.
Note: the names of the predefined type constructors are
Int, Float, Bool, Char, IO, Success,
() (unit type), (,...,) (tuple types), [] (list type)
A constructor declaration consists of the name and arity of the constructor and a list of the argument types of the constructor.
Constructors
| Cons QName Int Visibility [TypeExpr] |
Fixity of an operator.
Data type for representing function declarations.
A function declaration in FlatCurry is a term of the form
(Func name arity type (Rule [i_1,...,i_arity] e))
and represents the function "name" with definition
name :: type name x_1...x_arity = e
where each i_j is the index of the variable x_j
Note: The variable indices are unique inside each function declaration and are usually numbered from 0.
External functions are represented as
Func name arity type (External s)
where s is the external name associated to this function.
Thus, a function declaration consists of the name, arity, type, and rule.
A rule is either a list of formal parameters together with an expression
or an External tag.
Data type for representing expressions.
Remarks:
- if-then-else expressions are represented as function calls:
(if e1 then e2 else e3)
is represented as
(Comb FuncCall (Prelude,"if_then_else") [e1,e2,e3])
- Higher order applications are represented as calls to the (external)
function
apply. For instance, the rule
app f x = f x
is represented as
(Rule [0,1] (Comb FuncCall (Prelude,"apply") [Var 0, Var 1]))
- A conditional rule is represented as a call to an external function
condwhere the first argument is the condition (a constraint).
For instance, the rule
equal2 x | x=:=2 = success
is represented as
(Rule [0]
(Comb FuncCall (Prelude,"cond")
[Comb FuncCall (Prelude,"=:=") [Var 0, Lit (Intc 2)],
Comb FuncCall (Prelude,"success") []]))
- Functions with evaluation annotation
choiceare represented by a rule whose right-hand side is enclosed in a call to the external functionPrelude.commit. Furthermore, all rules of the original definition must be represented by conditional expressions (i.e., (cond [c,e])) after pattern matching.
Example:
m eval choice m [] y = y m x [] = x
is translated into (note that the conditional branches can be also wrapped with Free declarations in general):
Rule [0,1]
(Comb FuncCall (Prelude,"commit")
[Or (Case Rigid (Var 0)
[(Pattern (Prelude,"[]") []
(Comb FuncCall (Prelude,"cond")
[Comb FuncCall (Prelude,"success") [],
Var 1]))] )
(Case Rigid (Var 1)
[(Pattern (Prelude,"[]") []
(Comb FuncCall (Prelude,"cond")
[Comb FuncCall (Prelude,"success") [],
Var 0]))] )])
Operational meaning of (Prelude.commit e):
evaluate e with local search spaces and commit to the first
(Comb FuncCall (Prelude,"cond") [c,ge]) in e whose constraint c
is satisfied
Constructors
| Var VarIndex | Variable, represented by unique index |
| Lit Literal | Literal (IntegerFloatChar constant) |
| Comb CombType QName [Expr] | Application |
| Free [VarIndex] Expr | Introduction of free local variables for an expression |
| Let [(VarIndex, Expr)] Expr | Local let-declarations |
| Or Expr Expr | Disjunction of two expressions (resulting from overlapping left-hand sides) |
| Case CaseType Expr [BranchExpr] | case expression |
| Typed Expr TypeExpr | typed expression |
Data type for representing literals.
A literal is either an integer, a float, or a character constant.
Note: The constructor definition of Intc differs from the original
PAKCS definition. It uses Haskell type Integer instead of Int
to provide an unlimited range of integer numbers. Furthermore,
float values are represented with Haskell type Double instead of
Float.
Data type for classifying combinations (i.e., a function/constructor applied to some arguments).
Constructors
| FuncCall | a call to a function where all arguments are provided |
| ConsCall | a call with a constructor at the top, all arguments are provided |
| FuncPartCall Int | a partial call to a function (i.e., not all arguments are provided) where the parameter is the number of missing arguments |
| ConsPartCall Int | a partial call to a constructor along with number of missing arguments |
Classification of case expressions, either flexible or rigid.
data BranchExpr Source #
Branches in a case expression.
Branches (m.c x1...xn) -> e in case expressions are represented as
(Branch (Pattern (m,c) [i1,...,in]) e)
where each ij is the index of the pattern variable xj, or as
(Branch (LPattern (Intc i)) e)
for integers as branch patterns (similarly for other literals like float or character constants).
Instances