1. Dmitry Grebeniuk
  2. coq-breakpoints

Commits

Dmitry Grebeniuk  committed 8e0aa3b

init

  • Participants
  • Branches default

Comments (0)

Files changed (3)

File Bp_examples.v

View file
+(* Good old factorial with nameless breakpoints *)
+
+
+Module TestNameless.
+
+        Require Import Breakpoints.
+        Import Nameless.
+
+        Require Import EqNat.
+
+        Definition fact (n : nat) : nat :=
+          (fix _self_ acc n :=
+             match n with
+             | O => acc
+             | S n' =>
+                 _self_
+                   ( (if beq_nat n 4
+                      then fun x => BREAK x
+                      else id
+                     )
+                      (n * acc)
+                   )
+                   n'
+             end
+          )
+          1 n
+        .
+
+
+        Goal DEBUG fact 6.
+        cbv -[mult].
+        (* Goal is:
+           DEBUG 1 * (2 * (3 * BREAK "new acc on n=4" (4 * (5 * (6 * 1)))))
+        *)
+        under_break ltac:(fun e => eval simpl in e).
+        (* Goal is:
+           DEBUG 1 * (2 * (3 * BREAK "new acc on n=4" 120))
+        *)
+        pass.
+        (* Goal is:
+           DEBUG 1 * (2 * (3 * 120))
+        *)
+        simpl.
+        (* Goal is:
+           DEBUG 720
+        *)
+        FINISH.
+        Qed.
+
+
+End TestNameless.
+
+
+
+
+(* Example demonstating "waits" usage. *)
+
+
+Module TestNamed.
+
+        Require Import Breakpoints.
+        Import Named.
+
+        Goal DEBUG (let q := BREAK "z" 1 in (BREAK "d" plus) q (BREAK "b" 3))
+             = (match BREAK "i" 4 with | O => O | S _ => 2 * 2 end).
+        waits.
+        (* output:
+        breaks' waits:
+         break  "b"  waits for beta-reduction
+         break  "d"  waits for delta-reduction
+         break  "i"  waits for iota-reduction
+         break  "z"  waits for zeta-reduction
+        ---
+        *)
+
+        set_break "m" mult.
+        waits.
+
+        (* you could try here
+        pass_all.
+        *)
+
+        pass "z".
+        cbv zeta.
+        pass "d".
+        pass "b".
+        cbv beta delta [plus] iota.
+        pass "i".
+        cbv iota.
+        cbv beta.
+        pass "m".
+        cbv beta delta [mult plus] iota.
+        FINISH.
+        Qed.
+
+End TestNamed.
+

File Breakpoints.v

View file
+Require Import String.
+Open Scope string_scope.
+
+Module Named.
+
+Definition mytt : unit := tt.
+
+Definition BREAK (lbl : string) {A} (a : A) : A :=
+  match mytt with
+  | tt => a
+  end
+.
+
+Definition DEBUG {A} (a : A) : Type.
+exact (a = a)
+.
+Defined.
+
+Global Opaque mytt.
+Global Opaque BREAK.
+Global Opaque DEBUG.
+
+Ltac FINISH :=
+  match goal with
+  | |- DEBUG ?x => exact eq_refl
+  | _ => idtac
+  end
+.
+
+Notation "'DEBUG' x" := (DEBUG x)
+  (at level 100)
+.
+
+
+Definition break_marked (lbl : string) {A} (a : A) := a.
+
+
+Ltac mark_breaks lbl :=
+  change (@BREAK lbl) with (@break_marked lbl)
+(*
+  match goal with
+  | |- appcontext [BREAK lbl] =>
+      change (@BREAK lbl) with (@break_marked lbl);
+      mark_breaks lbl
+  | _ => idtac
+  end
+*)
+.
+
+Ltac unmark_breaks :=
+  change (@break_marked) with (@BREAK)
+(*
+  match goal with
+  | |- appcontext [break_marked ?lbl] =>
+      change (@break_marked lbl) with (@BREAK lbl);
+      unmark_breaks
+  | _ => idtac
+  end
+*)
+.
+
+Ltac breaks_loop :=
+  match goal with
+  | |- appcontext [@BREAK ?lbl] =>
+      idtac " " lbl;
+      mark_breaks lbl;
+      breaks_loop
+  | _ => idtac
+  end
+.
+
+Ltac breaks :=
+  idtac "breakpoints:";
+  breaks_loop;
+  unmark_breaks;
+  idtac "---"
+.
+
+Ltac pass_loop lbl :=
+  match goal with
+  | |- appcontext c [ BREAK lbl ?v ] =>
+      change (BREAK lbl v) with (v);
+      pass_loop lbl
+  | _ => idtac
+  end
+.
+
+Ltac pass lbl :=
+  pass_loop lbl;
+  change (@BREAK lbl) with (@id)
+    (* for breakpoints inside fixpoint, not matched by context[] *)
+.
+
+Ltac pass_all :=
+  match goal with
+  | |- appcontext [ BREAK ?lbl _ ] =>
+      pass lbl;
+      pass_all
+  | _ => idtac
+  end
+.
+
+Ltac report_beta_named lbl :=
+  idtac " break " lbl " waits for beta-reduction";
+  mark_breaks lbl
+.
+
+Ltac waits_beta_loop report_beta :=
+  match goal with
+  | |- appcontext [_ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ _ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ _ _ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | |- appcontext [_ _ _ _ _ _ _ _ _ _ _ _ (BREAK ?lbl _)] =>
+      report_beta lbl; waits_beta_loop
+  | _ => idtac
+  end
+.
+
+Ltac waits_delta_loop_gen rep :=
+  match goal with
+  | |- appcontext [ (BREAK ?lbl _) _ ] =>
+      rep lbl;
+      mark_breaks lbl;
+      waits_delta_loop_gen rep
+  | _ => idtac
+  end
+.
+
+Ltac waits_delta_loop :=
+  waits_delta_loop_gen
+    ltac:(fun lbl => idtac " break " lbl " waits for delta-reduction")
+.
+
+Ltac waits_iota_loop rep :=
+  match goal with
+  | |- context [match (BREAK ?lbl _) with _ => _ end] =>
+      rep lbl;
+      mark_breaks lbl;
+      waits_iota_loop
+  | _ => idtac
+  end
+.
+
+Ltac waits_zeta_loop_gen rep :=
+  match goal with
+  | |- context [let _ := BREAK ?lbl _ in _] =>
+      rep lbl;
+      mark_breaks lbl;
+      waits_zeta_loop_gen rep
+  | _ => idtac
+  end
+.
+
+Ltac waits :=
+  idtac "breaks' waits:";
+  waits_beta_loop report_beta_named;
+  unmark_breaks;
+  waits_delta_loop;
+  unmark_breaks;
+  waits_iota_loop
+    ltac:(fun lbl => idtac " break " lbl " waits for iota-reduction");
+  unmark_breaks;
+  waits_zeta_loop_gen
+    ltac:(fun lbl => idtac " break " lbl " waits for zeta-reduction");
+  unmark_breaks;
+  idtac "---"
+.
+
+
+Ltac set_break lbl expr :=
+  change (expr) with (BREAK lbl expr)
+.
+
+
+Ltac under_break_loop lbl tacredexp :=
+  match goal with
+  | |- appcontext [ BREAK lbl ?e ] =>
+      let e' := tacredexp e in
+      change (BREAK lbl e) with (break_marked lbl e');
+      under_break_loop lbl tacredexp
+  | _ => idtac
+end.
+
+Ltac under_break lbl tacredexp :=
+  under_break_loop lbl tacredexp;
+  unmark_breaks
+.
+
+Ltac under_all_breaks_loop tacredexp :=
+  match goal with
+  | |- appcontext [ @BREAK ?lbl ] =>
+      under_break_loop lbl tacredexp;
+      under_all_breaks_loop tacredexp
+  | _ => idtac
+  end
+.
+
+Ltac under_all_breaks tacredexp :=
+  under_all_breaks_loop tacredexp;
+  unmark_breaks
+.
+
+End Named.
+
+
+Module Nameless.
+
+Ltac FINISH :=
+  match goal with
+  | |- Named.DEBUG ?x => exact eq_refl
+  | _ => idtac
+  end
+.
+
+Notation "'DEBUG' x" := (Named.DEBUG x)
+  (at level 100)
+.
+
+Definition BREAK {A} (a : A) : A :=
+  match Named.mytt with
+  | tt => a
+  end
+.
+
+Global Opaque BREAK.
+
+Ltac to_named :=
+  change (@BREAK) with (@Named.BREAK "")
+.
+
+Ltac from_named :=
+  change (@Named.BREAK "") with (@BREAK)
+.
+
+
+Ltac breaks :=
+  idtac "breakpoints:";
+  match goal with
+  | |- appcontext [@Named.BREAK ""] =>
+      idtac " present"
+  | _ =>
+      idtac " absent"
+  end
+.
+
+Ltac pass :=
+  to_named;
+  Named.pass "";
+  from_named
+.
+
+Ltac pass_all := pass.
+
+Ltac report_beta_nameless lbl :=
+  idtac " waits for beta-reduction";
+  Named.mark_breaks lbl
+.
+
+Ltac waits_delta_loop :=
+  Named.waits_delta_loop_gen
+    ltac:(fun lbl => idtac " waits for delta-reduction")
+.
+
+Ltac waits :=
+  to_named;
+  idtac "breaks' waits:";
+  Named.waits_beta_loop report_beta_nameless;
+  Named.unmark_breaks;
+  waits_delta_loop;
+  Named.unmark_breaks;
+  Named.waits_iota_loop
+    ltac:(fun lbl => idtac " waits for iota-reduction");
+  Named.unmark_breaks;
+  Named.waits_zeta_loop_gen
+    ltac:(fun lbl => idtac " waits for zeta-reduction");
+  Named.unmark_breaks;
+  idtac "---";
+  from_named
+.
+
+
+Ltac set_break expr :=
+  change (expr) with (BREAK expr)
+.
+
+
+Ltac under_break tacredexp :=
+  to_named;
+  Named.under_break_loop "" tacredexp;
+  Named.unmark_breaks;
+  from_named
+.
+
+End Nameless.
+
+

File README

View file
+        Coq breakpoints library.
+
+
+    Objective.
+
+  Big and complex functions sometimes appearing during
+developement may contain bugs.  Proving their correctness
+can be very hard, especially when Coq is used as a programming
+language with rich types, not as proof assistant.
+
+
+    What is suggested?
+
+  This library allows one to prevent reduction of expressions
+of interest.  This is achieved by wrapping them in so called
+"breakpoints", either modifying source code of function or
+"on fly".
+  Then programmer can look at partial reduction's results, allow
+reduction of some/all breakpoint(s), list present breakpoints,
+watch at what these breakpoints are "waiting for"
+(beta/iota/zeta reduction), apply conversion tactic to expression
+under some/all breakpoint(s).
+
+
+    Why not <alternative>?
+
+  Usual alternatives are:
+
+  - debug with eyes, paper and pencil.  Hard for big functions
+    and deep recursion.
+
+  - add debug prints in extracted code.  Requires extraction
+    and patching extracted sources manually.  Repeat when
+    function's body is changed.
+
+  - use "writer monad".  Programmer must change types, use monadic
+    bind instead of some function applications, monadic return
+    instead of simply returning function's value.  However this
+    approach is useful when debug information should be present
+    in extracted code.
+
+  (know more?  Please tell me about them!)
+
+
+    How it works?
+
+  Internally breakpoint is represented as an opaque wrapper
+containing expression.  Coq doesn't unfold breakpoints until
+programmer won't tell him to do this.
+
+  There are two modules, for named and for nameless breakpoints.
+Names are not required sometimes, since they can clutter the
+output.  However it's impossible to manipulate specific nameless
+breakpoints, only "for all breakpoints" commands.
+
+
+    How to use it?
+
+  First,
+
+        Require Import Breakpoints.
+
+  Then, for named breakpoints:
+
+        Import Named.
+        Open Scope string_scope.  (* for convenience *)
+
+  For nameless breakpoints:
+
+        Import Nameless.
+
+
+    Usage.
+
+  (note: file "Bp_examples.v" contains examples on how to use
+   these definitions/tactics.)
+
+  This section contains documentation on both named and nameless
+breakpoints.  Each description states on what kind of breakpoints
+the definition/tactic is applicable.  Don't mix named breakpoints
+with nameless ones.
+
+  - DEBUG <expr>
+      is an expression of sort Type, useful to start a debug
+      session using vernacular 'Goal DEBUG <expr>.'
+      ("Lemma somelemma : DEBUG <expr>." is fine too -- just
+      enter the proof mode with breakpoints in the goal,
+      "DEBUG" is just a convenience keyword.)
+
+  - BREAK "name" <expr>
+      for named breakpoints it is a wrapper for <expr> that
+      won't be unfolded by Coq until 'pass "name".' or
+      'pass_all.' (see below).
+
+  - BREAK <expr>
+      same as 'BREAK "name" <expr>', but for nameless breakpoints.
+
+  Following commands can be used in proof mode:
+
+  - breaks.
+      for named breakpoints: lists breakpoints present in the
+      current goal.
+      for nameless breakpoints: shows presence/absence of
+      breakpoints in the current goal.
+
+  - waits.
+      lists breakpoints and their positions in the goal:
+      - "beta"
+          breakpoint is an argument of some function
+      - "delta"
+          breakpoint is a function
+      - "iota"
+          breakpoint present in match construction as a
+          "match_item" -- expression that will be "destructed"
+          by "match"
+      - "zeta"
+          breakpoint is a right-hand side of some
+          "let lhs := rhs in expr" expression
+
+  - under_break "name" ltac:(fun e => eval <redexp> in e).
+      reduces expression wrapped in breakpoint "name" with
+      conversion tactic <redexp> (like "simpl", "cbv ..."
+      and so on).
+
+  - under_all_breaks ltac:(fun e => eval <redexp> in e).
+      same as 'under_break "name" ...", but for all named
+      breakpoints
+
+  - under_break ltac:(fun e => eval <redexp> in e).
+      same as 'under_break "name" ...', but for nameless
+      breakpoints
+
+  - pass-like commands:
+      allow some/all breakpoints to be reduced by Coq:
+
+      - pass "name".
+          for breakpoint with name "name"
+
+      - pass_all.
+          for all breakpoints (named/nameless)
+
+      - pass.
+          for all nameless breakpoints
+
+  - set_break "name" <expr>.
+      sets named breakpoint "on fly".
+
+  - set_break <expr>.
+      sets nameless breakpoint "on fly".
+
+  - FINISH.
+      Finishes the debug session, allows one to store it for
+      later debugging, with "Defined." / "Qed".
+
+  Coq "conversion tactics" are very useful during debug
+session, most notably "cbv" tactic which can be fine-tuned
+to make Coq do only needed reductions.
+
+
+    Examples.
+
+  See the file "Bp_examples.v".
+
+
+    Bugs.
+
+  Breakpoints that use fixpoint's arguments can't be manipulated:
+they are not seen in "breaks", "waits", can't be "pass"'ed.
+
+  Why?  Take a look at an example:
+
+        Goal (fix f (x : nat) := id x) 1 = 1.
+        match goal with
+        | |- appcontext [@id] => idtac "works"
+        | _ (* match failback *) => idtac "doesn't work"
+        end.
+
+  It's a Coq bug probably, it is already reported:
+
+        https://coq.inria.fr/bugs/show_bug.cgi?id=2998
+
+
+    Authors.
+
+  Code:
+    - Dmitry Grebeniuk <gdsfh1@gmail.com>
+
+  Ideas: 
+    - Robbert Krebbers
+    - AUGER Cédric
+
+
+    License:
+
+  GPL