Skip to content

Instantly share code, notes, and snippets.

View larsrh's full-sized avatar
🏝️
On hiatus.

Lars Hupel larsrh

🏝️
On hiatus.
View GitHub Profile
@larsrh
larsrh / perm.rs
Last active April 9, 2023 09:25
Rust implementation of high-level Unix file permission handling
use anyhow::{Error, Result};
use bitflags::bitflags;
use std::convert::TryFrom;
use std::fs::Permissions;
use std::os::unix::fs::PermissionsExt;
bitflags! {
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub struct Perms: u16 {
const UR = 0o400;
@larsrh
larsrh / gen.pl
Created March 28, 2020 17:19
Experiments with program generation in Prolog
:- discontiguous nat/2.
:- discontiguous typ/2.
natlit(0, _).
natlit(X, s(N)) :-
natlit(Y, N),
X is Y + 1.
nat(lit(nat, X), s(N)) :- natlit(X, N).
@larsrh
larsrh / witness.scala
Created July 19, 2019 07:03
Arbitrary[Arbitrary]
import $ivy.`org.scalacheck::scalacheck:1.14.0`
import org.scalacheck._
import org.scalacheck.Arbitrary._
import scala.reflect._
trait TypeWitness1 {
type F[_]
val name: String
def lift[A](implicit arb: Arbitrary[A]): Arbitrary[F[A]]
@larsrh
larsrh / demo1.scala
Last active September 14, 2018 14:18
LX Scala 2018/Scala Italy 2018 demo code: "Numeric programming with spire"
val cities1 = Map("Portugal" -> List("Lisbon"), "Spain" -> List("Madrid"))
val cities2 = Map("Portugal" -> List("Coimbra"))
cities1 |+| cities2
@larsrh
larsrh / scheduler.pl
Created March 19, 2018 11:24
Tiny job scheduler in SWI Prolog, for tutorial purposes.
:- dynamic running/2.
:- dynamic jobid/1.
jobid(0).
resource(node1, 1, linux).
resource(node2, 2, linux).
resource(node3, 1, macos).
capacity(Node, Capacity) :- resource(Node, Capacity, _).
@larsrh
larsrh / conditional.scala
Last active February 13, 2018 01:59
Summon a conditional implicit
/*
* implicit conversion ("view"): implicit def f(x: A): B
* non-view implicit: implicit def f(implicit x: A): B
*
* we can summon implicit conversions with `implicitly[A => B]`
* we can't do that with non-view implicits
* this macro provides the trait `Conditional[A, B]` that provides precisely that
*/
package conditional
@larsrh
larsrh / Proofs.idr
Last active November 20, 2017 17:58
Idris code from Munich Lambda meetup, 2017-11-20
module Proofs
%default total
data Natural : Type where
Zero : Natural
Succ : Natural -> Natural
add : Natural -> Natural -> Natural
add Zero y = y
@larsrh
larsrh / proposal.md
Last active August 3, 2017 20:52
Draft proposal for sbt upgrade

Aid the ecosystem in upgrading to sbt 1.0.x

Proposer

Proposed by Lars Hupel.

Abstract

Scala 2.10 used to (and still has, to some extent), huge gravitas in the Scala ecosystem. To large parts, this was due to Spark and sbt supporting only 2.10. Spark has migrated to 2.11, and sbt 1.0.x is already there (the RCs are binary compatible).

@larsrh
larsrh / lambda.fst
Created May 18, 2017 06:21
F* code from Munich Lambda meetup, 2017-05-17
module Lambda
open FStar.Mul
val factorial: n:nat -> Tot (y:nat{y >= 1 /\ y >= n})
let rec factorial n =
if n = 0 then
1
else
n * factorial (n - 1)
@larsrh
larsrh / build.sbt
Created March 15, 2017 10:29
Packaging a compiler plugin with dependencies (requires sbt-assembly)
// can be used like this:
// addCompilerPlugin("local.whatever" %% "whatever-plugin" % "0.1-SNAPSHOT" classifier "assembly" cross CrossVersion.patch)
name := "whatever-plugin"
organization := "local.whatever"
scalaVersion := "2.12.0"
crossScalaVersions := Seq("2.12.0", "2.12.1", "2.11.8", "2.11.7", "2.11.6")