------------------------------------------------------------------------
-- |
-- Module      : Verifier.SAW.Simulator.What4.PosNat
-- Copyright   : Galois, Inc. 2018
-- License     : BSD3
-- Maintainer  : sweirich@galois.com
-- Stability   : experimental
-- Portability : non-portable (language extensions)
-- 
-- A runtime representation of positive nats
------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

-- This module makes use of 'KnownNat' constraints in its interface as
-- opposed to arguments of type 'NatRepr' or 'PosNatRepr'
-- (cf. 'addPosNat'). As a result, we need two

-- to allow implicitly provided nats
{-# LANGUAGE AllowAmbiguousTypes #-}

-- to allow 'WithKnownNat' 
{-# OPTIONS_GHC -Wno-warnings-deprecations #-}

module Verifier.SAW.Simulator.What4.PosNat where
-- TODO: find the right place for this code

import GHC.TypeNats
import Data.Parameterized.NatRepr
import Data.Parameterized.Some(Some(..))


-- We include the KnownNat constraint here so that we can avoid using
-- withKnownNat outside this module.  The downside is that we have two
-- different runtime representations of these positive nats --- the
-- one stored in the KnownNat, and the one stored in the NatRepr.

-- | Runtime representation of a non-zero natural number
data PosNat (n :: Nat) where
  PosNat :: (1 <= n, KnownNat n) => NatRepr n -> PosNat n

-- | Check whether an integer is a positive nat
somePosNat :: Integral a => a -> Maybe (Some PosNat)
somePosNat n 
  | Just (Some nr) <- someNat n,
    Just LeqProof  <- testLeq (knownNat @1) nr
  = withKnownNat nr $ Just (Some (PosNat nr))
  | otherwise
  = Nothing

-- The above definition should be added to
-- 'Data.Parameterized.NatRepr' so that the redundant check for
-- positivity can be removed. Annoyingly, we cannot do 'testLeq'
-- without already knowing that w >= 0)


-- | Add two numbers together and return a proof that their
-- result is positive.
addPosNat :: forall w1 w2.
  (1 <= w1, 1 <= w2, KnownNat w1, KnownNat w2) => PosNat (w1 + w2)
addPosNat =
  let w1  = knownNat @w1
      w2  = knownNat @w2
      sm  = addNat w1 w2 in
  case leqAddPos w1 w2 of 
    LeqProof -> withKnownNat sm $ PosNat sm

-- I would hope that the 'leqAddPos' call can be compiled away...


--- Not needed but included for completeness

-- | Compare for equality, returning witness if true
instance TestEquality PosNat where
  testEquality (PosNat n1) (PosNat n2) =
    case testEquality n1 n2 of
      Just Refl -> Just Refl
      Nothing   -> Nothing
