Makes the Ltac debugger usable again.

This is just a port of the existing design. Basing the tactics on an IO monad
may allow to simplify things a bit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16985 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 40 insertions, 5 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 26583b0be5..c9cdfc2ad6 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -30,7 +30,6 @@ Extract Inductive prod => "(*)" [
 ].
 
 (*** Sum ***)
-Print sum.
 Extract Inductive sum => "Util.union" [
   "Util.Inl"
   "Util.Inr"
@@ -44,6 +43,26 @@ Extract Inlined Constant Exception => exn.
 Parameter tactic_failure : Exception -> Exception.
 Extract Inlined Constant tactic_failure => "(fun e -> Proof_errors.TacticFailure e)".
 
+(*** Basic integers ***)
+
+Parameter Int : Set.
+Extract Inlined Constant Int => int.
+
+(*** Char ***)
+
+Parameter Char : Set.
+Extract Inlined Constant Char => char.
+
+(*** Primitive strings ***)
+
+Parameter String : Set.
+Extract Inlined Constant String => string.
+
+(*** Pretty printer ***)
+
+Parameter Ppcmds : Set.
+Extract Inlined Constant Ppcmds => "Pp.std_ppcmds".
+
 (*** Monoids ***)
 
 Module Monoid.
@@ -162,8 +181,13 @@ Module IOBase.
  Extract Constant catch => "fun s h () -> try s () with Proof_errors.Exception e -> h e ()".
  Extraction Implicit catch [A].
 
- Parameter Int : Set.
- Extract Constant Int => int.
+ Parameter read_line : T String.
+ Extract Constant read_line => "fun () -> try Pervasives.read_line () with e -> raise e ()".
+ Parameter print_char : Char -> T unit.
+ Extract Constant print_char => "fun c () -> print_char c".
+ Parameter print : Ppcmds -> T unit.
+ Extract Constant print => "fun s () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()".
+
  Parameter timeout: forall A, Int -> T A -> T A.
  Extract Constant timeout => "fun n t () ->
     let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
@@ -193,9 +217,13 @@ Module IO.
    set : forall {A:Set}, Ref A -> A -> T unit;
    get : forall {A:Set}, Ref A -> T A;
 
+   read_line : T String;
+   print_char : Char -> T unit;
+   print : Ppcmds -> T unit;
+
    raise : forall {A:Set}, Exception -> T A;
    catch : forall {A:Set}, T A -> (Exception -> T A) -> T A;
-   timeout : forall {A:Set}, IOBase.Int -> T A -> T A
+   timeout : forall {A:Set}, Int -> T A -> T A
  }.
 
  Definition T : Set -> Set := IOBase.T.
@@ -213,6 +241,10 @@ Module IO.
    set := IOBase.set;
    get := IOBase.get;
 
+   read_line := IOBase.read_line;
+   print_char := IOBase.print_char;
+   print := IOBase.print;
+
    raise := IOBase.raise;
    catch := IOBase.catch;
    timeout := IOBase.timeout
@@ -550,6 +582,10 @@ Module NonLogical.
  Definition timeout {a:Set} n (x:t a) : t a := Eval compute in IO.timeout _ _ NonLogicalIO n x.
  Extraction Implicit timeout [a].
 
+ Definition read_line : t String := Eval compute in IO.read_line _ _ NonLogicalIO.
+ Definition print_char (c:Char) : t unit := Eval compute in IO.print_char _ _ NonLogicalIO c.
+ Definition print (s:Ppcmds) : t unit := Eval compute in IO.print _ _ NonLogicalIO s.
+
  (* /!\ The extracted code for [run] performs effects. /!\ *)
  Parameter run : forall a:Set, t a -> a.
  Extract Constant run => "fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e".
@@ -572,7 +608,6 @@ Module Logical.
 
  Definition set (s:LogicalState) : t unit := Eval compute in set _ _ LogicalStateM s.
  Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
- Print Environment.lift.
  Definition put (m:LogicalMessageType) : t unit := Eval compute in State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (put _ _ LogicalWriter m)).
  Definition current : t LogicalEnvironment := Eval compute in State.lift _ _ LogicalMonadEnv (current _ _ LogicalReader).