search

haskell-mafia / projector

A typed, total templating language
BSD 3-Clause "New" or "Revised" License
7 stars 7 forks source link

NF reduction bug #28

Closed thumphries closed 7 years ago

thumphries commented 7 years ago

Having trouble reducing this. Looks like a mistake in match or dodgy incomplete substitution somewhere, stashing for later.

λ> ppExpr (whnf expr)
"0"
λ> ppExpr (nf expr)
"case kermit_1 of Basin x_0 x_1 x_2 x_3 x_4 -> 0; Bbcbojgc x_0_1 x_1_1 x_2_1 x_3_1 -> 0; Billabong x_0_2 x_1_2 x_2_2 -> x_0_2"
λ> T.putStrLn $ ppExpr (expr)
(\kermit : Sdnmqbzw. (\kermit : Battleship. case kermit of Basin x_0 x_1 x_2 x_3 x_4 -> 0; Bbcbojgc x_0 x_1 x_2 x_3 -> 0; Billabong x_0 x_1 x_2 -> x_0) (case kermit of Sound  -> case kermit of Sound  -> Basin (\kermit : (String -> String). \kermit : Bool. 0) "salted" (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. "salted") "salted" (\kermit : (Int -> (Bool -> Bool)). "salted"); Spring x_0 x_1 -> Basin (\kermit : (String -> String). \kermit : Bool. 0) "salted" (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. "salted") "salted" (\kermit : (Int -> (Bool -> Bool)). "salted"); Swamp x_0 x_1 x_2 x_3 x_4 -> Basin (\kermit : (String -> String). \kermit : Bool. 0) "salted" (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. "salted") "salted" (\kermit : (Int -> (Bool -> Bool)). "salted"); Tlmbhjav x_0 x_1 x_2 x_3 -> Basin (\kermit : (String -> String). \kermit : Bool. 0) x_0 (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. x_0) x_0 (\kermit : (Int -> (Bool -> Bool)). x_0); Spring x_0 x_1 -> case kermit of Sound  -> Basin (\kermit : (String -> String). \kermit : Bool. 0) "salted" (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. "salted") "salted" (\kermit : (Int -> (Bool -> Bool)). "salted"); Spring x_0 x_1 -> Basin (\kermit : (String -> String). \kermit : Bool. 0) "salted" (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. "salted") "salted" (\kermit : (Int -> (Bool -> Bool)). "salted"); Swamp x_0 x_1 x_2 x_3 x_4 -> Basin (\kermit : (String -> String). \kermit : Bool. 0) "salted" (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. "salted") "salted" (\kermit : (Int -> (Bool -> Bool)). "salted"); Tlmbhjav x_0 x_1 x_2 x_3 -> Basin (\kermit : (String -> String). \kermit : Bool. 0) x_0 (\kermit : (((Int -> Int) -> ((Bool -> Bool) -> (Int -> String))) -> Bool). \kermit : Bool. x_0) x_0 (\kermit : (Int -> (Bool -> Bool)). x_0); Swamp x_0 x_1 x_2 x_3 x_4 -> x_4 "salted"; Tlmbhjav x_0 x_1 x_2 x_3 -> x_1)) (Sound )
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Kermit where

import Data.Map.Strict
import P
import Projector.Core
import Test.Projector.Core.Arbitrary

ty = TLit TInt

ctx = TypeDecls
    { unTypeDecls =
        fromList
          [ ( TypeName { unTypeName = "Battleship" }
            , DVariant
                [ ( Constructor { unConName = "Basin" }
                  , [ TArrow
                        (TArrow (TLit TString) (TLit TString))
                        (TArrow (TLit TBool) (TLit TInt))
                    , TLit TString
                    , TArrow
                        (TArrow
                           (TArrow
                              (TArrow (TLit TInt) (TLit TInt))
                              (TArrow
                                 (TArrow (TLit TBool) (TLit TBool))
                                 (TArrow (TLit TInt) (TLit TString))))
                           (TLit TBool))
                        (TArrow (TLit TBool) (TLit TString))
                    , TLit TString
                    , TArrow
                        (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                        (TLit TString)
                    ]
                  )
                , ( Constructor { unConName = "Bbcbojgc" }
                  , [ TArrow
                        (TArrow
                           (TLit TInt)
                           (TArrow (TLit TString) (TArrow (TLit TBool) (TLit TString))))
                        (TLit TBool)
                    , TArrow
                        (TArrow
                           (TLit TString)
                           (TArrow
                              (TArrow (TArrow (TLit TInt) (TLit TBool)) (TLit TBool))
                              (TLit TInt)))
                        (TLit TString)
                    , TArrow
                        (TArrow
                           (TArrow
                              (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TString)))
                              (TArrow (TLit TBool) (TLit TInt)))
                           (TArrow (TLit TInt) (TLit TInt)))
                        (TLit TString)
                    , TLit TString
                    ]
                  )
                , ( Constructor { unConName = "Billabong" }
                  , [ TLit TInt , TLit TBool , TLit TString ]
                  )
                ]
            )
          , ( TypeName { unTypeName = "Dinghy" }
            , DVariant
                [ ( Constructor { unConName = "Channel" }
                  , [ TArrow
                        (TArrow
                           (TLit TString)
                           (TArrow
                              (TArrow (TArrow (TLit TString) (TLit TInt)) (TLit TBool))
                              (TArrow (TLit TString) (TArrow (TLit TInt) (TLit TBool)))))
                        (TLit TString)
                    , TLit TString
                    , TArrow (TLit TString) (TLit TBool)
                    , TArrow
                        (TArrow
                           (TArrow (TLit TInt) (TLit TInt))
                           (TArrow
                              (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                              (TArrow (TArrow (TLit TString) (TLit TInt)) (TLit TString))))
                        (TArrow (TLit TInt) (TLit TBool))
                    , TLit TInt
                    ]
                  )
                , ( Constructor { unConName = "Harbour" } , [] )
                , ( Constructor { unConName = "Marsh" }
                  , [ TVar TypeName { unTypeName = "Battleship" }
                    , TLit TString
                    , TArrow
                        (TArrow
                           (TVar TypeName { unTypeName = "Battleship" })
                           (TVar TypeName { unTypeName = "Battleship" }))
                        (TArrow (TLit TInt) (TLit TInt))
                    , TLit TInt
                    ]
                  )
                , ( Constructor { unConName = "Nqqpgbjf" }
                  , [ TLit TInt , TLit TInt ]
                  )
                , ( Constructor { unConName = "Pond" }
                  , [ TArrow
                        (TArrow
                           (TVar TypeName { unTypeName = "Battleship" })
                           (TVar TypeName { unTypeName = "Battleship" }))
                        (TLit TBool)
                    ]
                  )
                , ( Constructor { unConName = "Puddle" }
                  , [ TArrow
                        (TLit TInt) (TVar TypeName { unTypeName = "Battleship" })
                    , TArrow (TLit TBool) (TVar TypeName { unTypeName = "Battleship" })
                    ]
                  )
                , ( Constructor { unConName = "Qjowkzdp" }
                  , [ TVar TypeName { unTypeName = "Battleship" }
                    , TArrow (TLit TBool) (TLit TBool)
                    , TArrow
                        (TVar TypeName { unTypeName = "Battleship" })
                        (TVar TypeName { unTypeName = "Battleship" })
                    ]
                  )
                , ( Constructor { unConName = "Reservoir" }
                  , [ TArrow
                        (TVar TypeName { unTypeName = "Battleship" })
                        (TArrow (TLit TString) (TLit TBool))
                    ]
                  )
                ]
            )
          , ( TypeName { unTypeName = "Nlksecfj" }
            , DVariant
                [ ( Constructor { unConName = "Rsagxofq" } , [ TLit TString ] )
                , ( Constructor { unConName = "Sea" }
                  , [ TArrow
                        (TArrow
                           (TLit TInt)
                           (TArrow (TVar TypeName { unTypeName = "Dinghy" }) (TLit TBool)))
                        (TVar TypeName { unTypeName = "Dinghy" })
                    , TArrow
                        (TArrow
                           (TVar TypeName { unTypeName = "Battleship" })
                           (TArrow
                              (TVar TypeName { unTypeName = "Battleship" })
                              (TVar TypeName { unTypeName = "Battleship" })))
                        (TVar TypeName { unTypeName = "Battleship" })
                    , TLit TInt
                    ]
                  )
                ]
            )
          , ( TypeName { unTypeName = "Sdnmqbzw" }
            , DVariant
                [ ( Constructor { unConName = "Sound" } , [] )
                , ( Constructor { unConName = "Spring" }
                  , [ TArrow
                        (TArrow
                           (TVar TypeName { unTypeName = "Nlksecfj" })
                           (TVar TypeName { unTypeName = "Nlksecfj" }))
                        (TLit TInt)
                    , TArrow
                        (TArrow (TLit TString) (TVar TypeName { unTypeName = "Dinghy" }))
                        (TArrow (TLit TBool) (TLit TString))
                    ]
                  )
                , ( Constructor { unConName = "Swamp" }
                  , [ TArrow
                        (TArrow
                           (TVar TypeName { unTypeName = "Nlksecfj" })
                           (TArrow
                              (TLit TBool)
                              (TArrow
                                 (TArrow
                                    (TVar TypeName { unTypeName = "Nlksecfj" })
                                    (TVar TypeName { unTypeName = "Nlksecfj" }))
                                 (TLit TInt))))
                        (TArrow (TVar TypeName { unTypeName = "Dinghy" }) (TLit TInt))
                    , TArrow (TVar TypeName { unTypeName = "Dinghy" }) (TLit TString)
                    , TVar TypeName { unTypeName = "Dinghy" }
                    , TLit TBool
                    , TArrow
                        (TLit TString) (TVar TypeName { unTypeName = "Battleship" })
                    ]
                  )
                , ( Constructor { unConName = "Tlmbhjav" }
                  , [ TLit TString
                    , TVar TypeName { unTypeName = "Battleship" }
                    , TLit TBool
                    , TVar TypeName { unTypeName = "Nlksecfj" }
                    ]
                  )
                ]
            )
          ]
    }

expr = EApp
    (ELam
       Name { unName = "kermit" }
       (TVar TypeName { unTypeName = "Sdnmqbzw" })
       (EApp
          (ELam
             Name { unName = "kermit" }
             (TVar TypeName { unTypeName = "Battleship" })
             (ECase
                (EVar Name { unName = "kermit" })
                [ ( PCon
                      Constructor { unConName = "Basin" }
                      [ PVar Name { unName = "x_0" }
                      , PVar Name { unName = "x_1" }
                      , PVar Name { unName = "x_2" }
                      , PVar Name { unName = "x_3" }
                      , PVar Name { unName = "x_4" }
                      ]
                  , ELit (VInt 0)
                  )
                , ( PCon
                      Constructor { unConName = "Bbcbojgc" }
                      [ PVar Name { unName = "x_0" }
                      , PVar Name { unName = "x_1" }
                      , PVar Name { unName = "x_2" }
                      , PVar Name { unName = "x_3" }
                      ]
                  , ELit (VInt 0)
                  )
                , ( PCon
                      Constructor { unConName = "Billabong" }
                      [ PVar Name { unName = "x_0" }
                      , PVar Name { unName = "x_1" }
                      , PVar Name { unName = "x_2" }
                      ]
                  , EVar Name { unName = "x_0" }
                  )
                ]))
          (ECase
             (EVar Name { unName = "kermit" })
             [ ( PCon Constructor { unConName = "Sound" } []
               , ECase
                   (EVar Name { unName = "kermit" })
                   [ ( PCon Constructor { unConName = "Sound" } []
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" } (TLit TBool) (ELit (VString "salted")))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (ELit (VString "salted"))
                         ]
                     )
                   , ( PCon
                         Constructor { unConName = "Spring" }
                         [ PVar Name { unName = "x_0" } , PVar Name { unName = "x_1" } ]
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" } (TLit TBool) (ELit (VString "salted")))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (ELit (VString "salted"))
                         ]
                     )
                   , ( PCon
                         Constructor { unConName = "Swamp" }
                         [ PVar Name { unName = "x_0" }
                         , PVar Name { unName = "x_1" }
                         , PVar Name { unName = "x_2" }
                         , PVar Name { unName = "x_3" }
                         , PVar Name { unName = "x_4" }
                         ]
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" } (TLit TBool) (ELit (VString "salted")))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (ELit (VString "salted"))
                         ]
                     )
                   , ( PCon
                         Constructor { unConName = "Tlmbhjav" }
                         [ PVar Name { unName = "x_0" }
                         , PVar Name { unName = "x_1" }
                         , PVar Name { unName = "x_2" }
                         , PVar Name { unName = "x_3" }
                         ]
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , EVar Name { unName = "x_0" }
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" }
                                (TLit TBool)
                                (EVar Name { unName = "x_0" }))
                         , EVar Name { unName = "x_0" }
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (EVar Name { unName = "x_0" })
                         ]
                     )
                   ]
               )
             , ( PCon
                   Constructor { unConName = "Spring" }
                   [ PVar Name { unName = "x_0" } , PVar Name { unName = "x_1" } ]
               , ECase
                   (EVar Name { unName = "kermit" })
                   [ ( PCon Constructor { unConName = "Sound" } []
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" } (TLit TBool) (ELit (VString "salted")))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (ELit (VString "salted"))
                         ]
                     )
                   , ( PCon
                         Constructor { unConName = "Spring" }
                         [ PVar Name { unName = "x_0" } , PVar Name { unName = "x_1" } ]
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" } (TLit TBool) (ELit (VString "salted")))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (ELit (VString "salted"))
                         ]
                     )
                   , ( PCon
                         Constructor { unConName = "Swamp" }
                         [ PVar Name { unName = "x_0" }
                         , PVar Name { unName = "x_1" }
                         , PVar Name { unName = "x_2" }
                         , PVar Name { unName = "x_3" }
                         , PVar Name { unName = "x_4" }
                         ]
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" } (TLit TBool) (ELit (VString "salted")))
                         , ELit (VString "salted")
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (ELit (VString "salted"))
                         ]
                     )
                   , ( PCon
                         Constructor { unConName = "Tlmbhjav" }
                         [ PVar Name { unName = "x_0" }
                         , PVar Name { unName = "x_1" }
                         , PVar Name { unName = "x_2" }
                         , PVar Name { unName = "x_3" }
                         ]
                     , ECon
                         Constructor { unConName = "Basin" }
                         TypeName { unTypeName = "Battleship" }
                         [ ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TString) (TLit TString))
                             (ELam Name { unName = "kermit" } (TLit TBool) (ELit (VInt 0)))
                         , EVar Name { unName = "x_0" }
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow
                                (TArrow
                                   (TArrow (TLit TInt) (TLit TInt))
                                   (TArrow
                                      (TArrow (TLit TBool) (TLit TBool))
                                      (TArrow (TLit TInt) (TLit TString))))
                                (TLit TBool))
                             (ELam
                                Name { unName = "kermit" }
                                (TLit TBool)
                                (EVar Name { unName = "x_0" }))
                         , EVar Name { unName = "x_0" }
                         , ELam
                             Name { unName = "kermit" }
                             (TArrow (TLit TInt) (TArrow (TLit TBool) (TLit TBool)))
                             (EVar Name { unName = "x_0" })
                         ]
                     )
                   ]
               )
             , ( PCon
                   Constructor { unConName = "Swamp" }
                   [ PVar Name { unName = "x_0" }
                   , PVar Name { unName = "x_1" }
                   , PVar Name { unName = "x_2" }
                   , PVar Name { unName = "x_3" }
                   , PVar Name { unName = "x_4" }
                   ]
               , EApp (EVar Name { unName = "x_4" }) (ELit (VString "salted"))
               )
             , ( PCon
                   Constructor { unConName = "Tlmbhjav" }
                   [ PVar Name { unName = "x_0" }
                   , PVar Name { unName = "x_1" }
                   , PVar Name { unName = "x_2" }
                   , PVar Name { unName = "x_3" }
                   ]
               , EVar Name { unName = "x_1" }
               )
             ])))
    (ECon
       Constructor { unConName = "Sound" }
       TypeName { unTypeName = "Sdnmqbzw" }
       [])
thumphries commented 7 years ago

Can fix by stashing the evaluated e' when a pattern match fails, but that might be papering over a more serious subst bug

thumphries commented 7 years ago

OK it's a decent bug. thank mr quickcheck

the lexically-scoped maps require a full traversal for substitution to complete. Since we go under binders etc (dumb use of nf instead of whnf when we hit an App), we are going to occasionally hit Apps and Cases where the e is not a redex, but we need to keep reducing anyway to finish substituting.

We also have a real inconsistency! If the e is not a redex, but we have a pattern PVar, we might take and inline the wrong branch. Might need to alter the semantics a little, I'm not sure any eval strategy will work. e.g. if we hit a Con pattern and we're not a Con yet, fail the match immediately.

steps: