|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Stm
module Util : sig
val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
val crawl :
document_view -> ?init:document_node option ->
('a -> document_node -> 'a until) -> 'a ->
static_block_declaration option
val unit_val : Stm.DynBlockData.t
val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
end = struct
let unit_tag = DynBlockData.create "unit"
let unit_val = DynBlockData.Easy.inj () unit_tag
let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"
let simple_goal sigma g gs =
let open Evar in
let open Evd in
let open Evarutil in
let evi = Evd.find sigma g in
Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
not (List.exists (Proofview.depends_on sigma g) gs)
let is_focused_goal_simple ~doc id =
match state_of_id ~doc id with
| `Expired | `Error _ | `Valid None -> `Not
| `Valid (Some { Vernacstate.proof }) ->
Option.cata (fun proof ->
let proof = Proof_global.give_me_the_proof proof in
let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
if List.for_all (fun x -> simple_goal sigma x rest) focused
then `Simple focused
else `Not) `Not proof
type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc =
let rec crawl node acc =
match node with
| None -> None
| Some node ->
match f acc node with
| `Stop -> None
| `Found x -> Some x
| `Cont acc -> crawl (prev_node node) acc in
crawl init acc
end
include Util
(* ****************** - foo - bar - baz *********************************** *)
let static_bullet ({ entry_point; prev_node } as view) =
assert (not (Vernacprop.has_Fail entry_point.ast));
match Vernacprop.under_control entry_point.ast with
| Vernacexpr.VernacBullet b ->
let base = entry_point.indentation in
let last_tac = prev_node entry_point in
crawl view ~init:last_tac (fun prev node ->
if node.indentation < base then `Stop else
if node.indentation > base then `Cont node else
if Vernacprop.has_Fail node.ast then `Stop
else match Vernacprop.under_control node.ast with
| Vernacexpr.VernacBullet b' when b = b' ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = of_bullet_val b }
| _ -> `Stop) entry_point
| _ -> assert false
let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
match is_focused_goal_simple ~doc id with
| `Simple focused ->
`ValidBlock {
base_state = id;
goals_to_admit = focused;
recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
}
| `Not -> `Leaks
let () = register_proof_block_delimiter
"bullet" static_bullet dynamic_bullet
(* ******************** { block } ***************************************** *)
let static_curly_brace ({ entry_point; prev_node } as view) =
assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
crawl view (fun (nesting,prev) node ->
if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
else match Vernacprop.under_control node.ast with
| Vernacexpr.VernacSubproof _ when nesting = 0 ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = unit_val }
| Vernacexpr.VernacSubproof _ ->
`Cont (nesting - 1,node)
| Vernacexpr.VernacEndSubproof ->
`Cont (nesting + 1,node)
| _ -> `Cont (nesting,node)) (-1, entry_point)
let dynamic_curly_brace doc { dynamic_switch = id } =
match is_focused_goal_simple ~doc id with
| `Simple focused ->
`ValidBlock {
base_state = id;
goals_to_admit = focused;
recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
}
| `Not -> `Leaks
let () = register_proof_block_delimiter
"curly" static_curly_brace dynamic_curly_brace
(* ***************** par: ************************************************* *)
let static_par { entry_point; prev_node } =
match prev_node entry_point with
| None -> None
| Some { id = pid } ->
Some { block_stop = entry_point.id; block_start = pid;
dynamic_switch = pid; carry_on_data = unit_val }
let dynamic_par doc { dynamic_switch = id } =
match is_focused_goal_simple ~doc id with
| `Simple focused ->
`ValidBlock {
base_state = id;
goals_to_admit = focused;
recovery_command = None;
}
| `Not -> `Leaks
let () = register_proof_block_delimiter "par" static_par dynamic_par
(* ***************** simple indentation *********************************** *)
let static_indent ({ entry_point; prev_node } as view) =
Printf.eprintf "@%d\n" (Stateid.to_int entry_point.id);
match prev_node entry_point with
| None -> None
| Some last_tac ->
if last_tac.indentation <= entry_point.indentation then None
else
crawl view ~init:(Some last_tac) (fun prev node ->
if node.indentation >= last_tac.indentation then `Cont node
else
`Found { block_stop = entry_point.id; block_start = node.id;
dynamic_switch = node.id;
carry_on_data = of_vernac_control_val entry_point.ast }
) last_tac
let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
Printf.eprintf "%s\n" (Stateid.to_string id);
match is_focused_goal_simple ~doc id with
| `Simple [] -> `Leaks
| `Simple focused ->
let but_last = List.tl (List.rev focused) in
`ValidBlock {
base_state = id;
goals_to_admit = but_last;
recovery_command = Some (to_vernac_control_val e);
}
| `Not -> `Leaks
let () = register_proof_block_delimiter "indent" static_indent dynamic_indent
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
