source: extracted/untrusted/glue.ml @ 2742

Last change on this file since 2742 was 2742, checked in by sacerdot, 7 years ago

Untrusted register colouring fully branched.

File size: 628 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.reverse0 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))
Note: See TracBrowser for help on using the repository browser.