open Batteries
open Map

(* Function implementation
  - 'i: input
  - 'o: output
  - 'd: datatype

  - 'r: result

  'i ~> 'o := ('i, 'o, 'd) fi
*)

type ('i, 'o, 'd) fi =
  {
    make: unit -> 'd;
    set: 'i -> 'o -> 'd -> 'd;
    unset: 'i -> 'd -> 'd;
    get: 'i -> 'd -> 'o option;
    foldi: 'r. ('i -> 'o -> 'r -> 'r) -> 'd -> 'r -> 'r
  }

(* Function implementation by PMap
  'i ~> 'o := ('i, 'o, ('i, 'o) PMap)
*)

let pmap_implementation =
  let make' () =
    PMap.empty
  in
  let set' input output data =
    PMap.add input output data
  in
  let unset' input data =
    PMap.remove input data
  in
  let get' input data =
    try
      Some (PMap.find input data)
    with
    | Not_found -> None
  in
  let foldi' f data x =
    PMap.foldi f data x
  in
  {
    make = make';
    set = set';
    unset = unset';
    get = get';
    foldi = foldi'
  }

(* Function recursive implementation
  - 't: type (abstract type)
  - 'd: datatype (concrete type)
  - 'a: abstraction (abstraction of abstract type) (it's the same thing as the abstract type except that in C, 'c is replaced by unit
                                to allow differetiation function types treated as constants and function types being implemented)

  - 'c: constant type
  - 'it: input type
  - 'id: input datatype
  - 'ia: input abstraction
  - 'ot: output type
  - 'od: output datatype
  - 'oa: output abstraction
*)

type ('t, 'd, 'a, 'plop) fri =
  | C: 'c -> ('c, 'c, unit, 'c) fri
  | F: ('it, 'id, 'ia, 'plopi) fri * ('ot, 'od, 'oa, 'plopo) fri * ('id, 'od, 'd) fi -> ('it -> 'ot, 'd, 'ia -> 'oa, 'id -> 'od) fri

(* Function
  - 't type (abstract type)
  - 'd datatype (concrete type)
  - 'a abstract (abstraction of abstract type)
*)
type ('t, 'd, 'a, 'plop) t =
  {
    data: 'd;
    implementation: ('t, 'd, 'a, 'plop) fri
  }

(* That's where the 'a is supposed to help: I only need to match against F *)
let get1 (i : 'id) (f : ('t, 'd, 'ai -> 'ao, 'id -> 'od) t) =
  match f.implementation with
  | F (ii, oi, fi) -> fi.get i f.data (* This works *)