Commit 4cf1a317 authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent cd5b4820
SHELL := /bin/bash
IDRIS = idris
IDRIS = idris2
IDRISFLAGS = -p contrib -p effects -V --allow-capitalized-pattern-variables
libs:
......
module SequentialDecisionProblems.CoreTheory
import Sigma.Sigma
import Sigma.Operations
%auto_implicits off
public export
State : (t : Nat) -> Type
public export
Ctrl : (t : Nat) -> (x : State t) -> Type
public export
M : Type -> Type
public export
nexts : (t : Nat) -> (x : State t) -> (y : Ctrl t x) -> M (State (S t))
public export
fmap : {A, B : Type} -> (A -> B) -> M A -> M B
postulate functorSpec1 : fmap . id = id
postulate functorSpec2 : {A, B, C : Type} -> {f : B -> C} -> {g : A -> B} ->
fmap (f . g) = (fmap f) . (fmap g)
> module SequentialDecisionProblems.CoreTheory
> import Sigma.Sigma
> public export
> record SDP where
> constructor MkSDP
> M : Type -> Type
> fM : Functor M
> X : (t : Nat) -> Type
> Y : (t : Nat) -> (x : X t) -> Type
> next : (t : Nat) -> (x : X t) -> (y : Y t x) -> M (X (S t))
> Val : Type
> reward : (t : Nat) -> (x : X t) -> (y : Y t x) -> (x' : X (S t)) -> Val
> (<+>) : Val -> Val -> Val
> zero : Val
> (<=) : Val -> Val -> Type
> meas : M Val -> Val
> Policy : SDP -> (t : Nat) -> Type
> Policy sdp t = (x : X sdp t) -> Y sdp t x
> data PolicySeq : SDP -> (t : Nat) -> (n : Nat) -> Type where
> Nil : {sdp : SDP} -> {t : Nat} ->
> PolicySeq sdp t Z
> (::) : {sdp : SDP} -> {t, n : Nat} ->
> Policy sdp t -> PolicySeq sdp (S t) n -> PolicySeq sdp t (S n)
> val : {sdp : SDP} -> {t, n : Nat} -> PolicySeq sdp t n -> X sdp t -> Val sdp
> val {sdp} {t} Nil x = zero sdp
> val {sdp} {t} (p :: ps) x = let y = p x in
> let mx' = next sdp t x y in
> let fM' = fM sdp in
> meas (map (\ x' => ((<+>) sdp) (reward sdp t x y x') (val ps x')) mx')
> {-
> ---}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment