modules.ml (937B)
1 module type SURFACE = sig 2 type term 3 end 4 5 module type CORE = sig 6 type term 7 end 8 9 module type DOMAIN = sig 10 type value 11 end 12 13 module type ENVIRONMENT = sig 14 end 15 16 module type CONTEXT = sig 17 type ctx 18 end 19 20 module type ELABORATOR = sig 21 module Ctx: CONTEXT 22 module Surf: SURFACE 23 module Core: CORE 24 25 val infer: Ctx.ctx -> Surf.term -> Core.term 26 val 27 end 28 29 module type BINDER = sig 30 type term 31 32 type t 33 34 val plicity: t -> Plicity.t 35 val names: t -> Name.t array 36 val annot: t -> term option 37 val to_string: t -> string 38 end 39 40 module type MULTI_BINDER = sig 41 module B: BINDER 42 43 type t 44 45 val reorder: bool 46 end 47 48 module type PATTERN = sig 49 type t 50 51 val names: t -> Name.t array 52 end 53 54 module type DEFINER = sig 55 module P: PATTERN 56 type term 57 58 type t 59 60 val recursive: t -> bool 61 val definiendum: t -> P.t 62 val annotation: t -> term option 63 val to_string: t -> string 64 end 65 66 module type MULTI_DEFINER = sig 67 module D: DEFINER 68 69 type t 70 71 val mutual: bool 72 end