text:
{-# OPTIONS --rewriting #-}

module Properties.StrictMode where

import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right; mapL; mapR; mapLR; swapLR; cond)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr)
open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
open import Luau.Subtyping using (_≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language)
open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; src; tgt; _≡ᵀ_; _≡ᴹᵀ_)
open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp)
open import Luau.Var using (_≡ⱽ_)
open import Luau.Addr using (_≡ᴬ_)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
open import Luau.VarCtxt using (VarCtxt; ∅)
open import Properties.Remember using (remember; _,_)
open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Contradiction using (CONTRADICTION; ¬)
open import Properties.Functions using (_∘_)
open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
open import Properties.TypeCheck using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)
open import Luau.RuntimeType using (RuntimeType; valueType; number; string; boolean; nil; function)

data _⊑_ (H : Heap yes) : Heap yes → Set where
  refl : (H ⊑ H)
  snoc : ∀ {H′ a O} → (H′ ≡ᴴ H ⊕ a ↦ O) → (H ⊑ H′)

rednᴱ⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′)
rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H′)

rednᴱ⊑ (function a p) = snoc p
rednᴱ⊑ (app₁ s) = rednᴱ⊑ s
rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s
rednᴱ⊑ (beta O v p q) = refl
rednᴱ⊑ (block s) = rednᴮ⊑ s
rednᴱ⊑ (return v) = refl
rednᴱ⊑ done = refl
rednᴱ⊑ (binOp₀ p) = refl
rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s
rednᴱ⊑ (binOp₂ s) = rednᴱ⊑ s

rednᴮ⊑ (local s) = rednᴱ⊑ s
rednᴮ⊑ (subst v) = refl
rednᴮ⊑ (function a p) = snoc p
rednᴮ⊑ (return s) = rednᴱ⊑ s

data LookupResult (H : Heap yes) a V : Set where
  just : (H [ a ]ᴴ ≡ just V) → LookupResult H a V
  nothing : (H [ a ]ᴴ ≡ nothing) → LookupResult H a V

lookup-⊑-nothing : ∀ {H H′} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ nothing) → (H [ a ]ᴴ ≡ nothing)
lookup-⊑-nothing {H} a refl p = p
lookup-⊑-nothing {H} a (snoc defn) p with a ≡ᴬ next H
lookup-⊑-nothing {H} a (snoc defn) p | yes refl = refl
lookup-⊑-nothing {H} a (snoc o) p | no q = trans (lookup-not-allocated o q) p

heap-weakeningᴱ : ∀ Γ H M {H′ U} → (H ⊑ H′) → (typeOfᴱ H′ Γ M ≮: U) → (typeOfᴱ H Γ M ≮: U)
heap-weakeningᴱ Γ H (var x) h p = p
heap-weakeningᴱ Γ H (val nil) h p = p
heap-weakeningᴱ Γ H (val (addr a)) refl p = p
heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p with a ≡ᴬ b
heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) p | yes refl = unknown-≮: p
heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ (lookup-not-allocated q r))) p
heap-weakeningᴱ Γ H (val (number x)) h p = p
heap-weakeningᴱ Γ H (val (bool x)) h p = p
heap-weakeningᴱ Γ H (val (string x)) h p = p
heap-weakeningᴱ Γ H (M $ N) h p = never-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-never-≮: p))
heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p
heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p
heap-weakeningᴱ Γ H (binexp M op N) h p = p

heap-weakeningᴮ : ∀ Γ H B {H′ U} → (H ⊑ H′) → (typeOfᴮ H′ Γ B ≮: U) → (typeOfᴮ H Γ B ≮: U)
heap-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h p = heap-weakeningᴮ (Γ ⊕ f ↦ (T ⇒ U)) H B h p
heap-weakeningᴮ Γ H (local var x ∈ T ← M ∙ B) h p = heap-weakeningᴮ (Γ ⊕ x ↦ T) H B h p
heap-weakeningᴮ Γ H (return M ∙ B) h p = heap-weakeningᴱ Γ H M h p
heap-weakeningᴮ Γ H done h p = p

substitutivityᴱ : ∀ {Γ T U} H M v x → (typeOfᴱ H Γ (M [ v / x ]ᴱ) ≮: U) → Either (typeOfᴱ H (Γ ⊕ x ↦ T) M ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
substitutivityᴱ-whenever : ∀ {Γ T U} H v x y (r : Dec(x ≡ y)) → (typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever r) ≮: U) → Either (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
substitutivityᴮ : ∀ {Γ T U} H B v x → (typeOfᴮ H Γ (B [ v / x ]ᴮ) ≮: U) → Either (typeOfᴮ H (Γ ⊕ x ↦ T) B ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
substitutivityᴮ-unless : ∀ {Γ T U V} H B v x y (r : Dec(x ≡ y)) → (typeOfᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r) ≮: V) → Either (typeOfᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T V} H B v x y (r : x ≡ y) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless yes r) ≮: V) → Either (typeOfᴮ H Γ′ B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless no r) ≮: V) → Either (typeOfᴮ H Γ′ B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)

substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p
substitutivityᴱ H (val w) v x p = Left p
substitutivityᴱ H (binexp M op N) v x p = Left p
substitutivityᴱ H (M $ N) v x p = mapL never-tgt-≮: (substitutivityᴱ H M v x (tgt-never-≮: p))
substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = Left p
substitutivityᴱ H (block var b ∈ T is B end) v x p = Left p
substitutivityᴱ-whenever H v x x (yes refl) q = swapLR (≮:-trans q)
substitutivityᴱ-whenever H v x y (no p) q = Left (≡-trans-≮: (cong orUnknown (sym (⊕-lookup-miss x y _ _ p))) q)

substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p = substitutivityᴮ-unless H B v x f (x ≡ⱽ f) p
substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p = substitutivityᴮ-unless H B v x y (x ≡ⱽ y) p
substitutivityᴮ H (return M ∙ B) v x p = substitutivityᴱ H M v x p
substitutivityᴮ H done v x p = Left p
substitutivityᴮ-unless H B v x y (yes p) q = substitutivityᴮ-unless-yes H B v x y p (⊕-over p) q
substitutivityᴮ-unless H B v x y (no p) q = substitutivityᴮ-unless-no H B v x y p (⊕-swap p) q
substitutivityᴮ-unless-yes H B v x y refl refl p = Left p
substitutivityᴮ-unless-no H B v x y p refl q = substitutivityᴮ H B v x q

binOpPreservation : ∀ H {op v w x} → (v ⟦ op ⟧ w ⟶ x) → (tgtBinOp op ≡ typeOfᴱ H ∅ (val x))
binOpPreservation H (+ m n) = refl
binOpPreservation H (- m n) = refl
binOpPreservation H (/ m n) = refl
binOpPreservation H (* m n) = refl
binOpPreservation H (< m n) = refl
binOpPreservation H (> m n) = refl
binOpPreservation H (<= m n) = refl
binOpPreservation H (>= m n) = refl
binOpPreservation H (== v w) = refl
binOpPreservation H (~= v w) = refl
binOpPreservation H (·· v w) = refl

reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M))
reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B))

reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR never-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-never-≮: p))
reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (never-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-never-≮: p)))
reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orUnknown (cong typeOfᴹᴼ q))) p)
reflect-subtypingᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) p = Left p
reflect-subtypingᴱ H (block var b ∈ T is B end) (block s) p = Left p
reflect-subtypingᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) p = mapR BlockMismatch (swapLR (≮:-trans p))
reflect-subtypingᴱ H (block var b ∈ T is done end) done p = mapR BlockMismatch (swapLR (≮:-trans p))
reflect-subtypingᴱ H (binexp M op N) (binOp₀ s) p = Left (≡-trans-≮: (binOpPreservation H s) p)
reflect-subtypingᴱ H (binexp M op N) (binOp₁ s) p = Left p
reflect-subtypingᴱ H (binexp M op N) (binOp₂ s) p = Left p

reflect-subtypingᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) p = mapLR (heap-weakeningᴮ _ _ B (snoc defn)) (CONTRADICTION ∘ ≮:-refl) (substitutivityᴮ _ B (addr a) f p)
reflect-subtypingᴮ H (local var x ∈ T ← M ∙ B) (local s) p = Left (heap-weakeningᴮ (x ↦ T) H B (rednᴱ⊑ s) p)
reflect-subtypingᴮ H (local var x ∈ T ← M ∙ B) (subst v) p = mapR LocalVarMismatch (substitutivityᴮ H B v x p)
reflect-subtypingᴮ H (return M ∙ B) (return s) p = mapR return (reflect-subtypingᴱ H M s p)

reflect-substitutionᴱ : ∀ {Γ T} H M v x → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Either (Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
reflect-substitutionᴱ-whenever : ∀ {Γ T} H v x y (p : Dec(x ≡ y)) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever p)) → Either (Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y))) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
reflect-substitutionᴮ : ∀ {Γ T} H B v x → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Either (Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
reflect-substitutionᴮ-unless : ∀ {Γ T U} H B v x y (r : Dec(x ≡ y)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r)) → Either (Warningᴮ H (typeCheckᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Either (Warningᴮ H (typeCheckᴮ H Γ′ B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Either (Warningᴮ H (typeCheckᴮ H Γ′ B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))

reflect-substitutionᴱ H (var y) v x W = reflect-substitutionᴱ-whenever H v x y (x ≡ⱽ y) W
reflect-substitutionᴱ H (val (addr a)) v x (UnallocatedAddress r) = Left (UnallocatedAddress r)
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) with substitutivityᴱ H N v x p
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Right W = Right (Right W)
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-unknown-≮: q)
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ unknown-src-≮: q) r)
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Right W = Right (Right W)
reflect-substitutionᴱ H (M $ N) v x (app₁ W) = mapL app₁ (reflect-substitutionᴱ H M v x W)
reflect-substitutionᴱ H (M $ N) v x (app₂ W) = mapL app₂ (reflect-substitutionᴱ H N v x W)
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (substitutivityᴮ-unless H B v x y (x ≡ⱽ y) q)
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x (function₁ W) = mapL function₁ (reflect-substitutionᴮ-unless H B v x y (x ≡ⱽ y) W)
reflect-substitutionᴱ H (block var b ∈ T is B end) v x (BlockMismatch q) =  mapLR BlockMismatch Right (substitutivityᴮ H B v x q)
reflect-substitutionᴱ H (block var b ∈ T is B end) v x (block₁ W′) = mapL block₁ (reflect-substitutionᴮ H B v x W′)
reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₁ q) = mapLR BinOpMismatch₁ Right (substitutivityᴱ H M v x q)
reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₂ q) = mapLR BinOpMismatch₂ Right (substitutivityᴱ H N v x q)
reflect-substitutionᴱ H (binexp M op N) v x (bin₁ W) = mapL bin₁ (reflect-substitutionᴱ H M v x W)
reflect-substitutionᴱ H (binexp M op N) v x (bin₂ W) = mapL bin₂ (reflect-substitutionᴱ H N v x W)

reflect-substitutionᴱ-whenever H a x x (yes refl) (UnallocatedAddress p) = Right (Left (UnallocatedAddress p))
reflect-substitutionᴱ-whenever H v x y (no p) (UnboundVariable q) = Left (UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) q))

reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (substitutivityᴮ-unless H C v x y (x ≡ⱽ y) q)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (function₁ W) =  mapL function₁ (reflect-substitutionᴮ-unless H C v x y (x ≡ⱽ y) W)
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (function₂ W) = mapL function₂ (reflect-substitutionᴮ-unless H B v x f (x ≡ⱽ f) W)
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (LocalVarMismatch q) = mapLR LocalVarMismatch Right (substitutivityᴱ H M v x q)
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (local₁ W) = mapL local₁ (reflect-substitutionᴱ H M v x W)
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (local₂ W) = mapL local₂ (reflect-substitutionᴮ-unless H B v x y (x ≡ⱽ y) W)
reflect-substitutionᴮ H (return M ∙ B) v x (return W) = mapL return (reflect-substitutionᴱ H M v x W)

reflect-substitutionᴮ-unless H B v x y (yes p) W = reflect-substitutionᴮ-unless-yes H B v x y p (⊕-over p) W
reflect-substitutionᴮ-unless H B v x y (no p) W = reflect-substitutionᴮ-unless-no H B v x y p (⊕-swap p) W
reflect-substitutionᴮ-unless-yes H B v x x refl refl W = Left W
reflect-substitutionᴮ-unless-no H B v x y p refl W = reflect-substitutionᴮ H B v x W

reflect-weakeningᴱ : ∀ Γ H M {H′} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M)
reflect-weakeningᴮ : ∀ Γ H B {H′} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B)

reflect-weakeningᴱ Γ H (var x) h (UnboundVariable p) = (UnboundVariable p)
reflect-weakeningᴱ Γ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p)
reflect-weakeningᴱ Γ H (M $ N) h (FunctionCallMismatch p) = FunctionCallMismatch (heap-weakeningᴱ Γ H N h (unknown-src-≮: p (heap-weakeningᴱ Γ H M h (src-unknown-≮: p))))
reflect-weakeningᴱ Γ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ Γ H M h W)
reflect-weakeningᴱ Γ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ Γ H N h W)
reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₁ p) = BinOpMismatch₁ (heap-weakeningᴱ Γ H M h p)
reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₂ p) = BinOpMismatch₂ (heap-weakeningᴱ Γ H N h p)
reflect-weakeningᴱ Γ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ Γ H M h W′)
reflect-weakeningᴱ Γ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ Γ H N h W′)
reflect-weakeningᴱ Γ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (Γ ⊕ y ↦ T) H B h p)
reflect-weakeningᴱ Γ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ (Γ ⊕ y ↦ T) H B h W)
reflect-weakeningᴱ Γ H (block var b ∈ T is B end) h (BlockMismatch p) = BlockMismatch (heap-weakeningᴮ Γ H B h p)
reflect-weakeningᴱ Γ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ Γ H B h W)

reflect-weakeningᴮ Γ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ Γ H M h W)
reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) = LocalVarMismatch (heap-weakeningᴱ Γ H M h p)
reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ Γ H M h W)
reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ (Γ ⊕ y ↦ T) H B h W)
reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (Γ ⊕ x ↦ T) H C h p)
reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ (Γ ⊕ x ↦ T) H C h W)
reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ (Γ ⊕ f ↦ (T ⇒ U)) H B h W)

reflect-weakeningᴼ : ∀ H O {H′} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O)
reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H B h p)
reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ (x ↦ T) H B h W)

reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H))
reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H))

reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ unknown-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-unknown-≮: p))
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) = mapL app₁ (reflectᴱ H M s W′)
reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = Left (app₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′))
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (unknown-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-unknown-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ H N s q)
reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = Left (app₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′))
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) = mapL app₂ (reflectᴱ H N s W′)
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with substitutivityᴮ H B v x q
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Left r = Right (addr a p (FunctionDefnMismatch r))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Right r = Left (FunctionCallMismatch (≮:-trans-≡ r ((cong src (cong orUnknown (cong typeOfᴹᴼ (sym p)))))))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with reflect-substitutionᴮ _ B v x W′
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Left W = Right (addr a p (function₁ W))
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Left W) = Left (app₂ W)
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Right q) = Left (FunctionCallMismatch (≮:-trans-≡ q (cong src (cong orUnknown (cong typeOfᴹᴼ (sym p))))))
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) = Left (cond BlockMismatch block₁ (reflect-subtypingᴮ H B s p))
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) = mapL block₁ (reflectᴮ H B s W′)
reflectᴱ H (block var b ∈ T is B end) (return v) W′ = Left (block₁ (return W′))
reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ())
reflectᴱ H (binexp M op N) (binOp₀ ()) (UnallocatedAddress p)
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) = Left (cond BinOpMismatch₁ bin₁ (reflect-subtypingᴱ H M s p))
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) = Left (BinOpMismatch₂ (heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) p))
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) = mapL bin₁ (reflectᴱ H M s W′)
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = Left (bin₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) = Left (BinOpMismatch₁ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) p))
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) = Left (cond BinOpMismatch₂ bin₂ (reflect-subtypingᴱ H N s p))
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = Left (bin₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′))
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) = mapL bin₂ (reflectᴱ H N s W′)

reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) = Left (cond LocalVarMismatch local₁ (reflect-subtypingᴱ H M s p))
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) = mapL local₁ (reflectᴱ H M s W′)
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = Left (local₂ (reflect-weakeningᴮ (x ↦ T) H B (rednᴱ⊑ s) W′))
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ = Left (cond local₂ (cond local₁ LocalVarMismatch) (reflect-substitutionᴮ H B v x W′))
reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ with reflect-substitutionᴮ _ B (addr a) f W′
reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Left W = Left (function₂ (reflect-weakeningᴮ (f ↦ (T ⇒ U)) H B (snoc defn) W))
reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Right (Left (UnallocatedAddress ()))
reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Right (Right p) = CONTRADICTION (≮:-refl p)
reflectᴮ H (return M ∙ B) (return s) (return W′) = mapL return (reflectᴱ H M s W′)

reflectᴴᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴ H′ (typeCheckᴴ H′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H))
reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴ H′ (typeCheckᴴ H′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H))

reflectᴴᴱ H (M $ N) (app₁ s) W = mapL app₁ (reflectᴴᴱ H M s W)
reflectᴴᴱ H (M $ N) (app₂ v s) W = mapL app₂ (reflectᴴᴱ H N s W)
reflectᴴᴱ H (M $ N) (beta O v refl p) W = Right W
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (addr b refl W) with b ≡ᴬ a
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H B (snoc defn) p))
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (addr b refl (function₁ W)) | yes refl = Left (function₁ (reflect-weakeningᴮ (x ↦ T) H B (snoc defn) W))
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (addr b refl W) | no q = Right (addr b (lookup-not-allocated p q) (reflect-weakeningᴼ H _ (snoc p) W))
reflectᴴᴱ H (block var b ∈ T is B end) (block s) W = mapL block₁ (reflectᴴᴮ H B s W)
reflectᴴᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) W = Right W
reflectᴴᴱ H (block var b ∈ T is done end) done W = Right W
reflectᴴᴱ H (binexp M op N) (binOp₀ s) W = Right W
reflectᴴᴱ H (binexp M op N) (binOp₁ s) W = mapL bin₁ (reflectᴴᴱ H M s W)
reflectᴴᴱ H (binexp M op N) (binOp₂ s) W = mapL bin₂ (reflectᴴᴱ H N s W)

reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a p) (addr b refl W) with b ≡ᴬ a
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H C (snoc defn) p))
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) (addr b refl (function₁ W)) | yes refl = Left (function₁ (reflect-weakeningᴮ (x ↦ T) H C (snoc defn) W))
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a p) (addr b refl W) | no q = Right (addr b (lookup-not-allocated p q) (reflect-weakeningᴼ H _ (snoc p) W))
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) W = mapL local₁ (reflectᴴᴱ H M s W)
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) W = Right W
reflectᴴᴮ H (return M ∙ B) (return s) W = mapL return (reflectᴴᴱ H M s W)

reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Either (Warningᴮ H′ (typeCheckᴮ H′ ∅ B′)) (Warningᴴ H′ (typeCheckᴴ H′)) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H))
reflect* H B refl W = W
reflect* H B (step s t) W = cond (reflectᴮ H B s) (reflectᴴᴮ H B s) (reflect* _ _ t W)

isntNumber : ∀ H v → (valueType v ≢ number) → (typeOfᴱ H ∅ (val v) ≮: number)
isntNumber H nil p = scalar-≢-impl-≮: nil number (λ ())
isntNumber H (addr a) p with remember (H [ a ]ᴴ)
isntNumber H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (function-≮:-scalar number)
isntNumber H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (unknown-≮:-scalar number)
isntNumber H (number x) p = CONTRADICTION (p refl)
isntNumber H (bool x) p = scalar-≢-impl-≮: boolean number (λ ())
isntNumber H (string x) p = scalar-≢-impl-≮: string number (λ ())

isntString : ∀ H v → (valueType v ≢ string) → (typeOfᴱ H ∅ (val v) ≮: string)
isntString H nil p = scalar-≢-impl-≮: nil string (λ ())
isntString H (addr a) p with remember (H [ a ]ᴴ)
isntString H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (function-≮:-scalar string)
isntString H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ q)) (unknown-≮:-scalar string)
isntString H (number x) p = scalar-≢-impl-≮: number string (λ ())
isntString H (bool x) p = scalar-≢-impl-≮: boolean string (λ ())
isntString H (string x) p = CONTRADICTION (p refl)

isntFunction : ∀ H v {T U} → (valueType v ≢ function) → (typeOfᴱ H ∅ (val v) ≮: (T ⇒ U))
isntFunction H nil p = scalar-≮:-function nil
isntFunction H (addr a) p = CONTRADICTION (p refl)
isntFunction H (number x) p = scalar-≮:-function number
isntFunction H (bool x) p = scalar-≮:-function boolean
isntFunction H (string x) p = scalar-≮:-function string

isntEmpty : ∀ H v → (typeOfᴱ H ∅ (val v) ≮: never)
isntEmpty H nil = scalar-≮:-never nil
isntEmpty H (addr a) with remember (H [ a ]ᴴ)
isntEmpty H (addr a) | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , p) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ p)) function-≮:-never
isntEmpty H (addr a) | (nothing , p) = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ p)) unknown-≮:-never
isntEmpty H (number x) = scalar-≮:-never number
isntEmpty H (bool x) = scalar-≮:-never boolean
isntEmpty H (string x) = scalar-≮:-never string

runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → (typeOfᴱ H ∅ (val v) ≮: srcBinOp op)
runtimeBinOpWarning H v (+ p) = isntNumber H v p
runtimeBinOpWarning H v (- p) = isntNumber H v p
runtimeBinOpWarning H v (* p) = isntNumber H v p
runtimeBinOpWarning H v (/ p) = isntNumber H v p
runtimeBinOpWarning H v (< p) = isntNumber H v p
runtimeBinOpWarning H v (> p) = isntNumber H v p
runtimeBinOpWarning H v (<= p) = isntNumber H v p
runtimeBinOpWarning H v (>= p) = isntNumber H v p
runtimeBinOpWarning H v (·· p) = isntString H v p

runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M)
runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B)

runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl
runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) = FunctionCallMismatch (unknown-src-≮: (isntEmpty H w) (isntFunction H v p))
runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err)
runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err)
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₁ v w p) = BinOpMismatch₁ (runtimeBinOpWarning H v p)
runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₂ v w p) = BinOpMismatch₂ (runtimeBinOpWarning H w p)
runtimeWarningᴱ H (binexp M op N) (bin₁ err) = bin₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (binexp M op N) (bin₂ err) = bin₂ (runtimeWarningᴱ H N err)

runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err)
runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err)

wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B)
wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (Left (runtimeWarningᴮ H′ B′ err))
wellTypedProgramsDontGoWrong H′ B B′ t err | Right (addr a refl ())
wellTypedProgramsDontGoWrong H′ B B′ t err | Left W = W

max_stars_repo_name: MeltzDev/luau

max_issues_repo_name: MeltzDev/luau

max_forks_repo_name: MeltzDev/luau


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the heterogeneous suffix relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Suffix.Heterogeneous where

open import Level
open import Relation.Binary using (REL; _⇒_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise as Pointwise
  using (Pointwise; []; _∷_)

module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where

  data Suffix : REL (List A) (List B) (a ⊔ b ⊔ r) where
    here  : ∀ {as bs} → Pointwise R as bs → Suffix as bs
    there : ∀ {b as bs} → Suffix as bs → Suffix as (b ∷ bs)

  data SuffixView (as : List A) : List B → Set (a ⊔ b ⊔ r) where
    _++_ : ∀ cs {ds} → Pointwise R as ds → SuffixView as (cs List.++ ds)

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  tail : ∀ {a as bs} → Suffix R (a ∷ as) bs → Suffix R as bs
  tail (here (_ ∷ rs)) = there (here rs)
  tail (there x) = there (tail x)

module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where

  map : R ⇒ S → Suffix R ⇒ Suffix S
  map R⇒S (here rs)   = here (Pointwise.map R⇒S rs)
  map R⇒S (there suf) = there (map R⇒S suf)

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  toView : ∀ {as bs} → Suffix R as bs → SuffixView R as bs
  toView (here rs) = [] ++ rs
  toView (there {c} suf) with toView suf
  ... | cs ++ rs = (c ∷ cs) ++ rs

  fromView : ∀ {as bs} → SuffixView R as bs → Suffix R as bs
  fromView ([]       ++ rs) = here rs
  fromView ((c ∷ cs) ++ rs) = there (fromView (cs ++ rs))

ext: agda


text:
module PredicateName where

open import OscarPrelude

record PredicateName : Set
 where
  constructor ⟨_⟩
  field
    name : Nat

open PredicateName public

instance EqPredicateName : Eq PredicateName
Eq._==_ EqPredicateName _ = decEq₁ (cong name) ∘ (_≟_ on name $ _)


text:
{-# OPTIONS --copatterns --sized-types #-}

open import Size
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

open import Algebra.Structures using (IsCommutativeSemiring; IsCommutativeMonoid)

open import Data.Nat
open import Data.Nat.Properties using (isCommutativeSemiring)
open import Stream
open ∼ˢ∞-Reasoning

⟦_⟧ : ℕ → Str ℕ
hd (⟦ n ⟧) = n
tl (⟦ n ⟧) = ⟦ 0 ⟧

_⊕_ : ∀{i} → Str {i} ℕ → Str {i} ℕ → Str {i} ℕ
hd (s ⊕ t) = (hd s) + (hd t)
tl (s ⊕ t) = (tl s) ⊕ (tl t)

_×_ : ∀{i} → Str {i} ℕ → Str {i} ℕ → Str {i} ℕ
hd (s × t) = hd s * hd t
tl (s × t)= ((tl s) × t) ⊕ (⟦ hd s ⟧ × (tl t))

comm-* : ∀ m n → m * n ≡ n * m
comm-* = IsCommutativeMonoid.comm
         (IsCommutativeSemiring.*-isCommutativeMonoid isCommutativeSemiring)

comm-+ : ∀ m n → m + n ≡ n + m
comm-+ = IsCommutativeMonoid.comm
         (IsCommutativeSemiring.+-isCommutativeMonoid isCommutativeSemiring)

Bisim = _∼ˢ_

{-
mutual
  comm-× : ∀{i} →
           (s t : Str {i} ℕ) → Bisim {ℕ} {i} (s × t) (t × s)
  hd≡ (comm-× s t) = comm-* (hd s) (hd t)
  tl∼ (comm-× s t) = lem-comm-× s t

  lem-comm-× : ∀{i} → ∀{j : Size< i} →
               (s t : Str {i} ℕ) →
               Bisim {ℕ} {j}
                 ((tl s × t) ⊕ (⟦ hd s ⟧ × tl t))
                 ((tl t × s) ⊕ (⟦ hd t ⟧ × tl s))
  hd≡ (lem-comm-× {i} {j} s t) =
    begin
      hd s' * hd t + hd s * hd t'
    ≡⟨ comm-+ (hd s' * hd t) (hd s * hd t') ⟩
      hd s * hd t' + hd s' * hd t
    ≡⟨ cong (λ x → x + hd s' * hd t) (comm-* (hd s) (hd t')) ⟩
      hd t' * hd s + hd s' * hd t
    ≡⟨ cong (λ x → hd t' * hd s + x) (comm-* (hd s') (hd t)) ⟩
      hd t' * hd s + hd t * hd s'
    ∎
    where
      s' = tl s {j}
      t' = tl t {j}

  tl∼ (lem-comm-× {i} {j} s t) {k} = lem {k}
    where
      s' = tl s {j}
      t' = tl t {j}

      lem : ∀{k : Size< j} → Bisim {ℕ} {k}
        (((tl s' × t) ⊕ (⟦ hd s' ⟧ × t')) ⊕ ((⟦ 0 ⟧ × t') ⊕ (⟦ hd s ⟧ × tl t')))
        (((tl t' × s) ⊕ (⟦ hd t' ⟧ × s')) ⊕ ((⟦ 0 ⟧ × s') ⊕ (⟦ hd t ⟧ × tl s')))
      lem = {!!}
        where
          s'' = tl s' {k}
          t'' = tl t' {k}
-}

zero-⊕-unit-l : (s : Str ℕ) → (⟦ 0 ⟧ ⊕ s) ∼ˢ∞ s
hd≡∞ (zero-⊕-unit-l s) = refl
tl∼∞ (zero-⊕-unit-l s) = zero-⊕-unit-l (tl s)

zero-⊕-unit-r : (s : Str ℕ) → (s ⊕ ⟦ 0 ⟧) ∼ˢ∞ s
hd≡∞ (zero-⊕-unit-r s) = comm-+ (hd s) 0
tl∼∞ (zero-⊕-unit-r s) = zero-⊕-unit-r (tl s)

zero-×-annihil-l : (s : Str ℕ) → (⟦ 0 ⟧ × s) ∼ˢ∞ ⟦ 0 ⟧
hd≡∞ (zero-×-annihil-l s) = refl
tl∼∞ (zero-×-annihil-l s) =
  beginˢ∞
    tl (⟦ 0 ⟧ × s)
  ∼ˢ∞⟨ s-bisim∞-refl ⟩
    (⟦ 0 ⟧ × s) ⊕ (⟦ 0 ⟧ × tl s)
  ∼ˢ∞⟨ {!!} ⟩
    tl (⟦ 0 ⟧)
  ∎ˢ∞

mutual
  comm-× : (s t : Str ℕ) → (s × t) ∼ˢ∞ (t × s)
  hd≡∞ (comm-× s t) = comm-* (hd s) (hd t)
  tl∼∞ (comm-× s t) = lem-comm-× s t

  lem-comm-× : (s t : Str ℕ) →
               ((tl s × t) ⊕ (⟦ hd s ⟧ × tl t))
               ∼ˢ∞ ((tl t × s) ⊕ (⟦ hd t ⟧ × tl s))
  hd≡∞ (lem-comm-× s t) =
    begin
      hd s' * hd t + hd s * hd t'
    ≡⟨ comm-+ (hd s' * hd t) (hd s * hd t') ⟩
      hd s * hd t' + hd s' * hd t
    ≡⟨ cong (λ x → x + hd s' * hd t) (comm-* (hd s) (hd t')) ⟩
      hd t' * hd s + hd s' * hd t
    ≡⟨ cong (λ x → hd t' * hd s + x) (comm-* (hd s') (hd t)) ⟩
      hd t' * hd s + hd t * hd s'
    ∎
    where
      s' = tl s
      t' = tl t

  tl∼∞ (lem-comm-× s t) = lem
    where
      s' = tl s
      t' = tl t

      lem :
        (((tl s' × t) ⊕ (⟦ hd s' ⟧ × t')) ⊕ ((⟦ 0 ⟧ × t') ⊕ (⟦ hd s ⟧ × tl t')))
        ∼ˢ∞ (((tl t' × s) ⊕ (⟦ hd t' ⟧ × s')) ⊕ ((⟦ 0 ⟧ × s') ⊕ (⟦ hd t ⟧ × tl s')))
      lem = {!!}
        where
          s'' = tl s'
          t'' = tl t'

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module _ where

open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  A : Set

super-tac : Term → TC ⊤
super-tac hole = unify hole (lit (nat 101))

solver : Nat → Term → TC ⊤
solver n hole = unify hole (lit (nat (n + 1)))

foo : {@(tactic super-tac) n : Nat}
      {@(tactic solver n)  x : A} → A
foo  {n = n} {x = x} = x

number : Nat
number = foo

check : number ≡ 102
check = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.NatSolver.HornerForms where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat hiding (isZero)
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Data.Bool using (Bool; true; false; if_then_else_)

private
  variable
    ℓ : Level

{-
  This defines the type of multivariate Polynomials over ℕ.
  The construction is based on the algebraic fact

    ℕ[X₀][X₁]⋯[Xₙ] ≅ ℕ[X₀,⋯,Xₙ]

  BUT: Contrary to algebraic convetions, we will give 'Xₙ' the lowest index
  in the definition of 'Variable' below. So if 'Variable n k' is identified
  with 'Xₖ', what we construct should rather be denoted with

    ℕ[Xₙ][Xₙ₋₁]⋯[X₀]

  or, to be precise about the evaluation order:

    (⋯((ℕ[Xₙ])[Xₙ₋₁])⋯)[X₀]

-}

data IteratedHornerForms : ℕ → Type ℓ-zero where
  const : ℕ → IteratedHornerForms ℕ.zero
  0H : {n : ℕ} → IteratedHornerForms (ℕ.suc n)
  _·X+_ : {n : ℕ} → IteratedHornerForms (ℕ.suc n) → IteratedHornerForms n
                  → IteratedHornerForms (ℕ.suc n)

eval : {n : ℕ} (P : IteratedHornerForms n)
       → Vec ℕ n → ℕ
eval (const r) [] = r
eval 0H (_ ∷ _) = 0
eval (P ·X+ Q) (x ∷ xs) =
  (eval P (x ∷ xs)) · x + eval Q xs

module IteratedHornerOperations where

  private
    1H' : (n : ℕ) → IteratedHornerForms n
    1H' ℕ.zero = const 1
    1H' (ℕ.suc n) = 0H ·X+ 1H' n

    0H' : (n : ℕ) → IteratedHornerForms n
    0H' ℕ.zero = const 0
    0H' (ℕ.suc n) = 0H

  1ₕ : {n : ℕ} → IteratedHornerForms n
  1ₕ {n = n} = 1H' n

  0ₕ : {n : ℕ} → IteratedHornerForms n
  0ₕ {n = n} = 0H' n

  X : (n : ℕ) (k : Fin n) → IteratedHornerForms n
  X (ℕ.suc m) zero = 1ₕ ·X+ 0ₕ
  X (ℕ.suc m) (suc k) = 0ₕ ·X+ X m k

  _+ₕ_ : {n : ℕ} → IteratedHornerForms n → IteratedHornerForms n
               → IteratedHornerForms n
  (const r) +ₕ (const s) = const (r + s)
  0H +ₕ Q = Q
  (P ·X+ r) +ₕ 0H = P ·X+ r
  (P ·X+ r) +ₕ (Q ·X+ s) = (P +ₕ Q) ·X+ (r +ₕ s)

  isZero : {n : ℕ} → IteratedHornerForms (ℕ.suc n)
                   → Bool
  isZero 0H = true
  isZero (P ·X+ P₁) = false

  _⋆_ : {n : ℕ} → IteratedHornerForms n → IteratedHornerForms (ℕ.suc n)
                → IteratedHornerForms (ℕ.suc n)
  _·ₕ_ : {n : ℕ} → IteratedHornerForms n → IteratedHornerForms n
                → IteratedHornerForms n
  r ⋆ 0H = 0H
  r ⋆ (P ·X+ Q) = (r ⋆ P) ·X+ (r ·ₕ Q)

  const x ·ₕ const y = const (x · y)
  0H ·ₕ Q = 0H
  (P ·X+ Q) ·ₕ S =
     let
        z = (P ·ₕ S)
     in if (isZero z)
        then (Q ⋆ S)
        else (z ·X+ 0ₕ) +ₕ (Q ⋆ S)

Variable : (n : ℕ) (k : Fin n) → IteratedHornerForms n
Variable n k = IteratedHornerOperations.X n k

Constant : (n : ℕ) (r : ℕ) → IteratedHornerForms n
Constant ℕ.zero r = const r
Constant (ℕ.suc n) r = IteratedHornerOperations.0ₕ ·X+ Constant n r

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Basic.Compiler.SplitCode where

open import Basic.Compiler.Code
open import Basic.AST
open import Basic.BigStep
open import Utils.Monoid

open import Data.Vec hiding (_++_; [_]; _∷ʳ_)
open import Data.Bool renaming (if_then_else_ to ifBool_then_else_)
open import Data.Nat
open import Data.List hiding ([_])
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Product
open import Algebra
import Level as L

private
  module LM {a}{A : Set a} = Algebra.Monoid (Data.List.monoid A)

{-
Exercise 3.5

This code logically belongs to either Compiler.Code or Compiler.CorrectFrom.
It has its own module solely because it slows down typechecking for the module
it's in, which is rather annoying.
-}

▷*-split :
  ∀ {n}{s s' : State n}{e e'} c₁ {c₂}
  → (p : ⟨ c₁ <> c₂ , e , s ⟩▷*⟨ [] , e' , s' ⟩)
  → ∃₂ λ s'' e''
  → ∃₂ λ (p1 : ⟨ c₁ , e  , s    ⟩▷*⟨ [] , e'' , s'' ⟩)
         (p2 : ⟨ c₂ , e'' , s'' ⟩▷*⟨ [] , e'  , s'  ⟩)
  → ▷*-length p1 + ▷*-length p2 ≡ ▷*-length p

▷*-split []       p = _ , _ , done , p , refl
▷*-split (.ADD ∷ cs) (ADD a b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , ADD a b ∷ p1 , p2 , cong suc eqn
▷*-split (.MUL ∷ cs) (MUL a b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , MUL a b ∷ p1 , p2 , cong suc eqn
▷*-split (.SUB ∷ cs) (SUB a b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , SUB a b ∷ p1 , p2 , cong suc eqn
▷*-split (.EQ ∷ cs) (EQ a b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , EQ a b ∷ p1 , p2 , cong suc eqn
▷*-split (.LT ∷ cs) (LT a b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , LT a b ∷ p1 , p2 , cong suc eqn
▷*-split (.LTE ∷ cs) (LTE a b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , LTE a b ∷ p1 , p2 , cong suc eqn
▷*-split (.AND ∷ cs) (AND a b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , AND a b ∷ p1 , p2 , cong suc eqn
▷*-split (.(PUSH n₁) ∷ cs) (PUSH n₁ ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , PUSH n₁ ∷ p1 , p2 , cong suc eqn
▷*-split (.TRUE ∷ cs) (TRUE ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , TRUE ∷ p1 , p2 , cong suc eqn
▷*-split (.FALSE ∷ cs) (FALSE ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , FALSE ∷ p1 , p2 , cong suc eqn
▷*-split (.NOT ∷ cs) (NOT b ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , NOT b ∷ p1 , p2 , cong suc eqn
▷*-split (.(FETCH x) ∷ cs) (FETCH x ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , FETCH x ∷ p1 , p2 , cong suc eqn
▷*-split (.(STORE x) ∷ cs) (STORE x ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , STORE x ∷ p1 , p2 , cong suc eqn
▷*-split (.NOOP ∷ cs) (NOOP ∷ p) with ▷*-split cs p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , NOOP ∷ p1 , p2 , cong suc eqn
▷*-split (._ ∷ cs){c₂} (BRANCH{ca}{cb}{._}{t}{e} ∷ p)
  rewrite sym $ LM.assoc (ifBool t then ca else cb) cs c₂
  with ▷*-split ((ifBool t then ca else cb) <> cs) p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , BRANCH ∷ p1 , p2 , cong suc eqn
▷*-split (._ ∷ cs){c₁} (LOOP{ca}{cb}{._}{e}{s} ∷ p)
  rewrite sym $ LM.assoc ca (BRANCH (cb ∷ʳ LOOP ca cb) (NOOP ∷ []) ∷ cs) c₁
  with ▷*-split (ca <> (BRANCH (cb ∷ʳ LOOP ca cb) (NOOP ∷ []) ∷ cs)) p
... | s'' , e'' , p1 , p2 , eqn = s'' , e'' , LOOP ∷ p1 , p2 , cong suc eqn

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
-- Andreas, 2016-05-13 Issue 1973 reported by Nisse
-- Problems with parameters to overloaded projections

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

record R₁ : Set₁ where
  field
    f : Set

open R₁ public

postulate
  F : ∀ {a} → Set a → Set a

module M (_ : Set₁) where

  record R₂ a (G : Set a → Set a) (A : Set a) : Set a where
    field
      f : G A

  open R₂ public

open module N = M Set using (f)

works : ∀ a (A : Set a) → N.R₂ a F A → F A
works a A x = N.R₂.f x

-- WAS:
-- a F !=< F A of type Set
-- when checking that the expression f x has type F A

ill-formed-term-in-error-message : ∀ a (A : Set a) → N.R₂ a F A → F A
ill-formed-term-in-error-message a A x = f x

-- What Agda did here is to copy parameters from the reduced record type
--   M.R₂ Set a F A
-- to the unreduced projection
--   N.R₂.f
-- The number of projections (3) was queried from N.R₂.f, but the projections
-- were taken from  M.R₂ Set a F A.
-- Now, take the original version of the projection,
--   M.R₂.f
-- which accepts 4 parameters, and these are the ones provided by  M.R₂ Set a F A.

-- WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:93

internal-error : (A : Set) → N.R₂ _ F A → F A
internal-error A x = f x

-- should work now.


text:
module Category.Monad.Reader {i}{I : Set i} where

open import Category.Applicative.Indexed
open import Category.Monad
open import Category.Monad.Predicate
open import Relation.Unary
open import Relation.Unary.PredicateTransformer
open import Data.Product
open import Data.Unit
open import Function
open import Level

ReaderT : Set i → Pt I i → Pt I i
ReaderT E M P = λ i → E → M P i

module ReaderT (E : Set i){M : Pt I i}(Mon : RawPMonad {ℓ = i} M) where

  module Mon = RawPMonad Mon

  open RawPMonad
  reader : RawPMonad {ℓ = i} (ReaderT E M)
  return? reader x e = Mon.return? x
  _=<?_  reader f m e = (λ x → f x e) Mon.=<? m e

  -- operations
  ask : ∀ {i : I} → ReaderT E M (λ _ → E) i
  ask E = return? Mon E

  asks : ∀ {A}{i : I} → (E → A i) → ReaderT E M A i
  asks f E = return? Mon (f E)

  local : ∀ {E'}{A}{i : I} → E' → ReaderT E' M A i → ReaderT E M A i
  local e' m = λ _ → m e'


text:
-- Andreas, 2019-03-25, issue #3647, reported and bisected by nad.
-- Regression introduced in refactoring a78d7f54e447cadf039da81b50ff40c81aa93909.

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v 90 #-}

postulate
  A : Set
  P : A → Set

Q : A → A → Set
Q _ x = P x

record R (P : A → Set) : Set where
  field f : (x : A) → P x → P x

open R ⦃ … ⦄

module M {x : A} where

  instance
    postulate
      r₁ r₂ : R (Q x)

postulate
  q₁ : (x : A) → P x

q₂ : (x : A) → P x
q₂ x = f _ (q₁ x)

-- WAS: internal error.

-- Should succeed with unsolved metas.


text:
module Test where

open import IO using (run; putStrLn)
import IO.Primitive as Prim using (IO)
open import Data.Nat.Show as Nat using (show)
open import Data.Unit using (⊤)

open import Vector

main : Prim.IO ⊤
main = run (putStrLn (Nat.show (length gravity₂)))

max_stars_repo_name: neosimsim/merkdas

max_issues_repo_name: neosimsim/merkdas

max_forks_repo_name: neosimsim/merkdas


text:
module Logic.Linear where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec using (Vec; []; _∷_; _++_; map)
open import Data.Empty using (⊥)

-- Operator precedences.
infix 10 _^⊥ e?_ e!_
infixl 9 _⊗_ _&_
infixl 8 _⊕_ _⅋_
infixl 7 _⊸_
infixl 6 _≡_

-- Primitive linear propositions.
data LinearProp {a} (A : Set a) : Set a where
  atom : A → LinearProp A
  atom^⊥ : A → LinearProp A
  _⊗_ : LinearProp A → LinearProp A → LinearProp A
  _⊕_ : LinearProp A → LinearProp A → LinearProp A
  _&_ : LinearProp A → LinearProp A → LinearProp A
  _⅋_ : LinearProp A → LinearProp A → LinearProp A
  u0 : LinearProp A
  u1 : LinearProp A
  u⊥ : LinearProp A
  u⊤ : LinearProp A
  e!_ : LinearProp A → LinearProp A
  e?_ : LinearProp A → LinearProp A

-- The equivalent of the propositional negation, called "dual".
_^⊥ : ∀ {a} {A : Set a} → LinearProp A → LinearProp A
(atom p) ^⊥ = atom^⊥ p
(atom^⊥ p) ^⊥ = atom p
(p ⊗ q) ^⊥ = (p ^⊥) ⅋ (q ^⊥)
(p ⊕ q) ^⊥ = (p ^⊥) & (q ^⊥)
(p ⅋ q) ^⊥ = (p ^⊥) ⊗ (q ^⊥)
(p & q) ^⊥ = (p ^⊥) ⊕ (q ^⊥)
u1 ^⊥ = u⊥
u0 ^⊥ = u⊤
u⊥ ^⊥ = u1
u⊤ ^⊥ = u0
(e! p) ^⊥ = e? (p ^⊥)
(e? p) ^⊥ = e! (p ^⊥)

-- The linear implication, also called "lollipop operator".
_⊸_ : ∀ {a} {A : Set a} → LinearProp A → LinearProp A → LinearProp A
p ⊸ q = p ^⊥ ⅋ q

-- The equivalent of the propositional equivalence (lmao).
_≡_ : ∀ {a} {A : Set a} → LinearProp A → LinearProp A → LinearProp A
p ≡ q = (p ⊸ q) & (q ⊸ p)

-- Swaps two elements with two given positions. Just a helper of `swap`.
swap-vec : ∀ {a} {A : Set a}
          {n : ℕ} →
          Fin n →
          Fin n →
          Vec A n →
          Vec A n
swap-vec = do-swap where
  insert : ∀ {a} {A : Set a}
              {n : ℕ} →
              A →
              Vec A (suc n) →
              Vec A (suc (suc n))
  insert y (x ∷ xs) = x ∷ y ∷ xs
  swap-first : ∀ {a} {A : Set a}
              {n : ℕ} →
              Fin n →
              Vec A n →
              Vec A n
  swap-first zero xs = xs
  swap-first (suc zero) (x ∷ y ∷ xs) = y ∷ x ∷ xs
  swap-first (suc m) (x ∷ y ∷ xs) = insert y (swap-first m (x ∷ xs))
  do-swap : ∀ {a} {A : Set a}
            {n : ℕ} →
            Fin n →
            Fin n →
            Vec A n →
            Vec A n
  do-swap zero zero xs = xs
  do-swap zero (suc m) xs = swap-first (suc m) xs
  do-swap (suc m) zero xs = swap-first (suc m) xs
  do-swap (suc k) (suc m) (x ∷ xs) = x ∷ do-swap k m xs

-- List of inference rules.
-- The S parameter is an axiom scheme.
-- To prove somthing, it must be the only proposition in the sequent.
data _⊢_ {a}
         {A : Set a}
         (S : LinearProp A → Set a) :
         {n : ℕ} →
         Vec (LinearProp A) n
         → Set a
         where

  empty : S ⊢ []

  axiom : {p : LinearProp A} → S p → S ⊢ (p ∷ [])

  swap : {n : ℕ}
         {ps : Vec (LinearProp A) n} →
         (i j : Fin n) →
         S ⊢ ps →
         S ⊢ (swap-vec i j ps)

  ^⊥-i : (p : LinearProp A) → S ⊢ (p ∷ p ^⊥ ∷ [])

  ^⊥-e : {p : LinearProp A}
        {m n : ℕ}
        {ps : Vec (LinearProp A) m} →
        {qs : Vec (LinearProp A) n} →
        S ⊢ (p ∷ ps) →
        S ⊢ (p ^⊥ ∷ qs) →
        S ⊢ (ps ++ qs)

  ⊗-i : {p q : LinearProp A}
        {m n : ℕ}
        {ps : Vec (LinearProp A) m} →
        {qs : Vec (LinearProp A) n} →
        S ⊢ (p ∷ ps) →
        S ⊢ (q ∷ qs) →
        S ⊢ (p ⊗ q ∷ ps ++ qs)

  ⅋-i : {p q : LinearProp A}
        {n : ℕ}
        {ps : Vec (LinearProp A) n} →
        S ⊢ (p ∷ q ∷ ps) →
        S ⊢ (p ⅋ q ∷ ps)

  u1-i : S ⊢ (u1 ∷ [])

  u⊥-i : {n : ℕ} {ps : Vec (LinearProp A) n} → S ⊢ ps →  S ⊢ (u⊥ ∷ ps)

  &-i : {p q : LinearProp A}
        {n : ℕ}
        {ps : Vec (LinearProp A) n} →
        S ⊢ (p ∷ ps) →
        S ⊢ (q ∷ ps) →
        S ⊢ (p & q ∷ ps)

  ⊕-i₁ : {p q : LinearProp A}
         {n : ℕ}
         {ps : Vec (LinearProp A) n} →
         S ⊢ (p ∷ ps) →
         S ⊢ (p ⊕ q ∷ ps)

  ⊕-i₂ : {p q : LinearProp A}
         {n : ℕ}
         {ps : Vec (LinearProp A) n} →
         S ⊢ (p ∷ ps) →
         S ⊢ (q ⊕ p ∷ ps)

  u⊤-i : {n : ℕ}
        {ps : Vec (LinearProp A) n} →
        S ⊢ (u⊤ ∷ ps)

  e?-i₁ : {p : LinearProp A}
         {n : ℕ}
         {ps : Vec (LinearProp A) n} →
         S ⊢ ps →
         S ⊢ (e? p ∷ ps)

  e?-i₂ : {p : LinearProp A}
         {n : ℕ}
         {ps : Vec (LinearProp A) n} →
         S ⊢ (p ∷ ps) →
         S ⊢ (e? p ∷ ps)

  e?-e : {p : LinearProp A}
         {n : ℕ}
         {ps : Vec (LinearProp A) n} →
         S ⊢ (e? p ∷ e? p ∷ ps) →
         S ⊢ (e? p ∷ ps)

  e!-i : {p : LinearProp A}
         {n : ℕ}
         {ps : Vec (LinearProp A) n} →
         S ⊢ (p ∷ map e?_ ps) →
         S ⊢ (e! p ∷ map e?_ ps)

-- Empty axiom scheme.
data NoAxioms {a} {A : Set a} : LinearProp A → Set a where

-- Just a helper to hint something has been proven.
Proof : ∀ {a} {A : Set a} → (LinearProp A → Set a) → LinearProp A → Set a
Proof S p = S ⊢ (p ∷ [])

max_stars_repo_name: brunoczim/linear-logic

max_issues_repo_name: brunoczim/linear-logic

max_forks_repo_name: brunoczim/linear-logic


text:
{-# OPTIONS --without-K #-}
module well-typed-syntax-interpreter where
open import common public
open import well-typed-syntax
import well-typed-syntax-pre-interpreter
open import well-typed-syntax-eq-dec

max-level : Level
max-level = well-typed-syntax-pre-interpreter.max-level

Context⇓ : (Γ : Context) → Set (lsuc max-level)
Context⇓ = well-typed-syntax-pre-interpreter.inner.Context⇓
           (λ ℓ P Γ' dummy val → context-pick-if {P = P} dummy val)
           (λ ℓ P dummy val → context-pick-if-refl {P = P} {dummy})

Typ⇓ : {Γ : Context} → Typ Γ → Context⇓ Γ → Set max-level
Typ⇓ = well-typed-syntax-pre-interpreter.inner.Typ⇓
       (λ ℓ P Γ' dummy val → context-pick-if {P = P} dummy val)
       (λ ℓ P dummy val → context-pick-if-refl {P = P} {dummy})

Term⇓ : ∀ {Γ : Context} {T : Typ Γ} → Term T → (Γ⇓ : Context⇓ Γ) → Typ⇓ T Γ⇓
Term⇓ = well-typed-syntax-pre-interpreter.inner.Term⇓
        (λ ℓ P Γ' dummy val → context-pick-if {P = P} dummy val)
        (λ ℓ P dummy val → context-pick-if-refl {P = P} {dummy})

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
{-# OPTIONS --without-K #-}

module ForAmr where

open import Level using (Level)

open import Relation.Nullary.Core
open import Data.Vec
  using (Vec; tabulate; []; _∷_; lookup; allFin)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import  Data.Vec.Properties
  using (lookup-++-≥; lookup∘tabulate; tabulate-∘; tabulate∘lookup; map-cong)
open import Function using (id;_∘_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong; cong₂; subst; proof-irrelevance;
             _≗_; module ≡-Reasoning)
open import Data.Nat using (ℕ; zero; suc; _+_; z≤n; _≟_)
open import Data.Nat.Properties.Simple using (+-comm)
open import Data.Nat.Properties using (m≤m+n)
open import Data.Fin using (Fin; zero; suc; inject+; raise; reduce≥; toℕ; fromℕ≤)
open import Data.Fin.Properties using (toℕ-injective; toℕ-raise; toℕ-fromℕ≤)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (proj₁)
open import Function using (flip)

open import Proofs
open import Equiv
open import FinEquiv
open import Cauchy
open import TypeEquiv using (swap₊; swapswap₊)

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

-- and now this is completely obvious.  But not actually needed!
swap+-idemp : {A B : Set} → {m n : ℕ} → (v : Vec (A ⊎ B) (m + n)) →
  swap+ {m} (swap+ {m} v) ≡ v
swap+-idemp v =
  begin (
    tabulate (λ i → swap₊ (tabulate (λ j → swap₊ (v !! j)) !! i))
        ≡⟨ denest-tab-!! swap₊ swap₊ v ⟩
    mapV (swap₊ ∘ swap₊) v
        ≡⟨ map-cong swapswap₊ v ⟩
    mapV id v
        ≡⟨ map-id v ⟩
    v ∎)
  where open ≡-Reasoning

-- because this is 'pointwise', no need for swap+-idemp.
pointwise-swap+v-idemp : {m n : ℕ} → ∀ i →
  lookup (lookup i (swap+v m n)) (swap+v n m) ≡ i
pointwise-swap+v-idemp {m} {n} i =
  let fnm = swapper n m in
  let fmn = swapper m n in
  begin (
    lookup (lookup i (swap+v m n)) (swap+v n m)
      ≡⟨ cong (λ x → lookup x (swap+v n m)) (lookup∘tabulate fmn i) ⟩
    lookup (fmn i) (swap+v n m)
      ≡⟨ lookup∘tabulate fnm (fmn i) ⟩
    fnm (fmn i) -- bingo!
      ≡⟨ cong (fwd ∘ swap₊) (bwd∘fwd~id (swap₊ (bwd {m} i))) ⟩
    fwd (swap₊ (swap₊ (bwd {m} i)))
      ≡⟨ cong fwd (swapswap₊ (bwd {m} i)) ⟩
    fwd (bwd {m} i)
      ≡⟨ fwd∘bwd~id {m} i ⟩
    i ∎ )
  where open ≡-Reasoning

-- this is true, but the above is what is used in practice.
swap+v-idemp : {m n : ℕ} →
  tabulate (λ i → lookup (lookup i (swap+v m n)) (swap+v n m)) ≡ tabulate id
swap+v-idemp {m} = finext (pointwise-swap+v-idemp {m})

---------------------------------------------------------------
-- Everything below here is based on Cauchy as Vec (Fin n) n
-- and might get tossed.  Comment it out for now.

{-
-- the Cauchy version.
swap+c : (m n : ℕ) → Cauchy (m + n)
swap+c m n = subst (λ x → Vec (Fin x) (m + n)) (+-comm n m) (swap+v m n)

-- the action of subst on swap+, pointwise
switch-swap+ : {m n : ℕ} → (i : Fin (m + n)) →
  subst Fin (+-comm n m) (swapper m n i) ≡
  swapper n m (subst Fin (+-comm m n) i)
switch-swap+ {m} {n} i with m ≟ n
switch-swap+ i | yes p = {!!}
switch-swap+ i | no ¬p = {!!}
{-
switch-swap+ {m} {n} i with (toℕ i <? m) | (toℕ (subst Fin (+-comm m n) i) <? n)
switch-swap+ {m} {n} i | yes p | yes q = {!!} {- toℕ-injective (
  begin (
    toℕ (subst Fin (+-comm n m) (raise n (fromℕ≤ p)))
      ≡⟨ toℕ-invariance (raise n (fromℕ≤ p)) (+-comm n m) ⟩
    toℕ (raise n (fromℕ≤ p))
      ≡⟨ toℕ-raise n (fromℕ≤ p) ⟩
    n + toℕ (fromℕ≤ p)
      ≡⟨ cong (_+_ n) (toℕ-fromℕ≤ p) ⟩
    n + toℕ i
      ≡⟨ {!!} ⟩
    m + toℕ (subst Fin (+-comm m n) i)
      ≡⟨ sym (cong (_+_ m) (toℕ-fromℕ≤ q)) ⟩
    m + toℕ (fromℕ≤ q)
      ≡⟨ sym (toℕ-raise m (fromℕ≤ q)) ⟩
    toℕ (raise m (fromℕ≤ q)) ∎))
  where open ≡-Reasoning -}
switch-swap+ i | yes p | no ¬q = {!!}
switch-swap+ i | no ¬p | yes q = {!!}
switch-swap+ i | no ¬p | no ¬q = {!!}
-}

-- the Cauchy version:
pcomp' : ∀ {m n} → Cauchy m → Cauchy n → Cauchy (m + n)
pcomp' α β = mapV fwd (pcomp α β)

-- the action of subst on swap+v
switch-swap : {m n : ℕ} → (i : Fin (m + n)) →
  subst Fin (+-comm n m) ((swap+v m n) !! i) ≡
  (swap+v n m) !! subst Fin (+-comm m n) i
switch-swap {m} {n} i =
  let fnm = swapper n m in
  let fmn = swapper m n in
  begin (
    subst Fin (+-comm n m) ((tabulate fmn) !! i)
      ≡⟨ cong (subst Fin (+-comm n m)) (lookup∘tabulate fmn i) ⟩
    subst Fin (+-comm n m) (fmn i)
      ≡⟨ switch-swap+ {m} i ⟩
    fnm (subst Fin (+-comm m n) i)
      ≡⟨ sym (lookup∘tabulate fnm (subst Fin (+-comm m n) i)) ⟩
    tabulate (fnm) !! subst Fin (+-comm m n) i ∎)
  where open ≡-Reasoning

-- the crucial part for the next theorem:
swap+-idemp' : {m n : ℕ} → ∀ (i : Fin (m + n)) → lookup
      (subst (λ x → Vec (Fin x) (m + n)) (+-comm n m) (swap+v m n) !! i)
      (subst (λ x → Vec (Fin x) (m + n)) (+-comm n m) (swap+v m n))
      ≡ i
swap+-idemp' {m} {n} i =
  let j = subst (λ x → Vec (Fin x) (m + n)) (+-comm n m) (swap+v m n) !! i in
  begin (
    lookup j (subst (λ x → Vec (Fin x) (m + n)) (+-comm n m) (swap+v m n))
      ≡⟨ lookup-subst j (swap+v m n) (+-comm n m) ⟩
    subst Fin (+-comm n m) ((swap+v m n) !! j)
      ≡⟨ cong (λ x → subst Fin (+-comm n m) ((swap+v m n) !! x))
                   (lookup-subst i (swap+v m n) (+-comm n m)) ⟩
    subst Fin (+-comm n m) ((swap+v m n) !! subst Fin (+-comm n m) (swap+v m n !! i))
      ≡⟨ cong (λ x → subst Fin (+-comm n m) ((swap+v m n) !! x))
                   (switch-swap {m} i) ⟩
    subst Fin (+-comm n m) ((swap+v m n) !! (swap+v n m !! subst Fin (+-comm m n) i))
      ≡⟨ cong (subst Fin (+-comm n m)) (pointwise-swap+v-idemp {n} (subst Fin (+-comm m n) i)) ⟩
    subst Fin (+-comm n m) (subst Fin (+-comm m n) i)
      ≡⟨ subst-subst (+-comm n m) (+-comm m n)
                              (proof-irrelevance (sym (+-comm n m)) (+-comm m n)) i ⟩
    i ∎)
  where open ≡-Reasoning

-- and let's see what that does to the Cauchy version:
swap+c-idemp : {m n : ℕ} → scompcauchy (swap+c m n) (swap+c m n) ≡ allFin (m + n)
swap+c-idemp  {m} {n} = finext (swap+-idemp' {m} {n})
-}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- Parser indices
------------------------------------------------------------------------

module StructurallyRecursiveDescentParsing.Index where

open import Data.Bool
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Function

------------------------------------------------------------------------
-- Indices to the parser type

-- Does the parser accept empty strings?

Empty : Set
Empty = Bool

-- The proper left corners of the parser, represented as a tree. See
-- StructurallyRecursiveDescentParsing.Grammar.

infix 5 _∪_

data Corners : Set where
  ε   : Corners
  _∪_ : (c₁ c₂ : Corners) → Corners

-- The index type.

infix 4 _◇_

record Index : Set where
  constructor _◇_
  field
    empty   : Empty
    corners : Corners

open Index public

-- Type signature for non-terminals. The second argument is the result
-- type.

NonTerminalType : Set2
NonTerminalType = Index → Set → Set1

------------------------------------------------------------------------
-- Operations on indices

infixr 50 _·_
infixr 40 _∥_

0I : Index
0I = false ◇ ε

1I : Index
1I = true ◇ ε

_∥_ : Index → Index → Index
i₁ ∥ i₂ = empty i₁ ∨ empty i₂ ◇ corners i₁ ∪ corners i₂

_·_ : Index → Index → Index
i₁ · i₂ = (empty i₁ ∧ empty i₂)
          ◇
          (if empty i₁ then corners i₁ ∪ corners i₂
                       else corners i₁)

------------------------------------------------------------------------
-- Testing indices for equality

infix 15 _Index-≟_ _Corners-≟_

private

  drop-∪₁ : ∀ {c₁ c₂ c₃ c₄} → c₁ ∪ c₂ ≡ c₃ ∪ c₄ → c₁ ≡ c₃
  drop-∪₁ refl = refl

  drop-∪₂ : ∀ {c₁ c₂ c₃ c₄} → c₁ ∪ c₂ ≡ c₃ ∪ c₄ → c₂ ≡ c₄
  drop-∪₂ refl = refl

_Corners-≟_ : Decidable {A = Corners} _≡_
ε         Corners-≟ ε           = yes refl
(c₁ ∪ c₂) Corners-≟ ( c₃ ∪  c₄) with c₁ Corners-≟ c₃ | c₂ Corners-≟ c₄
(c₁ ∪ c₂) Corners-≟ (.c₁ ∪ .c₂) | yes refl | yes refl = yes refl
(c₁ ∪ c₂) Corners-≟ ( c₃ ∪  c₄) | no  ¬c₁≡c₂ | _          = no (¬c₁≡c₂ ∘ drop-∪₁)
(c₁ ∪ c₂) Corners-≟ ( c₃ ∪  c₄) | _          | no  ¬c₁≡c₂ = no (¬c₁≡c₂ ∘ drop-∪₂)
ε         Corners-≟ (_ ∪ _)     = no λ()
(_ ∪ _)   Corners-≟ ε           = no λ()

_Index-≟_ : Decidable {A = Index} _≡_
i₁ Index-≟ i₂ with empty i₁ ≟ empty i₂
                 | corners i₁ Corners-≟ corners i₂
... | yes e₁≡e₂ | yes c₁≡c₂ = yes (cong₂ _◇_ e₁≡e₂ c₁≡c₂)
... | no ¬e₁≡e₂ | _         = no (¬e₁≡e₂ ∘ cong empty)
... | _         | no ¬c₁≡c₂ = no (¬c₁≡c₂ ∘ cong corners)

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module LF where

data Zero : Set where

record One : Set where

★ : One
★ = record {}

One-elim : (C : One -> Set) -> C ★ -> (a : One) -> C a
One-elim C h _ = h

One-elim₁ : (C : One -> Set1) -> C ★ -> (a : One) -> C a
One-elim₁ C h _ = h

-- data One' : Set1 where
--   ★' : One'

data Two : Set where
  ★₀ : Two
  ★₁ : Two

case₂ : {A : Set1} -> Two -> A -> A -> A
case₂ ★₀ x y = x
case₂ ★₁ x y = y

data _+_ (A : Set)(B : Set) : Set where
  inl : A -> A + B
  inr : B -> A + B

record _×_ (A : Set)(B : A -> Set) : Set where
  field
    π₀ : A
    π₁ : B π₀

open _×_ public

_,_ : {A : Set}{B : A -> Set}(a : A) -> B a -> A × B
x , y = record { π₀ = x; π₁ = y }

_*_ : (A B : Set) -> Set
A * B = A × \_ -> B

-- data _×'_ (A : Set)(B : A -> Set1) : Set1 where
--   _,'_ : (a : A) -> B a -> A ×' B
--
-- π₀' : {A : Set}{B : A -> Set1} -> A ×' B -> A
-- π₀' (a ,' b) = a
--
-- π₁' : {A : Set}{B : A -> Set1}(p : A ×' B) -> B (π₀' p)
-- π₁' (a ,' b) = b

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- We show by allowing the reminder of integer division to be
-- negative, we can get more precise estimation of the rank of the
-- remainder: rank reminder ≤ (rank divisor) / 2.

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

module Integer.EucDomain2 where

-- ----------------------------------------------------------------------
-- ℕ is an "Euclidean SemiRing".
module NatESR where
  -- ℕ satisfy the euc-eq and euc-rank property with the usual div and
  -- mod function. Still we need to do the translation from non-equality
  -- to NonZero predicate.

  -- imports form stdlib.
  open import Relation.Nullary using (¬_)
  open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

  open import Data.Nat as Nat using (ℕ ; zero ; suc)

  import Data.Nat.DivMod as NDM
  import Data.Nat.Properties as NatP

  -- imports from local.
  open import Instances

  -- We already make ℕ an instance of Rank. For convinence we restate it
  -- here.
  rank' : ℕ -> ℕ
  rank' x = x

  -- Division with the annoying translation from ¬ d ≡ 0 to NonZero
  -- predicate.
  div : ∀ (n d : ℕ) -> ¬ d ≡ 0 -> ℕ
  div n zero n0 with n0 refl
  ... | ()
  div n (suc d) n0 = NDM._/_ n (suc d)

  -- Reminder.
  mod : ∀ (n d : ℕ) -> ¬ d ≡ 0 -> ℕ
  mod n zero n0 with n0 refl
  ... | ()
  mod n (suc d) n0 = NDM._%_ n (suc d)

  -- Dividend = reminder + quotient * divisor.
  euc-eq : ∀ (n d : ℕ) (n0 : ¬ d ≡ 0) ->
               let r = mod n d n0 in let q = div n d n0 in
               n ≡ r + q * d
  euc-eq n zero n0 with n0 refl
  ... | ()
  euc-eq n (suc d) n0 = NDM.m≡m%n+[m/n]*n n (suc d)

  -- rank reminder < rank divisor.
  euc-rank : ∀ (n d : ℕ) (n0 : ¬ d ≡ 0) ->
               let r = mod n d n0 in let q = div n d n0 in
               rank r < rank d
  euc-rank n zero n0 with n0 refl
  ... | ()
  euc-rank n (suc d) n0 = NDM.m%n<n n (suc d)

-- ----------------------------------------------------------------------
-- Allow Integer division to have negative reminder

-- Let n, d be integers and d nonzero, by the usual divison with
-- reminder we have q, r such that n = r + q * d and ∣ r ∣ < ∣ d ∣.
-- What we want is q' and r' such that n = r' + q' * d and ∣ r' ∣ ≤ ∣
-- d ∣ / 2. Asssume d > 0, an easy calculation shows if ∣ r ∣ ≤ ∣ d ∣
-- / 2, we let q' = q and r' = r, and if ∣ r ∣ > ∣ d ∣ / 2, we let q'
-- = q + 1 and r' = r - d. The case when d < 0 is similar.

-- imports from stdlib.
open import Relation.Nullary using (yes ; no ; ¬_)
open import Relation.Binary.PropositionalEquality as PE
  using (_≡_ ; refl ; sym ; cong ; trans)

open import Data.Empty using (⊥-elim)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
open import Data.Bool using (T ; not)
open import Data.Nat as Nat using (ℕ ; suc ; s≤s ; zero ; z≤n)
import Data.Nat.DivMod as NDM
import Data.Nat.Properties as NatP
open import Data.Integer as Int
  using (ℤ ; ∣_∣ ; +_ ; +[1+_] ; -[1+_] ; 1ℤ ; _◃_ ; +<+ ; -<- ; -≤- ; -<+ ; -≤+ ; +≤+ ; 0ℤ)
import Data.Integer.Properties as IntP
open import Data.Integer.DivMod
  using (_div_ ; _mod_ ; a≡a%n+[a/n]*n ; n%d<d)
open import Data.Integer.Solver

-- imports from local.
open import Instances

-- Aother integer division allowing negative reminder.
div' : ∀ (n d : ℤ) -> ¬ d ≡ 0ℤ -> ℤ
div' n (+_ zero) n0 with n0 refl
... | ()
div' n d@(+[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2
... | yes pr = n div d
... | no np =  1ℤ + n div d
div' n d@(-[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2
... | yes pr = n div d
... | no np =  - 1ℤ + n div d

-- Another integer mod allowing negative reminder.
mod' : ∀ (n d : ℤ) -> ¬ d ≡ 0ℤ -> ℤ
mod' n (+_ zero) n0 with n0 refl
... | ()
mod' n d@(+[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2
... | yes pr = + (n mod d)
... | no np =  + (n mod d) - d
mod' n d@(-[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2
... | yes pr = + (n mod d)
... | no np =  + (n mod d) + d

-- Dividend = reminder + quotient * divisor.
euc-eq' : ∀ (n d : ℤ) (n0 : ¬ d ≡ 0ℤ) ->
             let r = mod' n d n0 in let q = div' n d n0 in
             n ≡ r + q * d
euc-eq' n (+_ zero) n0 with n0 refl
... | ()
euc-eq' n d@(+[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2
... | yes pr = a≡a%n+[a/n]*n n d
... | no np =  claim
  where
    claim : n ≡ (+ (n mod d) - d) + (1ℤ + n div d) * d
    claim = begin
      n ≡⟨  a≡a%n+[a/n]*n n d  ⟩
      + (n mod d) + (n div d) * d ≡⟨ solve 3 (\ x y z -> x :+ y :* z := x :- z :+ (con 1ℤ :+ y) :* z) refl (+ (n mod d)) (n div d) d ⟩
      (+ (n mod d) - d) + (1ℤ + n div d) * d ∎
        where
          open +-*-Solver
          open PE.≡-Reasoning
euc-eq' n d@(-[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2
... | yes pr = a≡a%n+[a/n]*n n d
... | no np = claim
  where
    claim : n ≡ (+ (n mod d) + d) + (- 1ℤ + n div d) * d
    claim = begin
      n ≡⟨  a≡a%n+[a/n]*n n d  ⟩
      + (n mod d) + (n div d) * d ≡⟨ solve 3 (\ x y z -> x :+ y :* z := x :+ z :+ (con (- 1ℤ) :+ y) :* z) refl (+ (n mod d)) (n div d) d ⟩
      (+ (n mod d) + d) + (- 1ℤ + n div d) * d ∎
        where
          open +-*-Solver
          open PE.≡-Reasoning

-- rank reminder ≤ (rank divisor) / 2.
euc-rank' : ∀ (n d : ℤ) (n0 : ¬ d ≡ 0ℤ) ->
             let r = mod' n d n0 in let q = div' n d n0 in
             ∣ r ∣ ≤ ∣ d ∣ / 2
euc-rank' n (+_ zero) n0 with n0 refl
... | ()
euc-rank' n d@(+[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2
... | yes pr = pr
... | no ¬p =  claim
  where
    r = + (n mod d) - d

    d≠0 : ¬ ∣ d ∣ ≡ 0
    d≠0 = λ ()

    -- We follow the steps to show ∣ r ∣ ≤ ∣ d ∣ / 2, in the current case, i.e. ∣
    -- n % d - d ∣ ≤ d / 2. We follows the steps below:
    -- 1) d / 2 < n % d
    -- 2) d / 2 - d < n % d - d
    -- 3) n % d - d < 0, hence d / 2 - d < n % d - d < 0
    -- 4) ∣ d / 2 - d ∣ > ∣ n % d - d ∣
    -- 5)  d / 2 - d ≡ - d / 2 or d / 2 - d  ≡ - (d / 2 + 1)
    -- 6) ∣ d / 2 - d ∣ ≡ d / 2 or ∣ d / 2 - d ∣ ≡ d / 2 + 1
    -- 7) d / 2 > ∣ n % d - d ∣ or d / 2 + 1 > ∣ n % d - d ∣
    -- 8) d / 2 ≥ ∣ n % d - d ∣

    -- By negate ¬p, we can show ∣ d ∣ / 2 < n mod d.
    -- By negation of ¬p (we are using the decidable order).
    open import Relation.Binary using (tri< ; tri≈ ; tri>)
    step1 : ∣ d ∣ / 2 < n mod d
    step1 with NatP.<-cmp (n mod d) (∣ d ∣ / 2)
    ... | tri< a ¬b ¬c = ⊥-elim (¬p (NatP.<⇒≤ a))
    ... | tri≈ ¬a b ¬c = ⊥-elim (¬p (NatP.≤-reflexive b))
    ... | tri> ¬a ¬b c = c
      where
        notle : ¬ (n mod d ≤ ∣ d ∣ / 2)
        notle = ¬p

    -- Step 2. ∣ d ∣ / 2 - ∣ d ∣ < n mod d - ∣ d ∣. Subtracting ∣ d ∣
    -- from both sides of step1 preserves the inequality.
    step2 : + (∣ d ∣ / 2) - + ∣ d ∣ < + (n mod d) - + ∣ d ∣
    step2 = IntP.+-monoʳ-< (- (+ ∣ d ∣)) (+<+ step1)

    -- Step 3. n mod d - ∣ d ∣ < 0

    -- Some auxillary.
    n-n=0 : ∀ {n} -> n - n ≡ 0ℤ
    n-n=0 {n} = IntP.+-inverseʳ n

    step3 : + (n mod d) - (+ ∣ d ∣) < 0ℤ
    step3 rewrite (sym (n-n=0 {+ ∣ d ∣})) = r-d<d-d
      where
        -- n mod d < ∣ d ∣, by Euclidean property of integers.
        r<∣d∣ : + (n mod d) < + ∣ d ∣
        r<∣d∣ = +<+ (n%d<d n d)

        -- Substract ∣ d ∣ on both sides of n mod d < ∣ d ∣.
        r-d<d-d : + (n mod d) - (+ ∣ d ∣) < (+ ∣ d ∣) - (+ ∣ d ∣)
        r-d<d-d = IntP.+-monoʳ-< (- + ∣ d ∣) r<∣d∣

    -- Step 4. ∣ d / 2 - d ∣ > ∣ n % d - d ∣. By 2, we have
    --  d / 2 - d  <  n % d - d < 0. By taking absolute values, we show
    -- ∣ d / 2 - d ∣ > ∣ n % d - d ∣.

    -- Some lemmas about take absolute value of negative and nonpositive
    -- numbers.
    lemma-∣neg∣ : ∀ {a : ℤ} -> a < 0ℤ -> + ∣ a ∣ ≡ - a
    lemma-∣neg∣ -<+ = refl

    lemma-∣non-pos∣ : ∀ {a : ℤ} -> a ≤ 0ℤ -> + ∣ a ∣ ≡ - a
    lemma-∣non-pos∣ {.(-[1+ _ ])} -≤+ = refl
    lemma-∣non-pos∣ {.(+ zero)} (+≤+ z≤n) = refl

    -- The injection of natural numbers into integers reflect order.
    lemma-inj-reflect-ord : ∀ {a b} -> + a < + b -> a < b
    lemma-inj-reflect-ord (+<+ m<n) = m<n

    lemma-inj-reflect-ord' : ∀ {a b} -> + a ≤ + b -> a ≤ b
    lemma-inj-reflect-ord' (+≤+ m<n) = m<n

    -- Taking absolute value on both sides of a strict inequality of
    -- negative numbers (can relax this to non-positive numbers)
    -- reverses the order.
    lemma-∣neg<neg∣ : ∀ {a b} -> a < 0ℤ -> b < a -> ∣ a ∣ < ∣ b ∣
    lemma-∣neg<neg∣ {a} {b} a<0 b<a = lemma-inj-reflect-ord claim where
      0<b : b < 0ℤ
      0<b = IntP.<-trans b<a a<0
      claim : (+ ∣ a ∣) < (+ ∣ b ∣)
      claim = begin-strict
        + ∣ a ∣              ≡⟨ lemma-∣neg∣ {a} a<0  ⟩
        - a                 <⟨ IntP.neg-mono-< b<a  ⟩
        - b                 ≡⟨ sym (lemma-∣neg∣ 0<b)  ⟩
        + ∣ b ∣  ∎
          where open IntP.≤-Reasoning

    -- Goal step4 achieved.
    step4 : ∣ + (n mod d) - d ∣ < ∣ + (∣ d ∣ / 2) - d ∣
    step4 = lemma-∣neg<neg∣ step3 step2

    -- Step 5. d / 2 - d ≡ - d / 2 or d / 2 - d ≡ - (d / 2 + 1)

    -- Natural number version of Step 5.
    step5-nat : ∣ d ∣ / 2 + ∣ d ∣ / 2 ≡ ∣ d ∣ ⊎ suc (∣ d ∣  / 2 + ∣ d ∣  / 2) ≡ ∣ d ∣
    step5-nat = lemma-div-by-2 ∣ d ∣
      where
        -- An easy and useful fact.
        *2+ : ∀ {a} -> a * 2 ≡ a + a
        *2+ {zero} = refl
        *2+ {suc a} rewrite *2+ {a} | NatP.+-comm a (suc a) = refl

        -- Either d / 2 + d / 2 ≡ d or d / 2 + d / 2 + 1 ≡ d.
        lemma-div-by-2 : ∀ d -> let hd = d / 2 in
                hd + hd ≡ d ⊎ suc (hd + hd) ≡ d
        lemma-div-by-2 d with d / 2 | d % 2 | NatESR.euc-eq d 2 (λ { ()}) | NatESR.euc-rank d 2 (λ { ()})
        ... | hd | zero | proj₁₁ | pr rewrite *2+ {hd} = inj₁ (sym proj₁₁)
        ... | hd | suc zero | proj₁₁ | pr  rewrite *2+ {hd} = inj₂ (sym proj₁₁)
        ... | hd | suc (suc r₁) | proj₁₁ | pr =  ⊥-elim ((c1 r₁) pr )
          where
            c1  : ∀ a -> ¬ (suc (suc (suc a)) ≤ 2)
            c1 a = λ { (s≤s (s≤s ()))}

    -- Next we need inject naturals to integers. We do the two
    -- identities separately.

    -- Step 5a. If (d / 2) + (d / 2) ≡ d, we show d / 2 - d ≡ - d / 2.
    step5a : ∀ d -> (d / 2) + (d / 2) ≡ d -> let -_ = λ x -> - (+ x) in
               + (d / 2) - (+ d) ≡ - (d / 2)
    step5a d hyp = sym claim4
      where
        open PE.≡-Reasoning
        claim : + (d / 2 + d / 2)  ≡  + d
        claim = cong +_ hyp

        claim2 : + (d / 2)  +  + (d / 2) ≡  + d
        claim2 = begin
          + (d / 2)  +  + (d / 2) ≡⟨ IntP.pos-+-commute (d / 2) (d / 2) ⟩
          + (d / 2 + d / 2) ≡⟨ cong +_ hyp ⟩
          + d ∎

        claim3 :  + (d / 2)  ≡  + d - + (d / 2)
        claim3 = begin
          + (d / 2)   ≡⟨ (solve 1 (λ a -> a := a :+ a :- a) refl) (+ (d / 2))  ⟩
          + (d / 2) +  + (d / 2) - + (d / 2) ≡⟨ cong (_- + (d / 2)) claim2 ⟩
          + d - + (d / 2) ∎
            where open +-*-Solver

        claim4 : let -_ = λ x -> - (+ x) in
                 - (d / 2)  ≡  + (d / 2) - + d
        claim4 =  begin
          - (+ (d / 2))   ≡⟨ cong -_ claim3 ⟩
          - (+ d - + (d / 2)) ≡⟨ (solve 2 (λ a b -> :- (a :- b) := b :- a) refl) (+ d) (+ (d / 2)) ⟩
          + (d / 2) - + d ∎
            where open +-*-Solver

    -- Step 5b. If (d / 2) + (d / 2) + 1 ≡ d, we show d / 2 - d ≡ - (d
    -- / 2 + 1). (Note that we change the sign of the equality)
    step5b : ∀ d -> suc ((d / 2) + (d / 2)) ≡ d -> let -_ = λ x -> - (+ x) in
              (+ d) - + (d / 2) ≡ + (d / 2) + 1ℤ
    step5b d hyp = begin
          + d - + (d / 2)  ≡⟨ cong (λ x → + x - + (d / 2)) (sym hyp) ⟩
          + (suc (d / 2 + d / 2))  - + (d / 2) ≡⟨ refl ⟩
          + (1 + (d / 2 + d / 2))  - + (d / 2) ≡⟨ cong (_- + (d / 2)) (IntP.pos-+-commute 1 (d / 2 + d / 2)) ⟩
          + 1 + + (d / 2 + d / 2) - + (d / 2) ≡⟨ cong (λ x → + 1 + x - + (d / 2)) (IntP.pos-+-commute (d / 2) (d / 2)) ⟩
          + 1 +  + (d / 2) + + (d / 2) - + (d / 2) ≡⟨ solve 1 (λ x → (con 1ℤ) :+ (x :+ x) :- x := x :+ con 1ℤ) refl (+ (d / 2)) ⟩
          + (d / 2) + 1ℤ ∎
            where
              open +-*-Solver
              open PE.≡-Reasoning

    -- Goal 5.
    step5 : let -_ = λ x -> - (+ x) in
        + (∣ d ∣ / 2) - d ≡ - (∣ d ∣ / 2) ⊎ d - + (∣ d ∣ / 2) ≡ + (∣ d ∣ / 2) + 1ℤ
    step5 with step5-nat
    ... | inj₁ x = inj₁ (step5a ∣ d ∣ x)
    ... | inj₂ y = inj₂ (step5b ∣ d ∣ y)

    -- Step 6. ∣ d / 2 - d ∣ ≡ d / 2 or ∣ d / 2 - d ∣ ≡ d / 2 + 1
    step6 : let -_ = λ x -> - (+ x) in
       ∣ + (∣ d ∣ / 2) - d ∣ ≡ ∣ d ∣ / 2 ⊎ ∣ d - + (∣ d ∣ / 2) ∣ ≡ ∣ d ∣ / 2 + 1
    step6 with step5
    ... | inj₁ x rewrite x = inj₁ (trans ∣-d/2∣≡∣d/2∣ ∣d/2∣≡d/2)
      where
        ∣-d/2∣≡∣d/2∣ : ∣ - (+ (∣ d ∣ / 2)) ∣ ≡ ∣ + (∣ d ∣ / 2) ∣
        ∣-d/2∣≡∣d/2∣ = IntP.∣-i∣≡∣i∣ (+ (∣ d ∣ / 2))
        ∣d/2∣≡d/2 : ∣ + (∣ d ∣ / 2) ∣ ≡ (∣ d ∣ / 2)
        ∣d/2∣≡d/2 = refl
    ... | inj₂ y rewrite y = inj₂ claim
      where
        claim : ∣ + (∣ d ∣ / 2) + 1ℤ ∣ ≡ ∣ d ∣ / 2 + 1
        claim = begin
          ∣ + (∣ d ∣ / 2) + 1ℤ ∣ ≡⟨ refl ⟩
          ∣ + ((∣ d ∣ / 2) + 1) ∣ ≡⟨ refl ⟩
          ∣ d ∣ / 2  + 1 ∎
            where
              open PE.≡-Reasoning

    -- Step 7. d / 2 > ∣ n % d - d ∣ or d / 2 + 1 > ∣ n % d - d ∣
    step7 : ∣ + (n mod d) - d ∣ < ∣ d ∣ / 2 ⊎ ∣ + (n mod d) - d ∣ < ∣ d ∣ / 2 + 1
    step7 with step6
    ... | inj₁ x = inj₁ claim
      where
        claim : ∣ + (n mod d) - d ∣ < ∣ d ∣ / 2
        claim = begin-strict
          ∣ + (n mod d) - d ∣ <⟨ step4 ⟩
          ∣ + (∣ d ∣ / 2) - d ∣ ≡⟨ x ⟩
          ∣ d ∣ / 2 ∎
            where
              open NatP.≤-Reasoning
    ... | inj₂ y = inj₂ claim
      where
        claim : ∣ + (n mod d) - d ∣ < ∣ d ∣ / 2 + 1
        claim = begin-strict
          ∣ + (n mod d) - d ∣ <⟨ step4 ⟩
          ∣ + (∣ d ∣ / 2) - d ∣ ≡⟨ IntP.∣i-j∣≡∣j-i∣ (+ (∣ d ∣ / 2)) d ⟩
          ∣ d - + (∣ d ∣ / 2) ∣ ≡⟨ y ⟩
          ∣ d ∣ / 2 + 1 ∎
            where
              open NatP.≤-Reasoning

    -- Step 8. d / 2 ≥ ∣ n % d - d ∣
    step8 : ∣ + (n mod d) - d ∣ ≤ ∣ d ∣ / 2
    step8 with step7
    ... | inj₁ x = NatP.<⇒≤ x
    ... | inj₂ y = m<sucn⇒m≤n claim
      where
        m<sucn⇒m≤n : ∀ {m n : ℕ} → m < suc n → m ≤ n
        m<sucn⇒m≤n (s≤s le) = le

        lemma-+1 : ∀ {a : ℕ} -> a + 1 ≡ suc a
        lemma-+1 {zero} = refl
        lemma-+1 {suc a} = cong suc (lemma-+1 {a})

        claim : ∣ + (n mod d) - d ∣ < suc (∣ d ∣ / 2)
        claim = begin-strict
          ∣ + (n mod d) - d ∣ <⟨ y ⟩
          ∣ d ∣ / 2 + 1 ≡⟨ lemma-+1 ⟩
          suc (∣ d ∣ / 2) ∎
            where
              open NatP.≤-Reasoning

    claim : ∣ r ∣ ≤ ∣ d ∣ / 2
    claim = step8

-- This case is solved by recursive call with argument n and - d.
euc-rank' n d@(-[1+ e ]) n0 with n mod d ≤? ∣ d ∣ / 2 | euc-rank' n (+[1+ e ]) (λ {()})
... | yes pr | hyp  = pr
... | no ¬p | hyp = hyp

-- We can relax the estimation.
euc-rank'' : ∀ (n d : ℤ) (n0 : ¬ d ≡ 0ℤ) ->
               let r = mod' n d n0 in let q = div' n d n0 in
               ∣ r ∣ < ∣ d ∣
euc-rank'' n d n0 = let r = mod' n d n0 in let q = div' n d n0 in
             begin-strict
               ∣ r ∣ ≤⟨ euc-rank' n d n0 ⟩
               ∣ d ∣ / 2 <⟨ aux ∣ d ∣ ∣d∣≠0 ⟩
               ∣ d ∣ ∎
                 where
                   open NatP.≤-Reasoning
                   aux : ∀ n -> ¬ n ≡ 0 -> n / 2 < n
                   aux zero n0 with n0 refl
                   ... | ()
                   aux (suc n) n0 = NDM.m/n<m (suc n) 2 (s≤s (s≤s z≤n))
                   ∣d∣≠0 : ¬ ∣ d ∣ ≡ 0
                   ∣d∣≠0 x = n0 (IntP.∣i∣≡0⇒i≡0 x)

-- ----------------------------------------------------------------------
-- Alternative Euclidean Structure

-- The newly defined div' and mod' together with euc-eq' and
-- euc-rank'' make ℤ an Euclidean Domain with more precise estimate on
-- the rank of the reminder.

open import Integer.EucDomain
  using (+-*-isEuclideanDomain ; +-*-euclideanDomain)
import EuclideanDomain
open   EuclideanDomain.Bundles

-- We update the old Euclidean structure in EucDomain.
+-*-isEuclideanDomain' = record +-*-isEuclideanDomain
                         { div = div'
                         ; mod = mod'
                         ; euc-eq = euc-eq'
                         ; euc-rank = euc-rank''
                         }

-- Bundle.
+-*-euclideanDomain' : EuclideanDomainBundle _ _
+-*-euclideanDomain' = record
  { isEuclideanDomain = +-*-isEuclideanDomain'
  }

-- ----------------------------------------------------------------------
-- Make a new instance for DivMod ℤ

-- Translation between two nonzeros.
nz : ∀ (x : ℤ) -> .{{NonZero x}} -> ¬ x ≡ 0#
nz +[1+ n ] ()

-- We use the newly defined div and mod function.
instance
  new-DMℤ : DivMod ℤ
  new-DMℤ .NZT = NZTℤ
  new-DMℤ ._/_ n d = div' n d (nz d)
  new-DMℤ ._%_ n d = mod' n d (nz d)

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
module _ where

data Nat : Set where

postulate
  C Q : Set → Set
  unQ : ∀ {A} → Q A → A
  instance
    CQ : C (Q Nat)

  theC : {A : Set} {{_ : C A}} → A

-- We shouldn't solve this based on CQ being the only instance available for Q _.
dont-solve : _
dont-solve = unQ theC

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-

Holey congruence where congruence is limited to specific functions.

To use, open the module `AutoCong` with a database that maps function names to
congruences for those functions.

-}

module Holes.Cong.Limited where

open import Holes.Prelude
open import Holes.Term

open Holes.Prelude public using (quote-term)

private
  find : ∀ {a} {A : Set a} → (A → Bool) → List A → Maybe A
  find p [] = nothing
  find p (x ∷ xs) = if p x then just x else find p xs

  last2 : ∀ {ℓ} {A : Set ℓ} → List A → Maybe (A × A)
  last2 (x ∷ y ∷ []) = just (x , y)
  last2 (x ∷ xs) = last2 xs
  last2 _ = nothing

  getArgs : Term → Maybe (List (Arg Term))
  getArgs (con _ args) = just args
  getArgs (def _ args) = just args
  getArgs (var _ args) = just args
  getArgs _ = nothing

  decomposeEquiv : Term → Maybe (Term × Term)
  decomposeEquiv tm =
    getArgs tm >>= λ args →
    last2 args >>=² λ x y →
    return (getArg x , getArg y)

Congruence = Name
ArgPlace = ℕ

private
  data CongErr : Set where
    termsDontMatch : ℕ → Term → HoleyTerm → CongErr
    typeNotEquivalence noHole : CongErr
    appliedVar : (varIdx : ℕ) (goalLhs : Term) → CongErr
    metaOnPath piOnPath lamOnPath sortOnPath : CongErr
    noCongAvailable : Name → ArgPlace → CongErr
    holeyErr : (goalLhs : Term) (holeyErr : HoleyErr) → CongErr

  fillErrLhs : Term → CongErr → CongErr
  fillErrLhs lhs (appliedVar v _) = appliedVar v lhs
  fillErrLhs lhs e = e

  natToTerm : ℕ → Term
  natToTerm zero = con (quote zero) []
  natToTerm (suc n) = con (quote suc) (basicArg (natToTerm n) ∷ [])

  fillHoleyHole : HoleyTerm → Term
  fillHoleyHole = fillHoley′ (λ _ → quote-term ⌞_⌟)

  printCongErr : CongErr → List ErrorPart
  printCongErr (termsDontMatch depth original holey)
    = strErr "There was an attempt to create a path based on non-matching terms"
    ∷ termErr original
    ∷ strErr "and"
    ∷ termErr (fillHoleyHole holey)
    ∷ strErr "at depth"
    ∷ termErr (natToTerm depth)
    ∷ strErr "This is a bug in the holes library!"
    ∷ []
  printCongErr typeNotEquivalence = strErr "The goal type does not appear to be a binary relation." ∷ []
  printCongErr noHole = strErr "There is no hole the goal LHS." ∷ []
  printCongErr (appliedVar v goalLhs)
    = strErr "Variable applications on the path to the hole are not supported. The applied variable was"
    ∷ termErr (var v [])
    ∷ strErr "and the goal LHS was:"
    ∷ termErr goalLhs
    ∷ []
  printCongErr metaOnPath = strErr "Metavariables in the goal LHS are not supported." ∷ []
  printCongErr piOnPath = strErr "Pi types in the goal LHS are not supported." ∷ []
  printCongErr lamOnPath = strErr "Lambdas in the goal LHS are not supported." ∷ []
  printCongErr sortOnPath = strErr "Sorts in the goal LHS are not supported." ∷ []
  printCongErr (noCongAvailable nm argPlace)
    = strErr "No congruence available for function"
    ∷ nameErr nm
    ∷ strErr "at required argument place, index"
    ∷ termErr (natToTerm argPlace)
    ∷ []
  printCongErr (holeyErr goalLhs h) = printHoleyErr goalLhs h

  printCongErrs : List CongErr → List ErrorPart
  printCongErrs (e ∷ []) = printCongErr e
  printCongErrs es = strErr "One of these errors happened:\n" ∷ (intercalate (strErr ";\n" ∷ []) ∘ map printCongErr) es

  data HolePath : Set where
    hole : HolePath
    app : (nm : Name) (index : ℕ) (allArgs : List (Arg Term)) → HolePath → HolePath

module AutoCong (database : List (Name × ArgPlace × Congruence)) where

  private
    findCong : Name → ArgPlace → Maybe Congruence
    findCong nm argPlace =
      proj₂ ∘ proj₂ <$>
      find ((λ { (nm′ , argPlace′ , _) →
                      (nm =Name? nm′) ∧
                      (argPlace =ℕ? argPlace′) }))
        database

    -- Tries to apply the given function to each element of the list, and
    -- returns the first successful result. If none of the results are
    -- successful, accumulates the errors using the error monoid.

    findOk : ∀ {a e r} {A : Set a} {E : Set e} {{errMonoid : RawMonoid E}} {R : Set r} → (ℕ → A → Result E R) → List A → Result E R
    findOk {A = A}{E}{R} = go 0
      where
        go : ℕ → (ℕ → A → Result E R) → List A → Result E R
        go i f [] = err mempty
        go i f (x ∷ xs) with f i x
        ... | ok y = ok y
        ... | err e₁ with go (1 + i) f xs
        ... | ok y = ok y
        ... | err e₂ = err (e₁ <> e₂)

    zipArglists : ∀ {A B : Set} → List (Arg A) → List (Arg B) → List (Arg (A × B))
    zipArglists xs ys = map (λ { (arg i x , arg _ y) → arg i (x , y)}) (zip xs ys)

    mutual
      findHole : ℕ → List (Arg (Term × HoleyTerm)) → Result (List CongErr) (ℕ × HolePath)
      findHole depth = findOk (λ { n (arg i (t , h)) → (n ,_) <$> buildPath depth t h })

      {-# TERMINATING #-}
      buildPath : ℕ → Term → HoleyTerm → Result (List CongErr) HolePath
      buildPath depth original (hole _) = return hole
      buildPath depth (lit _) (lit l) = err (noHole ∷ [])
      buildPath depth unknown unknown = err (noHole ∷ [])
      buildPath depth (var _ _) (var x _) = err (appliedVar x unknown ∷ [])
      buildPath depth (con _ originalArgs) (con nm args) =
        findHole (suc depth) (zipArglists originalArgs args) >>=² λ argPlace nextPath →
        return (app nm argPlace originalArgs nextPath)
      buildPath depth (def _ originalArgs) (def nm args) =
        findHole (suc depth) (zipArglists originalArgs args) >>=² λ argPlace nextPath →
        return (app nm argPlace originalArgs nextPath)
      buildPath depth (lam _ _) (lam _ _) = err (lamOnPath ∷ [])
      buildPath depth (lam _ _) (pi _ _) = err (piOnPath ∷ [])
      buildPath depth (lam _ _) (meta _ _) = err (metaOnPath ∷ [])
      buildPath depth (agda-sort _) (agda-sort _) = err (sortOnPath ∷ [])
      buildPath depth original holey = err (termsDontMatch depth original holey ∷ [])

    pathToCong : HolePath → Term → Result (List CongErr) Term
    pathToCong hole eq = return eq
    pathToCong (app nm argPlace allArgs hp) eq =
      liftMaybe (noCongAvailable nm argPlace ∷ []) (findCong nm argPlace) >>= λ cong →
      pathToCong hp eq >>= λ rec →
      return (def cong (allArgs ++ (basicArg rec ∷ [])))

    fillErrHoley : HoleyTerm → CongErr → CongErr
    fillErrHoley = fillErrLhs ∘ fillHoleyHole

    autoCong : Term → Term → RTC (List CongErr) ⊤
    autoCong equiv goal =
      -- Infer the type of the goal
      liftTC (inferType goal) >>= λ goalType →
      -- Try to decompose the goal type into a left and right hand side.
      liftMaybe (typeNotEquivalence ∷ []) (decomposeEquiv goalType) >>=² λ goalLhs goalRhs →
      -- Try to convert the goal LHS to a holey term.
      liftResult′ (singleton ∘ holeyErr goalLhs) (termToHoley goalLhs) >>= λ holeyLhs →
      -- Try to build a path to a hole in the LHS.
      liftResult′ (map (fillErrHoley holeyLhs)) (buildPath 0 goalLhs holeyLhs) >>= λ lhsPath →
      -- Try to convert the path to a chain of congruence applications.
      liftResult (pathToCong lhsPath equiv) >>= λ congTerm →
      -- Try to unify the result with the goal to complete the proof.
      liftTC (unify congTerm goal)

    autoCongDebug : Term → Term → RTC (List CongErr) ⊤
    autoCongDebug equiv goal =
      liftTC (inferType goal) >>= λ goalType →
      liftMaybe (singleton typeNotEquivalence) (decomposeEquiv goalType) >>=² λ goalLhs goalRhs →
      liftResult′ (singleton ∘ holeyErr goalLhs) (termToHoley goalLhs) >>= λ holeyLhs →
      let showArgs = map (termErr ∘ getArg) ∘ getArglist
      in typeError′ (showArgs goalLhs ++ (strErr "and" ∷ showArgs (fillHoleyHole holeyLhs))) >>= λ (_ : ⊤) →
      liftResult′ (map (fillErrHoley holeyLhs)) (buildPath 0 goalLhs holeyLhs) >>= λ lhsPath →
      liftResult (pathToCong lhsPath equiv) >>= λ congTerm →
      liftTC (unify congTerm goal)

  macro
    cong! : Term → Term → TC ⊤
    cong! equiv = runRtcOrTypeError printCongErrs ∘ autoCong equiv

    -- debug version

    cong!Debug : Term → Term → TC ⊤
    cong!Debug equiv = runRtcOrTypeError printCongErrs ∘ autoCongDebug equiv


text:
open import Prelude
open import Nat
open import dynamics-core
open import contexts
open import contraction
open import weakening
open import exchange
open import lemmas-disjointness
open import binders-disjoint-checks

module lemmas-subst-ta where
  -- this is what makes the binders-unique assumption below good enough: it
  -- tells us that we can pick fresh variables
  mutual
    binders-envfresh : ∀{Δ Γ Γ' y σ} →
                       Δ , Γ ⊢ σ :s: Γ' →
                       y # Γ →
                       unbound-in-σ y σ →
                       binders-unique-σ σ →
                       envfresh y σ
    binders-envfresh {Γ' = Γ'} {y = y} (STAId x) apt unbound unique with ctxindirect Γ' y
    binders-envfresh {Γ' = Γ'} {y = y} (STAId x₁) apt unbound unique | Inl x = abort (somenotnone (! (x₁ y (π1 x) (π2 x)) · apt))
    binders-envfresh (STAId x₁) apt unbound unique | Inr x = EFId x
    binders-envfresh {Γ = Γ} {y = y} (STASubst  {y = z} subst x₁) apt (UBσSubst x₂ unbound neq) (BUσSubst zz x₃ x₄) =
                                                                                EFSubst (binders-fresh {y = y} x₁ zz x₂ apt)
                                                                                (binders-envfresh subst (apart-extend1 Γ neq apt) unbound x₃)
                                                                                neq

    binders-fresh : ∀{Δ Γ d2 τ y} →
                    Δ , Γ ⊢ d2 :: τ →
                    binders-unique d2 →
                    unbound-in y d2 →
                    Γ y == None →
                    fresh y d2
    binders-fresh TANum BUHole UBNum apt = FNum
    binders-fresh {y = y} (TAVar {x = x} x₁)  BUVar UBVar apt with natEQ y x
    binders-fresh (TAVar x₂) BUVar UBVar apt | Inl refl = abort (somenotnone (! x₂ · apt))
    binders-fresh (TAVar x₂) BUVar UBVar apt | Inr x₁ = FVar x₁
    binders-fresh {y = y} (TALam {x = x} x₁ wt) bu2 ub apt  with natEQ y x
    binders-fresh (TALam x₂ wt) bu2 (UBLam2 x₁ ub) apt | Inl refl = abort (x₁ refl)
    binders-fresh {Γ = Γ} (TALam {x = x} x₂ wt) (BULam bu2 x₃) (UBLam2 x₄ ub) apt | Inr x₁ =  FLam x₁ (binders-fresh wt bu2 ub (apart-extend1 Γ x₄ apt))
    binders-fresh (TAAp wt wt₁)  (BUAp bu2 bu3 x) (UBAp ub ub₁) apt = FAp (binders-fresh wt bu2 ub apt) (binders-fresh wt₁ bu3 ub₁ apt)
    binders-fresh (TAEHole x₁ x₂) (BUEHole x) (UBHole x₃) apt = FHole (binders-envfresh x₂ apt x₃ x )
    binders-fresh (TANEHole x₁ wt x₂) (BUNEHole bu2 x) (UBNEHole x₃ ub) apt = FNEHole (binders-envfresh x₂ apt x₃ x) (binders-fresh wt bu2  ub apt)
    binders-fresh (TACast wt x₁) (BUCast bu2) (UBCast ub) apt = FCast (binders-fresh wt  bu2  ub apt)
    binders-fresh (TAFailedCast wt x x₁ x₂) (BUFailedCast bu2) (UBFailedCast ub) apt = FFailedCast (binders-fresh wt  bu2  ub apt)
    binders-fresh (TAInl wt) (BUInl bu) (UBInl ub) apt = FInl (binders-fresh wt bu ub apt)
    binders-fresh (TAInr wt) (BUInr bu) (UBInr ub) apt = FInr (binders-fresh wt bu ub apt)
    binders-fresh {Γ = Γ} (TACase wt x wt₁ x₁ wt₂) (BUCase bu bu₁ bu₂ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) (UBCase ub x₁₁ ub₁ x₁₂ ub₂) apt = FCase (binders-fresh wt bu ub apt) x₁₁ (binders-fresh wt₁ bu₁ ub₁ (apart-extend1 Γ x₁₁ apt)) x₁₂ (binders-fresh wt₂ bu₂ ub₂ (apart-extend1 Γ x₁₂ apt))
    binders-fresh (TAPlus wt wt₁) (BUPlus bu bu₁ x) (UBPlus ub ub₁) apt = FPlus (binders-fresh wt bu ub apt) (binders-fresh wt₁ bu₁ ub₁ apt)
    binders-fresh (TAPair wt wt₁) (BUPair bu bu₁ x) (UBPair ub ub₁) apt = FPair (binders-fresh wt bu ub apt) (binders-fresh wt₁ bu₁ ub₁ apt)
    binders-fresh (TAFst wt) (BUFst bu) (UBFst ub) apt = FFst (binders-fresh wt bu ub apt)
    binders-fresh (TASnd wt) (BUSnd bu) (UBSnd ub) apt = FSnd (binders-fresh wt bu ub apt)

  -- the substition lemma for preservation
  lem-subst : ∀{Δ Γ x τ1 d1 τ d2} →
              x # Γ →
              binders-disjoint d1 d2 →
              binders-unique d2 →
              Δ , Γ ,, (x , τ1) ⊢ d1 :: τ →
              Δ , Γ ⊢ d2 :: τ1 →
              Δ , Γ ⊢ [ d2 / x ] d1 :: τ
  lem-subst apt bd bu2 (TANum) wt = TANum
  lem-subst apt (BDPlus bd bd₁) bu2 (TAPlus wt1 wt2) wt3 = TAPlus (lem-subst apt bd bu2 wt1 wt3) (lem-subst apt bd₁ bu2 wt2 wt3)
  lem-subst {x = x} apt bd bu2 (TAVar {x = x'} x₂) wt2 with natEQ x' x
  ... | Inl refl with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl with someinj x₂
  ... | refl = wt2
  lem-subst {x = x} apt bd bu2 (TAVar {x = x'} x₂) wt2 | Inr x'≠x with natEQ x x'
  ... | Inl refl = abort (x'≠x refl)
  ... | Inr x'≠x = TAVar x₂
  lem-subst {Δ = Δ} {Γ = Γ} {x = x} {d2 = d2} x#Γ (BDLam bd bd') bu2 (TALam {x = y} {τ1 = τ1} {d = d} {τ2 = τ2} x₂ wt1) wt2 with natEQ y x
  ... | Inl refl with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl = abort (somenotnone x₂)
  lem-subst {Δ = Δ} {Γ = Γ} {x = x} {d2 = d2} x#Γ (BDLam bd bd') bu2 (TALam {x = y} {τ1 = τ1} {d = d} {τ2 = τ2} x₂ wt1) wt2 | Inr y≠x with natEQ x y
  ... | Inl refl = abort (y≠x refl)
  ... | Inr x≠y = TALam x₂ (lem-subst (apart-extend1 Γ x≠y x#Γ) bd bu2 (exchange-ta-Γ x≠y wt1) (weaken-ta (binders-fresh wt2 bu2 bd' x₂) wt2))
  lem-subst apt (BDAp bd bd₁) bu3 (TAAp wt1 wt2) wt3 = TAAp (lem-subst apt bd bu3 wt1 wt3) (lem-subst apt bd₁ bu3 wt2 wt3)
  lem-subst apt bd bu2 (TAEHole inΔ sub) wt2 = TAEHole inΔ (STASubst sub wt2)
  lem-subst apt (BDNEHole x₁ bd) bu2 (TANEHole x₃ wt1 x₄) wt2 = TANEHole x₃ (lem-subst apt bd bu2 wt1 wt2) (STASubst x₄ wt2)
  lem-subst apt (BDCast bd) bu2 (TACast wt1 x₁) wt2 = TACast (lem-subst apt bd bu2 wt1 wt2) x₁
  lem-subst apt (BDFailedCast bd) bu2 (TAFailedCast wt1 x₁ x₂ x₃) wt2 = TAFailedCast (lem-subst apt bd bu2 wt1 wt2) x₁ x₂ x₃
  lem-subst apt (BDInl bd) bu (TAInl wt1) wt2 = TAInl (lem-subst apt bd bu wt1 wt2)
  lem-subst apt (BDInr bd) bu (TAInr wt1) wt2 = TAInr (lem-subst apt bd bu wt1 wt2)
  lem-subst {Δ = Δ} {Γ = Γ} {x = x} {d1 = .(case _ _ _ _ _)} {d2 = d2} apt (BDCase bd x₁ bd₁ x₂ bd₂) bu (TACase {d = d} {τ1 = τ1} {τ2 = τ2} {x = y} {y = z} wt1 x₃ wt3 x₄ wt4) wt2
    with natEQ y x | natEQ z x
  ... | Inl refl | Inl refl with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl = abort (somenotnone x₄)
  lem-subst {Δ = Δ} {Γ = Γ} {x = x} {d1 = .(case _ _ _ _ _)} {d2 = d2} apt (BDCase bd x₁ bd₁ x₂ bd₂) bu (TACase {d = d} {τ1 = τ1} {τ2 = τ2} {x = y} {y = z} wt1 x₃ wt3 x₄ wt4) wt2 | Inl refl | Inr z≠x with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl = abort (somenotnone x₃)
  lem-subst {Δ = Δ} {Γ = Γ} {x = x} {d1 = .(case _ _ _ _ _)} {d2 = d2} apt (BDCase bd x₁ bd₁ x₂ bd₂) bu (TACase {d = d} {τ1 = τ1} {τ2 = τ2} {x = y} {y = z} wt1 x₃ wt3 x₄ wt4) wt2 | Inr y≠x  | Inl refl with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl = abort (somenotnone x₄)
  lem-subst {Δ = Δ} {Γ = Γ} {x = x} {d1 = .(case _ _ _ _ _)} {d2 = d2} apt (BDCase bd x₁ bd₁ x₂ bd₂) bu (TACase {d = d} {τ1 = τ1} {τ2 = τ2} {x = y} {y = z} wt1 x₃ wt3 x₄ wt4) wt2 | Inr y≠x  | Inr z≠x with natEQ x z
  ... | Inl refl = abort (z≠x refl)
  ... | Inr x≠z with natEQ x y
  ... | Inl refl = abort (y≠x refl)
  ... | Inr x≠y = TACase (lem-subst apt bd bu wt1 wt2) x₃ (lem-subst (apart-extend1 Γ x≠y apt) bd₁ bu (exchange-ta-Γ x≠y wt3) (weaken-ta (binders-fresh wt2 bu x₁ x₃) wt2)) x₄ (lem-subst (apart-extend1 Γ x≠z apt) bd₂ bu (exchange-ta-Γ x≠z wt4) (weaken-ta (binders-fresh wt2 bu x₂ x₄) wt2))
  lem-subst apt (BDPair bd bd₁) bu (TAPair wt1 wt3) wt2 = TAPair (lem-subst apt bd bu wt1 wt2) (lem-subst apt bd₁ bu wt3 wt2)
  lem-subst apt (BDFst bd) bu (TAFst wt1) wt2 = TAFst (lem-subst apt bd bu wt1 wt2)
  lem-subst apt (BDSnd bd) bu (TASnd wt1) wt2 = TASnd (lem-subst apt bd bu wt1 wt2)

  lem-subst-cast-sta : ∀{Δ Γ x τ1 τ2 σ Γ'} →
                       x # Γ →
                       τ1 ~ τ2 →
                       Δ , Γ ,, (x , τ2) ⊢ σ :s: Γ' →
                       Δ , Γ ,, (x , τ1) ⊢ Subst (X x ⟨ τ1 ⇒ τ2 ⟩) x σ :s: Γ'
  lem-subst-cast-sta {Γ = Γ} {x = x} {τ1 = τ1} {τ2 = τ2} {Γ' = Γ'} x#Γ con (STAId sub) = STASubst (STAId Γ'⊆) (TACast (TAVar (ctx-top Γ x τ1 x#Γ)) con)
      where
        Γ'⊆ : (y : Nat) (τ : htyp) → (y , τ) ∈ Γ' → (y , τ) ∈ (Γ ,, (x , τ1) ,, (x , τ2))
        Γ'⊆ y τ y∈Γ' with lem-dom-union {Δ1 = ■(x , τ2)} {Δ2 = Γ} (sub y τ y∈Γ')
        ... | Inl y∈x with natEQ x y
        ... | Inr x≠y = abort (somenotnone (! y∈x))
        ... | Inl refl = y∈x
        Γ'⊆ y τ y∈Γ' | Inr y∈Γ with natEQ x y
        ... | Inl refl = abort (somenotnone ((! y∈Γ) · x#Γ))
        ... | Inr x≠y with natEQ x y
        ... | Inl refl = abort (x≠y refl)
        ... | Inr x≠y' = y∈Γ
  lem-subst-cast-sta {Δ = Δ} {Γ = Γ} {x = x} {τ1 = τ1} {τ2 = τ2} {Γ' = Γ'} x#Γ con (STASubst {σ = σ} {y = y} {d = d} {τ = τ} wsta wt) = STASubst (STASubst (tr (λ c → Δ , c ,, (y , τ) ⊢ σ :s: Γ') (! (update Γ x τ1 τ2)) wsta) (tr (λ c → Δ , c ⊢ d :: τ) (! (update Γ x τ1 τ2)) wt)) (TACast (TAVar (ctx-top Γ x τ1 x#Γ)) con)

  lem-subst-cast-ta : ∀{Δ Γ d x τ1 τ2 τ} →
                      x # Γ →
                      binders-unique d →
                      τ1 ~ τ2 →
                      Δ , Γ ,, (x , τ2) ⊢ d :: τ →
                      Δ , Γ ,, (x , τ1) ⊢ [ (X x ⟨ τ1 ⇒ τ2 ⟩) / x ] d :: τ
  lem-subst-cast-ta apt bu con TANum = TANum
  lem-subst-cast-ta apt (BUPlus bu bu₁ x) con (TAPlus wt wt₁) = TAPlus (lem-subst-cast-ta apt bu con wt) (lem-subst-cast-ta apt bu₁ con wt₁)
  lem-subst-cast-ta {Γ = Γ} {x = x} {τ1 = τ1} {τ2 = τ2} apt bu con (TAVar {x = x'} x₁)
      with natEQ x x'
  ... | Inl refl with natEQ x' x
  ... | Inr x'≠x = abort (x'≠x refl)
  ... | Inl refl with Γ x
  ... | None with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl with someinj x₁
  ... | refl = TACast (TAVar (x∈∪l (■ (x , τ1)) Γ x τ1 (x∈■ x τ1))) con
  lem-subst-cast-ta {Γ = Γ} {x = x} {τ1 = τ1} {τ2 = τ2} apt bu con (TAVar {x = x} x₁) | Inl refl | Inl refl | Some t with someinj x₁
  ... | refl = abort (somenotnone apt)
  lem-subst-cast-ta {Γ = Γ} {x = x} {τ1 = τ1} {τ2 = τ2} {τ = τ} apt bu con (TAVar {x = x'} x₁) | Inr x≠x' with natEQ x' x
  ... | Inl refl = abort (x≠x' refl)
  ... | Inr x'≠x = TAVar (x∈∪r (■(x , τ1)) Γ x' τ x₁ (apart-singleton (λ refl → abort (x'≠x refl))))
  lem-subst-cast-ta {Δ = Δ} {Γ = Γ} {x = x} {τ = τ1 ==> τ3} apt (BULam bu x₁) con (TALam {x = y} x₂ wt)
    with natEQ x y
  ... | Inl refl = abort (somenotnone x₂)
  ... | Inr x≠y with natEQ y x
  ... | Inl refl = abort (x≠y refl)
  ... | Inr y≠x = TALam (apart-extend1 Γ y≠x x₂) (exchange-ta-Γ y≠x (lem-subst-cast-ta (apart-extend1 Γ x≠y apt) bu con (exchange-ta-Γ x≠y wt)))
  lem-subst-cast-ta {Γ = Γ} apt (BUAp bu bu₁ x) con (TAAp wt wt₁) = TAAp (lem-subst-cast-ta {Γ = Γ} apt bu con wt) (lem-subst-cast-ta {Γ = Γ} apt bu₁ con wt₁)
  lem-subst-cast-ta {Γ = Γ} apt (BUInl bu) con (TAInl wt) = TAInl (lem-subst-cast-ta {Γ = Γ} apt bu con wt)
  lem-subst-cast-ta {Γ = Γ} apt (BUInr bu) con (TAInr wt) = TAInr (lem-subst-cast-ta {Γ = Γ} apt bu con wt)
  lem-subst-cast-ta {x = x} apt (BUCase bu bu₁ bu₂ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) con (TACase {x = y} {y = z} wt apty wt₁ aptz wt₂) with natEQ y x | natEQ z x
  ... | Inl refl | Inl refl with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl = abort (somenotnone aptz)
  lem-subst-cast-ta {x = x} apt (BUCase bu bu₁ bu₂ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) con (TACase {x = y} {y = z} wt apty wt₁ aptz wt₂) | Inl refl | Inr z≠x with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl = abort (somenotnone apty)
  lem-subst-cast-ta {x = x} apt (BUCase bu bu₁ bu₂ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) con (TACase {x = y} {y = z} wt apty wt₁ aptz wt₂) | Inr y≠x  | Inl refl with natEQ x x
  ... | Inr x≠x = abort (x≠x refl)
  ... | Inl refl = abort (somenotnone aptz)
  lem-subst-cast-ta {Γ = Γ} {x = x} apt (BUCase bu bu₁ bu₂ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) con (TACase {x = y} {y = z} wt apty wt₁ aptz wt₂) | Inr y≠x  | Inr z≠x with natEQ x z
  ... | Inl refl = abort (z≠x refl)
  ... | Inr x≠z with natEQ x y
  ... | Inl refl = abort (y≠x refl)
  ... | Inr x≠y = TACase (lem-subst-cast-ta apt bu con wt) (apart-extend1 Γ y≠x apty) (exchange-ta-Γ y≠x (lem-subst-cast-ta (apart-extend1 Γ x≠y apt) bu₁ con (exchange-ta-Γ x≠y wt₁))) (apart-extend1 Γ z≠x aptz) (exchange-ta-Γ z≠x (lem-subst-cast-ta (apart-extend1 Γ x≠z apt) bu₂ con (exchange-ta-Γ x≠z wt₂)))
  lem-subst-cast-ta apt (BUEHole x₂) con (TAEHole x x₁) = TAEHole x (lem-subst-cast-sta apt con x₁)
  lem-subst-cast-ta apt (BUNEHole bu x₂) con (TANEHole x wt x₁) = TANEHole x (lem-subst-cast-ta apt bu con wt) (lem-subst-cast-sta apt con x₁)
  lem-subst-cast-ta apt (BUCast bu) con (TACast wt x) = TACast (lem-subst-cast-ta apt bu con wt) x
  lem-subst-cast-ta apt (BUFailedCast bu) con (TAFailedCast wt x x₁ x₂) = TAFailedCast (lem-subst-cast-ta apt bu con wt) x x₁ x₂
  lem-subst-cast-ta apt (BUPair bu bu₁ x) con (TAPair wt wt₁) = TAPair (lem-subst-cast-ta apt bu con wt) (lem-subst-cast-ta apt bu₁ con wt₁)
  lem-subst-cast-ta apt (BUFst bu) con (TAFst wt) = TAFst (lem-subst-cast-ta apt bu con wt)
  lem-subst-cast-ta apt (BUSnd bu) con (TASnd wt) = TASnd (lem-subst-cast-ta apt bu con wt)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda