diff options
Diffstat (limited to 'lib/syntax/check.ml')
| -rw-r--r-- | lib/syntax/check.ml | 83 |
1 files changed, 23 insertions, 60 deletions
diff --git a/lib/syntax/check.ml b/lib/syntax/check.ml index 9292a7a..b642945 100644 --- a/lib/syntax/check.ml +++ b/lib/syntax/check.ml @@ -1,51 +1,14 @@ -(** This module provide a way to create new Id dynamically in the runtime, - and some fonctions for comparing them. *) -module Id : sig - type 'a typeid - (** The type created on-the-fly. *) - - val newtype : unit -> 'a typeid - (** Create a new instance of a dynamic type *) - - type ('a, 'b) eq = Eq : ('a, 'a) eq - - val try_cast : 'a typeid -> 'b typeid -> ('a, 'b) eq option - (** Compare two types using the Eq pattern *) -end = struct - type 'a witness = .. - - module type Witness = sig - type t - type _ witness += Id : t witness - end - - type 'a typeid = (module Witness with type t = 'a) - type ('a, 'b) eq = Eq : ('a, 'a) eq - - let try_cast : type a b. a typeid -> b typeid -> (a, b) eq option = - fun x y -> - let module X : Witness with type t = a = (val x) in - let module Y : Witness with type t = b = (val y) in - match X.Id with Y.Id -> Some Eq | _ -> None - - let newtype (type u) () = - (* The extensible type need to be extended in a module, it is not possible - to declare a type in a function. That’s why we need to pack a module - here *) - let module Witness = struct - type t = u - type _ witness += Id : t witness - end in - (module Witness : Witness with type t = u) -end +module Id = Type.Id (** The the Id module, wrap a value in an existencial type with a witness associate with. *) -type result = R : { value : 'a; witness : 'a Id.typeid } -> result +type result = R : { value : 'a; witness : 'a Id.t } -> result -let get : type a. a Id.typeid -> result -> a option = +let get : type a. a Id.t -> result -> a option = fun typeid (R { value; witness }) -> - match Id.try_cast typeid witness with Some Eq -> Some value | None -> None + match Id.provably_equal typeid witness with + | Some Type.Equal -> Some value + | None -> None type t = | E : { @@ -57,12 +20,12 @@ type t = and type Instruction.t' = 'd and type Location.t = 'e and type context = 'f); - expr_witness : 'a Id.typeid; - expr' : 'b Id.typeid; - instr_witness : 'c Id.typeid; - instr' : 'd Id.typeid; - location_witness : 'e Id.typeid; - context : 'f Id.typeid; + expr_witness : 'a Id.t; + expr' : 'b Id.t; + instr_witness : 'c Id.t; + instr' : 'd Id.t; + location_witness : 'e Id.t; + context : 'f Id.t; } -> t @@ -74,14 +37,14 @@ let build : and type Instruction.t' = _ and type Location.t = 'a and type context = _) -> - 'a Id.typeid * t = + 'a Id.t * t = fun module_ -> - let expr_witness = Id.newtype () - and expr' = Id.newtype () - and instr_witness = Id.newtype () - and instr' = Id.newtype () - and location_witness = Id.newtype () - and context = Id.newtype () in + let expr_witness = Id.make () + and expr' = Id.make () + and instr_witness = Id.make () + and instr' = Id.make () + and location_witness = Id.make () + and context = Id.make () in let t = E { @@ -106,9 +69,9 @@ end open StdLabels module Helper = struct - type 'a expr_list = { witness : 'a Id.typeid; values : 'a list } + type 'a expr_list = { witness : 'a Id.t; values : 'a list } - let expr_i : result array list -> 'a Id.typeid -> int -> 'a expr_list = + let expr_i : result array list -> 'a Id.t -> int -> 'a expr_list = fun args witness i -> let result = List.fold_left args ~init:{ values = []; witness } @@ -355,8 +318,8 @@ module Make (A : App) = struct let rebuild_clause : type a b. int -> - a Id.typeid -> - b Id.typeid -> + a Id.t -> + b Id.t -> S.pos * result array * result array list -> (b, a) S.clause = fun i instr_witness expr' clause -> |