Commit 1c21c061 authored by Andrei Paskevich's avatar Andrei Paskevich

refactor theory.ml:

- split clone code between contexts and theories

- add [Dclone] declarations after cloned decls

- account for the used theories in [ctxt_known]
  (the hash-consed [Duse] declaration is referenced)

- provide use and clone for contexts with a distinct semantics:

    Context.use_export ctxt th :
        Copies the contents of [th] and its dependencies
        into [ctxt]. The [Duse] declarations are erased
        from the list of decls, but keeped in [ctxt_known],
        so that theories are not copied twice. Useful to
        build flat contexts.

    Context.clone_export ctxt th :
        Clones the contents of [th] into [ctxt]. Dependencies
        of [th] are copied, too. Erases the [Duse] declarations,
        but keeps them in [ctxt_known], so that theories are not
        copied twice. Useful to build flat contexts.

    Theory.use_export uc th :
        Marks the dependency on [th]. [Duse th] is added to [uc],
        unless [th] is already used.

    Theory.clone_export uc th :
        Clones the contents of [th] into [uc]. The dependencies
        of [th] become dependencies of [uc]. [Duse] declarations
        are added, when a theory is used for the first time.
parent 4a1ccfbe
This diff is collapsed.
......@@ -21,7 +21,7 @@ open Ident
open Ty
open Term
(** Theory *)
(** Declarations *)
(* type declaration *)
......@@ -41,6 +41,15 @@ type logic_decl =
| Lpredicate of lsymbol * ps_defn option
| Linductive of lsymbol * (ident * fmla) list
val make_fs_defn : lsymbol -> vsymbol list -> term -> fs_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ps_defn
val open_fs_defn : fs_defn -> lsymbol * vsymbol list * term
val open_ps_defn : ps_defn -> lsymbol * vsymbol list * fmla
val fs_defn_axiom : fs_defn -> fmla
val ps_defn_axiom : ps_defn -> fmla
(* proposition declaration *)
type prop_kind =
......@@ -50,50 +59,44 @@ type prop_kind =
type prop_decl = prop_kind * ident * fmla
(* smart constructors *)
val make_fs_defn : lsymbol -> vsymbol list -> term -> fs_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ps_defn
val open_fs_defn : fs_defn -> lsymbol * vsymbol list * term
val open_ps_defn : ps_defn -> lsymbol * vsymbol list * fmla
val fs_defn_axiom : fs_defn -> fmla
val ps_defn_axiom : ps_defn -> fmla
(** Context and Theory *)
module Snm : Set.S with type elt = string
module Mnm : Map.S with type key = string
type theory = private {
th_name : ident;
th_local : Sid.t; (* locally declared abstract symbols *)
th_export : namespace;
th_ctxt : context;
th_name : ident; (* theory name *)
th_ctxt : context; (* theory declarations *)
th_export : namespace; (* exported namespace *)
th_local : Sid.t; (* locally declared idents *)
}
and namespace = private {
ns_ts : tysymbol Mnm.t; (* type symbols *)
ns_ls : lsymbol Mnm.t; (* logic symbols *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
ns_pr : fmla Mnm.t; (* propositions *)
}
and context = private {
ctxt_tag : int;
ctxt_known : decl Mid.t; (* imported and locally declared symbols *)
ctxt_decls : (decl * context) option;
ctxt_known : decl Mid.t;
ctxt_tag : int;
}
and decl = private {
d_node : decl_node;
d_tag : int;
}
and decl_node =
| Dtype of ty_decl list
| Dlogic of logic_decl list
| Dprop of prop_decl
| Duse of theory
| Duse of theory
| Dclone of (ident * ident) list
and decl = private {
d_node : decl_node;
d_tag : int;
}
and namespace = private {
ns_ts : tysymbol Mnm.t; (* type symbols *)
ns_ls : lsymbol Mnm.t; (* logic symbols *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
ns_pr : fmla Mnm.t; (* propositions *)
}
(** Declaration constructors *)
val create_type : ty_decl list -> decl
val create_logic : logic_decl list -> decl
......@@ -109,51 +112,57 @@ exception IllegalConstructor of lsymbol
exception UnboundVars of Svs.t
exception BadDecl of ident
(* context *)
(** Context constructors and utilities *)
type th_inst = {
inst_ts : tysymbol Mts.t;
inst_ls : lsymbol Mls.t;
}
module Context : sig
val empty_context : context
val add_decl : context -> decl -> context
val iter : (decl -> unit) -> context -> unit
(** bottom-up, tail-rec *)
val fold_left : ('a -> decl -> 'a) -> 'a -> context -> 'a
(** bottom-up, tail-rec *)
end
val use_export : context -> theory -> context
val clone_export : context -> theory -> th_inst -> context
(* theory construction *)
val ctxt_fold : ('a -> decl -> 'a) -> 'a -> context -> 'a
val ctxt_iter : (decl -> unit) -> context -> unit
type theory_uc (* a theory under construction *)
val get_decls : context -> decl list (* top-down list of decls *)
val create_theory : preid -> theory_uc
exception UnknownIdent of ident
exception RedeclaredIdent of ident
exception CannotInstantiate of ident
val close_theory : theory_uc -> theory
end
val open_namespace : theory_uc -> theory_uc
(** Theory constructors and utilities *)
val close_namespace : theory_uc -> string -> import:bool -> theory_uc
type theory_uc (* a theory under construction *)
val add_decl : theory_uc -> decl -> theory_uc
module Theory : sig
val use_export : theory_uc -> theory -> theory_uc
val create_theory : preid -> theory_uc
val close_theory : theory_uc -> theory
type th_inst = {
inst_ts : tysymbol Mts.t;
inst_ls : lsymbol Mls.t;
}
val add_decl : theory_uc -> decl -> theory_uc
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val open_namespace : theory_uc -> theory_uc
val close_namespace : theory_uc -> string -> import:bool -> theory_uc
val get_namespace : theory_uc -> namespace
val use_export : theory_uc -> theory -> theory_uc
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
(* exceptions *)
val get_namespace : theory_uc -> namespace
exception CloseTheory
exception NoOpenedNamespace
exception ClashSymbol of string
exception CloseTheory
exception NoOpenedNamespace
exception RedeclaredIdent of ident
exception CannotInstantiate of ident
exception ClashSymbol of string
end
(** Debugging *)
......
......@@ -31,31 +31,31 @@ sig
end
(* The datastructure for hashconsed list *)
module LH (X:Sig) =
module LH (X:Sig) =
struct
module L =
struct
type t = X.t hashconsedlist
let equal a b =
let equal a b =
match a,b with
| [], [] -> true
| [], _ | _, [] -> false
(* work evenif al and bl are nil *)
| (_,ae::_)::al,(_,be::_)::bl -> X.tag ae = X.tag be && al == bl
| (_,[])::_,_ | _,(_,[])::_ -> assert false
let hash a =
| (_,[])::_,_ | _,(_,[])::_ -> assert false
let hash a =
match a with
| [] -> 0
| (_,[ae])::[] -> X.tag ae
| _::[] -> assert false
| (_,ae::_)::(at,_)::_ -> Hashcons.combine (X.tag ae) at
| (_,[])::_ -> assert false
| (_,[])::_ -> assert false
let tag t = function
| [] -> []
| (_,lae)::al -> (t,lae)::al
end
module LH = Hashcons.Make(L)
type t = L.t
let empty : t = []
......@@ -66,8 +66,8 @@ struct
let to_list t : X.t list = match t with
| [] -> []
| (_,l)::_ -> l
let from_list = List.fold_left (fun t e -> cons e t) empty
let from_list = List.fold_left (fun t e -> cons e t) empty
let fold_left f acc l =
List.fold_left (fun acc l -> match l with
......@@ -78,7 +78,7 @@ struct
let tag = function
| [] -> -1
| (t,_)::_ -> t
end
......@@ -95,12 +95,12 @@ let compose f g = {all = (fun x -> g.all (f.all x));
to_list = g.to_list}
let apply f x = (List.rev (f.to_list (f.all (f.from_list x))))
let clear f = f.clear ()
let memo f tag h x =
try Hashtbl.find h (tag x:int)
with Not_found ->
with Not_found ->
let r = f x in
Hashtbl.add h (tag x) r;
r
......@@ -125,51 +125,51 @@ struct
module LH1 = LH(X1)
module LH2 = LH(X2)
let memo_to_list2 h : X2.t hashconsedlist -> X2.t list =
let memo_to_list2 h : X2.t hashconsedlist -> X2.t list =
memo LH2.to_list LH2.tag h
let t all clear =
let t all clear =
let h_to_list = Hashtbl.create 16 in
{all = all;
clear = clear;
from_list = LH1.from_list;
to_list = memo_to_list2 h_to_list
}
}
let fold_map_left f_fold v_empty =
let memo_t = Hashtbl.create 64 in
let rewind edonev eltss =
let edone,_ = List.fold_left
(fun (edone,v) (tag,elts) ->
let rewind edonev eltss =
let edone,_ = List.fold_left
(fun (edone,v) (tag,elts) ->
let v,l = f_fold v elts in
let edone = List.fold_left (fun e t -> LH2.cons t e) edone l in
Hashtbl.add memo_t tag (edone,v);
(edone,v)) edonev eltss in
edone in
let rec f acc t1 =
let rec f acc t1 =
match t1 with
| [] -> rewind (LH2.empty,v_empty) acc
| (_,[])::_ -> assert false
| (tag,e::_)::t2 ->
try
| (tag,e::_)::t2 ->
try
let edonev = Hashtbl.find memo_t tag in
rewind edonev acc
with Not_found -> f ((tag,e)::acc) t2
with Not_found -> f ((tag,e)::acc) t2
in
t (f []) (fun () -> Hashtbl.clear memo_t)
let elt f_elt =
let elt f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt () x = (),memo f_elt X1.tag memo_elt x in
let f = fold_map_left f_elt () in
{f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
let fold_map_right f_fold v_empty =
let rec f (acc,v) t =
let rec f (acc,v) t =
match t with
| [] -> List.fold_left (List.fold_left (fun t e -> LH2.cons e t)) LH2.empty acc
| (_,[])::_ -> assert false
| (_,e::_)::t ->
| (_,[])::_ -> assert false
| (_,e::_)::t ->
let v,res = f_fold v e in
f (res::acc,v) t in
let memo_t = Hashtbl.create 16 in
......@@ -195,7 +195,7 @@ module SDecl =
module STheory =
struct
type t = theory
let tag t = t.th_name.Ident.id_tag
let tag t = t.th_name.Ident.id_tag
end
module STerm =
......
......@@ -26,10 +26,10 @@ type ('a,'b) t
(* compose two transformation, the underlying datastructures for
the memoisation are shared *)
val compose : ('a,'b) t -> ('b,'c) t -> ('a,'c) t
(* apply a transformation and memoise *)
val apply : ('a,'b) t -> 'a list -> 'b list
(* clear the datastructures used to store the memoisation *)
val clear : ('a,'b) t -> unit
......@@ -55,7 +55,7 @@ sig
(* map the element of the list without an environnment.
A memoisation is performed at each step, and for each elements *)
val elt : (t1 -> t2 list) -> (t1,t2) t
end
(* a type with a tag function *)
......
......@@ -26,6 +26,8 @@ open Term
open Ptree
open Theory
open Theory
(** errors *)
type error =
......
......@@ -171,7 +171,7 @@ let print_decl fmt d = match d.d_node with
let print_decl_list fmt de =
fprintf fmt "@[<hov>%a@]" (print_list newline print_decl) de
let print_ctxt = print_iter1 Context.iter newline print_decl
let print_ctxt = print_iter1 Context.ctxt_iter newline print_decl
let print_theory fmt t =
fprintf fmt "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n" print_ident t.th_name
......
......@@ -4,7 +4,7 @@ open Theory
let elt a =
let rec aux acc d = match d.d_node with
| Duse t -> Context.fold_left aux (d::acc) t.th_ctxt
| Duse t -> Context.ctxt_fold aux (d::acc) t.th_ctxt
| _ -> d::acc
in List.rev (aux [] a)
......
......@@ -26,6 +26,8 @@ let of_option = function Some v -> v | None -> assert false
let option_map f = function None -> None | Some x -> Some (f x)
let option_iter f = function None -> () | Some x -> f x
exception FoldSkip
let all_fn pr _ t = pr t || raise FoldSkip
......
......@@ -21,6 +21,8 @@ val of_option : 'a option -> 'a
val option_map : ('a -> 'b) -> 'a option -> 'b option
val option_iter : ('a -> unit) -> 'a option -> unit
exception FoldSkip
val all_fn : ('a -> bool) -> 'b -> 'a -> bool
......
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