Commits

camlspotter  committed 596013a

phantom improvement fix

  • Participants
  • Parent commits 590fd7b

Comments (0)

Files changed (13)

 open Spotlib.Spot
+open Spotlib.Spot.Phantom
 
 module Builder = struct
   include Monad.Make(struct
   type 'a m = 'a Monad.t
 
   let unknownM (v : 'a v m) : unknown v m = 
-    v >>= fun v -> return (!=?v)
+    v >>= fun v -> return (!?v)
     
   let magicM (v : 'a v m) : 'b v m = perform
     v <-- v;
-    return (Value.magic v)
+    return (magic v)
 
   let unsafeM v = perform
     v <-- v;
-    return (Value.unsafe v)
+    return (unsafe v)
 
   let call 
       ?(name="called") (* CR jfuruse: called + f's name *)
       | Llvm.TypeKind.Void -> ""
       | _ -> name
     in
-    unsafeM (Llvm.build_call !=<f (Value.to_array args) name)
+    unsafeM (Llvm.build_call !<f (to_array args) name)
 
   let call_va_args
       ?(name="called")
       | Llvm.TypeKind.Void -> ""
       | _ -> name
     in
-    unsafeM (Llvm.build_call !=<f (Array.of_list (Value.to_list args 
-                                            @ List.map (!=<) va_args)) name)
+    unsafeM (Llvm.build_call !<f (Array.of_list (to_list args 
+                                            @ List.map (!<) va_args)) name)
 
   let global_stringptr ?(name="stringptr") str : i8 pointer v m = 
     unsafeM (Llvm.build_global_stringptr str name)
       (v : 'a v) 
       (ty : 'ty typ)
       : 'ty v m = 
-    unsafeM (Llvm.build_bitcast !=<v !:<ty name)
+    unsafeM (Llvm.build_bitcast !<v !<ty name)
 
   let pointercast 
       ?(name="pointer")
       (v : 'a pointer v)
       (ty : 'ty typ)
       : 'ty v m =
-    unsafeM (Llvm.build_pointercast !=<v !:<ty name)
+    unsafeM (Llvm.build_pointercast !<v !<ty name)
 
   (* unsafe *)
   let unsafe_gep 
       (v : 'a pointer v)
       (xs : i32 v list)
       : 'unsafe pointer v m = 
-    unsafeM (Llvm.build_gep !=<v (Array.of_list (List.map (!=<) xs)) name)
+    unsafeM (Llvm.build_gep !<v (Array.of_list (List.map (!<) xs)) name)
 
   let load 
       ?(name="loaded")
       (v : 'ty pointer v)
       : 'ty v m = 
-    unsafeM (Llvm.build_load !=<v name)
+    unsafeM (Llvm.build_load !<v name)
 
   let store 
       (x : 'a v)
       ~dst:(dst : 'a pointer v)
       : unit m = 
-    Monad.ignore (Llvm.build_store !=<x !=<dst)
+    Monad.ignore (Llvm.build_store !<x !<dst)
 
-  let ret x : unit m = Monad.ignore (Llvm.build_ret !=<x)
+  let ret x : unit m = Monad.ignore (Llvm.build_ret !<x)
   let ret_void : unit m = Monad.ignore Llvm.build_ret_void
 
   let phi 
       ?(name="phi")
       (lst : ('a v * Llvm.llbasicblock) list)
       : 'a v m =
-    unsafeM (Llvm.build_phi (List.map (fun (v, b) -> !=<v, b) lst) name)
+    unsafeM (Llvm.build_phi (List.map (fun (v, b) -> !<v, b) lst) name)
 
   let cond_br 
       (b : i1 v)
       bthen belse
       : unit m
-      = Monad.ignore (Llvm.build_cond_br !=<b bthen belse)
+      = Monad.ignore (Llvm.build_cond_br !<b bthen belse)
 
   let br b = Monad.ignore (Llvm.build_br b)
 
   let is_null ?(name="is_null") (lv : 'a pointer v) : i1 v m = 
-    unsafeM (Llvm.build_is_null !=<lv name)
+    unsafeM (Llvm.build_is_null !<lv name)
 
   (* CR jfuruse: unfortunately no arith type check is done yet *)      
   let arith (defname : string) f = 
     fun ?(name=defname) (x : 'a v) (y : 'a v) ->
-      (unsafeM (f !=<x !=<y name) : 'a v m)
+      (unsafeM (f !<x !<y name) : 'a v m)
   let cmp (defname : string) f = 
     fun ?(name=defname) (x : 'a v) (y : 'a v) ->
-      (unsafeM (f !=<x !=<y name) : i1 v m)
+      (unsafeM (f !<x !<y name) : i1 v m)
 
   let add  ?name = arith "added" Llvm.build_add ?name
   let sub  ?name = arith "subed" Llvm.build_sub ?name
   let printf : string -> unknown v list -> unit m = 
     fun fmt args -> perform
       fmt <-- global_stringptr ~name:"fmt" fmt;
-      Monad.ignore (call_va_args (Module.External.printf) (Value.c1 fmt) args ~name:"res")
+      Monad.ignore (call_va_args (Module.External.printf) (c1 fmt) args ~name:"res")
   ;;
 
   let cast_name v lty =
     in
     pointercast ~name v lty
 
-  let memcpy ~dst ~src ~size = call ~name:"copied" Module.External.memcpy (Value.c3 dst src size)
+  let memcpy ~dst ~src ~size = call ~name:"copied" Module.External.memcpy (c3 dst src size)
 
-  let bzero dst ~size = Monad.ignore (call Module.External.bzero (Value.c2 dst size))
+  let bzero dst ~size = Monad.ignore (call Module.External.bzero (c2 dst size))
 
   let malloc : ?name:string -> ?bzero:bool -> i32 v -> void_pointer v m =
     fun ?(name="alloced") ?bzero:(zero=false) size -> perform
-      ptr <-- call ~name Module.External.malloc (Value.c1 size);
+      ptr <-- call ~name Module.External.malloc (c1 size);
       if zero then bzero ptr ~size else return ();
       return ptr
   ;;
 
   let free ptr = perform
     ptr <-- bitcast ptr pointer_void;
-    Monad.ignore (call Module.External.free (Value.c1 ptr))
+    Monad.ignore (call Module.External.free (c1 ptr))
   ;;
 
   let unsafe_const_load ?name ptr indices = perform
     let insertion = Llvm.insertion_block
 
     (* They are independent from the builder *) 	
-    let append ?(name="block") (v : ('a -> 'b) pointer t) = Llvm.append_block context name !=<v  
-    let parent bb : ('a -> 'b) pointer t = Value.unsafe (Llvm.block_parent bb)
+    let append ?(name="block") (v : ('a -> 'b) pointer v) = Llvm.append_block context name !<v  
+    let parent bb : ('a -> 'b) pointer v = unsafe (Llvm.block_parent bb)
   end
 
-  let func name (ty_ret : 'ret typ) (args : 'args Ltype.Base.WithString.ts) 
+  let func name (ty_ret : 'ret typ) (args : ('args, (string * Llvm.lltype)) ts) 
       (f : ('args -> 'ret) pointer v -> 'args vs -> 'ret v m) : ('args -> 'ret) pointer v m =
     Format.eprintf "Creating function %s@." name;
     let lty = function_ ty_ret (Ltype.Base.WithString.types args) in
     (* name args *)
     List.iter2 (fun lv_param name ->
       Value.set_name name lv_param) 
-      (Value.to_unknown_list (function_params lv_f))
+      (to_unknown_list (function_params lv_f))
       (Ltype.Base.WithString.tags args);
     let bb = Block.append ~name:"entry" lv_f in
     perform 
         phi incoming ~name:"fortmp");
 
     (do_enter,   do_,  do_exit)   <-- append_code_block "do" (do_ phi);
-    \ Llvm.add_incoming (!=<do_, do_exit) !=<phi; (* now we can add the other incoming *)
+    \ Llvm.add_incoming (!<do_, do_exit) !<phi; (* now we can add the other incoming *)
 
     let exit_bb = Block.append ~name:"exit" current_function in
 
       let name = Printf.sprintf "lbuilder.exec%d" !cntr in
       Format.eprintf "Executing %s...@." name;
       let f : (unit -> void) pointer v =
-        let proto = function_ void Type.c0 in
+        let proto = function_ void c0 in
         match Module.Function.lookup name with
         | Some _ -> failwithf "function %s is defined more than once" name
         | None -> Module.Function.declare name proto

File lbuilder_intf.ml

 open Ltype.Base
 open Lvalue.Base
 
+open Spotlib.Spot.Phantom
+
 module type S = sig
 
   (** Monad for builder *)    
     val parent : Llvm.llbasicblock -> ('a -> 'b) pointer v
   end
 
-  val func : string -> 'a typ -> 'b Ltype.Base.WithString.ts 
+  val func : string -> 'a typ -> ('b, (string * Llvm.lltype)) ts
     -> (('b -> 'a) pointer v (* self *)
         -> 'b vs -> 'a v m) -> ('b -> 'a) pointer v m
   (** [func name return_type arg_types f] defines a function of a name [name] whose type is

File lgenvalue.ml

 open Llvm_executionengine
 open Ltype.Base
 
+open Spotlib.Spot.Phantom
+
 module GV = GenericValue
 
 (** phantom *)
-include Phantom.Make(struct type t = GV.t end)
-type 'a v = 'a t
-type 'a vs = 'a ts
+type 'a v = ('a, GV.t) t
+type 'a vs = ('a, GV.t) ts
 
-let (!==<) = (!<)
-let (!==>) = (!>)
-let (!==?) = (!?)
 let unsafe_annotate v _t = v
 
-let of_float : ([>`floating] as 'a) typ -> float -> 'a t = 
-  fun ty -> GV.of_float !:<ty
+let of_float : ([>`floating] as 'a) typ -> float -> 'a v = 
+  fun ty v -> unsafe ^$ GV.of_float !<ty v
 
-let unsafe_of_pointer : 'a (* unsafe *) -> 'b pointer t = 
-  GV.of_pointer
+let unsafe_of_pointer : 'a (* unsafe *) -> 'b pointer v = 
+  fun v -> unsafe ^$ GV.of_pointer v
 
-let of_int32 : ([>`int] as 'a) typ -> int32 -> 'a t =
-  fun ty -> GV.of_int32 !:<ty
+let of_int32 : ([>`int] as 'a) typ -> int32 -> 'a v =
+  fun ty v -> unsafe ^$ GV.of_int32 !<ty v
 
-let of_int : ([>`int] as 'a) typ -> int -> 'a t =
-  fun ty -> GV.of_int !:<ty
+let of_int : ([>`int] as 'a) typ -> int -> 'a v =
+  fun ty v -> unsafe ^$ GV.of_int !<ty v
 
-let of_nativeint : ([>`int] as 'a) typ -> nativeint -> 'a t =
-  fun ty -> GV.of_nativeint !:<ty
+let of_nativeint : ([>`int] as 'a) typ -> nativeint -> 'a v =
+  fun ty v -> unsafe ^$ GV.of_nativeint !<ty v
 
-let of_int64 : ([>`int] as 'a) typ -> int64 -> 'a t =
-  fun ty -> GV.of_int64 !:<ty
+let of_int64 : ([>`int] as 'a) typ -> int64 -> 'a v =
+  fun ty v -> unsafe ^$ GV.of_int64 !<ty v
 
-let as_float : ([>`floating] as 'a) typ -> 'a t -> float = 
-  fun ty -> GV.as_float !:<ty
-let as_unsafe_pointer : 'a pointer t -> 'b (* unsafe *) = GV.as_pointer
-let as_int32 : ([>`int] as 'a) t -> int32  = GV.as_int32
-let as_int : ([>`int] as 'a) t -> int = GV.as_int
-let as_nativeint : ([>`int] as 'a) t -> nativeint = GV.as_nativeint
-let as_int64 : ([>`int] as 'a) t -> int64 = GV.as_int64
+let as_float : ([>`floating] as 'a) typ -> 'a v -> float = 
+  fun ty v -> GV.as_float !<ty !<v
+let as_unsafe_pointer : 'a pointer v -> 'b (* unsafe *) = fun v -> GV.as_pointer !<v
+let as_int32 : ([>`int] as 'a) v -> int32  = fun v -> GV.as_int32 !<v
+let as_int : ([>`int] as 'a) v -> int = fun v -> GV.as_int !<v
+let as_nativeint : ([>`int] as 'a) v -> nativeint = fun v -> GV.as_nativeint !<v
+let as_int64 : ([>`int] as 'a) v -> int64 = fun v -> GV.as_int64 !<v
 

File lgenvalue.mli

 open Ltype.Base
 open Llvm_executionengine
 
+open Spotlib.Spot.Phantom
+
+type 'a v = ('a, GenericValue.t) t 
+type 'a vs = ('a, GenericValue.t) ts
+
 (** phantom *)
-include Phantom_intf.S with type elt = GenericValue.t
-
-val ( !==< ) : 'a t -> GenericValue.t
-val ( !==> ) : GenericValue.t -> unknown t
-val ( !==? ) : 'a t -> unknown t
 (* val unsafe_annotate : GenericValue.t -> 'a v _t = v *)
 
-val of_float : ([>`floating] as 'a) typ -> float -> 'a t
-val unsafe_of_pointer : 'a (* unsafe *) -> 'b pointer t
-val of_int32 : ([>`int] as 'a) typ -> int32 -> 'a t
-val of_int : ([>`int] as 'a) typ -> int -> 'a t
-val of_nativeint : ([>`int] as 'a) typ -> nativeint -> 'a t
-val of_int64 : ([>`int] as 'a) typ -> int64 -> 'a t
+val of_float : ([>`floating] as 'a) typ -> float -> 'a v
+val unsafe_of_pointer : 'a (* unsafe *) -> 'b pointer v
+val of_int32 : ([>`int] as 'a) typ -> int32 -> 'a v
+val of_int : ([>`int] as 'a) typ -> int -> 'a v
+val of_nativeint : ([>`int] as 'a) typ -> nativeint -> 'a v
+val of_int64 : ([>`int] as 'a) typ -> int64 -> 'a v
 
-val as_float : ([>`floating] as 'a) typ -> 'a t -> float
-val as_unsafe_pointer : 'a pointer t -> 'b (* unsafe *)
-val as_int32 : ([>`int] as 'a) t -> int32
-val as_int : ([>`int] as 'a) t -> int
-val as_nativeint : ([>`int] as 'a) t -> nativeint
-val as_int64 : ([>`int] as 'a) t -> int64
+val as_float : ([>`floating] as 'a) typ -> 'a v -> float
+val as_unsafe_pointer : 'a pointer v -> 'b (* unsafe *)
+val as_int32 : ([>`int] as 'a) v -> int32
+val as_int : ([>`int] as 'a) v -> int
+val as_nativeint : ([>`int] as 'a) v -> nativeint
+val as_int64 : ([>`int] as 'a) v -> int64
 
 open Spotlib.Spot
+open Spotlib.Spot.Phantom
 
 module E = Llvm_executionengine
 module T = Llvm_target
   let engine = E.ExecutionEngine.create module_
   module ExecutionEngine = struct
     let run_function (lv : ('a -> 'b) pointer v) args = 
-      E.ExecutionEngine.run_function !=<lv args engine
+      E.ExecutionEngine.run_function !<lv args engine
   end
   
   let fpm = Llvm.PassManager.create_function module_
   
   let define_type_name n (t : 'a typ) = 
     let name = A.name ^ "." ^ n in
-    if Llvm.define_type_name name !:<t module_ then
+    if Llvm.define_type_name name !<t module_ then
       match Llvm.type_by_name module_ name with
       | Some t -> 
-          let t = (Type.unsafe t : 'a typ) in
+          let t = (unsafe t : 'a typ) in
           Type.define_name ~modname:A.name n t;
           t
       | None -> assert false
   let dump module_ = Llvm.dump_module module_
   
   module Function = struct
-    let lookup n = Option.map ~f:Value.unsafe (Llvm.lookup_function n module_)
-    let declare n ty = Value.unsafe (Llvm.declare_function n !:<ty module_)
+    let lookup n = Option.map ~f:unsafe (Llvm.lookup_function n module_)
+    let declare n ty = unsafe (Llvm.declare_function n !<ty module_)
   end
   
   module External = struct
-    let declare cname (l_ret : 'a typ) (l_args : 'b typs) : (('b -> 'a) pointer) t =
-      Value.unsafe (Llvm.declare_function cname !:<(function_ l_ret l_args) module_)
+    let declare cname (l_ret : 'a typ) (l_args : 'b typs) : (('b -> 'a) pointer) v =
+      unsafe (Llvm.declare_function cname !<(function_ l_ret l_args) module_)
   
-    let declare_var_arg cname (l_ret : 'a typ) (l_args : 'b typs) : (('b -> dots -> 'a) pointer) t =
-      Value.unsafe (Llvm.declare_function cname !:<(var_arg_function l_ret l_args) module_)
+    let declare_var_arg cname (l_ret : 'a typ) (l_args : 'b typs) : (('b -> dots -> 'a) pointer) v =
+      unsafe (Llvm.declare_function cname !<(var_arg_function l_ret l_args) module_)
   
-    let malloc = declare "malloc" (pointer_void) (Type.c1 i32)
-    let free = declare "free" void (Type.c1 (pointer_void))
-    let memcpy = declare "memcpy" (pointer_void) (Type.c3 (pointer_void) (pointer_void) i32)
-    let printf = declare_var_arg "printf" i32 (Type.c1 (pointer i8))
-    let bzero = declare "bzero" void (Type.c2 (pointer_void) i32)
+    let malloc = declare "malloc" (pointer_void) (c1 i32)
+    let free = declare "free" void (c1 (pointer_void))
+    let memcpy = declare "memcpy" (pointer_void) (c3 (pointer_void) (pointer_void) i32)
+    let printf = declare_var_arg "printf" i32 (c1 (pointer i8))
+    let bzero = declare "bzero" void (c2 (pointer_void) i32)
   end
   
   module PassManager = struct
-    let run_function_if_opt lv = if opt then ignore (Llvm.PassManager.run_function !=<lv fpm : bool);
+    let run_function_if_opt lv = if opt then ignore (Llvm.PassManager.run_function !<lv fpm : bool);
   end
   
 end

File lmodule_intf.ml

 open Ltype.Base
 open Lvalue.Base
 
+open Spotlib.Spot.Phantom
+
 open Llvm_executionengine (* for GenericValue *)
 
 module type S = sig
   end
 
   module Function : sig
-    val lookup : string -> (unknown -> unknown) pointer t option
+    val lookup : string -> (unknown -> unknown) pointer v option
     val declare : string -> ('a -> 'b) typ -> ('a -> 'b) pointer v
   end
   
 (* llvm type algebra *)
 
 open Llvm
+open Spotlib.Spot
+open Spotlib.Spot.Phantom
 
 module Base = struct
   (** phantom *)
-  include Spotlib.Spot.Phantom.Make(struct type t = lltype end)
-  type 'a typ = 'a t 
-  type 'a typs = 'a ts
-  
-  let (!:<) = (!<)
-  let (!:>) = (!>)
-  let (!:?) = (!?)
+  type 'a typ = ('a, lltype) t 
+  type 'a typs = ('a, lltype) ts
   
   (** descriptors *)
   
   type void_pointer = i8 pointer
 
   module type Tagged = sig
-    type tag
-    include Spotlib.Spot.Phantom_intf.S with type elt = tag * Llvm.lltype
-    val tags : 'a ts -> tag list
-    val types : 'a ts -> 'a typs
-    val combine : tag list -> 'a typs -> 'a ts
-    val tag : tag -> 'a typ -> 'a t
+    val tags : ('a, ('tag * lltype)) ts -> 'tag list
+    val types : ('a, ('tag * lltype)) ts -> 'a typs
+    val combine : 'tag list -> 'a typs -> ('a, ('tag * lltype)) ts
+    val tag : 'tag -> 'a typ -> ('a, ('tag * lltype)) t
   end
 
-  module Tagged(Tag : sig type t end) = struct
-    let base_unsafe = unsafe
-    let base_to_list = to_list
-    let base_unsafe_of_list = unsafe_of_list
-
-    type tag = Tag.t
-    include Spotlib.Spot.Phantom.Make(struct 
-      type t = tag * lltype
-    end)
-  
+  module Tagged = struct
     let tags ts = List.map fst (to_list ts)
-    let types (ts : 'a ts) : 'a typs = 
-      base_unsafe_of_list (List.map (fun (_,ty) -> base_unsafe ty) (to_list ts))
-    let combine tags (ts : 'a typs) : 'a ts =
-      unsafe_of_list (List.map unsafe (List.combine tags (base_to_list ts)))
-    let tag t v = (t, v)
+    let types (ts : ('a, 'tag * lltype) ts) : 'a typs = 
+      unsafe_of_list (List.map snd (to_list ts))
+    let combine (tags : 'tag list) (ts : 'a typs) : ('a, ('tag * lltype)) ts =
+      unsafe_of_list (List.combine tags (to_list ts))
+    let tag t (v : ('a, lltype) t) : ('a, ('tag * lltype)) t = unsafe (t, !<v)
   end
   
-  module WithString = Tagged(struct type t = string end)
+  module WithString = Tagged
 end
 
 open Base
   include Base
 
   (* shorter names *)
-  let classify = classify_type
+  let classify ty = classify_type !<ty
   
-  let integer c (_tag, x) = integer_type c x
-  let float = float_type
-  let double = double_type
-  let function_ ret args = function_type ret (to_array args)
-  let var_arg_function ret args = var_arg_function_type ret (to_array args)
-  let function_params (t : ('args -> 'ret) typ) : 'args typs = unsafe_of_array (param_types t)
-  let function_return = return_type
-  let struct_ c args = struct_type c (Array.of_list (to_list args))
+  let integer c ((_tag : 'itag), x) : 'itag integer typ = unsafe ^$ integer_type c x
+  let float c : float typ = unsafe ^$ float_type c
+  let double c : double typ = unsafe ^$ double_type c
+  let function_ : 'ret typ -> 'args typs -> ('args -> 'ret) typ = fun ret args -> unsafe ^$ function_type !<ret (to_array args)
+  let var_arg_function : 'ret typ -> 'args typs -> ('args -> dots -> 'ret) typ = fun ret args -> unsafe ^$ var_arg_function_type !<ret (to_array args)
+
+  (* CR jfuruse: not for dots !*)
+  let function_params (t : ('args -> 'ret) typ) : 'args typs = unsafe_of_array (param_types !<t)
+  let function_return (ty : ('args -> 'ret) typ) : 'ret typ = unsafe ^$ return_type !<ty
+
+  let struct_ c (args : 'args typs) : 'args struct_ typ = unsafe ^$ struct_type c (to_array args)
+(*
   let check_struct t = match classify t with
     | TypeKind.Struct -> t
     | _ -> assert false
+*)
   
-  let struct_elements (t : 'typs struct_ typ) : 'typs typs = unsafe_of_array (struct_element_types t)
-  let array_ t (_tag, size) = array_type t size
+  let struct_elements (t : 'typs struct_ typ) : 'typs typs = unsafe_of_array (struct_element_types !<t)
+  let array_ (t : 't typ) ((_tag : 'itag), size) : ('t, 'itag) array_ typ = unsafe ^$ array_type !<t size
     
-  let pointer = pointer_type
-  let element = element_type
+  let pointer (t : 't typ) : 't pointer typ = unsafe ^$ pointer_type !<t
+(*
   let check_pointer t = match classify t with
     | TypeKind.Pointer _ -> t
     | _ -> assert false
+*)
+  let element (t : [>`container of 't] typ) : 't typ = unsafe ^$ element_type !<t
 
   let define_name ~modname n t =
     Format.eprintf "Registered named type %s.%s@." modname n;
-    defined_names := (t, (modname, n)) :: !defined_names
+    defined_names := (!<t, (modname, n)) :: !defined_names
 
   (** [string_of_lltype] of LLVM 2.8 has a bug: if it tries to print a recursive type, cabooom! *)        
   (* Here is a fix *)        
     in
     fst (string_of_lltype [] ty)
 
-  let string_of = string_of_lltype
+  let string_of ty = string_of_lltype !<ty
 
   (* now with context *)
-  let void = void_type context
-  let i1 = i1_type context
-  let i8 = i8_type context
-  let i16 = i16_type context
-  let i32 = i32_type context 
-  let i64 = i64_type context
+  let void : void typ = unsafe ^$ void_type context
+  let i1 : i1 typ = unsafe ^$ i1_type context
+  let i8 : i8 typ = unsafe ^$ i8_type context
+  let i16 : i16 typ = unsafe ^$ i16_type context
+  let i32 : i32 typ = unsafe ^$ i32_type context 
+  let i64 : i64 typ = unsafe ^$ i64_type context
   let integer x = integer context x
   let float = float context 
   let double = double context
   let struct_ x = struct_ context x
+(*
   let check_pointer t = match classify t with
     | TypeKind.Pointer _ -> Obj.magic t (* !! *)
     | _ -> assert false
+*)
 
   (* void pointer is special in LLVM. It is illegal! *)
   let pointer_void = pointer i8
   let refine opaque ~by = refine_type opaque by
   let recursive (f : 'a typ -> 'b typ) : 'b typ =
     let op = opaque () in
-    let ty = f op in
-    refine op ~by:ty;
+    let ty = f (unsafe op) in
+    refine op ~by:(!<ty);
     ty
 end
 
 module Make(A : sig val context : Llvm.llcontext end) : S
   (* lots of equalities but we cannot live without them... *)
-  with type 'a t = 'a t
-  and type 'a ts = 'a ts
-  and type void = void
+  with type void = void
   and type i1 = i1
   and type i8 = i8
   and type i16 = i16

File ltype_intf.ml

+open Spotlib.Spot.Phantom
+
 module type S0 = sig
   (** phantom *)
-  include Spotlib.Spot.Phantom_intf.S with type elt = Llvm.lltype
-  type 'a typ = 'a t
-  type 'a typs = 'a ts
-  
-  val ( !:< ) : 'a typ -> Llvm.lltype
-  val ( !:> ) : Llvm.lltype -> unknown typ
-  val ( !:? ) : 'a typ -> unknown typ
+  type 'a typ = ('a, Llvm.lltype) t
+  type 'a typs = ('a, Llvm.lltype) ts
   
   (** descriptors *)
   
   type void_pointer = i8 pointer
 
   module type Tagged = sig
-    type tag
-    include Spotlib.Spot.Phantom_intf.S with type elt = tag * Llvm.lltype
-    val tags : 'a ts -> tag list
-    val types : 'a ts -> 'a typs
-    val combine : tag list -> 'a typs -> 'a ts
-    val tag : tag -> 'a typ -> 'a t
+    val tags : ('a, ('tag * Llvm.lltype)) ts -> 'tag list
+    val types : ('a, ('tag * Llvm.lltype)) ts -> 'a typs
+    val combine : 'tag list -> 'a typs -> ('a, ('tag * Llvm.lltype)) ts
+    val tag : 'tag -> 'a typ -> ('a, ('tag * Llvm.lltype)) t
   end
 
-  module Tagged(Tag : sig type t end) 
-    : Tagged with type tag = Tag.t
-
-  module WithString 
-    : Tagged with type tag = string
+  module Tagged : Tagged
+  module WithString : Tagged
 end
 
 module type S = sig
   val function_return : ('args -> 'ret) typ -> 'ret typ
     (* function_ is prefixed to avoid the name clash with Monad.return *)
   val struct_ : 'args typs -> 'args struct_ typ
+(*
   val check_struct : 'a typ -> unknown struct_ typ
     (** may raise Assert_failure *)
+*)
 
   val struct_elements : 'args struct_ typ -> 'args typs
   val array_ : 'a typ -> 'tag * int -> ('a, 'tag) array_ typ
   val pointer : 'a typ -> 'a pointer typ
+(*
   val check_pointer : 'a typ -> 'a pointer typ
     (** may raise Assert_failure *)
+*)
 
   val element : [>`container of 'a] typ -> 'a typ
 
 open Llvm
+open Spotlib.Spot
+open Spotlib.Spot.Phantom
+
+open Ltype.Base
 
 module Base = struct
   (** phantom *)
-  include Spotlib.Spot.Phantom.Make(struct type t = llvalue end)
-  type 'a v = 'a t
-  type 'a vs = 'a ts
+  type 'a v = ('a, llvalue) t
+  type 'a vs = ('a, llvalue) ts
   
-  let (!=<) = (!<)
-  let (!=>) = (!>)
-  let (!=?) = (!?)
-  let unsafe_annotate v _t = v
+  let unsafe_annotate v (_t : 'ty typ) : 'ty v = unsafe v
   
-  let dump = dump_value
-  let type_of v = Obj.magic (type_of v) (* !! *)
-  let typs_of (ts : 'typs ts) : 'typs Ltype.Base.typs =
-    Ltype.Base.unsafe_of_list (List.map Llvm.type_of (to_list ts))
-  let set_name = set_value_name
-  let name = value_name
+  let dump v = dump_value !<v
+  let type_of (v : 'typ v) = unsafe ^$ type_of !<v
+  let typs_of (ts : 'typs vs) : 'typs typs = 
+    unsafe_of_list (List.map Llvm.type_of (to_list ts))
+  let set_name name v = set_value_name name !<v
+  let name v = value_name !<v
   
-  let function_params f = unsafe_list (Array.to_list (params f))
+  let function_params (f : ('args -> 'ret) pointer v) : 'args vs = 
+    unsafe_list (Array.to_list (params !<f))
 end
 
 open Base
 
   module Ltype = Ltype.Make(A)
 
-  (* We cannot easily open Ltype, since it overwrites Phantom *)
-  let (!:<) = Ltype.(!:<)
-
   module Const = struct
-    let int = const_int (if Sys.word_size = 32 then !:<Ltype.i32 else !:<Ltype.i64)
-    let nativeint n = 
-      const_of_int64 (if Sys.word_size = 32 then !:<Ltype.i32 else !:<Ltype.i64) (Int64.of_nativeint n) false
-    let i32 n = const_of_int64 (!:<Ltype.i32) (Int64.of_int32 n) false
-    let i32_of_int n = const_of_int64 (!:<Ltype.i32) (Int64.of_int n) false
+    let int v : [`int] v = unsafe ^$ const_int (if Sys.word_size = 32 then !<Ltype.i32 else !<Ltype.i64) v
+    let nativeint n : [`int] v = 
+      unsafe ^$ const_of_int64 (if Sys.word_size = 32 then !<Ltype.i32 else !<Ltype.i64) (Int64.of_nativeint n) false
+    let i32 n : i32 v = unsafe ^$ const_of_int64 (!<Ltype.i32) (Int64.of_int32 n) false
+    let i32_of_int n : i32 v = unsafe ^$ const_of_int64 (!<Ltype.i32) (Int64.of_int n) false
     let i32_0 = i32_of_int 0
     let i32_1 = i32_of_int 1
-    let i64 n = const_of_int64 (!:<Ltype.i64) n false
-    let double = const_float (!:<Ltype.double)
-    let bool b = const_int (!:<Ltype.i1) (if b then 1 else 0)
+    let i64 n : i64 v = unsafe ^$ const_of_int64 (!<Ltype.i64) n false
+    let double f : double v = unsafe ^$ const_float (!<Ltype.double) f
+    let bool b : i1 v = unsafe ^$ const_int (!<Ltype.i1) (if b then 1 else 0)
   
-    let bitcast v ty = const_bitcast v !:<ty
-    let intcast v ty = const_intcast v !:<ty
-    let ptrtoint v ty = const_ptrtoint v !:<ty
-    let null ty = const_null !:<ty
+    let bitcast v (ty : 'typ typ) : 'typ v = unsafe ^$ const_bitcast !<v !<ty
+    let intcast (v : [>`int] v) (ty : ([>`int] as 'typ) typ) : 'typ v = unsafe ^$ const_intcast !<v !<ty
+    let ptrtoint (v : 'a pointer v) (ty : ([>`int] as 'typ) typ) : 'typ v = unsafe ^$ const_ptrtoint !<v !<ty
+    let null (ty : 'typ typ) : 'typ v = unsafe ^$ const_null !<ty
   
     let unsafe_gep v ints = 
-      const_gep v (Array.of_list (List.map i32_of_int ints))
+      unsafe ^$ const_gep !<v (Array.of_list (List.map (fun x -> !<(i32_of_int x)) ints))
 
     let offset_of ty indices =
       (* CR jfuruse: only for 32 bit arch! *)
   end
   
   (* CR: size of is defined here, where value is available *)
-  let size_i64_of ty : Ltype.i64 t = Llvm.size_of !:<ty
-  let size_of ty = Const.intcast (size_i64_of ty) Ltype.i32
+  let size_i64_of ty : i64 v = unsafe ^$ Llvm.size_of !<ty
+  let size_of ty : i32 v = Const.intcast (size_i64_of ty) Ltype.i32
 
   module Analysis = struct
-    let assert_valid_function (v : ('a -> 'b) Ltype.pointer v) = Llvm_analysis.assert_valid_function !=<v
+    let assert_valid_function (v : ('a -> 'b) pointer v) = Llvm_analysis.assert_valid_function !<v
   end
 end
 
 open Base
 
 module Make(A : sig val context : llcontext end) : S
-  with type 'a t = 'a t
-  and type 'a ts = 'a ts

File lvalue_intf.ml

 open Ltype.Base
+open Spotlib.Spot.Phantom
 
 module type S0 = sig
   (** phantom *)
-  include Spotlib.Spot.Phantom_intf.S with type elt = Llvm.llvalue
-  type 'a v = 'a t
-  type 'a vs = 'a ts
+  type 'a v = ('a, Llvm.llvalue) t
+  type 'a vs = ('a, Llvm.llvalue) ts
 
-  (** safe/unsafe coercions. Begin with "!=". ("!:" is for type coercions.) *)
-  val ( !=< ) : 'a v -> Llvm.llvalue
-    (** Coerce down to [llvalue] *)
-  val ( !=? ) : 'a v -> unknown v
-    (** Forget the type info *)
-  val ( !=> ) : Llvm.llvalue -> unknown v
-    (** Lift up to [unknown v] *)
   val unsafe_annotate : Llvm.llvalue -> 'ty typ -> 'ty v 
     (** annotate a type, but unsafe *)
 
   include S0
 
   module Const : sig
-    val int : int -> unknown v
-    val nativeint : nativeint -> unknown v
+    val int : int -> [`int] v
+    val nativeint : nativeint -> [`int] v
     val i32 : int32 -> i32 v
     val i32_of_int : int -> i32 v
     val i32_0 : i32 v

File lwrap_intf.ml

 
   open Lvalue.Base
   module Value : Lvalue_intf.S
-    with type 'a t = 'a t
-    and type 'a ts = 'a ts
 
   open Ltype.Base
   module Type : sig
     include Ltype_intf.S
 	(* lots of equalities but we cannot live without them... *)
-      with type 'a t = 'a t
-      and type 'a ts = 'a ts
-      and type void = void
+      with type void = void
       and type i1 = i1
       and type i8 = i8
       and type i16 = i16