$Id: CoreTypeHelpers.lhs,v 1.6 2004/10/18 23:47:48 leavens Exp leavens $ Some helpful functions for type checking (without type environments). AUTHOR: Gary T. Leavens To use this module, you may need to make your own copy of CoreTypeAttributes, 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 CoreTypeHelpers(module CoreTypeHelpers, module Tree, > module CoreTypeAttributes) where > import Tree > import CoreTypeAttributes > import Subst > infix 9 ::: 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 attrisbuted 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 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 :: 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 Skip = axiom (Skip ::: Acomm) annotate e@(Deref l) = rule [Loct l ::: Aloc (Avar tau)] ---------------------------------------------- (e ::: 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 Aloc (Avar tau) instead of just the type attribute (Avar tau). A type error (Aerr) will not unify with Aloc (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 e@(e1 `Equals` e2) = (rule [e1 ::: Aexp Aint, e2 ::: Aexp Aint] -------------------------- (e ::: (Aexp Abool))) `ruleOr` (rule [e1 ::: Aexp Abool, e2 ::: Aexp Abool] -------------------------- (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 declartions). More explanation follows the example. annotate e@(e1 `Equals` e2) = ruleIf [Expr e1 ::: Aexp (Avar tau1), Expr e2 ::: Aexp (Avar tau2)] (\[Aexp t1, Aexp t2] -> t1 == t2 && isAtomic t1) (\_ -> nullSubst) ---------------------------------- (e ::: Aexp Abool) where tau1 = (1, "tau") tau2 = (2, "tau") isAtomic Aint = True isAtomic Abool = True isAtomic _ = False 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. Implementations A rule without hypotheses is an axiom. We make this strict in its type environment, to allow better error handling. > axiom :: Annotatable csyn => > AttribTree csyn PrimitiveAttrib -> TreeNSubst csyn > axiom (syn ::: tau) = 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) => > [(AttribTree hsyn PrimitiveAttrib)] > -> (AttribTree csyn PrimitiveAttrib) > -> TreeNSubst csyn > rule hs conc = > ruleIf hs (\_ -> True) (\_ -> nullSubst) 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) => > [(AttribTree hsyn PrimitiveAttrib)] > -> ([PrimitiveAttrib] -> Bool) > -> ([PrimitiveAttrib] -> Subst PrimitiveAttrib) > -> (AttribTree csyn PrimitiveAttrib) > -> TreeNSubst csyn > ruleIf hs side_cond side_defs (syn ::: tau) = > (case (resultsubl, substl) of > ([resultsub], [s]) -> > let ts = map_tops (app s) result_trees > ts_tops = map root ts > in if side_cond ts_tops > then let s' = (side_defs ts_tops) @@ (s @@ resultsub) > ts' = map_tops (app s') ts > in (Tree_Subst (syn ::: Node (app s' tau) ts') [s']) > else (Tree_Subst (syn ::: Node Aerr ts) []) > _ -> (Tree_Subst (syn ::: Node Aerr result_trees) [])) > where > substl = listUnify tops (map (\(_ ::: tau) -> tau) hs) > tops = map root result_trees > (result_trees, resultsubl) = check hs ([], [nullSubst]) > check [] (attrs, subl) = (attrs, subl) > check ((s ::: _):ss) (attrs, subl) = > (case (subl, annotate s) of > ([cur_subst], Tree_Subst (_ ::: nd) [resultsub]) -> > check ss (attrs ++ [nd], [cur_subst @@ resultsub]) > (_, Tree_Subst (_ ::: nd) []) -> > check ss (attrs ++ [nd], []) > _ -> check ss (attrs ++ [Node Aerr []], [])) The following helper function is used above > map_tops :: (a -> a) -> [(Tree a)] -> [(Tree a)] > map_tops f ts = map (\(Node t ls) -> (Node (f t) ls)) ts