console.cr

@@ -1,36 +0,0 @@
-def parse(input)
-  input.lines.map do |s|
-    code, int = s.split(" ")
-    {code, int.to_i32}
-  end
-end
-
-def run(prog)
-  acc = 0
-  pc = 0
-  visited = Set(Int32).new
-  input = Channel(Int32).new
-  output = Channel({Symbol, Int32}).new
-  spawn do
-    loop do
-      if pc >= prog.size
-        output.send({:term, acc})
-        break
-      elsif visited.includes? pc
-        output.send({:inf, acc})
-        break
-      end
-
-      visited << pc
-      code, int = prog[pc]
-      case code
-      when "acc"
-        acc += int
-      when "jmp"
-        pc += int - 1
-      end
-      pc += 1
-    end
-  end
-  {input, output}
-end

day10.cr

@@ -1,37 +0,0 @@
-require "advent"
-INPUT = input(2020, 10).lines.map(&.to_i32).sort!
-
-def part1(input)
-  diff_1 = 0
-  diff_3 = 0
-  curr = 0
-  input << (input.max + 3)
-  input.each do |i|
-    diff_1 += 1 if (i - curr) == 1
-    diff_3 += 1 if (i - curr) == 3
-    curr = i
-  end
-  puts diff_1 * diff_3
-end
-
-def count_ways(input, prev, index, mem, indent = 0)
-  if m = mem[{prev, index}]?
-    return m 
-  end
-  return 0_i64 if input[index] - prev > 3 || index >= input.size
-  return 1_i64 if index == input.size - 1
-
-  total = count_ways(input, input[index], index+1, mem, indent + 1)
-  total += count_ways(input, prev, index+1, mem, indent + 1)
-
-  mem[{prev, index}] = total
-  return total
-end
-
-def part2(input)
-  input << (input.max + 3)
-  count_ways(input, 0, 0, {} of {Int32, Int32} => Int64)
-end
-
-puts part1(INPUT.clone)
-puts part2(INPUT.clone)

day11.cr

@@ -1,64 +0,0 @@
-require "advent"
-INPUT = input(2020, 11).lines.map(&.chars) 
-
-abstract class Search
-  def search(current, x, y, dx, dy)
-    x, y = x + dx, y + dy
-    return 0 if y < 0 || y >= current.size
-    return 0 if x < 0 || x >= current[y].size
-    search_impl(current,x,y,dx,dy)
-  end
-
-  abstract def search_impl(current, x, y, dx, dy)
-end
-
-class FirstSearch < Search
-  def search_impl(current, x, y, dx, dy)
-    return current[y][x] == '#' ? 1 : 0
-  end
-end
-
-class SecondSearch < Search
-  def search_impl(current, x, y, dx, dy)
-    return 1 if current[y][x] == '#'
-    return 0 if current[y][x] == 'L'
-    return search(current, x, y, dx, dy)
-  end
-end
-
-DIRS = [{-1,-1}, {-1, 0}, {-1, 1}, {0, -1}, {0, 1}, {1, -1}, {1, 0}, {1,1}]
-
-def step(current, step, check, n)
-  current.each_with_index do |row, y|
-    row.each_with_index do |seat, x|
-      step[y][x] = current[y][x]
-      count = DIRS.sum do |dx, dy|
-        check.search(current, x, y, dx, dy)
-      end
-      step[y][x] = 'L' if seat == '#' && count >= n
-      step[y][x] = '#' if seat == 'L' && count == 0
-    end
-  end
-  {step, current}
-end
-
-def run(input, search, n)
-  current = input
-  step = input.clone
-  loop do
-    current, step = step(current, step, search, n)
-    break if current.zip_with(step) { |l, r| l == r }.all?
-  end
-  current.sum(&.count(&.==('#')))
-end
-
-def part1(input)
-  run(input, FirstSearch.new, 4)
-end
-
-def part2(input)
-  run(input, SecondSearch.new, 5)
-end
-
-puts part1(INPUT.clone)
-puts part2(INPUT.clone)

day8.cr

@@ -1,21 +1,41 @@
 require "advent"
-require "./console.cr"
+INPUT = input(2020, 8).lines.map do |s|
+  code, int = s.split(" ")
+  {code, int.to_i32}
+end
 
-INPUT = input(2020, 8)
+def run(prog)
+  acc = 0
+  pc = 0
+  visited = Set(Int32).new
+  loop do
+    return {:term, acc} if pc >= prog.size
+    return {:inf, acc} if visited.includes? pc
+      
+    visited << pc
+    code, int = prog[pc]
+    case code
+    when "acc"
+      acc += int
+    when "jmp"
+      pc += int - 1
+    end
+    pc += 1
+  end
+end
 
 def part1
-  run(parse(INPUT))[1].receive[1]
+  run(INPUT)[1]
 end
 
 def part2
-  input = parse(INPUT)
+  jnp = INPUT.find_indices { |e| e[0] == "jmp" || e[0] == "nop" }
-  jnp = input.find_indices { |e| e[0] == "jmp" || e[0] == "nop" }
   jnp.each do |i|
-    prog = input.clone
+    prog = INPUT.clone
     op, int = prog[i]
     prog[i] = {op.tr("jmpnop", "nopjmp"), int}
 
-    code, acc = run(prog)[1].receive
+    code, acc = run(prog)
     return acc if code == :term
   end
 end

day8.v

@@ -1,98 +0,0 @@
-Require Import Coq.ZArith.Int.
-Require Import Coq.Lists.ListSet.
-Require Import Coq.Vectors.VectorDef.
-Require Import Coq.Vectors.Fin.
-
-Module DayEight (Import M:Int).
-  (* We need to coerce natural numbers into integers to add them. *)
-  Parameter nat_to_t : nat -> t.
-  (* We need a way to convert integers back into finite sets. *)
-  Parameter clamp : forall {n}, t -> option (Fin.t n).
-
-  Definition fin := Fin.t.
-  
-  (* The opcode of our instructions. *)
-  Inductive opcode : Type :=
-    | add
-    | nop
-    | jmp.
-
-  (* The result of running a program is either the accumulator
-     or an infinite loop error. In the latter case, we return the
-     set of instructions that we tried. *)
-  Inductive run_result {n : nat} : Type :=
-    | Ok : t -> run_result
-    | Fail : set (fin n) -> run_result.
-
-  Definition state n : Type := (fin (S n) * set (fin n) * t).
-
-  (* An instruction is a pair of an opcode and an argument. *)
-  Definition inst : Type := (opcode * t).
-  (* An input is a bounded list of instructions. *)
-  Definition input (n : nat) := VectorDef.t inst n.
-  (* 'indices' represents the list of instruction
-     addresses, which are used for calculating jumps. *)
-  Definition indices (n : nat) := VectorDef.t (fin n) n.
-
-  (* Compute the destination jump index, an integer. *)
-  Definition jump_t {n} (pc : fin n) (off : t) : t :=
-    M.add (nat_to_t (proj1_sig (to_nat pc))) off.
-
-  (* Compute a destination index that's valid.
-     Not all inputs are valid, so this may fail. *)
-  Definition valid_jump_t {n} (pc : fin n) (off : t) : option (fin (S n)) := @clamp (S n) (jump_t pc off).
-
-  Definition weaken_one {n} (f : fin n) : fin (S n).
-  Proof.
-    apply (@cast (n + 1)).
-    + apply L. apply f.
-    + rewrite <- plus_n_Sm. rewrite <- plus_n_O. reflexivity.
-  Defined.
-
-  Inductive step_noswap {n} : input n -> state n -> state n -> Prop :=
-    | step_noswap_acc : forall inp pc' v acc t,
-        nth inp pc' = (add, t) ->
-        ~ set_mem Fin.eq_dec pc' v = true ->
-        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_add Fin.eq_dec pc' v, M.add acc t)
-    | step_noswap_nop : forall inp pc' v acc t,
-        nth inp pc' = (nop, t) ->
-        ~ set_mem Fin.eq_dec pc' v = true ->
-        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_add Fin.eq_dec pc' v, acc)
-    | step_noswap_jmp : forall inp pc' pc'' v acc t,
-        nth inp pc' = (jmp, t) ->
-        ~ set_mem Fin.eq_dec pc' v = true ->
-        valid_jump_t pc' t = Some pc'' ->
-        step_noswap inp (weaken_one pc', v, acc) (pc'', set_add Fin.eq_dec pc' v, acc).
-
-  Fixpoint nat_to_fin (n : nat) : fin (S n) :=
-    match n with
-    | O => F1
-    | S n' => FS (nat_to_fin n')
-    end.
-
-  Inductive run_noswap {n} : input n -> state n -> state n -> Prop :=
-    | run_noswap_ok : forall inp v acc,
-        run_noswap inp (nat_to_fin n, v, acc) (nat_to_fin n, v, acc)
-    | run_noswap_fail : forall inp pc' v acc,
-        set_mem Fin.eq_dec pc' v = true ->
-        run_noswap inp (weaken_one pc', v, acc) (weaken_one pc', v, acc)
-    | run_noswap_trans : forall inp st st' st'',
-        step_noswap inp st st' -> run_noswap inp st' st'' -> run_noswap inp st st''.
-
-  Inductive valid_inst {n} : inst -> fin n -> Prop :=
-    | valid_inst_add : forall t f, valid_inst (add, t) f
-    | valid_inst_nop : forall t f f',
-        valid_jump_t f t = Some f' -> valid_inst (nop, t) f
-    | valid_inst_jmp : forall t f f',
-        valid_jump_t f t = Some f' -> valid_inst (jmp, t) f.
-
-  (* An input is valid if all its instructions are valid. *)
-  Definition valid_input {n} (inp : input n) : Prop := forall (pc : fin n),
-    valid_inst (nth inp pc) pc.
-
-  Theorem valid_input_terminates  : forall n (inp : input n) st,
-    valid_input inp -> exists st', run_noswap inp st st'.
-  Proof.
-    (* Stoppped here. *)
-  Admitted.
-End DayEight.

day9.cr

@@ -1,37 +0,0 @@
-require "advent"
-INPUT = input(2020, 9).lines.map(&.to_i64) 
-
-def is_sum(is, from, to, n)
-  if to <= from
-    return n == 0_i64
-  end
-  return is_sum(is, from, to-1, n) || is_sum(is, from, to-1, n-is[to-1])
-end
-
-def part1(input)
-  is = input
-  i = 25
-  loop do
-    return is[i] unless is_sum(is, i-25, i, is[i])
-    i += 1
-  end
-end
-
-def part2(input, i)
-  input.each_with_index do |e, j|
-    next if e == i
-    acc = i-e
-    k = j
-    while acc > 0
-      k += 1
-      acc -= input[k]
-    end
-    if acc == 0
-      min, max = input[j..k].minmax
-      return min+max
-    end
-  end
-end
-
-p1 = part1(INPUT.clone)
-puts part2(INPUT.clone, p1)

template.cr

@@ -1,11 +1,13 @@
 require "advent"
-INPUT = input(2020, n)#.lines.map(&.to_i32) 
+INPUT = input(2020, n)#.lines.map(&.chomp) 
 
-def part1(input)
+def part1
+  input = INPUT.clone
 end
 
-def part2(input)
+def part2
+  input = INPUT.clone
 end
 
-puts part1(INPUT.clone)
+part1
-puts part2(INPUT.clone)
+part2