This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

design problem
• Pietro Abate
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Pietro Abate Subject: design problem
```Hi all,
I've the following code to write types and functions in an extensible
way, so to re-use my code a bit. Everything seems working fine.

I've two questions:
- Is there a better way of achieving a similar result ? Here I'm using
polymorphic variants, but I'm wondering if somebody already cooked
something together by using variants and camlp4 extensions...
- At the moment type errors are pretty horrible. How can I coerce these
functions to give prettier errors ? I've tried to coerce the function
f in the *_aux functions below, but of course this is not possible as
it needs to be polymorphic by design ...

thanks :)
p

(* my basic data type *)
type 'a termpc =
[`And of 'a * 'a
|`Or of 'a * 'a
|`Not of 'a
|`Atom of string
]
;;

(* a simple normal form function *)
let nnfpc_aux f = function
|`Not ( `Not x   )  -> f x
|`Not ( `And(x,y) ) -> `Or  (f (`Not x), f (`Not y) )
|`Not ( `Or (x,y) ) -> `And (f (`Not x), f (`Not y) )
|`And (x,y)         -> `And (f x, f y)
|`Or  (x,y)         -> `Or  (f x, f y)
|`Not ( `Atom _) as x -> x
|`Atom _ as x -> x
|_ -> failwith "impossible pc"
;;

let rec nnfpc t = nnfpc_aux nnfpc t;;

(* extension of the basic data type *)
type 'a termk =
[`Dia of 'a
|`Box of 'a
|'a termpc
]
;;

let nnfk_aux f = function
|`Not (`Dia x ) -> `Box (f (`Not x))
|`Not (`Box x ) -> `Dia (f (`Not x))
|`Dia x         -> `Dia (f x)
|`Box x         -> `Box (f x)
|#termpc as x -> nnfpc_aux f x
|_ -> failwith "impossible k"
;;

let rec nnfk t = nnfk_aux nnfk t;;

(* an other extension on top of termk *)
type 'a termlck =
[`CDia of 'a
|`CBox of 'a
|'a termk
]
;;

let rec nnflck_aux f = function
|`Not (`CDia x ) -> `CBox (f (`Not x))
|`Not (`CBox x ) -> `CDia (f (`Not x))
|`CDia x         -> `CDia (f x)
|`CBox x         -> `CBox (f x)
|#termk as x -> nnfk_aux f x
|_ -> failwith "impossible lck"
;;

let rec nnflck t = nnflck_aux nnflck t;;

let a = `Not (`Not (`Not (`Dia (`CDia (`Atom "a")))));;
let b = nnflck a;;

--
++ Blog: http://blog.rsise.anu.edu.au/?q=pietro
++
++ "All great truths begin as blasphemies." -George Bernard Shaw
++ Please avoid sending me Word or PowerPoint attachments.
See http://www.fsf.org/philosophy/no-word-attachments.html

```