Ignore:
Timestamp:
Nov 12, 2010, 4:01:48 PM (9 years ago)
Author:
mulligan
Message:

Strange problem with matita and the Maybe file? Cannot find Maybe.ng.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r235 r236  
     1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     2(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
     3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     4
    15include "Vector.ma".
    26include "List.ma".
    37include "Nat.ma".
    48include "Bool.ma".
     9
     10(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     11(* Common synonyms.                                                           *)
     12(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    513
    614ndefinition BitVector ≝ λn: Nat. Vector Bool n.
     
    1119ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
    1220
     21(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     22(* Creating bitvectors from scratch.                                          *)
     23(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     24
     25(* @name: zero
     26   @desc: Produces a bitvector containing <tt>n</tt> copies of <tt>False</tt>.
     27*)
    1328ndefinition zero ≝
    1429  λn: Nat.
    1530    replicate Bool n False.
    1631   
     32ndefinition max ≝
     33  λn: Nat.
     34    replicate Bool n True.
     35   
     36ndefinition append ≝ append.
     37
     38(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     39(* Logical operations.                                                        *)
     40(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     41   
     42(*
     43 @name: conjunction
     44 @desc: The logical conjunction of two bitvectors of length <tt>n</tt>.
     45*)
    1746ndefinition conjunction ≝
    1847  λn: Nat.
     
    2049  λc: BitVector n.
    2150    zip Bool Bool Bool n conjunction b c.
    22    
     51
     52(*
     53 @name: inclusive_disjunction
     54 @desc: The logical inclusive disjunction of two bitvectors of length
     55        <tt>n</tt>.
     56*)   
    2357ndefinition inclusive_disjunction ≝
    2458  λn: Nat.
     
    2761    zip Bool Bool Bool n inclusive_disjunction b c.
    2862   
     63(*
     64 @name: exclusive_disjunction
     65 @desc: The logical exclusive disjunction of two bitvectors of length
     66        <tt>n</tt>.  (XOR).
     67*)       
    2968ndefinition exclusive_disjunction ≝
    3069  λn: Nat.
     
    3372    zip Bool Bool Bool n exclusive_disjunction b c.
    3473   
     74(*
     75 @name: complement
     76 @desc: The logical complement of a bitvector of length <tt>n</tt>.
     77*)   
    3578ndefinition complement ≝
    3679  λn: Nat.
    3780  λb: BitVector n.
    3881    map Bool Bool n (negation) b.
     82   
     83(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     84(* Conversions to and from lists and natural numbers.                         *)
     85(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3986
    4087ndefinition divide_with_remainder ≝
    4188  λm, n: Nat.
    4289    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
     90   
     91(* @name: pad
     92   @desc: Pads the front of a bitvector of length <tt>n</tt> with <tt>m</tt>
     93          copies of <tt>False</tt>.
     94*)
     95ndefinition pad ≝
     96  λm, n: Nat.
     97  λb: BitVector n.
     98    let padding ≝ replicate Bool m False in
     99      append Bool m n padding b.
    43100
    44101nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
     
    58115          ]
    59116      ].
     117
     118(* @name: bitvector_of_nat
     119   @desc: Constructs a bitvector whose integer value is the same as <tt>m</tt>.
     120          Size of the resulting bitvector is clamped to <tt>n</tt>.
     121*)
     122ndefinition bitvector_of_nat ≝
     123  λm, n: Nat.
     124    let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
     125    let size ≝ length Bool biglist in
     126    let bvector ≝ bitvector_of_list Bool biglist in
     127    let difference ≝ n - size in
     128      pad difference size bvector.
     129     
     130ndefinition list_of_bitvector ≝ list_of_vector.
     131ndefinition bitvector_of_list ≝ vector_of_list.
Note: See TracChangeset for help on using the changeset viewer.