1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 |
------------------------------------------------------------------------------ --- This module contains operations to transform FlatCurry entities --- into some normalized form so that they can be easier compared --- for equivalence. --- --- For instance, a type expression is normalize by replacing --- type variable indices into a uniquely enumerated form. --- --- @author Michael Hanus --- @version May 2021 ------------------------------------------------------------------------------ module FlatCurry.Normalize ( normalizeTypeExpr ) where import Control.Monad.Trans.State import FlatCurry.Types ------------------------------------------------------------------------------ -- The state used during the normalization process. -- The state consists of a current number for enumerating type variables -- and a mapping from the original type variable indices into -- normalized indices (which will be expanded during the transformation). data TransInfo = TransInfo { currNr :: TVarIndex , tvarMap :: [(TVarIndex,TVarIndex)] } -- The initial state. initState :: TransInfo initState = TransInfo 0 [] -- The type of the state normalization monad. type TransState a = State TransInfo a -- Auxiliary operation: get a unique index for a given type variable. -- Either return the existing index or create a fresh one and update -- the state. getTVarIndex :: TVarIndex -> TransState TVarIndex getTVarIndex v = do ti <- get maybe (do let nv = currNr ti put ti { currNr = nv + 1, tvarMap = (v,nv) : tvarMap ti } return nv ) return (lookup v (tvarMap ti)) ------------------------------------------------------------------------------ --- Normalize a type expression by enumerating the type variables --- starting from `0`. normalizeTypeExpr :: TypeExpr -> TypeExpr normalizeTypeExpr texp = evalState (normTExp texp) initState -- The actual implementation of the normalization task performs -- a monadic traversal over the given type expression. normTExp :: TypeExpr -> TransState TypeExpr normTExp texp = case texp of TVar v -> do vi <- getTVarIndex v return $ TVar vi FuncType t1 t2 -> do nt1 <- normTExp t1 nt2 <- normTExp t2 return (FuncType nt1 nt2) TCons qn tes -> do ntes <- mapM normTExp tes return $ TCons qn ntes ForallType tvs te -> do ntvs <- mapM normTVarWithKind tvs nte <- normTExp te return $ ForallType ntvs nte where normTVarWithKind (v,k) = do vi <- getTVarIndex v return (vi,k) ----------------------------------------------------------------------- |