Commit ea1e0bec authored by Andrei Paskevich's avatar Andrei Paskevich

- separate Theory.tdecl and Task.tdecl and make both private

- provide several helper functions in Task
- Pretty.print_named_task will also print Use and Clone decls
parent 3a8c3e5f
......@@ -344,18 +344,26 @@ let print_tdecl fmt = function
fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
print_th th (print_list comma print_inst) inst
let print_decls fmt dl =
fprintf fmt "@[<hov>%a@]@." (print_list newline2 print_decl) dl
let print_task fmt task =
fprintf fmt "@[<hov>%a@]@."
(print_list newline2 print_decl) (task_decls task)
let print_task fmt task = print_decls fmt (task_decls task)
let print_named_task fmt name task =
fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
name (print_list newline2 print_tdecl) (task_tdecls task)
let print_th_tdecl fmt = function
| Theory.Decl d ->
print_decl fmt d
| Theory.Use th ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
| Theory.Clone (th,inst) ->
fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
print_th th (print_list comma print_inst) inst
let print_theory fmt th =
fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
print_th th (print_list newline2 print_tdecl) th.th_decls
let print_named_task fmt name task =
fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
name print_task task
print_th th (print_list newline2 print_th_tdecl) th.th_decls
module NsTree = struct
type t =
......
......@@ -54,7 +54,6 @@ val print_ind_decl : formatter -> ind_decl -> unit
val print_prop_decl : formatter -> prop_decl -> unit
val print_decl : formatter -> decl -> unit
val print_decls : formatter -> decl list -> unit
val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit
......
......@@ -37,6 +37,11 @@ and task_hd = {
task_tag : int; (* unique task tag *)
}
and tdecl =
| Decl of decl
| Use of theory
| Clone of theory * (ident * ident) list
module Task = struct
type t = task_hd
......@@ -124,30 +129,32 @@ let rec use_export task th = match task with
| Some task_hd when Mid.mem th.th_name task_hd.task_used -> task
| _ -> add_tdecl (List.fold_left flat_tdecl task th.th_decls) (Use th)
and flat_tdecl task td = match td with
| Decl { d_node = Dprop (Pgoal,_,_) } -> task
| Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
| Decl _ -> add_tdecl task td
| Clone _ -> add_tdecl task td
| Use th -> use_export task th
and flat_tdecl task = function
| Theory.Decl { d_node = Dprop (Pgoal,_,_) } ->
task
| Theory.Decl { d_node = Dprop (Plemma,pr,f) } ->
add_prop_decl task Paxiom pr f
| Theory.Decl d -> add_tdecl task (Decl d)
| Theory.Clone (th,sl) -> add_tdecl task (Clone (th,sl))
| Theory.Use th -> use_export task th
let clone_export = clone_theory flat_tdecl
let split_tdecl names (res,task) td = match td with
| Decl { d_node = Dprop (Pgoal,pr,_) }
let split_tdecl names (res,task) = function
| Theory.Decl { d_node = Dprop (Pgoal,pr,f) }
when option_apply true (Spr.mem pr) names ->
add_tdecl task td :: res, task
| Decl { d_node = Dprop (Pgoal,_,_) } ->
add_prop_decl task Pgoal pr f :: res, task
| Theory.Decl { d_node = Dprop (Pgoal,_,_) } ->
res, task
| Decl { d_node = Dprop (Plemma,pr,f) }
| Theory.Decl { d_node = Dprop (Plemma,pr,f) }
when option_apply true (Spr.mem pr) names ->
add_prop_decl task Pgoal pr f :: res,
add_prop_decl task Paxiom pr f
| Decl { d_node = Dprop (Plemma,pr,f) } ->
| Theory.Decl { d_node = Dprop (Plemma,pr,f) } ->
res, add_prop_decl task Paxiom pr f
| Decl _ -> res, add_tdecl task td
| Clone _ -> res, add_tdecl task td
| Use th -> res, use_export task th
| Theory.Decl d -> res, add_tdecl task (Decl d)
| Theory.Clone (th,sl) -> res, add_tdecl task (Clone (th,sl))
| Theory.Use th -> res, use_export task th
let split_theory th names =
fst (List.fold_left (split_tdecl names) ([],None) th.th_decls)
......@@ -167,6 +174,20 @@ let task_tdecls = task_fold (fun acc d -> d::acc) []
let task_decls =
task_fold (fun acc -> function Decl d -> d::acc | _ -> acc) []
let rec last_use task = match task with
| Some { task_decl = Use _ } -> task
| Some { task_prev = task } -> last_use task
| None -> None
let rec last_clone task = match task with
| Some { task_decl = Clone _ } -> task
| Some { task_prev = task } -> last_clone task
| None -> None
let get_known = option_apply Mid.empty (fun t -> t.task_known)
let get_clone = option_apply Mid.empty (fun t -> t.task_clone)
let get_used = option_apply Mid.empty (fun t -> t.task_used)
exception GoalNotFound
let task_goal = function
......
......@@ -36,6 +36,11 @@ and task_hd = private {
task_tag : int; (* unique task tag *)
}
and tdecl = private
| Decl of decl
| Use of theory
| Clone of theory * (ident * ident) list
(* constructors *)
val add_tdecl : task -> tdecl -> task
......@@ -65,7 +70,15 @@ val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
val task_tdecls : task -> tdecl list
val task_decls : task -> decl list
val task_goal : task -> prsymbol
val task_goal : task -> prsymbol
val last_clone : task -> task
val last_use : task -> task
val get_known : task -> known_map
val get_clone : task -> clone_map
val get_used : task -> use_map
(* exceptions *)
......
......@@ -53,7 +53,7 @@ type theory = private {
th_local : Sid.t; (* locally declared idents *)
}
and tdecl =
and tdecl = private
| Decl of decl
| Use of theory
| Clone of theory * (ident * ident) list
......
......@@ -19,7 +19,6 @@
open Term
open Decl
open Theory
open Task
let rec rewriteT kn t = match t.t_node with
......
......@@ -22,7 +22,6 @@ open Ident
open Ty
open Term
open Decl
open Theory
open Task
type state = {
......
......@@ -149,7 +149,7 @@ let add_ld kn task (ls,ld) = match ld with
let add_ls task (ls,_) = add_decl task (create_logic_decl [ls,None])
let elim t task = match t.task_decl with
| Theory.Decl { d_node = Dlogic ll } ->
| Decl { d_node = Dlogic ll } ->
let task = List.fold_left add_ls task ll in
let task = List.fold_left (add_ld t.task_known) task ll in
task
......
......@@ -107,7 +107,7 @@ let fold isnotinlinedt isnotinlinedf d (env, task) =
let fold isnotinlinedt isnotinlinedf task0 (env, task) =
match task0.task_decl with
| Theory.Decl d -> fold isnotinlinedt isnotinlinedf d (env, task)
| Decl d -> fold isnotinlinedt isnotinlinedf d (env, task)
| td -> env, add_tdecl task td
let t ~isnotinlinedt ~isnotinlinedf =
......
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