{"header":{"message":"some attempts at abstract syntax","description":null,"timestamp":"2024-08-23T13:42:15.353688962Z","authors":[{}]},"hash":"JDF4JUMSZJ6JD4Y27R2G5JC6LFT6SNCP52UDVCGKQ4QAGMGUDMJAC","authors":[{"login":"fogti","key":"ZFnYYAXSF9fgPaXKyrt5a2oor75nLVcpU8T8fEnRqwm"}],"deps":{"hashes":[["JDF4JUMSZJ6JD4Y27R2G5JC6LFT6SNCP52UDVCGKQ4QAGMGUDMJAC","some attempts at abstract syntax"],["AA",null],["EFHQIYTCATMP3PQNVAUSK75EDA5E3QCOB737TTJWURPFCUO7VSXQC","add Literal from yanais"],["6XMVEBZAMRKHRYLFMJ6ZNSBM5ZXPTPK4YS4QUNGGPPUS4HLPO6GAC","add simple stuff (e.g. haskell basics)"],["GMGXNJEPA2NENYJKQFAFYWHDEJOK62T4PK6EY7NE6GIX4Y2JPHTAC","add back more stuff from yanais"]],"deps":["EFHQIYTCATMP3PQNVAUSK75EDA5E3QCOB737TTJWURPFCUO7VSXQC"],"known":[]},"hunks":[{"FileAdd":{"meta":{"basename":"Abstract.hs","metadata":0},"context":[{"change":2,"pos":18}],"contents":[{"Add":"{-# LANGUAGE DeriveGeneric #-}"},{"Add":""},{"Add":"module GardGround.Syntax.Abstract ("},{"Add":" NeutralRoot,"},{"Add":" Neutral,"},{"Add":" ValueError,"},{"Add":" Value,"},{"Add":" vapp,"},{"Add":" quote,"},{"Add":") where"},{"Add":""},{"Add":"import Control.Monad (foldM)"},{"Add":"import qualified Deque.Strict as Deq"},{"Add":"import Generic.Data (Generic)"},{"Add":"import Numeric.Natural (Natural)"},{"Add":""},{"Add":"import GardGround.Syntax.Literal (Literal)"},{"Add":"import GardGround.Utils.SteParser.Lex (Ident)"},{"Add":""},{"Add":"data NeutralRoot = NrLiteral Literal"},{"Add":" | Global Ident"},{"Add":" | Local Natural"},{"Add":" | Quote Natural"},{"Add":" -- note that Local and Quote are numbered in opposite directions"},{"Add":" deriving (Eq, Generic)"},{"Add":""},{"Add":"instance Show NeutralRoot where"},{"Add":" show (NrLiteral lit) = show lit"},{"Add":" show (Global i) = \"Global:\" <> show i"},{"Add":" show (Local i) = \"Local:\" <> show i"},{"Add":" show (Quote i) = \"Quote:\" <> show i"},{"Add":""},{"Add":"type Deque a = Deq.Deque a"},{"Add":""},{"Add":"-- | neutral values (a root, to which might be some values applied)"},{"Add":"-- values at the front are applied first, further applications get appended to back"},{"Add":"data Neutral = Neutral NeutralRoot (Deque Value)"},{"Add":""},{"Add":"data ValueError ="},{"Add":" VEInvalidApply Value Value"},{"Add":" | VEOutOfRangeQuote Natural"},{"Add":""},{"Add":"data Value = VLam (Value -> Either ValueError Value)"},{"Add":" | VPi Value (Value -> Either ValueError Value)"},{"Add":" | VNeutral Neutral"},{"Add":" | VRefOf Value -- ^ value being pointed to"},{"Add":" | VRefOfTy Natural Value -- ^ region and type being pointed to"},{"Add":""},{"Add":"-- base design based upon LambdaPi (https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf)"},{"Add":"-- and with advanced techniques from smalltt (https://github.com/AndrasKovacs/smalltt)"},{"Add":""},{"Add":"type EvalResult = Either ValueError Value"},{"Add":""},{"Add":"vapp :: Value -> Value -> EvalResult"},{"Add":"vapp (VLam f) = f"},{"Add":"vapp (VPi _ f) = f -- ^ this is mostly for convenience"},{"Add":"vapp (VRefOf r) = vapp r"},{"Add":"vapp (VNeutral (Neutral (NrLiteral lit) xs)) = Left . VEInvalidApply (VNeutral $ Neutral (NrLiteral lit) xs)"},{"Add":"vapp (VNeutral (Neutral nam xs)) = \\v -> Right . VNeutral . Neutral nam $ Deq.snoc v xs"},{"Add":"vapp l = Left . VEInvalidApply l"},{"Add":""},{"Add":"vfree :: NeutralRoot -> Value"},{"Add":"vfree r = VNeutral $ Neutral r mempty"},{"Add":""},{"Add":"data Expr ="},{"Add":" ENeutralRoot NeutralRoot"},{"Add":" | EApply Expr Expr"},{"Add":" | ELam Expr"},{"Add":" | EPi Expr Expr"},{"Add":" | ERefOf Expr"},{"Add":" | ERefOfTy Natural Expr"},{"Add":""},{"Add":"type QuoteResult = Either ValueError Expr"},{"Add":""},{"Add":"neutralQuote :: Natural -> Neutral -> QuoteResult"},{"Add":"neutralQuote i (Neutral nam xs) ="},{"Add":" let "},{"Add":" boundfree = case nam of"},{"Add":" Quote j ->"},{"Add":" let jp1 = j + 1 in"},{"Add":" if i < jp1"},{"Add":" then Left . VEOutOfRangeQuote $ jp1 - i"},{"Add":" else Right . Local $ i - jp1"},{"Add":" _ -> Right nam"},{"Add":" in"},{"Add":" boundfree >>= \\bf -> foldM (\\a b -> EApply a <$> quote i b) (ENeutralRoot bf) xs"},{"Add":""},{"Add":"-- quote0 = quote 0"},{"Add":""},{"Add":"quote :: Natural -> Value -> QuoteResult"},{"Add":"quote i (VLam f) = ELam <$> ((f . vfree $ Quote i) >>= quote (i + 1))"},{"Add":"quote i (VNeutral neut) = neutralQuote i neut"},{"Add":"quote i (VPi arg f) = do"},{"Add":" arge <- quote i arg"},{"Add":" fe <- (f . vfree $ Quote i) >>= quote (i + 1)"},{"Add":" pure (EPi arge fe)"},{"Add":""},{"Add":"quote i (VRefOf pt) = ERefOf <$> quote i pt"},{"Add":"quote i (VRefOfTy j pt) = ERefOfTy j <$> quote i pt"}]}},{"Edit":{"inode":{"change":4,"pos":4616},"path":"core/gardground-core.cabal","line":24,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":10877}],"down_context":[{"change":4,"pos":5078}],"flag":"BLOCK","start":2935,"end":2970,"inode":{"change":4,"pos":4616}}},"contents":[{"Add":" GardGround.Syntax.Abstract"}]}},{"Edit":{"inode":{"change":4,"pos":4616},"path":"core/gardground-core.cabal","line":41,"atom":{"NewVertex":{"up_context":[{"change":4,"pos":5290}],"down_context":[{"change":4,"pos":5290}],"flag":"BLOCK","start":2971,"end":3004,"inode":{"change":4,"pos":4616}}},"contents":[{"Add":" , deque ^>= 0.4.0.0"}]}}],"owner":"fogti","repo":"gardground","token":"iUvTqP9G8O3qXufqsc3NmJ08cVdZiQaP2bqR7JwiguM=","login":null}

…

Dependencies

Change contents