From 509bc021200b0de7713a0fdb27c730eaff3be206 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 26 Nov 2021 18:53:17 -0300 Subject: [PATCH] initial commit --- .gitignore | 1 + LICENSE | 30 ++++++++++++++++++ README.md | 1 + Setup.hs | 2 ++ agda-fold-equations.cabal | 11 +++++++ hie.yaml | 2 ++ src/Main.hs | 45 ++++++++++++++++++++++++++ stack.yaml | 67 +++++++++++++++++++++++++++++++++++++++ stack.yaml.lock | 13 ++++++++ 9 files changed, 172 insertions(+) create mode 100644 .gitignore create mode 100644 LICENSE create mode 100644 README.md create mode 100644 Setup.hs create mode 100644 agda-fold-equations.cabal create mode 100644 hie.yaml create mode 100644 src/Main.hs create mode 100644 stack.yaml create mode 100644 stack.yaml.lock diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..8ee1bf9 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.stack-work diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..ca46626 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Abigail Magalhães (c) 2021 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Abigail Magalhães nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..b38a931 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# agda-fold-equations diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/agda-fold-equations.cabal b/agda-fold-equations.cabal new file mode 100644 index 0000000..b97c309 --- /dev/null +++ b/agda-fold-equations.cabal @@ -0,0 +1,11 @@ +cabal-version: 2.2 +name: agda-fold-equations +version: 0.1.0.0 + +executable agda-fold-equations + hs-source-dirs: src + main-is: Main.hs + default-language: Haskell2010 + build-depends: base >= 4.7 && < 5 + , tagsoup + , text diff --git a/hie.yaml b/hie.yaml new file mode 100644 index 0000000..142e69f --- /dev/null +++ b/hie.yaml @@ -0,0 +1,2 @@ +cradle: + stack: \ No newline at end of file diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..4bda2d5 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE OverloadedStrings #-} +module Main where + +import qualified Data.Text.Lazy.IO as Text +import qualified Data.Text.Lazy as Text +import Data.Text.Lazy (Text) + +import Text.HTML.TagSoup +import System.Environment +import Control.Exception +import Data.Maybe + +main :: IO () +main = do + [file] <- getArgs + tags <- parseTags <$> Text.readFile file + evaluate (length tags) + Text.writeFile file (renderTags (hideSteps False tags)) + +hideSteps :: Bool -> [Tag Text] -> [Tag Text] +hideSteps has_eqn (to@(TagOpen "a" attrs):tt@(TagText t):tc@(TagClose "a"):rest) + | Text.length t >= 1, Text.last t == '⟨', Just href <- lookup "href" attrs = + [ TagOpen "span" [("class", "reasoning-step")] + , TagOpen "span" [("class", "as-written " <> fromMaybe "" (lookup "class" attrs))] + , to, tt, tc ] ++ go href rest + where + alternate = Text.init t + go href (to@(TagOpen "a" attrs):tt@(TagText t):tc@(TagClose "a"):cs) + | Text.length t >= 1 + , Text.head t == '⟩' + , Just href' <- lookup "href" attrs + , href' == href + = [ to, tt, tc, TagClose "span" + , TagOpen "span" [("class", "alternate " <> fromMaybe "" (lookup "class" attrs))] + , TagText alternate + , TagClose "span" + , TagClose "span" + ] ++ hideSteps True cs + go href (c:cs) = c:go href cs + go _ [] = [] +hideSteps False (TagClose "html":cs) = + [TagOpen "style" [], TagText ".equations { display: none !important; }", TagClose "style", TagClose "html"] + ++ hideSteps True cs +hideSteps has_eqn (c:cs) = c:hideSteps has_eqn cs +hideSteps _ [] = [] \ No newline at end of file diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..21ac023 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,67 @@ +# This file was automatically generated by 'stack init' +# +# Some commonly used options have been documented as comments in this file. +# For advanced use and comprehensive documentation of the format, please see: +# https://docs.haskellstack.org/en/stable/yaml_configuration/ + +# Resolver to choose a 'specific' stackage snapshot or a compiler version. +# A snapshot resolver dictates the compiler version and the set of packages +# to be used for project dependencies. For example: +# +# resolver: lts-3.5 +# resolver: nightly-2015-09-21 +# resolver: ghc-7.10.2 +# +# The location of a snapshot can be provided as a file or url. Stack assumes +# a snapshot provided as a file might change, whereas a url resource does not. +# +# resolver: ./custom-snapshot.yaml +# resolver: https://example.com/snapshots/2018-01-01.yaml +resolver: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/13.yaml + +# User packages to be built. +# Various formats can be used as shown in the example below. +# +# packages: +# - some-directory +# - https://example.com/foo/bar/baz-0.0.2.tar.gz +# subdirs: +# - auto-update +# - wai +packages: +- . +# Dependency packages to be pulled from upstream that are not in the resolver. +# These entries can reference officially published versions as well as +# forks / in-progress versions pinned to a git hash. For example: +# +# extra-deps: +# - acme-missiles-0.3 +# - git: https://github.com/commercialhaskell/stack.git +# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a +# +# extra-deps: [] + +# Override default flag values for local packages and extra-deps +# flags: {} + +# Extra package databases containing global packages +# extra-package-dbs: [] + +# Control whether we use the GHC we find on the path +# system-ghc: true +# +# Require a specific version of stack, using version ranges +# require-stack-version: -any # Default +# require-stack-version: ">=2.7" +# +# Override the architecture used by stack, especially useful on Windows +# arch: i386 +# arch: x86_64 +# +# Extra directories used by stack for building +# extra-include-dirs: [/path/to/dir] +# extra-lib-dirs: [/path/to/dir] +# +# Allow a newer minor version of GHC than the snapshot specifies +# compiler-check: newer-minor diff --git a/stack.yaml.lock b/stack.yaml.lock new file mode 100644 index 0000000..659abd6 --- /dev/null +++ b/stack.yaml.lock @@ -0,0 +1,13 @@ +# This file was autogenerated by Stack. +# You should not edit this file by hand. +# For more information, please see the documentation at: +# https://docs.haskellstack.org/en/stable/lock_files + +packages: [] +snapshots: +- completed: + size: 586268 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/13.yaml + sha256: d9e658a22cfe8d87a64fdf219885f942fef5fe2bcb156a9800174911c5da2443 + original: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/13.yaml