Commit 7adf6371 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

introduce_premises does not introduce a meta anymore

parent 0ac9d709
...@@ -88,11 +88,6 @@ let debug_print_labels = ...@@ -88,11 +88,6 @@ let debug_print_labels =
let debug_print_locs = Debug.register_info_flag "print_locs" let debug_print_locs = Debug.register_info_flag "print_locs"
~desc:"Print@ locations@ of@ identifiers@ and@ expressions." ~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
let meta_introduced_hypotheses =
register_meta
~desc:"marks beginning of hypotheses introduced by introduce_premises"
"introduced_premises" []
let create iprinter aprinter tprinter pprinter do_forget_all = let create iprinter aprinter tprinter pprinter do_forget_all =
(module (struct (module (struct
...@@ -588,22 +583,18 @@ let local_decls task symbmap = ...@@ -588,22 +583,18 @@ let local_decls task symbmap =
| _ :: rest -> skip t rest | _ :: rest -> skip t rest
| [] -> [] | [] -> []
in in
let rec filter ((b,acc1,acc2) as acc) = function let rec filter ((acc1,acc2) as acc) = function
| { td_node = Meta (m,_) } :: rest
when meta_equal m meta_introduced_hypotheses ->
filter (true, acc2 @ acc1, []) rest
| { td_node = Decl d } :: rest -> | { td_node = Decl d } :: rest ->
let id = Sid.choose d.d_news in let id = Sid.choose d.d_news in
(try filter acc (skip (Mid.find id symbmap) rest) (try filter acc (skip (Mid.find id symbmap) rest)
with Not_found -> with Not_found ->
filter (b,acc1,d::acc2) rest) filter (acc1,d::acc2) rest)
| _ :: rest -> filter acc rest | _ :: rest -> filter acc rest
| [] -> if b then List.rev acc1, List.rev acc2 | [] -> match acc1,acc2 with
else match acc1,acc2 with
| [], g::r -> List.rev r, [g] | [], g::r -> List.rev r, [g]
| _ -> assert false | _ -> assert false
in in
filter (false,[],[]) (task_tdecls task) filter ([],[]) (task_tdecls task)
let print_sequent fmt task = let print_sequent fmt task =
let ut = Task.used_symbols (Task.used_theories task) in let ut = Task.used_symbols (Task.used_theories task) in
......
...@@ -76,8 +76,6 @@ module type Printer = sig ...@@ -76,8 +76,6 @@ module type Printer = sig
include Printer include Printer
val meta_introduced_hypotheses : Theory.meta
val create : Ident.ident_printer ->Ident.ident_printer -> val create : Ident.ident_printer ->Ident.ident_printer ->
Ident.ident_printer -> Ident.ident_printer -> Ident.ident_printer -> Ident.ident_printer ->
bool -> (module Printer) bool -> (module Printer)
...@@ -65,12 +65,7 @@ let intros pr f = ...@@ -65,12 +65,7 @@ let intros pr f =
let subst = Mtv.map (fun ts -> ty_app ts []) tvm in let subst = Mtv.map (fun ts -> ty_app ts []) tvm in
Mtv.values decls @ intros pr (t_ty_subst subst Mvs.empty f) Mtv.values decls @ intros pr (t_ty_subst subst Mvs.empty f)
let intros_with_meta pr f = let introduce_premises = Trans.goal intros
let l = intros pr f in
Theory.create_meta Pretty.meta_introduced_hypotheses [] ::
List.rev (List.rev_map Theory.create_decl l)
let introduce_premises = Trans.tgoal intros_with_meta
let () = Trans.register_transform "introduce_premises" introduce_premises let () = Trans.register_transform "introduce_premises" introduce_premises
~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \ ~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
......
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