Changeset 697 for src/ASM/Util.ma

Timestamp:

Mar 18, 2011, 1:28:33 PM (9 years ago)

Author:

campbell

Message:

Merge Clight branch of vectors and friends.
Start making stuff build.

Location:

src/ASM

Files:

• . (modified) (1 prop)
• Util.ma (modified) (6 diffs)

src/ASM/Util.ma

@@ -1 +1 @@
 include "arithmetics/nat.ma".
 include "basics/list.ma".
-include "basics/sums.ma".
+include "basics/types.ma".
 
 definition if_then_else ≝
@@ -13 +13 @@
   ].
     
+(*
 notation "hvbox('if' b 'then' t 'else' f)"
   non associative with precedence 83
   for @{ 'if_then_else $b $t $f }.
+*)
+notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
 
 interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
@@ -27 +31 @@
 
 definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
+
+let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝
+match l with
+[ nil ⇒ r
+| cons h t ⇒ revapp T t (h::r)
+].
+
+definition rev ≝ λT:Type[0].λl. revapp T l [ ].
 
 lemma eq_rect_Type0_r :
@@ -64 +76 @@
 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
  with precedence 10
-for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.
+for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
 
 notation "⊥" with precedence 90
@@ -100 +112 @@
 
 let rec division_aux (m: nat) (n : nat) (p: nat) ≝
-  match ltb n p with
+  match ltb n (S p) with
     [ true ⇒ O
     | false ⇒
@@ -147 +159 @@
 definition divide_with_remainder ≝
   λm, n: nat.
-    mk_pair ? ? (m ÷ n) (modulus m n).
+    pair ? ? (m ÷ n) (modulus m n).
     
 let rec exponential (m: nat) (n: nat) on n ≝