dram dramforever

dram.like || (wip && interesting)

A bit of extra stuff

TODO Make on-configuration-change restart more specific
TODO Alert users for configuration migration
- ghcSimple.useObjectCode is gone.
- ghcSimple.workspaceType is gone.

This is a link to something, which is cleaner.

This is a description of the mirroring script at tuna/tunasync-scripts#49 (and other related things)

Links:

NixOS/nixpkgs#32659 (Asking about how to create a mirror)
tuna/issues#323 (TUNA mirror request)
tuna/tunasync-scripts#49 (PR with script to TUNA mirror)
ustclug/mirrorrequest#165 (USTC mirror request)
ustclug/ustcmirror-images#57 (PR with script to USTC mirror)
http://www.shlug.org/discuss/2020/01/11/nixos_mirror.html (Discussion by @yuchangyuan, in Chinese)

	module Parser where

	newtype Parser a = P { parse :: String -> [(a, String)] }

	instance Functor Parser where
	fmap g p = P (\inp -> case parse p inp of
	[] -> []
	[(v, out)] -> [(g v, out)])

	instance Applicative Parser where

	Ltac detect :=
	match goal with
	\| [ \|- context G [ forall x : ?T, _ (* ?E *) ] ] =>
	idtac G T; fail
	end.

	Theorem test : (forall x, x = 1) = (forall x, x = 2).
	Proof.
	try detect.
	(* As shown above: _ matches inside binders expectedly

	module Hs8b.Register where

	import Clash.Prelude

	type Reg = Unsigned 4
	type Value = Unsigned 8

	{-# ANN registerFileMono Synthesize
	{ t_name = "register_file"
	, t_inputs = PortName <$> words "clk rst write read"

	class AccModule extends Module {
	val io = IO(new Bundle{
	val in = Input(UInt(32.W))
	val out = Output(UInt(32.W))
	})

	val reg = RegInit(0.U(32.W))
	reg := reg + io.in
	io.out := reg
	}