alessio-b-zak

pmmc <- function(y, initialState, proposal, nparticles, nsteps, dprior, fixParams, initVarParams, pf, ncores) {
  # intialise vector to store generated samples
  samples <- matrix(,nrow = length(initVarParams), ncol = nsteps+1)
  # calculate log likelihood for initial parameter guess
  oldLL <- pf(y, c(fixParams, initVarParams), nparticles, initialState, ncores)
  # extract fixed parameters
  # extract variable parameters
  samples[,1] <- initVarParams
  newVal <- 0

alessio-b-zak

// [[Rcpp::depends(RcppArmadillo)]]
#include <RcppArmadillo.h>
#include <RcppArmadilloExtensions/sample.h>
#include <RcppParallel.h>
#include <dqrng_distribution.h>
#include <boost/random/binomial_distribution.hpp>
#include <boost/random/poisson_distribution.hpp>
#include <xoshiro.h>
#include <omp.h>
using namespace arma;

alessio-b-zak

// [[Rcpp::depends(RcppArmadillo)]]
#include <RcppArmadillo.h>
#include <RcppArmadilloExtensions/sample.h>
#include <RcppParallel.h>
#include <dqrng_distribution.h>
#include <boost/random/binomial_distribution.hpp>
#include <xoshiro.h>
#include <omp.h>
using namespace arma;
using namespace Rcpp;

alessio-b-zak

// [[Rcpp::depends(RcppArmadillo)]]
#include <RcppArmadillo.h>
#include <RcppArmadilloExtensions/sample.h>
using namespace arma;
using namespace Rcpp;


void resampleParticles(Rcpp::NumericMatrix& rParticles,
                       Rcpp::NumericMatrix& particles,
                       Rcpp::NumericVector& weights){

alessio-b-zak

Bool-elim : ∀ {a} {A : Bool → Set a} → A true → A false → (i : Bool) → A i
Bool-elim x y true = x
Bool-elim x y false = y

⟨_×_⟩ : ∀ {A B A′ B′} → A ⇒ A′ → B ⇒ B′ → A × B ⇒ A′ × B′
⟨_×_⟩ {A} {B} {A′} {B′} f g
  = Bld.times (A ×′ B) (A′ ×′ B′) (Bool-elim f g)

alessio-b-zak

Bool-elim : ∀ {a} {A : Bool → Set a} → A true → A false → (i : Bool) → A i
Bool-elim x y true = x
Bool-elim x y false = y

⟨_×_⟩ : ∀ {A B A′ B′} → A ⇒ A′ → B ⇒ B′ → A × B ⇒ A′ × B′
⟨_×_⟩ {A} {B} {A′} {B′} f g
  = Bld.times (A ×′ B) (A′ ×′ B′) (Bool-elim f g)

alessio-b-zak

module Monoids where

open import Level
open import Relation.Binary.PropositionalEquality
open import Function hiding (id)


record Monoid (a : Level) : Set (Level.suc a) where
  field
    Underlying : Set a 

alessio-b-zak

rossHelp : Num a => tensor s a -> tensor s a -> tensor s a
rossHelp {s = []} x y = x + y
rossHelp {s = (Z :: xs)} [] y = ?rossHelp_rhs_1
rossHelp {s = ((S len) :: xs)} (x :: ys) y = ?rossHelp_rhs_2

alessio-b-zak

replaceAtProof : (xs : Vect n a)
              -> (i : Fin n)
              -> (f : a -> b)
              -> ((index i xs) = x)
              -> (map f xs) = (replaceAt i (f x) (map f xs))
replaceAtProof [] FZ _ _ impossible
replaceAtProof [] (FS _) _ _ impossible
replaceAtProof (x :: xs) FZ f Refl = Refl
replaceAtProof (x :: xs) (FS y) f Refl =
  let replacedElement = replaceAt y (f (index y xs)) (map f xs)

alessio-b-zak

--Proofs in idris are primarily done in 3 ways.

--Using the propositional equality data type to express the fact that
--two expressions are equal.
--e.g. (a = b) says that a can be reduced to b

--Another proof is by constructing an explicit data type
--e.g. (Fin n) which implicitly carries round a proof that the elem is less
--that something (I call these predicates but I don't know if they are.)
--Other examples include Elem