From a3749c0b8d31e542bcf8fb43c7496a7e5aae6660 Mon Sep 17 00:00:00 2001
From: Claude Marche
Date: Tue, 19 Aug 2014 16:24:36 +0200
Subject: [PATCH] transf compute: comments in .mli

src/transform/compute.ml  4 +++
src/transform/reduction_engine.mli  15 +++++++++++++++
2 files changed, 18 insertions(+), 1 deletion()
diff git a/src/transform/compute.ml b/src/transform/compute.ml
index a0220889c..63b74cbcf 100644
 a/src/transform/compute.ml
+++ b/src/transform/compute.ml
@@ 4,6 +4,8 @@ open Decl
open Task
open Theory
+(* obsolete
+
type env = {
tknown : Decl.known_map;
vsenv : term Mvs.t;
@@ 328,7 +330,7 @@ let () =
(fun env > Trans.store (compute env))
~desc:"Compute@ as@ much@ as@ possible"

+ *)
(* compute with rewrite rules *)
diff git a/src/transform/reduction_engine.mli b/src/transform/reduction_engine.mli
index aa45c905e..7d5cebee1 100644
 a/src/transform/reduction_engine.mli
+++ b/src/transform/reduction_engine.mli
@@ 68,15 +68,30 @@ terms are normalized with respect to
*)
type engine
+(** abstract type for reduction engines *)
val create : Env.env > Decl.decl Ident.Mid.t > engine
+(** [create env known_map] creates a reduction engine with
+ . builtins theories (int.Int, etc.) extracted from [env]
+ . known declarations from [known_map]
+ . empty set of rewrite rules
+*)
exception NotARewriteRule of string
val add_rule : Term.term > engine > engine
+(** [add_rule t e] turns [t] into a new rewrite rule and returns the
+ new engine.
+ raise NotARewriteRule if [t] cannot be seen as a rewrite rule
+ according to the general rules given above.
+*)
val normalize : engine > Term.term > Term.term
+(** [normalize e t] normalizes the term [t] with respect to the engine
+ [e]
+ TODO: specify the behavior when nontermination...
+*)

GitLab