diff --git a/coq/README.org b/coq/README.org index 1fdff59..b4fbc8a 100644 --- a/coq/README.org +++ b/coq/README.org @@ -1,8 +1,8 @@ #+TITLE: Coq - - [[./sumn.v]]: Sum of first n natural numbers, their squares and cubes. - - [[./de-morgan.v]]: de-Morgan's laws - - [[./eqns.v]]: A 'hello world' using the 'equations' plugin - - [[./cpdt/]]: stuff from the book CPDT - - [[./sf/]]: stuff from /Software foundations/ + - [[./sumn.v][sumn.v]]: Sum of first n natural numbers, their squares and cubes. + - [[./de-morgan.v][de-morgan.v]]: de-Morgan's laws + - [[./eqns.v][eqns.v]]: A 'hello world' using the 'equations' plugin + - [[./cpdt/][cpdt/]]: stuff from the book CPDT + - [[./sf/][sf]]: stuff from /Software foundations/ diff --git a/lua/README.org b/lua/README.org index 456dfba..1834250 100644 --- a/lua/README.org +++ b/lua/README.org @@ -1,14 +1,14 @@ #+TITLE: Lua Most code snippets are from 2018.. - - [[./calc.lua]]: Basic calculator - - [[./gambler_ruin.lua]]: Gambler's ruin problem - - [[./quadraticEqn.lua]]: Solving a quadratic equation - - [[./co-routine.lua]]: Coroutines - - [[./lua]]-dice.lua: Random number generation - - [[./producer_consumer.lua]]: Producer consumer problem - - [[./tables.lua]]: Using tables - - [[./rev_table.lua]]: Reverse a table + - [[./calc.lua][calc.lua]]: Basic calculator + - [[./gambler_ruin.lua][gambler_ruin.lua]]: Gambler's ruin problem + - [[./quadraticEqn.lua][quadraticEqn.lua]]: Solving a quadratic equation + - [[./co-routine.lua][co-routine.lua]]: Coroutines + - [[./lua][lua]]-dice.lua: Random number generation + - [[./producer_consumer.lua][producer_consumer.lua]]: Producer consumer problem + - [[./tables.lua][tables.lua]]: Using tables + - [[./rev_table.lua][rev_table.lua]]: Reverse a table #- [[./tail_call_debate.lua]] #- [[./sinlua]].lua diff --git a/sml/re-cps.sml b/sml/re-cps.sml new file mode 100644 index 0000000..47f1ca0 --- /dev/null +++ b/sml/re-cps.sml @@ -0,0 +1,54 @@ +(* Starting with int regex *) +datatype re + = Null + | Eps + | Chr of int + | Cat of re * re + | Alt of re * re + | Star of re + +fun op /\ (x, y) = Cat (x, y) +fun op \/ (x, y) = Alt (x, y) +infixr 8 /\ +infixr 9 \/ + +(* checker : re -> (int list -> bool) -> (int list -> bool) *) +fun compile r k l = + case r of + Null => false + | Eps => k l + | Chr c => + (case l of + [] => false + | x::xs => if x=c then k xs + else k (x::xs)) + | Cat (r1, r2) => compile r1 + (fn xs => compile r2 k xs) l + | Alt (r1, r2) => compile r1 k l orelse compile r2 k l + | Star rr => (compile Eps k l) orelse compile (Cat (r, Star rr)) k l +(* +- compile (Chr 3) (fn l => fn b => if l=nil then b else false) [3]; +val it = true : bool +- compile (Chr 3) (fn l => fn b => if l=nil then b else false) [2]; +val it = false : bool +*) + +(* matcher : re -> (int list -> bool) *) +fun matcher r l = compile r + (fn l => if l=nil then true else false) l +(* +- matcher ((Chr 1) /\ (Chr 2)) [1]; +val it = false : bool +- matcher ((Chr 1) /\ (Chr 2)) [1,2]; +val it = true : bool +- matcher ((Chr 1) /\ (Chr 2)) [1,2,3]; +val it = false : bool +*) + +(* +Goes into an infinite loop when [Star] is involved. + +Puzzles me.. + +See: https://www.cs.cmu.edu/~rwh/papers/regexp/jfp.pdf +*)