Commit a3749c0b authored by MARCHE Claude's avatar MARCHE Claude

transf compute: comments in .mli

parent 367307fe
...@@ -4,6 +4,8 @@ open Decl ...@@ -4,6 +4,8 @@ open Decl
open Task open Task
open Theory open Theory
(* obsolete
type env = { type env = {
tknown : Decl.known_map; tknown : Decl.known_map;
vsenv : term Mvs.t; vsenv : term Mvs.t;
...@@ -328,7 +330,7 @@ let () = ...@@ -328,7 +330,7 @@ let () =
(fun env -> Trans.store (compute env)) (fun env -> Trans.store (compute env))
~desc:"Compute@ as@ much@ as@ possible" ~desc:"Compute@ as@ much@ as@ possible"
*)
(* compute with rewrite rules *) (* compute with rewrite rules *)
......
...@@ -68,15 +68,30 @@ terms are normalized with respect to ...@@ -68,15 +68,30 @@ terms are normalized with respect to
*) *)
type engine type engine
(** abstract type for reduction engines *)
val create : Env.env -> Decl.decl Ident.Mid.t -> engine 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 exception NotARewriteRule of string
val add_rule : Term.term -> engine -> engine 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 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 non-termination...
*)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment