Commits

Jacques-Pascal Deplaix committed ff3327d

Use a GADT for constraining int types and having the same int type in array + add a function LLVM_types.string

Comments (0)

Files changed (3)

examples/hello.ml

-let c c = LLVM_types.int 8 (int_of_char c)
-
 let () =
   LLVM.print_context_module
     (LLVM.new_global
        ~link_type:(Some `Internal)
        ~constant:true
        "msg"
-       (LLVM_types.Value (LLVM_types.array 13 (LLVM_types.Int 8) [c 'h'; c 'e'; c 'l'; c 'l'; c 'o'; c ' '; c 'w'; c 'o'; c 'r'; c 'l'; c 'd'; LLVM_types.int 8 0]))
+       (LLVM_types.Value (LLVM_types.string 13 "hello world!"))
     );
   LLVM.print_context_module
     (LLVM.new_declaration
-       (LLVM_types.Int 32)
+       (LLVM_types.Int LLVM_types.thirty_two)
        "puts"
-       [| LLVM_types.Pointer (LLVM_types.Int 8) |]
+       [| LLVM_types.Pointer (LLVM_types.Int LLVM_types.eight) |]
       ~link_type:(Some `External)
     );
   LLVM.print_context_module
     (LLVM.new_definition
-      (LLVM_types.Int 32)
+      (LLVM_types.Int LLVM_types.thirty_two)
       "main"
       [||]
-      [LLVM.Ret (LLVM_types.int 32 0)]
+      [LLVM.Ret (LLVM_types.int32 0)]
     )

src/LLVM_types.ml

+module N_star : sig
+  type one
+  type 'a s
+
+  type _ t =
+    | One : one t
+    | Succ : 'a t -> 'a s t
+
+  val to_int : 'a t -> int
+end = struct
+  type one
+  type 'a s
+
+  type _ t =
+    | One : one t
+    | Succ : 'a t -> 'a s t
+
+  let rec to_int : type a. a t -> int = function
+    | One -> 1
+    | Succ n -> succ (to_int n)
+end
+
 type _ f =
   | Ret : 'a t -> 'a t f
   | App : 'a t * 'b f -> ('a * 'b) f
 
 and _ t =
-  | Int : int -> int t
+  | Int : 'a N_star.t -> (int * 'a N_star.t) t
   | Array : int * 'a t -> 'a value list t
   | Pointer : 'a t -> 'a t t
   | FunctionPointer : 'a f -> 'a f t
     | App (t, f) -> aux (acc ^ ", " ^ to_string t) f (* FALSE ! Also before *)
   in
   match data with
-    | Int i -> "i" ^ string_of_int i
+    | Int i -> "i" ^ string_of_int (N_star.to_int i)
     | Array (i, t) ->
         "[" ^ string_of_int i ^ " x " ^ to_string t ^ "]"
     | Pointer t -> to_string t ^ "*"
 
 let value_to_string (t, value) = to_string t ^ " " ^ value
 
+type one = N_star.one
+type 'a seven_plus = 'a N_star.s N_star.s N_star.s N_star.s N_star.s N_star.s N_star.s
+type 'a eight_plus = 'a N_star.s seven_plus
+type eight = N_star.one seven_plus
+type sixteen = eight eight_plus
+type thirty_two = sixteen eight_plus eight_plus
+type sixty_four = thirty_two eight_plus eight_plus eight_plus eight_plus
+
+let one = N_star.One
+let seven_plus x = N_star.(Succ (Succ (Succ (Succ (Succ (Succ (Succ x)))))))
+let eight_plus x = seven_plus (N_star.Succ x)
+let eight = seven_plus one
+let sixteen = eight_plus eight
+let thirty_two = eight_plus (eight_plus sixteen)
+let sixty_four = eight_plus (eight_plus (eight_plus (eight_plus thirty_two)))
+
 let int x value = (Int x, string_of_int value)
+let int1 = int one
+let int8 = int eight
+let int16 = int sixteen
+let int32 = int thirty_two
+let int64 = int sixty_four
 let array n t value =
   (Array (n, t), "[" ^ String.concat ", " (List.map value_to_string value) ^ "]")
 let pointer t value = (Pointer t, to_string value)
+
+let string n value = (Array (n, Int eight), "\"" ^ String.escaped value ^ "\\00\"")

src/LLVM_types.mli

+module N_star : sig
+  type one
+  type 'a s
+
+  type _ t =
+    | One : one t
+    | Succ : 'a t -> 'a s t
+
+  val to_int : 'a t -> int
+end
+
 type _ f =
   | Ret : 'a t -> 'a t f
   | App : 'a t * 'b f -> ('a * 'b) f
 
 and _ t =
-  | Int : int -> int t
+  | Int : 'a N_star.t -> (int * 'a N_star.t) t
   | Array : int * 'a t -> 'a value list t
   | Pointer : 'a t -> 'a t t
   | FunctionPointer : 'a f -> 'a f t
 val to_string : 'a t -> string
 val value_to_string : 'a value -> string
 
-val int : int -> int -> int value
+type one = N_star.one
+type 'a seven_plus = 'a N_star.s N_star.s N_star.s N_star.s N_star.s N_star.s N_star.s
+type 'a eight_plus = 'a N_star.s seven_plus
+type eight = N_star.one seven_plus
+type sixteen = eight eight_plus
+type thirty_two = sixteen eight_plus eight_plus
+type sixty_four = thirty_two eight_plus eight_plus eight_plus eight_plus
+
+val eight : eight N_star.t
+val seven_plus : 'a N_star.t -> 'a seven_plus N_star.t
+val eight_plus : 'a N_star.t -> 'a eight_plus N_star.t
+val sixteen : sixteen N_star.t
+val thirty_two : thirty_two N_star.t
+val sixty_four : sixty_four N_star.t
+
+val int : 'a N_star.t -> int -> (int * 'a N_star.t) value
+val int1 : int -> (int * one N_star.t) value
+val int8 : int -> (int * eight N_star.t) value
+val int16 : int -> (int * sixteen N_star.t) value
+val int32 : int -> (int * thirty_two N_star.t) value
+val int64 : int -> (int * sixty_four N_star.t) value
 val array : int -> 'a t -> 'a value list -> 'a value list value
 val pointer : 'a t -> 'a t -> 'a t value
+val string : int -> string -> (int * eight N_star.t) value list value