home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / Caml Light 0.61 / Binaries / examples / kb / equation.ml next >
Encoding:
Text File  |  1993-09-24  |  2.3 KB  |  89 lines  |  [TEXT/ttxt]
  1. (****************** Equation manipulations *************)
  2.  
  3. #open "prelude";;
  4. #open "terms";;
  5.  
  6. (* standardizes an equation so its variables are 1,2,... *)
  7.  
  8. let mk_rule M N =
  9.   let all_vars = union (vars M) (vars N) in
  10.   let (k,subst) =
  11.     it_list (fun (i,sigma) v -> (i+1,(v,Var(i))::sigma)) (1,[]) all_vars in
  12.   (k-1, (substitute subst M, substitute subst N))
  13. ;;
  14.  
  15. (* checks that rules are numbered in sequence and returns their number *)
  16. let check_rules =
  17.   it_list (fun n (k,_) -> if k=n+1 then k
  18.                           else failwith "Rule numbers not in sequence") 0
  19. ;;
  20.  
  21. let pretty_rule (k,(n,(M,N))) =
  22.   print_int k; print_string " : ";
  23.   pretty_term M; print_string " = "; pretty_term N;
  24.   print_newline()
  25. ;;
  26.  
  27. let pretty_rules = do_list pretty_rule
  28. ;; 
  29.  
  30. (****************** Rewriting **************************)
  31.  
  32. (* Top-level rewriting. Let eq:L=R be an equation, M be a term such that L<=M.
  33.    With sigma = matching L M, we define the image of M by eq as sigma(R) *)
  34. let reduce L M =
  35.   substitute (matching L M)
  36. ;;
  37.  
  38. (* A more efficient version of can (rewrite1 (L,R)) for R arbitrary *)
  39. let reducible L = redrec
  40.   where rec redrec M =
  41.     try
  42.       matching L M; true
  43.     with Failure _ ->
  44.       match M with Term(_,sons) -> exists redrec sons
  45.                 |         _     -> false
  46. ;;
  47.  
  48. (* mreduce : rules -> term -> term *)
  49. let mreduce rules M =
  50.   let redex (_,(_,(L,R))) = reduce L M R in try_find redex rules
  51. ;;
  52.  
  53. (* One step of rewriting in leftmost-outermost strategy, with multiple rules *)
  54. (* fails if no redex is found *)
  55. (* mrewrite1 : rules -> term -> term *)
  56. let mrewrite1 rules = rewrec
  57.   where rec rewrec M =
  58.     try
  59.       mreduce rules M
  60.     with Failure _ ->
  61.       let rec tryrec = function
  62.           [] -> failwith "mrewrite1"
  63.         | son::rest ->
  64.             try
  65.               rewrec son :: rest
  66.             with Failure _ ->
  67.               son :: tryrec rest in
  68.       match M with
  69.           Term(f, sons) -> Term(f, tryrec sons)
  70.         | _ -> failwith "mrewrite1"
  71. ;;
  72.  
  73. (* Iterating rewrite1. Returns a normal form. May loop forever *)
  74. (* mrewrite_all : rules -> term -> term *)
  75. let mrewrite_all rules M = rew_loop M
  76.   where rec rew_loop M =
  77.     try
  78.       rew_loop(mrewrite1 rules M)
  79.     with Failure _ ->
  80.       M
  81. ;;
  82.  
  83. (*
  84. pretty_term (mrewrite_all Group_rules M where M,_=<<A*(I(B)*B)>>);;
  85. ==> A*U
  86. *)
  87.  
  88.  
  89.