(* An all-in-one unification program *) type term = Sym | Var ;; let rec assoc_env x = \ env:[]; (Var x) | env:[|t]; if (x=y) then:v else:(assoc_env env:t x) ;; let rec subst n by:v = \ on:(Var m); if (m=n) then:v else:(Var m) | on:(Sym a l); Sym a (map f:(\x; subst n by:v on:x) l) ;; let rec simplify = \ (Var a); assoc_env a | (Sym a l),*env; Sym a (map f:(simplify env:env) l) ;; let rec not_occur n = \ on:(Var m); if (m=n) then:false else:true | on:(Sym a l); it_list f:(\ ok:true,v /ok:not_occur n on:v | ok:false,_ /ok:false) l ok:true \*ok; ok ;; let rec add_env *env = if (not_occur n on:v) then:::map f:(\ /x,subst n by:v on:y) env> else: ;; let rec unify *env = /simplify env:env a,simplify env:env b,env:env; \ (Var a),b ; add_env | a,(Var b) ; add_env | (Sym a l),(Sym b m) ; if (a=b && length l = length m) then: else: ;;