The Coq mailing list

[Satrajit Roy <admin AT satrajit.com>]

I posted the following a couple days ago and re-posting just to make sure it made it to the list.

This may be too trivial, but I just can't get the typing quite right.

I need to do something like the following in order to have an object factory that parses through serialized data (i.e. a stream of bytes) and constructs the appropriate objects.  I'd appreciate any help.

I would also appreciate any pointers to relevant work already done or some reading material that describes how to implement such arbitrary object factories.

Require Import List.

Record a:Set:=A{a':nat}.
Record b:Set:=B{b':nat;b'':list a}.
Record c:Set:=C{c':nat;c'':b}.

Inductive obj_enum:Set:=
  | A'
  | B'
  | C'
.

Definition obj_kind (o:obj_enum) :=
  match o with
    | A' => a
    | B' => b
    | C' => c
  end
.

Fixpoint create_obj (l:list nat) (o:obj_enum) {struct o}:=
  match o return (obj_kind o) with
    | A' => (A (nth 0 l 0))
    | B' => (B (nth 0 l 1) (create_objs (tail l) A'))
    | C' => (C (nth 0 l 2) (create_obj  (tail l) B'))
  end
  with create_objs (l:list nat) (o:obj_enum) {struct l}:=
    match l with
      | nil => nil
      | n :: l' => (create_obj (n::nil) o) :: (create_objs l' o)
  end
.