Commit f0218f41 authored by Andrei Paskevich's avatar Andrei Paskevich

"I want to believe" commit.

Not only Theory, but also Task and Transformation 
do not need to depend on environment. Moreover,
we don't have to track the clone history in tasks.

The only thing we need to do, is to provide three
registration functions in Driver, namely:

  val register_transform : string -> (unit -> task_t) -> unit
  val register_transform_env : string -> (env -> task_t) -> unit
  val register_transform_clone : string -> (env -> clone -> task_t) -> unit

and then another three for task_list_t.

Then any particular transformation that is going to depend
on environment or clone_history, must register itself via
the appropriate registration function. It will be the
responsibility of Driver to recreate the transformation
for every new environment and/or clone history. It will
be easy, given that both [env] and [clone] are physically
comparable and provide a unique tag.

Thus, the generic interface provided by Transform can be
completely independent on [env] and [clone].

This commit implements the proposed interface of Task
and moves the environment stuff into a separate module.
parent 5f6f38a8
......@@ -117,8 +117,8 @@ doc/version.tex src/version.ml: Version version.sh config.status
# why
#####
CORE_CMO := ident.cmo ty.cmo term.cmo decl.cmo\
theory2.cmo task.cmo theory.cmo pretty.cmo
CORE_CMO := ident.cmo ty.cmo term.cmo decl.cmo theory2.cmo\
task.cmo env.cmo theory.cmo pretty.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo\
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
open Theory2
(** Environment *)
type env = {
env_retrieve : retrieve_theory;
env_memo : (string list, theory Mnm.t) Hashtbl.t;
env_tag : int;
}
and retrieve_theory = env -> string list -> theory Mnm.t
let create_env =
let r = ref 0 in
fun retrieve ->
incr r;
let env = {
env_retrieve = retrieve;
env_memo = Hashtbl.create 17;
env_tag = !r }
in
let th = builtin_theory in
let m = Mnm.add th.th_name.id_short th Mnm.empty in
Hashtbl.add env.env_memo [] m;
env
exception TheoryNotFound of string list * string
let find_theory env sl s =
let m =
try
Hashtbl.find env.env_memo sl
with Not_found ->
Hashtbl.add env.env_memo sl Mnm.empty;
let m = env.env_retrieve env sl in
Hashtbl.replace env.env_memo sl m;
m
in
try Mnm.find s m
with Not_found -> raise (TheoryNotFound (sl, s))
let env_tag env = env.env_tag
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Theory2
(** Environment *)
type env
type retrieve_theory = env -> string list -> theory Mnm.t
val create_env : retrieve_theory -> env
val find_theory : env -> string list -> string -> theory
val env_tag : env -> int
exception TheoryNotFound of string list * string
......@@ -26,46 +26,29 @@ open Termlib
open Decl
open Theory2
(** Environment *)
(** Cloning map *)
type clone = {
cl_map : clone_map;
cl_tag : int
}
type env = {
env_retrieve : retrieve_theory;
env_memo : (string list, theory Mnm.t) Hashtbl.t;
env_tag : int;
let empty_clone = {
cl_map = Mid.empty;
cl_tag = 0;
}
and retrieve_theory = env -> string list -> theory Mnm.t
let cloned_from cl i1 i2 =
try i1 = i2 || Sid.mem i2 (Mid.find i1 cl.cl_map)
with Not_found -> false
let create_env =
let add_clone =
let r = ref 0 in
fun retrieve ->
fun cl th sl ->
incr r;
let env = {
env_retrieve = retrieve;
env_memo = Hashtbl.create 17;
env_tag = !r }
in
let th = builtin_theory in
let m = Mnm.add th.th_name.id_short th Mnm.empty in
Hashtbl.add env.env_memo [] m;
env
exception TheoryNotFound of string list * string
let find_theory env sl s =
let m =
try
Hashtbl.find env.env_memo sl
with Not_found ->
Hashtbl.add env.env_memo sl Mnm.empty;
let m = env.env_retrieve env sl in
Hashtbl.replace env.env_memo sl m;
m
in
try Mnm.find s m
with Not_found -> raise (TheoryNotFound (sl, s))
{ cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
let env_tag env = env.env_tag
let clone_tag cl = cl.cl_tag
(** Known identifiers *)
......@@ -100,17 +83,52 @@ let add_known id decl kn =
raise DejaVu
with Not_found -> Mid.add id decl kn
let add_constr d kn fs = add_known fs.ls_name d kn
(** Cloning map *)
let add_type d kn (ts,def) =
let kn = add_known ts.ts_name d kn in
match def with
| Tabstract -> kn
| Talgebraic lfs -> List.fold_left (add_constr d) kn lfs
type clone = {
cl_map : Sid.t Mid.t;
cl_tag : int
}
let check_type kn (ts,def) =
let check_constr fs = List.iter (known_ty kn) fs.ls_args in
match def with
| Tabstract -> option_iter (known_ty kn) ts.ts_def
| Talgebraic lfs -> List.iter check_constr lfs
let cloned_from cl i1 i2 =
try i1 = i2 || Sid.mem i2 (Mid.find i1 cl.cl_map)
with Not_found -> false
let add_logic d kn (ls,_) = add_known ls.ls_name d kn
let check_ls_defn kn ld =
let _,e = open_ls_defn ld in
e_apply (known_term kn) (known_fmla kn) e
let check_logic kn (ls,ld) =
List.iter (known_ty kn) ls.ls_args;
option_iter (known_ty kn) ls.ls_value;
option_iter (check_ls_defn kn) ld
let add_ind d kn (ps,la) =
let kn = add_known ps.ls_name d kn in
let add kn (pr,_) = add_known (pr_name pr) d kn in
List.fold_left add kn la
let check_ind kn (ps,la) =
List.iter (known_ty kn) ps.ls_args;
let check (_,f) = known_fmla kn f in
List.iter check la
let add_decl kn d = match d.d_node with
| Dtype dl -> List.fold_left (add_type d) kn dl
| Dlogic dl -> List.fold_left (add_logic d) kn dl
| Dind dl -> List.fold_left (add_ind d) kn dl
| Dprop (_,pr,_) -> add_known (pr_name pr) d kn
let check_decl kn d = match d.d_node with
| Dtype dl -> List.iter (check_type kn) dl
| Dlogic dl -> List.iter (check_logic kn) dl
| Dind dl -> List.iter (check_ind kn) dl
| Dprop (_,_,f) -> known_fmla kn f
(** Task *)
......@@ -119,8 +137,6 @@ type task = {
task_decl : decl;
task_prev : task option;
task_known : decl Mid.t;
task_clone : clone;
task_env : env;
task_tag : int;
}
......@@ -128,9 +144,7 @@ module Task = struct
type t = task
let equal a b =
a.task_decl == b.task_decl &&
a.task_clone == b.task_clone &&
a.task_env == b.task_env &&
a.task_decl == b.task_decl &&
match a.task_prev, b.task_prev with
| Some na, Some nb -> na == nb
| None, None -> true
......@@ -141,81 +155,86 @@ module Task = struct
| Some task -> 1 + task.task_tag
| None -> 0
in
let hs = Hashcons.combine task.task_decl.d_tag prev in
Hashcons.combine2 hs task.task_env.env_tag task.task_clone.cl_tag
Hashcons.combine task.task_decl.d_tag prev
let tag i task = { task with task_tag = i }
end
module Htask = Hashcons.Make(Task)
let mk_task decl prev known clone env = Htask.hashcons {
let mk_task decl prev known = Htask.hashcons {
task_decl = decl;
task_prev = prev;
task_known = known;
task_clone = clone;
task_env = env;
task_tag = -1;
}
let push_decl task kn d =
mk_task d (Some task) kn task.task_clone task.task_env
(* Add declarations to a task *)
let add_constr d kn fs = add_known fs.ls_name d kn
let add_type d kn (ts,def) =
let kn = add_known ts.ts_name d kn in
match def with
| Tabstract -> kn
| Talgebraic lfs -> List.fold_left (add_constr d) kn lfs
let check_type kn (ts,def) =
let check_constr fs = List.iter (known_ty kn) fs.ls_args in
match def with
| Tabstract -> option_iter (known_ty kn) ts.ts_def
| Talgebraic lfs -> List.iter check_constr lfs
let add_logic d kn (ls,_) = add_known ls.ls_name d kn
let check_ls_defn kn ld =
let _,e = open_ls_defn ld in
e_apply (known_term kn) (known_fmla kn) e
let check_logic kn (ls,ld) =
List.iter (known_ty kn) ls.ls_args;
option_iter (known_ty kn) ls.ls_value;
option_iter (check_ls_defn kn) ld
let add_ind d kn (ps,la) =
let kn = add_known ps.ls_name d kn in
let add kn (pr,_) = add_known (pr_name pr) d kn in
List.fold_left add kn la
let init_task =
let add opt td =
let known task = task.task_known in
let kn = option_apply Mid.empty known opt in
match td with
| Decl d -> Some (mk_task d opt (add_decl kn d))
| _ -> opt
in
List.fold_left add None builtin_theory.th_decls
let check_ind kn (ps,la) =
List.iter (known_ty kn) ps.ls_args;
let check (_,f) = known_fmla kn f in
List.iter check la
let init_task = of_option init_task
let add_decl task d =
try
let kn = task.task_known in
let kn = match d.d_node with
| Dtype dl -> List.fold_left (add_type d) kn dl
| Dlogic dl -> List.fold_left (add_logic d) kn dl
| Dind dl -> List.fold_left (add_ind d) kn dl
| Dprop (_,pr,_) -> add_known (pr_name pr) d kn
in
let () = match d.d_node with
| Dtype dl -> List.iter (check_type kn) dl
| Dlogic dl -> List.iter (check_logic kn) dl
| Dind dl -> List.iter (check_ind kn) dl
| Dprop (_,_,f) -> known_fmla kn f
in
push_decl task kn d
let kn = add_decl kn d in
ignore (check_decl kn d);
mk_task d (Some task) kn
with DejaVu ->
task
let rec use_export names acc td =
let used, cl, res, task = acc in
match td with
| Use th when Sid.mem th.th_name used ->
acc
| Use th ->
let used = Sid.add th.th_name used in
let acc = used, cl, res, task in
let names = Some Spr.empty in
List.fold_left (use_export names) acc th.th_decls
| Clone (th,sl) ->
let cl = add_clone cl th sl in
used, cl, res, task
| Decl d ->
begin match d.d_node with
| Dprop (Pgoal,pr,_)
when option_apply true (Spr.mem pr) names ->
let res = (add_decl task d, cl) :: res in
used, cl, res, task
| Dprop (Pgoal,_,_) ->
acc
| Dprop (Plemma,pr,f)
when option_apply true (Spr.mem pr) names ->
let d = create_prop_decl Pgoal pr f in
let res = (add_decl task d, cl) :: res in
let d = create_prop_decl Paxiom pr f in
used, cl, res, add_decl task d
| Dprop (Plemma,pr,f) ->
let d = create_prop_decl Paxiom pr f in
used, cl, res, add_decl task d
| Dprop (Paxiom,_,_) ->
used, cl, res, add_decl task d
| Dtype _ | Dlogic _ | Dind _ ->
used, cl, res, add_decl task d
end
let split_theory_opt th names =
let acc = Sid.empty, empty_clone, [], init_task in
let _, _, res, _ =
List.fold_left (use_export names) acc th.th_decls
in
res
let split_theory th names = split_theory_opt th (Some names)
let split_theory_full th = split_theory_opt th None
(* Generic utilities *)
let rec task_fold fn acc task =
......
......@@ -23,48 +23,39 @@ open Term
open Decl
open Theory2
(** Environment *)
type env
type retrieve_theory = env -> string list -> theory Mnm.t
val create_env : retrieve_theory -> env
val find_theory : env -> string list -> string -> theory
val env_tag : env -> int
exception TheoryNotFound of string list * string
(** Cloning map *)
type clone = private {
cl_map : Sid.t Mid.t;
cl_tag : int
}
type clone
val cloned_from : clone -> ident -> ident -> bool
val clone_tag : clone -> int
(** Task *)
type task = private {
task_decl : decl;
task_prev : task option;
task_known : decl Mid.t;
task_clone : clone;
task_env : env;
task_tag : int;
}
(* constructors *)
val init_task : task
val add_decl : task -> decl -> task
val split_theory : theory -> Spr.t -> (task * clone) list
val split_theory_full : theory -> (task * clone) list
(* bottom-up, tail-recursive traversal functions *)
val task_fold : ('a -> decl -> 'a) -> 'a -> task -> 'a
val task_iter : (decl -> unit) -> task -> unit
(* top-down list of declarations *)
val task_decls : task -> decl list
(* exceptions *)
......
......@@ -83,6 +83,7 @@ type theory = {
th_name : ident; (* theory name *)
th_decls : tdecl list; (* theory declarations *)
th_export : namespace; (* exported namespace *)
th_clone : clone_map; (* cloning history *)
th_local : Sid.t; (* locally declared idents *)
}
......@@ -91,6 +92,7 @@ and tdecl =
| Use of theory
| Clone of theory * (ident * ident) list
and clone_map = Sid.t Mid.t
let builtin_theory =
let decl_int = create_ty_decl [ts_int, Tabstract] in
......@@ -98,13 +100,6 @@ let builtin_theory =
let decl_equ = create_logic_decl [ps_equ, None] in
let decl_neq = create_logic_decl [ps_neq, None] in
(*
let kn_int = Mid.add ts_int.ts_name decl_int Mid.empty in
let kn_real = Mid.add ts_real.ts_name decl_real kn_int in
let kn_equ = Mid.add ps_equ.ls_name decl_equ kn_real in
let kn_neq = Mid.add ps_neq.ls_name decl_neq kn_equ in
*)
let decls = [ Decl decl_int; Decl decl_real;
Decl decl_equ; Decl decl_neq ] in
......@@ -119,6 +114,7 @@ let builtin_theory =
{ th_name = id_register (id_fresh "BuiltIn");
th_decls = decls;
th_export = export;
th_clone = Mid.empty;
th_local = Sid.empty }
......@@ -129,6 +125,7 @@ type theory_uc = {
uc_decls : tdecl list;
uc_import : namespace list;
uc_export : namespace list;
uc_clone : Sid.t Mid.t;
uc_local : Sid.t;
}
......@@ -140,6 +137,7 @@ let create_theory n =
uc_decls = [Use builtin_theory];
uc_import = [builtin_theory.th_export];
uc_export = [builtin_theory.th_export];
uc_clone = Mid.empty;
uc_local = Sid.empty; }
let close_theory uc = match uc.uc_export with
......@@ -147,6 +145,7 @@ let close_theory uc = match uc.uc_export with
{ th_name = uc.uc_name;
th_decls = List.rev uc.uc_decls;
th_export = e;
th_clone = uc.uc_clone;
th_local = uc.uc_local; }
| _ ->
raise CloseTheory
......@@ -217,6 +216,18 @@ let add_decl uc d =
in
{ uc with uc_decls = Decl d :: uc.uc_decls }
let merge_clone cl th sl =
let get m id = try Mid.find id m with Not_found -> Sid.empty in
let add m m' (id,id') =
Mid.add id' (Sid.add id (Sid.union (get m id) (get m' id'))) m'
in
List.fold_left (add th.th_clone) cl sl
let add_clone uc th sl =
let decls = Clone (th,sl) :: uc.uc_decls in
let clone = merge_clone uc.uc_clone th sl in
{ uc with uc_decls = decls; uc_clone = clone }
(** Clone *)
......@@ -420,32 +431,30 @@ let cl_add_decl cl inst d = match d.d_node with
let pr',f' = cl_new_prop cl (pr,f) in
Some (create_prop_decl k' pr' f')
let cl_add_tdecl add_tdecl cl inst acc td = match td with
let cl_add_tdecl cl inst uc td = match td with
| Decl d ->
let od = cl_add_decl cl inst d in
let td = option_map (fun d -> Decl d) od in
option_apply acc (add_tdecl acc) td
| Use _ | Clone _ ->
add_tdecl acc td
let clone_theory add_tdecl acc th inst =
let cl = cl_init th inst in
let clone = cl_add_tdecl add_tdecl cl inst in
let acc = List.fold_left clone acc th.th_decls in
let add_idid id id' acc = (id,id') :: acc in
let d = Clone (th, Hid.fold add_idid cl.id_table []) in
add_tdecl acc d
let decls = match cl_add_decl cl inst d with
| Some d -> Decl d :: uc.uc_decls
| None -> uc.uc_decls
in
{ uc with uc_decls = decls }
| Use _ ->
{ uc with uc_decls = td :: uc.uc_decls }
| Clone (th,sl) ->
add_clone uc th sl
let clone_export uc th inst =
let cl = cl_init th inst in
let add_tdecl acc td = td :: acc in
let clone = cl_add_tdecl add_tdecl cl inst in
let decls = List.fold_left clone uc.uc_decls th.th_decls in
let add_tdecl = cl_add_tdecl cl inst in
let uc = List.fold_left add_tdecl uc th.th_decls in
let add_idid id id' acc = (id,id') :: acc in
let decls = Clone (th, Hid.fold add_idid cl.id_table []) :: decls in
let sl = Hid.fold add_idid cl.id_table [] in
let uc = add_clone uc th sl in
let add_local id' () acc = Sid.add id' acc in
let local = Hid.fold add_local cl.nw_local uc.uc_local in
let lc = Hid.fold add_local cl.nw_local uc.uc_local in
let uc = { uc with uc_local = lc } in
let find_ts ts =
if Sid.mem ts.ts_name th.th_local
......@@ -476,9 +485,7 @@ let clone_export uc th inst =
match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste -> { uc with
uc_import = merge_ns false ns i0 :: sti;
uc_export = merge_ns true ns e0 :: ste;
uc_local = local;
uc_decls = decls }
uc_export = merge_ns true ns e0 :: ste; }
| _ ->
assert false
......@@ -47,6 +47,7 @@ type theory = private {
th_name : ident; (* theory name *)
th_decls : tdecl list; (* theory declarations *)
th_export : namespace; (* exported namespace *)
th_clone : clone_map; (* cloning history *)
th_local : Sid.t; (* locally declared idents *)
}
......@@ -55,6 +56,8 @@ and tdecl = private
| Use of theory
| Clone of theory * (ident * ident) list
and clone_map = Sid.t Mid.t
val builtin_theory : theory
(** Constructors and utilities *)
......@@ -85,6 +88,8 @@ val empty_inst : th_inst
val use_export : theory_uc -> theory -> theory_uc
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val merge_clone : clone_map -> theory -> (ident * ident) list -> clone_map
(* exceptions *)
exception NonLocal of ident
......
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