Iainmon

module Prim


import Data.Vect
import Data.Fin
-- import Data.Nat
-- import Data.List
-- %hide Prelude.cong

Iainmon

Require Import Coq.Init.Nat.


Inductive bit : Set := I | O.

Inductive bits : nat -> Set :=
  | bnil  : bits 0
  | bcons : forall (n : nat), bit -> bits n -> bits (S n).
Arguments bcons [n] _ _.

Iainmon

Require Import Unicode.Utf8.

Require Import Psatz.
Require Import Coq.Arith.Arith.
Require Import Coq.Init.Nat. (* needed? it seems no, with next line. *)
Import Nat.

Open Scope nat_scope.

Iainmon

Ltac save h1 h2 := 
  (*pose proof h1 as h2*)
  let t := type of h1 in 
    assert (h2 : t) by (exact h1).

Tactic Notation "save" constr(h1) "as" ident(h2) := 
  save h1 h2.


(* Ltac replace_equivalent a b p :=

Iainmon

Lemma my_eq_sym: forall a b : Set, a = b -> b = a.
Proof.
  intros a b.
  intros H.
  rewrite -> H || rewrite <- H.
  reflexivity.
Qed.

Ltac inv H := inversion H; clear H; try subst.

Iainmon

module Ficu where

import Text.Parsec
    ( anyChar,
      char,
      noneOf,
      oneOf,
      between,
      choice,
      many1,

Iainmon

proc convShape() {}

iter regions(dom: domain(2,int), k: int, stride: int) {
    const (h,w) = convShape(dom.shape,k,stride,padding=0);
    for (i,j) in {0..#h,0..#w} {
        yield dom[i * k * stride..#k,j * k * stride..#k];
    }
}

Iainmon

INCLUDE Irvine32.inc

; #define MAX_ITER 45
; int main() {
;     int n;
;     int m;
;     int tmp;
;     int i;
;     i = 0;
;     n = 0;

Iainmon

import Control.Applicative ( Alternative(empty, (<|>)) )

newtype Branch s a = Branch (s -> [(a,s)])

branch :: (s -> [(a,s)]) -> Branch s a
branch = Branch

run :: Branch s a -> (s -> [(a,s)])
run (Branch f) = f

Iainmon

const float rt = sqrt(2.);

float anim(float speed) {
    return (.5*sin(iTime * speed)) + 0.5;
}

const vec3 paint = vec3(0.17, 0.55, 0.70);

void mainImage( out vec4 fragColor, in vec2 fragCoord )