open Printf
(** Variables and terms *)
type var = string
type 'a term =
| Var of var
| Cons of 'a * 'a term list
(* For example:
- "0" would be represented by: Cons ('0', [])
- "S x" would be represented by: Cons ('S', [Var "x"])
- "x + S x" would be represented by: Cons ('+', [Var "x"; Cons ('S', [Var "x"])]) *)
(** Unification algorithm *)
(* Type of substitutions and constraints *)
type 'a subst = (var * 'a term) list
type 'a constraintlist = ('a term * 'a term) list
(* Does a variable appear in a term? *)
let rec appear (x : var) : 'a term -> bool =
function _ -> failwith "not implemented"
(* Replace [x] with [u] in a term *)
let rec replace (x : var) (u : 'a term) : 'a term -> 'a term =
function _ -> failwith "not implemented"
(* Replace [x] with [u] in a list of constraints *)
let replace_clist x u : 'a constraintlist -> 'a constraintlist =
function _ -> failwith "not implemented"
(* Unification algorithm for a list of constraints *)
let rec solve (p : 'a constraintlist) : 'a subst =
failwith "not implemented"
(* Unification algorithm between two terms, using [solve] *)
let unify t u =
failwith "not implemented"
(** Arithmetical expressions : parsing and printing *)
(* Parsing *)
let parse s =
let n = String.length s in
let rec f i =
if n = i then
failwith "String not terminated"
else
match s.[i] with
| ' ' -> f (i + 1)
| '0'..'9' as c -> i+1, Cons(c, [])
| 'a' .. 'z' as c -> (i + 1, Var (String.make 1 c))
| 'S' -> let j, e = f (i + 1) in j, Cons('S', [e])
| ('+' | '-' | '*' | '/') as c ->
let j, a = f (i+1) in
let k, b = f (j+1) in
k, Cons(c, [a; b])
| c -> failwith (sprintf "unknown char: '%c'" c)
in
let (n', a) = f 0 in
if n = n' then
a
else
failwith "Unused part of string"
(* Generic printing *)
let print_term print_constr =
let p = sprintf in
let rec f = function
| Var s -> s
| Cons (c, args) ->
let c = print_constr c in
match args with
| [] -> c
| [a] -> p "%s(%s)" c (f a)
| [a; b] -> p "(%s %s %s)" (f a) c (f b)
| xs -> p "%s(%s)" c (String.concat ", " (List.map f xs))
in f
(* Arithmetical expression printing *)
let print_term = print_term (sprintf "%c")
(* Test on arithmetical expressions *)
let test s1 s2 =
let p = print_term in
let u, v = parse s1, parse s2 in
printf "%s == %s : " (p u) (p v);
try
let subst = unify u v in
let ps = List.map (fun (x, v) -> sprintf "%s -> %s" x (p v)) subst in
printf "[%s]\n" (String.concat "; " ps);
with
Failure err -> printf "error : %s\n" err
let () = test "S x" "S S 0"
let () = test "S x" "S S y"
let () = test "+ x x" "+ 1 2"
let () = test "S x" "x" (* recursive *)
let () = test "S + x y" "+ x z" (* constructors *)
let () = test "S + x S y" "S + S t z"
let () = test "* S + x S y 0" "* S + S t z w"
let () = test "S * S + x S y 0" "S * S + S t z w"
let () = test "S * S + x S y 0" "S * S z w"
let () = test "+ x y" "+ y x"
let () = test "+ x y" "+ S y S x" (* recursive *)
let () = test "+ x y" "+ S y S y" (* recursive *)
let () = test "+ x x" "+ + y z + + z a a"
let () = test "+ x x" "+ + y z + + y a a" (* error? *)