hs-to-coq/examples/containers/lib/IntSetValidity.v at master · antalsz/hs-to-coq · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Converted imports: *)

Require Coq.Numbers.BinNums.
Require Data.Bits.
Require Data.Foldable.
Require Data.IntSet.Internal.
Require GHC.Base.
Require GHC.Num.
Import Data.Bits.Notations.
Import GHC.Base.Notations.
Import GHC.Num.Notations.

(* No type declarations to convert. *)

(* Converted value declarations: *)

Fixpoint commonPrefix (t : Data.IntSet.Internal.IntSet) : bool
           := let sharedPrefix
               : Data.IntSet.Internal.Prefix -> Coq.Numbers.BinNums.N -> bool :=
                fun p a => p GHC.Base.== (p Data.Bits..&.(**) a) in
              match t with
              | Data.IntSet.Internal.Nil => true
              | Data.IntSet.Internal.Tip _ _ => true
              | (Data.IntSet.Internal.Bin p _ l r as b) =>
                  andb (Data.Foldable.all (sharedPrefix p) (Data.IntSet.Internal.elems b)) (andb
                        (commonPrefix l) (commonPrefix r))
              end.

Fixpoint maskPowerOfTwo (t : Data.IntSet.Internal.IntSet) : bool
           := match t with
              | Data.IntSet.Internal.Nil => true
              | Data.IntSet.Internal.Tip _ _ => true
              | Data.IntSet.Internal.Bin _ m l r =>
                  andb (Utils.Containers.Internal.BitUtil.bitcount #0 (m) GHC.Base.== #1) (andb
                        (maskPowerOfTwo l) (maskPowerOfTwo r))
              end.

Fixpoint maskRespected (t : Data.IntSet.Internal.IntSet) : bool
           := match t with
              | Data.IntSet.Internal.Nil => true
              | Data.IntSet.Internal.Tip _ _ => true
              | Data.IntSet.Internal.Bin _ binMask l r =>
                  andb (Data.Foldable.all (fun x => Data.IntSet.Internal.zero x binMask)
                        (Data.IntSet.Internal.elems l)) (andb (Data.Foldable.all (fun x =>
                                                                                    negb (Data.IntSet.Internal.zero x
                                                                                          binMask))
                                                               (Data.IntSet.Internal.elems r)) (andb (maskRespected l)
                                                                                                     (maskRespected r)))
              end.

Definition nilNeverChildOfBin : Data.IntSet.Internal.IntSet -> bool :=
  fun t =>
    let fix noNilInSet t'
              := match t' with
                 | Data.IntSet.Internal.Nil => false
                 | Data.IntSet.Internal.Tip _ _ => true
                 | Data.IntSet.Internal.Bin _ _ l' r' => andb (noNilInSet l') (noNilInSet r')
                 end in
    match t with
    | Data.IntSet.Internal.Nil => true
    | Data.IntSet.Internal.Tip _ _ => true
    | Data.IntSet.Internal.Bin _ _ l r => andb (noNilInSet l) (noNilInSet r)
    end.

Definition validTipPrefix : Data.IntSet.Internal.Prefix -> bool :=
  fun p => (#63 Data.Bits..&.(**) p) GHC.Base.== #0.

Fixpoint tipsValid (t : Data.IntSet.Internal.IntSet) : bool
           := match t with
              | Data.IntSet.Internal.Nil => true
              | (Data.IntSet.Internal.Tip p b as tip) => validTipPrefix p
              | Data.IntSet.Internal.Bin _ _ l r => andb (tipsValid l) (tipsValid r)
              end.

Definition valid : Data.IntSet.Internal.IntSet -> bool :=
  fun t =>
    andb (nilNeverChildOfBin t) (andb (maskPowerOfTwo t) (andb (commonPrefix t)
                                                               (andb (maskRespected t) (tipsValid t)))).

(* External variables:
     andb bool false negb true Coq.Numbers.BinNums.N Data.Bits.op_zizazi__
     Data.Foldable.all Data.IntSet.Internal.Bin Data.IntSet.Internal.IntSet
     Data.IntSet.Internal.Nil Data.IntSet.Internal.Prefix Data.IntSet.Internal.Tip
     Data.IntSet.Internal.elems Data.IntSet.Internal.zero GHC.Base.op_zeze__
     GHC.Num.fromInteger Utils.Containers.Internal.BitUtil.bitcount
*)