File: enumclass.mlw

package info (click to toggle)
why3 1.8.2-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 45,028 kB
  • sloc: xml: 185,443; ml: 111,224; ansic: 3,998; sh: 2,578; makefile: 2,568; java: 865; python: 720; javascript: 290; lisp: 205; pascal: 173
file content (23 lines) | stat: -rw-r--r-- 467 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
 
module EnumClass
  use mach.java.lang.Integer

  type kind_of_t = Some_kind | Another_Kind | Some_other_sort

  type t = {
    kind : kind_of_t;
    dummy_value : integer
  }

  let constructor [@java:constructor] () = {
      kind = Some_other_sort; dummy_value = 0
  }
  
  let get_kind (self : t) = self.kind

  let get_integer_kind (self : t) : integer =
    match self.kind with
    | Some_kind -> 1
    | Another_Kind -> 0
    | Some_other_sort -> 2
    end
end