Plecra

-- Foundational logics tend to be stated in terms of derivations that produce valid sentences,
-- by replicating this with the style of proofs below we can encode a small implicational
-- calculus to get a lighter encoding of contexts.
-- 
-- this demo isn't complete yet, I still need to add all the normal results,
-- and to fully demonstrate the translation into contexts: we want a version of
-- cut elimination for the forall quantifier I've introduced.
-- generally, we can normalize all judgements required in typing derivations into the form `(forall x.)* (P =>)* C`,
-- removing the `forall`s via the IntroForall rule: This produces entailment directly.
--

Plecra

How to read typing rules, by Rust intuition

This is just a brief little walkthrough of how to interpret the simplest typing rules, by presenting them as Rust types to appeal to what you already know. There's plenty uncovered, but this should get you off to a great start!

(I originally wrote this in response to a particular question, so it's a little targeted. Anyone is very welcome to suggest edits, I might come by and fix it up later)

We want typing contexts because some expressions have free variables. To know the type of (x, y),

Plecra

use std::cell::{Cell};
use std::rc::Rc;
use std::collections::HashMap;
use std::ops;


// seen = 0 for all objects
// for each object in the queue
//     for child in object
//         if child not aggregate, continue

Plecra

#![allow(non_snake_case)]
use std::path::Path;
use std::cell::Cell;
use std::ffi::c_void;
use std::sync::atomic::{AtomicU32, Ordering};

use bindings::Windows::Win32::{
    Foundation::{HWND, LPARAM, PWSTR, WPARAM, E_UNEXPECTED, E_NOTIMPL},
    Media::{Audio::CoreAudio::GUID_NULL, MediaFoundation::*},
    System::LibraryLoader::GetModuleHandleW,

Plecra

use core::ptr;
use core::sync::atomic::{fence, AtomicPtr, AtomicUsize, Ordering};
use std::alloc;

#[cfg(not(target_pointer_width = "32"))]
const DIVISIONS: usize = 24;
#[cfg(target_pointer_width = "32")]
const DIVISIONS: usize = 12;

struct MonotonicVec<T> {

Plecra

[package]
name = "keylogger"
version = "0.1.0"
authors = ["..."]
edition = "2018"

[dependencies]
winit = { version = "0.23.0", features = ["serde"] }
chrono = { version = "0.4.19", features = ["serde"] }
serde = { version = "1.0", features = ["derive"] }

Plecra

pub enum ModifiedUtf8Error {
    Incomplete,
    Malformed,
}

/// Decode a Modified UTF-8 encoded string.
///
/// This encoding is used by Java for fast serialization of its strings, and
/// has some minor deviations from standard UTF-8.
pub fn from_modified_utf8(mut bytes: &[u8]) -> Result<String, ModifiedUtf8Error> {

Plecra

const HIGH_BIT: u8 = 0b10000000;
fn hi_bit_set(byte: u8) -> bool {
    byte & HIGH_BIT != 0
}

pub fn naive(buf: &mut &[u8]) -> Result<u64, ()> {
    let mut value = 0;
    let mut iter = buf.iter();
    for (count, &byte) in (&mut iter).enumerate().take(10) {
        value += u64::from(byte & !HIGH_BIT) << (count * 7);

Plecra

use error::*;
use nom::*;

#[derive(Debug, Clone)]
struct Complete<T>(T);
impl<T> Complete<T> {
    fn into_inner(self) -> T {
        self.0
    }
}

Plecra

use anyhow::*;
use futures::io::{copy, AsyncReadExt, AsyncWriteExt};
use futures::stream::StreamExt;
use log::*;
use smol::Async;

use std::net;

const PORT: u16 = 5000;