$Id: TypeHelpers.lhs,v 1.22 2004/10/18 23:47:48 leavens Exp leavens $ Some helpful functions for type checking with type environments. AUTHOR: Gary T. Leavens, with help from Brian Dorn To use this module, you may need to make your own copy of TypeAttributes, and change the definition of PrimitiveAttrib there. (Ideally, this module would be independent of the primitive type attributes defined in TypeAttributes, and could thus be easily reused for different languages. Unfortunately, in Haskell, there seems to be no easy way to do this, although with an ML-style functor it would be easy.) > module TypeHelpers(module TypeHelpers, module Tree, > module TypeAttributes) where > import Tree > import Environments > import TypeAttributes > import Subst > import List (intersect) We make the precedence of :- (and :?-) be lower than :::, so that :- binds less tightly. Thus one can write (pi :- e ::: tau) without having to put extra parentheses in, and it still means (pi :- (e ::: tau)). > infix 9 ::: > infix 8 :-, :?- The rule combinator, `ruleOr`, is useful to have as an infix operator. > infixl 0 `ruleOr` ATTRIBUTED SYNTAX TREES Attributed syntax trees are a pair that contains a piece of syntax and some kind of attribute. The ::: is the constructor for such pairs. > data AttribTree syntax attrib = > syntax ::: attrib The following instance of show shows the syntax and the attribute, separated by a colon. > instance (Show syntax, Show attrib) => Show (AttribTree syntax attrib) where > showsPrec p (s ::: atr) = showsPrec p s . showString " : " > . showsPrec p atr ATrees are attributed syntax trees where the attributes are trees of primitive attributes. This allows the attributes of subtrees to be recovered if needed. > type ATree syntax = > AttribTree syntax > (Tree PrimitiveAttrib) The following instance of Show shows only the root attribute. This is easier for humans to read, although sometimes seeing the entire tree is more helpful. > instance (Show attrib) => Show (Tree attrib) where > showsPrec p (Node r _) = showsPrec p r TYPE ENVIRONMENTS Type environments are finite functions from Strings to primitive attributes. > type TypeEnv = FiniteFun String PrimitiveAttrib > emptyTypeEnv :: TypeEnv > emptyTypeEnv = emptyEnv TYPE JUDGEMENTS Typing judgements with inherited attributes that are type environments are defined by the following. The second form allows the inherited attribute to be a logical variable. This is only useful in certain declaration forms; normally the first kind of judgement would be used. > data Judgement atree = TypeEnv :- atree > | LogicalVar :?- atree And of course, we need an instance of Show for judgements. > instance (Show atree) => Show (Judgement atree) where > showsPrec p (pi :- atr) = showsPrec p pi . showString " |- " > . showsPrec p atr > showsPrec p (lv :?- atr) = showsPrec p lv . showString " |?- " > . showsPrec p atr ANNOTATABLE CLASS The function "annotate" is overloaded on each syntactic domain in the abstract syntax. The class declaration that follows declares the shape of these functions. Unfortunately, this declaration is also the source of the coupling between this module and TypeAttributes, because if the type of the primitive type attributes was polymorphic, then the requirement on instances of this class would be that they also have a polymorphic annotate function. > class Annotatable a where > annotate :: TypeEnv -> a -> TreeNSubst a The type TreeNSubst is used in the return type of annotate and the rules. They are essentially pairs, but a data definition is used so we can define show for them. > data TreeNSubst a = Tree_Subst (ATree a) [Subst PrimitiveAttrib] > instance (Show a) => Show (TreeNSubst a) where > showsPrec p (Tree_Subst a _) = showsPrec p a HELPERS FOR WRITING TYPE CHECKING RULES Note: the functions below have different interfaces than the ones in CoreTypeHelpers. Examples The following are examples of how to use the functions defined below. The horizontal lines are simply Haskell comments, but they look nice (:->). The following are examples of the basic helpers; you can do almost everything with these two. annotate pi Skip = axiom (pi :- Skip ::: Acomm) annotate pi d@(Fun i e) = rule [pi :- Expr e ::: Aexp (Avar tau)] ---------------------------------------------- (pi :- d ::: Adec (Api [(i, Aexp (Avar tau))])) where tau = (0, "tau") The rule example also shows how to use logical variables to express simple dependencies of the resulting type on the types of parts of the hypothesis. Often you won't need even this complication. But note the use of Aexp (Avar tau) instead of just the type attribute (Avar tau). A type error (Aerr) will not unify with Aexp (Avar tau), hence if an error is detected in the hypothesis, the rule as a whole will generate an error, as desired. A convenience that allows more fine-grained splitting of rules into cases is the ruleOr combinator. This combines two rules. (The rules combined don't have to be programmed with "rule", it just happens to work that way in common examples.) annotate pi e@(e1 `Equals` e2) = (rule [pi :- e1 ::: Aexp Aint, pi :- e2 ::: Aexp Aint] -------------------------- (pi :- e ::: (Aexp Abool))) `ruleOr` (rule [pi :- e1 ::: Aexp Abool, pi :- e2 ::: Aexp Abool] -------------------------- (pi :- e ::: (Aexp Abool))) For rules with side conditions the ruleIf form usually suffices. The following is an example (of how to use it for sequential declarations). More explanation follows the example. annotate pi d@(d1 `Also` d2) = ruleIf [pi :- Decl d1 ::: Adec (Avar pi1), pi :- Decl d2 ::: Adec (Avar pi2)] (\[t1, t2] -> isDisjoint t1 t2) (\[Adec (Api ff1), Adec (Api ff2)] -> (pi3 ->- Api (uniondisjoint ff1 ff2))) ---------------------------------- (pi :- d ::: Adec (Avar pi3)) where pi1 = (1, "pi") pi2 = (2, "pi") pi3 = (3, "pi") isDisjoint t1 t2 = ... uniondisjoint ff1 ff2 = ... Notice that the ruleIf helper takes two functions as side conditions. The first is a function from the type attributes to a boolean value. If this returns True, then the type attributes are passed to the second, which is to return a substitution. This substitution can define the values of logical variables used in the conclusion, based on the values of the logical variables that result from checking the hypotheses. Note that the substitution returned by the second side condition function is computed last, so it can't affect the checking of the hypotheses or the type attributes passed to the first side condition function. You are guaranteed that the argument passed to the first side condition function in ruleIf is a list with the same number of elements as the list of hypotheses, and that the type attributes unify with expected attributes. Thus, if errors are detected, the first function is not even called. You are also guaranteed that the second side condition function is only called if the first returns True. On thing you can't do with the helpers shown above is sequential declarations. For this you need a specialized form, ruleSeq. This processes its first argument list sequentially (see example below). Each element of this list is tagged. Ones with the tag "Hyp" are hypotheses, and do checking for expected type attributes, but the judgement form (pi :?- s :::t) allows the type environment (pi) to be a logical variable, which is substituted for before the checking is done. Ones with the tag "Def" and "When" are side condition functions that are passed the list of attributes so far. The "Def" functions return a substitution, which can be used to define the values of logical variables to be used later. Ones with the tag "When" are tests that return booleans; these stop most checking if they return False. annotate pi d@(d1 `Then` d2) = ruleSeq [Hyp (pi :- Decl d1 ::: Adec (Avar pi1)), Def (\[Adec (Api ff1)] -> (pi4 ->- Api (pi `unionMinus` ff1))), Hyp (pi4 :?- Decl d2 ::: Adec (Avar pi2)), When (\[t1, t2] -> isDisjoint t1 t2), Def (\[Adec (Api ff1), Adec (Api ff2)] -> (pi3 ->- Api (uniondisjoint ff1 ff2) ))] ------------------------------------------ (pi :- d ::: Adec (Avar pi3)) where pi1 = (1, "pi") pi2 = (2, "pi") pi3 = (3, "pi") pi4 = (4, "pi") Implementations A rule without hypotheses is an axiom. We make this strict in its type environment, to allow better error handling. > axiom :: Annotatable csyn => > Judgement (AttribTree csyn PrimitiveAttrib) > -> TreeNSubst csyn > axiom (pi :- syn ::: tau) = > pi `seq` Tree_Subst (syn ::: Node tau []) [nullSubst] The "rule" helper doesn't allow side conditions. It is implemented by just calling the "ruleIf" form with vacuous side conditions. > rule :: (Annotatable hsyn, Annotatable csyn) => > [Judgement (AttribTree hsyn PrimitiveAttrib)] > -> Judgement (AttribTree csyn PrimitiveAttrib) > -> TreeNSubst csyn > rule hs conc = ruleSeq (map Hyp hs) conc A sequential case analysis is provided by ruleOr > ruleOr :: TreeNSubst csyn -> TreeNSubst csyn -> TreeNSubst csyn > t1@(Tree_Subst (_ ::: (Node pta ts)) _) `ruleOr` t2 = > if (Aerr /= pta) then t1 else t2 Rules with side conditions are handled in ruleIf. Note that it actually takes two side condition functions, as described above. > ruleIf :: (Annotatable hsyn, Annotatable csyn) => > [Judgement (AttribTree hsyn PrimitiveAttrib)] > -> ([PrimitiveAttrib] -> Bool) > -> ([PrimitiveAttrib] -> Subst PrimitiveAttrib) > -> Judgement (AttribTree csyn PrimitiveAttrib) > -> TreeNSubst csyn > ruleIf hs side_cond side_defs conclusion = > ruleSeq ((map Hyp hs) ++ [When side_cond, Def side_defs]) conclusion The following helper function is used in the next form. > map_tops :: (a -> a) -> [(Tree a)] -> [(Tree a)] > map_tops f ts = map (\(Node t ls) -> (Node (f t) ls)) ts The form ruleSeq is for sequentially processing hypotheses and side conditions, as occurs in sequential declarations. It also allows the type environment computed in one hypothesis to be used in the next. The data type (Mixed hyn) is for mixing true hypotheses with side conditions and side definitions that are to be executed to define new substitutions or to test for some correctness condition before going on to the next hypothesis. > data Mixed hsyn = Hyp (Judgement (AttribTree hsyn PrimitiveAttrib)) > | When ([PrimitiveAttrib] -> Bool) > | Def ([PrimitiveAttrib] -> Subst PrimitiveAttrib) > ruleSeq :: (Annotatable hsyn, Annotatable csyn) => > [Mixed hsyn] > -> Judgement (AttribTree csyn PrimitiveAttrib) > -> TreeNSubst csyn > ruleSeq hs (pi0 :- syn ::: tau) = > pi0 `seq` > (case substl of > [s] -> let ts = map_tops (app s) result_trees > in (Tree_Subst (syn ::: Node (app s tau) ts) substl) > _ -> (Tree_Subst (syn ::: Node Aerr result_trees) [nullSubst])) > where > (result_trees, substl) = sequence hs ([], [nullSubst]) > sequence :: Annotatable hsyn => > [Mixed hsyn] > -> ([Tree PrimitiveAttrib], [Subst PrimitiveAttrib]) > -> ([Tree PrimitiveAttrib], [Subst PrimitiveAttrib]) > -- sequence hs (attrs, cur_subst_l) > -- uses two "accumulators": attrs, and cur_subst_l > -- attrs is attributes of each hypotheses checked, > -- this is kept in order, not reversed > -- cur_subst_l is either the empty list > -- or a substitution > -- when cur_subst_l is [], we've seen a type error > sequence [] (attrs, cur_subst_l) = (attrs, cur_subst_l) > sequence (Def f:hs) (attrs, [cur_subst]) = > let delta_subst = f (map root attrs) > in sequence hs (attrs, [cur_subst @@ delta_subst]) > sequence (Def f:hs) (attrs, []) = > -- already working on a type error, so ignore this > sequence hs (attrs, []) > sequence (When p:hs) (attrs, [cur_subst]) = > if p (map root attrs) > then sequence hs (attrs, [cur_subst]) > else sequence hs (attrs, []) > sequence (When p:hs) (attrs, []) = > -- already working on a type error, so ignore this > sequence hs (attrs, []) > sequence (Hyp (pi :- s ::: expected):hs) (attrs, [cur_subst]) = > case (resultsubl, mgu (renaming t) expected) of > ([resultsub], [delta_subst]) -> > let new_subst = cur_subst @@ (resultsub @@ delta_subst) > t' = app new_subst (renaming t) > in sequence hs (attrs ++ [Node t' ts], [new_subst]) > _ -> -- no result substitution or no unifier (type error) > sequence hs (attrs ++ [attr], []) > where (Tree_Subst (_::: attr@(Node t ts)) resultsubl) = annotate pi s > renaming = if intersect (varsIn t) (varsIn expected) == [] > then (\trm -> trm) > else renameVars (1 + foldl1 max > (map (\(i,_) -> i) > (varsIn expected) > )) > sequence (Hyp (lv :?- s ::: expected):hs) (attrs, [cur_subst]) = > case app cur_subst (Avar lv) of > (Api pi) -> > sequence (Hyp (pi :- s ::: expected):hs) > (attrs, [cur_subst]) > _ -> -- bad binding for this logical variable > -- this is an error in the rule being processed... > error ("bad binding for logical var" ++ (show lv)) > sequence (Hyp (pi :- s ::: expected):hs) (attrs, []) = > -- the current substitution indicates a type error, > -- carry on as best we can > let (Tree_Subst (_::: attr) _) = annotate pi s > in sequence hs (attrs ++ [attr], []) > sequence (Hyp (lv :?- _ ::: expected):hs) (attrs, []) = > -- the current substitution indicates a type error, > -- but we can't do much here, > -- since we don't have a type assignment > sequence hs (attrs ++ [Node expected []], [])