forked from GitHub/gf-core
"Committed_by_peb"
This commit is contained in:
@@ -1,18 +1,25 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : AbsCompute
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.6 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-- computation in abstract syntax w.r.t. explicit definitions.
|
||||
--
|
||||
-- old GF computation; to be updated
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module AbsCompute where
|
||||
module AbsCompute (LookDef,
|
||||
compute,
|
||||
computeAbsTerm,
|
||||
computeAbsTermIn,
|
||||
beta
|
||||
) where
|
||||
|
||||
import Operations
|
||||
|
||||
@@ -24,16 +31,13 @@ import Compute
|
||||
|
||||
import Monad (liftM, liftM2)
|
||||
|
||||
-- computation in abstract syntax w.r.t. explicit definitions.
|
||||
--- old GF computation; to be updated
|
||||
|
||||
compute :: GFCGrammar -> Exp -> Err Exp
|
||||
compute = computeAbsTerm
|
||||
|
||||
computeAbsTerm :: GFCGrammar -> Exp -> Err Exp
|
||||
computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
|
||||
|
||||
--- a hack to make compute work on source grammar as well
|
||||
-- | a hack to make compute work on source grammar as well
|
||||
type LookDef = Ident -> Ident -> Err (Maybe Term)
|
||||
|
||||
computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
|
||||
|
||||
@@ -1,13 +1,13 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Abstract
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.3 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
@@ -1,18 +1,19 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : AppPredefined
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.9 $
|
||||
--
|
||||
-- Predefined function type signatures and definitions.
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module AppPredefined where
|
||||
module AppPredefined (isInPredefined, typPredefined, appPredefined
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Grammar
|
||||
|
||||
@@ -1,18 +1,18 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Compute
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.13 $
|
||||
--
|
||||
-- Computation of source terms. Used in compilation and in 'cc' command.
|
||||
-- Computation of source terms. Used in compilation and in @cc@ command.
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Compute where
|
||||
module Compute (computeConcrete, computeTerm) where
|
||||
|
||||
import Operations
|
||||
import Grammar
|
||||
@@ -31,9 +31,8 @@ import AppPredefined
|
||||
import List (nub,intersperse)
|
||||
import Monad (liftM2, liftM)
|
||||
|
||||
-- computation of concrete syntax terms into normal form
|
||||
-- | computation of concrete syntax terms into normal form
|
||||
-- used mainly for partial evaluation
|
||||
|
||||
computeConcrete :: SourceGrammar -> Term -> Err Term
|
||||
computeConcrete g t = {- refreshTerm t >>= -} computeTerm g [] t
|
||||
|
||||
@@ -295,8 +294,7 @@ computeTerm gr = comp where
|
||||
cs' <- mapM (compBranch g) [(p, f v) | (p,v) <- cs]
|
||||
return $ S (T i cs') e
|
||||
|
||||
-- argument variables cannot be glued
|
||||
|
||||
-- | argument variables cannot be glued
|
||||
checkNoArgVars :: Term -> Err Term
|
||||
checkNoArgVars t = case t of
|
||||
Vr (IA _) -> Bad $ glueErrorMsg $ prt t
|
||||
|
||||
@@ -1,18 +1,54 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Grammar
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.7 $
|
||||
--
|
||||
-- GF source abstract syntax used internally in compilation.
|
||||
--
|
||||
-- AR 23\/1\/2000 -- 30\/5\/2001 -- 4\/5\/2003
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Grammar where
|
||||
module Grammar (SourceGrammar,
|
||||
SourceModInfo,
|
||||
SourceModule,
|
||||
SourceAbs,
|
||||
SourceRes,
|
||||
SourceCnc,
|
||||
Info(..),
|
||||
Perh,
|
||||
MPr,
|
||||
Type,
|
||||
Cat,
|
||||
Fun,
|
||||
QIdent,
|
||||
Term(..),
|
||||
Patt(..),
|
||||
TInfo(..),
|
||||
Label(..),
|
||||
MetaSymb(..),
|
||||
Decl,
|
||||
Context,
|
||||
Equation,
|
||||
Labelling,
|
||||
Assign,
|
||||
Case,
|
||||
Cases,
|
||||
LocalDef,
|
||||
Param,
|
||||
Altern,
|
||||
Substitution,
|
||||
Branch(..),
|
||||
Con,
|
||||
Trm,
|
||||
wildPatt,
|
||||
varLabel
|
||||
) where
|
||||
|
||||
import Str
|
||||
import Ident
|
||||
@@ -21,10 +57,7 @@ import Modules
|
||||
|
||||
import Operations
|
||||
|
||||
-- AR 23/1/2000 -- 30/5/2001 -- 4/5/2003
|
||||
|
||||
-- grammar as presented to the compiler
|
||||
|
||||
-- | grammar as presented to the compiler
|
||||
type SourceGrammar = MGrammar Ident Option Info
|
||||
|
||||
type SourceModInfo = ModInfo Ident Option Info
|
||||
@@ -35,29 +68,39 @@ type SourceAbs = Module Ident Option Info
|
||||
type SourceRes = Module Ident Option Info
|
||||
type SourceCnc = Module Ident Option Info
|
||||
|
||||
-- judgements in abstract syntax
|
||||
|
||||
-- | the constructors are judgements in
|
||||
--
|
||||
-- - abstract syntax (/ABS/)
|
||||
--
|
||||
-- - resource (/RES/)
|
||||
--
|
||||
-- - concrete syntax (/CNC/)
|
||||
--
|
||||
-- and indirection to module (/INDIR/)
|
||||
data Info =
|
||||
AbsCat (Perh Context) (Perh [Term]) -- constructors; must be Id or QId
|
||||
| AbsFun (Perh Type) (Perh Term) -- Yes f = canonical
|
||||
| AbsTrans Term
|
||||
-- judgements in abstract syntax
|
||||
AbsCat (Perh Context) (Perh [Term]) -- ^ (/ABS/) constructors; must be 'Id' or 'QId'
|
||||
| AbsFun (Perh Type) (Perh Term) -- ^ (/ABS/) 'Yes f' = canonical
|
||||
| AbsTrans Term -- ^ (/ABS/)
|
||||
|
||||
-- judgements in resource
|
||||
| ResParam (Perh [Param])
|
||||
| ResValue (Perh Type) -- to mark parameter constructors for lookup
|
||||
| ResOper (Perh Type) (Perh Term)
|
||||
| ResParam (Perh [Param]) -- ^ (/RES/)
|
||||
| ResValue (Perh Type) -- ^ (/RES/) to mark parameter constructors for lookup
|
||||
| ResOper (Perh Type) (Perh Term) -- ^ (/RES/)
|
||||
|
||||
-- judgements in concrete syntax
|
||||
| CncCat (Perh Type) (Perh Term) MPr -- lindef ini'zed,
|
||||
| CncFun (Maybe (Ident,(Context,Type))) (Perh Term) MPr -- type info added at TC
|
||||
| CncCat (Perh Type) (Perh Term) MPr -- ^ (/CNC/) lindef ini'zed,
|
||||
| CncFun (Maybe (Ident,(Context,Type))) (Perh Term) MPr -- (/CNC/) type info added at 'TC'
|
||||
|
||||
-- indirection to module Ident; the Bool says if canonical
|
||||
| AnyInd Bool Ident
|
||||
-- indirection to module Ident
|
||||
| AnyInd Bool Ident -- ^ (/INDIR/) the 'Bool' says if canonical
|
||||
deriving (Read, Show)
|
||||
|
||||
type Perh a = Perhaps a Ident -- to express indirection to other module
|
||||
-- | to express indirection to other module
|
||||
type Perh a = Perhaps a Ident
|
||||
|
||||
type MPr = Perhaps Term Ident -- printname
|
||||
-- | printname
|
||||
type MPr = Perhaps Term Ident
|
||||
|
||||
type Type = Term
|
||||
type Cat = QIdent
|
||||
@@ -66,80 +109,81 @@ type Fun = QIdent
|
||||
type QIdent = (Ident,Ident)
|
||||
|
||||
data Term =
|
||||
Vr Ident -- variable
|
||||
| Cn Ident -- constant
|
||||
| Con Ident -- constructor
|
||||
| EData -- to mark in definition that a fun is a constructor
|
||||
| Sort String -- basic type
|
||||
| EInt Int -- integer literal
|
||||
| K String -- string literal or token: "foo"
|
||||
| Empty -- the empty string []
|
||||
Vr Ident -- ^ variable
|
||||
| Cn Ident -- ^ constant
|
||||
| Con Ident -- ^ constructor
|
||||
| EData -- ^ to mark in definition that a fun is a constructor
|
||||
| Sort String -- ^ basic type
|
||||
| EInt Int -- ^ integer literal
|
||||
| K String -- ^ string literal or token: @\"foo\"@
|
||||
| Empty -- ^ the empty string @[]@
|
||||
|
||||
| App Term Term -- application: f a
|
||||
| Abs Ident Term -- abstraction: \x -> b
|
||||
| Meta MetaSymb -- metavariable: ?i (only parsable: ? = ?0)
|
||||
| Prod Ident Term Term -- function type: (x : A) -> B
|
||||
| Eqs [Equation] -- abstraction by cases: fn {x y -> b ; z u -> c}
|
||||
| App Term Term -- ^ application: @f a@
|
||||
| Abs Ident Term -- ^ abstraction: @\x -> b@
|
||||
| Meta MetaSymb -- ^ metavariable: @?i@ (only parsable: ? = ?0)
|
||||
| Prod Ident Term Term -- ^ function type: @(x : A) -> B@
|
||||
| Eqs [Equation] -- ^ abstraction by cases: @fn {x y -> b ; z u -> c}@
|
||||
-- only used in internal representation
|
||||
| Typed Term Term -- type-annotated term
|
||||
|
||||
-- below this only for concrete syntax
|
||||
| RecType [Labelling] -- record type: { p : A ; ...}
|
||||
| R [Assign] -- record: { p = a ; ...}
|
||||
| P Term Label -- projection: r.p
|
||||
| ExtR Term Term -- extension: R ** {x : A} (both types and terms)
|
||||
| Typed Term Term -- ^ type-annotated term
|
||||
--
|
||||
-- /below this, the constructors are only for concrete syntax/
|
||||
| RecType [Labelling] -- ^ record type: @{ p : A ; ...}@
|
||||
| R [Assign] -- ^ record: @{ p = a ; ...}@
|
||||
| P Term Label -- ^ projection: @r.p@
|
||||
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
|
||||
|
||||
| Table Term Term -- table type: P => A
|
||||
| T TInfo [Case] -- table: table {p => c ; ...}
|
||||
| TSh TInfo [Cases] -- table with discjunctive patters (only back end opt)
|
||||
| V Type [Term] -- table given as course of values: table T [c1 ; ... ; cn]
|
||||
| S Term Term -- selection: t ! p
|
||||
| Table Term Term -- ^ table type: @P => A@
|
||||
| T TInfo [Case] -- ^ table: @table {p => c ; ...}@
|
||||
| TSh TInfo [Cases] -- ^ table with discjunctive patters (only back end opt)
|
||||
| V Type [Term] -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
|
||||
| S Term Term -- ^ selection: @t ! p@
|
||||
|
||||
| Let LocalDef Term -- local definition: let {t : T = a} in b
|
||||
| Let LocalDef Term -- ^ local definition: @let {t : T = a} in b@
|
||||
|
||||
| Alias Ident Type Term -- constant and its definition, used in inlining
|
||||
| Alias Ident Type Term -- ^ constant and its definition, used in inlining
|
||||
|
||||
| Q Ident Ident -- qualified constant from a package
|
||||
| QC Ident Ident -- qualified constructor from a package
|
||||
| Q Ident Ident -- ^ qualified constant from a package
|
||||
| QC Ident Ident -- ^ qualified constructor from a package
|
||||
|
||||
| C Term Term -- concatenation: s ++ t
|
||||
| Glue Term Term -- agglutination: s + t
|
||||
| C Term Term -- ^ concatenation: @s ++ t@
|
||||
| Glue Term Term -- ^ agglutination: @s + t@
|
||||
|
||||
| FV [Term] -- alternatives in free variation: variants { s ; ... }
|
||||
| FV [Term] -- ^ alternatives in free variation: @variants { s ; ... }@
|
||||
|
||||
| Alts (Term, [(Term, Term)]) -- alternatives by prefix: pre {t ; s/c ; ...}
|
||||
| Strs [Term] -- conditioning prefix strings: strs {s ; ...}
|
||||
|
||||
--- these three are obsolete
|
||||
| LiT Ident -- linearization type
|
||||
| Ready Str -- result of compiling; not to be parsed ...
|
||||
| Computed Term -- result of computing: not to be reopened nor parsed
|
||||
| Alts (Term, [(Term, Term)]) -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
|
||||
| Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@
|
||||
--
|
||||
-- /below this, the last three constructors are obsolete/
|
||||
| LiT Ident -- ^ linearization type
|
||||
| Ready Str -- ^ result of compiling; not to be parsed ...
|
||||
| Computed Term -- ^ result of computing: not to be reopened nor parsed
|
||||
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
data Patt =
|
||||
PC Ident [Patt] -- constructor pattern: C p1 ... pn C
|
||||
| PP Ident Ident [Patt] -- package constructor pattern: P.C p1 ... pn P.C
|
||||
| PV Ident -- variable pattern: x
|
||||
| PW -- wild card pattern: _
|
||||
| PR [(Label,Patt)] -- record pattern: {r = p ; ...} -- only concrete
|
||||
| PString String -- string literal pattern: "foo" -- only abstract
|
||||
| PInt Int -- integer literal pattern: 12 -- only abstract
|
||||
| PT Type Patt -- type-annotated pattern
|
||||
PC Ident [Patt] -- ^ constructor pattern: @C p1 ... pn@ @C@
|
||||
| PP Ident Ident [Patt] -- ^ package constructor pattern: @P.C p1 ... pn@ @P.C@
|
||||
| PV Ident -- ^ variable pattern: @x@
|
||||
| PW -- ^ wild card pattern: @_@
|
||||
| PR [(Label,Patt)] -- ^ record pattern: @{r = p ; ...}@ -- only concrete
|
||||
| PString String -- ^ string literal pattern: @\"foo\"@ -- only abstract
|
||||
| PInt Int -- ^ integer literal pattern: @12@ -- only abstract
|
||||
| PT Type Patt -- ^ type-annotated pattern
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
-- to guide computation and type checking of tables
|
||||
-- | to guide computation and type checking of tables
|
||||
data TInfo =
|
||||
TRaw -- received from parser; can be anything
|
||||
| TTyped Type -- type annontated, but can be anything
|
||||
| TComp Type -- expanded
|
||||
| TWild Type -- just one wild card pattern, no need to expand
|
||||
TRaw -- ^ received from parser; can be anything
|
||||
| TTyped Type -- ^ type annontated, but can be anything
|
||||
| TComp Type -- ^ expanded
|
||||
| TWild Type -- ^ just one wild card pattern, no need to expand
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
-- | record label
|
||||
data Label =
|
||||
LIdent String
|
||||
| LVar Int
|
||||
deriving (Read, Show, Eq, Ord) -- record label
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
newtype MetaSymb = MetaSymb Int deriving (Read, Show, Eq, Ord)
|
||||
|
||||
@@ -158,10 +202,11 @@ type Altern = (Term, [(Term, Term)])
|
||||
|
||||
type Substitution = [(Ident, Term)]
|
||||
|
||||
-- branches à la Alfa
|
||||
-- | branches à la Alfa
|
||||
newtype Branch = Branch (Con,([Ident],Term)) deriving (Eq, Ord,Show,Read)
|
||||
type Con = Ident ---
|
||||
|
||||
varLabel :: Int -> Label
|
||||
varLabel = LVar
|
||||
|
||||
wildPatt :: Patt
|
||||
|
||||
@@ -1,15 +1,17 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Lockfield
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.5 $
|
||||
--
|
||||
-- Creating and using lock fields in reused resource grammars.
|
||||
--
|
||||
-- AR 8\/2\/2005 detached from 'compile/MkResource'
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Lockfield (lockRecType, unlockRecord, lockLabel, isLockLabel) where
|
||||
@@ -21,8 +23,6 @@ import PrGrammar
|
||||
|
||||
import Operations
|
||||
|
||||
-- AR 8/2/2005 detached from compile/MkResource
|
||||
|
||||
lockRecType :: Ident -> Type -> Err Type
|
||||
lockRecType c t@(RecType rs) =
|
||||
let lab = lockLabel c in
|
||||
|
||||
@@ -1,18 +1,35 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : LookAbs
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.12 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module LookAbs where
|
||||
module LookAbs (GFCGrammar,
|
||||
lookupAbsDef,
|
||||
lookupFunType,
|
||||
lookupCatContext,
|
||||
lookupTransfer,
|
||||
isPrimitiveFun,
|
||||
lookupRef,
|
||||
refsForType,
|
||||
funRulesOf,
|
||||
allCatsOf,
|
||||
allBindCatsOf,
|
||||
funsForType,
|
||||
funsOnType,
|
||||
funsOnTypeFs,
|
||||
allDefs,
|
||||
lookupFunTypeSrc,
|
||||
lookupCatContextSrc
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import qualified GFC as C
|
||||
@@ -62,8 +79,7 @@ lookupCatContext gr m c = errIn ("looking up context of cat" +++ prt c) $ do
|
||||
_ -> prtBad "unknown category" c
|
||||
_ -> Bad $ prt m +++ "is not an abstract module"
|
||||
|
||||
-- lookup for transfer function: transfer-module-name, category name
|
||||
|
||||
-- | lookup for transfer function: transfer-module-name, category name
|
||||
lookupTransfer :: GFCGrammar -> Ident -> Ident -> Err Term
|
||||
lookupTransfer gr m c = errIn ("looking up transfer of cat" +++ prt c) $ do
|
||||
mi <- lookupModule gr m
|
||||
@@ -77,7 +93,7 @@ lookupTransfer gr m c = errIn ("looking up transfer of cat" +++ prt c) $ do
|
||||
_ -> Bad $ prt m +++ "is not a transfer module"
|
||||
|
||||
|
||||
---- should be revised (20/9/2003)
|
||||
-- | should be revised (20\/9\/2003)
|
||||
isPrimitiveFun :: GFCGrammar -> Fun -> Bool
|
||||
isPrimitiveFun gr (m,c) = case lookupAbsDef gr m c of
|
||||
Ok (Just (Eqs [])) -> True -- is canonical
|
||||
@@ -85,8 +101,7 @@ isPrimitiveFun gr (m,c) = case lookupAbsDef gr m c of
|
||||
_ -> True -- has no definition
|
||||
|
||||
|
||||
-- looking up refinement terms
|
||||
|
||||
-- | looking up refinement terms
|
||||
lookupRef :: GFCGrammar -> Binds -> Term -> Err Val
|
||||
lookupRef gr binds at = case at of
|
||||
Q m f -> lookupFunType gr m f >>= return . vClos
|
||||
@@ -147,8 +162,7 @@ allDefs gr = [((i,c),d) | (i, ModMod m) <- modules gr,
|
||||
isModAbs m,
|
||||
(c, C.AbsFun _ d) <- tree2list (jments m)]
|
||||
|
||||
-- this is needed at compile time
|
||||
|
||||
-- | this is needed at compile time
|
||||
lookupFunTypeSrc :: Grammar -> Ident -> Ident -> Err Type
|
||||
lookupFunTypeSrc gr m c = do
|
||||
mi <- lookupModule gr m
|
||||
@@ -161,6 +175,7 @@ lookupFunTypeSrc gr m c = do
|
||||
_ -> prtBad "cannot find type of" c
|
||||
_ -> Bad $ prt m +++ "is not an abstract module"
|
||||
|
||||
-- | this is needed at compile time
|
||||
lookupCatContextSrc :: Grammar -> Ident -> Ident -> Err Context
|
||||
lookupCatContextSrc gr m c = do
|
||||
mi <- lookupModule gr m
|
||||
|
||||
@@ -1,18 +1,29 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Lookup
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.12 $
|
||||
--
|
||||
-- Lookup in source (concrete and resource) when compiling.
|
||||
--
|
||||
-- lookup in resource and concrete in compiling; for abstract, use 'Look'
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Lookup where
|
||||
module Lookup (lookupResDef,
|
||||
lookupResType,
|
||||
lookupParams,
|
||||
lookupParamValues,
|
||||
lookupFirstTag,
|
||||
allParamValues,
|
||||
lookupAbsDef,
|
||||
lookupLincat,
|
||||
opersForType
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Abstract
|
||||
@@ -22,8 +33,6 @@ import Lockfield
|
||||
import List (nub)
|
||||
import Monad
|
||||
|
||||
-- lookup in resource and concrete in compiling; for abstract, use Look
|
||||
|
||||
lookupResDef :: SourceGrammar -> Ident -> Ident -> Err Term
|
||||
lookupResDef gr = look True where
|
||||
look isTop m c = do
|
||||
|
||||
@@ -1,15 +1,15 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : MMacros
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.6 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-- some more abstractions on grammars, esp. for Edit
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module MMacros where
|
||||
@@ -27,8 +27,6 @@ import Macros
|
||||
|
||||
import Monad
|
||||
|
||||
-- some more abstractions on grammars, esp. for Edit
|
||||
|
||||
nodeTree (Tr (n,_)) = n
|
||||
argsTree (Tr (_,ts)) = ts
|
||||
|
||||
@@ -69,7 +67,7 @@ changeMetaSubst f (N (b,a,v,(c,m),x)) = N (b,a,v,(c, f m),x)
|
||||
changeAtom :: (Atom -> Atom) -> TrNode -> TrNode
|
||||
changeAtom f (N (b,a,v,(c,m),x)) = N (b,f a,v,(c, m),x)
|
||||
|
||||
------ on the way to Edit
|
||||
-- * on the way to Edit
|
||||
|
||||
uTree :: Tree
|
||||
uTree = Tr (uNode, []) -- unknown tree
|
||||
@@ -139,7 +137,7 @@ substTerm ss g c = case c of
|
||||
metaSubstExp :: MetaSubst -> [(Meta,Exp)]
|
||||
metaSubstExp msubst = [(m, errVal (meta2exp m) (val2expSafe v)) | (m,v) <- msubst]
|
||||
|
||||
-- belong here rather than to computation
|
||||
-- * belong here rather than to computation
|
||||
|
||||
substitute :: [Var] -> Substitution -> Exp -> Err Exp
|
||||
substitute v s = return . substTerm v s
|
||||
@@ -245,7 +243,7 @@ fun2wrap oldvars ((fun,i),typ) exp = do
|
||||
let vars = mkFreshVars (length cont) oldvars
|
||||
return $ mkAbs vars $ if n==i then exp else mExp
|
||||
|
||||
-- weak heuristics: sameness of value category
|
||||
-- | weak heuristics: sameness of value category
|
||||
compatType :: Val -> Type -> Bool
|
||||
compatType v t = errVal True $ do
|
||||
cat1 <- val2cat v
|
||||
@@ -269,8 +267,7 @@ identVar (Vr x) = return x
|
||||
identVar _ = Bad "not a variable"
|
||||
|
||||
|
||||
-- light-weight rename for user interaction; also change names of internal vars
|
||||
|
||||
-- | light-weight rename for user interaction; also change names of internal vars
|
||||
qualifTerm :: Ident -> Term -> Term
|
||||
qualifTerm m = qualif [] where
|
||||
qualif xs t = case t of
|
||||
@@ -287,8 +284,7 @@ string2var s = case s of
|
||||
c:'_':i -> identV (readIntArg i,[c]) ---
|
||||
_ -> zIdent s
|
||||
|
||||
-- reindex variables so that they tell nesting depth level
|
||||
|
||||
-- | reindex variables so that they tell nesting depth level
|
||||
reindexTerm :: Term -> Term
|
||||
reindexTerm = qualif (0,[]) where
|
||||
qualif dg@(d,g) t = case t of
|
||||
|
||||
@@ -1,15 +1,19 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Macros
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:12 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.17 $
|
||||
--
|
||||
-- Macros for constructing and analysing source code terms.
|
||||
--
|
||||
-- operations on terms and types not involving lookup in or reference to grammars
|
||||
--
|
||||
-- AR 7\/12\/1999 - 9\/5\/2000 -- 4\/6\/2001
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Macros where
|
||||
@@ -23,10 +27,6 @@ import PrGrammar
|
||||
import Monad (liftM)
|
||||
import Char (isDigit)
|
||||
|
||||
-- AR 7/12/1999 - 9/5/2000 -- 4/6/2001
|
||||
|
||||
-- operations on terms and types not involving lookup in or reference to grammars
|
||||
|
||||
firstTypeForm :: Type -> Err (Context, Type)
|
||||
firstTypeForm t = case t of
|
||||
Prod x a b -> do
|
||||
@@ -366,7 +366,7 @@ varX i = identV (i,"x")
|
||||
mkFreshVar :: [Ident] -> Ident
|
||||
mkFreshVar olds = varX (maxVarIndex olds + 1)
|
||||
|
||||
-- trying to preserve a given symbol
|
||||
-- | trying to preserve a given symbol
|
||||
mkFreshVarX :: [Ident] -> Ident -> Ident
|
||||
mkFreshVarX olds x = if (elem x olds) then (varX (maxVarIndex olds + 1)) else x
|
||||
|
||||
@@ -376,22 +376,22 @@ maxVarIndex = maximum . ((-1):) . map varIndex
|
||||
mkFreshVars :: Int -> [Ident] -> [Ident]
|
||||
mkFreshVars n olds = [varX (maxVarIndex olds + i) | i <- [1..n]]
|
||||
|
||||
--- quick hack for refining with var in editor
|
||||
-- | quick hack for refining with var in editor
|
||||
freshAsTerm :: String -> Term
|
||||
freshAsTerm s = Vr (varX (readIntArg s))
|
||||
|
||||
-- create a terminal for concrete syntax
|
||||
-- | create a terminal for concrete syntax
|
||||
string2term :: String -> Term
|
||||
string2term = ccK
|
||||
|
||||
ccK = K
|
||||
ccC = C
|
||||
|
||||
-- create a terminal from identifier
|
||||
-- | create a terminal from identifier
|
||||
ident2terminal :: Ident -> Term
|
||||
ident2terminal = ccK . prIdent
|
||||
|
||||
-- create a constant
|
||||
-- | create a constant
|
||||
string2CnTrm :: String -> Term
|
||||
string2CnTrm = Cn . zIdent
|
||||
|
||||
@@ -441,7 +441,7 @@ mkFreshMetasInTrm metas = fst . rms minMeta where
|
||||
_ -> (trm,meta)
|
||||
minMeta = if null metas then 0 else (maximum (map metaSymbInt metas) + 1)
|
||||
|
||||
-- decides that a term has no metavariables
|
||||
-- | decides that a term has no metavariables
|
||||
isCompleteTerm :: Term -> Bool
|
||||
isCompleteTerm t = case t of
|
||||
Meta _ -> False
|
||||
@@ -492,7 +492,7 @@ redirectTerm n t = case t of
|
||||
Q _ f -> Q n f
|
||||
_ -> composSafeOp (redirectTerm n) t
|
||||
|
||||
-- to gather s-fields; assumes term in normal form, preserves label
|
||||
-- | to gather s-fields; assumes term in normal form, preserves label
|
||||
allLinFields :: Term -> Err [[(Label,Term)]]
|
||||
allLinFields trm = case unComputed trm of
|
||||
---- R rs -> return [[(l,t) | (l,(Just ty,t)) <- rs, isStrType ty]] -- good
|
||||
@@ -502,24 +502,24 @@ allLinFields trm = case unComputed trm of
|
||||
return $ concat lts
|
||||
_ -> prtBad "fields can only be sought in a record not in" trm
|
||||
|
||||
---- deprecated
|
||||
-- | deprecated
|
||||
isLinLabel l = case l of
|
||||
LIdent ('s':cs) | all isDigit cs -> True
|
||||
_ -> False
|
||||
|
||||
-- to gather ultimate cases in a table; preserves pattern list
|
||||
-- | to gather ultimate cases in a table; preserves pattern list
|
||||
allCaseValues :: Term -> [([Patt],Term)]
|
||||
allCaseValues trm = case unComputed trm of
|
||||
T _ cs -> [(p:ps, t) | (p,t0) <- cs, (ps,t) <- allCaseValues t0]
|
||||
_ -> [([],trm)]
|
||||
|
||||
-- to gather all linearizations; assumes normal form, preserves label and args
|
||||
-- | to gather all linearizations; assumes normal form, preserves label and args
|
||||
allLinValues :: Term -> Err [[(Label,[([Patt],Term)])]]
|
||||
allLinValues trm = do
|
||||
lts <- allLinFields trm
|
||||
mapM (mapPairsM (return . allCaseValues)) lts
|
||||
|
||||
-- to mark str parts of fields in a record f by a function f
|
||||
-- | to mark str parts of fields in a record f by a function f
|
||||
markLinFields :: (Term -> Term) -> Term -> Term
|
||||
markLinFields f t = case t of
|
||||
R r -> R $ map mkField r
|
||||
@@ -530,7 +530,7 @@ markLinFields f t = case t of
|
||||
T i cs -> T i [(p, mkTbl v) | (p,v) <- cs]
|
||||
_ -> f t
|
||||
|
||||
-- to get a string from a term that represents a sequence of terminals
|
||||
-- | to get a string from a term that represents a sequence of terminals
|
||||
strsFromTerm :: Term -> Err [Str]
|
||||
strsFromTerm t = case unComputed t of
|
||||
K s -> return [str s]
|
||||
@@ -558,13 +558,12 @@ strsFromTerm t = case unComputed t of
|
||||
Alias _ _ d -> strsFromTerm d --- should not be needed...
|
||||
_ -> prtBad "cannot get Str from term" t
|
||||
|
||||
-- to print an Str-denoting term as a string; if the term is of wrong type, the error msg
|
||||
-- | to print an Str-denoting term as a string; if the term is of wrong type, the error msg
|
||||
stringFromTerm :: Term -> String
|
||||
stringFromTerm = err id (ifNull "" (sstr . head)) . strsFromTerm
|
||||
|
||||
|
||||
-- to define compositional term functions
|
||||
|
||||
-- | to define compositional term functions
|
||||
composSafeOp :: (Term -> Term) -> Term -> Term
|
||||
composSafeOp op trm = case composOp (mkMonadic op) trm of
|
||||
Ok t -> t
|
||||
@@ -572,6 +571,7 @@ composSafeOp op trm = case composOp (mkMonadic op) trm of
|
||||
where
|
||||
mkMonadic f = return . f
|
||||
|
||||
-- | to define compositional term functions
|
||||
composOp :: Monad m => (Term -> m Term) -> Term -> m Term
|
||||
composOp co trm =
|
||||
case trm of
|
||||
@@ -686,8 +686,7 @@ collectOp co trm = case trm of
|
||||
Strs tt -> concatMap co tt
|
||||
_ -> [] -- covers K, Vr, Cn, Sort, Ready
|
||||
|
||||
-- to find the word items in a term
|
||||
|
||||
-- | to find the word items in a term
|
||||
wordsInTerm :: Term -> [String]
|
||||
wordsInTerm trm = filter (not . null) $ case trm of
|
||||
K s -> [s]
|
||||
@@ -705,8 +704,7 @@ defaultLinType = mkRecType linLabel [typeStr]
|
||||
metaTerms :: [Term]
|
||||
metaTerms = map (Meta . MetaSymb) [0..]
|
||||
|
||||
-- from GF1, 20/9/2003
|
||||
|
||||
-- | from GF1, 20\/9\/2003
|
||||
isInOneType :: Type -> Bool
|
||||
isInOneType t = case t of
|
||||
Prod _ a b -> a == b
|
||||
|
||||
@@ -1,18 +1,21 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : PatternMatch
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.5 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-- pattern matching for both concrete and abstract syntax. AR -- 16\/6\/2003
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module PatternMatch where
|
||||
module PatternMatch (matchPattern,
|
||||
testOvershadow,
|
||||
findMatch
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Grammar
|
||||
@@ -23,8 +26,6 @@ import PrGrammar
|
||||
import List
|
||||
import Monad
|
||||
|
||||
-- pattern matching for both concrete and abstract syntax. AR -- 16/6/2003
|
||||
|
||||
|
||||
matchPattern :: [(Patt,Term)] -> Term -> Err (Term, Substitution)
|
||||
matchPattern pts term =
|
||||
@@ -105,7 +106,7 @@ varsOfPatt p = case p of
|
||||
PT _ q -> varsOfPatt q
|
||||
_ -> []
|
||||
|
||||
-- to search matching parameter combinations in tables
|
||||
-- | to search matching parameter combinations in tables
|
||||
isMatchingForms :: [Patt] -> [Term] -> Bool
|
||||
isMatchingForms ps ts = all match (zip ps ts') where
|
||||
match (PC c cs, (Cn d, ds)) = c == d && isMatchingForms cs ds
|
||||
|
||||
@@ -1,18 +1,36 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : PrGrammar
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.11 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-- AR 7\/12\/1999 - 1\/4\/2000 - 10\/5\/2003
|
||||
--
|
||||
-- printing and prettyprinting class
|
||||
--
|
||||
-- 8\/1\/2004:
|
||||
-- Usually followed principle: 'prt_' for displaying in the editor, 'prt'
|
||||
-- in writing grammars to a file. For some constructs, e.g. 'prMarkedTree',
|
||||
-- only the former is ever needed.
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module PrGrammar where
|
||||
module PrGrammar (Print(..),
|
||||
prtBad,
|
||||
prGrammar, prModule,
|
||||
prContext, prParam,
|
||||
prQIdent, prQIdent_,
|
||||
prRefinement, prTermOpt,
|
||||
prt_Tree, prMarkedTree, prTree,
|
||||
tree2string, prprTree,
|
||||
prConstrs, prConstraints,
|
||||
prMetaSubst, prEnv, prMSubst,
|
||||
prExp, prPatt, prOperSignature
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Zipper
|
||||
@@ -30,15 +48,14 @@ import Str
|
||||
|
||||
import List (intersperse)
|
||||
|
||||
-- AR 7/12/1999 - 1/4/2000 - 10/5/2003
|
||||
|
||||
-- printing and prettyprinting class
|
||||
|
||||
class Print a where
|
||||
prt :: a -> String
|
||||
prt2 :: a -> String -- printing with parentheses, if needed
|
||||
prpr :: a -> [String] -- pretty printing
|
||||
prt_ :: a -> String -- printing without ident qualifications
|
||||
-- | printing with parentheses, if needed
|
||||
prt2 :: a -> String
|
||||
-- | pretty printing
|
||||
prpr :: a -> [String]
|
||||
-- | printing without ident qualifications
|
||||
prt_ :: a -> String
|
||||
prt2 = prt
|
||||
prt_ = prt
|
||||
prpr = return . prt
|
||||
@@ -48,11 +65,14 @@ class Print a where
|
||||
--- in writing grammars to a file. For some constructs, e.g. prMarkedTree,
|
||||
--- only the former is ever needed.
|
||||
|
||||
-- to show terms etc in error messages
|
||||
-- | to show terms etc in error messages
|
||||
prtBad :: Print a => String -> a -> Err b
|
||||
prtBad s a = Bad (s +++ prt a)
|
||||
|
||||
prGrammar :: SourceGrammar -> String
|
||||
prGrammar = P.printTree . trGrammar
|
||||
|
||||
prModule :: (Ident, SourceModInfo) -> String
|
||||
prModule = P.printTree . trModule
|
||||
|
||||
instance Print Term where
|
||||
@@ -108,7 +128,7 @@ instance Print a => Print (Tr a) where
|
||||
prt (Tr (n, trees)) = prt n +++ unwords (map prt2 trees)
|
||||
prt2 t@(Tr (_,args)) = if null args then prt t else prParenth (prt t)
|
||||
|
||||
-- we cannot define the method prt_ in this way
|
||||
-- | we cannot define the method prt_ in this way
|
||||
prt_Tree :: Tree -> String
|
||||
prt_Tree = prt_ . tree2exp
|
||||
|
||||
@@ -133,7 +153,8 @@ prMarkedTree = prf 1 where
|
||||
prTree :: Tree -> [String]
|
||||
prTree = prMarkedTree . mapTr (\n -> (n,False))
|
||||
|
||||
-- a pretty-printer for parsable output
|
||||
-- | a pretty-printer for parsable output
|
||||
tree2string :: Tree -> String
|
||||
tree2string = unlines . prprTree
|
||||
|
||||
prprTree :: Tree -> [String]
|
||||
@@ -204,8 +225,7 @@ prQIdent (m,f) = prt m ++ "." ++ prt f
|
||||
prQIdent_ :: QIdent -> String
|
||||
prQIdent_ (_,f) = prt f
|
||||
|
||||
-- print terms without qualifications
|
||||
|
||||
-- | print terms without qualifications
|
||||
prExp :: Term -> String
|
||||
prExp e = case e of
|
||||
App f a -> pr1 f +++ pr2 a
|
||||
@@ -232,10 +252,12 @@ prPatt p = case p of
|
||||
A.PC _ (_:_) -> prParenth $ prPatt p
|
||||
_ -> prPatt p
|
||||
|
||||
-- option -strip strips qualifications
|
||||
-- | option @-strip@ strips qualifications
|
||||
prTermOpt :: Options -> Term -> String
|
||||
prTermOpt opts = if oElem nostripQualif opts then prt else prExp
|
||||
|
||||
--- to get rid of brackets in the editor
|
||||
-- | to get rid of brackets in the editor
|
||||
prRefinement :: Term -> String
|
||||
prRefinement t = case t of
|
||||
Q m c -> prQIdent (m,c)
|
||||
QC m c -> prQIdent (m,c)
|
||||
|
||||
@@ -1,18 +1,20 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Refresh
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.5 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Refresh where
|
||||
module Refresh (refreshTerm, refreshTermN,
|
||||
refreshModule
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Grammar
|
||||
|
||||
@@ -1,25 +1,23 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : ReservedWords
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.4 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-- reserved words of GF. (c) Aarne Ranta 19\/3\/2002 under Gnu GPL.
|
||||
-- modified by Markus Forsberg 9\/4.
|
||||
-- modified by AR 12\/6\/2003 for GF2 and GFC
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module ReservedWords (isResWord, isResWordGFC) where
|
||||
|
||||
import List
|
||||
|
||||
-- reserved words of GF. (c) Aarne Ranta 19/3/2002 under Gnu GPL
|
||||
-- modified by Markus Forsberg 9/4.
|
||||
-- modified by AR 12/6/2003 for GF2 and GFC
|
||||
|
||||
|
||||
isResWord :: String -> Bool
|
||||
isResWord s = isInTree s resWordTree
|
||||
|
||||
@@ -1,18 +1,24 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : TC
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.7 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-- Thierry Coquand's type checking algorithm that creates a trace
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module TC where
|
||||
module TC (AExp(..),
|
||||
Theory,
|
||||
checkExp,
|
||||
inferExp,
|
||||
eqVal,
|
||||
whnf
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Abstract
|
||||
@@ -20,8 +26,6 @@ import AbsCompute
|
||||
|
||||
import Monad
|
||||
|
||||
-- Thierry Coquand's type checking algorithm that creates a trace
|
||||
|
||||
data AExp =
|
||||
AVr Ident Val
|
||||
| ACn QIdent Val
|
||||
|
||||
@@ -1,18 +1,37 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : TypeCheck
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.13 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module TypeCheck where
|
||||
module TypeCheck (-- * top-level type checking functions; TC should not be called directly.
|
||||
annotate, annotateIn,
|
||||
justTypeCheck, checkIfValidExp,
|
||||
reduceConstraints,
|
||||
splitConstraints,
|
||||
possibleConstraints,
|
||||
reduceConstraintsNode,
|
||||
performMetaSubstNode,
|
||||
-- * some top-level batch-mode checkers for the compiler
|
||||
justTypeCheckSrc,
|
||||
grammar2theorySrc,
|
||||
checkContext,
|
||||
checkTyp,
|
||||
checkEquation,
|
||||
checkConstrs,
|
||||
editAsTermCommand,
|
||||
exp2termCommand,
|
||||
exp2termlistCommand,
|
||||
tree2termlistCommand
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Zipper
|
||||
@@ -35,14 +54,14 @@ import List (nub) ---
|
||||
annotate :: GFCGrammar -> Exp -> Err Tree
|
||||
annotate gr exp = annotateIn gr [] exp Nothing
|
||||
|
||||
-- type check in empty context, return a list of constraints
|
||||
-- | type check in empty context, return a list of constraints
|
||||
justTypeCheck :: GFCGrammar -> Exp -> Val -> Err Constraints
|
||||
justTypeCheck gr e v = do
|
||||
(_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
|
||||
constrs1 <- reduceConstraints (lookupAbsDef gr) 0 constrs0
|
||||
return $ fst $ splitConstraints gr constrs1
|
||||
|
||||
-- type check in empty context, return the expression itself if valid
|
||||
-- | type check in empty context, return the expression itself if valid
|
||||
checkIfValidExp :: GFCGrammar -> Exp -> Err Exp
|
||||
checkIfValidExp gr e = do
|
||||
(_,_,constrs0) <- inferExp (grammar2theory gr) (initTCEnv []) e
|
||||
@@ -63,11 +82,11 @@ annotateIn gr gamma exp = maybe (infer exp) (check exp) where
|
||||
c' <- reduceConstraints (lookupAbsDef gr) (length gamma) c
|
||||
aexp2tree (a,c')
|
||||
|
||||
-- invariant way of creating TCEnv from context
|
||||
-- | invariant way of creating TCEnv from context
|
||||
initTCEnv gamma =
|
||||
(length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
|
||||
|
||||
-- process constraints after eqVal by computing by defs
|
||||
-- | process constraints after eqVal by computing by defs
|
||||
reduceConstraints :: LookDef -> Int -> Constraints -> Err Constraints
|
||||
reduceConstraints look i = liftM concat . mapM redOne where
|
||||
redOne (u,v) = do
|
||||
@@ -92,7 +111,7 @@ computeVal look v = case v of
|
||||
compt = computeAbsTermIn look
|
||||
compv = computeVal look
|
||||
|
||||
-- take apart constraints that have the form (? <> t), usable as solutions
|
||||
-- | take apart constraints that have the form (? <> t), usable as solutions
|
||||
splitConstraints :: GFCGrammar -> Constraints -> (Constraints,MetaSubst)
|
||||
splitConstraints gr = splitConstraintsGen (lookupAbsDef gr)
|
||||
|
||||
@@ -141,10 +160,11 @@ performMetaSubstNode subst n@(N (b,a,v,(c,m),s)) = let
|
||||
Meta m -> errVal e $ maybe (return e) val2expSafe $ lookup m subst
|
||||
_ -> composSafeOp metaSubstExp e
|
||||
|
||||
reduceConstraintsNode :: GFCGrammar -> TrNode -> TrNode
|
||||
reduceConstraintsNode gr = changeConstrs red where
|
||||
red cs = errVal cs $ reduceConstraints (lookupAbsDef gr) 0 cs
|
||||
|
||||
-- weak heuristic to narrow down menus; not used for TC. 15/11/2001
|
||||
-- | weak heuristic to narrow down menus; not used for TC. 15\/11\/2001.
|
||||
-- the age-old method from GF 0.9
|
||||
possibleConstraints :: GFCGrammar -> Constraints -> Bool
|
||||
possibleConstraints gr = and . map (possibleConstraint gr)
|
||||
|
||||
@@ -1,18 +1,21 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Unify
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.3 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-- (c) Petri Mäenpää & Aarne Ranta, 1998--2001
|
||||
--
|
||||
-- brute-force adaptation of the old-GF program AR 21\/12\/2001 ---
|
||||
-- the only use is in 'TypeCheck.splitConstraints'
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Unify where
|
||||
module Unify (unifyVal) where
|
||||
|
||||
import Abstract
|
||||
|
||||
@@ -20,11 +23,6 @@ import Operations
|
||||
|
||||
import List (partition)
|
||||
|
||||
-- (c) Petri Mäenpää & Aarne Ranta, 1998--2001
|
||||
|
||||
-- brute-force adaptation of the old-GF program AR 21/12/2001 ---
|
||||
-- the only use is in TypeCheck.splitConstraints
|
||||
|
||||
unifyVal :: Constraints -> Err (Constraints,MetaSubst)
|
||||
unifyVal cs0 = do
|
||||
let (cs1,cs2) = partition notSolvable cs0
|
||||
|
||||
@@ -1,18 +1,27 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : (Module)
|
||||
-- Maintainer : (Maintainer)
|
||||
-- Module : Values
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date $
|
||||
-- > CVS $Author $
|
||||
-- > CVS $Revision $
|
||||
-- > CVS $Date: 2005/02/18 19:21:13 $
|
||||
-- > CVS $Author: peb $
|
||||
-- > CVS $Revision: 1.6 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module Values where
|
||||
module Values (-- * values used in TC type checking
|
||||
Exp, Val(..), Env,
|
||||
-- * annotated tree used in editing
|
||||
Tree, TrNode(..), Atom(..), Binds, Constraints, MetaSubst,
|
||||
-- * for TC
|
||||
valAbsInt, valAbsString, vType,
|
||||
isPredefCat,
|
||||
cType, cPredefAbs, cInt, cString,
|
||||
eType, tree2exp, loc2treeFocus
|
||||
) where
|
||||
|
||||
import Operations
|
||||
import Zipper
|
||||
@@ -45,19 +54,28 @@ type MetaSubst = [(MetaSymb,Val)]
|
||||
|
||||
-- for TC
|
||||
|
||||
valAbsInt, valAbsString :: Val
|
||||
valAbsInt :: Val
|
||||
valAbsInt = VCn (cPredefAbs, cInt)
|
||||
|
||||
valAbsString :: Val
|
||||
valAbsString = VCn (cPredefAbs, cString)
|
||||
|
||||
vType :: Val
|
||||
vType = VType
|
||||
|
||||
cType,cPredefAbs,cInt,cString :: Ident
|
||||
cType :: Ident
|
||||
cType = identC "Type" --- #0
|
||||
|
||||
cPredefAbs :: Ident
|
||||
cPredefAbs = identC "PredefAbs"
|
||||
|
||||
cInt :: Ident
|
||||
cInt = identC "Int"
|
||||
|
||||
cString :: Ident
|
||||
cString = identC "String"
|
||||
|
||||
isPredefCat :: Ident -> Bool
|
||||
isPredefCat c = elem c [cInt,cString]
|
||||
|
||||
eType :: Exp
|
||||
|
||||
Reference in New Issue
Block a user