Commit e3e82257 authored by Michael Hanus 's avatar Michael Hanus
Browse files

Type inference tool added

parent df266301
......@@ -15,6 +15,7 @@ all:
@cd currytest && $(MAKE)
@cd genint && $(MAKE)
@cd importcalls && $(MAKE)
@cd typeinference && $(MAKE)
.PHONY: clean
clean:
......@@ -28,3 +29,4 @@ clean:
cd currytest && $(MAKE) clean
cd genint && $(MAKE) clean
cd importcalls && $(MAKE) clean
cd typeinference && $(MAKE) clean
......@@ -10,12 +10,18 @@ Currently it contains:
A tool that adds type signatures to a given Curry program.
`analysis`:
A directory containing various analyzers for Curry programs.
A directory containing various analyses for Curry programs.
These are used in the `CASS` and `currydoc` tools.
`browser`:
A tool to browse through the modules and functions of a Curry program,
show them in various formats, and analyze their properties.
`CASS`:
This directory contains the implementation of the
Curry Analysis Server System, a generic and distributed analysis system
for Curry programs.
`createmakefile`:
A tool to create a simple makefile for a Curry application.
......@@ -36,3 +42,9 @@ of some Curry systems).
`importcalls`:
A tool to show all calls to imported functions in a module.
`typeinference`:
This directory contains the implementation of a type
inferencer for FlatCurry programs which annotates
each expression occurring in a FlatCurry program with its
actual type.
This diff is collapsed.
# Makefile for the type inference tool
# No executable is generated but the modules are pre-compiled
# so that they can be included in other programs.
# Required:
# - installed Curry System (PAKCS or KiCS2) specified by variable CURRYSYSTEM
# - root location of the Curry System specified by variable ROOT
LIB=$(ROOT)/lib
META=$(LIB)/meta
# pre-compiler type inference tool:
.curry/Inference.fcy: Inference.curry Unification.curry UnificationSpec.curry
$(ROOT)/bin/$(CURRYSYSTEM) $(REPL_OPTS) :l Inference :q
.PHONY: clean
clean:
$(ROOT)/bin/cleancurry
Type Inference for FlatCurry
============================
This directory contains the implementation of a type
inferencer for FlatCurry programs which annotates
each expression occurring in a FlatCurry program with its
actual type.
It can be used by any other Curry program which processes
or transforms FlatCurry programs. The main operation to use is
Inference.inferProg :: Prog -> IO (Either String (AProg TypeExpr))
which annotates a FlatCurry program with type information.
module Unification
( module UnificationSpec
, unify
) where
import UnificationSpec
( VarIdx, Term (..), TermEq, TermEqs, Subst, UnificationError (..)
, showSubst, emptySubst, extendSubst, lookupSubst )
import FiniteMap
import List (mapAccumL)
--- An RTerm is the unification algorithm's internal term representation.
--- Its RTermCons and RTermVar constructors are similar to the TermCons
--- and TermVar constructors of the original Term data type, but it has
--- an additional Ref constructor. This Ref constructor is used to
--- represent references into a RefTable.
data RTerm
= RTermCons String [RTerm]
| RTermVar VarIdx
| Ref VarIdx
--- Type of the reference table used to store the values referenced
--- by Ref RTerms.
type RefTable = FM Int RTerm
--- An equation of RTerms.
type REq = (RTerm, RTerm)
--- A list of equations of RTerms.
type REqs = [REq]
--- Unifies the given equations.
---
--- @param eqs - the equations to unify
--- @return either an UnificationError or a substitution
unify :: TermEqs -> Either UnificationError Subst
unify ts = let (r, rts) = termEqsToREqs ts in case unify' r rts [] of
Right (r', ts') -> Right (eqsToSubst r' ts')
Left err -> Left err
-- ---------------------------------------------------------------------------
-- conversion to internal structure
-- ---------------------------------------------------------------------------
--- Converts a list of equations of terms into a list of equations
--- of RTerms. Places references into a fresh RefTable.
---
--- @param eqs - the equations to convert
--- @return a tuple of the newly created RefTable and the converted
--- equations
termEqsToREqs :: TermEqs -> (RefTable, REqs)
termEqsToREqs l = mapAccumL termEqToREq (emptyFM (<)) l
--- Converts an equation of terms into an equation of RTerms.
---
--- @param tab - the RefTable to use for storing references
--- @param eq - the equation to convert
--- @return a tuple of the RefTable and the converted equation
termEqToREq :: RefTable -> TermEq -> (RefTable, REq)
termEqToREq r (a, b) = let (r1, a') = termToRTerm r a
(r2, b') = termToRTerm r1 b
in (r2, (a', b'))
--- Converts a Term to an RTerm, placing all TermVars in the given RefTable
--- and replacing them by references inside the result RTerm.
---
--- @param tab - the RefTable to place references in
--- @param term - the Term to convert to RTerm
--- @return a tuple of the RefTable and the converted RTerm
termToRTerm :: RefTable -> Term -> (RefTable, RTerm)
termToRTerm r (TermVar i) = (addToFM r i (RTermVar i), Ref i)
termToRTerm r (TermCons n l) = let (r', l') = mapAccumL termToRTerm r l
in (r', RTermCons n l')
-- ---------------------------------------------------------------------------
-- conversion from internal structure
-- ---------------------------------------------------------------------------
--- Converts a list of term equations to a substitution
--- by turning every equation of the form (TermVar n, a) or (a, TermVar n)
--- into a mapping (n, a).
--- Equations that do not have a TermVar on either side are ignored.
--- Works on RTerms, dereferences all Refs.
---
--- @param eqs - the equations to convert
--- @return the resulting substitution
eqsToSubst :: RefTable -> REqs -> Subst
eqsToSubst _ [] = emptySubst
eqsToSubst r ((a, b) : ts) = case a of
Ref _ -> eqsToSubst r ((deref r a, b) : ts)
RTermVar n -> extendSubst (eqsToSubst r ts) n (rTermToTerm r b)
RTermCons _ _ -> case b of
RTermVar n -> extendSubst (eqsToSubst r ts) n (rTermToTerm r a)
Ref _ -> eqsToSubst r ((a, deref r b) : ts)
_ -> eqsToSubst r ts
--- Converts an RTerm to a Term, dereferencing all references inside
--- the RTerm.
---
--- @param tab - the RefTable to use for reference lookups
--- @param term - the RTerm to convert to Term
--- @return the converted Term
rTermToTerm :: RefTable -> RTerm -> Term
rTermToTerm r i@(Ref _) = rTermToTerm r (deref r i)
rTermToTerm _ (RTermVar n) = TermVar n
rTermToTerm r (RTermCons n l) = TermCons n (map (rTermToTerm r) l)
--- Dereferences an RTerm, following chained references.
--- Simply returns the same value for RTermVar and RTermCons.
---
--- @param tab - the RefTable to use for reference lookups
--- @param t - the RTerm to dereference
--- @return the dereferenced RTerm
deref :: RefTable -> RTerm -> RTerm
deref t (Ref i) = case lookupFM t i of
Nothing -> error $ "Unification.deref: " ++ show i
Just a -> case a of
RTermVar _ -> a
RTermCons _ _ -> a
Ref _ -> deref t a
deref _ a@(RTermVar _) = a
deref _ a@(RTermCons _ _) = a
-- ---------------------------------------------------------------------------
-- unification algorithm
-- ---------------------------------------------------------------------------
--- Internal unification function, the core of the algorithm.
unify' :: RefTable -> REqs -> REqs -> Either UnificationError (RefTable, REqs)
-- No equations left, we are done.
unify' r [] s = Right (r, s)
-- Substitute the constructor for the variable.
unify' r (((RTermVar i), b@(RTermCons _ _)):e) s = elim r i b e s
-- Substitute the constructor for the variable.
unify' r ((a@(RTermCons _ _), (RTermVar i)):e) s = elim r i a e s
-- If both vars are equal, simply remove the equation. Otherwise substitute
-- the second var for the first var.
unify' r ((RTermVar i, b@(RTermVar i')):e) s | i == i' = unify' r e s
| otherwise = elim r i b e s
-- If both constructors have the same name, build equations between their arguments.
-- Otherwise fail with clash.
unify' r ((a@(RTermCons aname as), b@(RTermCons bname bs)):e) s
| aname == bname = unify' r ((zip as bs) ++ e) s
| otherwise = Left (Clash (rTermToTerm r a) (rTermToTerm r b))
-- If we encounter a Ref, simply dereference it and try again.
unify' r ((a@(Ref _), b@(RTermVar _)):e) s = unify' r ((deref r a, b):e) s
unify' r ((a@(Ref _), b@(RTermCons _ _)):e) s = unify' r ((deref r a, b):e) s
unify' r ((a@(Ref _), b@(Ref _)):e) s = unify' r ((deref r a, deref r b):e) s
unify' r ((a@(RTermVar _), b@(Ref _)):e) s = unify' r ((a, deref r b):e) s
unify' r ((a@(RTermCons _ _), b@(Ref _)):e) s = unify' r ((a, deref r b):e) s
--- Substitutes a term for a variable inside the list of equations
--- that have yet to be unified and the right-hand sides of all
--- equations of the result list. Also adds a mapping from that
--- variable to that term to the result list.
elim :: RefTable -> VarIdx -> RTerm -> REqs -> REqs
-> Either UnificationError (RefTable, REqs)
elim r i t e s
| dependsOn r (RTermVar i) t
= Left (OccurCheck i (rTermToTerm r t))
| otherwise = case t of
-- Make sure to place a Ref in the RefTable and Subst, not the RTermVar
-- itself.
RTermVar i' -> unify' (addToFM r i (Ref i')) e ((RTermVar i, Ref i'):s)
RTermCons _ _ -> unify' (addToFM r i t ) e ((RTermVar i, t) :s)
--- Checks wether the first term occurs as a subterm of the second term.
--- @param a - the term to search for
--- @param b - the term to search
--- @return whether the first term is found in the second term
dependsOn :: RefTable -> RTerm -> RTerm -> Bool
dependsOn t a b = a /= b && dependsOnRecurse b
where
dependsOnRecurse v@(RTermVar _) = a == v
dependsOnRecurse (RTermCons _ vs) = or (map dependsOnRecurse vs)
dependsOnRecurse r@(Ref _) = deref t r == a
------------------------------------------------------------------------------
--- Library for general unification - specification
---
--- This library implements a general unification algorithm.
--- Because the algorithm is easy to understand, but rather slow,
--- it serves as a specification for more elaborate implementations.
---
--- @author Jonas Oberschweiber, Björn Peemöller
--- @version February 2013
------------------------------------------------------------------------------
module UnificationSpec
( VarIdx, Term (..), TermEq, TermEqs, Subst, UnificationError (..)
, showSubst, emptySubst, extendSubst, lookupSubst, applySubst, unify
) where
import FiniteMap
-- ---------------------------------------------------------------------------
-- representation of terms
-- ---------------------------------------------------------------------------
--- Variable index, identifying a variable.
type VarIdx = Int
--- Representation of a constructor term.
---
--- @cons TermVar i - The variable with index `i`
--- @cons TermCons name args - The constructor with constructor `name`
--- and argument terms `args`
data Term = TermVar VarIdx | TermCons String [Term]
--- The type of an equation.
type TermEq = (Term, Term)
--- The type of multiple equations.
type TermEqs = [TermEq]
-- ---------------------------------------------------------------------------
-- substitution
-- ---------------------------------------------------------------------------
--- The (abstract) data type for substitutions.
type Subst = FM VarIdx Term
showSubst :: Subst -> String
showSubst = unlines . map showOne . fmToList
where showOne (k, v) = show k ++ " -> " ++ show v
--- The empty substitution
emptySubst :: Subst
emptySubst = emptyFM (<)
--- Extend the substitution with the given mapping.
---
--- @param subst - the substitution
--- @param index - the variable which should be mapped
--- @param term - the term the variable should be mapped to
--- @return the extended substitution
extendSubst :: Subst -> VarIdx -> Term -> Subst
extendSubst = addToFM
--- Searches the substitution for a mapping from the given variable index
--- to a term.
---
--- @param subst - the substitution to search
--- @param i - the index to search for
--- @return the found term or Nothing
lookupSubst :: Subst -> VarIdx -> Maybe Term
lookupSubst = lookupFM
--- Applies a substitution to a single term.
---
--- @param sub - the substitution to apply
--- @param t - the term to apply the substitution to
--- @return the resulting term
applySubst :: Subst -> Term -> Term
applySubst s t@(TermVar n) = maybe t id (lookupSubst s n)
applySubst s (TermCons c vs) = TermCons c (map (applySubst s) vs)
--- Applies a substitution to a single equation.
---
--- @param sub - the substitution to apply
--- @param eq - the equation to apply the substitution to
--- @return the resulting equation
substituteSingle :: Subst -> TermEq -> TermEq
substituteSingle s (a, b) = (applySubst s a, applySubst s b)
--- Applies a substitution to a list of equations.
---
--- @param sub - the substitution to apply
--- @param eqs - the equations to apply the substitution to
--- @return the resulting equations
substitute :: Subst -> TermEqs -> TermEqs
substitute s eqs = map (substituteSingle s) eqs
-- ---------------------------------------------------------------------------
-- unification
-- ---------------------------------------------------------------------------
--- The data type for the different kinds of errors that can occur during
--- unification.
---
--- @cons Clash eq - Two term constructors with different names
--- are supposed to be equal.
--- @cons OccurCheck eq - A term is supposed to be equal to a term
--- in which it occurs as a subterm.
data UnificationError = Clash Term Term | OccurCheck VarIdx Term
--- Unifies the given equations.
---
--- @param eqs - the equations to unify
--- @return either an UnificationError or a substitution
unify :: TermEqs -> Either UnificationError Subst
unify ts = either Left (Right . eqsToSubst) (unify' ts [])
eqsToSubst :: TermEqs -> Subst
eqsToSubst [] = emptySubst
eqsToSubst ((a, b) : ts) = case a of
TermVar n -> extendSubst (eqsToSubst ts) n b
TermCons _ _ -> case b of
TermVar n -> extendSubst (eqsToSubst ts) n a
_ -> error $ "eqsToSubst: " ++ show (a, b)
unify' :: TermEqs -> TermEqs -> Either UnificationError TermEqs
unify' s [] = Right s
unify' s (((TermVar i), b@(TermCons _ _)):e) = elim s i b e
unify' s ((a@(TermCons _ _), (TermVar i)):e) = elim s i a e
unify' s ((TermVar i, b@(TermVar i')):e) | i == i' = unify' s e
| otherwise = elim s i b e
unify' s ((a@(TermCons ac as), b@(TermCons bc bs)):e)
| ac == bc = unify' s ((zip as bs) ++ e)
| otherwise = Left (Clash a b)
elim :: TermEqs -> VarIdx -> Term -> TermEqs -> Either UnificationError TermEqs
elim s i t e
| dependsOn (TermVar i) t = Left (OccurCheck i t)
| otherwise = unify' s' (substitute' i t e)
where s' = (TermVar i, t) : map (\(x, y) -> (x, termSubstitute' i t y)) s
--- Substitutes a variable with the given index by a term inside another term.
---
--- @param i - the index of the variable to substitute
--- @param t - the term to substitute
--- @param subj - the term to substitute in
--- @return the resulting term
termSubstitute' :: VarIdx -> Term -> Term -> Term
termSubstitute' b s v@(TermVar n)
| n == b = s
| otherwise = v
termSubstitute' b s (TermCons t vars) = TermCons t (termsSubstitute' b s vars)
--- Substitute a variable with the given index by a term inside a list of terms.
---
--- @param i - the index of the variable to substitute
--- @param t - the term to substitute
--- @param subjs - the terms to substitute in
--- @return the resulting terms
termsSubstitute' :: VarIdx -> Term -> [Term] -> [Term]
termsSubstitute' i t ts = map (termSubstitute' i t) ts
--- Substitute a variable with the given index by a term inside a list of equations.
---
--- @param i - the index of the variable to substitute
--- @param t - the term to substitute
--- @param eqs - the equations to substitute in
--- @return the resulting equations
substitute' :: VarIdx -> Term -> TermEqs -> TermEqs
substitute' i t ts = map (substituteSingle' i t) ts
--- Substitute a variable with the given index by a term inside a single equation.
---
--- @param i - the index of the variable to substitute
--- @param t - the term to substitute
--- @param eq - the equation to substitute in
--- @return the resulting equation
substituteSingle' :: VarIdx -> Term -> TermEq -> TermEq
substituteSingle' i t (a, b) = (termSubstitute' i t a, termSubstitute' i t b)
--- Checks wether the first term occurs as a subterm of the second term.
--- @param a - the term to search for
--- @param b - the term to search in
--- @return whether the first term is found in the second term
dependsOn :: Term -> Term -> Bool
dependsOn a b = and [(not (a == b)), dependsOnRecurse a b]
where dependsOnRecurse c v@(TermVar _) = c == v
dependsOnRecurse c (TermCons _ vars) = any id (map (dependsOnRecurse c) vars)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment