Commit d993dad4 authored by Andrei Paskevich's avatar Andrei Paskevich

Task: use "Use" to represent theory use

up to this point, we used Clone declarations with an empty substitution
to represent use of theories in tasks. The intention was to stress the
fact that the imported declarations are physically present in the task
and thus are followed by a "witness" Clone declaration (whereas a Use
inside a theory acts rather as a pointer to follow).

However, this encoding requires the clone substitution to cover every
locally defined symbol: otherwise we might not be able to distinguish
a use from a clone. Therefore, we had to clone even Pgoal propositions
as Pskip, in order to keep the substitutions complete.

This commit restricts the Clone declarations in tasks to actual
theory cloning, and represents theory use with Use declarations.
This hopefully makes the API more clear, and will allow us to
abolish Pskip.
parent 895898dc
......@@ -457,8 +457,6 @@ let print_tdecl fmt td = match td.td_node with
print_decl fmt d
| Use th ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_qt th
| Clone (th,sm) when is_empty_sm sm ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_qt th
| Clone (th,sm) ->
let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
let lm = Mls.fold (fun x y a -> (x,y)::a) sm.sm_ls [] in
......
......@@ -70,7 +70,7 @@ and task_hd = {
task_decl : tdecl; (* last declaration *)
task_prev : task; (* context *)
task_known : known_map; (* known identifiers *)
task_clone : clone_map; (* cloning history *)
task_clone : clone_map; (* use/clone history *)
task_meta : meta_map; (* meta properties *)
task_tag : Weakhtbl.tag; (* unique magical tag *)
}
......@@ -139,7 +139,6 @@ let task_separate_goal = function
goal,task
| _ -> raise GoalNotFound
let check_task task = match find_goal task with
| Some _ -> raise GoalFound
| None -> task
......@@ -176,23 +175,29 @@ let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)
(* task constructors *)
let rec add_tdecl task td = match td.td_node with
let add_tdecl task td = match td.td_node with
| Decl d -> new_decl task d td
| Use th -> use_export task th
| Use th ->
if Stdecl.mem td (find_clone_tds task th).tds_set then task else
new_clone task th td
| Clone (th,_) -> new_clone task th td
| Meta (t,_) -> new_meta task t td
and flat_tdecl task td = match td.td_node with
let rec flat_tdecl task td = match td.td_node with
| Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
| Decl { d_node = Dprop ((Pgoal|Pskip),_,_) } -> task
| _ -> add_tdecl task td
| Decl d -> new_decl task d td
| Use th -> use_export task th td
| Clone (th,_) -> new_clone task th td
| Meta (t,_) -> new_meta task t td
and use_export task th =
let td = create_null_clone th in
and use_export task th td =
if Stdecl.mem td (find_clone_tds task th).tds_set then task else
let task = List.fold_left flat_tdecl task th.th_decls in
new_clone task th td
let use_export task th = use_export task th (create_use th)
let clone_export = clone_theory flat_tdecl
let add_meta task t al = new_meta task t (create_meta t al)
......@@ -227,13 +232,19 @@ let task_decls = task_fold (fun acc td ->
(* Realization utilities *)
let check_use td = match td.td_node with
| Use _ -> true
| Clone _ -> false
| _ -> assert false
let used_theories task =
let used { tds_set = s } =
let th = match Mtdecl.choose s with
| { td_node = Clone (th,_) }, _ -> th
| _ -> assert false in
let td = create_null_clone th in
if Stdecl.mem td s then Some th else None
let th = match (Stdecl.choose s).td_node with
| Use th
| Clone (th, _) -> th
| _ -> assert false
in
if Stdecl.exists check_use s then Some th else None
in
Mid.map_filter used (task_clone task)
......@@ -244,7 +255,7 @@ let used_symbols thmap =
let local_decls task symbmap =
let rec skip t = function
| { td_node = Clone (th,_) } :: rest
| { td_node = Use th } :: rest
when id_equal t.th_name th.th_name -> rest
| _ :: rest -> skip t rest
| [] -> []
......@@ -272,9 +283,10 @@ let on_meta t fn acc task =
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set acc
let on_theory th fn acc task =
let on_cloned_theory th fn acc task =
let add td acc = match td.td_node with
| Clone (_,sm) -> fn acc sm
| Use _ -> acc
| _ -> assert false
in
let tds = find_clone_tds task th in
......@@ -290,9 +302,8 @@ let on_meta_excl t task =
Stdecl.fold add tds.tds_set None
let on_used_theory th task =
let td = create_null_clone th in
let tds = find_clone_tds task th in
Stdecl.mem td tds.tds_set
Stdecl.exists check_use tds.tds_set
let on_tagged_ty t task =
begin match t.meta_type with
......
......@@ -29,8 +29,8 @@ val tds_empty : tdecl_set
val mk_tds : Stdecl.t -> tdecl_set
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
type clone_map = tdecl_set Mid.t (* Use and Clone *)
type meta_map = tdecl_set Mmeta.t (* Meta *)
(** Task *)
......@@ -40,7 +40,7 @@ and task_hd = private {
task_decl : tdecl; (* last declaration *)
task_prev : task; (* context *)
task_known : known_map; (* known identifiers *)
task_clone : clone_map; (* cloning history *)
task_clone : clone_map; (* use/clone history *)
task_meta : meta_map; (* meta properties *)
task_tag : Weakhtbl.tag; (* unique magical tag *)
}
......@@ -116,7 +116,7 @@ val task_separate_goal : task -> tdecl * task
(** {2 selectors} *)
val on_meta : meta -> ('a -> meta_arg list -> 'a) -> 'a -> task -> 'a
val on_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
val on_cloned_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
val on_meta_excl : meta -> task -> meta_arg list option
val on_used_theory : theory -> task -> bool
......
......@@ -722,19 +722,6 @@ let clone_export uc th inst =
let clone_theory add_td acc th inst =
clone_theory (cl_init th inst) add_td acc th inst
let create_null_clone th =
let sm = {
sm_ts = Mts.empty;
sm_ls = Mls.empty;
sm_pr = Mpr.empty}
in
mk_tdecl (Clone (th,sm))
let is_empty_sm sm =
Mts.is_empty sm.sm_ts &&
Mls.is_empty sm.sm_ls &&
Mpr.is_empty sm.sm_pr
(** Meta properties *)
let get_meta_arg_type = function
......
......@@ -179,10 +179,6 @@ val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val create_null_clone : theory -> tdecl
val is_empty_sm : symbol_map -> bool
(** {2 Meta} *)
val create_meta : meta -> meta_arg list -> tdecl
......
......@@ -170,8 +170,9 @@ let on_meta_tds t fn =
let fn = Wtds.memoize 17 fn in
fun task -> fn (find_meta_tds task t) task
let on_theory th fn =
let on_cloned_theory th fn =
let add td acc = match td.td_node with
| Use _ -> acc
| Clone (_,sm) -> sm::acc
| _ -> assert false
in
......@@ -185,8 +186,12 @@ let on_meta t fn =
on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set []))
let on_used_theory th fn =
let td = create_null_clone th in
on_theory_tds th (fun tds -> fn (Stdecl.mem td tds.tds_set))
let check td = match td.td_node with
| Use _ -> true
| Clone _ -> false
| _ -> assert false
in
on_theory_tds th (fun tds -> fn (Stdecl.exists check tds.tds_set))
let on_meta_excl t fn =
if not t.meta_excl then raise (NotExclusiveMeta t);
......
......@@ -69,10 +69,10 @@ val add_tdecls : tdecl list -> task trans
(* Dependent Transformations *)
val on_meta : meta -> (meta_arg list list -> 'a trans) -> 'a trans
val on_theory : theory -> (symbol_map list -> 'a trans) -> 'a trans
val on_meta_excl : meta -> (meta_arg list option -> 'a trans) -> 'a trans
val on_used_theory : theory -> (bool -> 'a trans) -> 'a trans
val on_cloned_theory : theory -> (symbol_map list -> 'a trans) -> 'a trans
val on_tagged_ty : meta -> (Sty.t -> 'a trans) -> 'a trans
val on_tagged_ts : meta -> (Sts.t -> 'a trans) -> 'a trans
......
......@@ -259,7 +259,14 @@ exception NoPrinter
let update_task = let ht = Hint.create 5 in fun drv ->
let update task0 =
Mid.fold (fun _ (th,s) task ->
Task.on_theory th (fun task sm ->
let task = if Task.on_used_theory th task0 then
Stdecl.fold (fun tdm task ->
add_tdecl task tdm
) s task
else
task
in
Task.on_cloned_theory th (fun task sm ->
Stdecl.fold (fun tdm task ->
add_tdecl task (clone_meta tdm sm)
) s task
......
......@@ -949,12 +949,12 @@ let print_task printer_args realize ?old fmt task =
Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
| _ -> assert false
) Mid.empty task in
(* 2 cases: goal is clone T with [] or goal is a real goal *)
(* 2 cases: goal is use T or goal is a real goal *)
let rec upd_realized_theories = function
| Some { Task.task_decl = { Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, _) }}} ->
realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
| Some { Task.task_decl = { Theory.td_node = Theory.Use th }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
Mid.remove th.Theory.th_name realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Meta _ };
......
......@@ -435,12 +435,12 @@ let print_task printer_args realize fmt task =
Mid.add th.Theory.th_name (th, s1) mid
| _ -> assert false
) Mid.empty task in
(* two cases: task is clone T with [] or task is a real goal *)
(* two cases: task is use T or task is a real goal *)
let rec upd_realized_theories = function
| Some { Task.task_decl = { Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, pr, _) }}} ->
id_unique thprinter pr.pr_name, realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
| Some { Task.task_decl = { Theory.td_node = Theory.Use th }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
let id = th.Theory.th_name in
String.concat "." (th.Theory.th_path @ [id_unique thprinter id]),
......
......@@ -834,12 +834,12 @@ let print_task printer_args realize ?old fmt task =
(th, (f, if s2 = "" then String.concat "." f else s2)) mid
| _ -> assert false
) Mid.empty task in
(* two cases: task is clone T with [] or task is a real goal *)
(* two cases: task is use T or task is a real goal *)
let rec upd_realized_theories = function
| Some { Task.task_decl = { Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, pr, _) }}} ->
get_th_name pr.pr_name, [], realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
| Some { Task.task_decl = { Theory.td_node = Theory.Use th }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
let id = th.Theory.th_name in
get_th_name id,
......
......@@ -370,8 +370,6 @@ let print_tdecl fmt td = match td.td_node with
print_decl fmt d
| Use th ->
fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" print_qt th
| Clone (th,sm) when is_empty_sm sm ->
fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" print_qt th
| Clone (th,sm) ->
let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
let lm = Mls.fold (fun x y a -> (x,y)::a) sm.sm_ls [] in
......
......@@ -568,6 +568,19 @@ module Checksum = struct
| Theory.MAstr s -> char b 's'; string b s
| Theory.MAint i -> char b 'i'; int b i
let tdecl b d = match d.Theory.td_node with
| Theory.Decl d -> decl b d
| Theory.Use th
| Theory.Clone (th, _) ->
char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
| Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal
(* not used anymore
NOTE: if we come back to checksumming theories, use the separate recursive
[tdecl] function for it. [Use] in a theory requires a recursive call
(as below), [Use] in a task is just a witness declaration.
let rec tdecl b d = match d.Theory.td_node with
| Theory.Decl d -> decl b d
| Theory.Use th ->
......@@ -594,7 +607,6 @@ module Checksum = struct
Ident.Wid.set table t.Theory.th_name v;
v
(* not used anymore
let theory ~version t = match version with
| CV1 -> assert false
| CV2 -> theory_v2 t
......
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