Commit f8785b5e authored by Andrei Paskevich's avatar Andrei Paskevich

Decl: remove Pskip and use Task.split_theory to avoid reproving lemmas

parent d993dad4
......@@ -254,7 +254,7 @@ let print_decl info fmt d = match d.d_node with
let head = if info.info_fmt = FOF then "fof" else "tff" in
fprintf fmt "@[<hov 2>%s(%a, conjecture,@ %a).@]@\n"
head print_pr pr (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) -> assert false
| Dprop (Plemma, _, _) -> assert false
let print_decls fm nm =
let print_decl (sm,fm,ct) fmt d =
......
......@@ -288,7 +288,6 @@ type prop_kind =
| Plemma (* prove, use as a premise *)
| Paxiom (* do not prove, use as a premise *)
| Pgoal (* prove, do not use as a premise *)
| Pskip (* do not prove, do not use as a premise *)
type prop_decl = prop_kind * prsymbol * term
......@@ -352,7 +351,7 @@ module Hsdecl = Hashcons.Make (struct
let hs_ind (ps,al) = Hashcons.combine_list hs_prop (ls_hash ps) al
let hs_kind = function
| Plemma -> 11 | Paxiom -> 13 | Pgoal -> 17 | Pskip -> 19
| Plemma -> 11 | Paxiom -> 13 | Pgoal -> 17
let hash d = match d.d_node with
| Dtype s -> ts_hash s
......
......@@ -82,7 +82,6 @@ type prop_kind =
| Plemma (** prove, use as a premise *)
| Paxiom (** do not prove, use as a premise *)
| Pgoal (** prove, do not use as a premise *)
| Pskip (** do not prove, do not use as a premise *)
type prop_decl = prop_kind * prsymbol * term
......
......@@ -391,7 +391,6 @@ let sprint_pkind = function
| Paxiom -> "axiom"
| Plemma -> "lemma"
| Pgoal -> "goal"
| Pskip -> "skip"
let print_pkind fmt k = pp_print_string fmt (sprint_pkind k)
......
......@@ -116,7 +116,6 @@ let find_meta_tds task (t : meta) = mm_find (task_meta task) t
(* constructors with checks *)
exception LemmaFound
exception SkipFound
exception GoalFound
exception GoalNotFound
......@@ -144,8 +143,7 @@ let check_task task = match find_goal task with
| None -> task
let check_decl = function
| { d_node = Dprop (Plemma,_,_)} -> raise LemmaFound
| { d_node = Dprop (Pskip,_,_)} -> raise SkipFound
| {d_node = Dprop (Plemma,_,_)} -> raise LemmaFound
| d -> d
let new_decl task d td =
......@@ -185,7 +183,7 @@ let add_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
| Decl { d_node = Dprop (Pgoal,_,_) } -> task
| Decl d -> new_decl task d td
| Use th -> use_export task th td
| Clone (th,_) -> new_clone task th td
......@@ -204,16 +202,22 @@ let add_meta task t al = new_meta task t (create_meta t al)
(* split theory *)
let split_tdecl names (res,task) td = match td.td_node with
| Decl { d_node = Dprop ((Pgoal|Plemma),pr,f) }
when Opt.fold (fun _ -> Spr.mem pr) true names ->
let res = add_prop_decl task Pgoal pr f :: res in
res, flat_tdecl task td
| _ ->
res, flat_tdecl task td
let split_theory th names init =
fst (List.fold_left (split_tdecl names) ([],init) th.th_decls)
let facts = ref Spr.empty in
let named pr = match names with Some s -> Spr.mem pr s | _ -> true in
let split (task, acc) td = flat_tdecl task td, match td.td_node with
| Clone (th, sm) -> (* do not reprove instantiations of lemmas *)
Mpr.iter (fun o n -> match find_prop_decl th.th_known o with
| (Plemma|Pgoal), _ -> facts := Spr.add n !facts
| _ -> ()) sm.sm_pr;
acc
| Decl { d_node = Dprop ((Plemma|Pgoal),pr,f) } when named pr ->
(pr, add_prop_decl task Pgoal pr f) :: acc
| _ -> acc in
let _, tasks = List.fold_left split (init, []) th.th_decls in
let filter acc (pr, task) =
if Spr.mem pr !facts then acc else task :: acc in
List.fold_left filter [] tasks
(* Generic utilities *)
......@@ -357,7 +361,6 @@ let on_tagged_pr t task =
let () = Exn_printer.register (fun fmt exn -> match exn with
| LemmaFound -> Format.fprintf fmt "Task cannot contain a lemma"
| SkipFound -> Format.fprintf fmt "Task cannot contain a skip"
| GoalFound -> Format.fprintf fmt "The task already ends with a goal"
| GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
| NotTaggingMeta m ->
......
......@@ -79,9 +79,13 @@ val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
(** {2 utilities} *)
val split_theory : theory -> Spr.t option -> task -> task list
(** [split_theory th s t] returns the tasks of [th] added to [t]
that end by one of [s]. They are in the opposite order than
in the theory *)
(** [split_theory th s t] returns the list of proof tasks that
correspond to goals in [th], in the order of appearance.
If set [s] is not empty, then only the goals in [s] are
proved. The goals which are instances of already proved
propositions (introduced by cloning) are not proved.
Task [t] is the task prefix that can be used to add
some metas to every generated proof task. *)
(** {2 realization utilities} *)
......@@ -133,5 +137,4 @@ exception NotExclusiveMeta of meta
exception GoalNotFound
exception GoalFound
exception SkipFound
exception LemmaFound
......@@ -396,7 +396,7 @@ let create_decl d = mk_tdecl (Decl d)
let warn_dubious_axiom uc k p syms =
match k with
| Plemma | Pgoal | Pskip -> ()
| Plemma | Pgoal -> ()
| Paxiom ->
try
Sid.iter
......@@ -615,14 +615,11 @@ let cl_ind cl inst (s, idl) =
let cl_prop cl inst (k,pr,f) =
let k' = match k, Mpr.find_opt pr inst.inst_pr with
| _, Some Pskip -> invalid_arg "Theory.clone_export"
| (Pskip | Pgoal), _ -> raise EmptyDecl
| Pgoal, _ -> raise EmptyDecl
| Plemma, Some Pgoal -> raise EmptyDecl
| Paxiom, Some Pgoal -> Pgoal
| (Paxiom | Plemma), Some Paxiom -> Paxiom
| (Paxiom | Plemma), Some Plemma -> Plemma
| Paxiom, None -> Paxiom (* TODO: Plemma *)
| Plemma, None -> Paxiom in
| Plemma, _ -> Plemma
| Paxiom, Some k -> k
| Paxiom, None -> Paxiom (* TODO: Plemma *) in
let pr' = cl_clone_pr cl pr in
let f' = cl_trans_fmla cl f in
create_prop_decl k' pr' f'
......@@ -690,25 +687,26 @@ let clone_export uc th inst =
let cl = cl_init th inst in
let uc = clone_theory cl add_tdecl uc th inst in
let g_ts _ ts = not (Mts.mem ts inst.inst_ts) in
let g_ls _ ls = not (Mls.mem ls inst.inst_ls) in
let g_pr _ pr = not (Mid.mem pr.pr_name th.th_local &&
let k, _ = find_prop_decl th.th_known pr in k = Pgoal || k = Pskip) in
let f_ts p ts =
try let ts = Mts.find ts cl.ts_table in store_path uc p ts.ts_name; ts
with Not_found -> ts in
if Mid.mem ts.ts_name th.th_local then
try let ts = Mts.find ts cl.ts_table in
store_path uc p ts.ts_name; Some ts
with Not_found -> None else Some ts in
let f_ls p ls =
try let ls = Mls.find ls cl.ls_table in store_path uc p ls.ls_name; ls
with Not_found -> ls in
if Mid.mem ls.ls_name th.th_local then
try let ls = Mls.find ls cl.ls_table in
store_path uc p ls.ls_name; Some ls
with Not_found -> None else Some ls in
let f_pr p pr =
try let pr = Mpr.find pr cl.pr_table in store_path uc p pr.pr_name; pr
with Not_found -> pr in
if Mid.mem pr.pr_name th.th_local then
try let pr = Mpr.find pr cl.pr_table in
store_path uc p pr.pr_name; Some pr
with Not_found -> None else Some pr in
let rec f_ns p ns = {
ns_ts = Mstr.map (f_ts p) (Mstr.filter g_ts ns.ns_ts);
ns_ls = Mstr.map (f_ls p) (Mstr.filter g_ls ns.ns_ls);
ns_pr = Mstr.map (f_pr p) (Mstr.filter g_pr ns.ns_pr);
ns_ts = Mstr.map_filter (f_ts p) ns.ns_ts;
ns_ls = Mstr.map_filter (f_ls p) ns.ns_ls;
ns_pr = Mstr.map_filter (f_pr p) ns.ns_pr;
ns_ns = Mstr.mapi (fun n -> f_ns (n::p)) ns.ns_ns; } in
let ns = f_ns [] th.th_export in
......@@ -750,11 +748,14 @@ let create_meta m al =
let add_meta uc s al = add_tdecl uc (create_meta s al)
let clone_meta tdt sm = match tdt.td_node with
let clone_meta tdt th sm = match tdt.td_node with
| Meta (t,al) ->
let find_ts ts = Mts.find_def ts ts sm.sm_ts in
let find_ls ls = Mls.find_def ls ls sm.sm_ls in
let find_pr pr = Mpr.find_def pr pr sm.sm_pr in
let find_ts ts = if Mid.mem ts.ts_name th.th_local
then Mts.find ts sm.sm_ts else ts in
let find_ls ls = if Mid.mem ls.ls_name th.th_local
then Mls.find ls sm.sm_ls else ls in
let find_pr pr = if Mid.mem pr.pr_name th.th_local
then Mpr.find pr sm.sm_pr else pr in
let cl_marg = function
| MAty ty -> MAty (ty_s_map find_ts ty)
| MAts ts -> MAts (find_ts ts)
......@@ -762,36 +763,9 @@ let clone_meta tdt sm = match tdt.td_node with
| MApr pr -> MApr (find_pr pr)
| a -> a
in
mk_tdecl (Meta (t, List.map cl_marg al))
| _ -> invalid_arg "clone_meta"
(** access to meta *)
(*
let theory_meta = Opt.fold (fun _ t -> t.task_meta) Mmeta.empty
let find_meta_tds th (t : meta) = mm_find (theory_meta th) t
let on_meta meta fn acc theory =
let add td acc = match td.td_node with
| Meta (_,ma) -> fn acc ma
| _ -> assert false
in
let tds = find_meta_tds theory meta in
Stdecl.fold add tds.tds_set acc
*)
(*
let on_meta _meta fn acc theory =
let tdecls = theory.th_decls in
List.fold_left
(fun acc td ->
match td.td_node with
| Meta (_,ma) -> fn acc ma
| _ -> acc)
acc tdecls
*)
begin try Some (mk_tdecl (Meta (t, List.map cl_marg al)))
with Not_found -> None end
| _ -> invalid_arg "Theory.clone_meta"
(** Base theories *)
......
......@@ -185,13 +185,12 @@ val create_meta : meta -> meta_arg list -> tdecl
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
val clone_meta : tdecl -> symbol_map -> tdecl
(** [clone_meta td_meta sm] produces from [td_meta]
a new Meta tdecl instantiated with respect to [sm]. *)
(*
val on_meta: meta-> ('a -> meta_arg list -> 'a) -> 'a -> theory -> 'a
*)
val clone_meta : tdecl -> theory -> symbol_map -> tdecl option
(** [clone_meta td_meta th sm] produces from [td_meta]
a new [Meta] tdecl instantiated with respect to [sm].
Returns [None] if [td_meta] mentions proposition symbols
that were not cloned (e.g. goals) or type symbols that
were cloned into complex types. *)
(** {2 Base theories} *)
......
......@@ -251,26 +251,23 @@ let call_on_buffer ~command ?timelimit ?memlimit ?steplimit
~command ?timelimit ?memlimit ?steplimit ~res_parser:drv.drv_res_parser
~filename ~printer_mapping ?inplace buffer
(** print'n'prove *)
exception NoPrinter
let update_task = let ht = Hint.create 5 in fun drv ->
let update task0 =
Mid.fold (fun _ (th,s) task ->
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
) task task0
Mid.fold (fun _ (th,tdms) task ->
let tdcs = (Task.find_clone_tds task0 th).tds_set in
Stdecl.fold (fun tdc task ->
Stdecl.fold (fun tdm task -> match tdc.td_node with
| Use _ -> add_tdecl task tdm
| Clone (_,sm) ->
let tdm = Theory.clone_meta tdm th sm in
Opt.fold add_tdecl task tdm
| _ -> assert false
) tdms task
) tdcs task
) drv.drv_meta task0
in
function
......
......@@ -92,7 +92,7 @@ let process () =
List.iter (fun th ->
ACSLtoWhy3.Self.result "running theory 1:";
ACSLtoWhy3.Self.result "@[<hov 2>%a@]" Pretty.print_theory th;
let tasks = List.rev (Task.split_theory th None None) in
let tasks = Task.split_theory th None None in
ACSLtoWhy3.Self.result "@[<h 0>Provers: %a@]"
(Pp.print_list Pp.comma
(fun fmt (_n,p,_d) ->
......
......@@ -528,14 +528,11 @@ let clone_decl inst cl uc d = match d.d_node with
add_pdecl ~vc:false uc (create_pure_decl d)
| Dprop (k,pr,f) ->
let skip, k' = match k, Mpr.find_opt pr inst.inst_pr with
| _, Some Pskip -> invalid_arg "Pmodule.clone_export"
| (Pskip | Pgoal), _ -> true, Pskip
| Plemma, Some Pgoal -> true, Pskip
| Paxiom, Some Pgoal -> false, Pgoal
| (Paxiom | Plemma), Some Paxiom -> false, Paxiom
| (Paxiom | Plemma), Some Plemma -> false, Plemma
| Paxiom, None -> false, Paxiom (* TODO: Plemma *)
| Plemma, None -> false, Paxiom in
| Pgoal, _ -> true, Pgoal
| Plemma, Some Pgoal -> true, Pgoal
| Plemma, _ -> false, Plemma
| Paxiom, Some k -> false, k
| Paxiom, None -> false, Paxiom (* TODO: Plemma *) in
if skip then uc else
let pr' = create_prsymbol (id_clone pr.pr_name) in
cl.pr_table <- Mpr.add pr pr' cl.pr_table;
......
......@@ -85,8 +85,7 @@ let find_prop_of_kind k tuc q =
| Dprop (l,_,_) when l = k -> pr
| _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
print_qualid q (match k with
| Plemma -> "a lemma" | Paxiom -> "an axiom"
| Pgoal -> "a goal" | Pskip -> assert false (* what? *))
| Plemma -> "a lemma" | Paxiom -> "an axiom" | Pgoal -> "a goal")
let find_itysymbol_ns ns q =
find_qualid (fun s -> s.its_ts.ts_name) Pmodule.ns_find_its ns q
......
......@@ -315,7 +315,7 @@ let print_prop_decl info fmt k pr f = match k with
| Pgoal ->
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
print_ident pr.pr_name (print_fmla info) f
| Plemma| Pskip -> assert false
| Plemma -> assert false
let print_prop_decl info fmt k pr f =
if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
......
......@@ -879,7 +879,6 @@ let print_prop_decl ~prev info fmt (k,pr,f) =
| Paxiom -> ""
| Plemma -> "Lemma"
| Pgoal -> "Theorem"
| Pskip -> assert false (* impossible *)
in
if stt <> "" then
match prev with
......
......@@ -256,7 +256,7 @@ let print_decl info fmt d = match d.d_node with
| Some loc -> fprintf fmt " @[%% %a@]@\n" Loc.gen_report_position loc
| None -> ());
fprintf fmt " @[%a;@]@]@\n" (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) -> assert false
| Dprop (Plemma, _, _) -> assert false
let print_decls =
let print_decl (sm,ct) fmt d =
......
......@@ -322,7 +322,7 @@ unsupportedDecl d
fprintf fmt "@[<hv 2>{ %a@ }@]@\n" (print_fmla info) f
*)
fprintf fmt "@[<hv 2>%a@]@\n" (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) ->
| Dprop (Plemma, _, _) ->
unsupportedDecl d
"gappa: lemmas are not supported"
*)
......@@ -392,7 +392,7 @@ let prepare info defs ((eqs,hyps,goal) as acc) d =
| Goal_none -> (eqs,hyps,filter_goal pr f)
| _ -> assert false
end
| Dprop ((Plemma|Pskip), _, _) ->
| Dprop (Plemma, _, _) ->
unsupportedDecl d
"gappa: lemmas are not supported"
......
......@@ -393,7 +393,6 @@ let print_prop_decl info fmt (k, pr, f) =
| Paxiom -> "axiom"
| Plemma -> "lemma"
| Pgoal -> "lemma"
| Pskip -> assert false (* impossible *)
in
print_statement stt (print_pr info) pr info fmt f
......
......@@ -413,7 +413,7 @@ let prepare info defs ((params,funs,preds,eqs,hyps,goal,types) as acc) d =
| Dind _ ->
unsupportedDecl d
"please remove inductive definitions before calling Mathematica printer"
| Dprop ((Plemma|Pskip), _, _) ->
| Dprop (Plemma, _, _) ->
unsupportedDecl d
"math: lemmas are not supported"
......
......@@ -767,8 +767,7 @@ let print_prop_decl ~prev info fmt (k,pr,f) =
| Paxiom when info.realization -> "LEMMA" (* axiom_or_lemma prev *)
| Paxiom -> "AXIOM"
| Plemma -> "LEMMA"
| Pgoal -> "THEOREM"
| Pskip -> assert false (* impossible *) in
| Pgoal -> "THEOREM" in
print_name fmt pr.pr_name;
fprintf fmt "@[<hov 2>%a%a: %s %a@]@\n@\n"
print_pr pr print_params params kind (print_fmla info) f;
......
......@@ -140,7 +140,7 @@ let print_decl info fmt d = match d.d_node with
| Some loc -> fprintf fmt " @[;; %a@]@\n" Loc.gen_report_position loc
| None -> ());
fprintf fmt "@[<hov 2>%a@]@\n" (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) ->
| Dprop (Plemma, _, _) ->
assert false
let print_decls =
......
......@@ -213,7 +213,7 @@ let print_decl info fmt d = match d.d_node with
| Some loc -> fprintf fmt " @[;; %a@]@\n" Loc.gen_report_position loc
| None -> ());
fprintf fmt " @[(not@ %a)@]@\n" (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) -> assert false
| Dprop (Plemma, _, _) -> assert false
let print_decls =
let print_decl (sm,ct) fmt d =
......
......@@ -90,7 +90,7 @@ let debug_print_term message t =
let form = Debug.get_debug_formatter () in
begin
Debug.dprintf debug message;
if Debug.test_flag debug then
if Debug.test_flag debug then
Pretty.print_term form t;
Debug.dprintf debug "@.";
end
......@@ -136,8 +136,8 @@ let collect_model_ls info ls =
(t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) :: info.info_model
(** expr *)
let rec print_term info fmt t =
debug_print_term "Printing term: " t;
let rec print_term info fmt t =
debug_print_term "Printing term: " t;
if Slab.mem model_label t.t_label then
info.info_model <- (t) :: info.info_model;
......@@ -200,11 +200,11 @@ let rec print_term info fmt t =
"smtv2: you must eliminate epsilon"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
and print_fmla info fmt f =
debug_print_term "Printing formula: " f;
and print_fmla info fmt f =
debug_print_term "Printing formula: " f;
if Slab.mem model_label f.t_label then
info.info_model <- (f) :: info.info_model;
match f.t_node with
| Tapp ({ ls_name = id }, []) ->
print_ident fmt id
......@@ -333,13 +333,13 @@ let print_logic_decl info fmt (ls,def) =
let print_info_model cntexample fmt info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if info_model != [] && cntexample then
if info_model != [] && cntexample then
begin
(*
fprintf fmt "@[(get-value (%a))@]@\n"
(Pp.print_list Pp.space (print_fmla info_copy)) model_list;*)
fprintf fmt "@[(get-value (";
List.iter (fun f ->
List.iter (fun f ->
fprintf str_formatter "%a" (print_fmla info) f;
let s = flush_str_formatter () in
fprintf fmt "%s " s;
......@@ -366,11 +366,9 @@ let print_prop_decl cntexample args info fmt k pr f = match k with
fprintf fmt " @[(not@ %a))@]@\n" (print_fmla info) f;
fprintf fmt "@[(check-sat)@]@\n";
print_info_model cntexample fmt info;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
queried_terms = info.info_model; }
| Plemma| Pskip -> assert false
| Plemma -> assert false
let print_constructor_decl info fmt (ls,args) =
......@@ -425,10 +423,10 @@ let print_decls cntexample args =
Printer.on_converter_map (fun cm ->
Trans.fold print_decl ((sm, cm, []),[])))
let set_produce_models fmt cntexample =
let set_produce_models fmt cntexample =
if cntexample then
fprintf fmt "(set-option :produce-models true)@\n"
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
......
......@@ -265,7 +265,7 @@ let print_decl info fmt d = match d.d_node with
| Some loc -> fprintf fmt " @[;; %a@]@\n" Loc.gen_report_position loc
| None -> ());
fprintf fmt " @[(not %a)@])@]@\n(check)@\n" (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) -> assert false
| Dprop (Plemma, _, _) -> assert false
let print_decls =
let print_decl (sm,ct) fmt d =
......
......@@ -1710,7 +1710,7 @@ let add_file ~keygen env ?format filename =
raw_add_theory ~keygen ~expanded:true ~checksum rfile thname
in
let parent = Parent_theory rtheory in
let tasks = List.rev (Task.split_theory theory None None) in
let tasks = Task.split_theory theory None None in
let goals = List.fold_left (add_goal parent) [] tasks in
rtheory.theory_goals <- List.rev goals;
rtheory.theory_verified <- theory_verified rtheory;
......@@ -2250,7 +2250,7 @@ let recover_theory_tasks env_session th =
let theories = Opt.get_exn NoTask th.theory_parent.file_for_recovery in
let theory = Opt.get_exn NoTask th.theory_task in
th.theory_checksum <- None (* Some (Tc.theory_checksum theory) *);
let tasks = List.rev (Task.split_theory theory None None) in
let tasks = Task.split_theory theory None None in
List.iter2 (recover_sub_tasks ~theories env_session) tasks th.theory_goals
let rec theory_goal g =
......
......@@ -541,7 +541,6 @@ module Checksum = struct
| Decl.Plemma -> "PL"
| Decl.Paxiom -> "PA"
| Decl.Pgoal -> "PG"
| Decl.Pskip -> "PS"
in
string b tag;
ident b n.Decl.pr_name;
......
......@@ -320,7 +320,7 @@ let do_theory env drv fname tname th glist elist =
let drv = Opt.get drv in
let prs = Queue.fold add Decl.Spr.empty glist in
let sel = if Decl.Spr.is_empty prs then None else Some prs in
let tasks = List.rev (split_theory th sel !opt_task) in
let tasks = Task.split_theory th sel !opt_task in
List.iter (do_tasks env drv fname tname th) tasks;
let eval (x,l) =
let ls = try ns_find_ls th.th_export l with Not_found ->
......
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