packages feed

free-theorems 0.3 → 0.3.1

raw patch · 10 files changed

+192/−26 lines, 10 files

Files

free-theorems.cabal view
@@ -1,5 +1,5 @@ name:           free-theorems-version:        0.3+version:        0.3.1 license:        PublicDomain license-file:   LICENSE author:         Sascha Boehme@@ -18,6 +18,7 @@     may be derived in addition to classical equational results. category:       Language tested-with: 	GHC==6.8.2+cabal-version:  >= 1.2.3 build-type:	Simple build-depends:     base >= 1.0@@ -32,10 +33,10 @@     Language.Haskell.FreeTheorems.Parser.Haskell98     Language.Haskell.FreeTheorems.Parser.Hsx     Language.Haskell.FreeTheorems.Theorems-other-modules:     Language.Haskell.FreeTheorems.BasicSyntax     Language.Haskell.FreeTheorems.ValidSyntax     Language.Haskell.FreeTheorems.NameStores+other-modules:     Language.Haskell.FreeTheorems.Frontend     Language.Haskell.FreeTheorems.Frontend.Error     Language.Haskell.FreeTheorems.Frontend.TypeExpressions
src/Language/Haskell/FreeTheorems.hs view
@@ -73,6 +73,7 @@   , Intermediate   , interpret   , asTheorem+  , asCompleteTheorem   , relationVariables   , specialise   , specialiseInverse
src/Language/Haskell/FreeTheorems/BasicSyntax.hs view
@@ -204,8 +204,18 @@   | TypeFun TypeExpression TypeExpression       -- ^ The function type constructor @->@. +  | TypeFunLab TypeExpression TypeExpression+      -- ^ The function type constructor @->^o@ for the non-bottom-reflecting+      --   logical relation for functions in the languagesubset with seq+      --   for equational theorems.+   | TypeAbs TypeVariable [TypeClass] TypeExpression       -- ^ The type abstraction constructor @forall@.++  | TypeAbsLab TypeVariable [TypeClass] TypeExpression+      -- ^ The type abstraction constructor @forall^o@, allowing+      --   non-bottom-reflecting logical relations for types the type variable+      --   is instantiated with in the calculus with seq.    | TypeExp FixedTypeExpression       -- ^ A variable representing a fixed type expression.
src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs view
@@ -43,9 +43,10 @@ allTypeVariables = synthesize Set.empty Set.union (id `mkQ` update)   where     update t s = case t of-      TypeVar v     -> Set.insert v s-      TypeAbs v _ _ -> Set.insert v s-      otherwise     -> s+      TypeVar v        -> Set.insert v s+      TypeAbs v _ _    -> Set.insert v s+      TypeAbsLab v _ _ -> Set.insert v s+      otherwise        -> s   @@ -55,9 +56,10 @@ freeTypeVariables = synthesize Set.empty Set.union (id `mkQ` update)   where     update t s = case t of-      TypeVar v     -> Set.insert v s-      TypeAbs v _ _ -> Set.delete v s-      otherwise     -> s+      TypeVar v        -> Set.insert v s+      TypeAbs v _ _    -> Set.delete v s+      TypeAbsLab v _ _ -> Set.delete v s+      otherwise        -> s   @@ -76,8 +78,9 @@     -- Removes bound type variables from the mapping. Thus, these variables     -- won't be replaced in the second stage.     update t env = case t of-      TypeAbs v _ _ -> Map.delete v env-      otherwise     -> env+      TypeAbs v _ _    -> Map.delete v env+      TypeAbsLab v _ _ -> Map.delete v env+      otherwise        -> env          -- Replaces a type variable by a type expression, if the type variable is     -- contained in the environment.@@ -124,8 +127,9 @@     -- If we are at the type abstraction where 'old' is bound, then 'old' has     -- to be replaced in every subexpression by the new type variable.     change t f = case t of-      TypeAbs v _ _ -> if (v == old) then rep else f-      otherwise     -> f+      TypeAbs    v _ _ -> if (v == old) then rep else f+      TypeAbsLab v _ _ -> if (v == old) then rep else f+      otherwise         -> f      -- Applies the current replacement function to type variables.     -- In type abstractions, the static function 'rep' is used to replace@@ -133,8 +137,9 @@     -- Note that - independent of the usage of 'rep' - the replacement function     -- 'r' will be modified by 'change' when advancing to subexpressions.     replace r t = case t of-      TypeVar v       -> TypeVar (r v)-      TypeAbs v cs t' -> TypeAbs (rep v) cs t'+      TypeVar    v       -> TypeVar    (r v)+      TypeAbs    v cs t' -> TypeAbs    (rep v) cs t'+      TypeAbsLab v cs t' -> TypeAbsLab (rep v) cs t'       otherwise       -> t
src/Language/Haskell/FreeTheorems/Intermediate.hs view
@@ -1,6 +1,3 @@--- -- | Declares an intermediate data structure along with a function to transform --   type signatures into the intermediate structure. There are also other --   functions working on intermediate structures, namely to retrieve relation@@ -152,6 +149,12 @@     ri <- mkRelationInfo l t       -- create the relation info     liftM2 (RelFun ri) (interpretM l t1) (interpretM l t2) +    -- create a second relation for function types (used only for language+    -- subset with seq and the equational setting+  TypeFunLab t1 t2 -> do+    ri <- mkRelationInfo l t       -- create the relation info+    liftM2 (RelFunLab ri) (interpretM l t1) (interpretM l t2)+     -- create a relation for type abstractions   TypeAbs v cs t' -> do     ri <- mkRelationInfo l t                    -- create the relation info@@ -161,6 +164,16 @@     let res = relRes l ++ (if null cs then [] else [RespectsClasses cs])     return (RelAbs ri rv (t1,t2) res r) +    -- create a second relation for type abstractions (used only for language+    -- subset with seq and the equational setting+  TypeAbsLab v cs t' -> do+    ri <- mkRelationInfo l t                    -- create the relation info+    (rv, t1, t2) <- lift newRelationVariable    -- create a new variable+    let rvar = RelVar (RelationInfo l t1 t2) rv+    r  <- local (Map.insert v rvar) $ interpretM l t'  -- subrelations+    let res = (filter (/= BottomReflecting) (relRes l)) ++ (if null cs then [] else [RespectsClasses cs])+    return (RelAbs ri rv (t1,t2) res r)+   where     mkRelationInfo l t = do       env <- ask@@ -247,6 +260,7 @@     getRVar ok rel = case rel of       RelLift _ _ rs    -> concatMap (getRVar ok) rs       RelFun _ r1 r2    -> getRVar (not ok) r1 ++ getRVar ok r2+      RelFunLab _ r1 r2 -> getRVar (not ok) r1 ++ getRVar ok r2       RelAbs _ rv _ _ r -> (if ok then [rv] else []) ++ getRVar ok r       FunAbs _ _ _ _ r  -> getRVar ok r        otherwise         -> []@@ -294,7 +308,11 @@         let tv = either (Left . TermVar) (Right . TermVar) fv          in if rv == r then FunVar ri tv else rel       RelAbs ri (RVar r) ts res rel' ->-        let res' = either (const funResL) (const funResR) fv+        let res'' = either (const funResL) (const funResR) fv+            -- hack! should be somehow better implemented+	    -- if BottomReflecting is not present, we had+            -- TypeAbsLab quantification in (SubsetWithSeq Equational)+            res'  = if elem BottomReflecting res then res'' else filter (/= Total) res''          in if rv == r               then FunAbs ri fv ts (res' ++ (classConstraints res)) rel'               else rel@@ -337,6 +355,10 @@                                  else rel       RelFun ri r1 r2       -> RelFun ri (re (mk' (not ok) ri r1) r1)                                           (re (mk ok ri r2) r2)+      -- second logical relation for functions. Only used for the language+      -- subset with Seq in the equational setting+      RelFunLab ri r1 r2    -> RelFunLab ri (re (mk' (not ok) ri r1) r1) +                                            (re (mk ok ri r2) r2)       RelAbs ri rv ts res r -> RelAbs ri rv ts res (re ok r)       FunAbs ri fv ts res r -> FunAbs ri fv ts res (re ok r)       otherwise             -> rel
src/Language/Haskell/FreeTheorems/NameStores.hs view
@@ -3,7 +3,14 @@  -- | Provides functions to generate new variable names of different kinds. -module Language.Haskell.FreeTheorems.NameStores where+module Language.Haskell.FreeTheorems.NameStores+    ( typeNameStore+    , relationNameStore+    , typeExpressionNameStore+    , functionNameStore1+    , functionNameStore2+    , variableNameStore+    ) where
src/Language/Haskell/FreeTheorems/PrettyTheorems.hs view
@@ -41,7 +41,7 @@      | OmitLanguageSubsets         -- ^ Omit mentioning language subsets explicitly for certain relations.-  +   deriving Eq  @@ -345,6 +345,13 @@         fsep [ prettyRelation (useParens pc) False r1              , text "->" <> l              , prettyRelation (useParens pc) False r2 ]++-- second function relation only used in the equational setting with Seq+prettyRelation pc _ (RelFunLab ri r1 r2) = +   parensIf (withParens pc) $+      fsep [ prettyRelation (useParens pc) False r1+           , text "->^o" <> empty+           , prettyRelation (useParens pc) False r2 ]  prettyRelation pc _ (RelAbs ri v _ res r) =    let tcs = getTypeClasses res
src/Language/Haskell/FreeTheorems/PrettyTypes.hs view
@@ -194,6 +194,14 @@     funs (TypeFun t1 t2) = t1 : funs t2     funs t               = [t] +prettyTypeExpression p (TypeFunLab t1 t2) =+  parensIf (p > NoParens) $ +    fsep (zipWith (<+>) (empty : repeat (text "->")) +                        (map (prettyTypeExpression ParensFun) (t1 : funs t2)))+  where+    funs (TypeFunLab t1 t2) = t1 : funs t2+    funs t                  = [t]+ prettyTypeExpression p (TypeAbs v tcs t) =   let (vs, cx, t') = collectAbstractions v tcs t    in parensIf (p > NoParens) $@@ -201,6 +209,13 @@           [text "forall"] ++ (map prettyTypeVariable vs)           ++ [char '.', prettyContext cx, prettyTypeExpression NoParens t'] +prettyTypeExpression p (TypeAbsLab v tcs t) =+  let (vs, cx, t') = collectAbstractions v tcs t+   in parensIf (p > NoParens) $+        fsep $ +          [text "forall"] ++ (map prettyTypeVariable vs)+          ++ [char '.', prettyContext cx, prettyTypeExpression NoParens t']+ prettyTypeExpression p (TypeExp te) = prettyFixedTypeExpression te  @@ -217,11 +232,14 @@ collectAbstractions v tcs t =   let cx = zip tcs (repeat v)    in case t of-        TypeAbs v' tcs' t' -> +        TypeAbs v' tcs' t'    ->            let (vs, cx', t'') = collectAbstractions v' tcs' t'            in (v : vs, cx ++ cx', t'')+	TypeAbsLab v' tcs' t' -> +          let (vs, cx', t'') = collectAbstractions v' tcs' t'+           in (v : vs, cx ++ cx', t'')          -        otherwise          -> ([v], cx, t)+        otherwise             -> ([v], cx, t)
src/Language/Haskell/FreeTheorems/Theorems.hs view
@@ -143,6 +143,13 @@         --   requiring bottom-reflectiveness of its members.         --   In the inequational subset with seq, this relation is explicitly         --   requiring totality of its members.++  | RelFunLab RelationInfo Relation Relation+        -- ^ A relation corresponding to a function type constructor.+        --   The semantics of this relation differs with the language subset:+        --   Apart from the equational subset with seq, it is equal to RelFun.+        --   In the equational subset with Seq, this relation is _not_ +        --   explicitly requiring bottom-reflectiveness of its members.      | RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression)            [Restriction] Relation@@ -165,6 +172,7 @@   RelBasic ri       -> ri   RelLift ri _ _    -> ri   RelFun ri _ _     -> ri+  RelFunLab ri _ _  -> ri   RelAbs ri _ _ _ _ -> ri   FunAbs ri _ _ _ _ -> ri
src/Language/Haskell/FreeTheorems/Unfold.hs view
@@ -3,6 +3,7 @@  module Language.Haskell.FreeTheorems.Unfold (     asTheorem+  , asCompleteTheorem   , unfoldFormula   , unfoldLifts   , unfoldClasses@@ -28,7 +29,6 @@   - ------- Basic structures and functions ----------------------------------------  @@ -92,6 +92,11 @@                          let ([f], fs) = splitAt 1 (newFunctionNames2 state)                          put (state { newFunctionNames2 = fs })                          return (TVar f)++    TypeFunLab _ _ -> do state <- get+                         let ([f], fs) = splitAt 1 (newFunctionNames2 state)+                         put (state { newFunctionNames2 = fs })+                         return (TVar f)          TypeAbs _ _ t' -> newVariableFor t'     @@ -136,7 +141,16 @@    in runReader (evalStateT (unfoldFormula v v r) s) (True, True)  +-- | Unfolds an intermediate structure to a theorem with _all_ restrictions. +asCompleteTheorem :: Intermediate -> Theorem+asCompleteTheorem i = +  let v = TermVar . TVar . intermediateName $ i+      r = intermediateRelation i+      s = initialState i+   in runReader (evalStateT (unfoldFormula v v r) s) (True, False)++ -- | Unfolds the logical relation "R" in the expression "(x,y) in R" to a --   theorem. It works by recursively applying unfolding operations of --   relational actions.@@ -148,6 +162,7 @@   RelBasic ri          -> unfoldBasic x y ri   RelLift _ _ _        -> return . Predicate . IsMember x y $ rel   RelFun ri r1 r2      -> unfoldFun x y ri r1 r2+  RelFunLab ri r1 r2   -> unfoldFunLab x y ri r1 r2   RelAbs ri v ts res r -> unfoldAbsRel x y ri v ts res r   FunAbs ri v ts res r -> unfoldAbsFun x y ri v ts res r @@ -224,12 +239,39 @@         EquationalTheorem   -> unfoldFunOneVar x y ri (Left id) rel1 rel2         InequationalTheorem -> unfoldFunVars x y ri rel1 rel2     RelLift _ _ _       -> unfoldFunPairs x y ri rel1 rel2-    RelFun _ _ _        -> unfoldFunVars x y ri rel1 rel2 -    RelAbs _ _ _ _ _    -> unfoldFunVars x y ri rel1 rel2+    RelFun _ _ _        -> unfoldFunVars x y ri rel1 rel2+    RelFunLab _ _ _     -> unfoldFunVars x y ri rel1 rel2+    RelAbs _ _ _ r _    -> unfoldFunVars x y ri rel1 rel2     FunAbs _ _ _ _ _    -> unfoldFunVars x y ri rel1 rel2 +-- | Unfolding operation for relational actions of function type constructors. +unfoldFunLab :: +    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula+unfoldFunLab x y ri rel1 rel2 =+  case rel1 of+    RelVar _ _          -> unfoldFunLabPairs x y ri rel1 rel2+    FunVar _ t          -> +      let ta = either (\t -> Left (TermApp t)) (\t -> Right (TermApp t)) t+          one = unfoldFunLabOneVar x y ri ta rel1 rel2+          two = unfoldFunLabVars x y ri rel1 rel2+       in case theoremType (relationLanguageSubset ri) of+            EquationalTheorem   -> one+            InequationalTheorem -> do+              simple <- simplificationsAllowed+              if simple then one else two+    RelBasic _          -> +      case theoremType (relationLanguageSubset ri) of+        EquationalTheorem   -> unfoldFunLabOneVar x y ri (Left id) rel1 rel2+        InequationalTheorem -> unfoldFunLabVars x y ri rel1 rel2+    RelLift _ _ _       -> unfoldFunLabPairs x y ri rel1 rel2+    RelFun _ _ _        -> unfoldFunLabVars x y ri rel1 rel2+    RelFunLab _ _ _     -> unfoldFunLabVars x y ri rel1 rel2+    RelAbs _ _ _ r _    -> unfoldFunLabVars x y ri rel1 rel2+    FunAbs _ _ _ _ _    -> unfoldFunLabVars x y ri rel1 rel2 ++ unfoldFunOneVar ::      Term -> Term -> RelationInfo -> Either (Term -> Term) (Term -> Term)      -> Relation -> Relation -> Unfolded Formula@@ -246,9 +288,27 @@          Right t -> unfoldFormula (TermApp x (t tx')) (TermApp y tx') rel2    addRestriction x y (relationLanguageSubset ri) (ForallVariables x' t f)+--  return (ForallVariables x' t f) +unfoldFunLabOneVar :: +    Term -> Term -> RelationInfo -> Either (Term -> Term) (Term -> Term) +    -> Relation -> Relation -> Unfolded Formula+unfoldFunLabOneVar x y ri termapp rel1 rel2 = do+  let t = either (const (relationLeftType (relationInfo rel1))) +                 (const (relationRightType (relationInfo rel1)))+                 termapp+  +  x' <- newVariableFor t+  let tx' = TermVar x' +  f <- case termapp of+         Left t  -> unfoldFormula (TermApp x tx') (TermApp y (t tx')) rel2+         Right t -> unfoldFormula (TermApp x (t tx')) (TermApp y tx') rel2 +-- addRestriction x y (relationLanguageSubset ri) (ForallVariables x' t f)+  return (ForallVariables x' t f)++ unfoldFunPairs ::      Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula unfoldFunPairs x y ri rel1 rel2 = do@@ -258,7 +318,18 @@   f  <- unfoldFormula (TermApp x (TermVar x')) (TermApp y (TermVar y')) rel2      addRestriction x y (relationLanguageSubset ri) (ForallPairs (x', y') rel1 f)+--  return (ForallPairs (x', y') rel1 f)++unfoldFunLabPairs :: +    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula+unfoldFunLabPairs x y ri rel1 rel2 = do+  x' <- newVariableFor . relationLeftType  . relationInfo $ rel1+  y' <- newVariableFor . relationRightType . relationInfo $ rel1++  f  <- unfoldFormula (TermApp x (TermVar x')) (TermApp y (TermVar y')) rel2   +-- addRestriction x y (relationLanguageSubset ri) (ForallPairs (x', y') rel1 f)+  return (ForallPairs (x', y') rel1 f)   unfoldFunVars :: @@ -275,9 +346,25 @@    let f = ForallVariables x' t1 (ForallVariables y' t2 (Implication l r))   addRestriction x y (relationLanguageSubset ri) f+--  return f  +unfoldFunLabVars :: +    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula+unfoldFunLabVars x y ri rel1 rel2 = do+  let t1 = relationLeftType (relationInfo rel1)+  let t2 = relationRightType (relationInfo rel1) +  x' <- newVariableFor t1+  y' <- newVariableFor t2++  l  <- toggleSimplifications (unfoldFormula (TermVar x') (TermVar y') rel1)+  r  <- unfoldFormula (TermApp x (TermVar x')) (TermApp y (TermVar y')) rel2++  let f = ForallVariables x' t1 (ForallVariables y' t2 (Implication l r))+  return f++ addRestriction :: Term -> Term -> LanguageSubset -> Formula -> Unfolded Formula addRestriction x y l f = do   simple <- simplificationsAllowed@@ -320,7 +407,7 @@                                          in (UnfoldedLift r u, ms)              eqLift (UnfoldedLift r1 _) (UnfoldedLift r2 _) = r1 == r2-   in nubBy eqLift $ recUnfold [] rs+  in nubBy eqLift $ recUnfold [] rs