[coq] remembering bitvectors

c/README.org

@@ -3,4 +3,5 @@
  - [[./pi-val.c][pi-val.c]]: Approximating value of pi
  - [[./pi-val-leibnitz.c][pi-val-leibnitz.c]]: Approximating value of pi using Ramanjuan's method
  - [[./pi-val-ramanjuan.c][pi-val-ramanjuan.c]]: Approximating value of pi using Leibnitz's method
+ - [[./grammar-comment-like.c][grammar-comment-like.c]]: A C-grammar 'pitfall'
 

c/grammar-comment-like.c

@@ -0,0 +1,21 @@
+/* https://en.wikipedia.org/wiki/Maximal_munch */
+
+#include<stdio.h>
+int main() {
+    int a=2, *ptr=&a, b;
+    //b = 2/*ptr;
+/*
+grammar-comment-like.c: In function 'main':
+grammar-comment-like.c:13:12: error: invalid type argument of unary '*' (have 'int')
+     b = 2/(*a);
+            ^~
+2
+
+Press ENTER or type command to continue
+grammar-comment-like.c: In function 'main':
+grammar-comment-like.c:12:1: error: expected ';' before '}' token
+ }
+ ^
+*/
+    b = 2/ *ptr;  // This is okay.
+}

coq/bv.v

@@ -0,0 +1,51 @@
+Require Bvector.  (* stdlib uses LSB first (little-endian) representation *)
+Require Vector.
+Require List.
+
+(* Convert a nat list to a bitvector. Non-zero values are considered true *)
+Fixpoint list2Bvec (l:list nat) : Bvector.Bvector (List.length l) :=
+  match l return Bvector.Bvector (List.length l) with
+  | List.cons O xs =>
+      Bvector.Bcons false _ (list2Bvec xs)
+  | List.cons _ xs =>
+      Bvector.Bcons true _ (list2Bvec xs)
+  | List.nil => Bvector.Bnil
+  end.
+
+(* Convert a bitvector to nat. Little-endian representation assumed *)
+Fixpoint bvec2nat_aux {n:nat} (cur:nat) (bv:Bvector.Bvector n): nat :=
+  match bv with
+  | Vector.cons _ x _ xs =>
+      if x then (Nat.pow 2 cur) + bvec2nat_aux (S cur) xs
+      else bvec2nat_aux (S cur) xs
+  | Vector.nil _ => 0
+  end.
+Definition bvec2nat {n:nat} (bv:Bvector.Bvector n): nat := bvec2nat_aux 0 bv.
+
+(* Find nth bit of a bitvector *)
+Definition bvnth {z i:nat} (bv: Bvector.Bvector z) (pf:i<z): bool :=
+  Vector.nth_order bv pf.
+
+Require Import List. 
+Import ListNotations. 
+Compute list2Bvec [0;0;1;0].  (* 0100₂ ie, 4₁₀ *)
+(*
+= [false; false; true; false]
+     : Bvector (length [0; 0; 1; 0])
+*)
+Compute bvec2nat (list2Bvec [0;0;1;0]).
+(* = 4 : nat *)
+
+Compute bvnth (list2Bvec [0;0;1;0]) (_:2<_).
+(* = true : bool *)
+Compute bvnth (list2Bvec [0;0;1;0]) (_:1<_).
+(* = false : bool *)
+
+Check Bcons.
+
+Check Nat.pow.
+Compute Nat.pow 2 3.
+Check Vector.nth_order.
+Check Vector.nth_order (list2Bvec [0;0;1;0]).
+Compute Vector.nth_order (list2Bvec [0;0;1;0]) (_:0<_).
+