123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280 |
- {-- test.agda - playing with agda/haskell interop
- -- Copyright (C) 2018-2019 caryoscelus
- --
- -- This program is free software: you can redistribute it and/or modify
- -- it under the terms of the GNU General Public License as published by
- -- the Free Software Foundation, either version 3 of the License, or
- -- (at your option) any later version.
- --
- -- This program is distributed in the hope that it will be useful,
- -- but WITHOUT ANY WARRANTY; without even the implied warranty of
- -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- -- GNU General Public License for more details.
- --
- -- You should have received a copy of the GNU General Public License
- -- along with this program. If not, see <http://www.gnu.org/licenses/>.
- --}
- -- {-# OPTIONS --without-K #-}
- module test where
- open import Data.Empty
- open import Data.Unit hiding (_≟_)
- open import Data.Bool hiding (_≟_)
- open import Data.Nat
- open import Data.Nat.Properties
- open import Data.Nat.DivMod
- import Data.Integer as ℤ
- open import Data.Sum hiding (map)
- open import Data.Product hiding (map ; zip)
- import Data.Product as P
- open import Data.List
- import Data.List as L
- open import Relation.Binary.PropositionalEquality
- open import Relation.Nullary
- open import Relation.Nullary.Decidable hiding (map)
- import IO
- open import Function
- open import Util
- open import Hask
- import GLFW
- open GLFW.Types
- open import NanoLens
- open import GLApp
- record Stroke : Set where
- constructor mkStroke
- field
- sZoom : Int
- sPoints : List Point
- open Stroke
- Picture = List Stroke
- record AllApp : Set where
- field
- frames : List Picture
- zoomLevel : Int
- cursor : V2 Coord
- isDrawing : Bool
-
- nowFrame : ℕ
- frameCount : ℕ
- needToClearTexture : Bool
- open AllApp
- emptyApp : ℕ → AllApp
- emptyApp nFrames = record
- { frameCount = nFrames
- ; nowFrame = 0
- ; frames = replicate nFrames []
- ; cursor = v2 (ℤ.+ 0) (ℤ.+ 0)
- ; isDrawing = false
- ; zoomLevel = I0
- ; needToClearTexture = true
- }
- modifyAt : ∀ {ℓ} {A : Set ℓ} (n : ℕ) (f : A → A) → List A → List A
- modifyAt n f [] = []
- modifyAt zero f (x ∷ l) = f x ∷ l
- modifyAt (suc n) f (x ∷ l) = x ∷ modifyAt n f l
- newShape : AllApp → AllApp
- newShape app =
- let
- zl = zoomLevel app
- fi = nowFrame app
- in
- modify ፦[ frames ] (modifyAt fi (mkStroke zl [] ∷_)) app
- appendShape : AllApp → AllApp
- appendShape app =
- let
- xy = cursor app
- fi = nowFrame app
- in
- modify ፦[ frames ]
- (modifyAt fi (λ
- { (mkStroke z ss ∷ shapes) → mkStroke z (xy ∷ ss) ∷ shapes
- ; [] → [] -- TODO should never happen, eliminate
- }))
- app
- mouseCallback : GLFW.MouseCallback AllApp
- mouseCallback button MouseButtonState'Pressed mods =
- set ፦[ isDrawing ] true ⟫ newShape
- mouseCallback button _ mods = set ፦[ isDrawing ] false
- cursorCallback : GLFW.CursorCallback AllApp
- cursorCallback x y app =
- (set ፦[ cursor ] (screenToGl wh wh x y) ⟫ λ app →
- let
- draw = isDrawing app
- in
- when′ draw appendShape app) app
- loopFrameLeft : ℕ → ℕ → ℕ
- loopFrameLeft m zero = pred m
- loopFrameLeft m (suc n) = n
- loopFrameRight : ℕ → ℕ → ℕ
- loopFrameRight m n
- with suc n <? m
- ... | yes _ = suc n
- ... | no _ = 0
- keyCallback : GLFW.KeyCallback AllApp
- keyCallback _ _ KeyState'Released _ = id
- keyCallback Key'Equal _ _ _ =
- set ፦[ needToClearTexture ] true ⟫
- modify ፦[ zoomLevel ] Isuc
- keyCallback Key'Minus _ _ _ =
- set ፦[ needToClearTexture ] true ⟫
- modify ፦[ zoomLevel ] Ipred
- keyCallback Key'Left _ _ _ app =
- ( set ፦[ needToClearTexture ] true
- ⟫ modify ፦[ nowFrame ] (loopFrameLeft (frameCount app))
- ) app
- keyCallback Key'Right _ _ _ app =
- ( set ፦[ needToClearTexture ] true
- ⟫ modify ፦[ nowFrame ] (loopFrameRight (frameCount app))
- ) app
- keyCallback _ _ _ _ = id
- pic⇒triangles : Int → Picture → List (V2 Float)
- pic⇒triangles zoom = foldr addStroke []
- where
- addStroke :
- (stroke : Stroke) (vertices : List (V2 Float)) → List (V2 Float)
- addStroke stroke =
- let
- sp = sPoints stroke
- q = toZoom zoom (sZoom stroke)
- ss = zip sp (drop 1 sp)
- in
- concat (map (uncurry (drawLine q)) ss) ++_
- getLast : ∀ {ℓ} {A : Set ℓ} (z : A) (xs : List A) → A
- getLast z [] = z
- getLast z (x ∷ xs) = getLast x xs
- index : ∀ {ℓ} {A : Set ℓ} (z : A) (n : ℕ) (xs : List A) → A
- index z _ [] = z
- index z zero (x ∷ xs) = x
- index z (suc n) (x ∷ xs) = index x n xs
- module _ where
- import Data.Vec as V
- import Data.Fin as Fin
- vec-length : ∀ {ℓ n} {A : Set ℓ} → V.Vec A n → ℕ
- vec-length {_} {n} _ = n
- getAround : ∀ {ℓ} {A : Set ℓ} (z : A) (n : ℕ) (xs : List A) → A × A
- getAround z n xs
- with length xs | V.fromList xs
- ... | .zero | V.[] = z , z
- ... | .(suc _) | xs′@(_ V.∷ _) =
- let
- kk x = V.lookup xs′ (x mod (vec-length xs′))
- in
- P.map kk kk (pred n , suc n)
- v2avg : V2 Coord → V2 Coord → V2 Coord
- v2avg a b = v2
- (avgC (V2.x a) (V2.x b))
- (avgC (V2.y a) (V2.y b))
- sample-at :
- ∀ {m} (n : ℕ)
- {m≠0 : m ≡ 0 → ⊥}
- {n≠0 : False (n ≟ 0)}
- (xs : V.Vec (V2 Coord) m)
- (i : ℕ)
- → V2 Coord
- sample-at {m} n {m≠0} {n≠0} xs i =
- let
- p′ = _div_ (i * m) n {n≠0}
- p = p′ ⊓ pred m
- p-ok : p < m
- p-ok = ≤-trans
- (s≤s (m⊓n≤n p′ (pred m)))
- (≤-reflexive (m≢0⇒suc[pred[m]]≡m m≠0))
- in
- V.lookup xs (Fin.fromℕ≤ p-ok)
- doIt : List (V2 Coord) → List (V2 Coord) → List (V2 Coord)
- doIt a b
- with length a | V.fromList a | length b | V.fromList b
- ... | .zero | V.[] | .zero | V.[] = []
- ... | .(suc _) | _ V.∷ _ | .zero | V.[] = []
- ... | .zero | V.[] | .(suc _) | _ V.∷ _ = []
- ... | .(suc _) | xs@(_ V.∷ _) | .(suc _) | ys@(_ V.∷ _) =
- let
- l = vec-length xs ⊔ vec-length ys
- in
- V.toList $
- V.map (λ n →
- v2avg
- (sample-at l {λ ()} xs n)
- (sample-at l {λ ()} ys n))
- (V.fromList $ upTo l)
- -- UGH ; ignoring zoom ; ...
- iStrokes : Stroke → Stroke → Stroke
- iStrokes a b = modify ፦[ sPoints ] (doIt (sPoints b)) a
- interpolate : Int → Picture → Picture → List (V2 Float)
- interpolate zoom before after =
- pic⇒triangles zoom (map (uncurry iStrokes) (zip before after))
- half : Float
- half = ℕratioToFloat 1 2
- penColor : V3 Float
- penColor = v3 half half half
- toTriangles′ : Int → ℕ → List Picture → List (V2 Float)
- toTriangles′ zoom n frames
- with drop n frames
- ... | [] = []
- ... | frame ∷ tail
- with frame
- ... | [] = uncurry (interpolate zoom) (getAround frame n frames)
- ... | _ ∷ _ = pic⇒triangles zoom frame
- toTriangles : AllApp → RenderResult AllApp
- RenderResult.newState (toTriangles x) = x -- TODO: dirty
- RenderResult.result (toTriangles x) = L.map (λ p → rgbPoint p penColor) $ toTriangles′
- (zoomLevel x) -- -256
- (nowFrame x)
- (frames x)
- defaultFrameCount = 24
- drawApp : DrawApp AllApp
- drawApp = record
- { empty = emptyApp defaultFrameCount
- ; render = toTriangles
- ; frameCount = frameCount
- ; nowFrame = nowFrame
- ; dontClearTexture = set ፦[ needToClearTexture ] false
- ; getNeedToClearTexture = needToClearTexture
- ; mouseCallback = GLFW.mouseCallbackWrap mouseCallback
- ; cursorCallback = GLFW.cursorCallbackWrap cursorCallback
- ; keyCallback = GLFW.keyCallbackWrap keyCallback
- ; isDirty = λ _ _ → true
- }
- main = run ∘ lift ∘ everything $ drawApp
- where open IO
|