ftshell 0.2 → 0.3

raw patch · 4 files changed

+45/−8 lines, 4 filesdep ~free-theoremsnew-uploader

Dependency ranges changed: free-theorems

Files

• ftshell.cabal +12/−4
• src/Commands.hs +24/−3
• src/Shell.hs +4/−1
• src/ShellState.hs +5/−0

@@ -1,5 +1,5 @@ name:           ftshell-version:        0.2+version:        0.3 license:        PublicDomain license-file:   LICENSE author:         Sascha Boehme@@ -11,19 +11,27 @@     that library to generate free theorems from Haskell type     expressions. category:       Language, Source-tools-tested-with: 	GHC==6.8.2-build-type:	Simple+tested-with:    GHC==6.8.2+build-type:     Simple build-depends:     base >= 1.0   , mtl >= 1.0   , Shellac >= 0.9   , Shellac-readline >= 0.9-  , free-theorems >= 0.2+  , free-theorems >= 0.3   , pretty >= 1.0.0.0   , containers >= 0.1.0.1 data-files:     declarations.hs+    README executable:     ftshell main-is:        main.hs+other-modules: +        Shell+        Evaluate+        Settings+        Commands+        ShellState+        HelpCommands hs-source-dirs: src extensions: MultiParamTypeClasses

@@ -276,7 +276,13 @@ cmdShowTheorem :: Sh ShellState () cmdShowTheorem = withCurrentContext $ \sig intermediate -> do   opts <- fromShellSt getCurrentTheoremOptions-  let pt = prettyTheorem opts (asTheorem intermediate)+  simp <- fromShellSt getSimplifyOutput+  l <- fromShellSt getCurrentLanguageSubset+  let pt = prettyTheorem opts $+           (if simp && l `elem` [BasicSubset, SubsetWithFix EquationalTheorem]+           then simplify+           else id) $+           asTheorem intermediate   shellPutStrLn "The free theorem for the type signature\n"   (shellPutStrLn . doRender 2 . prettySignature . rawSignature) sig   l <- fromShellSt getCurrentLanguageSubset@@ -291,12 +297,17 @@ cmdShowLiftedRelations = withCurrentContext $ \_ intermediate -> do   vds  <- fromShellSt (concat . Map.elems . getAllDeclarations)   opts <- fromShellSt getCurrentTheoremOptions+  simp <- fromShellSt getSimplifyOutput+  l <- fromShellSt getCurrentLanguageSubset+  let simpL = if simp && l `elem` [BasicSubset, SubsetWithFix EquationalTheorem]+	      then simplifyUnfoldedLift+              else id   let lifts = unfoldLifts vds intermediate   if null lifts     then shellPutStrLn "There are no lifted relations in the current theorem."     else do shellPutStrLn ""             mapM_ (\s -> shellPutStrLn (s ++ "\n"))-                  (map (doRender 2 . prettyUnfoldedLift opts) lifts)+                  (map (doRender 2 . prettyUnfoldedLift opts . simpL) lifts)   @@ -408,6 +419,9 @@   opts <- fromShellSt getCurrentTheoremOptions   shellPutStrLn "The current options for displaying theorems are:"   mapM_ (showOpt opts) (Map.keys allTheoremOptions)+  simp <- fromShellSt getSimplifyOutput+  if simp then shellPutStrLn "The output will be simplified, if possible."+          else shellPutStrLn "The output will not be simplified."   where     showOpt opts o =       if fromJust (Map.lookup o allTheoremOptions) `elem` opts@@ -430,7 +444,14 @@   let add opt os = if opt `notElem` os then opt : os else os    in updateTheoremOptions add -+-- Toggles the simplify output flag+cmdToggleSimplify :: Sh ShellState ()+cmdToggleSimplify = do+  modifyShellSt $ \s -> s { getSimplifyOutput = not (getSimplifyOutput s) }+  simp <- fromShellSt getSimplifyOutput+  if simp then shellPutStrLn "The output will be simplified, if possible."+          else shellPutStrLn "The output will not be simplified."+    -- Modifies the current theorem options with the help of a modification -- function.

@@ -191,7 +191,10 @@         "Turn on a theorem option"    , cmd "omit" cmdTheoremOptionOmit-        "Turn off a theorem option\n"+        "Turn off a theorem option"++  , cmd "toggle-simplify" cmdToggleSimplify+	"Toggle whether the theorems are simplified\n"      , exitCommand "quit"   ]

@@ -76,6 +76,9 @@   , getCurrentTheoremOptions :: [PrettyTheoremOption]         -- The current options which modify how theorems are pretty-printed. +  , getSimplifyOutput :: Bool+	-- Whether the Theorems.Simplify module should be used (if allowed by the+	-- language subtype)   }  @@ -95,6 +98,7 @@   , getCurrentTheoremOptions = [ OmitTypeInstantiations                                -- , OmitLanguageSubsets                                ]+  , getSimplifyOutput        = True   }  @@ -112,6 +116,7 @@   , getCurrentContext        = Nothing   , getSpecialisationHistory = []   , getCurrentTheoremOptions = getCurrentTheoremOptions state+  , getSimplifyOutput        = True   }