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