Lysxia

{-# LANGUAGE
    PolyKinds,
    InstanceSigs,
    DataKinds,
    GADTs #-}

module Cat where

import Control.Category
import Prelude hiding ((.))

Lysxia

efactor' :: Integer -> Float -> Float
efactor' x y
    | ef < 1.3 = 1.3
    | ef > 2.5 = 2.5
    | otherwise = ef
    where ef = y - 0.8 + 0.28 * q - 0.02 * q * q
          q = fromIntegral x :: Float

Lysxia

Class Container : Type :=
  { Shape : Type;
    Pos : Shape -> Type;
  }.

Inductive Ext (C : Container) (A : Type) :=
| ext : forall s, (forall p : Pos s, A) -> Ext C A.

Class HContainer : Type :=
  { C0 :> Container;

Lysxia

(* Untyped lambda calculus *)

(* Terms with free variables in [V]. *)
Inductive term {V : Type} : Type :=
| Var : V -> term
| App : term -> term -> term
| Lam : @term (unit + V) -> term
.

Arguments term : clear implicits.

Lysxia

Require Import List.
Import ListNotations.

Notation "0" := false : bool_scope.
Notation "1" := true : bool_scope.
Local Open Scope bool_scope.

Inductive tape :=
| Tape (l : list bool) (b : bool) (r : list bool)
.

Lysxia

withFunction :: (Int -> IO b) -> IO b
withFunction fun = do
  let val = 3
  fun val
  
  
class WithFunction proxy where
  withFunction_ :: proxy -> (Int -> IO b) -> IO b

data Number1 = Number1

Lysxia

Set Primitive Projections.

Record pr : Type := { fst : nat ; snd : nat }.

Goal forall x : pr, x = let (u, v) := x in {| fst := u ; snd := v |}.
Proof.
  intros. cbn.
  reflexivity.
Qed.

Lysxia

Require Arith.
Require Import List.
Import ListNotations.


(** * Coinductive types and coinduction *)

Lysxia

Inductive bitarray : nat -> Type :=
| empty : bitarray O
| cons  : forall (sz : nat), bool -> bitarray sz -> bitarray (S sz)
.
 
Notation "{| |}" := empty.
Notation "{| x |}" := (cons _ x empty).
Notation "{| x ; y ; .. ; z |}" := (cons _ x (cons _ y .. (cons _ z empty) .. )).
 
Check {| true; true; false |}.

Lysxia

Require Import List.
Import ListNotations.
Fixpoint tuple (ts : list Type) : Type :=
  match ts with
  | [] => unit
  | t :: ts' => (t * tuple ts')%type
  end.