save

Draft.shitt

@@ -94,8 +94,10 @@ fun nomatchTest (n : N) (_: Id (succ (succ n)) (succ n)) : N where
 
 
 mutual
+
   fun even (_ : N) : Bool
   fun odd  (_ : N) : Bool
+
 begin
 
   fun even

README.md

@@ -360,3 +360,17 @@ def addComm (x y : N) : Id (add x y) (add y x) where
 
 
 ```
+
+## Reference
+
+Pattern matching and inductive type:
+
+- Ulf Norell. [Towards a practical programming language based on dependent type theory](https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf).
+
+Solving meta variables:
+
+- András Kovács. [elaboration-zoo](https://github.com/AndrasKovacs/elaboration-zoo).
+
+Termination checking:
+
+- Karl Mehltretter. [Termination Checking for a Dependently Typed Language](https://www.cse.chalmers.se/~abela/mehltret-da.pdf).

package.yaml

@@ -26,6 +26,7 @@ dependencies:
 - exception-transformers
 - megaparsec
 - mtl
+- matrix
 
 ghc-options:
 - -Wall

shitt.cabal

@@ -34,6 +34,8 @@ library
       ShiTT.Meta
       ShiTT.Parser
       ShiTT.Syntax
+      ShiTT.Termination.Call
+      ShiTT.Termination.Ord
       ShiTT.TermParser
       Test
   other-modules:
@@ -68,6 +70,7 @@ library
       base >=4.7 && <5
     , containers
     , exception-transformers
+    , matrix
     , megaparsec
     , mtl
     , transformers
@@ -108,6 +111,7 @@ executable shitt-exe
       base >=4.7 && <5
     , containers
     , exception-transformers
+    , matrix
     , megaparsec
     , mtl
     , shitt
@@ -150,6 +154,7 @@ test-suite shitt-test
       base >=4.7 && <5
     , containers
     , exception-transformers
+    , matrix
     , megaparsec
     , mtl
     , shitt

src/ShiTT/Context.hs

@@ -212,6 +212,12 @@ data Fun = Fun
  , funClauses :: Maybe [Clause]
  }
 
+instance Eq Fun where 
+  f == g = f.funName == g.funName
+
+instance Ord Fun where 
+  compare f g = compare f.funName g.funName
+
 instance Show Fun where 
   show = funName
 

src/ShiTT/Termination/Call.hs

@@ -0,0 +1,21 @@
+module ShiTT.Termination.Call where 
+
+import ShiTT.Eval
+import ShiTT.Context
+import ShiTT.Syntax
+import Data.Matrix hiding (trace)
+import qualified Data.Set as S
+import ShiTT.Termination.Ord
+
+instance Ord e => Ord (Matrix e) where 
+  compare a b = compare (toList a) (toList b)
+
+data CallMat = CallMat 
+  { fromFun :: Fun 
+  , callFun :: Fun 
+  , callMat :: Matrix Order
+  } deriving (Eq, Ord, Show)
+
+-- | The cm function from paper.
+-- getCallMat :: (Fun, [Pattern]) -> (Fun, Spine) -> CallMat
+-- getCallMat 

src/ShiTT/Termination/Ord.hs

@@ -0,0 +1,70 @@
+module ShiTT.Termination.Ord where
+
+import ShiTT.Context
+import ShiTT.Syntax
+
+data Order = Unsure | LessEq | Less
+  deriving (Eq, Ord)
+
+instance Show Order where
+  show = \case
+    Unsure -> "?"
+    Less   -> "<"
+    LessEq -> "<="
+
+-- | Unsure as zero, LessEq as one, Less as infinity
+instance Num Order where
+  fromInteger 0 = Unsure
+  fromInteger _ = LessEq
+
+  x + y = max x y
+    -- case (x, y) of 
+    --   (Unsure, x) -> x -- Unsure as zero 
+    --   (x, Unsure) -> x 
+    --   (Less, x) -> Less -- Less as inf 
+    --   (x, Less) -> Less 
+    --   (LessEq, LessEq) -> LessEq
+
+  x * y = case (x, y) of
+    (Unsure, _) -> Unsure -- Unsure as zero
+    (_, Unsure) -> Unsure
+    (LessEq, x) -> x      -- LessEq as one
+    (x, LessEq) -> x
+    (Less, Less) -> Less
+
+  abs = error "I hate Num"
+  signum = error "I hate Num"
+  negate = error "I hate Num"
+
+maxOf :: Foldable f => f Order -> Order
+maxOf = foldr (+) Unsure
+
+minOf :: Foldable f => f Order -> Order
+minOf = foldr min Less
+
+-- | We would simply ignore the inaccessible patterns, so no need for context. 
+--   It would not be a big problem, since we (usually) could show the decreasing by other accessible pattern .
+compareTP :: Context -> Value -> Pattern -> Order
+compareTP ctx e p = case (e, p) of
+  (VVar x, p) -> compareNP ctx x p     -- This case might be useless
+  (VPatVar x [], p) -> compareNP ctx x p
+  (VCon con' [], PCon con ps _)
+    | con' == con -> LessEq
+  (VCon con' con_arg, PCon con pcon_arg _)
+    | con' == con ->
+        case lookupCon' con ctx of
+          Just (dat, con) ->
+            let data_para_leng = length dat.dataPara 
+                con_arg' = map fst $ drop data_para_leng con_arg in
+              if (length con_arg - data_para_leng) == length pcon_arg then
+                minOf $ zipWith (compareTP ctx) con_arg' pcon_arg
+              else
+                Unsure
+          _ -> Unsure
+  _ -> Unsure
+
+compareNP :: Context -> Name -> Pattern -> Order
+compareNP ctx x = \case 
+  PVar x' _ | x == x' -> LessEq
+  PCon con ps _       -> Less * maxOf (map (compareNP ctx x) ps)
+  _                   -> Unsure

src/ShiTT/Termination/README.md

@@ -0,0 +1 @@
+This part is mainly based on [Termination Checking for a Dependently Typed Language](https://www.cse.chalmers.se/~abela/mehltret-da.pdf).