text:
module Structure.Operator.Monoid.Submonoid where

import      Lvl
open import Logic
open import Logic.Predicate
open import Logic.Predicate.Equiv
open import Sets.PredicateSet renaming (_≡_ to _≡ₛ_)
open import Structure.Setoid
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T : Type{ℓ}

module _ {ℓₛ} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫_ : T → T → T} (M : Monoid(_▫_)) where
  record Submonoid (S : PredSet{ℓₛ}(T)) : Stmt{Lvl.of(T) Lvl.⊔ ℓₛ} where
    constructor intro
    open Monoid(M) using (id)
    field
      ⦃ contains-identity ⦄ : (id ∈ S)
      ⦃ operator-closure ⦄  : ∀{x y} → ⦃ x ∈ S ⦄ → ⦃ y ∈ S ⦄ → ((x ▫ y) ∈ S)

    Object = ∃(S)

    _▫ₛ_ : Object → Object → Object
    ([∃]-intro x) ▫ₛ ([∃]-intro y) = [∃]-intro (x ▫ y)

    instance
      monoid : Monoid(_▫ₛ_)
      BinaryOperator.congruence                (Monoid.binary-operator    monoid)   = congruence₂(_▫_)
      Associativity.proof                      (Monoid.associativity      monoid)   = associativity(_▫_)
      ∃.witness                                (Monoid.identity-existence monoid)   = [∃]-intro id
      Identityₗ.proof (Identity.left  (∃.proof (Monoid.identity-existence monoid))) = identityₗ(_▫_)(id)
      Identityᵣ.proof (Identity.right (∃.proof (Monoid.identity-existence monoid))) = identityᵣ(_▫_)(id)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Structures
open import SacTy

module ExtractSac where
open import Data.String as S hiding (_++_) renaming (_≟_ to _≟s_)
open import Data.List as L hiding (_++_)
open import Data.List.Categorical
open import Data.List.Properties as L
open import Data.Nat as N
open import Agda.Builtin.Nat using (div-helper; mod-helper)

open import Data.Nat.Properties as N
open import Data.Nat.Show renaming (show to showNat)
open import Data.Product as Σ hiding (map)
open import Data.Sum hiding (map)
open import Data.Vec as V using (Vec; [] ; _∷_)
open import Data.Char using (Char) renaming (_≈?_ to _c≈?_)
open import Data.Bool
open import Data.Fin as F using (Fin; zero; suc; inject₁; fromℕ<; #_)
open import Data.Maybe as M using (Maybe; just; nothing)
open import Data.Unit

open import Category.Monad
open import Category.Monad.State

open import Relation.Binary.PropositionalEquality as Eq hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)

open import Reflection hiding (return; _>>=_; _>>_)
open import Reflection.Term
import      Reflection.Name as RN
open import Reflection.Annotated
open import Reflection.Universe
open import Reflection.Annotated.Free

open import Function

open import Array.Base
open import Array.Properties
open import APL2 using (reduce-1d; _↑_; _↓_; ▴_; ▾_; _-↑⟨_⟩_; _↑⟨_⟩_)

open import Agda.Builtin.Float

open RawMonad ⦃ ... ⦄

-- Glorified sigma type for variable-type pairs
record VarTy : Set where
  constructor _∈_~_
  field v : String
        s : Err SacTy
        t : Arg Type

-- Glorified sigma type for variable-assertion pairs
record Assrt : Set where
  constructor mk
  field v : String
        a : String

Assrts = List Assrt

-- The state used when traversing a Pi type.
record PS : Set where
  field
    cnt : ℕ           -- The source of unique variable names
    cur : String      -- Current variable name (used to collect assertions from its type)
    ctx : List VarTy  -- Names in the telscopes to resolve deBruijn indices
    ret : String      -- Variable that the function returns as a result.
                      -- We assume that there is always a single variable and its name
                      -- is known upfront.  We need this to generate assertions from the
                      -- return type.
    assrts : Assrts   -- Assertions that we generate per each variable.
    kst : KS          -- Compilation state (in case we have to extract some functions used in types)

defaultPS : PS
defaultPS = record { cnt = 1
                   ; cur = ""
                   ; ctx = []
                   ; ret = "__ret"
                   ; assrts = []
                   ; kst = defaultKS
                   }

-- Pack the information about new variables generated
-- by patterns in the clause, assignments to these,
-- and the list of conditions for "getting into" the
-- clause.  E.g.
--   foo : List ℕ → ℕ
--   foo (x ∷ xs) 2 = ...
--
-- Assume that we named top-level arguments [a, b]
-- Then, new variables for this clause are going to be
--     [x, xs]
-- Assignments are:
--     [x = hd a, xs = tl a]
-- Conditions are:
--     [is-cons a, b == 2]
--
-- `cnt` is merely a source of fresh variables.
record PatSt : Set where
  constructor mk
  field
    vars    : List (String × ℕ) --Strings
    assigns : Strings
    conds   : Strings
    cnt     : ℕ

defaultPatSt : PatSt
defaultPatSt = mk [] [] [] 1

SPS = State PS

-- The main function kit to extract sac functions.
kompile-fun    : Type → Term → Name → SKS Prog
kompile-pi     : Type → SPS (Err SacTy) --Prog
kompile-cls    : Clauses → (vars : Strings) → (ret : String) → SKS Prog
kompile-clpats : Telescope → (pats : List $ Arg Pattern) → (vars : Strings) → PatSt → Err PatSt
{-# TERMINATING #-}
kompile-term   : Term → {- (varctx : Strings) -} {- List VarTy -} Telescope → SKS Prog

-- Normalise the name of the symbols (functions, constructors, ...)
-- that we obtain from showName, i.e. remove dots, replace weird
-- symbols with ascii.
nnorm : String → String
nnorm s = replace '.' "_"
        $ replace '-' "_"
        $ replace '+' "plus"
        $ replace 'α' "alpha"
        $ replace 'ω' "omega"
        $ replace '→' "to"
        $ s
  where
    repchar : (from : Char) (to : String) (x : Char) → String
    repchar from to x with does $ x c≈? from
    ... | true  = to
    ... | false = fromList (x ∷ [])

    replace : (from : Char) (to : String) → String → String
    replace f t s = "" ++/ L.map (repchar f t) (toList s)

private
  kf : String → Prog
  kf x = error $ "kompile-fun: " ++ x

  validate-ty : Err SacTy → Prog
  validate-ty (error x) = error x
  validate-ty (ok τ) = let τ′ = sacty-normalise τ in
                       case nested? τ′ of λ where
                         hom → ok $ sacty-to-string τ′
                         nes → error $ "sac does not support nested types, but `"
                                    ++ sacty-to-string τ′ ++ "` found"

  module R = RawMonadState (StateMonadState KS)

kompile-fun ty (pat-lam [] []) n =
  return $ kf "got zero clauses in a lambda term"
kompile-fun ty (pat-lam cs []) n = do
  kst ← R.get
  let (rt , ps) = kompile-pi ty $ record defaultPS{ kst = kst }
      rt = validate-ty rt
      rv = PS.ret ps
      ns = showName n
      args = ok ", " ++/ L.map (λ where (v ∈ t ~ _) → validate-ty t ⊕ " " ⊕ v) (PS.ctx ps)
      ret-assrts = list-filter (λ where (mk v _) → v ≈? rv) $ PS.assrts ps
      arg-assrts = list-filter (dec-neg λ where (mk v _) → v ≈? rv) $ PS.assrts ps
      assrt-to-code = ("/* " ++_) ∘ (_++ " */") ∘ Assrt.a
  R.put $ PS.kst ps
  --b ← if does (showName n S.≟ "Example-02.testn") then kompile-cls cs (L.map (λ where (v ∈ _ ~ _) → v) $ PS.ctx ps) rv else (return $ ok "XX")
  b ← kompile-cls cs (L.map (λ where (v ∈ _ ~ _) → v) $ PS.ctx ps) rv
  return $ "// Function " ⊕ ns ⊕ "\n"
         ⊕ rt ⊕ "\n"
         ⊕ nnorm ns ⊕ "(" ⊕ args ⊕ ") {\n"
         ⊕ "\n" ++/ L.map assrt-to-code arg-assrts
         ⊕ rt ⊕ " " ⊕ rv ⊕ ";\n"
         ⊕ b -- function body
         ⊕ "\n" ++/ L.map assrt-to-code ret-assrts
         ⊕ "return " ⊕ rv ⊕ ";\n"
         ⊕ "}\n\n"

kompile-fun _ _ _ =
  return $ kf "expected pattern-matching lambda"

private
  kp : ∀ {X} → String → SPS (Err X)
  kp x = return $ error $ "kompile-pi: " ++ x

  ke : ∀ {X} → String → SPS (Err X)
  ke x = return $ error x

  module P = RawMonadState (StateMonadState PS)

  infixl 10 _p+=c_ _p+=a_
  _p+=c_ : PS → ℕ → PS
  ps p+=c n = record ps{ cnt = PS.cnt ps + n }

  _p+=a_ : PS → Assrt → PS
  ps p+=a a = record ps{ assrts = a ∷ PS.assrts ps }

  ps-fresh : String → SPS String
  ps-fresh x = do
    ps ← P.get
    P.modify (_p+=c 1)
    return $ x ++ showNat (PS.cnt ps)

  lift-ks : ∀ {X} → SKS X → SPS X
  lift-ks xf sps = let (x , sks) = xf (PS.kst sps) in x , record sps {kst = sks}

  sps-kompile-term : Term → SPS Prog
  sps-kompile-term t = do
    ps ← P.get
    lift-ks $ kompile-term t $ (L.map (λ where (v ∈ _ ~ t) → (v , t)) $ PS.ctx ps)

kompile-ty : Type → (pi-ok : Bool) → SPS (Err SacTy)
kompile-ty (Π[ s ∶ arg i x ] y) false = kp "higher-order functions are not supported"
kompile-ty (Π[ s ∶ arg i x ] y) true  = do
    v ← ps-fresh "x_"
    P.modify λ k → record k { cur = v }
    (ok t) ← kompile-ty x false
      where e → return e
    P.modify λ k → record k { cur = PS.ret k  -- In case this is a return type
                            ; ctx = PS.ctx k ++ [ v ∈ ok t ~ arg i x ] }
    kompile-ty y true

kompile-ty (con c args) pi-ok =
  kp $ "don't know how to handle `" ++ showName c ++ "` constructor"
kompile-ty (def (quote ℕ) args) _ = return $ ok int
kompile-ty (def (quote Bool) args) _ = return $ ok bool
kompile-ty (def (quote Float) args) _ = return $ ok float
kompile-ty (def (quote Fin) (arg _ x ∷ [])) _ = do
  ok p ← sps-kompile-term x where error x → ke x
  v ← PS.cur <$> P.get
  P.modify $ _p+=a (mk v $′ "assert (" ++ v ++ " < " ++ p ++ ")")
  return $ ok int

kompile-ty (def (quote L.List) (_ ∷ arg _ ty ∷ _)) _ = do
  el ← ps-fresh "el_"
  v , as ← < PS.cur , PS.assrts > <$> P.get
  -- Any constraints that the subsequent call would
  -- generate will be constraints about the elements
  -- of the list.
  P.modify λ k → record k { cur = el ; assrts = [] }
  ok τ ← kompile-ty ty false where e → return e
  P.modify λ k → record k {
    cur = v;
    assrts = as ++ (L.map {B = Assrt} (λ where (mk _ a) → mk v ("foreach-v " ++ el ++ " in " ++ v ++ ": " ++ a)) $ PS.assrts k)
    -- No need to modify context, as we don't allow higher order functions, so it stays the same.
    }
  return $ ok $ akd nes τ (error "lists do not have static shape") 1

kompile-ty (def (quote V.Vec) (_ ∷ arg _ ty ∷ arg _ n ∷ [])) _ = do
  el ← ps-fresh "el_"
  v , as ← < PS.cur , PS.assrts > <$> P.get
  ok p ← sps-kompile-term n where error x → ke x
  P.modify λ k → record k { cur = el ; assrts = [] }
  ok τ ← kompile-ty ty false where e → return e
  P.modify λ k → record k {
    cur = v;
    assrts = as ++ (L.map {B = Assrt} (λ where (mk _ a) → mk v ("foreach-v " ++ el ++ " in " ++ v ++ ": " ++ a)) $ PS.assrts k)
                ++ [ mk v $′ "assert (shape (" ++ v ++ ")[[0]] == " ++ p ++ ")" ]
    }
  let sh = "[" ⊕ p ⊕ "]"
  case n of λ where
    -- XXX can we possibly miss on any constant expressions?
    (lit (nat n′)) → return $ ok $ aks hom τ sh 1 V.[ n′ ]
    _              → return $ ok $ akd hom τ sh 1

kompile-ty (def (quote Ar) (_ ∷ arg _ el-ty ∷ arg _ dim ∷ arg _ sh ∷ [])) _ = do
  el ← ps-fresh "el_"
  v , as ← < PS.cur , PS.assrts > <$> P.get
  ok d ← sps-kompile-term dim where error x → ke x
  ok s ← sps-kompile-term sh where error x → ke x
  P.modify λ k → record k { cur = el ; assrts = [] }
  ok τ ← kompile-ty el-ty false where e → return e
  P.modify λ k → record k {
    cur = v;
    assrts = as ++ (L.map {B = Assrt} (λ where (mk _ a) → mk v ("foreach-a sh=" ++ s ++ " " ++ el ++ " in " ++ v ++ ": " ++ a)) $ PS.assrts k)
                ++ [ mk v $′ "assert (take (" ++ d ++ ", shape (" ++ v ++ ")) == " ++ s ++ ")" ]
                -- XXX do we want to assert stuff about rank?
    }
  case dim of λ where
    -- XXX can we possibly miss on any constant expressions?
    -- FIXME consider AKS case here!
    (lit (nat d′)) → return $ ok $ akd hom τ (ok s) d′
    _ → return $ ok $ aud hom τ (ok s)

kompile-ty (def (quote Ix) (arg _ dim ∷ arg _ s ∷ [])) _ = do
  v ← PS.cur <$> P.get
  ok d ← sps-kompile-term dim where error x → ke x
  ok s ← sps-kompile-term s where error x → ke x
  P.modify $ _p+=a (mk v $′ "assert (dim (" ++ v ++ ") == " ++ d ++ ")")
           ∘ _p+=a (mk v $′ "assert (" ++ v ++ " < " ++ s ++ ")")

  case dim of λ where
    (lit (nat d′)) → return $ ok $ aks hom int (ok s) 1 V.[ d′ ]
    _              → return $ ok $ akd hom int (ok s) 1

kompile-ty (def (quote _≡_) (_ ∷ arg _ ty ∷ arg _ x ∷ arg _ y ∷ [])) _ = do
  ok x ← sps-kompile-term x where error x → ke x
  ok y ← sps-kompile-term y where error x → ke x
  v ← PS.cur <$> P.get
  P.modify $ _p+=a (mk v $′ "assert (" ++ x ++ " == " ++ y ++ ")")
  return $ ok unit

kompile-ty (def (quote _≥a_) (_ ∷ _ ∷ arg _ x ∷ arg _ y ∷ [])) _ = do
  ok x ← sps-kompile-term x where error x → ke x
  ok y ← sps-kompile-term y where error x → ke x
  v ← PS.cur <$> P.get
  P.modify $ _p+=a (mk v $′ "assert (" ++ x ++ " >= " ++ y ++ ")")
  return $ ok unit

kompile-ty (def (quote _<a_) (_ ∷ _ ∷ arg _ x ∷ arg _ y ∷ [])) _ = do
  ok x ← sps-kompile-term x where error x → ke x
  ok y ← sps-kompile-term y where error x → ke x
  v ← PS.cur <$> P.get
  P.modify $ _p+=a (mk v $′ "assert (" ++ x ++ " < " ++ y ++ ")")
  return $ ok unit

kompile-ty (def (quote Dec) (_ ∷ arg _ p ∷ [])) _ = do
  _ ← kompile-ty p false
  return $ ok bool

kompile-ty (def n _) _ = kp $ "cannot handle `" ++ showName n ++ "` type"

kompile-ty t _ =
  kp $ "failed with the term `" ++ showTerm t ++ "`"

kompile-pi x = kompile-ty x true

-- The names in the telescopes very oftern are not unique, which
-- would be pretty disasterous if the code generation relies on them.
-- see https://github.com/agda/agda/issues/5048 for more details.
--
-- This function simply ensures that variable names are unique in
-- in the telescope.
tel-rename : Telescope → (db : List (String × ℕ)) → Telescope
tel-rename [] db = []
tel-rename ((v , ty) ∷ tel) db with list-find-el ((_≟s v) ∘ proj₁) db
... | just (_ , n) = (v ++ "_" ++ showNat n , ty)
                     ∷ tel-rename tel (list-update-fst ((_≟s v) ∘ proj₁) db (Σ.map₂ suc))
... | nothing      = (v , ty)
                     ∷ tel-rename tel ((v , 1) ∷ db)

private
  kc : String → SKS Prog
  kc x = return $ error $ "kompile-cls: " ++ x

  _>>=e_ : ∀ {a}{X : Set a} → Err X → (X → SKS Prog) → SKS Prog
  (error s) >>=e _ = return $ error s
  (ok x)    >>=e f = f x

  -- sort in increasing order
  list-sort : ∀ {a}{X : Set a} → (acc l : List (X × ℕ)) → List (X × ℕ)
  list-sort acc [] = acc
  list-sort acc (x ∷ l) = list-sort (insert acc x) l
    where
      insert : _ → _ → _
      insert [] y = y ∷ []
      insert (x ∷ xs) y with proj₂ y N.<? proj₂ x
      ... | yes y<x = y ∷ x ∷ xs
      ... | no  y≥x = x ∷ insert xs y

  isperm : ∀ {a}{X : Set a} → (n max : ℕ) → (db : List ℕ) → List (X × ℕ) → Bool
  isperm 0 0   [] [] = true
  isperm n max db [] = does (1 + max N.≟ n) ∧ does (L.length db N.≟ n)
  isperm n max db ((_ , x) ∷ xs) with list-has-el (N._≟ x) db
  ...                      | true = false
  ...                      | false = isperm n (max N.⊔ x) (x ∷ db) xs

  perm : Telescope → List (String × ℕ) → Err (List String)
  perm tel vs with isperm (L.length tel) 0 [] vs
  ... | false = error $ ", " ++/ L.map (λ where (x , y) → "(" ++ x ++ ", " ++ showNat y ++ ")") vs
                     ++ " is not a permutation of the telescope "
                     ++ showTel tel
  ... | true = ok $ L.reverse $ L.map proj₁ $ list-sort [] vs

  module test-perm where
    test₀ : isperm {X = ℕ} 0 0 [] [] ≡ true
    test₀ = refl

    test₁ : isperm 1 0 [] (("" , 0) ∷ []) ≡ true
    test₁ = refl

    test₂′ : isperm 2 0 [] (("" , 1) ∷ ("" , 0) ∷ []) ≡ true
    test₂′ = refl

    test₃ : isperm 3 0 [] (("" , 2) ∷ ("" , 0) ∷ ("" , 1) ∷ []) ≡ true
    test₃ = refl

    test₄ : isperm 4 0 [] (("" , 2) ∷ ("" , 2) ∷ ("" , 1) ∷ ("" , 3) ∷ []) ≡ false
    test₄ = refl

kompile-tel : Telescope → SPS (Err ⊤)
kompile-tel [] = return $ ok tt
kompile-tel ((v , t@(arg i x)) ∷ tel) = do
  --(ok τ) ← kompile-ty x false where (error x) → return $ error x
  P.modify λ k → record k{ ctx = PS.ctx k ++ [ v ∈ error "?" ~ t ] }
  kompile-tel tel

kompile-cls [] ctx ret = kc "zero clauses found"
kompile-cls (clause tel ps t ∷ []) ctx ret =
  -- Make telscope names unique.
  let tel = (tel-rename $! tel) $! [] in
  kompile-clpats tel ps ctx defaultPatSt >>=e λ pst → do
  let (mk vars assgns _ _) = pst --in
  t ← kompile-term t $! tel
  let as = "\n" ++/ assgns
  return $ as ⊕ "\n"
      ⊕ ret ⊕ " = " ⊕ t ⊕ ";\n"

kompile-cls (absurd-clause tel ps ∷ []) ctx ret =
  -- Exactly the same as above
  -- We don't really need to make this call, but we keep it
  -- for sanity checks.  I.e. if we'll get an error in the
  -- patterns, it will bubble up to the caller.
  kompile-clpats ((tel-rename $! tel) $! []) ps ctx defaultPatSt >>=e λ pst → do
  return $ ok "unreachable ();"

kompile-cls (absurd-clause tel ps ∷ ts@(_ ∷ _)) ctx ret =
  kompile-clpats ((tel-rename $! tel) $! []) ps ctx defaultPatSt >>=e λ pst → do
  let (mk vars _ conds _) = pst
      cs = " && " ++/ (if L.length conds N.≡ᵇ 0 then [ "true" ] else conds)
  r ← kompile-cls ts ctx ret
  return $ "if (" ⊕ cs ⊕ ") {\n"
         ⊕ "unreachable();\n"
         ⊕ "} else {\n"
         ⊕ r ⊕ "\n"
         ⊕ "}\n"

kompile-cls (clause tel ps t ∷ ts@(_ ∷ _)) ctx ret =
  kompile-clpats ((tel-rename $! tel) $! []) ps ctx defaultPatSt >>=e λ pst → do
  let (mk vars assgns conds _) = pst
      cs = " && " ++/ (if L.length conds N.≡ᵇ 0 then [ "true" ] else conds)
      as = "\n" ++/ assgns
  t ← kompile-term t $! tel --telv --{!!} --PS.ctx ps
  r ← kompile-cls ts ctx ret
  return $ "if (" ⊕ cs ⊕ ") {\n"
         ⊕ as ⊕ "\n"
         ⊕ ret ⊕ " = " ⊕ t ⊕ ";\n"
         ⊕ "} else {\n"
         ⊕ r ⊕ "\n"
         ⊕ "}\n"

tel-lookup-name : Telescope → ℕ → Prog
tel-lookup-name tel n with n N.<? L.length (reverse tel)
... | yes n<l = ok $ proj₁ $ lookup (reverse tel) $ fromℕ< n<l
... | no _ = error "Variable lookup in telescope failed"

private
  kcp : String → Err PatSt
  kcp x = error $ "kompile-clpats: " ++ x

  infixl 10 _+=c_ _+=a_ _+=v_ _+=n_
  _+=c_ : PatSt → String → PatSt
  p +=c c = record p { conds = PatSt.conds p ++ [ c ] }

  _+=a_ : PatSt → String → PatSt
  p +=a a = record p { assigns = PatSt.assigns p ++ [ a ] }

  _+=v_ : PatSt → String × ℕ → PatSt
  p +=v v = record p { vars = PatSt.vars p ++ [ v ] }

  _+=n_ : PatSt → ℕ → PatSt
  p +=n n = record p { cnt = PatSt.cnt p + 1 }

  pst-fresh : PatSt → String → Err $ String × PatSt
  pst-fresh pst x =
    return $ x ++ showNat (PatSt.cnt pst) , pst +=n 1

kompile-clpats tel (arg i (con (quote true) ps) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel l ctx $ pst +=c (v {- == true -})
kompile-clpats tel (arg i (con (quote false) ps) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel l ctx $ pst +=c ("!" ++ v)

kompile-clpats tel (arg i (con (quote N.zero) ps) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel l ctx $ pst +=c (v ++ " == 0")
kompile-clpats tel (arg i (con (quote N.suc) ps) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel (ps ++ l) ((v ++ " - 1") ∷ ctx) $ pst +=c (v ++ " > 0")

kompile-clpats tel (arg i (con (quote F.zero) ps) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel l ctx $ pst +=c (v ++ " == 0")
kompile-clpats tel (arg i (con (quote F.suc) ps@(_ ∷ _ ∷ [])) ∷ l) (v ∷ ctx) pst = do
  (ub , pst) ← pst-fresh pst "ub_"
  -- XXX here we are not using `ub` in conds.  For two reasons:
  -- 1) as we have assertions, we should check the upper bound on function entry
  -- 2) typically, the value of this argument would be Pat.dot, which we ignore
  --    right now.  It is possible to capture the value of the dot-patterns, as
  --    they carry the value when reconstructed.
  kompile-clpats tel (ps ++ l) (ub ∷ (v ++ " - 1") ∷ ctx) $ pst +=c (v ++ " > 0")

kompile-clpats tel (arg i (con (quote L.List.[]) []) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel l ctx $ pst +=c ("emptyvec_p (" ++ v ++ ")")
kompile-clpats tel (arg i (con (quote L.List._∷_) ps@(_ ∷ _ ∷ [])) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel (ps ++ l) (("hd (" ++ v ++ ")") ∷ ("tl (" ++ v ++ ")") ∷ ctx)
                 $ pst +=c ("nonemptyvec_p (" ++ v ++ ")")

-- Almost the same as List (extra parameter in cons)
kompile-clpats tel (arg i (con (quote V.Vec.[]) []) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel l ctx $ pst +=c ("emptyvec_p (" ++ v ++ ")")
kompile-clpats tel (arg i (con (quote V.Vec._∷_) ps@(_ ∷ _ ∷ _ ∷ [])) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel (ps ++ l) (("len (" ++ v ++ ") - 1") ∷ ("hd (" ++ v ++ ")") ∷ ("tl (" ++ v ++ ")") ∷ ctx)
                 $ pst +=c ("nonemptyvec_p (" ++ v ++ ")")

-- Patterns for Ix constructors
kompile-clpats tel (arg i (con (quote Ix.[]) []) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel l ctx $ pst +=c ("emptyvec_p (" ++ v ++ ")")

kompile-clpats tel (arg i (con (quote Ix._∷_) ps@(d ∷ arg _ (dot s) ∷ arg _ (dot x) ∷ finx ∷ tailix ∷ [])) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel (d ∷ finx ∷ tailix ∷ l) (("len (" ++ v ++ ") - 1") ∷ ("hd (" ++ v ++ ")") ∷ ("tl (" ++ v ++ ")") ∷ ctx)
                 $ pst +=c ("nonemptyvec_p (" ++ v ++ ")")
kompile-clpats tel (arg i (con (quote Ix._∷_) _) ∷ l) (v ∷ ctx) pst =
  kcp $ "matching on `s` and `x` in the Ix._∷_ is not supported, please rewrite the pattern"

kompile-clpats tel (arg _ (con (quote imap) (arg _ (var i) ∷ [])) ∷ l) (v ∷ ctx) pst = do
  (ub , pst) ← pst-fresh pst $ "IMAP_" ++ v ++ "_"
  -- The only thing that `x` could be is a variable, and since
  -- we don't have higher-order functions in sac, we define a local
  -- macro.  Note that we do not pass x further, to avoid assignment.
  kompile-clpats tel l ctx $ pst +=v (ub , i) +=a ("#define " ++ ub ++ "(__x) (" ++ v ++ ")[__x]")

kompile-clpats tel (arg i (con (quote imap) (arg _ (dot _) ∷ [])) ∷ l) (v ∷ ctx) pst =
  -- We simply ignore this inner function entirely.
  kompile-clpats tel l ctx $ pst

kompile-clpats tel (arg i (con (quote imap) (arg _ (absurd _) ∷ [])) ∷ l) (v ∷ ctx) pst =
  kcp "don't know how to handle absurd pattern as an argument to imap"

kompile-clpats tel (arg i (con (quote refl) ps) ∷ l) (v ∷ ctx) pst =
  -- No constraints, as there could only be a single value.
  kompile-clpats tel l ctx pst

kompile-clpats tel (arg i (con (quote _because_) ps) ∷ l) (v ∷ ctx) pst = do
  pf , pst ← pst-fresh pst $ "pf_"
  kompile-clpats tel (ps ++ l) (v ∷ pf ∷ ctx) pst
kompile-clpats tel (arg i (con (quote Reflects.ofʸ) ps) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel (ps ++ l) ("true" ∷ ctx) pst
kompile-clpats tel (arg i (con (quote Reflects.ofⁿ) ps) ∷ l) (v ∷ ctx) pst =
  kompile-clpats tel (ps ++ l) ("false" ∷ ctx) pst

-- End of constructors here.

kompile-clpats tel (arg (arg-info _ r) (var i) ∷ l) (v ∷ vars) pst = do
  -- Note that we do not distinguish between hidden and visible variables
  s ← tel-lookup-name tel i
  let s = nnorm s
  -- If the order of variable binding doesn't match the order
  -- of the variables in the telescope, we have to consider `i` as well.
  -- This changed with https://github.com/agda/agda/issues/5075
  let pst = pst +=v (s , i)
  let pst = if does (s ≈? "_")
            then pst
            else pst +=a (s ++ " = " ++ v ++ ";")
  {-
  -- XXX If I replace the above if with this one, I end up with
  -- the unsolved meta in the test₂ in Example.agda.  Is this a bug?
  let pst = case (s ≈? "_") of λ where
             (yes _) → pst
             (no _)  → pst +=a (s ++ " = " ++ v ++ ";")
  -}
  kompile-clpats tel l vars pst

kompile-clpats tel (arg i (dot t) ∷ l) (v ∷ vars) pst =
  -- For now we just skip dot patterns.
  kompile-clpats tel l vars pst

kompile-clpats tel (arg i (absurd _) ∷ l) (v ∷ ctx) pst =
  -- If have met the absurd pattern, we are done, as
  -- we have accumulated enough conditions to derive
  -- impossibility.  So we are simply done.
  ok pst

kompile-clpats _ [] [] pst = ok pst
kompile-clpats tel ps ctx patst = kcp $ "failed on pattern: ["
                                     ++ (", " ++/ L.map (λ where (arg _ x) → showPattern x) ps)
                                     ++ "], ctx: [" ++ (", " ++/ ctx) ++ "]"

private
  kt : String → SKS Prog
  kt x = return $ error $ "kompile-term: " ++ x

  kt-fresh : String → SKS String
  kt-fresh x = do
    ps ← R.get
    R.modify λ k → record k{ cnt = 1 + KS.cnt k }
    return $ x ++ showNat (KS.cnt ps)

var-lookup : List VarTy → ℕ → SKS Prog
var-lookup []       _       = kt "Variable lookup failed"
var-lookup (v ∈ _ ~ _ ∷ xs) zero    = return $ ok v
var-lookup (x ∷ xs) (suc n) = var-lookup xs n

vty-lookup : List VarTy → ℕ → Err (VarTy)
vty-lookup []       _       = error "Variable lookup failed"
vty-lookup (x ∷ xs) zero    = ok x
vty-lookup (x ∷ xs) (suc n) = vty-lookup xs n

mk-mask : (n : ℕ) → List $ Fin n
mk-mask zero =    []
mk-mask (suc n) = L.reverse $ go n (suc n) N.≤-refl
  where
    sa<b⇒a<b : ∀ a b → suc a N.< b → a N.< b
    sa<b⇒a<b zero    (suc b) _        = s≤s z≤n
    sa<b⇒a<b (suc a) (suc n) (s≤s pf) = s≤s $ sa<b⇒a<b a n pf

    go : (m n : ℕ) → m N.< n → List $ Fin n
    go 0       (suc _) _  = zero ∷ []
    go (suc m) n       pf = F.fromℕ< pf ∷ go m n (sa<b⇒a<b m n pf)

te-to-lvt : Telescope → List VarTy
te-to-lvt tel = L.map (λ where (v , t) → v ∈ error "?" ~ t) tel

-- TODO lift it up
SAC-funs : List (Name × String)
SAC-funs = (quote _+_ , "_add_SxS_")
         ∷ (quote _*_ , "_mul_SxS_")
         ∷ (quote primFloatPlus , "_add_SxS_")
         ∷ (quote primFloatMinus , "_sub_SxS_")
         ∷ (quote primFloatTimes , "_mul_SxS_")
         ∷ (quote primFloatDiv , "_div_SxS_")
         ∷ (quote primFloatExp , "Math::exp")
         ∷ (quote primFloatNegate , "_neg_S_")
         ∷ []

private
  module mask-tests where
    test-mk-mask₁ : mk-mask 0 ≡ []
    test-mk-mask₁ = refl

    test-mk-mask₂ : mk-mask 1 ≡ # 0 ∷ []
    test-mk-mask₂ = refl

    test-mk-mask₃ : mk-mask 2 ≡ # 0 ∷ # 1 ∷ []
    test-mk-mask₃ = refl

kompile-arglist : (n : ℕ) → List $ Arg Term → List $ Fin n → Telescope → SKS Prog
kompile-arglist n args mask varctx with L.length args N.≟ n | V.fromList args
... | yes p | vargs rewrite p = do
                 l ← mapM (λ where (arg _ x) → kompile-term x varctx)
                          $ L.map (V.lookup vargs) mask
                 return $ ok ", " ++/ l
              where open TraversableM (StateMonad KS)

... | no ¬p | _ = kt "Incorrect argument mask"

kompile-term (var x []) vars =
  return $ tel-lookup-name vars x

kompile-term (var x args@(_ ∷ _)) vars = do
  let f = tel-lookup-name vars x
      l = L.length args
  args ← kompile-arglist l args (mk-mask l) vars
  return $ f ⊕ "(" ⊕ args ⊕ ")"

kompile-term (lit l@(float _)) vars = return $ showLiteral l ⊕ "f"
kompile-term (lit l) vars = return $ ok $ showLiteral l

kompile-term (con (quote N.zero) _) _ =
  return $ ok "0"
kompile-term (con (quote N.suc) args) vars = do
  args ← kompile-arglist 1 args [ # 0 ] vars
  return $ "(1 + " ⊕ args ⊕ ")"

kompile-term (con (quote Fin.zero) _) _ =
  return $ ok "0"
kompile-term (con (quote Fin.suc) args) vars = do
  args ← kompile-arglist 2 args [ # 1 ] vars
  return $ "(1 + " ⊕ args ⊕ ")"

kompile-term (con (quote L.List.[]) (_ ∷ (arg _ ty) ∷ [])) vars = do
  -- We want to call kompile-ty, and we need a context that "should"
  -- contain vars with their types.  But, we never actually access these
  -- types in the context, we only refer to variables, therefore the
  -- following hack is justified.
  kst ← R.get
  let ctx = L.map (λ where (v , t) → v ∈ error "?" ~ t) $ vars
      (rt , ps) = kompile-ty ty false $ record defaultPS{ kst = kst; ctx = ctx }
      in-sh = sacty-shape =<< rt
  --R.put (PS.kst ps)
  return $ "empty (" ⊕ in-sh ⊕ ")" --ok "[]"

kompile-term (con (quote L.List._∷_) args) vars = do
  args ← kompile-arglist 4 args (# 2 ∷ # 3 ∷ []) vars
  return $ "cons (" ⊕ args ⊕ ")"

-- Almost the same as List
kompile-term (con (quote V.Vec.[]) (_ ∷ (arg _ ty) ∷ [])) vars = do
  kst ← R.get
  let ctx = L.map (λ where (v , t) → v ∈ error "?" ~ t) $ vars
      (rt , ps) = kompile-ty ty false $ record defaultPS{ kst = kst; ctx = ctx }
      in-sh = sacty-shape =<< rt
  R.put (PS.kst ps)
  return $ "empty (" ⊕ in-sh ⊕ ")"

kompile-term (con (quote V.Vec._∷_) args) vars = do
  args ← kompile-arglist 5 args (# 3 ∷ # 4 ∷ []) vars
  return $ "cons (" ⊕ args ⊕ ")"

-- Ix constructors
kompile-term (con (quote Ix.[]) []) vars =
  return $ ok "[]"

kompile-term (con (quote Ix._∷_) args) vars = do
  args ← kompile-arglist 5 args (# 3 ∷ # 4 ∷ []) vars
  return $ "cons (" ⊕ args ⊕ ")"

kompile-term (con (quote refl) _) _ =
  return $ ok "tt"

-- Imaps with explicit lambdas
kompile-term (con (quote Array.Base.imap) (_ ∷ arg _ ty ∷ arg _ d ∷ X@(arg _ s) ∷ arg _ (vLam x e) ∷ [])) vars = do
  kst ← R.get
  let ctx = L.map (λ where (v , t) → v ∈ error "?" ~ t) $ vars
      (rt , ps) = kompile-ty ty false $ record defaultPS{ kst = kst; ctx = ctx }
      in-sh = sacty-shape =<< rt
      bt = bt <$> rt
  R.put (PS.kst ps)
  iv ← kt-fresh "iv_"
  let iv-type = vArg (def (quote Ix) ((vArg d) ∷ vArg s ∷ []))
  s ← kompile-term s vars
  b ← kompile-term e $! vars ++ [ (iv , iv-type) ]
  return $! "with { (. <= " ⊕ iv ⊕ " <= .): " ⊕ b ⊕ "; }: genarray (" ⊕ s ⊕ ", zero_" ⊕ bt ⊕ " (" ⊕ in-sh ⊕ "))"

-- Imaps with an expression
kompile-term (con (quote Array.Base.imap) (_ ∷ arg _ ty ∷ _ ∷ arg _ s ∷ arg _ e ∷ [])) vars = do
  kst ← R.get
  let ctx = L.map (λ where (v , t) → v ∈ error "?" ~ t) $ vars
      (rt , ps) = kompile-ty ty false $ record defaultPS{ kst = kst; ctx = ctx }
      in-sh = sacty-shape =<< rt
      bt = bt <$> rt
  R.put (PS.kst ps)
  iv ← kt-fresh "iv_"
  s ← kompile-term s vars
  b ← kompile-term e $ vars
  return $ "with { (. <= " ⊕ iv ⊕ " <= .): " ⊕ b ⊕ " (" ⊕ iv ⊕ "); }: genarray (" ⊕ s ⊕ ", zero_" ⊕ bt ⊕ " (" ⊕ in-sh ⊕ "))"

kompile-term (con c _) vars  = kt $ "don't know constructor " ++ (showName c)

-- Definitions

-- From Agda.Builtin.Nat: div-helper k m n j = k + (n + m - j) div (1 + m)
kompile-term (def (quote div-helper) (arg _ k ∷ arg _ m ∷ arg _ n ∷ arg _ j ∷ [])) vars = do
  k ← kompile-term k vars
  m ← kompile-term m vars
  n ← kompile-term n vars
  j ← kompile-term j vars
  return $ "_div_SxS_ (" ⊕ k ⊕ " + (" ⊕ n ⊕ " + " ⊕ m ⊕ " - " ⊕ j ⊕ "), 1 + " ⊕ m ⊕ ")"

kompile-term (def (quote N._≟_) (arg _ a ∷ arg _ b ∷ [])) vars = do
  a ← kompile-term a vars
  b ← kompile-term b vars
  return $ a ⊕ " == " ⊕  b

kompile-term (def (quote V._++_) args) vars = do
  args ← kompile-arglist 6 args (# 4 ∷ # 5 ∷ []) vars
  return $ "concat (" ⊕ args ⊕ ")"

kompile-term (def (quote V.tabulate) (_ ∷ arg _ ty ∷ X@(arg _ l) ∷ arg _ (vLam x e) ∷ [])) vars = do
  kst ← R.get
  let ctx = te-to-lvt vars --L.map (λ where (v , t) → v ∈ error "?" ~ t) $ TelView.tel vars
      (rt , ps) = kompile-ty ty false $ record defaultPS{ kst = kst; ctx = ctx }
      in-sh = sacty-shape =<< rt
      bt = bt <$> rt
  R.put (PS.kst ps)
  iv ← kt-fresh "iv_"
  let iv-type = vArg (def (quote Fin) (vArg l ∷ []))
  l ← kompile-term l vars
  b ← kompile-term e $ vars ++ [(iv , iv-type)]
  return $ "with { (. <= " ⊕ iv ⊕ " <= .): " ⊕ b ⊕ "; }: genarray ([" ⊕ l ⊕ "], zero_" ⊕ bt ⊕ " (" ⊕ in-sh ⊕ "))"

kompile-term (def (quote ix-tabulate) (arg _ d ∷ X ∷ arg _ (vLam x e) ∷ [])) vars = do
  iv ← kt-fresh "iv_"
  let iv-type = vArg (def (quote Fin) (vArg d ∷ []))
  d ← kompile-term d vars
  b ← kompile-term e $ vars ++ [(iv , iv-type)]
  return $ "with { (. <= " ⊕ iv ⊕ " <= .): " ⊕ b ⊕ "; }: genarray ([" ⊕ d ⊕ "], 0)"

-- Array stuff
kompile-term (def (quote sel) (_ ∷ _ ∷ _ ∷ _ ∷ arg _ a ∷ arg _ iv ∷ [])) vars = do
  a ← kompile-term a vars
  iv ← kompile-term iv vars
  return $ a ⊕ "[" ⊕ iv ⊕ "]"

kompile-term (def (quote ix-lookup) (_ ∷ _ ∷ arg _ iv ∷ arg _ el ∷ [])) vars = do
  iv ← kompile-term iv vars
  el ← kompile-term el vars
  return $ iv ⊕ "[" ⊕ el ⊕ "]"

kompile-term (def (quote V.lookup) (_ ∷ _ ∷ _ ∷ arg _ v ∷ arg _ i ∷ [])) vars = do
  v ← kompile-term v vars
  i ← kompile-term i vars
  return $ v ⊕ "[" ⊕ i ⊕ "]"

kompile-term (def (quote V.foldr) (_ ∷ _ ∷ ty₁ ∷ arg _ (vLam _ ty₂) ∷ arg _ len ∷ arg _ (hLam _ (def f args)) ∷ arg _ neut ∷ arg _ arr ∷ [])) vars = do
  let f = case list-find-el ((RN._≟ f) ∘ proj₁) SAC-funs of λ where
            (just (_ , f)) → f
            _ → nnorm $ showName f
  len ← kompile-term len vars
  neut ← kompile-term neut vars
  arr ← kompile-term arr vars
  iv ← kt-fresh "iv_"
  return $ "with { ([0] <= " ⊕ iv ⊕ " < [" ⊕ len ⊕ "]): " ⊕ arr ⊕ "[" ⊕ iv ⊕ "]; }: fold (" ⊕ f ⊕ ", " ⊕ neut ⊕ ")"

kompile-term (def (quote reduce-1d) (_ ∷ _ ∷ arg _ s ∷ arg _ (def f args) ∷ arg _ ε ∷ arg _ a ∷ [])) vars = do
  let f = case list-find-el ((RN._≟ f) ∘ proj₁) SAC-funs of λ where
            (just (_ , f)) → f
            _ → nnorm $ showName f
  ε ← kompile-term ε vars
  a ← kompile-term a vars
  s ← kompile-term s vars
  iv ← kt-fresh "iv_"
  return $ "with { ([0] <= " ⊕ iv ⊕ " < " ⊕ s ⊕ "): " ⊕ a ⊕ "[" ⊕ iv ⊕ "]; }: fold (" ⊕ f ⊕ ", " ⊕ ε ⊕ ")"

kompile-term (def (quote reduce-1d) (Xa@(arg _ X) ∷ Ya@(arg _ Y) ∷ arg _ s ∷ arg _ L@(vLam a (vLam b e)) ∷ arg _ ε ∷ arg _ arr ∷ [])) vars = do
  a ← kt-fresh "a"
  b ← kt-fresh "b"

  kst ← R.get
  let (Xs , ps) = kompile-ty X false $ record defaultPS{ kst = kst; ctx = te-to-lvt vars }
      (Ys , ps) = kompile-ty Y false $ record ps { ctx = PS.ctx ps ++ [ a ∈ Xs ~ Xa ] }
  R.put $ PS.kst ps
  t ← kompile-term e $ vars ++ (a , Xa) ∷ (b , Ya) ∷ [] -- (PS.ctx ps ++ [ b ∈ Ys ~ Ya ])

  kst ← R.get
  fname ← kt-fresh "lifted_"
  let e , ps = kompile-ctx vars $ record defaultPS{ kst = kst }
      vs     = L.map {B = String × Prog} (λ where (v ∈ τ ~ _) → (v , (sacty-to-string <$> τ))) $′ PS.ctx ps
      vs     = vs ++ ((a , (sacty-to-string <$> Xs)) ∷ (b , (sacty-to-string <$> Ys)) ∷ [])
      vs     = ok ", " ++/ L.map (λ where (v , τ) → τ ⊕ " " ⊕ v) vs
      fun    = (sacty-to-string <$> Ys) ⊕ " " ⊕ fname ⊕ "(" ⊕ vs ⊕ ") "
             ⊕ "{ return " ⊕ t ⊕ "; }"

  -- error out in case our current context was broken
  (ok _) ← return e where (error x) → return (error x)

  --R.modify $! λ k → record k{ defs = (KS.defs k ⊕_) $! fun }
  kst ← R.get
  R.put $! record kst{ defs = KS.defs kst ⊕ fun }

  let part-app = fname ⊕ "(" ⊕ ", " ++/ L.map proj₁ vars ⊕ ")"
  ε ← kompile-term ε vars
  arr ← kompile-term arr vars
  s ← kompile-term s vars
  iv ← kt-fresh "iv_"
  return $! "with { ([0] <= " ⊕ iv ⊕ " < " ⊕ s ⊕ "): " ⊕ arr ⊕ "[" ⊕ iv ⊕ "]; }: fold (" ⊕ part-app ⊕ ", " ⊕ ε ⊕ ")"

  where
    kompile-ctx : Telescope → SPS (Err ⊤)
    kompile-ctx [] = return $ ok tt
    kompile-ctx ((v , t@(arg i x)) ∷ ctx) = do
      (ok τ) ← kompile-ty x false where (error x) → return $ error x
      P.modify λ k → record k{ ctx = PS.ctx k ++ [ v ∈ ok τ ~ t ] }
      kompile-ctx ctx

-- A bunch of functions that are mapped to id in sac
-- XXX get rid of id call, only keeping for debugging purposes.
kompile-term (def (quote F.fromℕ<) args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 3 args (# 0 ∷ []) vars
kompile-term (def (quote F.toℕ)    args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 2 args (# 1 ∷ []) vars
kompile-term (def (quote subst-ar) args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 7 args (# 6 ∷ []) vars
kompile-term (def (quote subst-ix) args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 5 args (# 4 ∷ []) vars
kompile-term (def (quote ▾_)       args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 6 args (# 5 ∷ []) vars
kompile-term (def (quote ▴_)       args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 6 args (# 5 ∷ []) vars
kompile-term (def (quote a→ix)     args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 4 args (# 1 ∷ []) vars
kompile-term (def (quote a→s)      args) vars = ("id (" ⊕_) ∘ (_⊕ ")") <$> kompile-arglist 2 args (# 1 ∷ []) vars

kompile-term (def (quote Array.Base.magic-fin) args) vars = return $ ok "unreachable ()"

kompile-term (def (quote Array.Base.off→idx) args) vars = do
  args ← kompile-arglist 3 args (# 1 ∷ # 2 ∷ []) vars
  return $ "off_to_idx (" ⊕ args ⊕ ")"
kompile-term (def (quote _↑_) args) vars = do
  args ← kompile-arglist 7 args (# 4 ∷ # 5 ∷ []) vars
  return $ "take (" ⊕ args ⊕ ")"
kompile-term (def (quote _↓_) args) vars = do
  args ← kompile-arglist 7 args (# 4 ∷ # 5 ∷ []) vars
  return $ "drop (" ⊕ args ⊕ ")"

kompile-term (def (quote _↑⟨_⟩_) args) vars = do
  args ← kompile-arglist 7 args (# 4 ∷ # 5 ∷ # 6 ∷ []) vars
  return $ "overtake (" ⊕ args ⊕ ")"
kompile-term (def (quote _-↑⟨_⟩_) args) vars = do
  args ← kompile-arglist 7 args (# 4 ∷ # 5 ∷ # 6 ∷ []) vars
  return $ "overtake_back (" ⊕ args ⊕ ")"

-- The last pattern in the list of `def` matches
kompile-term (def n []) _ =
  kt $ "attempting to compile `" ++ showName n ++ "` as function with 0 arguments"

kompile-term (def n args@(_ ∷ _)) vars with list-find-el ((RN._≟ n) ∘ proj₁) SAC-funs
... | just (_ , f) = do
  let l = L.length args
  args ← kompile-arglist l args (mk-mask l) vars
  return $ f ⊕ " (" ⊕ args ⊕ ")"

... | nothing  = do
  R.modify λ k → record k { funs = KS.funs k ++ [ n ] }
  let n = nnorm $ showName n
      l = L.length args
  args ← kompile-arglist l args (mk-mask l) vars
  return $ n ⊕ " (" ⊕ args ⊕ ")"

kompile-term t vctx = kt $ "failed to compile term `" ++ showTerm t ++ "`"

ext: agda

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by strict partial orders
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Properties.StrictPartialOrder
       {s₁ s₂ s₃} (SPO : StrictPartialOrder s₁ s₂ s₃) where

open Relation.Binary.StrictPartialOrder SPO
  renaming (trans to <-trans)
import Relation.Binary.StrictToNonStrict as Conv
open Conv _≈_ _<_

------------------------------------------------------------------------
-- Strict partial orders can be converted to posets

poset : Poset _ _ _
poset = record
  { isPartialOrder = record
    { isPreorder = record
        { isEquivalence = isEquivalence
        ; reflexive     = reflexive
        ; trans         = trans isEquivalence <-resp-≈ <-trans
        }
    ; antisym = antisym isEquivalence <-trans irrefl
    }
  }

open Poset poset public


text:
module Function.DomainRaise where

open import Data
open import Data.Boolean
import      Functional as Fn
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Syntax.Number
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T X Y Z : Type{ℓ}
private variable n : ℕ

-- Repeated function type like an n-ary operator.
-- Examples:
--   (a →̂ b)(0) = (b)
--   (a →̂ b)(1) = (a → b)
--   (a →̂ b)(2) = (a → a → b)
--   (a →̂ b)(3) = (a → a → a → b)
--   (a →̂ b)(4) = (a → a → a → a → b)
_→̂_ : Type{ℓ₁} → Type{ℓ₂} → (n : ℕ) → Type{if positive?(n) then (ℓ₁ Lvl.⊔ ℓ₂) else ℓ₂} -- TODO: Is the level thing really working?
(A →̂ B)(𝟎)       = B
(A →̂ B)(𝐒(𝟎))    = A → B
(A →̂ B)(𝐒(𝐒(n))) = A → (A →̂ B)(𝐒(n))

open import Data.Tuple
open import Data.Tuple.Raise

apply₁ : let _ = n in X → (X →̂  Y)(𝐒(n)) → (X →̂  Y)(n)
apply₁ {𝟎}   = Fn.apply
apply₁ {𝐒 _} = Fn.apply

apply₊ : let _ = n in (X ^ n) → (X →̂  Y)(n) → Y
apply₊ {𝟎}       <>        f = f
apply₊ {𝐒(𝟎)}    x         f = f(x)
apply₊ {𝐒(𝐒(n))} (x , xs)  f = apply₊ {𝐒(n)} xs (f(x))

-- Applies the same argument on all arguments.
-- Examples:
--   f : (a →̂ b)(5)
--   applyRepeated{0} f(x) = f
--   applyRepeated{1} f(x) = f(x)
--   applyRepeated{2} f(x) = f(x)(x)
--   applyRepeated{3} f(x) = f(x)(x)(x)
--   applyRepeated{2}(applyRepeated{3} f(x)) (y) = f(x)(x)(y)(y)(y)
applyRepeated : let _ = n in (X →̂ Y)(n) → (X → Y)
applyRepeated{𝟎}       f(x) = f
applyRepeated{𝐒(𝟎)}    f(x) = f(x)
applyRepeated{𝐒(𝐒(n))} f(x) = applyRepeated{𝐒(n)} (f(x)) (x)

{-
  -- Applies arguments from a function.
  -- Almost (not really) like a composition operation.
  -- Examples:
  --   f : (a →̂ b)(3)
  --   applyFn f g = f (g(2)) (g(1)) (g(0))
  applyFn : ∀{n}{T₁}{T₂} → (T₁ →̂ T₂)(n) → (𝕟(n) → T₁) → T₂
  applyFn{𝟎}    f g = f
  applyFn{𝐒(n)} f g = applyFn{n} (f(g(ℕ-to-𝕟 (n) {𝐒(n)} ⦃ [<?]-𝐒 {n} ⦄))) (g ∘ (bound-𝐒{n}))

  -- TODO: Examples:
  --   swapReverse {3} f (y₂) (y₁) (y₀)
  --   = swapReverse {2} (f(y₂)) (y₁) (y₀)
  --   = swapReverse {1} (f(y₂) (y₁)) (y₀)
  --   = swapReverse {0} (f(y₂) (y₁) (y₀))
  --   = f(y₂) (y₁) (y₀)
  -- swapReverse : ∀{n}{T₁}{T₂} → (T₁ →̂ T₂)(n) → (T₁ →̂ T₂)(n)
  -- swapReverse {𝟎}    y₀   = y₀
  -- swapReverse {𝐒(n)} f(yₙ) = (swapReverse {n} f) ∘ (f(yₙ))

  -- directOp : ∀{n}{X}{Y} → ((X → Y) →̂ ((X ^ n) → (Y ^ n)))(n)
-}

-- Function composition on a multi-argument function (Like PrimitiveRecursion.Composition).
-- Examples:
--   (f ∘₄ g) x₁ x₂ x₃ x₄
--   = (f ∘₃ g x₁) x₂ x₃ x₄
--   = (f ∘₂ g x₁ x₂) x₃ x₄
--   = (f ∘₁ g x₁ x₂ x₃) x₄
--   = (f ∘ g x₁ x₂ x₃) x₄
--   = f(g x₁ x₂ x₃ x₄)
_∘_ : let _ = n ; _ = X ; _ = Y ; _ = Z in (Y → Z) → (X →̂ Y)(n) → (X →̂ Z)(n)
_∘_ {𝟎}       = Fn.id
_∘_ {𝐒(𝟎)}    = Fn._∘_
_∘_ {𝐒(𝐒(n))} = Fn._∘_ Fn.∘ (_∘_) -- (f ∘ₙ₊₂ g)(x) = f ∘ₙ₊₁ g(x)

_∘[_]_ : let _ = X ; _ = Y ; _ = Z in (Y → Z) → (n : ℕ) → (X →̂ Y)(n) → (X →̂ Z)(n)
f ∘[ n ] g = _∘_ {n = n} f g

_∘₀_ = _∘_ {0}
_∘₁_ = _∘_ {1}
_∘₂_ = _∘_ {2}
_∘₃_ = _∘_ {3}
_∘₄_ = _∘_ {4}
_∘₅_ = _∘_ {5}
_∘₆_ = _∘_ {6}
_∘₇_ = _∘_ {7}
_∘₈_ = _∘_ {8}
_∘₉_ = _∘_ {9}

-- TODO: Flip the arguments and make n explicit
-- Single function composition on every argument.
-- (f on g)(y₁)(y₂).. = g (f(y₁)) (f(y₂)) ..
-- Examples:
--   _on_ {3} f g (y₂) (y₁) (y₀)
--   = _on_ {2} f (g (f(y₂))) (y₁) (y₀)
--   = _on_ {1} f (g (f(y₂)) (f(y₁))) (y₀)
--   = _on_ {0} f (g (f(y₂)) (f(y₁)) (f(y₀)))
--   = g (f(y₂)) (f(y₁)) (f(y₀))
on : let _ = n ; _ = X ; _ = Y ; _ = Z in (Y →̂ Z)(n) → (X → Y) → (X →̂ Z)(n)
on {n = 𝟎}               = Fn.const
on {n = 𝐒(𝟎)}            = Fn._∘_
on {n = 𝐒(𝐒(n))} f g(yₙ) = on {n = 𝐒(n)} (f(g(yₙ))) g

-- applyOnFn : ∀{n}{X}{Y} → (Y →̂ Y)(n) → ((X → Y) →̂ (X → Y))(n)
-- applyOnFn

-- Constructs a left-associated n-ary operator from a binary operator.
-- Example:
--   naryₗ{3} (_▫_) x₁ x₂ x₃ x₄ x₅
--   = ((naryₗ{2} (_▫_)) Fn.∘ (x₁ ▫_)) x₂ x₃ x₄
--   = (naryₗ{2} (_▫_) (x₁ ▫ x₂)) x₃ x₄ x₅
--   = ((naryₗ{1} (_▫_)) Fn.∘ ((x₁ ▫ x₂) ▫_)) x₃ x₄ x₅
--   = (naryₗ{1} (_▫_) ((x₁ ▫ x₂) ▫ x₃)) x₄ x₅
--   = ((naryₗ{0} (_▫_)) Fn.∘ (((x₁ ▫ x₂) ▫ x₃) ▫_)) x₃ x₄ x₅
--   = (naryₗ{0} (_▫_) (((x₁ ▫ x₂) ▫ x₃) ▫ x₄)) x₅
--   = ((_▫_) (((x₁ ▫ x₂) ▫ x₃) ▫ x₄)) x₅
--   = ((((x₁ ▫ x₂) ▫ x₃) ▫ x₄) ▫_) x₅
--   = (((x₁ ▫ x₂) ▫ x₃) ▫ x₄) x₅
naryₗ : (n : ℕ) → (X → X → X) → (X →̂ X)(𝐒(𝐒(n)))
naryₗ(𝟎)    (_▫_)   = (_▫_)
naryₗ(𝐒(n)) (_▫_) x = (naryₗ(n) (_▫_)) Fn.∘ (x ▫_)

-- Constructs a right-associated n-ary operator from a binary operator.
-- Example:
--   naryᵣ{3} (_▫_) x₁ x₂ x₃ x₄ x₅
--   = ((x₁ ▫_) ∘[ 4 ] (naryᵣ{2} (_▫_))) x₂ x₃ x₄ x₅
--   = x₁ ▫ (naryᵣ{2} (_▫_) x₂ x₃ x₄ x₅)
--   = x₁ ▫ (((x₂ ▫_) ∘[ 3 ] (naryᵣ{1} (_▫_))) x₃ x₄ x₅)
--   = x₁ ▫ (x₂ ▫ (naryᵣ{1} (_▫_) x₃ x₄ x₅))
--   = x₁ ▫ (x₂ ▫ (((x₃ ▫_) ∘[ 2 ] (naryᵣ{0} (_▫_))) x₄ x₅))
--   = x₁ ▫ (x₂ ▫ (x₃ ▫ (naryᵣ{0} (_▫_) x₄ x₅)))
--   = x₁ ▫ (x₂ ▫ (x₃ ▫ ((_▫_) x₄ x₅)))
--   = x₁ ▫ (x₂ ▫ (x₃ ▫ (x₄ ▫ x₅)))
naryᵣ : (n : ℕ) → (X → X → X) → (X →̂ X)(𝐒(𝐒(n)))
naryᵣ(𝟎)    (_▫_)   = (_▫_)
naryᵣ(𝐒(n)) (_▫_) x = (x ▫_) ∘[ 𝐒(𝐒(n)) ] (naryᵣ(n) (_▫_))

{-
[→̂]-to-[⇉] : (n : ℕ) → ∀{X : Type{ℓ₁}}{Y : Type{ℓ₂}} → (X →̂ Y)(n) → (RaiseType.repeat(n) X ⇉ Y)
[→̂]-to-[⇉] 0         f = f
[→̂]-to-[⇉] 1         f = f
[→̂]-to-[⇉] (𝐒(𝐒(n))) f = [→̂]-to-[⇉] (𝐒(n)) ∘ f
-}


text:
data Unit : Set where
  tt : Unit

f : Unit

mutual
  f = tt

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --exact-split --rewriting #-}

module index where

-- An organised list of modules:
import Pi.Everything

-- An exhaustive list of all modules:


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Transitivity

module Oscar.Class.Transassociativity where

module Transassociativity
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ) (let infix 4 _∼̇_ ; _∼̇_ = _∼̇_)
  (transitivity : Transitivity.type _∼_) (let infixr 9 _∙_ ; _∙_ : FlipTransitivity.type _∼_; _∙_ g f = transitivity f g)
  = ℭLASS (λ {x y} → _∼̇_ {x} {y} , (λ {x y z} → transitivity {x} {y} {z}))
          (∀ {w x y z} (f : w ∼ x) (g : x ∼ y) (h : y ∼ z) → (h ∙ g) ∙ f ∼̇ h ∙ g ∙ f)

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  {ℓ} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ}
  {transitivity : Transitivity.type _∼_}
  where
  transassociativity = Transassociativity.method _∼_ _∼̇_ transitivity
  syntax transassociativity f g h = h ⟨∙ g ⟨∙ f

module Transassociativity!
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ)
  ⦃ _ : Transitivity.class _∼_ ⦄
  = Transassociativity (_∼_) (_∼̇_) transitivity

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ)
  ⦃ _ : Transitivity.class _∼_ ⦄
  where
  transassociativity![_] = Transassociativity.method _∼_ _∼̇_ transitivity


text:
{-# OPTIONS --universe-polymorphism #-}
-- {-# OPTIONS --verbose tc.records.ifs:15 #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}
-- {-# OPTIONS --verbose cta.record.ifs:15 #-}
-- {-# OPTIONS --verbose tc.section.apply:25 #-}
-- {-# OPTIONS --verbose tc.mod.apply:100 #-}
-- {-# OPTIONS --verbose scope.rec:15 #-}
-- {-# OPTIONS --verbose tc.rec.def:15 #-}

module 07-subclasses where

open import Data.Bool hiding (_≟_)
open import Data.Nat hiding (_<_)
open import Relation.Nullary.Decidable
open import Function using (_$_; id)

record Eq (A : Set) : Set where
  field eq : A → A → Bool

primEqBool : Bool → Bool → Bool
primEqBool true = id
primEqBool false = not

eqBool : Eq Bool
eqBool = record { eq = primEqBool }

primEqNat : ℕ → ℕ → Bool
primEqNat a b = ⌊ a ≟ b ⌋

primLtNat : ℕ → ℕ → Bool
primLtNat 0 _ = true
primLtNat (suc a) (suc b) = primLtNat a b
primLtNat _ _ = false

neq : {t : Set} → {{eqT : Eq t}} → t → t → Bool
neq a b = not $ eq a b
  where open Eq {{...}}

record Ord₁ (A : Set) : Set where
  field _<_ : A → A → Bool
        eqA : Eq A

ord₁Nat : Ord₁ ℕ
ord₁Nat = record { _<_ = primLtNat; eqA = eqNat }
  where eqNat : Eq ℕ
        eqNat = record { eq = primEqNat }

record Ord₂ {A : Set} (eqA : Eq A) : Set where
  field _<_ : A → A → Bool

ord₂Nat : Ord₂ (record { eq = primEqNat })
ord₂Nat = record { _<_ = primLtNat }

record Ord₃ (A : Set) : Set where
  field _<_ : A → A → Bool
        eqA : Eq A
  open Eq eqA public

ord₃Nat : Ord₃ ℕ
ord₃Nat = record { _<_ = primLtNat; eqA = eqNat }
  where eqNat : Eq ℕ
        eqNat = record { eq = primEqNat }

record Ord₄ {A : Set} (eqA : Eq A) : Set where
  field _<_ : A → A → Bool
  open Eq eqA public

ord₄Nat : Ord₄ (record { eq = primEqNat })
ord₄Nat = record { _<_ = primLtNat }

module test₁ where
  open Ord₁ {{...}}
  open Eq {{...}}

  eqNat = eqA

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq true false
  test₄ : {A : Set} → {{ ordA : Ord₁ A }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b
    where eqA' = eqA

module test₂ where
  open Ord₂ {{...}}
  open Eq {{...}}

  eqNat : Eq ℕ
  eqNat = record { eq = primEqNat }

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq true false
  test₄ : {A : Set} → {eqA : Eq A} → {{ ordA : Ord₂ eqA }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b

module test₃ where
  open Ord₃ {{...}}
  open Eq {{...}} renaming (eq to eq')

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq' true false
  test₄ : {A : Set} → {{ ordA : Ord₃ A }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b

module test₄ where
  open Ord₄ {{...}}
  open Eq {{...}} renaming (eq to eq')

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq' true false
  test₄ : {A : Set} → {eqA : Eq A} → {{ ordA : Ord₄ eqA }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b

module test₄′ where
  open Ord₄ {{...}} hiding (eq)
  open Eq {{...}}

  eqNat : Eq ℕ
  eqNat = record { eq = primEqNat }

  test₁ = 5 < 3
  test₂ = eq 5 3
  test₃ = eq true false
  test₄ : {A : Set} → {eqA : Eq A} → {{ ordA : Ord₄ eqA }} → A → A → Bool
  test₄ a b = a < b ∨ eq a b

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
module QualifiedConstructors where

data Nat₁ : Set where
  zero : Nat₁
  suc  : Nat₁ → Nat₁

data Nat₂ : Set where
  zero : Nat₂
  suc  : Nat₂ → Nat₂

zero₁ = Nat₁.zero
one₂  = Nat₂.suc Nat₂.zero

record Suc : Set where
  constructor suc
  field n : Nat₁

one₃ = Suc.suc zero₁

pred : Suc → Nat₁
pred s = Suc.n s

conv : Nat₂ → Nat₁
conv Nat₂.zero    = Nat₁.zero
conv (Nat₂.suc n) = Nat₁.suc (conv n)

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

inj : (n m : Nat₁) → Nat₁.suc n ≡ suc m → n ≡ m
inj .m m refl = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Weight biased leftist heap that proves rank invariant and uses   --
-- a single-pass merging algorithm.                                 --
----------------------------------------------------------------------

module SinglePassMerge.RankProof where

open import Basics
-- We import rank proofs conducted earlier - they will be re-used.
open import TwoPassMerge.RankProof
            using    ( makeT-lemma )
            renaming ( proof-1 to proof-1a; proof-2 to proof-2a )

data Heap : Nat → Set where
  empty : Heap zero
  node  : Priority → {l r : Nat} → l ≥ r → Heap l → Heap r → Heap (suc (l + r))

-- Note [Privoving rank invariant in single-pass merge]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- Recall that in TwoPassMerge.RankProof we need to prove that:
--
--  1) makeT constructs node of correct size. There were two cases:
--
--     a) constructing a node without swapping l and r subtrees passed
--        to makeT. No extra proof was required as everything followed
--        from definitions.
--
--     b) constructing a node by swapping l and r subtrees (when rank
--        of r was greater than rank of l). We had to prove that:
--
--                    suc (a + b) ≡ suc (b + a)
--
--        This proof is supplied by a function makeT-lemma.
--
--  2) resulting heap produced by merge has correct size. Merge has 4
--     cases (see [Two-pass merging algorithm]):
--
--     a) h1 is empty. No extra proof required (everything follows
--        from definition of +). See [merge, proof 0a].
--
--     b) h2 is empty. We had to prove that:
--
--                 h1 ≡ h1 + 0
--
--        This proof is supplied by +0 (in Basics.Reasoning) and is
--        inlined in the definition of merge. See [merge, proof 0b].
--
--     c) priority p1 is higher than p2. We had to prove:
--
--            suc (l1 + (r1 + suc (l2 + r2)))
--                           ≡ suc ((l1 + r1) + suc (l2 + r2))
--
--        This proof is supplied by proof-1 (renamed to proof-1a in
--        this module). See [merge, proof 1] for details.
--
--     d) priority p2 is higher than p1. We had to prove:
--
--            suc (l2 + (r2  + suc (l1 + r1)))
--                           ≡ suc ((l1 + r1) + suc (l2 + r2))
--
--        This proof is supplied by proof-2 (renamed to proof-2a in
--        this module). See [merge, proof 2] for details.
--
-- Now that we inline makeT into merge and we will have to construct
-- new proofs of merge that take into account the fact that makeT has
-- been inlinined. Let's take a detailed look into the problem and
-- analyze possible solutions.
--
-- First of all let us note that we only made calls to makeT in
-- inductive cases of merge (points 2c and 2d above). This means that
-- implementation of base cases of merge (2a and 2b above) remains
-- unchanged. Let's take a look at proofs we need to supply for each
-- of four inductive cases of merge (see [Single-pass merging
-- algorithm] for description of each case):
--
--   1) case c described in [Single-pass merging algorithm]. Call to
--      makeT would not swap left and right when creating a node from
--      parameters passed to it. Required proof is:
--
--            suc (l1 + (r1 + suc (l2 + r2)))
--                           ≡ suc ((l1 + r1) + suc (l2 + r2))
--
--   2) case d described in [Single-pass merging algorithm]. Call to
--      makeT would swap left and right when creating a node from
--      parameters passed to it. Required proof is:
--
--            suc ((r1 + suc (l2 + r2)) + l1)
--                           ≡ suc ((l1 + r1) + suc (l2 + r2))
--
--   3) case e described in [Single-pass merging algorithm]. Call to
--      makeT would not swap left and right when creating a node from
--      parameters passed to it. Required proof is:
--
--            suc (l2 + (r2  + suc (l1 + r1)))
--                           ≡ suc ((l1 + r1) + suc (l2 + r2))
--
--   4) case f described in [Single-pass merging algorithm]. Call to
--      makeT would swap left and right when creating a node from
--      parameters passed to it. Required proof is:
--
--            suc ((r2 + suc (l1 + r1)) + l2)
--                           ≡ suc ((l1 + r1) + suc (l2 + r2))
--
-- First of all we must note that proofs required in cases 1 and 3 are
-- exactly the same as in the two-pass merging algorithm. This allows
-- us to re-use the old proofs (renamed to proof-1a and proof-2a
-- here). What about proofs of cases 2 and 4? One thing we could do is
-- construct proofs of these properties using technique described in
-- Note [Constructing equality proofs using transitivity]. This is
-- left as an exercise to the reader. Here we will proceed in a
-- different way. Notice that properties we have to prove in cases for
-- 2 and 4 are very similar to properties 1 and 3 (we omit the RHS
-- since it is always the same):
--
--  1: suc (l1 + (r1 + suc (l2 + r2)))
--  2: suc ((r1 + suc (l2 + r2)) + l1)
--
--  3: suc (l2 + (r2  + suc (l1 + r1)))
--  4: suc ((r2 + suc (l1 + r1)) + l2)
--
-- The only difference between 1 and 2 and between 3 and 4 is the
-- order of parameters inside outer suc. This is expected: in cases 2
-- and 4 we swap left and right subtree passed to node and this is
-- reflected in the types. Now, if we could prove that:
--
--            suc ((r1 + suc (l2 + r2)) + l1)
--                           ≡ suc (l1 + (r1 + suc (l2 + r2)))
--
-- and
--
--            suc ((r2 + suc (l1 + r1)) + l2)
--                           ≡ suc (l2 + (r2  + suc (l1 + r1)))
--
-- then we could use transitivity to combine these new proofs with old
-- proof-1a and proof-2a. If we abstract the parameters in the above
-- equalities we see that the property we need to prove is:
--
--                    suc (a + b) ≡ suc (b + a)
--
-- And that happens to be makeT-lemma! New version of merge was
-- created by inlining calls to make and now it turns out we can
-- construct proofs of that implementation by using proofs of
-- makeT. This leads us to very elegant solutions presented below.

proof-1b : (l1 r1 l2 r2 : Nat) → suc ((r1 + suc (l2 + r2)) + l1)
                               ≡ suc ((l1 + r1) + suc (l2 + r2))
proof-1b l1 r1 l2 r2 = trans (makeT-lemma (r1 + suc (l2 + r2)) l1)
                             (proof-1a l1 r1 l2 r2)

proof-2b : (l1 r1 l2 r2 : Nat) → suc ((r2 + suc (l1 + r1)) + l2)
                               ≡ suc ((l1 + r1) + suc (l2 + r2))
proof-2b l1 r1 l2 r2 = trans (makeT-lemma (r2 + suc (l1 + r1)) l2)
                             (proof-2a l1 r1 l2 r2)

-- We can now use proof-1a, proof-1b, proof-2a and proof-2b in
-- definition of merge.
merge : {l r : Nat} → Heap l → Heap r → Heap (l + r)
merge {zero} {_}     empty h2 = h2
merge {suc l} {zero} h1 empty = subst Heap (sym (+0 (suc l))) h1
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node p1 {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node p2 {l2-rank} {r2-rank} l2≥r2 l2 r2)
  with p1 < p2
  | order l1-rank (r1-rank + suc (l2-rank + r2-rank))
  | order l2-rank (r2-rank + suc (l1-rank + r1-rank))
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node p1 {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node p2 {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | true
  | ge l1≥r1+h2
  | _
  = subst Heap
          (proof-1a l1-rank r1-rank l2-rank r2-rank)
          (node p1 l1≥r1+h2 l1 (merge r1 (node p2 l2≥r2 l2 r2)))
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node p1 {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node p2 {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | true
  | le l1≤r1+h2
  | _
  = subst Heap
          (proof-1b l1-rank r1-rank l2-rank r2-rank)
          (node p1 l1≤r1+h2 (merge r1 (node p2 l2≥r2 l2 r2)) l1)
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node p1 {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node p2 {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | false
  | _
  | ge l2≥r2+h1
  = subst Heap
          (proof-2a l1-rank r1-rank l2-rank r2-rank)
          (node p2 l2≥r2+h1 l2 (merge r2 (node p1 l1≥r1 l1 r1)))
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node p1 {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node p2 {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | false
  | _
  | le l2≤r2+h1
  = subst Heap
          (proof-2b l1-rank r1-rank l2-rank r2-rank)
          (node p2 l2≤r2+h1 (merge r2 (node p1 l1≥r1 l1 r1)) l2)

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
{-# OPTIONS --without-K --safe --overlapping-instances #-}
module Examples where

open import Data.Nat

-- local imports
open import Interpreter

pf : y' ∈ y' ::: `ℕ , (x' ::: `ℕ , ·)
pf = H

pf2 : x' ∈ y' ::: `ℕ , (x' ::: `ℕ , ·)
pf2 = TH

testSimpleLambda : · ⊢ `ℕ
testSimpleLambda = (`λ x' `: `ℕ ⇨ (`v x' `+ `v x')) `₋ `n 10

testSimpleLambda2 : · ⊢ `ℕ `⇨ `ℕ
testSimpleLambda2 = `λ x' `: `ℕ ⇨ (`v x') `+ (`v x')

testNestedLambda : · ⊢ `ℕ
testNestedLambda = (`λ x' `: `ℕ ⇨ (`λ_`:_⇨_ y' `ℕ (`v x' `* `v y'))) `₋ `n 10  `₋ `n 15

testNestedLambda2 : · ⊢  `ℕ `⇨ `ℕ `⇨ `ℕ
testNestedLambda2 = (`λ x' `: `ℕ ⇨ (`λ_`:_⇨_ y' `ℕ (`v x' `* `v y')))

-- The following definitions do not type check. They are a relic from
-- when the interpreter still had some bugs. Uncomment them to verify
-- they don't type check
-- testNamingNotWorking : · ⊢ `Bool
-- testNamingNotWorking = (`λ x' `: `Bool ⇨ (`λ x' `: `⊤ ⇨ `v x')) `₋ `true `₋ `tt

-- testNamingNotWorking2 : · ⊢ `Bool `⇨ `⊤ `⇨ `Bool -- incorrect type!
-- testNamingNotWorking2 = `λ x' `: `Bool ⇨ (`λ x' `: `⊤ ⇨ `v x')

testNamingWorking : · ⊢ `⊤
testNamingWorking = (`λ x' `: `Bool ⇨ (`λ x' `: `⊤ ⇨ `v x')) `₋ `true `₋ `tt

testNamingWorking2 : · ⊢ `Bool `⇨ `⊤ `⇨ `⊤
testNamingWorking2 = `λ x' `: `Bool ⇨ (`λ x' `: `⊤ ⇨ `v x')

testSum1 : · ⊢ `ℕ
testSum1 = `let z' `= `case `left (`n 10) `of
                              `λ z' `: `ℕ ⇨ `v z'
                           || `λ x' `: `Bool ⇨ `if `v x' `then `n 1 `else `n 0
           `in `v z'

testSum2 : · ⊢ `ℕ
testSum2 = `let z' `= `case `right `true `of
                              `λ z' `: `ℕ ⇨ `v z'
                           || `λ x' `: `Bool ⇨ `if `v x' `then `n 1 `else `n 0
           `in `v z'

testProduct1 : · ⊢ `Bool
testProduct1 = `fst (`true `, (`n 10 `, `tt ))

testProduct2 : · ⊢ `ℕ `× `⊤
testProduct2 = `snd (`true `, (`n 10 `, `tt ))

testDeMorganFullOr : · ⊢ `Bool
testDeMorganFullOr = `let z' `= `λ x' `: `Bool ⇨ `λ y' `: `Bool ⇨ `¬ (`v x' `∨ `v y')
                     `in `v z' `₋ `true `₋ `true

testDeMorganBrokenAnd : · ⊢ `Bool
testDeMorganBrokenAnd = `let z' `= `λ x' `: `Bool ⇨ `λ y' `: `Bool ⇨ `¬ `v x' `∧ `¬ `v y'
                        `in `v z' `₋ `true `₋ `true

tester : Set
tester = {! interpret testSimpleLambda2 !}

max_stars_repo_name: sseefried/well-typed-agda-interpreter

max_issues_repo_name: sseefried/well-typed-agda-interpreter

max_forks_repo_name: sseefried/well-typed-agda-interpreter


text:
module Data.Bin.Rec where

open import Data.Bin hiding (suc; fromℕ)
open import Induction.WellFounded

open import Data.Nat using (ℕ; zero; suc) renaming (_<_ to _ℕ<_)
open import Data.Nat.Properties

open import Relation.Binary.PropositionalEquality
open import Data.Bin.Bijection

import Induction.Nat

wf : Well-founded _<_
wf x = go' x where
  P : ℕ → Set
  P x = Acc _<_ (fromℕ x)

  podgon : ∀ {y} → P (toℕ y) → Acc _<_ y
  podgon = subst (λ q → Acc _<_ q) (fromToℕ-inverse _)

  go'' : (x : ℕ) → ((y : ℕ) → y ℕ< x → P y) → P x
  go'' x rec = acc (λ { y (less ty<tfx) → podgon (rec (toℕ y) (subst (λ q → toℕ y ℕ< q) (toFromℕ-inverse x) ty<tfx ) )})

  go : (x : ℕ) → P x
  go = Induction.Nat.<-rec P go''

  go' : (x : Bin) → Acc _<_ x
  go' x = podgon (go (toℕ x))

open All wf

rec : ∀ (P : Bin → Set) → ((a : Bin) → ((a' : Bin) → (a' < a) → P a') → P a) → (a : Bin) → P a
rec P f = wfRec _ P f

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core lemmas needed to make list argmin/max functions work
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary using (Trans; TotalOrder; Setoid)

module Data.List.Extrema.Core
  {b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where

open import Algebra.Core
open import Algebra.Definitions
import Algebra.Construct.NaturalChoice.Min as Min
import Algebra.Construct.NaturalChoice.Max as Max
open import Data.Product using (_×_; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_)

open import Algebra.Construct.LiftedChoice

open TotalOrder totalOrder renaming (Carrier to B)
open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
  using (_<_; <-≤-trans; ≤-<-trans)

------------------------------------------------------------------------
-- Setup

-- open NonStrictToStrict totalOrder using (_<_; ≤-<-trans; <-≤-trans)

open Max totalOrder
open Min totalOrder

private

  variable
    a : Level
    A : Set a

  <-transʳ : Trans _≤_ _<_ _<_
  <-transʳ = ≤-<-trans trans antisym ≤-respˡ-≈

  <-transˡ : Trans _<_ _≤_ _<_
  <-transˡ = <-≤-trans Eq.sym trans antisym ≤-respʳ-≈

  module _ (f : A → B) where

    lemma₁ : ∀ {x y v} → f x ≤ v → f x ⊓ f y ≈ f y → f y ≤ v
    lemma₁ fx≤v fx⊓fy≈fy = trans (x⊓y≈y⇒y≤x fx⊓fy≈fy) fx≤v

    lemma₂ : ∀ {x y v} → f y ≤ v → f x ⊓ f y ≈ f x → f x ≤ v
    lemma₂ fy≤v fx⊓fy≈fx = trans (x⊓y≈x⇒x≤y fx⊓fy≈fx) fy≤v

    lemma₃ : ∀ {x y v} → f x < v → f x ⊓ f y ≈ f y → f y < v
    lemma₃ fx<v fx⊓fy≈fy = <-transʳ (x⊓y≈y⇒y≤x fx⊓fy≈fy) fx<v

    lemma₄ : ∀ {x y v} → f y < v → f x ⊓ f y ≈ f x → f x < v
    lemma₄ fx<v fx⊓fy≈fy = <-transʳ (x⊓y≈x⇒x≤y fx⊓fy≈fy) fx<v

------------------------------------------------------------------------
-- Definition of lifted max and min

⊓ᴸ : (A → B) → Op₂ A
⊓ᴸ = Lift _≈_ _⊓_ ⊓-sel

⊔ᴸ : (A → B) → Op₂ A
⊔ᴸ = Lift _≈_ _⊔_ ⊔-sel

------------------------------------------------------------------------
-- Properties of ⊓ᴸ

⊓ᴸ-sel : ∀ f → Selective {A = A} _≡_ (⊓ᴸ f)
⊓ᴸ-sel f = sel-≡ ⊓-isSelectiveMagma f

⊓ᴸ-presᵒ-≤v : ∀ f {v} (x y : A) → f x ≤ v ⊎ f y ≤ v → f (⊓ᴸ f x y) ≤ v
⊓ᴸ-presᵒ-≤v f = preservesᵒ ⊓-isSelectiveMagma f (lemma₁ f) (lemma₂ f)

⊓ᴸ-presᵒ-<v : ∀ f {v} (x y : A) → f x < v ⊎ f y < v → f (⊓ᴸ f x y) < v
⊓ᴸ-presᵒ-<v f = preservesᵒ ⊓-isSelectiveMagma f (lemma₃ f) (lemma₄ f)

⊓ᴸ-presᵇ-v≤ : ∀ f {v} {x y : A} → v ≤ f x → v ≤ f y → v ≤ f (⊓ᴸ f x y)
⊓ᴸ-presᵇ-v≤ f {v} = preservesᵇ ⊓-isSelectiveMagma {P = λ x → v ≤ f x} f

⊓ᴸ-presᵇ-v< : ∀ f {v} {x y : A} → v < f x → v < f y → v < f (⊓ᴸ f x y)
⊓ᴸ-presᵇ-v< f {v} = preservesᵇ ⊓-isSelectiveMagma {P = λ x → v < f x} f

⊓ᴸ-forcesᵇ-v≤ : ∀ f {v} (x y : A) → v ≤ f (⊓ᴸ f x y) → v ≤ f x × v ≤ f y
⊓ᴸ-forcesᵇ-v≤ f {v} = forcesᵇ ⊓-isSelectiveMagma f
  (λ v≤fx fx⊓fy≈fx → trans v≤fx (x⊓y≈x⇒x≤y fx⊓fy≈fx))
  (λ v≤fy fx⊓fy≈fy → trans v≤fy (x⊓y≈y⇒y≤x fx⊓fy≈fy))

------------------------------------------------------------------------
-- Properties of ⊔ᴸ

⊔ᴸ-sel : ∀ f → Selective {A = A} _≡_ (⊔ᴸ f)
⊔ᴸ-sel f = sel-≡ ⊔-isSelectiveMagma f

⊔ᴸ-presᵒ-v≤ : ∀ f {v} (x y : A) → v ≤ f x ⊎ v ≤ f y → v ≤ f (⊔ᴸ f x y)
⊔ᴸ-presᵒ-v≤ f {v} = preservesᵒ ⊔-isSelectiveMagma f
  (λ v≤fx fx⊔fy≈fy → trans v≤fx (x⊔y≈y⇒x≤y fx⊔fy≈fy))
  (λ v≤fy fx⊔fy≈fx → trans v≤fy (x⊔y≈x⇒y≤x fx⊔fy≈fx))

⊔ᴸ-presᵒ-v< : ∀ f {v} (x y : A) → v < f x ⊎ v < f y → v < f (⊔ᴸ f x y)
⊔ᴸ-presᵒ-v< f {v} = preservesᵒ ⊔-isSelectiveMagma f
  (λ v<fx fx⊔fy≈fy → <-transˡ v<fx (x⊔y≈y⇒x≤y fx⊔fy≈fy))
  (λ v<fy fx⊔fy≈fx → <-transˡ v<fy (x⊔y≈x⇒y≤x fx⊔fy≈fx))

⊔ᴸ-presᵇ-≤v : ∀ f {v} {x y : A} → f x ≤ v → f y ≤ v → f (⊔ᴸ f x y) ≤ v
⊔ᴸ-presᵇ-≤v f {v} = preservesᵇ ⊔-isSelectiveMagma {P = λ x → f x ≤ v} f

⊔ᴸ-presᵇ-<v : ∀ f {v} {x y : A} → f x < v → f y < v → f (⊔ᴸ f x y) < v
⊔ᴸ-presᵇ-<v f {v} = preservesᵇ ⊔-isSelectiveMagma {P = λ x → f x < v} f

⊔ᴸ-forcesᵇ-≤v : ∀ f {v} (x y : A) → f (⊔ᴸ f x y) ≤ v → f x ≤ v × f y ≤ v
⊔ᴸ-forcesᵇ-≤v f {v} = forcesᵇ ⊔-isSelectiveMagma f
  (λ fx≤v fx⊔fy≈fx → trans (x⊔y≈x⇒y≤x fx⊔fy≈fx) fx≤v)
  (λ fy≤v fx⊔fy≈fy → trans (x⊔y≈y⇒x≤y fx⊔fy≈fy) fy≤v)


text:
{-# OPTIONS -W error #-}
module Issue2596a where

{-# REWRITE #-}

-- We will never encounter this, because the harmless warning above
-- has been turned into an error
f : Set
f = f


text:
module Issue450 where

open import Common.Level
open import Common.Coinduction

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

data Wrap (A : Set) : Set where
  con : A -> Wrap A

out : forall {A} -> Wrap A -> A
out (con x) = x

out' : forall {A} -> ∞ (Wrap A) -> A
out' y = out (♭ y)

inn : forall {A}  -> A -> ∞ (Wrap A)
inn y = ♯ (con y)

prf : (A : Set)(x : A) → out' (inn x) ≡ x
prf A x = refl

test : forall {A : Set}{x : A} -> out (con x) ≡ x
test = refl

-- these work
test1 : forall {A}{x : A} -> out' (inn x) ≡ x
test1 {A} {x} = test

test2 : forall {A}{x : A} -> out' (inn x) ≡ x
test2 {A} {x} = test {A}

-- but the following ones won't typecheck

test3 : forall {A}{x : A} -> out' (inn x) ≡ x
test3 {A} {x} = test {A} {x}

test4 : forall {A}{x : A} -> out' (inn x) ≡ x
test4 {A} {x} = refl


text:
-- Andreas, 2017-09-09, re issue #2732
-- eta-contraction needed in termination checker

-- {-# OPTIONS -v term:30 #-}

open import Agda.Builtin.Equality

data O (A : Set) : Set where
  leaf : O A
  node : (A → O A) → O A

postulate
  A : Set
  a : A

test1 : (t u : O A) → O A
test1 leaf     leaf     = leaf
test1 leaf     (node g) = test1 leaf (g a)
test1 (node f) leaf     = test1 (f a) (node f)
test1 (node f) (node g) = test1 (node λ x → f x) (g a)
-- Should pass even with the eta-expansion.

data Q (A : Set) : Set where
  leaf : Q A
  node : (f g : A → Q A) (p : f ≡ g) → Q A

-- Having various call arguments in eta-expanded form.
test : (t u : Q A) → Q A
test leaf leaf = leaf
test leaf (node f g p) = test leaf (f a)
test (node f g p) leaf = test (g a) (node f g p)
test (node f .f refl) (node g g' p) = test (node (λ x → f x) _ refl) (g' a)


text:
-- Andreas, 2017-10-11, issue #2796

-- A failed check for projection-likeness
-- made the overloaded projection not resolve.

-- {-# OPTIONS -v tc.proj.like:100 #-}
-- {-# OPTIONS -v tc.proj.amb:100 #-}

postulate
  L     : Set
  lzero : L
  Type  : L → Set
  El    : ∀{l} → Type l → Set

record Pred (A : Set) l : Set where  -- Works without l
  field
    app : A → Type l

record Sub l : Set1 where
  field
    Carrier : Set
    pred    : Pred Carrier l
  open Pred pred public

open Pred   -- Works without this (of course)
open Sub

test : (S T : Sub lzero) → (f : S .Carrier → T .Carrier) → Set
test S T f = (a : S .Carrier) → El (S .app a) → El (T .app (f a))

-- Problem WAS:
-- Cannot resolve overloaded projection app because no matching candidate found
-- when checking that the expression S .app a has type
-- Type (_l_22 S T f a)

-- Should succeed.


text:
-- Andreas, 2012-01-13, error reported by Rob Simmons
module Issue555 where

data Exp : Set
data Exp Γ where -- internal error


text:
open import Oscar.Prelude
open import Oscar.Data.𝟘

module Oscar.Data.Decidable where

data Decidable {a} (A : Ø a) : Ø a where
  ↑_ : A → Decidable A
  ↓_ : ¬ A → Decidable A


text:
open import Relation.Binary hiding (_⇒_)

module Category.Monad.Monotone.Error {i}(pre : Preorder i i i)(Exc : Set i) where

open Preorder pre renaming (Carrier to I; _∼_ to _≤_; refl to ≤-refl)

open import Function
open import Level hiding (lift)
open import Data.Sum

open import Relation.Unary
open import Relation.Unary.Monotone pre
open import Relation.Unary.PredicateTransformer

open import Category.Monad.Monotone pre
open import Category.Monad.Monotone.Identity pre

pattern left x = inj₁ x
pattern right x = inj₂ x

ErrorT : Pt I i → Pt I i
ErrorT M P = M (λ i → Exc ⊎ P i)

Error = ErrorT Identity

record ErrorMonad (M : Pt I i) : Set (suc i) where
  field
    throw : ∀ {P i} → Exc → M P i
    try_catch_ : ∀ {P}   → M P ⊆ ((const Exc ↗ M P) ⇒ M P)

module _ {M} ⦃ Mon : RawMPMonad M ⦄ where
  private module M = RawMPMonad Mon

  open RawMPMonad
  errorT-monad : RawMPMonad (ErrorT M)
  return errorT-monad px = M.return (right px)
  _≥=_ errorT-monad {P}{Q} px f = px M.≥= λ where
      _ (left e)  → M.return (left e)
      w (right x) → f w x

  open ErrorMonad
  errorT-monad-ops : ErrorMonad (ErrorT M)
  throw errorT-monad-ops e = M.return (left e)
  try_catch_ errorT-monad-ops c f = c M.≥= λ where
    w (left e)  → f w e
    w (right x) → M.return (right x)

  lift-error : ∀ {P} → M P ⊆ ErrorT M P
  lift-error x = x M.>>= (λ z → M.return (right z))

module Instances where
  -- Defining instances for the transformer
  -- leads to divergence of instance search,
  -- because M is on the outside.
  instance
    open RawMPMonad
    error-monad : RawMPMonad Error
    error-monad = errorT-monad

    open ErrorMonad
    error-monad-ops : ErrorMonad Error
    error-monad-ops = errorT-monad-ops


text:
{-# OPTIONS --cubical-compatible --sized-types #-}
------------------------------------------------------------------------
-- From the Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------

module Common.Size where

open import Agda.Builtin.Size public


text:
{-# OPTIONS --experimental-irrelevance #-}

-- Andreas, 2015-05-18  Irrelevant module parameters
-- should not be resurrected in module body.

postulate
  A : Set

module M .(a : A) where

  bad : (..(_ : A) -> Set) -> Set
  bad f = f a
    -- SHOULD FAIL: variable a is declared irrelevant,
    -- so it cannot be used here.

-- This fails of course:
-- fail : .(a : A) -> (..(_ : A) -> Set) -> Set
-- fail a f = f a


text:
module Capability where

open import Relation.Nullary
     using (yes; no)

open import Data.List
     using (List; []; [_]; _∷_; _++_)

open import Data.String
     using (String; _≟_)

open import Relation.Binary.PropositionalEquality
     using (_≢_; refl; _≡_)

-- Local modules ---------------------------------------------------------------

open import Common
     using (Id)

-- Capabilities Definition -----------------------------------------------------

infix  50 `_
infixr 15 _∙_

data Capability : Set where
  `_   : Id → Capability                          -- Name
  In   : Id → Capability                          -- Can enter
  Out  : Id → Capability                          -- Can exit
  Open : Id → Capability                          -- Can open
  ε    : Capability                               -- Null
  _∙_  : Capability → Capability → Capability     -- Path

-- Free variable ---------------------------------------------------------------

freeVar : Capability -> List Id
freeVar (` a)    = [ a ]
freeVar (a ∙ b)  = (freeVar a) ++ (freeVar b)
freeVar _        = []

-- Capability substitution -----------------------------------------------------

_[_/_] : Capability -> Id -> Capability -> Capability

` x [ y / M ] with x ≟ y
... | yes _       = M
... | no _        = ` x
(N ∙ R) [ y / M ] = N [ y / M ] ∙ R [ y / M ]
C [ _ / _ ]       = C

module Test where
  a = "a"
  b = "b"

  ------------------------------------------------------------------------------

  _ : freeVar (` a) ≡ [ a ]
  _ = refl

  _ : freeVar (` a ∙ ` b) ≡ a ∷ b ∷ []
  _ = refl

  ------------------------------------------------------------------------------

  _ : ∀ {M} → ` a [ a / M ] ≡ M
  _ = refl

  _ : ∀ {M} → ` b [ a / M ] ≡ ` b
  _ = refl

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity

module HoTT.Transport.Identity where

open variables

unitₗᵣ : {x y : A} {p : x == y} → p == refl ∙ p ∙ refl
unitₗᵣ {p = refl} = refl

-- Theorem 2.11.3
transport= : {a a' : A} (f g : A → B) (p : a == a') (q : f a == g a) →
             transport (λ x → f x == g x) p q == ap f p ⁻¹ ∙ q ∙ ap g p
transport= _ _ refl _ = unitₗᵣ

transport=-id-const : (a : A) {x₁ x₂ : A} (p : x₁ == x₂) (q : x₁ == a) →
                      transport (λ x → x == a) p q == p ⁻¹ ∙ q
transport=-id-const _ refl refl = refl

transport=-const-id : {x₁ x₂ : A} (p : x₁ == x₂) (a : A) (q : a == x₁) →
                      transport (λ x → a == x) p q == q ∙ p
transport=-const-id refl _ refl = refl

transport=-id-id : {x₁ x₂ : A} (p : x₁ == x₂) (q : x₁ == x₁) →
                   transport (λ x → x == x) p q == p ⁻¹ ∙ q ∙ p
transport=-id-id refl _ = unitₗᵣ

transport=-constₗ : (b : B) (f : A → B) {x₁ x₂ : A} (p : x₁ == x₂) (q : b == f x₁) →
                    transport (λ x → b == f x) p q == q ∙ ap f p
transport=-constₗ _ _ refl _ = unitᵣ

transport=-constᵣ : (f : A → B) (b : B) {x₁ x₂ : A} (p : x₁ == x₂) (q : f x₁ == b) →
                    transport (λ x → f x == b) p q == ap f p ⁻¹ ∙ q
transport=-constᵣ _ _ refl refl = refl

transport=-idₗ : (f : A → A) {x₁ x₂ : A} (p : x₁ == x₂) (q : x₁ == f x₁) →
                 transport (λ x → x == f x) p q == p ⁻¹ ∙ q ∙ ap f p
transport=-idₗ _ refl _ = unitₗᵣ

transport=-idᵣ : (f : A → A) {x₁ x₂ : A} (p : x₁ == x₂) (q : f x₁ == x₁) →
                 transport (λ x → f x == x) p q == ap f p ⁻¹ ∙ q ∙ p
transport=-idᵣ _ refl _ = unitₗᵣ

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by bounded meet semilattices
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary.Lattice

module Relation.Binary.Properties.BoundedMeetSemilattice
  {c ℓ₁ ℓ₂} (M : BoundedMeetSemilattice c ℓ₁ ℓ₂) where

open BoundedMeetSemilattice M

import Algebra.FunctionProperties as P; open P _≈_
open import Data.Product
open import Function using (_∘_; flip)
open import Relation.Binary
open import Relation.Binary.Properties.Poset poset
import Relation.Binary.Properties.BoundedJoinSemilattice as J

-- The dual construction is a bounded join semilattice.

dualIsBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ (flip _≤_) _∧_ ⊤
dualIsBoundedJoinSemilattice = record
  { isJoinSemilattice = record
    { isPartialOrder  = invIsPartialOrder
    ; supremum        = infimum
    }
  ; minimum           = maximum
  }

dualBoundedJoinSemilattice : BoundedJoinSemilattice c ℓ₁ ℓ₂
dualBoundedJoinSemilattice = record
  { ⊥                        = ⊤
  ; isBoundedJoinSemilattice = dualIsBoundedJoinSemilattice
  }

open J dualBoundedJoinSemilattice
  hiding (dualIsBoundedMeetSemilattice; dualBoundedMeetSemilattice) public


text:
-- Andreas, 2018-04-16, issue #3033, reported by Christian Sattler

-- The DotPatternCtx was not used inside dot patterns in ConcreteToAbstract.

postulate
  A : Set
  B : Set
  a : A
  f : A → B

data C : B → Set where
  c : C (f a)

foo : (b : B) → C b → Set
foo .{!f a!} c = A  -- give "f a" here

-- WAS: foo .f a c = A
-- NOW: foo .(f a) c = A


text:
module Tactic.Monoid where

open import Prelude
open import Tactic.Reflection
open import Tactic.Reflection.Quote

open import Tactic.Monoid.Exp
open import Tactic.Monoid.Reflect
open import Tactic.Monoid.Proofs

monoidTactic : ∀ {a} {A : Set a} {{_ : Monoid/Laws A}} → Tactic
monoidTactic {A = A} {{laws}} hole = do
  goal   ← inferNormalisedType hole
  `A     ← quoteTC A
  unify goal (def (quote _≡_) (hArg unknown ∷ hArg `A ∷ vArg unknown ∷ vArg unknown ∷ []))
    <|> do typeErrorFmt "Goal is not an equality: %t" goal
  goal   ← normalise goal
  ensureNoMetas goal
  match  ← monoidMatcher (Monoid/Laws.super laws)
  `dict  ← quoteTC (Monoid/Laws.super laws)
  `laws  ← quoteTC laws
  ensureNoMetas `dict
  debugPrintFmt "tactic.monoid" 20 "monoidTactic %t, dict = %t" goal `dict
  (lhs , rhs) , env ← parseGoal match goal
  unify hole (def (quote proof) (iArg `dict ∷ iArg `laws ∷ vArg (` lhs) ∷ vArg (` rhs) ∷
                                 vArg (quoteEnv `dict env) ∷ vArg (con (quote refl) []) ∷ []))
    <|> do typeErrorFmt "Can't prove %t == %t because %t /= %t"
                        (` lhs) (` rhs) (` (flatten lhs)) (` (flatten rhs))

macro
  auto-monoid : ∀ {a} {A : Set a} {{Laws : Monoid/Laws A}} → Tactic
  auto-monoid {{Laws}} = monoidTactic {{Laws}}

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module MetaId where

  data Nat : Set where
    zero : Nat
    suc  : Nat -> Nat

  expr = (\ (a : Set) (x : a) -> x) _ zero

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module MoreLogic.Definitions where -- hProp logic

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) renaming (⊥ to ⊥⊥) -- `⊥` and `elim`

import Cubical.Data.Empty as Empty
open import Cubical.Data.Unit.Base

open import MoreLogic.Reasoning
open import Utils

-- lifted versions of ⊥ and ⊤

hPropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
hPropRel A B ℓ' = A → B → hProp ℓ'

isSetIsProp : ∀{ℓ} {A : Type ℓ} → isProp (isSet A)
isSetIsProp is-set₀ is-set₁ = funExt (λ x → funExt λ y → isPropIsProp (is-set₀ x y) (is-set₁ x y))

isSetᵖ : ∀{ℓ} (A : Type ℓ) → hProp ℓ
isSetᵖ A = isSet A , isSetIsProp

-- hProp-syntax for Σ types of hProps to omit propositional truncation
-- this should be equivalent to ∃! from the standard library but ∃! is not an hProp
-- proof sketch:
--   `∃! A B = isContr (Σ A B) = Σ[ x ∈ Σ A B ] ∀(  y : Σ A B) → x ≡ y`
--   `Σᵖ[]-syntax A B          ≈ Σ[ c ∈ Σ A B ] ∀(x y : Σ A B) → x ≡ y`
-- NOTE: we also have isProp→Iso in `Cubical.Foundations.Isomorphism`

Σᵖ[]-syntax : ∀{ℓ ℓ'} → {A : hProp ℓ'} → ([ A ] → hProp ℓ) → hProp _
Σᵖ[]-syntax {A = A} P = Σ [ A ] ([_] ∘ P) , isPropΣ (isProp[] A) (isProp[] ∘ P)

syntax  Σᵖ[]-syntax (λ x → P) = Σᵖ[ x ] P
infix 2 Σᵖ[]-syntax

Σᵖ[∶]-syntax : ∀{ℓ ℓ'} → {A : hProp ℓ'} → ([ A ] → hProp ℓ) → hProp _
Σᵖ[∶]-syntax {A = A} P = Σ [ A ] ([_] ∘ P) , isPropΣ (isProp[] A) (isProp[] ∘ P)

syntax  Σᵖ[∶]-syntax {A = A} (λ x → P) = Σᵖ[ x ∶ A ] P
infix 2 Σᵖ[∶]-syntax

isProp⊎ˡ : ∀{ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → (A → ¬ᵗ B) → isProp (A ⊎ B)
isProp⊎ˡ pA pB A⇒¬B (inl x) (inl y) = cong inl (pA x y)
isProp⊎ˡ pA pB A⇒¬B (inr x) (inr y) = cong inr (pB x y)
isProp⊎ˡ pA pB A⇒¬B (inl x) (inr y) = ⊥-elim (A⇒¬B x y)
isProp⊎ˡ pA pB A⇒¬B (inr x) (inl y) = ⊥-elim (A⇒¬B y x)

-- hProp-syntax for disjoint unions to omit propositional truncation
⊎ᵖ-syntax : ∀{ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → {[ P ] → ¬ᵗ [ Q ]} → hProp _
⊎ᵖ-syntax P Q {P⇒¬Q} = ([ P ] ⊎ [ Q ]) , isProp⊎ˡ (isProp[] P) (isProp[] Q) P⇒¬Q

syntax ⊎ᵖ-syntax P Q {P⇒¬Q} = [ P⇒¬Q ] P ⊎ᵖ Q

{-# DISPLAY ⊎ᵖ-syntax a b = a ⊎ b #-}

-- hProp-syntax for equality on sets to omit propositional truncation
≡ˢ-syntax : {ℓ : Level} {A : Type ℓ} → A → A → {isset : isSet A} → hProp ℓ
≡ˢ-syntax a b {isset} = (a ≡ b) , isset a b

syntax ≡ˢ-syntax a b {isset} = [ isset ] a ≡ˢ b

infix 1 ⊎ᵖ-syntax
infix 1 ≡ˢ-syntax

{-# DISPLAY ≡ˢ-syntax a b = a ≡ b #-}

-- pretty print ∀-syntax from cubical standard library
{-# DISPLAY ∀[]-syntax {A = A} P = P #-}
-- {-# DISPLAY ∀[]-syntax {A = A} P = ∃ P #-}
-- {-# DISPLAY ∀[]-syntax (λ a → P) = ∀[ a ] P #-}
-- {-# DISPLAY ∃[]-syntax (λ x → P) = ∃[ x ] P #-}

-- ∀-syntax to quantify over hProps (without needing to `[_]` them)
∀ᵖ[∶]-syntax : ∀{ℓ ℓ'} {A : hProp ℓ'} → ([ A ] → hProp ℓ) → hProp (ℓ-max ℓ ℓ')
∀ᵖ[∶]-syntax {A = A} P = (∀ x → [ P x ]) , isPropΠ (isProp[] ∘ P)

syntax ∀ᵖ[∶]-syntax {A = A} (λ a → P) = ∀ᵖ[ a ∶ A ] P
infix 2 ∀ᵖ[∶]-syntax

{-# DISPLAY ∀ᵖ[∶]-syntax {A = A} P = P #-}

-- isPropΠ for a function with an instance argument
isPropΠⁱ : ∀{ℓ ℓ'} {A : Type ℓ} {B : {{p : A}} → Type ℓ'} (h : (x : A) → isProp (B {{x}})) → isProp ({{x : A}} → B {{x}})
isPropΠⁱ h f g i {{x}} = (h x) (f {{x}}) (g {{x}}) i

-- ∀-syntax to quantify over hProps (without needing to `[_]` them) which produces an intance argument
∀ᵖ〚∶〛-syntax : ∀{ℓ ℓ'} {A : hProp ℓ'} → ([ A ] → hProp ℓ) → hProp (ℓ-max ℓ ℓ')
∀ᵖ〚∶〛-syntax {A = A} P = (∀ {{x}} → [ P x ]) , isPropΠⁱ (isProp[] ∘ P)

syntax ∀ᵖ〚∶〛-syntax {A = A} (λ a → P) = ∀ᵖ〚 a ∶ A 〛 P
infix 2 ∀ᵖ〚∶〛-syntax

!isProp : ∀{ℓ} {P : Type ℓ} → isProp P → isProp (! P)
!isProp is-prop (!! x) (!! y) = subst (λ z → (!! x) ≡ (!! z)) (is-prop x y) refl

∀ᵖ!〚∶〛-syntax : ∀{ℓ ℓ'} {A : hProp ℓ'} → (! [ A ] → hProp ℓ) → hProp (ℓ-max ℓ ℓ')
∀ᵖ!〚∶〛-syntax {A = A} P = (∀ {{x}} → [ P x ]) , isPropΠⁱ (λ p → isProp[] (P (p))) -- isPropΠⁱ (isProp[] ∘ P) -- isPropΠⁱ (!isProp ∘ isProp[] ∘ P) --  --

syntax ∀ᵖ!〚∶〛-syntax {A = A} (λ a → P) = ∀ᵖ!〚 a ∶ A 〛 P
infix 2 ∀ᵖ!〚∶〛-syntax

{-# DISPLAY ∀ᵖ[∶]-syntax {A = A} P = P #-}

-- ∀-syntax which produces an intance argument
∀〚∶〛-syntax : ∀{ℓ ℓ'} {A : Type ℓ'} → (A → hProp ℓ) → hProp _
∀〚∶〛-syntax {A = A} P = (∀ {{x}} → [ P x ]) , isPropΠⁱ (isProp[] ∘ P)

syntax ∀〚∶〛-syntax {A = A} (λ a → P) = ∀〚 a ∶ A 〛 P
infix 2 ∀〚∶〛-syntax

{-# DISPLAY ∀〚∶〛-syntax {A = A} P = P #-}

⊎⇒⊔ : ∀ {ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → [ P ] ⊎ [ Q ] → [ P ⊔ Q ]
⊎⇒⊔ P Q (inl x) = inlᵖ x
⊎⇒⊔ P Q (inr x) = inrᵖ x

-- pretty `⊔-elim`
case[⊔]-syntaxᵈ : ∀ {ℓ ℓ' ℓ''} (P : hProp ℓ) (Q : hProp ℓ')
                  → (z : [ P ⊔ Q ])
                  → (R : [ P ⊔ Q ] → hProp ℓ'')
                  → (S : (x : [ P ] ⊎ [ Q ]) → [ R (⊎⇒⊔ P Q x) ] )
                  → [ R z ]
case[⊔]-syntaxᵈ P Q z R S = ⊔-elim P Q R (λ p → S (inl p)) (λ q → S (inr q)) z

syntax case[⊔]-syntaxᵈ P Q z (λ x → R) S = case z as x ∶ P ⊔ Q ⇒ R of S

case[⊔]-syntax : ∀ {ℓ ℓ' ℓ''} (P : hProp ℓ) (Q : hProp ℓ')
                  → (z : [ P ⊔ Q ])
                  → (R : hProp ℓ'')
                  → (S : (x : [ P ] ⊎ [ Q ]) → [ R ] )
                  → [ R ]
case[⊔]-syntax P Q z R S = ⊔-elim P Q (λ _ → R) (λ p → S (inl p)) (λ q → S (inr q)) z

syntax case[⊔]-syntax P Q z R S = case z as P ⊔ Q ⇒ R of S

-- {-# DISPLAY case[⊔]-syntax P Q z R S = case z of S #-}

-- for a function, to be an hProp, it suffices that the result is an hProp
-- so in principle we might inject any non-hProps as arguments with `_ᵗ⇒_`
_ᵗ⇒_ : ∀{ℓ ℓ'} (A : Type ℓ) → (B : hProp ℓ') → hProp _
A ᵗ⇒ B = (A → [ B ]) , isPropΠ λ _ → isProp[] B

infixr 6 _ᵗ⇒_

-- lifting of hProps to create "universe-homogeneous" pathes
--   this is not necessary when using _⇔_ which is universe-inhomogeneous
--   because `_⇔_` can "cross" universes, where `PathP` needs to stay in the same universe

Liftᵖ : ∀{i j : Level} → hProp i → hProp (ℓ-max i j)
Liftᵖ {i} {j} P = Lift {i} {j} [ P ] , λ{ (lift p) (lift q) → λ i → lift (isProp[] P p q i) }

liftᵖ : ∀{i j : Level} → (P : hProp i) → [ P ] → [ Liftᵖ {i} {j} P ]
liftᵖ P p = lift p

unliftᵖ : ∀{i j : Level} → (P : hProp i) → [ Liftᵖ {i} {j} P ] → [ P ]
unliftᵖ P (lift p) = p

⊥↑ : ∀{ℓ} → hProp ℓ
⊥↑ = Lift Empty.⊥ , λ ()

⊤↑ : ∀{ℓ} → hProp ℓ
⊤↑ = Lift Unit , isOfHLevelLift 1 (λ _ _ _ → tt)

infix 10 ¬↑_
¬↑_ : ∀{ℓ} → hProp ℓ → hProp ℓ
¬↑_ {ℓ} A = ([ A ] → Lift {j = ℓ} Empty.⊥) , isPropΠ λ _ → isOfHLevelLift 1 Empty.isProp⊥

-- negation with an instance argument
¬ⁱ_ : ∀{ℓ} → hProp ℓ → hProp ℓ
¬ⁱ A = ({{p : [ A ]}} → ⊥⊥) , isPropΠⁱ {A = [ A ]} λ _ → isProp⊥

¬'_ : ∀{ℓ} → Type ℓ → hProp ℓ
¬' A = (A → ⊥⊥) , isPropΠ λ _ → isProp⊥

¬-≡-¬ⁱ : ∀{ℓ} (P : hProp ℓ) → ¬ P ≡ ¬ⁱ P
¬-≡-¬ⁱ P =
  ⇒∶ (λ f {{p}} → f   p  )
  ⇐∶ (λ f   p   → f {{p}})

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals