← Back to branch summary

~ubuntu-branches/ubuntu/hardy/ocaml-doc/hardy

« back to all changes in this revision

Viewing changes to examples/kb/terms.ml

  • Committer: Bazaar Package Importer
  • Author(s): Samuel Mimram
  • Date: 2007-09-08 01:49:22 UTC
  • mfrom: (0.1.3 upstream)
  • Revision ID: james.westby@ubuntu.com-20070908014922-lvihyehz0ndq7suu
Tags: 3.10-1
* New upstream release.
* Removed camlp4 documentation since it is not up-to-date.
* Updated to standards version 3.7.2, no changes needed.
* Updated my email address.

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/kb/terms.ml
1
 
(****************** Term manipulations *****************)
2
 
open Prelude;;
3
 
 
4
 
type term =
5
 
   | Var of int
6
 
   | Term of string * term list;;
7
 
 
8
 
let rec vars = function
9
 
  | Var n -> [n]
10
 
  | Term (_, l) -> vars_of_list l
11
 
and vars_of_list = function
12
 
  | [] -> []
13
 
  | t :: r -> union (vars t) (vars_of_list r)
14
 
;;
15
 
 
16
 
let substitute subst =
17
 
  let rec subst_rec = function
18
 
  | Term (oper, sons) -> Term (oper, List.map subst_rec sons)
19
 
  | Var (n) as t      -> try List.assoc n subst with Not_found -> t in
20
 
  subst_rec
21
 
;;
22
 
 
23
 
let change f =
24
 
  let rec change_rec l n =
25
 
  match l with
26
 
  | h :: t -> if n = 1 then f h :: t else h :: change_rec t (n - 1)
27
 
  | _ -> failwith "change" in
28
 
  change_rec
29
 
;;
30
 
 
31
 
(* Term replacement replace m u n => m[u<-n] *)
32
 
let replace m u n =
33
 
  let rec reprec = function
34
 
  | _, [] -> n
35
 
  | Term (oper, sons), (n :: u) ->
36
 
             Term (oper, change (fun p -> reprec (p, u)) sons n)
37
 
  | _ -> failwith "replace" in
38
 
 reprec (m, u)
39
 
;;
40
 
 
41
 
(* matching = - : (term -> term -> subst) *)
42
 
let matching term1 term2 =
43
 
  let rec match_rec subst t1 t2 =
44
 
    match t1, t2 with
45
 
    | Var v, m ->
46
 
        if List.mem_assoc v subst then
47
 
          if m = List.assoc v subst then subst else failwith "matching"
48
 
        else
49
 
          (v,t2) :: subst
50
 
    | Term (op1, sons1), Term (op2, sons2) ->
51
 
        if op1 = op2 then List.fold_left2 match_rec subst sons1 sons2
52
 
                     else failwith "matching"
53
 
    | _, _ ->
54
 
        failwith "matching" in
55
 
  match_rec [] term1 term2
56
 
;;
57
 
 
58
 
(* A naive unification algorithm *)
59
 
 
60
 
let compsubst subst1 subst2 = 
61
 
  (List.map (fun (v, t) -> (v, substitute subst1 t)) subst2) @ subst1
62
 
;;
63
 
 
64
 
let occurs n =
65
 
  let rec occur_rec = function
66
 
  | Var m -> m=n
67
 
  | Term (_, sons) -> List.exists occur_rec sons in
68
 
  occur_rec
69
 
;;
70
 
 
71
 
let rec unify = function
72
 
  | (Var n1 as term1), term2 ->
73
 
      if term1 = term2 then []
74
 
      else if occurs n1 term2 then failwith "unify1"
75
 
      else [n1,term2]
76
 
  | term1, Var n2 ->
77
 
      if occurs n2 term1 then failwith "unify2"
78
 
      else [n2,term1]
79
 
  | Term (op1, sons1), Term (op2, sons2) ->
80
 
      if op1 = op2 then 
81
 
        List.fold_left2 (fun s t1 t2 -> compsubst (unify (substitute s t1,
82
 
                                                   substitute s t2)) s)
83
 
                 [] sons1 sons2
84
 
      else failwith "unify3"
85
 
;;
86
 
 
87
 
(* We need to print terms with variables independently from input terms
88
 
  obtained by parsing. We give arbitrary names v1,v2,... to their variables. *)
89
 
 
90
 
let infixes = ["+";"*";"-";"/"];;
91
 
 
92
 
let rec pretty_term = function
93
 
  | Var n ->
94
 
      print_string "v"; print_int n
95
 
  | Term (oper, sons) ->
96
 
      if List.mem oper infixes then
97
 
        match sons with
98
 
          | [s1;s2] ->
99
 
              pretty_close s1; print_string oper; pretty_close s2
100
 
          | _ ->
101
 
              failwith "pretty_term : infix arity <> 2"
102
 
      else
103
 
       (print_string oper;
104
 
        match sons with
105
 
          |  []   -> ()
106
 
          | t::lt -> print_string "(";
107
 
                     pretty_term t;
108
 
                     List.iter (fun t -> print_string ","; pretty_term t) lt;
109
 
                     print_string ")")
110
 
and pretty_close = function
111
 
  | Term (oper, _) as m ->
112
 
      if List.mem oper infixes then
113
 
        (print_string "("; pretty_term m; print_string ")")
114
 
      else pretty_term m
115
 
  | m -> pretty_term m
116
 
;;
117