From 9afee48c78cba9f394df78e4973613f1e2bc4779 Mon Sep 17 00:00:00 2001 From: Julin S Date: Tue, 23 May 2023 22:04:54 +0530 Subject: [PATCH] add a bunch of old files --- awk/one.awk | 75 +++++++++ coq/README.org | 1 + coq/hlist-shallow.v | 57 +++++++ coq/log10-casteran.v | 75 +++++++++ coq/nat2str.v | 32 ++++ coq/nth_tuple.v | 25 +++ coq/parity.v | 252 ++++++++++++++++++++++++++++ coq/ranged.v | 37 ++++ coq/re.v | 109 ++++++++++++ coq/records.v | 18 ++ coq/sigs.v | 11 ++ coq/unfinished/33-miniatures-fibo.v | 54 ++++++ coq/unfinished/at-most.v | 94 +++++++++++ coq/unfinished/calc-ce.v | 112 +++++++++++++ coq/unfinished/chlipala-oplls.v | 74 ++++++++ coq/unfinished/covariance.v | 13 ++ coq/unfinished/datetime.v | 7 + coq/unfinished/email.v | 37 ++++ coq/unfinished/hanoi.v | 127 ++++++++++++++ coq/unfinished/kmt.v | 24 +++ coq/unfinished/phoas-stlc2cps.v | 112 +++++++++++++ coq/unfinished/regex-harper.v | 57 +++++++ coq/unfinished/regex.v | 120 +++++++++++++ coq/unfinished/subtypes.v | 168 +++++++++++++++++++ coq/unfinished/water-jars.v | 11 ++ coq/unique-list.v | 19 +++ coq/vector_nth.v | 84 ++++++++++ cpp/optional-fopen.cpp | 38 +++++ cpp/optional.cpp | 41 +++++ elisp/README.org | 3 + elisp/matrix-gen.el | 93 ++++++++++ latex/expl3-hello.tex | 17 ++ latex/listings-define-lang.tex | 33 ++++ latex/tikz-automata.tex | 24 +++ metapost/dots-lines.mp | 10 ++ metapost/hello.mp | 19 +++ misc/uclid5-hello.ucl | 31 ++++ ocaml/stlc.ml | 57 +++++++ racket/chess.rkt | 107 ++++++++++++ racket/hello.rkt | 29 ++++ racket/pics.rkt | 68 ++++++++ sml/comb.sml | 19 +++ vimscript/README.org | 3 + vimscript/five.vim | 61 +++++++ vimscript/latex.vim | 31 ++++ vimscript/md.vim | 206 +++++++++++++++++++++++ vimscript/py-eg.vim | 16 ++ vimscript/supersub.vim | 43 +++++ 48 files changed, 2754 insertions(+) create mode 100644 awk/one.awk create mode 100644 coq/hlist-shallow.v create mode 100644 coq/log10-casteran.v create mode 100644 coq/nat2str.v create mode 100644 coq/nth_tuple.v create mode 100644 coq/parity.v create mode 100644 coq/ranged.v create mode 100644 coq/re.v create mode 100644 coq/records.v create mode 100644 coq/sigs.v create mode 100644 coq/unfinished/33-miniatures-fibo.v create mode 100644 coq/unfinished/at-most.v create mode 100644 coq/unfinished/calc-ce.v create mode 100644 coq/unfinished/chlipala-oplls.v create mode 100644 coq/unfinished/covariance.v create mode 100644 coq/unfinished/datetime.v create mode 100644 coq/unfinished/email.v create mode 100644 coq/unfinished/hanoi.v create mode 100644 coq/unfinished/kmt.v create mode 100644 coq/unfinished/phoas-stlc2cps.v create mode 100644 coq/unfinished/regex-harper.v create mode 100644 coq/unfinished/regex.v create mode 100644 coq/unfinished/subtypes.v create mode 100644 coq/unfinished/water-jars.v create mode 100644 coq/unique-list.v create mode 100644 coq/vector_nth.v create mode 100644 cpp/optional-fopen.cpp create mode 100644 cpp/optional.cpp create mode 100644 elisp/README.org create mode 100644 elisp/matrix-gen.el create mode 100644 latex/expl3-hello.tex create mode 100644 latex/listings-define-lang.tex create mode 100644 latex/tikz-automata.tex create mode 100644 metapost/dots-lines.mp create mode 100644 metapost/hello.mp create mode 100644 misc/uclid5-hello.ucl create mode 100644 ocaml/stlc.ml create mode 100644 racket/chess.rkt create mode 100644 racket/hello.rkt create mode 100644 racket/pics.rkt create mode 100644 sml/comb.sml create mode 100644 vimscript/README.org create mode 100644 vimscript/five.vim create mode 100644 vimscript/latex.vim create mode 100644 vimscript/md.vim create mode 100644 vimscript/py-eg.vim create mode 100644 vimscript/supersub.vim diff --git a/awk/one.awk b/awk/one.awk new file mode 100644 index 0000000..8020021 --- /dev/null +++ b/awk/one.awk @@ -0,0 +1,75 @@ +# Use with gawk + +function timeliner(line) { + split(line, hms, ":") + h = hms[1] + m = hms[2] + split(hms[3], sms, ",") + s = sms[1] + ms = sms[2]/10 + rv = sprintf("%d:%02d:%02d.%02d",h,m,s,ms) + return rv +} + +function flush(IDX, start, end, TEXT) { + initial = "Dialogue: Marked=0" + middle = "DefaultVCD, NTP,0000,0000,0000,,{\pos(400,570)}" + sstart = timeliner(start) + send = timeliner(end) + printf("%s,%s,%s,%s,%s\n", initial, sstart, send, middle, TEXT) +} + +BEGIN{ + # Rows separated by blank lines + #RS = ""; + + # Columns separated by new lines + #F = "\n" + + IDX = 0 + TIME = 0 + TEXT = "" +} + + # Change if ending is CRLF + sub(/\r$/,"") {} + + # gawk has 3 arg match, but not awk + match($0, /^([0-9]+$)/, a) { + if (IDX==0 && TIME==0) { + IDX=a[1] + next + } + } + + match($0, /([0-9]{2}:[0-9]{2}:[0-9]{2},[0-9]{3}) --> ([0-9]{2}:[0-9]{2}:[0-9]{2},[0-9]{3})/, a) { + if (IDX!=0 && TIME==0) { + start = a[1] + end = a[2] + + # Set flag + TIME = 1 + + TEXT = "" + next + } + } + + # Anything other than a blank line + !/^\s*$/ { + TEXT = TEXT$0 + } + + match($0, /^$/, a) { + if (IDX!=0 && TIME!=0) { + flush(IDX, start, end, TEXT) + + # Reset flags + TIME = 0 + IDX = 0 + } + } + + END { + flush(IDX, start, end, TEXT) + } diff --git a/coq/README.org b/coq/README.org index 6962d44..373f5e0 100644 --- a/coq/README.org +++ b/coq/README.org @@ -1,5 +1,6 @@ #+TITLE: Coq + - [[./hlist-shallow.v][hlist.shallow.v]]: hlist with normal list under the hood - [[./hlist.v][hlist.v]]: Hlist (with notations) - [[./union.v][union.v]]: Mimicking a set operation using lists - [[./bv.v][bv.v]]: Demo of a few bitvector operations diff --git a/coq/hlist-shallow.v b/coq/hlist-shallow.v new file mode 100644 index 0000000..baefeca --- /dev/null +++ b/coq/hlist-shallow.v @@ -0,0 +1,57 @@ +Require Import List. +Import ListNotations. + +Fixpoint hlist (l:list Type):Type := + match l with + | [] => unit + | t::ts => t * (hlist ts) + end. + +Definition hd {t:Type} {ts:list Type} + (l:hlist (t::ts)) : t := fst l. +Definition tl {t:Type} {ts:list Type} + (l:hlist (t::ts)) : hlist ts := snd l. + +Definition hnil : hlist [] := tt. + +Definition hcons {t:Type} {ts:list Type} (a:t) + : hlist ts -> hlist (t::ts) := + match ts with + | [] => fun _ => (a, tt) + | (x::xs) => fun hl => (a, hl) + end. + +Fixpoint append {ts1 ts2:list Type} : + hlist ts1 -> hlist ts2 -> hlist (ts1 ++ ts2) := + match ts1 with + | [] => fun _ => fun hl2 => hl2 + | t::ts => fun hl1 => fun hl2 => + (*hcons (hd hl1) (append (tl hl1) hl2)*) + (hd hl1, append (tl hl1) hl2) + end. + +Example foo0 : hlist [nat:Type] := (2,tt). +Compute hcons 3 foo0. +(* + = (3, (2, tt)) + : hlist [nat; nat : Type] +*) + +Compute hcons true (hcons 3 foo0). +(* + = (true, (3, (2, tt))) + : hlist [bool; nat; nat : Type] +*) + +Example foo1 : hlist [nat:Type; bool:Type] := (2,(true,tt)). +Compute append foo1 foo0. +(* + = (2, (true, (2, tt))) + : hlist ([nat : Type; bool : Type] ++ [nat : Type]) +*) + +Compute append foo1 (hcons 3 foo0). +(* + = (2, (true, (3, (2, tt)))) + : hlist ([nat : Type; bool : Type] ++ [nat; nat : Type]) +*) diff --git a/coq/log10-casteran.v b/coq/log10-casteran.v new file mode 100644 index 0000000..7e5d89e --- /dev/null +++ b/coq/log10-casteran.v @@ -0,0 +1,75 @@ +Require Import Recdef. +Require Import ZArith Lia. + +Compute (2/3)%Z. + +Fail Fixpoint log10 (n:Z): Z := + if Zlt_bool n 10 then 0 + else 1 + log10 (n/10). + +Fail Program Fixpoint log10 (n:nat): nat := + if Nat.ltb n 10 then 0 + else 1 + log10 (Nat.div n 10). + +Function log10 (n:Z) {measure Z.abs_nat n} : nat := + if Z.ltb n 10 then 0 + else 1 + log10 (n/10). +Proof. + intros n H. + rewrite Z.ltb_ge in H. + Search (Z.abs_nat). + Search (_ / _)%Z. + rewrite Nat2Z.inj_abs_nat. + lia. + + + + rewrite Z.ltb_nlt in H. + rewrite (Znot_lt_ge n 10) in H. + Search (~(_ < _)-> _)%Z. + + induction n. + - now simpl. + - + - Search ((_ (_ <=? _))%Z. + Search ((_ <=? _) -> (_ / _))%Z. + +Locate "_ nat -> nat). +Search (nat -> nat). +Compute Nat.div 12 10. + +Fail Fixpoint log10 (n:nat): nat := + if Nat.ltb n 10 then 0 + else S (log10 (Nat.div n 10)). +(* Error: *) +(* Recursive definition of log10 is ill-formed. *) +(* In environment *) +(* log10 : nat -> nat *) +(* n : nat *) +(* Recursive call to log10 has principal argument equal to *) +(* "Nat.div n 10" instead of *) +(* a subterm of "n". *) +(* Recursive definition is: *) +(* "fun n : nat => *) +(* if Nat.ltb n 10 then 0 else S (log10 (Nat.div n 10))". *) + + +Function log10 (n:nat) {measure n} : nat := + if Nat.ltb n 10 then 0 + else S (log10 (Nat.div n 10)). diff --git a/coq/nat2str.v b/coq/nat2str.v new file mode 100644 index 0000000..aae026a --- /dev/null +++ b/coq/nat2str.v @@ -0,0 +1,32 @@ +Require Import String +Open Scope String. + +Definition digit2str (n:nat):string:= + match n with + | 0 => "0" + | 1 => "1" + | 2 => "2" + | 3 => "3" + | 4 => "4" + | 5 => "5" + | 6 => "6" + | 7 => "7" + | 8 => "8" + | 9 => "9" + | _ => "" + end. + +Fixpoint nat2str_helper (n:nat) : string := + match n with + | O => "" + | _ => + let digit := Nat.modulo n 10 in + (nat2str_helper (Nat.div n 10)) ++ (digit2str digit) + end. + +Definition nat2str (n:nat) : string := + match n with + | O => "0" + | _ => nat2str_helper n + end. + diff --git a/coq/nth_tuple.v b/coq/nth_tuple.v new file mode 100644 index 0000000..e936a65 --- /dev/null +++ b/coq/nth_tuple.v @@ -0,0 +1,25 @@ +(* +https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Project.20nth.20element.20of.20n-tuple + +Soln by guillaume melquiond: https://www.lri.fr/~melquion/index.html.en +*) + +Require Import List. + +Definition nth_tup {l : list Type}: + forall (x:fold_right prod unit l) (n:nat), nth n l unit. +Proof. +induction l as [|A l IH]. +- intros _ [|] ; exact tt. +- intros [a b] [|n]. + exact a. + now apply IH. +Restart. + induction l. + - intros _ [|]. + + exact tt. + + exact tt. + - intros H n. + + apply (IHl H). +Defined. diff --git a/coq/parity.v b/coq/parity.v new file mode 100644 index 0000000..24f1ae5 --- /dev/null +++ b/coq/parity.v @@ -0,0 +1,252 @@ +Require Import ZArith. +Require Import Arith. +Require Import Lia. + +Definition Zeven_even : forall n m:Z, + ((Z.Even n) /\ (Z.Even m)) + -> Z.Even (n+m) /\ Z.Even (n-m). + intros n m [[p Hp] [q Hq]]. + unfold Z.Even. + rewrite Hp. + rewrite Hq. + split. + - exists (p+q)%Z. + lia. + - exists (p-q)%Z. + lia. +Qed. + + +Definition Zodd_odd : forall n m:Z, + ((Z.Odd n) /\ (Z.Odd m)) + -> Z.Even (n+m) /\ Z.Even (n-m). +Proof. + intros n m [[p Hp] [q Hq]]. + unfold Z.Even. + rewrite Hp. + rewrite Hq. + split. + - exists (p+q+1)%Z. + lia. + - exists (p-q)%Z. + lia. +Qed. + +Definition Zeven_odd : forall n m:Z, + (Z.Even n) /\ (Z.Odd m) + -> Z.Odd (n+m) /\ Z.Odd (n-m). +Proof. + intros n m [[p Hp] [q Hq]]. + unfold Z.Odd. + rewrite Hp. + rewrite Hq. + split. + - exists (p+q)%Z. + lia. + - exists (p-q-1)%Z. + lia. +Qed. + +Fixpoint sum_i_n (start:Z) (n:nat):Z := + match n with + | O => 0%Z + | S n' => start + (sum_i_n (start+1) n') + end. +Compute sum_i_n 1 10. + +Search (nat -> Z). + +Lemma Even_0: Nat.Even 0. +Proof. + unfold Nat.Even. + exists 0. + reflexivity. +Qed. + + +Require Import Arith ZArith. + +Lemma Odd_Nat_Z : forall n:nat, + Nat.Odd n -> Z.Odd (Z.of_nat n). +Proof. + intros n H. + destruct n. + - destruct H. + lia. + - destruct H. + unfold Z.Odd. + rewrite H. + Search (Nat.Odd _ -> Z.Odd _). + unfold Z.of_nat. + lia. +unfold Z.Odd. + + unfold Z.Odd. + unfold Z.of_nat. +Theorem foo: forall n:nat, + Nat.Odd n -> + Z.Odd (sum_i_n 1 n). +Proof. + intros n H. + induction n. + - simpl. + Search (Z.Odd). + Search (Nat.Even). + +Print Z. +Search (N -> Z). +Compute Z.of_N 2. + +(* +Fixpoint sumn_aux (n acc:nat) : nat := + match n with + | O => acc + | S n' => n + (sumn_aux n' acc) + end. +Definition sumn (n:nat) : nat := sumn_aux n 0. + +Lemma nat_sum_n (n:nat): sumn n = (n*(n+1)/2). +Proof. + unfold sumn. + induction n. + - trivial. + - simpl. + rewrite IHn. + simpl. + unfold sumn_aux. + +Lemma foo: forall n:nat, + Nat.Odd n -> Z.Odd (Z.of_nat (sumn n)). +Proof. + intros n H. + unfold sumn. + unfold Z.Odd. + unfold sumn_aux. +*) + +(*************************************************************) +(* nat *) +(*************************************************************) +Require Import Arith. +Require Import Lia. + +Definition even_even : forall n m:nat, + ((Nat.Even n) /\ (Nat.Even m)) + -> Nat.Even (n+m) /\ Nat.Even (n-m). + intros n m [[p Hp] [q Hq]]. + split. + - unfold Nat.Even. + rewrite Hp. + rewrite Hq. + exists (p+q). + lia. + - unfold Nat.Even. + rewrite Hp. + rewrite Hq. + exists (p-q). + lia. +Qed. + +Definition odd_odd : forall n m:nat, + ((Nat.Odd n) /\ (Nat.Odd m)) + -> Nat.Even (n+m) /\ Nat.Even (n-m). +Proof. + intros n m [[p Hp] [q Hq]]. + unfold Nat.Even. + rewrite Hp. + rewrite Hq. + split. + - exists (p+q+1). + lia. + - exists (p-q). + lia. +Qed. + + + + +Definition even_odd : forall n m:nat, + n < m + -> (Nat.Even n) /\ (Nat.Odd m) + -> Nat.Odd (n+m) /\ Nat.Odd (n-m). +Proof. + intros n m H [[p Hp] [q Hq]]. + unfold Nat.Odd. + subst. + split. + - exists (p+q). + lia. + - exists (p-q-1). + (* --output DPI-1 --mode 1960x1080 *) + lia. + simpl. + rewrite (Nat.add_0_r p). + rewrite (Nat.add_0_r q). + simpl. + Search (_ + 0 = _). + lia. +Qed. + +Definition odd_even : forall n m:nat, + (Nat.Odd m) /\ (Nat.Even n) + -> Nat.Odd (n+m). +Proof. + intros n m [[p Hp] [q Hq]]. + exists (p+q). + lia. +Qed. + + + +Lemma odd7: Nat.Odd 7. +Proof. + unfold Nat.Odd. + exists 3. + lia. +Qed. + + +Lemma even4: Nat.Even 4. +Proof. + unfold Nat.Even. + exists 2. + lia. +Qed. + +(* +Definition even_even_b : forall n m:nat, + andb (Nat.even n) (Nat.even m) = true + -> Nat.even (n+m) = true. +Proof. + intros n m H. + induction n. + - trivial. + - Abort. + +Definition even_even : forall n m:nat, + ((Nat.Even n) /\ (Nat.Even m)) + -> Nat.Even (n+m). + intros n m H. + destruct H. + Search (Nat.Even). + induction n. + - trivial. + - simpl. + + + destruct IHn. + trivial. + + simpl. + destruct H. + rewrite Nat.Even_succ. + Search (Nat.Even). + destruct IHn. + * split. + simpl. + rewrite Nat.Even_succ in H. + try contradiction. + +(* + +*) +*) diff --git a/coq/ranged.v b/coq/ranged.v new file mode 100644 index 0000000..aae5eec --- /dev/null +++ b/coq/ranged.v @@ -0,0 +1,37 @@ +Require Import Streams. +Require Import Lia. + +Inductive range {A:Type} (p:A->Prop) (low high:nat) + : Stream A -> nat -> Prop := +| RangeStart: forall (s:Stream A), + range p low high s 0 +| RangeMore: forall (s:Stream A) (n:nat), + n>=low /\ (S n)<=high + -> p (hd s) + -> range p (low-1) (high-1) (tl s) n + -> range p low high s (S n). + +Definition egstr1 := const 3. + +Goal + range (fun x=>x=2) 2 5 + (Cons 2 (Cons 2 (Cons 2 (Cons 2 (Cons 2 egstr1))))) 3. +Proof. + eapply RangeMore; simpl; try lia. + eapply RangeMore; simpl; try lia. + eapply RangeMore; simpl; try lia. + eapply RangeStart. +Qed. + + +(* +Inductive range {A:Type} (p:A->Prop) (low high:nat) + : Stream A -> nat -> Prop := +| RangeDone: forall (s:Stream A) (n:nat), + n>=low /\ n<=high + -> range p low high s n +| RangeMore: forall (s:Stream A) (n:nat), + p (hd s) + -> range p low high (tl s) (S n) + -> range p low high s n. +*) diff --git a/coq/re.v b/coq/re.v new file mode 100644 index 0000000..669126f --- /dev/null +++ b/coq/re.v @@ -0,0 +1,109 @@ +Require Import Ascii String. + +Inductive re : Set := +| Atom: Ascii.ascii -> re +| Epsilon: re +| Dot: re +| Concat: re -> re -> re +| Alt: re -> re -> re +| Star: re -> re. + +Inductive reDenote : re -> string -> Prop := +| AtomDe: forall ch:Ascii.ascii, + reDenote (Atom ch) (String ch EmptyString) +| EpsilonDe: reDenote Epsilon EmptyString +| DotDe: forall ch:Ascii.ascii, + reDenote Dot (String ch EmptyString) +| ConcatDe r1 r2: forall s1 s2 s:string, + reDenote r1 s1 -> reDenote r2 s2 -> s = append s1 s2 + -> reDenote (Concat r1 r2) s +| AltDe r1 r2: forall s:string, + reDenote r1 s \/ reDenote r2 s + -> reDenote (Alt r1 r2) s +| StarDe r: forall s:string, + reDenote (Alt (Concat r (Star r)) Epsilon) s + -> reDenote (Star r) s. + +(* +Definition transl {r:re} {s:string} (inp:re) : reDenote r e := + match inp with + | Atom + | Epsilon: re + | Dot: re + | Concat: re -> re -> re + | Alt: re -> re -> re + | Star: re -> re. + end. + +re -> reDenote +forall s:string, (r:re) : reDenote r s +Atom ch => AtomDe ch +*) + +Infix "│" := Alt (at level 51, only parsing). +Infix ";" := Concat (at level 5, only parsing). +Notation " 'ε' " := Epsilon (only parsing). + +Goal + reDenote (Star (Atom "a"%char)) ""%string. +Proof. + refine (StarDe (Atom "a"%char) _ _). + refine (AltDe _ _ _ _). + right. + exact EpsilonDe. +Qed. + +Ltac rhamm := + match goal with + | _ => auto + | [ |- reDenote (Star _) _ ] => auto + end. + + +Goal + reDenote (Star (Atom "a"%char)) "a"%string. +Proof. + refine (StarDe _ _ _). + refine (AltDe _ _ _ _). + left. + refine (ConcatDe _ _ _ _ _ _ _ _). + - exact (AtomDe "a"). + - refine (StarDe _ _ _). + refine (AltDe _ Epsilon ""%string _). + right. + exact EpsilonDe. + - reflexivity. + Show Proof. +Restart. + eapply StarDe. + eapply AltDe. + left. + eapply ConcatDe. + - eapply AtomDe. + - eapply StarDe. + eapply AltDe. + right. + eapply EpsilonDe. + - reflexivity. + Show Proof. +Qed. + +Goal + reDenote (Atom "a"%char) "a"%string. +Proof. + exact (AtomDe "a"%char). +Qed. + +(* +Inductive reDenote : re -> string -> Prop := +| AtomDe: forall (ch:Ascii.ascii) (s:string), + reDenote (Atom ch) (String ch s) +| EpsilonDe: forall ch:Ascii.ascii, + reDenote Epsilon EmptyString. +| DotDe:: forall ch:Ascii.ascii, + reDenote Epsilon (String ch EmptyString). + +| ConcatDe: re -> re -> re +| AltDe: re -> re -> re +| StarDe: re -> re. +*) diff --git a/coq/records.v b/coq/records.v new file mode 100644 index 0000000..4f0ed24 --- /dev/null +++ b/coq/records.v @@ -0,0 +1,18 @@ +Require Import Streams. + +Record sAB {A B:Type} : Type := mksAB +{ sA : Stream A +; sB : Stream B +}. +Arguments mksAB {A B}. + +Check const. +Check const 3. +Definition egrec1 := mksAB (const 3) (const true). +Check sA egrec1. +Check sB egrec1. + +Notation " s '[' name ']' " := (name s) (at level 50). +Check egrec1 [ sA ]. +Check hd (egrec1 [ sA ]). +Compute hd (egrec1 [ sA ]). diff --git a/coq/sigs.v b/coq/sigs.v new file mode 100644 index 0000000..4d140be --- /dev/null +++ b/coq/sigs.v @@ -0,0 +1,11 @@ +Definition X' : {a:nat & {b: nat | a < b}}. +Proof. + exists 2, 3. + constructor. +Defined. + +(* From Pierre Castéran *) +Definition X : {a:nat & {b: nat & {c: nat | a + b = c}}}. +Proof. + now exists 3, 4, 7. +Defined. diff --git a/coq/unfinished/33-miniatures-fibo.v b/coq/unfinished/33-miniatures-fibo.v new file mode 100644 index 0000000..0590203 --- /dev/null +++ b/coq/unfinished/33-miniatures-fibo.v @@ -0,0 +1,54 @@ +Inductive m22 : Type := +| M22: nat -> nat -> nat -> nat -> m22. + +Definition m22Mult (n m:m22): m22 := + match n, m with + | M22 a b c d, M22 p q r s => + M22 (a*p+b*r) (a*q+b*s) (c*p+d*r) (c*q+d*s) + end. + +Definition M: m22 := (M22 1 1 1 0). + +Compute m22Mult (M22 5 3 3 2) M. +(* = M22 8 5 5 3 : m22 *) + +Fixpoint m22Pow (acc m:m22) (n:nat): m22 := + match n with + | 0 => acc + | S n' => m22Pow (m22Mult acc m) m n' + end. +Compute m22Pow M M 1. + +Fixpoint fibo_aux (acc:nat*nat) (n:nat): nat := + match n with + | 0 => snd acc + | S n' => + let '(a,b) := acc in + fibo_aux (a+b, a) n' + end. +Definition fibo (n:nat) : nat := fibo_aux (1,0) n. + +Definition projc12 (m:m22): nat := + match m with + | M22 _ _ c _ => c + end. + +Compute fibo 7. +Compute projc12 (m22Pow M M 7). + +Theorem foo: forall n:nat, + fibo (S n) = projc12 (m22Pow M M n). +Proof. + intros n. + induction n. + - unfold fibo. + now simpl. + - unfold fibo. + simpl. + unfold M. + simpl. + +Compute fibo 5. +Compute fibo 8. + + diff --git a/coq/unfinished/at-most.v b/coq/unfinished/at-most.v new file mode 100644 index 0000000..35ea1fb --- /dev/null +++ b/coq/unfinished/at-most.v @@ -0,0 +1,94 @@ +Require Import Streams. +Require Import Lia. + +Inductive exactly {A:Type} (p:A -> Prop) + : Stream A -> nat -> Prop := +| ExactDone: forall s:Stream A, exactly p s 0 +| ExactMore: forall (n:nat) (s:Stream A), + p (hd s) -> exactly p (tl s) n -> exactly p s (S n). + +Inductive atMost {A:Type} (p:A -> Prop) + : Stream A -> nat -> Prop := +| MostDone: forall (n:nat) (s:Stream A), + atMost p s n +| MostMore: forall (n:nat) (s:Stream A), + p (hd s) -> atMost p (tl s) n -> atMost p s (S n). + +CoInductive atLeast {A:Type} (p:A -> Prop) + : Stream A -> nat -> nat -> Prop := +| LeastDone: forall (N n:nat) (s:Stream A), + n>=N -> atLeast p s N n +| LeastDoneMore: forall (N n:nat) (s:Stream A), + n>=N -> p (hd s) -> atLeast p (tl s) N (S n) -> atLeast p s N n +| LeastMore: forall (N n:nat) (s:Stream A), + n<=N -> p (hd s) -> atLeast p (tl s) N (S n) -> atLeast p s N n. + +Inductive range {A:Type} (p:A->Prop) (low high:nat) + : Stream A -> nat -> Prop := +| RangeDone: forall (s:Stream A) (n:nat), + n>=low /\ n<=high + -> range p low high s n +| RangeMore: forall (s:Stream A) (n:nat), + p (hd s) + -> range p low high (tl s) (S n) + -> range p low high s n. + +Definition egstr1 := const 3. + +Goal + range (fun x=>x=2) 2 5 + (Cons 2 (Cons 2 (Cons 2 (Cons 2 (Cons 2 egstr1))))) 0. +Proof. + Check RangeMore. + eapply RangeMore; simpl; try lia. + eapply RangeMore; simpl; try lia. + (* eapply RangeDone; simpl; try lia. *) + eapply RangeMore; simpl; try lia. + eapply RangeMore; simpl; try lia. + eapply RangeMore; simpl; try lia. + eapply RangeDone; simpl; try lia. + (* eapply RangeMore; simpl; try lia. ✗ *) +Qed. + +Goal + atLeast (fun x=>x=3) (const 3) 0 0. +Proof. + apply LeastDone; simpl; lia. +Qed. + +Goal + atLeast (fun x=>x=2) (const 3) 0 0. +Proof. + apply LeastDone; simpl; lia. +Qed. + +Goal + atLeast (fun x=>x=2) + (Cons 2 (Cons 2 (Cons 2 (Cons 2 (Cons 2 egstr1))))) + 2 0. +Proof. + constructor 3; simpl; try lia. + apply LeastMore; simpl; try lia. + apply LeastMore; simpl; try lia. + apply LeastDoneMore; simpl; try lia. + apply LeastDoneMore; simpl; try lia. + apply LeastDone; simpl; lia. +Qed. + +Goal + atMost (fun x=>x=3) egstr1 2. +Proof. + (* Could do a [left] here and be over with it *) + right; simpl; try lia. + right; simpl; try lia. + Fail (right; simpl; try lia). + left. +Qed. + +Goal + exactly (fun x=>x=3) egstr1 2. +Proof. + right; simpl; try lia. + right; simpl; try lia. + left. +Qed. diff --git a/coq/unfinished/calc-ce.v b/coq/unfinished/calc-ce.v new file mode 100644 index 0000000..fcdaaee --- /dev/null +++ b/coq/unfinished/calc-ce.v @@ -0,0 +1,112 @@ +Require Import List Vector. +Import ListNotations. +Import VectorNotations. + +Declare Custom Entry calc. + +Notation "<{ e }>" := (e) (e custom calc at level 99). +Notation "'`' e '`'" := (e) (in custom calc, e constr). + +Inductive type : Type := +| bv : type. + +Definition typeDenote (t : type) : Type := + match t with + | bv => Vector.t bool 8 + end. + +Inductive binop : Type := +| Addn +| Mult. + +Inductive exp : Type := +| Const : Vector.t bool 8 -> exp +| Binop : binop -> exp -> exp -> exp. + +Fixpoint xorn {n m : nat} (a : Vector.t bool n) + (b : Vector.t bool m) : Vector.t bool (max n m) := + match a, b with + | x :: xs, y :: ys => xorb x y :: xorn xs ys + | x :: xs, [] => x :: xs + | [], ys => ys + end. + +From Equations Require Import Equations. +Equations xorn_eq {n m : nat} (a : Vector.t bool n) (b : Vector.t bool m) : Vector.t bool (max n m) := +xorn_eq (x :: a) (y :: b) := xorb x y :: xorn a b ; +xorn_eq [] b := b ; +xorn_eq a [] := a. + + +Fixpoint repeat (n : nat) (val : bool) : Vector.t bool n := + (match n with + | O => [] + | S n' => val :: (repeat n' val) + end)%vector. + +(* +Fixpoint xorn {n m : nat} (a : Vector.t bool n) + (b : Vector.t bool m) : Vector.t bool (max n m) := + (match n, m with + | O, O => [] + | _, O => a + | O, _ => b + | S n', S m' => + match a, b with + | _, _ => repeat (max n m) true + end + end)%vector. + +Fixpoint addn {n m : nat} (a : Vector.t bool n) + (b : Vector.t bool m) : Vector.t bool (max n m) := + (match a, b return (Vector.t bool (max n m)) with + | [], [] => [] + | _, [] => a + | [], _ => b + | x::xs, y::ys => + let nval := + match x, y with + | false, false => false + | true, true => false + | _, _ => true + end + in + nval :: (addn xs ys) + end)%vector. + +(* Bits are from right to left *) +Definition add8 (a b : Vector.t bool 8) : Vector.t bool 8 := + (match a, b with + | nil, _ => nil + | cons x xs, cons y ys => + let nval := + match x, y with + | false, false => false + | true, true => false + | _, _ => true + end + in + cons nval add + end)%vector. + *) + + + +Definition binopDenote (bop : binop) + : Vector.t bool 8 -> Vector.t bool 8 -> Vector.t bool 8 := + match bop with + | Addn => add8 + +Fixpoint expDenote (e : exp) : Vector.t bool 8 := + match e with + | Const x => x + | Binop op e1 e2 => + (binopDenote op) (expDenote e1) (expDenote e2) + end. +3M + + + + + + diff --git a/coq/unfinished/chlipala-oplls.v b/coq/unfinished/chlipala-oplls.v new file mode 100644 index 0000000..a3af3b9 --- /dev/null +++ b/coq/unfinished/chlipala-oplls.v @@ -0,0 +1,74 @@ +Require Import ArithRing. (*Ring*) + +Inductive exp : Set := + | Constant : nat -> exp + | Plus : exp -> exp -> exp + | Times : exp -> exp -> exp. + +Fixpoint eval (e : exp) : nat := + match e with + | Constant n => n + | Plus e1 e2 => (eval e1) + (eval e2) + | Times e1 e2 => (eval e1) * (eval e2) + end. + +Fixpoint commuter (e : exp) : exp := + match e with + | Constant n => e + | Plus e1 e2 => Plus (commuter e2) (commuter e1) + | Times e1 e2 => Times (commuter e2) (commuter e1) + end. + +Compute eval (Plus (Constant 3) (Constant 4)). +Compute eval (commuter (Plus (Constant 3) (Constant 4))). + +Theorem commuter_equiv : forall e : exp, (eval e) = (eval (commuter e)). +Proof. + intros e. + induction e. + - reflexivity. + - simpl. + rewrite <- IHe1, <- IHe2. (* or rewrite in other direction *) + ring. (* based on properties of semi-rings *) + - simpl. + rewrite IHe1, IHe2. + ring. +Qed. + +Theorem commuter_equiv' : forall e : exp, (eval e) = (eval (commuter e)). +Proof. + intros e. + induction e; simpl. + - reflexivity. + - rewrite IHe1, IHe2. + ring. + - rewrite IHe1, IHe2. + ring. +Qed. + +Theorem commuter_equiv'' : forall e : exp, (eval e) = (eval (commuter e)). +(* Example of proof automation. This scales better. + When things like addition of a new constructor happens. *) +Proof. + induction e; simpl; + repeat match goal with + | [ H : _ = _ |- _ ] => rewrite H + end; ring. +Qed. + +(** * Untyped lambda calculus *) +Require Import String. +Inductive term : Set := + | Var : string -> term + | Abs : string -> term -> term + | App : term -> term -> term. + +Check string_dec. +(* string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2} *) + +Definition subst (var : string) (repl t : term) : term := + match t with + | Var x => if string_dec x var then var else t + | Abs x t => if string + | App t1 t2 => App (subst orig repl t1) (subst orig repl t2) + end. diff --git a/coq/unfinished/covariance.v b/coq/unfinished/covariance.v new file mode 100644 index 0000000..566722b --- /dev/null +++ b/coq/unfinished/covariance.v @@ -0,0 +1,13 @@ +(* http://poleiro.info/posts/2019-08-06-contravariance-and-recursion.html *) + +Inductive type : Type := +| Top: type +| Int: type +| Arrow: type -> type -> type. + +Inductive subtype : type -> type -> Type := +| STTop: forall t:type, subtype t Top +| STInt: subtype Int Int +| STArrow: forall t1 t2 s1 s2:type, + subtype s1 t1 -> subtype s2 t2 -> + subtype (Arrow t1 s2) (Arrow s1 t2). diff --git a/coq/unfinished/datetime.v b/coq/unfinished/datetime.v new file mode 100644 index 0000000..3857d42 --- /dev/null +++ b/coq/unfinished/datetime.v @@ -0,0 +1,7 @@ +Inductive Hour : Type := + | hour : Hour. + +Inductive Date : Type := + | date : Date. +Inductive RNat : Type := +| rnat : nat -> nat -> nat -> RNat. (* start, end, value *) diff --git a/coq/unfinished/email.v b/coq/unfinished/email.v new file mode 100644 index 0000000..5992d2b --- /dev/null +++ b/coq/unfinished/email.v @@ -0,0 +1,37 @@ +Require Import String. + +Inductive email : Set := +| Email: forall (username domain tld:string), email. + +Goal + email. +Proof. + eapply Email. + - exact "famubu"%string. + - exact "rawtext"%string. + - exact "club"%string. +Qed. + + + +Reset email. + + +(* https://en.wikipedia.org/wiki/Email_address#Local-part *) +Definition username := string. +Definition domain := string. + +(* https://en.wikipedia.org/wiki/List_of_Internet_top-level_domains *) +Definition tld := string. + +Inductive email : Set := +| Email (user:username) (dom: domain) (t:tld) : email. + +Goal + email. +Proof. + eapply Email. + - exact "famubu"%string. + - exact "rawtext"%string. + - exact "club"%string. +Qed. diff --git a/coq/unfinished/hanoi.v b/coq/unfinished/hanoi.v new file mode 100644 index 0000000..dedf59a --- /dev/null +++ b/coq/unfinished/hanoi.v @@ -0,0 +1,127 @@ +Require Import List. +Import ListNotations. + +Fixpoint hanoi (n:nat) (start via final:nat) : list (nat*nat) := + match n with + | O => [] + | S n' => (hanoi n' start final via) ++ [(start, final)] ++ + (hanoi n' via final start) + end. +Compute hanoi 3 0 1 2. +(* = [(0, 2); (0, 1); (2, 0); (0, 2); (1, 2); (1, 0); (2, 1)] + : list (nat * nat) *) +Compute hanoi 4 0 1 2. +Compute length (hanoi 5 0 1 2). (* 31 : nat *) + + + +(************************************************************************) + +(* 2ⁿ - 1 *) + +(* N=3 => 7 moves +[[3,2,1], [], []] +[[3,2], [], [1]] +[[3], [2], [1]] +[[3], [2,1], []] +[[], [2,1], [3]] +[[1], [2], [3]] +[[1], [], [3,2]] +[[], [], [3,2,1]] + *) + + +(* N=4 => 15 moves +[[4,3,2,1], [], []] +[[4,3,2], [1], []] +[[4,3], [1], [2]] +[[4,3], [], [2,1]] +[[4], [3], [2,1]] +[[4,1], [3], [2]] +[[4,1], [3,2], []] +[[4], [3,2,1], []] +[[], [3,2,1], [4]] +[[], [3,2], [4,1]] +[[2], [3], [4,1]] +[[2,1], [3], [4]] +[[2,1], [], [4,3]] +[[2], [1], [4,3]] +[[], [1], [4,3,2]] +[[], [], [4,3,2,1]] + *) + +Require Import List. +Import ListNotations. + +(* +Inductive moves : list (list nat) -> Set := +| A2B : forall (a b:nat) (aa bs cs:list nat), + a < b -> moves [a::aa; b::bs; cs] -> moves [aa; a::b::bs; cs] +| A2C : forall (a c:nat) (aa bs cs:list nat), + a < c -> moves [a::aa; bs; c::cs] -> moves [aa; bs; a::c::cs] +| B2A : forall (a b:nat) (aa bs cs:list nat), + b < a -> moves [a::aa; b::bs; cs] -> moves [b::a::aa; bs; cs] +| B2C : forall (b c:nat) (aa bs cs:list nat), + b < c -> moves [aa; b::bs; c::cs] -> moves [aa; bs; b::c::cs] +| C2A : forall (a c:nat) (aa bs cs:list nat), + c < a -> moves [a::aa; bs; c::cs] -> moves [c::a::aa; bs; cs] +| C2B : forall (b c:nat) (aa bs cs:list nat), + c < b -> moves [aa; b::bs; c::cs] -> moves [aa; c::b::bs; cs]. +*) + +(* +| A2BNil : forall (a:nat) (aa cc:list nat), + moves [a::aa; []; cc] + -> moves [aa; [List.last (a::aa) a]; cc] +*) + +Compute ( + match [1;2;3;4] with + | h::aa::x::nil => x + | _ => 0 + end). + +Check List.last. +Inductive moves : list (list nat) -> Set := +| A2BNil : forall (a:nat) (aa cc:list nat), + moves [a::aa::nil; []; cc] + -> moves [aa; [List.last (a::aa) a]; cc] +| A2CNil : forall (a:nat) (aa bb:list nat), + moves [a::aa; bb; []] -> moves [aa; bb; [a]] +| B2ANil : forall (b:nat) (bb cc:list nat), + moves [[]; b::bb; cc] -> moves [[b]; bb; cc] +| B2CNil : forall (b:nat) (aa bb:list nat), + moves [aa; b::bb; []] -> moves [aa; bb; [b]] +| C2ANil : forall (c:nat) (bb cc:list nat), + moves [[]; bb; c::cc] -> moves [[c]; bb; cc] +| C2BNil : forall (c:nat) (aa cc:list nat), + moves [aa; []; c::cc] -> moves [aa; [c]; cc] +| A2B : forall (a b:nat) (aa bb cc:list nat), + a < b -> moves [a::aa; b::bb; cc] -> moves [aa; a::b::bb; cc] +| A2C : forall (a c:nat) (aa bb cc:list nat), + a < c -> moves [a::aa; bb; c::cc] -> moves [aa; bb; a::c::cc] +| B2A : forall (a b:nat) (aa bb cc:list nat), + b < a -> moves [a::aa; b::bb; cc] -> moves [b::a::aa; bb; cc] +| B2C : forall (b c:nat) (aa bb cc:list nat), + b < c -> moves [aa; b::bb; c::cc] -> moves [aa; bb; b::c::cc] +| C2A : forall (a c:nat) (aa bb cc:list nat), + c < a -> moves [a::aa; bb; c::cc] -> moves [c::a::aa; bb; cc] +| C2B : forall (b c:nat) (aa bb cc:list nat), + c < b -> moves [aa; b::bb; c::cc] -> moves [aa; c::b::bb; cc]. + + + +Lemma foo : moves [[3;2;1];[];[]] -> moves [[];[];[3;2;1]]. +Proof. + intro H. + Check A2BNil. + Check A2BNil 3 _ _ H. + Compute A2BNil 3 _ _ H. + apply (A2BNil 3 _ _ H). + apply (A2B H). + moves [[3;2;1];[];[]]. +Qed. + + +Check moves [[];[];[]]. +Require Import Permutation. diff --git a/coq/unfinished/kmt.v b/coq/unfinished/kmt.v new file mode 100644 index 0000000..95a76c8 --- /dev/null +++ b/coq/unfinished/kmt.v @@ -0,0 +1,24 @@ +Print Nat.add. + +Fixpoint add (n m:nat):nat := + match n with + | 0 => m + | S n' => S (add n' m) + end. +Print add. + +(* Nat *) +Inductive op (V:Type) : Type := +| Abs: (V -> nat) -> op V +| Var: V -> op V +| Inc: -> op V +| Assign: op -> op V +| Gt: (V -> nat) -> op V. +Arguments Abs {V}. +Arguments Var {V}. +Arguments Gt {V}. +Arguments Inc {V}. +Arguments Assign {V}. + + +Check Gt (fun x => 3). diff --git a/coq/unfinished/phoas-stlc2cps.v b/coq/unfinished/phoas-stlc2cps.v new file mode 100644 index 0000000..72155f1 --- /dev/null +++ b/coq/unfinished/phoas-stlc2cps.v @@ -0,0 +1,112 @@ +(* +Source language: STLC +Target language: CPS +*) + +Module Stlc. + (* Source language *) + Inductive type : Set := + | Bool: type + | Arrow: type -> type -> type. + + (* V is type family of variables *) + Inductive term (V:type->Type): type -> Type := + | Tru: term V Bool + | Fls: term V Bool + | Var: forall t:type, + V t -> term V t + | App: forall t1 t2:type, + term V (Arrow t1 t2) -> term V t1 -> term V t2 + | Abs: forall t1 t2:type, + (V t1 -> term V t2) -> term V (Arrow t1 t2). + + Arguments Tru {V}. + Arguments Fls {V}. + Arguments Var {V t}. + Arguments App {V t1 t2}. + Arguments Abs {V t1 t2}. + + Definition Term (t:type) (V:type -> Type) := term V t. +End Stlc. + + +Module Cps. + + (* Target language *) + Inductive type : Set := + | Bool: type + | Cont: type -> type + | Prod: type -> type -> type. + + Inductive term (V:type -> Type) : type -> Type := + | Halt: forall t:type, (* Done. No more continuation *) + V t -> term V t + | App: forall t, + V (Cont t) -> V t -> term V t + | LetBind: forall (t:type), + primop V t + -> (V t -> term V t) + -> term V t + with primop (V:type -> Type) : type -> Type := + | Tru: primop V Bool + | Fls: primop V Bool + | Var: forall t:type, + V t -> primop V t + | Abs: forall t1 t2:type, + (V t1 -> term V t2) -> primop V (Cont t2) + | Pair: forall t1 t2:type, + V t1 -> V t2 -> primop V (Prod t1 t2) + | Fst: forall t1 t2:type, + V (Prod t1 t2) -> primop V t1 + | Snd: forall t1 t2:type, + V (Prod t1 t2) -> primop V t2. + + Arguments Halt {V t}. + Arguments App {V t}. + Arguments LetBind {V t}. + + Arguments Tru {V}. + Arguments Fls {V}. + Arguments Var {V t}. + Arguments Abs {V t1 t2}. + Arguments Pair {V t1 t2}. + Arguments Fst {V t1 t2}. + Arguments Snd {V t1 t2}. +End Cps. + + +Import Stlc. +Import Cps. + +Fixpoint stlcToCpsType (t: Stlc.type) : Cps.type := + match t with + | Stlc.Bool => Cps.Bool + | Stlc.Arrow t1 t2 => + let t1' := (stlcToCpsType t1) in + let t2' := (stlcToCpsType t2) in + Cps.Cont (Cps.Prod t1' (Cps.Cont t2')) + end. + +(* Convert Stlc terms to equivalent Cps terms *) +Fixpoint stlcToCps {sV: Stlc.type -> Type} {cV: Cps.type -> Type} + {sT: Stlc.type} {cT: Cps.type} (t: Stlc.term sV sT) + : Cps.term cV cT := + match t with + | Stlc.Tru => LetBind Cps.Tru Cps.Halt + | Stlc.Fls => LetBind Cps.Tru Cps.Halt + | Stlc.Var v => LetBind Cps.Tru Cps.Halt + | Stlc.App f e => LetBind Cps.Tru Cps.Halt + | Stlc.Abs f => LetBind Cps.Tru Cps.Halt + end. + + + + + match t with + | Halt v => + | App f v => + | LetBind op f => + end. + + + diff --git a/coq/unfinished/regex-harper.v b/coq/unfinished/regex-harper.v new file mode 100644 index 0000000..f5b67af --- /dev/null +++ b/coq/unfinished/regex-harper.v @@ -0,0 +1,57 @@ +Require Import List. +Import ListNotations. + +CoInductive b3 : Type := Ctrue | Cfalse | Dunno. + +Inductive re (A:Type) : Type := +| Char: (A->b3) -> re A +| Cat: re A -> re A -> re A +| Alt: re A -> re A -> re A +| Star: re A -> re A. +Arguments Char {A}. +Arguments Cat {A}. +Arguments Alt {A}. +Arguments Star {A}. + + +CoFixpoint acc {A:Type} (old:b3) (r:re A) + (l:list A) (k:list A -> b3) : b3 := + match old with + | Ctrue => Ctrue + | Cfalse => Cfalse + | _ => + match r with + | Char f => + match l with + | [] => Cfalse + | x::xs => + match f x with + | Ctrue => k xs + | _ => Cfalse + end + end + | Cat r1 r2 => acc old r1 l (fun xs => acc old r2 xs k) + | Alt r1 r2 => Ctrue + | Star r1 => Ctrue + end + end. + + +Fixpoint acc {A:Type} (r:re A) (l:list A) (k:list A -> bool) + : bool := + match r,l with + | Char _, [] => false + | Char f, x::xs => + if f x then k xs + else false + | Cat r1 r2, _ => acc r1 l (fun xs => acc r2 xs k) + | Alt r1 r2, _ => + let rv1 := acc r1 l k in + let rv2 := acc r2 l k in + orb rv1 rv2 + | Star r1, _ => + let rv1 := k l in + let rv2 := acc (Star r1) l k in + orb rv1 rv2 + end. + diff --git a/coq/unfinished/regex.v b/coq/unfinished/regex.v new file mode 100644 index 0000000..439bea1 --- /dev/null +++ b/coq/unfinished/regex.v @@ -0,0 +1,120 @@ +Require Import String. +Open Scope string. +Declare Scope re_scope. +Delimit Scope re_scope with re. +(* dot, plus, question mark, ranges of repetitions, ^, $ *) +Definition char := string. +Inductive re : Type := +| Atom : char -> re +(*| Star : re -> re*) +| Concat : re -> re -> re +| Alt : re -> re -> re +| Epsilon : re +| Dot : re. +(* +Definition Plus (a:re) : re := Alt a Epsilon. +Definition Optional (a:re) : re := Concat a a. +Fixpoint exactly_n (n:nat) (a:re) : re := + match n with + | O => Epsilon + | S n' => Concat a (exactly_n n' a) + end. +Definition atleast_n (n:nat) (a:re) : re := + Concat (exactly_n n a) (Star a). +Fixpoint atmost_n (n:nat) (a:re) : re := + match n with + | O => Epsilon + | S n' => Alt (atmost_n n' a) (exactly_n n a) + end. + +Definition exactly_ij (start stop:nat) (a:re) : re := + Concat (exactly_n start a) (atmost_n (stop-start-1) a). + +Infix ";" := Concat (at level 50) : re_scope. +Infix "│" := Alt (at level 50) : re_scope. +Notation "'۰'" := Dot (at level 30) : re_scope. +Notation "'ε'" := Epsilon (at level 30) : re_scope. +Notation " a '𐊛'" := (Plus a) (at level 50) : re_scope. +Notation " a '٭'" := (Star a) (at level 50) : re_scope. + +Notation " '❴' count '❵' a " := (exactly_n count a) + (at level 80, count at next level) : signal_scope. +Notation " a '❴' count '❵' " := (exactly_n count a) + (at level 80, count at next level) : signal_scope. +Notation " a '❨' ':' stop '❩' " := (atmost_n stop a) + (at level 80) : signal_scope. +Notation " a '❲' start ':' stop '❳' " := + (exactly_ij start stop a) + (at level 80, start at next level) : signal_scope. + +Check (Dot │ ε)%re. +Fail Check (Dot❴2❵)%re. +Fail Check (❴2❵ Dot)%re. +*) + +(* Indexing starts from zero. Empty string on invalid index. *) +Definition stridx (i:nat) (s:string) : char := + String.substring i 1 s. +Definition strdrop (n:nat) (s:string) : string := + String.substring n ((String.length s)-1) s. +Search (nat -> string -> string). + +Fixpoint reDenote (r:re) : string -> Prop := + match r with + | Atom ch => fun s:string => stridx 0 s = ch + | Epsilon => fun s:string => True (* TODO *) + | Dot => fun s:string => stridx 0 s = stridx 0 s + | Concat r1 r2 => fun s:string => + ((reDenote r1) s) /\ ((reDenote r2) (strdrop 1 s)) + | Alt r1 r2 => fun s:string => + ((reDenote r1) s) \/ ((reDenote r2) s) + end. +Compute (reDenote (Alt (Atom "a") (Atom "b"))) "a". + +(* +Infix ":-" := (Concat) (at level 50) : re_scope. +Infix "‖" := (Alt) (at level 51) : re_scope. (* and has less precedence *) +Compute ((Atom "a") :- (Atom "b"))%re. +Compute ((Atom "h") :- (Atom "e") :- (Atom "l"))%re. +*) +Compute + (reDenote (Concat (Concat (Concat (Concat (Atom "h") (Atom "e")) Dot) Dot) (Atom "o"))) "hello". + + +Goal + (reDenote (Alt (Atom "a") (Atom "b"))) "a". +Proof. + simpl. + unfold stridx. + simpl. + auto. +Qed. + +Goal + (reDenote (Concat (Atom "a") (Atom "b"))) "ab". +Proof. + simpl. + unfold stridx. + simpl. + auto. +Qed. + + +Goal + (reDenote (Concat (Concat (Concat (Concat (Atom "h") (Atom "e")) Dot) Dot) (Atom "o"))) "hello". +Proof. + simpl. + split. + split. + split. + split. + unfold stridx. + now simpl. + unfold strdrop. + unfold stridx. + now simpl. + now simpl. + now simpl. + unfold strdrop. + unfold stridx. + simpl. diff --git a/coq/unfinished/subtypes.v b/coq/unfinished/subtypes.v new file mode 100644 index 0000000..c34db4f --- /dev/null +++ b/coq/unfinished/subtypes.v @@ -0,0 +1,168 @@ +(* http://poleiro.info/posts/2019-08-06-contravariance-and-recursion.html *) +Require Import Lia. + +Inductive type : Type := +| Top: type +| Int: type +| Arrow: type -> type -> type. + +Inductive subtype : type -> type -> Type := +| STop: forall t:type, subtype t Top +| SIdty: forall t:type, subtype t t +| SArrow: forall s1 t1 s2 t2:type, + subtype s1 t1 -> subtype s2 t2 -> + subtype (Arrow s2 t1) (Arrow s1 t2). + +Fail Fixpoint isSubType (a b:type): bool := + match a, b with + | _, Top => true + | Top, _ => false + | Int, Int => true + | Arrow a1 b1, Arrow a2 b2 => + andb (isSubType b1 b2) (isSubType a2 a1) + | _, _ => false + end. + +Fixpoint isSubType (flag:bool) (a b:type): bool := + match a, b with + | _, Top => true + | Top, _ => false + | Int, Int => true + | Arrow a1 b1, Arrow a2 b2 => + andb (isSubType flag b1 b2) (isSubType (negb flag) a2 a1) + | _, _ => false + end. + + +Fixpoint psum (t:type) : nat := + match t with + | Arrow s t' => (psum s) + (psum t') + | _ => 1 + end. +Definition structFn (s t:type) : nat := (psum s) + (psum t). +Compute psum (Arrow (Arrow Int Int) (Arrow Int Int)). +Definition structFn' (st:type*type) : nat := + (psum (fst st)) + (psum (snd st)). +Compute psum (Arrow (Arrow Int Int) (Arrow Int Int)). + +Require Import FunInd. +Require Import Arith. +Require Import Program.Wf. +(* Error: The reference Arith.Wf_nat.ltof was not found in the current environment. *) + +Require Import Recdef. + +Program Fixpoint isSubtype (s t:type) + {measure( psum (Arrow s t))}: bool := + match s, t with + | _, Top => true + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1) (isSubtype t1 t2) + | _, _ => false + end. +Next Obligation. + simpl. + lia. + (* rewrite (Nat.add_comm (psum s2) (psum t2)). *) + (* Check Nat.add_assoc. *) + (* rewrite (Nat.add_assoc (psum s2) (psum t2)). *) + +Function isSubtype (s t:type) {measure psum (Arrow s t)}: bool := + match s, t with + | _, Top => true + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1) (isSubtype t1 t2) + | _, _ => false + end. + +Function isSubtype (s t:type) {measure structFn' (s,t)}: bool := + match s, t with + | _, Top => true + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1) (isSubtype t1 t2) + | _, _ => false + end. +Program Fixpoint isSubtype (s t:type) {measure psum}: bool := + match s, t with + | _, Top => true + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1) (isSubtype t1 t2) + | _, _ => false + end. + +Function isSubtype (s t:type) {measure structFn' (s,t)} : bool := + match s, t with + | _, Top => true + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1) (isSubtype t1 t2) + | _, _ => false + end. + +Fixpoint isSubtype (s t:type) (flag:bool) {struct flag} : bool := + match s, t with + | Top, Top => true + | Top, _ => negb (negb flag) + | _, Top => flag + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1 flag) (isSubtype t1 t2 (negb flag)) + | _, _ => false + end. + + +Fail Fixpoint isSubtype (s t:type) {struct s} : bool := + match s, t with + | _, Top => true + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1) (isSubtype t1 t2) + | _, _ => false + end. +(* The command has indeed failed with message: *) +(* Recursive definition of isSubtype is ill-formed. *) +(* In environment *) +(* isSubtype : type -> type -> bool *) +(* s : type *) +(* t : type *) +(* s1 : type *) +(* t1 : type *) +(* s2 : type *) +(* t2 : type *) +(* Recursive call to isSubtype has principal argument equal to *) +(* "s2" instead of one of the following variables: *) +(* "s1" "t1". *) +(* Recursive definition is: *) +(* "fun s t : type => *) +(* match s with *) +(* | Top => match t with *) +(* | Top => true *) +(* | _ => false *) +(* end *) +(* | Int => match t with *) +(* | Arrow _ _ => false *) +(* | _ => true *) +(* end *) +(* | Arrow s1 t1 => *) +(* match t with *) +(* | Top => true *) +(* | Int => false *) +(* | Arrow s2 t2 => *) +(* (isSubtype s2 s1 && isSubtype t1 t2)%bool *) +(* end *) +(* end". *) + + +Fail Fixpoint isSubtype (s t:type): bool := + match s, t with + | _, Top => true + | Int, Int => true + | Arrow s1 t1, Arrow s2 t2 => + andb (isSubtype s2 s1) (isSubtype t1 t2) + | _, _ => false + end. +(* Error: Cannot guess decreasing argument of fix. *) diff --git a/coq/unfinished/water-jars.v b/coq/unfinished/water-jars.v new file mode 100644 index 0000000..5f3f4bc --- /dev/null +++ b/coq/unfinished/water-jars.v @@ -0,0 +1,11 @@ +Inductive jar (capacity:nat) : nat -> Set := +| Jar : forall n:nat, n <= capacity -> jar capacity n. +(* Show me that n<=capacity then I'll give you a jar *) + +(* +Inductive system (S B:nat) : Set := +| System : forall s b:nat, s<=S /\ b<=B -> jar S s * jar B b -> system S B. +*) + +Inductive moves (sys: system 9 5) : system 9 5 : Set := +| S2B : System 9 5 _ (Jar diff --git a/coq/unique-list.v b/coq/unique-list.v new file mode 100644 index 0000000..766e330 --- /dev/null +++ b/coq/unique-list.v @@ -0,0 +1,19 @@ +(* List with unique elements. Sort of a set, basically. *) +Inductive ulist {A:Type} : list A -> Prop := +| unil : ulist nil +| ucons : forall (a:A) (l:list A), + ~(In a l) -> + ulist l -> ulist (a::l). + +Theorem egulist : ulist [1;2]. +Proof. + constructor. + - simpl. + intro H. + destruct H; congruence. + - constructor. + + simpl. + intro H. + assumption. + + constructor. +Qed. diff --git a/coq/vector_nth.v b/coq/vector_nth.v new file mode 100644 index 0000000..86ba53d --- /dev/null +++ b/coq/vector_nth.v @@ -0,0 +1,84 @@ +Require Import Vector Bvector. +Import BvectorNotations. +Import VectorNotations. + +Check [true;false;false]%Bvector. +Example foo := [true]%Bvector. + +Check cons nat 3. +Fixpoint cust_nth {A:Type} {n:nat} + (v:Vector.t A n) (i:nat) : option A := + if (Nat.eqb (n-1) i) then + match v with + | Vector.nil _ => None + | Vector.cons _ x n' vs => Some x + end + else + match v with + | Vector.nil _ => None + | Vector.cons _ _ _ vs => cust_nth vs i + end. +Compute cust_nth [true; false; true]%Bvector 0. +Compute cust_nth [true; false; true]%Bvector 1. +Compute cust_nth [true; false; true]%Bvector 2. + +Compute cust_nth [3; 2; 1]%vector 0. +Compute cust_nth [3; 2; 1]%vector 1. +Compute cust_nth [3; 2; 1]%vector 2. + +(* bool/bit to nat *) +Definition b2n (b:bool) : nat := + match b with + | true => 1 + | false => 0 + end. + +(* bool vector to nat *) +Fixpoint bvec2n {n:nat} (v:Vector.t bool n) : nat := + match v with + | Vector.nil _ => 0 + | Vector.cons _ x n' vs => + match x with + | true => (Nat.pow 2 n') + (bvec2n vs) + | false => (bvec2n vs) + end + end. +Compute bvec2n [true; false; true]%Bvector. + +(* bool vector to nat *) +Fixpoint bvec2n {n:nat} (v:Vector.t bool n) : nat := + match v with + | Vector.nil _ => 0 + | Vector.cons _ x n' vs => + match x with + | true => (Nat.pow 2 n') + (bvec2n vs) + | false => (bvec2n vs) + end + end. + +(* nat to bool/bit *) +Definition n2b (n:nat) : bool := + match n with + | O => false + | _ => true + end. + +Definition modulob (a b:nat): bool:= + match (Nat.modulo a b) with + | O => true + | _ => false + end. + +(* nat to bool vector *) +Fixpoint n2bvec (n z:nat) : Bvector z := + match z with + | O => []%vector + | S z' => + let e2n := Nat.pow 2 z' in + if Nat.leb e2n n then + Vector.cons _ true z' (n2bvec (n - e2n) z') + else + Vector.cons _ false z' (n2bvec n z') + end. +Compute n2bvec 6 3. + diff --git a/cpp/optional-fopen.cpp b/cpp/optional-fopen.cpp new file mode 100644 index 0000000..c0e792e --- /dev/null +++ b/cpp/optional-fopen.cpp @@ -0,0 +1,38 @@ +// https://en.cppreference.com/w/cpp/utility/optional + +#include +#include + +std::optional ffopen(char const* fname) +{ + FILE *fin = fopen(fname, "r"); + if(fin==NULL) + { + return {}; + } + return fin; +} + +int main() +{ + std::optional rv = ffopen("/home/famubu/hi.txt"); + char str[30]; + if (rv.has_value()) + { + fgets(str, 29, rv.value()); + puts(str); + printf("YES\n"); + } + else + { + printf("NO\n"); + } +} + +/* +$ g++ optional.cpp --std=c++17 -o a.out +$ ./a.out +0 +100 + */ + diff --git a/cpp/optional.cpp b/cpp/optional.cpp new file mode 100644 index 0000000..3e53adf --- /dev/null +++ b/cpp/optional.cpp @@ -0,0 +1,41 @@ +// https://en.cppreference.com/w/cpp/utility/optional + +#include +#include + +std::optional pred(bool cond) +{ + if(cond) + { + return 100; + } + return {}; +} + +int main() +{ + // value_or + std::cout << pred(false).value_or(0) << "\n"; + std::cout << pred(true).value_or(0) << "\n"; + + // value + /* + std::cout << pred(false).value() << "\n"; +terminate called after throwing an instance of 'std::bad_optional_access' + what(): bad optional access +Aborted (core dumped) + */ + std::cout << pred(true).value() << "\n"; + + // has_value + std::cout << pred(false).has_value() << "\n"; // 0 + std::cout << pred(true).has_value() << "\n"; // 1 + +} + +/* +$ g++ optional.cpp --std=c++17 -o a.out +$ ./a.out +0 +100 + */ diff --git a/elisp/README.org b/elisp/README.org new file mode 100644 index 0000000..97b309c --- /dev/null +++ b/elisp/README.org @@ -0,0 +1,3 @@ +#+TITLE: elisp + + - [[./matrix-gen.el][matrix-gen.el]]: A snippet to draw outline of a matrix diff --git a/elisp/matrix-gen.el b/elisp/matrix-gen.el new file mode 100644 index 0000000..048c022 --- /dev/null +++ b/elisp/matrix-gen.el @@ -0,0 +1,93 @@ +(defun matrgen (rows cols) + "Generate 2D matrix pattern with `rows' rows and `cols' columns" + (interactive "nRows:\nnCols:") + (when (and (> rows 0) (> cols 0)) + (if (= rows 1) + ; If there's only one row, just use square brackets + ; Eg: [1,2,3,4] + (progn + (insert "[ ") + (dotimes (c cols) + (insert "_ ")) + (insert " ]\n")) + + (progn + ; Draw top part + (insert "⎡ ") + (dotimes (c cols) + (insert "_ ")) + (insert " ⎤\n") + + ; Draw middle part + (dotimes (r (- rows 2)) + (insert "⎢ ") + (dotimes (c cols) + (insert "_ ")) + (insert " ⎥\n")) + + ; Draw bottom part + (insert "⎣ ") + (dotimes (c cols) + (insert "_ ")) + (insert " ⎦\n"))))) + + + +; (defun matrgen (rows cols) +; (interactive "nRows:\nnCols:") +; (when (> rows 0) +; (if (= rows 1) +; (progn +; (insert "[ ") +; (dotimes (c cols) +; (insert "_ ")) +; (insert " ]\n")) +; +; (progn +; (insert "⎡ ") +; (dotimes (c cols) +; (insert "_ ")) +; (insert " ⎤\n") +; +; (dotimes (r (- rows 2)) +; (insert "⎢ ") +; (dotimes (c cols) +; (insert "_ ")) +; (insert " ⎥\n")) +; +; (insert "⎣ ") +; (dotimes (c cols) +; (insert "_ ")) +; (insert " ⎦\n"))))) + + + + + + +; (dotimes (r (- rows 2)) +; (insert "⎢ ") +; (dotimes (c cols) +; (insert "_ ")) +; (insert "⎥\n"))) + + +; (defun matrgen (rows cols) +; (interactive "nRows:\nnCols:") +; (dotimes (i rows) +; (insert "⎢ ") +; (dotimes (i cols) +; (insert "_ ")) +; (insert "⎥\n"))) + + + ;(insert (format "%d %d" rows cols)))) + + + + ;(message "%s %s" (number-to-string rows) (number-to-string cols))) + + ;(insert "hi " (number-to-string rows) ".")) + + ;(insert "hi " string ".")) + ;(insert "\\label{" string "} \\index{\\nameref{" string "}}")) diff --git a/latex/expl3-hello.tex b/latex/expl3-hello.tex new file mode 100644 index 0000000..0e4e0cb --- /dev/null +++ b/latex/expl3-hello.tex @@ -0,0 +1,17 @@ +\documentclass{article} +\usepackage{xparse} % from expl3 +%\RequirePackage{expl3} +\ExplSyntaxOn + +\NewDocumentCommand{\DeclareListOfValues}{ m m } +{ + \clist_gclear_new:c {g_list_of_values_#1_clist} + \clist_gset:cn {g_list_of_values_#1_clist} {#2} +} + + + + +\begin{document} +3 +\end{document} diff --git a/latex/listings-define-lang.tex b/latex/listings-define-lang.tex new file mode 100644 index 0000000..5256475 --- /dev/null +++ b/latex/listings-define-lang.tex @@ -0,0 +1,33 @@ +\documentclass{article} +\usepackage{xcolor} +\usepackage{listings} +\usepackage{fontspec} +\setmonofont{DejaVu Sans Mono} + + +\begin{document} +\lstdefinelanguage{psl}{ + keywords={% + abort, never, until, until!, before + }, + otherkeywords={% operators + %:, ->, |->, |=>, ;, <, >, <=, >=, ==, != + }, + morekeywords={% + G, F, U, R, M, W + }, + keywordstyle=\color{green}, + numberstyle=\scriptsize, + sensitive=true, % keywords are case-sensitive + morecomment=[l]{//}, % l is for line comment + morecomment=[s]{/*}{*/}, % s is for start and end delimiter + morestring=[b]" % defines that strings are enclosed in double quotes +} + +\begin{lstlisting}{psl} +G a b +□ a b +a abort b +"a b c" +\end{lstlisting} +\end{document} diff --git a/latex/tikz-automata.tex b/latex/tikz-automata.tex new file mode 100644 index 0000000..ae12873 --- /dev/null +++ b/latex/tikz-automata.tex @@ -0,0 +1,24 @@ +\documentclass{standalone} +\usepackage{tikz} + +\usetikzlibrary{automata,arrows,positioning} +\usetikzlibrary{arrows.meta,chains,shapes.geometric} +\usetikzlibrary{decorations.pathreplacing} + +\begin{document} + +\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,auto] + \node[state,initial] (q_a) {$q_a$}; + \node[state,accepting] (q_b) [right=of q_a] {$q_b$}; + \path[->] + (q_a) edge [loop above] node {a} () + + (q_0) edge node {0} (q_1) + edge node [swap] {1} (q_2) + (q_1) edge node {1} (q_3) + edge [loop above] node {0} () + (q_2) edge node [swap] {0} (q_3) + edge [loop below] node {1} (); +\end{tikzpicture} + +\end{document} diff --git a/metapost/dots-lines.mp b/metapost/dots-lines.mp new file mode 100644 index 0000000..02b5e6d --- /dev/null +++ b/metapost/dots-lines.mp @@ -0,0 +1,10 @@ +prologues := 3; + +beginfig(1) +drawdot(0,30); +draw (0,0) -- (3,4); +draw (0,5) -- (3,4); +draw (0,5) -- (5,5); +endfig; + +end diff --git a/metapost/hello.mp b/metapost/hello.mp new file mode 100644 index 0000000..6d37744 --- /dev/null +++ b/metapost/hello.mp @@ -0,0 +1,19 @@ +prologues := 3; + +% `mpost filename.mp` produces encapsulated EPS. +% Convert to pdf with `mptopdf -raw hello.mp` + +beginfig(3) +pair a,b; +path p; +pen mypen; +a = (0,0); +b = (3,4); +p = a--b; +mypen = pencircle scaled 1; +pickup mypen; +draw p; + +endfig; + +end diff --git a/misc/uclid5-hello.ucl b/misc/uclid5-hello.ucl new file mode 100644 index 0000000..5986bb3 --- /dev/null +++ b/misc/uclid5-hello.ucl @@ -0,0 +1,31 @@ +module main { + var a, b : integer; + init { + a = 0; + b = 1; + } + next { + a', b' = b, a+b; + } + + // Part 2: System specification + invariant a_le_b: a <= b; + + // Part 3: Proof script + control { + // original uclid was like SRI's sat tool + //bmc(3); // do bounded model checking for 3 steps + //induction; + vobj = induction(1); // do induction for one step + + check; // call smt solver + print_results; + + vobj.print_cex(a, b); // print counterexample on failure + } +} + +// uclid name.ucl +// uclid name.ucl (failed ∵ invariant not powerful enough) + +// uclid name.ucl -m Sys // check Sys module instead of main module diff --git a/ocaml/stlc.ml b/ocaml/stlc.ml new file mode 100644 index 0000000..0878e2d --- /dev/null +++ b/ocaml/stlc.ml @@ -0,0 +1,57 @@ +(* +https://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/ +https://web.archive.org/web/20210423155718/https://www.cis.upenn.edu/~bcpierce/tapl/checkers/ +*) + +(* ** Compilation + +ocamlc in.sml -o out.out +*) + +type info = FI of string * int * int | UNKNOWN +type binding = NameBind +type context = (string * binding) list + +let rec isnamebound ctx x = + match ctx with + [] -> false + | (y,_)::rest -> + if y=x then true + else isnamebound rest x + +let rec pickfreshname ctx x = + if isnamebound ctx x then pickfreshname ctx (x^"'") + else ((x,NameBind)::ctx), x + + + +(* Bare bones definition of [term] + +type term = Var of int (* de-Bruijn index *) + | Abs of term + | App of term * term + +But we are using some annotations to make debugging easier. + + - info: File position where term was found, so errors can point out where the error occurred. + - int: For [Var] nodes. Total length of the context in which the variable is occuring. For a consistency check. + - string: For [Abs] nodes. To replace de-Bruijn index with a variable name similar to what was used by user. +*) + +type term = Var of info * int * int + | Abs of info * term * string + | App of info * term * term + + +(* Recursive function to print terms *) +let rec printTerm ctxt t = match t with + Abs(inf, trm, strng) -> + let (ctx', trm') = pickfreshname ctx x + in + print_string "(lambda "; + (* ... *) + | App(inf, t1, t2) -> + + +(* print_string "Hello world!" *) + diff --git a/racket/chess.rkt b/racket/chess.rkt new file mode 100644 index 0000000..67127d6 --- /dev/null +++ b/racket/chess.rkt @@ -0,0 +1,107 @@ +#lang slideshow + +; From ppk's talk + +;; Zebra crossing + +; Building blocks. Too lazy to define over and over again. :-) +(define black-bar + (filled-rectangle 20 100)) +(define white-bar + (colorize black-bar "white")) + +; Seeing some patterns. +(define z1 + (hc-append white-bar black-bar)) +(define z2 + (hc-append z1 z1)) +(define z3 + (hc-append z1 z2)) +(define z4 + (hc-append z1 z3)) + +; Ah.. so that's how it works! +(define (zebra n) + (if (<= n 1) z1 + (hc-append z1 (zebra (- n 1))))) + +;; Chess board + +; Building blocks +(define black-cell + (filled-rectangle 20 20)) +(define white-cell + (colorize black-cell "white")) + +; Experimenting +(define b1 + (vc-append + (hc-append white-cell black-cell) + (hc-append black-cell white-cell))) + +(define b2 + (vc-append + (hc-append b1 b1) + (hc-append b1 b1))) + +(define b3 + (vc-append + (hc-append b2 b2) + (hc-append b2 b2))) + +; General version +(define (board n) + (if (<= n 1) b1 + (vc-append + (hc-append (board (- n 1)) (board (- n 1))) + (hc-append (board (- n 1)) (board (- n 1)))))) + + +;; Sierpinski carpet +(define (square n) + (rectangle n n)) + +(define (filled-square n) + (filled-rectangle n n)) + +(define (black-sq z) (filled-square 20)) +(define (white-sq z) + (colorize (black-sq z) "white")) + + +;(define (sierpinski n z) +; (if (<= n 1) +; (white-sq z) +; (vc-append +; (black-sq z)))) + + +(define (sierpinski n z) + (if (<= n 1) + (white-sq z) + (let ([sub-patt (sierpinski (- n 1) (quotient z 3))]) + (vc-append + (hc-append sub-patt sub-patt sub-patt) + (hc-append sub-patt (square z) sub-patt) + (hc-append sub-patt sub-patt sub-patt))))) + +(define (sq side) + (colorize (filled-rectangle side side) "white")) + +(define (foo side lvl) + (if (not (= (remainder side 3) 0)) (blank 0) + (if (<= lvl 1) + (sq side) + (let* + ([sub-side (quotient side 3)] + [sub-patt (foo sub-side (- lvl 1))] + [removed (rectangle sub-side sub-side)]) + (vc-append + (hc-append sub-patt sub-patt sub-patt) + (hc-append sub-patt removed sub-patt) + (hc-append sub-patt sub-patt sub-patt)))))) + +(define pi 3.14) + +(define (area r) + (* pi r r)) diff --git a/racket/hello.rkt b/racket/hello.rkt new file mode 100644 index 0000000..0415ba3 --- /dev/null +++ b/racket/hello.rkt @@ -0,0 +1,29 @@ +#lang slideshow + +(define one 1) +(define c (circle 10)) +(define r (rectangle 10 20)) + +(define (square n) + ; A filled square of side n + (filled-rectangle n n)) + +(define (two-by-two p) + ; hc-append stacks p one after the other by default + ; vc-append does the same thing, but vertically + (define twice-hori + (hc-append p p)) + ; Here we used twice-hori as an intermediate value + ; Often, a let expression is more convenient + (vc-append twice-hori twice-hori)) + +(define (checker a b) + ; With let, we can define multiple names at once + (let ([ab (hc-append a b)] + [ba (hc-append b a)]) + (let ([top (colorize ab "red")] + [bott (colorize ba "green")]) + (vc-append top bott)))) + +(define checker-board + (checker (square 10) (square 10))) diff --git a/racket/pics.rkt b/racket/pics.rkt new file mode 100644 index 0000000..95d91b9 --- /dev/null +++ b/racket/pics.rkt @@ -0,0 +1,68 @@ +#lang racket +(require slideshow) + +(define (square n) + (filled-rectangle n n)) + +(define (zee w h) + (define bar + (filled-rectangle w h)) + (define black-bar + (colorize bar "black")) + (define white-bar + (colorize bar "white")) + (define (iter n) + (if (<= n 1) + (vc-append black-bar white-bar ) + (vc-append black-bar white-bar (iter (- n 1))))) + (iter 5)) + +;(define (chee sz) +; (define (hori a b n) +; (if (<= n 1) +; a (hc-append a [hori b a (- n 1)]))) +; (define (vert a b n) +; (if (<= n 1) +; (hori a b n) +; (vc-append [hori a b n] [vert b a (- n 1)]))) +; (vert +; (colorize (square 50) "white") +; (colorize (square 50) "black") sz)) + + +(define (chee rows cols) + (define (draw-row a b n) + (if (<= n 1) + a (hc-append a [hori b a (- n 1)]))) + (define (draw-board a b n) + (if (<= n 1) + (hori a b n) + (vc-append [hori a b n] [vert b a (- n 1)]))) + (vert + (colorize (square 20) "white") + (colorize (square 20) "black") rows)) + + +(define (add n m) + (if (equal? m 0) + m (+ n (add n (- m 1))))) + + +;(define (chee sz) +; (define white +; (colorize (square sz) "white")) +; (define black +; (colorize (square sz) "black")) +; (define white-black +; (hc-append white black)) +; (define black-white +; (hc-append black white)) +; (define row-white-black +; (define (iter n) +; (if (not (equal? n 0)) +; (hc-append white-black (iter (- n 1))))) +; (iter sz)) +; row-white-black) + + +; cc-superimpose diff --git a/sml/comb.sml b/sml/comb.sml new file mode 100644 index 0000000..8237bba --- /dev/null +++ b/sml/comb.sml @@ -0,0 +1,19 @@ +datatype 'a K + = C of 'a kcons + | P of 'a kprod +and 'a kcons + = B of 'a * ('a K) list * ('a K) list + | H of bool +and 'a kprod + = M of 'a * ('a K) list + | F of ('a K) list + +(* sem: 'a K -> 'a kcons *) +fun sem (C c) = c + | sem (P p) = + case p of + M (a, kns) => B a (P (M (a, kns))) kns + | F ks => F ks + + + diff --git a/vimscript/README.org b/vimscript/README.org new file mode 100644 index 0000000..20eebe8 --- /dev/null +++ b/vimscript/README.org @@ -0,0 +1,3 @@ +#+TITLE: vimscript + +Most of these are unfinished.. diff --git a/vimscript/five.vim b/vimscript/five.vim new file mode 100644 index 0000000..9917275 --- /dev/null +++ b/vimscript/five.vim @@ -0,0 +1,61 @@ +" Vim global plugin for limiting the width of text +" Last Change: 2021 Feb 22 +" Maintainer: Julin S +" License: MIT License + +if exists("g:loaded_mailify") + finish +endif +let g:loaded_mailify = 1 + +if !hasmapto('MailifyAdd') + " would cause error if the key is already bound + xnoremap m :call s:Mailify() MailifyMailify +endif + +function Mailify() + +py3 << EOF +from typing import List +import re +import vim + +def mailify(lines: "vim.buffer", limit: int = 80) -> List[str]: + rv = [] + for line in lines: + if not line or line.isspace(): + rv.append(line) + while line: + endidx = None + linelen = len(line) + if linelen < limit: + endidx = linelen + else: + for idx in range(limit-1, -1, -1): + if line[idx] == " ": + endidx = idx + break + if endidx is None: + for idx in range(limit, linelen): + if line[idx] == " ": + endidx = idx + break + if endidx is None: + enidx = linelen + rv.append(line[:endidx]) + line = line[endidx+1:] + return rv + +curbuf = vim.current.buffer +(startline, _) = curbuf.mark("<") +(endline, _) = curbuf.mark(">") +mailified_lines = mailify(curbuf[startline-1: endline]) +del curbuf[startline-1: endline] +curbuf.append(mailified_lines, startline-1) +EOF + +endfunction + +"xnoremap mmm :call Mailify() +" would cause error if the key is already bound +xnoremap m :call Mailify() diff --git a/vimscript/latex.vim b/vimscript/latex.vim new file mode 100644 index 0000000..f37ad89 --- /dev/null +++ b/vimscript/latex.vim @@ -0,0 +1,31 @@ +"" Only current word would be taken care of. +"" That too only if cursor is not on the first char of the word. + +"function! Fn(prefix) +" a:prefix . expand("") . "}" +"endfunction + +function! Fn2(prefix, suffix) + " colnum starts from 1 whereas string indexing starts from 0 + let curcolnum = col(".") - 1 + let curline = getline(".") + if curcolnum > 0: + let prevchar = strcharpart(curline, curcolnum-1, 1) + if prevchar != " " + normal! "b" + endif + else + normal! "ct " . a:prefix . "pa}" "but what if there is no space remaining + endif +endfunction + +" texttt +"inoremap t bi\texttt{ea} +nnoremap t ciw\texttt{pa} +" textit +"inoremap i bi\textit{ea} +nnoremap i ciw\textit{pa} + +" textbf +"inoremap b bi\textbf{ea} +nnoremap b ciw\textbf{pa} diff --git a/vimscript/md.vim b/vimscript/md.vim new file mode 100644 index 0000000..7a0ea0d --- /dev/null +++ b/vimscript/md.vim @@ -0,0 +1,206 @@ +function! PromoteHeading() + " Promote a heading to next level + let line = getline(".") + if (line =~ "^##* ") == 1 + call setline(".", "#" . line) + endif +endfunction + +function! DemoteHeading() + " Demote a heading to previous level + let line = getline(".") + if (line =~ "^###* ") == 1 + let modedline = strcharpart(line, 1) + call setline(".", modedline) + endif +endfunction + +function! PrevHeading() + " Like C-c C-p in emacs org-mode + let linenum = line(".") - 1 + while linenum > 0 + let line = getline(linenum) + if (line =~ "^##* ") == 1 + echo linenum + call cursor(linenum, 0) + break + endif + let linenum -= 1 + endwhile +endfunction + +function! NextHeading() + " Like C-c C-n in emacs org-mode + let linenum = line(".") + 1 + let linemax = line("$") + 1 + while linenum < linemax + let line = getline(linenum) + if (line =~ "^##* ") == 1 + echo linenum + call cursor(linenum, 0) + break + endif + let linenum += 1 + endwhile +endfunction + +function! FoldTitleContent() +py3 << EOF +from typing import Tuple +import re + +def fold_subtree(lines: "vim.buffer", curlinenum: int) -> Tuple[int, int]: + """ + Accept current line number and return the line numbers corresponding + to the subtree to be folded. + + Assume that indexing starts from zero for all line indices. + Including current line number and return values. + + Args: + lines: a vim buffer object + curlinenum: current line number + """ + heading_re = r"^#+ " + + # Find startline + startline = None + for linenum in range(curlinenum, -1, -1): + matchobj = re.match(heading_re, lines[linenum]) + if matchobj: + startline = linenum + 1 + hnum = len(matchobj.group(0)) + break + if startline is None: + # Not part of any heading (maybe top-most part outside of all headings) + return None + + # Find endline + endline = None + #for linenum, line in enumerate(lines[curlinenum+1:]): + for linenum in range(curlinenum+1, len(lines)): + matchobj = re.match(heading_re, lines[linenum]) + if matchobj is not None and hnum >= len(matchobj.group(0)): + endline = linenum - 1 + break + if endline is None: + # This heading is the last heading + endline = len(lines) - 1 + + return startline, endline + +curlinenum = int(vim.eval("line('.')")) +start, end = fold_subtree(vim.current.buffer, curlinenum - 1) +start += 1 +end += 1 +vim.command(f"{start},{end}fo") +EOF +endfunction + +"py3 << EOF +"import vim +"import re +" +"def fold_title_content(): +" curbuf = vim.current.buffer +" curline = int(vim.eval("line('.')")) - 1 +" startline = None +" for linenum in range(curline, -1, -1): +" line = curbuf[linenum] +" matchobj = re.match(r"^#+", line) +" if matchobj: +" startline = linenum + 1 # no need to fold the heading as well +" matchstr = matchobj.group(0) +" break +" +" if startline is not None: +" # Found startline by this point +" pattern = "^" + matchstr +" maxlinenum = len(curbuf) +" endline = None +" for linenum in range(curline+1, maxlinenum+1): +" line = curbuf[linenum] +" matchobj = re.match(pattern, line) +" if matchobj: +" endline = linenum - 1 +" break +" if endline is None: +" endline = maxlinenum +" +" # Translating Python indexing to vim indexing +" startline += 1 +" endline += 1 +" vim.command(f"{startline},{endline}fold") +" +"fold_title_content() +"EOF + +"function! FoldTitleContent() +" " Find heading section start +" let startline = -1 +" let linenum = line(".") +" while linenum > 0 +" let line = getline(linenum) +" if (line =~ "^##* ") == 1 +" startline = linenum + 1 " got to fold next line onwards +" break +" endif +" endwhile +" +" " No heading found before current cursor position +" if startline != -1 +" " get the starting of header including the space +" let heading = matchstr(line, "^##* ") +" let pattern = "^" . heading +" +" " Find heading section end +" let lastlinenum = line("$") +" let endline = -1 +" linenum = line(".") + 1 +" while linenum <= lastlinenum +" line = getline(linenum) +" if (line =~ pattern) == 1 +" endline = linenum - 1 " got to fold till before next heading +" break +" endif +" endwhile +" +" if endline == -1 +" endline = line("$") +" endif +" endif +"endfunction +" +" let astrsk_count = strchars(matchstr(line, "^##* ") - 1) +" if astrsk_count > 0 +" +" endif +" +" +"function! PrevNextHeading(incr) +" let linenum = line(".") + a:incr +" while linenum > 0 +" while linenum < max +" let line = getline(linenum) +" if (line =~ "^##* ") == 1 +" echo linenum +" call cursor(linenum, 0) +" break +" endif +" let linenum += a:incr +" endwhile +"endfunction + +"nnoremap :call DemoteHeading() +"nnoremap :call PromoteHeading() +nnoremap :call DemoteHeading() +nnoremap :call PromoteHeading() +nnoremap :call PrevHeading() +nnoremap :call NextHeading() +nnoremap :call FoldTitleContent() + + + +function! Co() + " 3,5fo +endfunction diff --git a/vimscript/py-eg.vim b/vimscript/py-eg.vim new file mode 100644 index 0000000..690a286 --- /dev/null +++ b/vimscript/py-eg.vim @@ -0,0 +1,16 @@ +function! Foo() +py3 << EOF +def hello(): + pass +hello() +EOF +endfunction + +function! Bar() +py3 << EOF +def hello(): + pass +hello() +EOF +endfunction + diff --git a/vimscript/supersub.vim b/vimscript/supersub.vim new file mode 100644 index 0000000..505a7a7 --- /dev/null +++ b/vimscript/supersub.vim @@ -0,0 +1,43 @@ +let g:modes = { +\ "super": ["0123456789abcdefghijklmnoprstuvwxyzABDEGHIJKLMNOPRTUVW+-=()", +\ "⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾᴿᵀᵁⱽᵂ⁺⁻⁼⁽⁾"], +\ "sub": ["0123456789abcdefghijklmnoprstuvwxyzABDEGHIJKLMNOPRTUVW+-=()", +\ "⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾᴿᵀᵁⱽᵂ⁺⁻⁼⁽⁾"], +\ } + +let g:superscript_from = '0123456789abcdefghijklmnoprstuvwxyzABDEGHIJKLMNOPRTUVW+-=()' +let g:superscript_to = '⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾᴿᵀᵁⱽᵂ⁺⁻⁼⁽⁾' + +function! Core(line_list, from_to_map) + return map(a:line_list, {key, val -> tr(val, a:from_to_map[0], a:from_to_map[1]}) +endfunction + +" https://stackoverflow.com/questions/1533565/how-to-get-visually-selected-text-in-vimscript +function! Get_visual() + let [line_start, column_start] = getpos("'<")[1:2] + let [line_end, column_end] = getpos("'>")[1:2] + let l:lines = getline(line_start, line_end) + echo l:lines + if len(l:lines) == 0 + return '' + endif + + "call map(l:lines, {key, val -> tr(val, g:superscript_from, g:superscript_to)}) + let l:result = Core(l:lines, g:modes["super"][0], g:modes["super"][1]) + let rv = setline(line_start, l:result) + "let rv = setline(line_start, l:lines) +endfunction + + +" function! s:get_visual_selection() +" " Why is this not a built-in Vim script function?! +" let [line_start, column_start] = getpos("'<")[1:2] +" let [line_end, column_end] = getpos("'>")[1:2] +" let lines = getline(line_start, line_end) +" if len(lines) == 0 +" return '' +" endif +" let lines[-1] = lines[-1][: column_end - (&selection == 'inclusive' ? 1 : 2)] +" let lines[0] = lines[0][column_start - 1:] +" return join(lines, "\n") +" endfunction