source: extracted/untrusted/glue.ml @ 2968

Last change on this file since 2968 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 718 bytes
Line 
1let int_of_bitvector v =
2  let rec aux pow v =
3    match v with
4      Vector.VEmpty -> 0
5    | Vector.VCons (_,hd,tl) ->
6        if hd = Bool.True then
7          pow + (aux (pow * 2) tl)
8        else
9          aux (pow * 2) tl
10  in
11    aux 1 (Vector.reverse Nat.O v)
12
13let rec int_of_matitapos =
14 function
15   Positive.One -> 1
16 | Positive.P0 v -> int_of_matitapos v * 2
17 | Positive.P1 v -> int_of_matitapos v * 2 + 1
18
19let option_of_matitaoption =
20 function
21    Types.None -> None
22  | Types.Some v -> Some v
23
24let rec matitanat_of_int n =
25 if n = 0 then Nat.O
26 else if n < 0 then assert false
27 else Nat.S (matitanat_of_int (n-1))
28
29let rec int_of_matitanat =
30 function
31    Nat.O -> 0
32  | Nat.S n -> int_of_matitanat n + 1
Note: See TracBrowser for help on using the repository browser.