<commit_before>{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PartialTypeSignatures #-}

{- |
Module      : Verifier.SAW.Term.CtxTerm
Copyright   : Galois, Inc. 2018
License     : BSD3
Stability   : experimental
Portability : non-portable (language extensions)

The purpose of this module is to define a dependently-typed / GADT approach
to representing SAW core terms, that reflects (to some degree) the typing
and context information in the Haskell type of a term.

Why are we doing this, when GADT programming can be so gross? The point of all
this is to get all the deBruijn indices right. Doing deBruijn index math when
manipulating open terms can be error prone and hard to read, and those bugs are
really hard to track down. Although GADT programming can be a pain sometimes,
this file is organized so at least you will always get the deBruijn indices
right when you finally get GHC to accept your code. :)
-}

module Verifier.SAW.Term.CtxTerm
  (
    -- * Re-exports from "Data.Parameterized.Context"
    -- | We use DataKinds to represent contexts of free variables at the type level.
    -- These contexts are "inside-out", meaning that the most recently-bound
    -- variable is listed on the outside. We reflect this by having that most
    -- recently-bound variable to the right in '::>'.
    Ctx(..), EmptyCtx, (::>), type (<+>)
    -- * Contexts and Bindings
  , Typ
  , CtxInvApp, CtxInv
  , Bindings(..), bindingsLength, InvBindings(..), InBindings(..)
  , invAppendBindings, invertBindings
    -- * Terms in Context
  , Arrows
  , CtxTerm(..), CtxTerms(..), CtxTermsCtx(..)
  , mkClosedTerm, mkClosedTyp, elimClosedTerm
  , ExistsTp(..), ctxBindingsOfTerms
  , ctxTermsForBindings
    -- * Operations on Terms-in-Context
  , MonadTerm(..)
  , ctxLambda, ctxPi, ctxPi1
    -- * Generalized Lifting and Substitution<commit_msg>Sort LANGUAGE pragmas and remove duplicates.<commit_after>{- |
Module      : Verifier.SAW.Term.CtxTerm
Copyright   : Galois, Inc. 2018
License     : BSD3
Stability   : experimental
Portability : non-portable (language extensions)

The purpose of this module is to define a dependently-typed / GADT approach
to representing SAW core terms, that reflects (to some degree) the typing
and context information in the Haskell type of a term.

Why are we doing this, when GADT programming can be so gross? The point of all
this is to get all the deBruijn indices right. Doing deBruijn index math when
manipulating open terms can be error prone and hard to read, and those bugs are
really hard to track down. Although GADT programming can be a pain sometimes,
this file is organized so at least you will always get the deBruijn indices
right when you finally get GHC to accept your code. :)
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Verifier.SAW.Term.CtxTerm
  (
    -- * Re-exports from "Data.Parameterized.Context"
    -- | We use DataKinds to represent contexts of free variables at the type level.
    -- These contexts are "inside-out", meaning that the most recently-bound
    -- variable is listed on the outside. We reflect this by having that most
    -- recently-bound variable to the right in '::>'.
    Ctx(..), EmptyCtx, (::>), type (<+>)
    -- * Contexts and Bindings
  , Typ
  , CtxInvApp, CtxInv
  , Bindings(..), bindingsLength, InvBindings(..), InBindings(..)
  , invAppendBindings, invertBindings
    -- * Terms in Context
  , Arrows
  , CtxTerm(..), CtxTerms(..), CtxTermsCtx(..)
  , mkClosedTerm, mkClosedTyp, elimClosedTerm
  , ExistsTp(..), ctxBindingsOfTerms
  , ctxTermsForBindings
    -- * Operations on Terms-in-Context
  , MonadTerm(..)
  , ctxLambda, ctxPi, ctxPi1
    -- * Generalized Lifting and Substitution
{'fraction_non_alphanumeric': 0.11118170266836086, 'fraction_numerical': 0.0025412960609911056, 'mean_word_length': 3.6623889437314907, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6634418', 'n_tokens_mistral': 1592, 'n_tokens_neox': 1535, 'n_words': 506}