OK, I think I have a solution .. and it is so dang simple too.

Basically, I normalise the type terms and use ocamls polymorphic
equality operator! The normalisation involves counting what
*real* level of the tree the recursive descent is in -- add one for
each binary Pair node. Each typedef name substituted along
the branch is tracked in an association list along with its level.
When a typedef name is encountered that is in this list,
replace it with Fix n, where n is the associated level number:
this uniquely determines the recursion argument.

The result of this algorithm is completely different to
what I had before .. and it seems right. There's ONLY
one way to represent a given type here.

The intended model is: a pair is a C struct,
the included types are expanded if they're
not strongly coupled with the containing type
if they are, a pointer is used.
[I think this model is sound, I'm not sure yet ..]

----------------------------------------------------------------------
type node_t =
  | Prim of string
  | Pair of node_t * node_t
  | Name of string

type env_t = (string * node_t) list

type lnode_t =
  | LPrim of string
  | LPair of lnode_t * lnode_t
  | LFix of int

let rec bind' env n labels t = match t with
  | Prim s -> LPrim s
  | Pair (t1, t2) ->
    LPair
    (
      bind' env (n+1) labels t1,
      bind' env (n+1) labels t2
    )
  | Name s ->
    if List.mem_assoc s labels
    then LFix (List.assoc s labels)
    else
      bind' env n ((s,n)::labels) (List.assoc s env)

let bind env t =  bind' env 0 [] t


let rec str' n t =
  string_of_int n ^":" ^
  match t with
  | LPrim s -> s
  | LPair (t1,t2) -> "(" ^ str' (n+1) t1 ^ " * " ^ str' (n+1) t2 ^ ")"
  | LFix i -> "fix " ^ string_of_int i

let str t = str' 0 t

let cmp a b = a = b
let strb b = if b then "true" else "false"
let pres a b =
  print_endline (str a);
  print_endline (str b);
  let res = cmp a b in
  print_endline (strb res)
;;

(* ---------------------------------- *)
let env = [
  "x", Pair (Name "y", Prim "int");  (* typedef x = y * int *)
  "y", Pair (Name "x", Prim "float") (* typedef y = x * float *)
]

let t1 = Pair (Name "x", Prim "float")
let t1' = bind env t1
let t2' = bind env (Name "y")
;;

pres t1' t2';; (* FALSE *)

(* ---------------------------------- *)
let env = [
  "x", Pair (Name "x", Prim "int");
  "y", Pair (Name "y", Prim "int")
]
;;

let t1' = bind env (Name "x")
let t2' = bind env (Name "y")
;;

pres t1' t2';; (* TRUE *)

(* ---------------------------------- *)
let env = [
  "x", Pair (Pair (Name "x", Prim "int"), Prim "int");
  "y", Pair (Name "y", Prim "int")
]
;;

let t1' = bind env (Name "x")
let t2' = bind env (Name "y")
;;

pres t1' t2';; (* FALSE *)

(* ---------------------------------- *)

pres t1' t1';; (* TRUE *)

(* ---------------------------------- *)
let env = ["x", Name "x"]
let t = bind env (Name "x")
;;
pres t t;;

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners