morte 1.0.0 → 1.0.1
raw patch · 4 files changed
+129/−141 lines, 4 filesdep ~text
Dependency ranges changed: text
Files
- dist/build/Morte/Lexer.hs +43/−64
- dist/build/Morte/Parser.hs +82/−60
- morte.cabal +4/−4
- src/Morte/Tutorial.hs +0/−13
dist/build/Morte/Lexer.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE CPP,MagicHash,BangPatterns #-}+{-# LANGUAGE CPP,MagicHash #-} {-# LINE 1 "src/Morte/Lexer.x" #-} {-# LANGUAGE OverloadedStrings #-}@@ -53,7 +53,7 @@ alex_deflt :: AlexAddr alex_deflt = AlexA# "\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x0a\x00\x0a\x00\xff\xff\xff\xff\xff\xff\x12\x00\x12\x00\xff\xff\xff\xff\xff\xff\xff\xff\x15\x00\x15\x00\x15\x00\xff\xff\xff\xff\x15\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"# -alex_accept = listArray (0::Int,43) [[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[(AlexAccSkip)],[(AlexAcc (alex_action_1))],[(AlexAccSkip)],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_4))],[(AlexAcc (alex_action_5))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_7))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_9))],[(AlexAcc (alex_action_10))],[(AlexAcc (alex_action_10))],[(AlexAcc (alex_action_11))],[(AlexAcc (alex_action_11))],[(AlexAcc (alex_action_12))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))]]+alex_accept = listArray (0::Int,43) [AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccSkip,AlexAcc (alex_action_1),AlexAccSkip,AlexAcc (alex_action_3),AlexAcc (alex_action_4),AlexAcc (alex_action_5),AlexAcc (alex_action_6),AlexAcc (alex_action_7),AlexAcc (alex_action_8),AlexAcc (alex_action_8),AlexAcc (alex_action_9),AlexAcc (alex_action_10),AlexAcc (alex_action_10),AlexAcc (alex_action_11),AlexAcc (alex_action_11),AlexAcc (alex_action_12),AlexAcc (alex_action_13),AlexAcc (alex_action_13),AlexAcc (alex_action_13),AlexAcc (alex_action_13),AlexAcc (alex_action_13),AlexAcc (alex_action_13),AlexAcc (alex_action_13),AlexAcc (alex_action_13),AlexAcc (alex_action_13)] {-# LINE 55 "src/Morte/Lexer.x" #-} toInt :: Text -> Int@@ -169,10 +169,6 @@ alex_action_12 = \text -> yield (Number (toInt text)) alex_action_13 = \text -> yield (Label text) {-# LINE 1 "templates/GenericTemplate.hs" #-}-{-# LINE 1 "templates/GenericTemplate.hs" #-}-{-# LINE 1 "<built-in>" #-}-{-# LINE 1 "<command-line>" #-}-{-# LINE 1 "templates/GenericTemplate.hs" #-} -- ----------------------------------------------------------------------------- -- ALEX TEMPLATE --@@ -182,13 +178,25 @@ -- ----------------------------------------------------------------------------- -- INTERNALS and main scanner engine -{-# LINE 37 "templates/GenericTemplate.hs" #-} -{-# LINE 47 "templates/GenericTemplate.hs" #-} -data AlexAddr = AlexA# Addr# +++-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex.+#if __GLASGOW_HASKELL__ > 706+#define GTE(n,m) (tagToEnum# (n >=# m))+#define EQ(n,m) (tagToEnum# (n ==# m))+#else+#define GTE(n,m) (n >=# m)+#define EQ(n,m) (n ==# m)+#endif++++data AlexAddr = AlexA# Addr#+-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex. #if __GLASGOW_HASKELL__ < 503 uncheckedShiftL# = shiftL# #endif@@ -198,10 +206,10 @@ #ifdef WORDS_BIGENDIAN narrow16Int# i where- !i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)- !high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))- !low = int2Word# (ord# (indexCharOffAddr# arr off'))- !off' = off *# 2#+ i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)+ high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ low = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 2# #else indexInt16OffAddr# arr off #endif@@ -215,14 +223,14 @@ #ifdef WORDS_BIGENDIAN narrow32Int# i where- !i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`+ i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#` (b2 `uncheckedShiftL#` 16#) `or#` (b1 `uncheckedShiftL#` 8#) `or#` b0)- !b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))- !b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))- !b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))- !b0 = int2Word# (ord# (indexCharOffAddr# arr off'))- !off' = off *# 4#+ b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))+ b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))+ b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ b0 = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 4# #else indexInt32OffAddr# arr off #endif@@ -231,6 +239,7 @@ + #if __GLASGOW_HASKELL__ < 503 quickIndex arr i = arr ! i #else@@ -297,36 +306,30 @@ - let- (!(base)) = alexIndexInt32OffAddr alex_base s- (!((I# (ord_c)))) = fromIntegral c- (!(offset)) = (base +# ord_c)- (!(check)) = alexIndexInt16OffAddr alex_check offset+ case fromIntegral c of { (I# (ord_c)) ->+ let+ base = alexIndexInt32OffAddr alex_base s+ offset = (base +# ord_c)+ check = alexIndexInt16OffAddr alex_check offset - (!(new_s)) = if (offset >=# 0#) && (check ==# ord_c)+ new_s = if GTE(offset,0#) && EQ(check,ord_c) then alexIndexInt16OffAddr alex_table offset else alexIndexInt16OffAddr alex_deflt s in- case new_s of + case new_s of -1# -> (new_acc, input) -- on an error, we want to keep the input *before* the -- character that failed, not after. _ -> alex_scan_tkn user orig_input (if c < 0x80 || c >= 0xC0 then (len +# 1#) else len) -- note that the length is increased ONLY if this is the 1st byte in a char encoding) new_input new_s new_acc-+ } where- check_accs [] = last_acc- check_accs (AlexAcc a : _) = AlexLastAcc a input (I# (len))- check_accs (AlexAccSkip : _) = AlexLastSkip input (I# (len))- check_accs (AlexAccPred a predx : rest)- | predx user orig_input (I# (len)) input- = AlexLastAcc a input (I# (len))- check_accs (AlexAccSkipPred predx : rest)- | predx user orig_input (I# (len)) input- = AlexLastSkip input (I# (len))- check_accs (_ : rest) = check_accs rest+ check_accs (AlexAccNone) = last_acc+ check_accs (AlexAcc a ) = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkip) = AlexLastSkip input (I# (len)) + data AlexLastAcc a = AlexNone | AlexLastAcc a !AlexInput !Int@@ -338,35 +341,11 @@ fmap f (AlexLastSkip x y) = AlexLastSkip x y data AlexAcc a user- = AlexAcc a+ = AlexAccNone+ | AlexAcc a | AlexAccSkip- | AlexAccPred a (AlexAccPred user)- | AlexAccSkipPred (AlexAccPred user) -type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool --- -------------------------------------------------------------------------------- Predicates on a rule--alexAndPred p1 p2 user in1 len in2- = p1 user in1 len in2 && p2 user in1 len in2----alexPrevCharIsPred :: Char -> AlexAccPred _ -alexPrevCharIs c _ input _ _ = c == alexInputPrevChar input--alexPrevCharMatches f _ input _ _ = f (alexInputPrevChar input)----alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _ -alexPrevCharIsOneOf arr _ input _ _ = arr ! alexInputPrevChar input----alexRightContext :: Int -> AlexAccPred _-alexRightContext (I# (sc)) user _ _ input = - case alex_scan_tkn user input 0# input sc AlexNone of- (AlexNone, _) -> False- _ -> True- -- TODO: there's no need to find the longest- -- match when checking the right context, just- -- the first match will do.- -- used by wrappers iUnbox (I# (i)) = i+
dist/build/Morte/Parser.hs view
@@ -30,8 +30,9 @@ import Pipes (Producer, hoist, lift, next) import qualified Data.Array as Happy_Data_Array import qualified GHC.Exts as Happy_GHC_Exts+import Control.Applicative(Applicative(..)) --- parser produced by Happy Version 1.18.9+-- parser produced by Happy Version 1.19.4 newtype HappyAbsSyn = HappyAbsSyn HappyAny #if __GLASGOW_HASKELL__ >= 607@@ -327,27 +328,46 @@ <> "\n" <> "Error: Parsing failed\n" ) {-# LINE 1 "templates/GenericTemplate.hs" #-}-{-# LINE 1 "templates/GenericTemplate.hs" #-}-{-# LINE 1 "<built-in>" #-}-{-# LINE 1 "<command-line>" #-}-{-# LINE 1 "templates/GenericTemplate.hs" #-} -- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp -{-# LINE 30 "templates/GenericTemplate.hs" #-} +++++-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex.+#if __GLASGOW_HASKELL__ > 706+#define LT(n,m) ((Happy_GHC_Exts.tagToEnum# (n Happy_GHC_Exts.<# m)) :: Bool)+#define GTE(n,m) ((Happy_GHC_Exts.tagToEnum# (n Happy_GHC_Exts.>=# m)) :: Bool)+#define EQ(n,m) ((Happy_GHC_Exts.tagToEnum# (n Happy_GHC_Exts.==# m)) :: Bool)+#else+#define LT(n,m) (n Happy_GHC_Exts.<# m)+#define GTE(n,m) (n Happy_GHC_Exts.>=# m)+#define EQ(n,m) (n Happy_GHC_Exts.==# m)+#endif+++ data Happy_IntList = HappyCons Happy_GHC_Exts.Int# Happy_IntList -{-# LINE 51 "templates/GenericTemplate.hs" #-} -{-# LINE 61 "templates/GenericTemplate.hs" #-} -{-# LINE 70 "templates/GenericTemplate.hs" #-} ++++++++++ infixr 9 `HappyStk` data HappyStk a = HappyStk a (HappyStk a) @@ -363,9 +383,9 @@ -- parse (a %partial parser). We must ignore the saved token on the top of -- the stack in this case. happyAccept 0# tk st sts (_ `HappyStk` ans `HappyStk` _) =- happyReturn1 ans+ happyReturn1 ans happyAccept j tk st sts (HappyStk ans _) = - (happyTcHack j (happyTcHack st)) (happyReturn1 ans)+ (happyTcHack j (happyTcHack st)) (happyReturn1 ans) ----------------------------------------------------------------------------- -- Arrays only: do the next action@@ -373,37 +393,35 @@ happyDoAction i tk st- = {- nothing -}--- case action of- 0# -> {- nothing -}- happyFail i tk st- -1# -> {- nothing -}- happyAccept i tk st- n | (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#)) -> {- nothing -}-- (happyReduceArr Happy_Data_Array.! rule) i tk st- where rule = (Happy_GHC_Exts.I# ((Happy_GHC_Exts.negateInt# ((n Happy_GHC_Exts.+# (1# :: Happy_GHC_Exts.Int#))))))- n -> {- nothing -}+ = {- nothing -}+ + case action of+ 0# -> {- nothing -}+ happyFail i tk st+ -1# -> {- nothing -}+ happyAccept i tk st+ n | LT(n,(0# :: Happy_GHC_Exts.Int#)) -> {- nothing -}+ + (happyReduceArr Happy_Data_Array.! rule) i tk st+ where rule = (Happy_GHC_Exts.I# ((Happy_GHC_Exts.negateInt# ((n Happy_GHC_Exts.+# (1# :: Happy_GHC_Exts.Int#))))))+ n -> {- nothing -}+ - happyShift new_state i tk st- where (new_state) = (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#))- where (off) = indexShortOffAddr happyActOffsets st- (off_i) = (off Happy_GHC_Exts.+# i)- check = if (off_i Happy_GHC_Exts.>=# (0# :: Happy_GHC_Exts.Int#))- then (indexShortOffAddr happyCheck off_i Happy_GHC_Exts.==# i)- else False- (action)+ happyShift new_state i tk st+ where new_state = (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#))+ where off = indexShortOffAddr happyActOffsets st+ off_i = (off Happy_GHC_Exts.+# i)+ check = if GTE(off_i,(0# :: Happy_GHC_Exts.Int#))+ then EQ(indexShortOffAddr happyCheck off_i, i)+ else False+ action | check = indexShortOffAddr happyTable off_i | otherwise = indexShortOffAddr happyDefActions st -{-# LINE 130 "templates/GenericTemplate.hs" #-} - indexShortOffAddr (HappyA# arr) off =- Happy_GHC_Exts.narrow16Int# i+ Happy_GHC_Exts.narrow16Int# i where i = Happy_GHC_Exts.word2Int# (Happy_GHC_Exts.or# (Happy_GHC_Exts.uncheckedShiftL# high 8#) low) high = Happy_GHC_Exts.int2Word# (Happy_GHC_Exts.ord# (Happy_GHC_Exts.indexCharOffAddr# arr (off' Happy_GHC_Exts.+# 1#)))@@ -422,13 +440,13 @@ ----------------------------------------------------------------------------- -- HappyState data type (not arrays) -{-# LINE 163 "templates/GenericTemplate.hs" #-} + ----------------------------------------------------------------------------- -- Shifting a token happyShift new_state 0# tk st sts stk@(x `HappyStk` _) =- let (i) = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in+ let i = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in -- trace "shifting the error token" $ happyDoAction i tk new_state (HappyCons (st) (sts)) (stk) @@ -464,30 +482,33 @@ = happyFail 0# tk st sts stk happyReduce k nt fn j tk st sts stk = case happyDrop (k Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) sts of- sts1@((HappyCons (st1@(action)) (_))) ->- let r = fn stk in -- it doesn't hurt to always seq here...- happyDoSeq r (happyGoto nt j tk st1 sts1 r)+ sts1@((HappyCons (st1@(action)) (_))) ->+ let r = fn stk in -- it doesn't hurt to always seq here...+ happyDoSeq r (happyGoto nt j tk st1 sts1 r) happyMonadReduce k nt fn 0# tk st sts stk = happyFail 0# tk st sts stk happyMonadReduce k nt fn j tk st sts stk =- happyThen1 (fn stk tk) (\r -> happyGoto nt j tk st1 sts1 (r `HappyStk` drop_stk))- where (sts1@((HappyCons (st1@(action)) (_)))) = happyDrop k (HappyCons (st) (sts))- drop_stk = happyDropStk k stk+ case happyDrop k (HappyCons (st) (sts)) of+ sts1@((HappyCons (st1@(action)) (_))) ->+ let drop_stk = happyDropStk k stk in+ happyThen1 (fn stk tk) (\r -> happyGoto nt j tk st1 sts1 (r `HappyStk` drop_stk)) happyMonad2Reduce k nt fn 0# tk st sts stk = happyFail 0# tk st sts stk happyMonad2Reduce k nt fn j tk st sts stk =- happyThen1 (fn stk tk) (\r -> happyNewToken new_state sts1 (r `HappyStk` drop_stk))- where (sts1@((HappyCons (st1@(action)) (_)))) = happyDrop k (HappyCons (st) (sts))- drop_stk = happyDropStk k stk+ case happyDrop k (HappyCons (st) (sts)) of+ sts1@((HappyCons (st1@(action)) (_))) ->+ let drop_stk = happyDropStk k stk - (off) = indexShortOffAddr happyGotoOffsets st1- (off_i) = (off Happy_GHC_Exts.+# nt)- (new_state) = indexShortOffAddr happyTable off_i+ off = indexShortOffAddr happyGotoOffsets st1+ off_i = (off Happy_GHC_Exts.+# nt)+ new_state = indexShortOffAddr happyTable off_i + in+ happyThen1 (fn stk tk) (\r -> happyNewToken new_state sts1 (r `HappyStk` drop_stk)) happyDrop 0# l = l happyDrop n (HappyCons (_) (t)) = happyDrop (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) t@@ -502,9 +523,9 @@ happyGoto nt j tk st = {- nothing -} happyDoAction j tk new_state- where (off) = indexShortOffAddr happyGotoOffsets st- (off_i) = (off Happy_GHC_Exts.+# nt)- (new_state) = indexShortOffAddr happyTable off_i+ where off = indexShortOffAddr happyGotoOffsets st+ off_i = (off Happy_GHC_Exts.+# nt)+ new_state = indexShortOffAddr happyTable off_i @@ -514,8 +535,8 @@ -- parse error if we are in recovery and we fail again happyFail 0# tk old_st _ stk@(x `HappyStk` _) =- let (i) = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in--- trace "failing" $ + let i = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in+-- trace "failing" $ happyError_ i tk {- We don't need state discarding for our restricted implementation of@@ -524,16 +545,16 @@ -- discard a state happyFail 0# tk old_st (HappyCons ((action)) (sts)) - (saved_tok `HappyStk` _ `HappyStk` stk) =--- trace ("discarding state, depth " ++ show (length stk)) $- happyDoAction 0# tk action sts ((saved_tok`HappyStk`stk))+ (saved_tok `HappyStk` _ `HappyStk` stk) =+-- trace ("discarding state, depth " ++ show (length stk)) $+ happyDoAction 0# tk action sts ((saved_tok`HappyStk`stk)) -} -- Enter error recovery: generate an error token, -- save the old token and carry on. happyFail i tk (action) sts stk = -- trace "entering error recovery" $- happyDoAction 0# tk action sts ( (Happy_GHC_Exts.unsafeCoerce# (Happy_GHC_Exts.I# (i))) `HappyStk` stk)+ happyDoAction 0# tk action sts ( (Happy_GHC_Exts.unsafeCoerce# (Happy_GHC_Exts.I# (i))) `HappyStk` stk) -- Internal happy errors: @@ -551,9 +572,9 @@ ----------------------------------------------------------------------------- -- Seq-ing. If the --strict flag is given, then Happy emits --- happySeq = happyDoSeq+-- happySeq = happyDoSeq -- otherwise it emits--- happySeq = happyDontSeq+-- happySeq = happyDontSeq happyDoSeq, happyDontSeq :: a -> b -> b happyDoSeq a b = a `seq` b@@ -583,3 +604,4 @@ {-# NOINLINE happyFail #-} -- end of Happy Template.+
morte.cabal view
@@ -1,5 +1,5 @@ Name: morte-Version: 1.0.0+Version: 1.0.1 Cabal-Version: >=1.8.0.2 Build-Type: Simple License: BSD3@@ -8,7 +8,7 @@ Author: Gabriel Gonzalez Maintainer: Gabriel439@gmail.com Bug-Reports: https://github.com/Gabriel439/Haskell-Morte-Library/issues-Synopsis: A bare-bones calculus of constructions+Synopsis: Bare-bones calculus of constructions Description: Morte is a typed, purely functional, and strongly normalizing intermediate language designed for whole-program super-optimization. Use this library to type-check, optimize, parse, pretty-print, serialize and@@ -38,7 +38,7 @@ containers < 0.6 , lens-family-core >= 1.0.0 && < 1.2 , pipes >= 4.0.0 && < 4.2 ,- text >= 0.11.1.0 && < 1.3 ,+ text >= 0.11.1.0 && < 1.2 , transformers >= 0.2.0.0 && < 0.5 Exposed-Modules: Morte.Core,@@ -55,4 +55,4 @@ base >= 4 && < 5 , morte , optparse-applicative < 0.11,- text >= 0.11.1.0 && < 1.3+ text >= 0.11.1.0 && < 1.2
src/Morte/Tutorial.hs view
@@ -88,7 +88,6 @@ > \(a : *) -> \(x : a) -> x <Enter> > <Ctrl-D> > ∀(a : *) → a → a-> > λ(a : *) → λ(x : a) → x > $ @@ -160,7 +159,6 @@ > $ morte < id.mt > ∀(String : *) → String → String-> > λ(String : *) → λ(x : String) → x Morte optimizes our program to the identity function on @String@s, but if@@ -322,7 +320,6 @@ > $ morte < id2.mt > ∀(a : *) → a → a-> > λ(a : *) → λ(x : a) → x -}@@ -513,7 +510,6 @@ > $ morte < bool.mt > ∀(Int : *) → Int → Int → Int-> > λ(Int : *) → λ(Zero : Int) → λ(One : Int) → One The compiler reduces the program to @One@. All the dead code has been@@ -611,7 +607,6 @@ > $ morte < pair.mt > ∀(a : *) → a → a → a-> > λ(a : *) → λ(x : a) → λ(y : a) → y This is also equal to our previous program. Just rename @\'a\'@ to @Int@,@@ -861,7 +856,6 @@ > $ morte < all.mt > ∀(r : *) → r → r → r-> > λ(r : *) → λ(x : r) → λ(_ : r) → x Here's another example of encoding a recursive type, using natural numbers:@@ -1092,7 +1086,6 @@ > $ morte < mapid1.mt > ∀(a : *) → (∀(x : *) → (a → x → x) → x → x) → ∀(x : *) → (a → x → x) → x → x-> > λ(a : *) → λ(l : ∀(x : *) → (a → x → x) → x → x) → l We can prove this by replacing our @map@ with the identity function on@@ -1127,7 +1120,6 @@ > $ morte < mapid2.mt > ∀(a : *) → (∀(x : *) → (a → x → x) → x → x) → ∀(x : *) → (a → x → x) → x → x-> > λ(a : *) → λ(va : ∀(x : *) → (a → x → x) → x → x) → va However, we don't have to trust our fallible eyes. We can enlist the@@ -1255,7 +1247,6 @@ > $ morte < mapcomp1.mt > ∀(a : *) → ∀(b : *) → ∀(c : *) → (b → c) → (a → b) → (∀(x : *) → (a → x → x) → > x → x) → ∀(x : *) → (c → x → x) → x → x-> > λ(a : *) → λ(b : *) → λ(c : *) → λ(f : b → c) → λ(g : a → b) → λ(l : ∀(x : *) > → (a → x → x) → x → x) → λ(x : *) → λ(Cons : c → x → x) → l x (λ(va : a) → Con > s (f (g va)))@@ -1446,7 +1437,6 @@ > $ morte < corecursive.mt > ∀(a : *) → (∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) → x) → > x) → ∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) → x) → x-> > λ(a : *) → λ(st : ∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) > → x) → x) → st @@ -1458,7 +1448,6 @@ > ∀(a : *) → ∀(b : *) → ∀(c : *) → (b → c) → (a → b) → (∀(x : *) → (∀(s : *) → s > → (s → ∀(x : *) → (a → s → x) → x) → x) → x) → ∀(x : *) → (∀(s : *) → s → (s > → ∀(x : *) → (c → s → x) → x) → x) → x-> > λ(a : *) → λ(b : *) → λ(c : *) → λ(f : b → c) → λ(g : a → b) → λ(st : ∀(x : *) > → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) → x) → x) → λ(x : *) → λ(S > : ∀(s : *) → s → (s → ∀(x : *) → (c → s → x) → x) → x) → st x (λ(s : *) → λ(s@@ -1794,7 +1783,6 @@ > $ morte < recursive.mt > ∀(String : *) → ∀(U : *) → U → ∀(x : *) → (String → x → x) → ((String → x > ) → x) → (U → x) → x-> > λ(String : *) → λ(U : *) → λ(Unit : U) → λ(x : *) → λ(PutStrLn : String → > x → x) → λ(GetLine : (String → x) → x) → λ(Return : U → x) → GetLine (λ( > va : String) → PutStrLn va (GetLine (λ(va@1 : String) → PutStrLn va@1 (Ge@@ -1979,7 +1967,6 @@ > $ morte < corecursive.mt > ∀(String : *) → ∀(r : *) → ∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (String > → s → x) → ((String → s) → x) → (r → x) → x) → x) → x-> > λ(String : *) → λ(r : *) → λ(x : *) → λ(k : ∀(s : *) → s → (s → ∀(x : *) → (St > ring → s → x) → ((String → s) → x) → (r → x) → x) → x) → k (∀(x : *) → (String > → x) → x → x) (λ(x : *) → λ(Just : String → x) → λ(Nothing : x) → Nothing) (λ