generic/generic_util_sum.ml at master · balez/generic · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
open Generic_core
open Ty.T

let (-<) = Generic_util_fun.(-<)

type empty (* empty type : no value *)
type ('a,'b) sum = Left of 'a | Right of 'b

let left x = Left x
let right x = Right x

let empty_elim (_ : empty) = assert false
(* it shouldn't be possible to execute that function since we cannot give it any actual argument *)

let either l r = function
  | Left x -> l x
  | Right x -> r x

let sum l r = either (left -< l) (right -< r)


(* TODO Boiler plate generated by reify *)
type _ ty +=
    Empty : empty ty
  | Sum : 'a ty * 'b ty -> ('a, 'b) sum ty

(*type _ Generic_core.Ty.ty +=
  | Empty: empty Generic_core.Ty.ty
let () =
  Generic_core.Desc_fun.ext_add_con (Generic_core.Ty.Ty Empty)
    {
      Generic_core.Desc.Ext.con = fun (type a) ->
        fun (ty : a Generic_core.Ty.ty)  ->
          (match ty with
           | Generic_core.Ty.Ty (Empty ) ->
               Generic_core.Desc.Con.make "Empty" Generic_core.Product.T.Nil
                 (fun ()  -> Empty)
                 (function | Empty  -> Some () | _ -> None)
           | _ -> assert false : a Generic_core.Desc.Con.t)
    }

let () =
  Generic_core.Desc_fun.ext Empty
    {
      Generic_core.Desc_fun.f = fun (type a) ->
        fun (ty : a Generic_core.Ty.ty)  ->
          (match ty with
           | Empty  -> Generic_core.Desc.Abstract
           | _ -> assert false : a Generic_core.Desc.t)
    }

type _ Generic_core.Ty.ty +=
  | Sum: 'a1 Generic_core.Ty.ty* 'a2 Generic_core.Ty.ty -> ('a1,'a2) sum
  Generic_core.Ty.ty
let () =
  Generic_core.Desc_fun.ext_add_con
    (Generic_core.Ty.Ty (Sum (Generic_core.Ty.Any, Generic_core.Ty.Any)))
    {
      Generic_core.Desc.Ext.con = fun (type a) ->
        fun (ty : a Generic_core.Ty.ty)  ->
          (match ty with
           | Generic_core.Ty.Ty (Sum (x1,x2)) ->
               Generic_core.Desc.Con.make "Sum"
                 (Generic_core.Product.T.Cons
                    ((Generic_core.Ty.Ty x1),
                      (Generic_core.Product.T.Cons
                         ((Generic_core.Ty.Ty x2),
                           Generic_core.Product.T.Nil))))
                 (fun (x1,(x2,()))  -> Sum (x1, x2))
                 (function | Sum (x1,x2) -> Some (x1, (x2, ())) | _ -> None)
           | _ -> assert false : a Generic_core.Desc.Con.t)
    }

let () =
  Generic_core.Desc_fun.ext (Sum (Generic_core.Ty.Any, Generic_core.Ty.Any))
    {
      Generic_core.Desc_fun.f = fun (type a) ->
        fun (ty : a Generic_core.Ty.ty)  ->
          (match ty with
           | Sum (x1,x2) ->
               Generic_core.Desc.Variant
                 {
                   Generic_core.Desc.Variant.name = "sum";
                   Generic_core.Desc.Variant.module_path =
                     ["Generic_util_sum"];
                   Generic_core.Desc.Variant.cons =
                     (Generic_core.Desc.Variant.cons
                        [Generic_core.Desc.Con.make "Left"
                           (Generic_core.Product.T.Cons
                              (x1, Generic_core.Product.T.Nil))
                           (fun (x1,())  -> Left x1)
                           (function | Left x1 -> Some (x1, ()) | _ -> None);
                        Generic_core.Desc.Con.make "Right"
                          (Generic_core.Product.T.Cons
                             (x2, Generic_core.Product.T.Nil))
                          (fun (x1,())  -> Right x1)
                          (function | Right x1 -> Some (x1, ()) | _ -> None)])
                 }
           | _ -> assert false : a Generic_core.Desc.t)
    }
*)