-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
3fdce1c
commit 99196fb
Showing
14 changed files
with
1,699 additions
and
52 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,10 +1,10 @@ | ||
| Goal: A | ||
| Elaborates to: hcomp {ℓ} {A} {(~ i ∨ i) ∨ ~ j ∨ j ∨ ~ k ∨ k} (λ l → primPOr {ℓ} (~ i ∨ i) (~ j ∨ j ∨ ~ k ∨ k) {λ _ → A} (primPOr {ℓ} (~ i) i {λ _ → A} (λ _ → hcomp {ℓ} {A} {(~ l ∨ l) ∨ ~ k ∨ k ∨ ~ j ∨ j} (λ l₁ → primPOr {ℓ} (~ l ∨ l) (~ k ∨ k ∨ ~ j ∨ j) {λ _ → A} (primPOr {ℓ} (~ l) l {λ _ → A} (λ _ → s (~ l₁) (k ∨ j)) (λ _ → a)) (primPOr {ℓ} (~ k ∨ k) (~ j ∨ j) {λ _ → A} (primPOr {ℓ} (~ k) k {λ _ → A} (λ _ → s (~ l₁) (~ l ∧ j)) (λ _ → a)) (primPOr {ℓ} (~ j) j {λ _ → A} (λ _ → s (l ∨ ~ l₁) k) (λ _ → s (k ∨ ~ l₁) (~ l))))) a) (λ _ → hcomp {ℓ} {A} {(l ∨ ~ l) ∨ k ∨ ~ k ∨ j ∨ ~ j} (λ l₁ → primPOr {ℓ} (l ∨ ~ l) (k ∨ ~ k ∨ j ∨ ~ j) {λ _ → A} (primPOr {ℓ} l (~ l) {λ _ → A} (λ _ → s (~ l₁) (~ k ∨ ~ j)) (λ _ → a)) (primPOr {ℓ} (k ∨ ~ k) (j ∨ ~ j) {λ _ → A} (primPOr {ℓ} k (~ k) {λ _ → A} (λ _ → s (~ l₁) (l ∧ ~ j)) (λ _ → a)) (primPOr {ℓ} j (~ j) {λ _ → A} (λ _ → s (~ l ∨ ~ l₁) (~ k)) (λ _ → s (~ k ∨ ~ l₁) l)))) a)) (primPOr {ℓ} (~ j ∨ j) (~ k ∨ k) {λ _ → A} (primPOr {ℓ} (~ j) j {λ _ → A} (λ _ → hcomp {ℓ} {A} {(k ∨ ~ k) ∨ ~ l ∨ l ∨ i ∨ ~ i} (λ l₁ → primPOr {ℓ} (k ∨ ~ k) (~ l ∨ l ∨ i ∨ ~ i) {λ _ → A} (primPOr {ℓ} k (~ k) {λ _ → A} (λ _ → s (~ l₁) (l ∨ ~ i)) (λ _ → a)) (primPOr {ℓ} (~ l ∨ l) (i ∨ ~ i) {λ _ → A} (primPOr {ℓ} (~ l) l {λ _ → A} (λ _ → s (~ l₁) (k ∧ ~ i)) (λ _ → a)) (primPOr {ℓ} i (~ i) {λ _ → A} (λ _ → s (~ k ∨ ~ l₁) l) (λ _ → s (l ∨ ~ l₁) k)))) a) (λ _ → hcomp {ℓ} {A} {(~ k ∨ k) ∨ l ∨ ~ l ∨ ~ i ∨ i} (λ l₁ → primPOr {ℓ} (~ k ∨ k) (l ∨ ~ l ∨ ~ i ∨ i) {λ _ → A} (primPOr {ℓ} (~ k) k {λ _ → A} (λ _ → s (~ l₁) (~ l ∨ i)) (λ _ → a)) (primPOr {ℓ} (l ∨ ~ l) (~ i ∨ i) {λ _ → A} (primPOr {ℓ} l (~ l) {λ _ → A} (λ _ → s (~ l₁) (~ k ∧ i)) (λ _ → a)) (primPOr {ℓ} (~ i) i {λ _ → A} (λ _ → s (k ∨ ~ l₁) (~ l)) (λ _ → s (~ l ∨ ~ l₁) (~ k))))) a)) (λ _ → a))) a | ||
| Goal: S² | ||
| Elaborates to: hcomp {ℓ} {S²} {(~ i ∨ i) ∨ ~ j ∨ j ∨ ~ k ∨ k} (λ l → primPOr {ℓ} (~ i ∨ i) (~ j ∨ j ∨ ~ k ∨ k) {λ _ → S²} (primPOr {ℓ} (~ i) i {λ _ → S²} (λ _ → hcomp {ℓ} {S²} {(~ l ∨ l) ∨ ~ k ∨ k ∨ ~ j ∨ j} (λ l₁ → primPOr {ℓ} (~ l ∨ l) (~ k ∨ k ∨ ~ j ∨ j) {λ _ → S²} (primPOr {ℓ} (~ l) l {λ _ → S²} (λ _ → surf (~ l₁) (k ∨ j)) (λ _ → base)) (primPOr {ℓ} (~ k ∨ k) (~ j ∨ j) {λ _ → S²} (primPOr {ℓ} (~ k) k {λ _ → S²} (λ _ → surf (~ l₁) (~ l ∧ j)) (λ _ → base)) (primPOr {ℓ} (~ j) j {λ _ → S²} (λ _ → surf (l ∨ ~ l₁) k) (λ _ → surf (k ∨ ~ l₁) (~ l))))) base) (λ _ → hcomp {ℓ} {S²} {(l ∨ ~ l) ∨ k ∨ ~ k ∨ j ∨ ~ j} (λ l₁ → primPOr {ℓ} (l ∨ ~ l) (k ∨ ~ k ∨ j ∨ ~ j) {λ _ → S²} (primPOr {ℓ} l (~ l) {λ _ → S²} (λ _ → surf (~ l₁) (~ k ∨ ~ j)) (λ _ → base)) (primPOr {ℓ} (k ∨ ~ k) (j ∨ ~ j) {λ _ → S²} (primPOr {ℓ} k (~ k) {λ _ → S²} (λ _ → surf (~ l₁) (l ∧ ~ j)) (λ _ → base)) (primPOr {ℓ} j (~ j) {λ _ → S²} (λ _ → surf (~ l ∨ ~ l₁) (~ k)) (λ _ → surf (~ k ∨ ~ l₁) l)))) base)) (primPOr {ℓ} (~ j ∨ j) (~ k ∨ k) {λ _ → S²} (primPOr {ℓ} (~ j) j {λ _ → S²} (λ _ → hcomp {ℓ} {S²} {(k ∨ ~ k) ∨ ~ l ∨ l ∨ i ∨ ~ i} (λ l₁ → primPOr {ℓ} (k ∨ ~ k) (~ l ∨ l ∨ i ∨ ~ i) {λ _ → S²} (primPOr {ℓ} k (~ k) {λ _ → S²} (λ _ → surf (~ l₁) (l ∨ ~ i)) (λ _ → base)) (primPOr {ℓ} (~ l ∨ l) (i ∨ ~ i) {λ _ → S²} (primPOr {ℓ} (~ l) l {λ _ → S²} (λ _ → surf (~ l₁) (k ∧ ~ i)) (λ _ → base)) (primPOr {ℓ} i (~ i) {λ _ → S²} (λ _ → surf (~ k ∨ ~ l₁) l) (λ _ → surf (l ∨ ~ l₁) k)))) base) (λ _ → hcomp {ℓ} {S²} {(~ k ∨ k) ∨ l ∨ ~ l ∨ ~ i ∨ i} (λ l₁ → primPOr {ℓ} (~ k ∨ k) (l ∨ ~ l ∨ ~ i ∨ i) {λ _ → S²} (primPOr {ℓ} (~ k) k {λ _ → S²} (λ _ → surf (~ l₁) (~ l ∨ i)) (λ _ → base)) (primPOr {ℓ} (l ∨ ~ l) (~ i ∨ i) {λ _ → S²} (primPOr {ℓ} l (~ l) {λ _ → S²} (λ _ → surf (~ l₁) (~ k ∧ i)) (λ _ → base)) (primPOr {ℓ} (~ i) i {λ _ → S²} (λ _ → surf (k ∨ ~ l₁) (~ l)) (λ _ → surf (~ l ∨ ~ l₁) (~ k))))) base)) (λ _ → base))) base | ||
| ———————————————————————————————————————————————————————————— | ||
| k : I | ||
| j : I | ||
| i : I | ||
| s : _≡_ {ℓ} {_≡_ {ℓ} {A} a a} (λ _ → a) (λ _ → a) | ||
| a : A | ||
| A : Type ℓ | ||
| surf : _≡_ {ℓ} {_≡_ {ℓ} {S²} base base} (λ _ → base) (λ _ → base) | ||
| base : S² | ||
| S² : Type ℓ | ||
| ℓ : Level |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,78 @@ | ||
|
|
||
| var vsCodeView = `#version 300 es | ||
| in vec3 vPosition; | ||
| uniform mat4 poseMat; | ||
| uniform mat4 projMat; | ||
| uniform mat4 modelMat; | ||
| out vec2 vTex; | ||
| void | ||
| main() | ||
| { | ||
| // vCol = vColor;//vec3(1.0,0.0,0.0);// | ||
| vTex = vec2(vPosition.x , vPosition.y); | ||
| gl_Position = | ||
| (projMat)*(poseMat)*modelMat* | ||
| (vec4(vPosition.x , vPosition.y , vPosition.z ,1.0)); | ||
| } | ||
| `; | ||
|
|
||
| var fsCodeView = `#version 300 es | ||
| precision highp float; | ||
| // The texture. | ||
| uniform sampler2D u_texture; | ||
| uniform sampler2D u_textureMap; | ||
| uniform vec2 coCu; | ||
| uniform float uTime; | ||
| out vec4 fColor; | ||
| in vec2 vTex; | ||
| void | ||
| main() | ||
| { | ||
| vec2 vTexCorrectedY = vec2(vTex.x*2.0 , 1.0 - vTex.y); | ||
| vec2 vTexMbInv; | ||
| if(gl_FrontFacing){ | ||
| vTexMbInv = vec2(1.0 - vTexCorrectedY.x , vTexCorrectedY.y); | ||
| }else{ | ||
| vTexMbInv = vTexCorrectedY; | ||
| } | ||
| vec4 co = texture(u_texture, vTexMbInv ); | ||
| vec4 coMap = texture(u_textureMap, vTexMbInv ); | ||
| vec4 coHover = texture(u_textureMap, coCu ); | ||
| float hovered; | ||
| if(coHover.xyz == coMap.xyz && coHover.xyz!=vec3(1.0,1.0,1.0)){ | ||
| hovered = 0.5+0.5*abs(sin(uTime/200.0)); | ||
| }else{ | ||
| hovered = 0.0; | ||
| } | ||
| if(abs(distance(coCu*vec2(1.0,2.0),vTexMbInv*vec2(1.0,2.0)))<0.02){ | ||
| fColor = vec4(0.0,0.0,1.0,1.0); | ||
| }else{ | ||
| fColor = co*vec4(1.0,1.0-hovered*0.5,1.0-hovered*0.5,1.0); | ||
| } | ||
| //vec4(step(0.5,co.x) , step(0.5,co.y) , step(0.5,co.z) , 1.0 ); | ||
| // vec4(1.0,0.0,0.0,1.0); | ||
| // fColor = vec4( | ||
| // //vCol.rgb | ||
| // finalRGB | ||
| // , vCol.a); | ||
| }`; |
Oops, something went wrong.