lambda Typer

Copyright(c) 2018 Nicolas Osborne
LicenseBSD 3-clauses
Safe HaskellSafe

Lambda2Ast

Contents

Description

Provide the function pg2ast which turn a program written in Simply Typed Lambda Calculus into an Abstract Syntax Tree.

A program in Simply Typed Lambda Calculus is divided into two main parts:

  • An Assignations part containing assignations instruction of the form:

    let id Exp
    

    Where id is an identificator and Exp is a simply styped lambda expression.

  • A Program part containing the actual computation which may contain id previously defined in the Assignations part.

Synopsis

Type declaration

data AST Source #

Abstract Syntax Tree type declaration.

Constructors

Leave

Correspond to the constant of the language.

Fields

Unary

Correspond to the unary operators of the language.

Fields

Binary

Correspond to the binary operators of the language.

Fields

  • name :: String
     
  • ltype :: String
     
  • size :: Int

    size of the AST

  • left :: AST

    first argument of the binary operator

  • right :: AST

    second argument of the binary operator

Instances

Show AST Source # 

Methods

showsPrec :: Int -> AST -> ShowS

show :: AST -> String

showList :: [AST] -> ShowS

Main programs

file2ast :: [Char] -> AST Source #

Turn a source file into the corresponding AST.

A source file must contain two main parts deliminated by the three following key words in that order: Assignations, Program, End. The assignation part (between the two first key words) is a series of assignation instruction (with the let key word) and the program part (between the two lasts key words) is the actual computation of which the source file is a description. The program part may contain the identificators declared in the assignation part.

input
The content of the source file.
output
the corresponding AST type checked.

exp2ast :: [Char] -> AST Source #

Return the corresponding AST of the given expression.

input
A well formed expression without any identificator, a "all in one" lambda expression.
output
The corresponding AST type checked.

Build the Abstract Syntax Tree

createAST :: [[Char]] -> AST Source #

Create the AST corresponding to the given list of tokens.

This function defines the syntax of the language.

input
the list of tokens representing the program.
output
the corresponding AST type checked.

Type manipulations

computeBinaryType :: [Char] -> [Char] -> [Char] -> [Char] Source #

Given two types and a binary operator, compute the expression's type.

input
operator name
input
type of the first argument
input
type of the second argument
output
type of the expression

computeAbstractionType :: [Char] -> [Char] -> [Char] Source #

Given the binder's type and the body's type, compute the type of the abstraction.

input
type of the binder.
input
type of the body.
output
type of the expression.

computeApplicationType :: [Char] -> [Char] -> [Char] Source #

Given the type of a function and the type of an argument, compute the type of the application.

input
the type of the function.
input
the type of the argument.
output
the type of the expression.

computePairType :: [Char] -> [Char] -> [Char] Source #

Given the type of two expression, compute the type of the pair.

input
the type of the first element of the pair.
input
the type of the second element of the pair.
output
the type of the expression.

parenthesizeType :: [Char] -> [Char] Source #

Prepare a type to be combined with another type. Put a pair parenthesis around the type if it is a complex type.

input
the type
output
the same type

isFunction :: [Char] -> Bool Source #

Predicate. Determine whether a type is the type of a function.

input
a type expression.
output
true if the type is the type of a function, false otherwise.

computePairElim :: [Char] -> [Char] -> [Char] Source #

Compute type of a pair elimination

input
operator, either first or second
input
type of the pair, ie of the from AxB
output
type of the expression

splitType :: [Char] -> [[Char]] Source #

Split a composed type in its two main parts.

input
a composed type
output
the list of the two types composing the composed type

Prepare the program into a list of tokens

file2pg :: [Char] -> [[Char]] Source #

Prepare the content of a file for createAST function.

input
The content of a file as described in the specifications.
output
A list of tokens ready for building an AST.

file2list :: [Char] -> [[Char]] Source #

Turn a String into the corresponding list of tokens.

Split the string and drop the separators. Separators are whitespace and end of line.

extractAssignations :: [[Char]] -> [[Char]] Source #

Return the sub-list corresponding to the list of tokens corresponding to the Assignation part of the source file.

extractPg :: [[Char]] -> [[Char]] Source #

Return the sub-list corresponding to the list of tokens corresponding to the Program part of the source file

parseA :: [[Char]] -> [[[Char]]] Source #

Parse the Assignation part of the source file.

Input
The list of tokens corresponding to the Assignation part of the source file.
Output
A list of assignations. The head of each item is an id and the tail is the expression

preparePg :: [[[Char]]] -> [[Char]] -> [[Char]] Source #

Substitute the Id in the list of tokens corresponding to the program part of the source file by the corresponding list of tokens.