Commit c67124fb authored by Francois Bobot's avatar Francois Bobot

petit toilettage

parent aba3c7c3
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Ident
open Theory
open Context
......@@ -107,3 +108,19 @@ let all ?clear f =
let memo_t = Hashtbl.create 16 in
t (memo f ctxt_tag memo_t) clear (fun () -> Hashtbl.clear memo_t)
(* Utils *)
(*type odecl =
| Otype of ty_decl
| Ologic of logic_decl
| Oprop of prop_decl
| Ouse of theory
| Oclone of (ident * ident) list*)
let elt_of_oelt ~ty ~logic ~prop ~use ~clone d =
match d.d_node with
| Dtype l -> [create_type (List.map ty l)]
| Dlogic l -> [create_logic (List.map logic l)]
| Dprop p -> prop p
| Duse th -> use th
| Dclone c -> clone c
......@@ -17,14 +17,15 @@
(* *)
(**************************************************************************)
open Ident
open Theory
(* Tranformation on list of element with some memoisations *)
(* Tranformation on context with some memoisations *)
(* The type of transformation from list of 'a to list of 'b *)
type t
(* compose two transformation, the underlying datastructures for
(* compose two transformations, the underlying datastructures for
the memoisation are shared *)
val compose : t -> t -> t
......@@ -34,15 +35,15 @@ val apply : t -> context -> context
(* clear the datastructures used to store the memoisation *)
val clear : t -> unit
(* The general tranformation only one memoisation is performed with
the argument given *)
(* the general tranformation only one memoisation is performed at the
beginning *)
val all :
?clear:(unit -> unit) ->
(context -> context) -> t
(* map the element of the list from the first to the last.
only one memoisation is performed. But if a tag function is given.
A memoisation is performed at each step *)
(* map the element of the list from the first to the last. only one
memoisation is performed at the beginning. But if a tag function is
given a memoisation is performed at each step *)
val fold_map_bottom :
?tag:('a -> int) ->
?clear:(unit -> unit) ->
......@@ -59,3 +60,19 @@ val fold_map_up :
val elt :
?clear:(unit -> unit) ->
(decl -> decl list) -> t
(*type odecl =
| Otype of ty_decl
| Ologic of logic_decl
| Oprop of prop_decl
| Ouse of theory
| Oclone of (ident * ident) list
*)
val elt_of_oelt :
ty:(ty_decl -> ty_decl) ->
logic:(logic_decl -> logic_decl) ->
prop:(prop_decl -> decl list) ->
use:(theory -> decl list) ->
clone:((ident * ident) list -> decl list) ->
(decl -> decl list)
(* Inline the definition not recursive *)
val t : Transform.t
(* Function to use in other transformations if inlining is needed *)
type env
val empty_env : env
(*val add_decl : env -> Theory.decl -> env *)
val replacet : env -> Term.term -> Term.term
val replacep : env -> Term.fmla -> Term.fmla
......@@ -21,3 +21,8 @@
(* Simplify the recursive type and logic definition *)
val t : Transform.t
(* ungroup recursive definition *)
val elt : Theory.decl -> Theory.decl list
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