Declarative Proof Language: main commit

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

12 files changed, 606 insertions, 59 deletions

diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
new file mode 100644
index 0000000000..8d7fd1f189
--- /dev/null
+++ b/parsing/g_decl_mode.ml4
@@ -0,0 +1,171 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Decl_expr
+open Names
+open Term
+open Genarg
+open Pcoq
+
+open Pcoq.Constr
+open Pcoq.Tactic
+open Pcoq.Vernac_
+
+let none_is_empty = function
+    None -> []
+  | Some l -> l
+
+GEXTEND Gram
+GLOBAL: proof_instr;
+  thesis :
+    [[ "thesis" -> Plain 
+     | "thesis"; "for"; i=ident -> (For i)
+     | "thesis"; "["; n=INT ;"]" -> (Sub (int_of_string n))
+     ]];
+  statement :
+    [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
+     | i=ident -> {st_label=Anonymous;
+		   st_it=Topconstr.CRef (Libnames.Ident (loc, i))}
+     | c=constr -> {st_label=Anonymous;st_it=c}
+     ]];
+  constr_or_thesis :
+     [[ t=thesis -> Thesis t ] |
+      [ c=constr -> This c
+      ]];
+  statement_or_thesis : 
+    [
+      [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] 
+    |
+      [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
+      | i=ident -> {st_label=Anonymous;
+		    st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))}
+      | c=constr -> {st_label=Anonymous;st_it=This c}
+      ]
+    ];
+  justification : 
+    [[ -> Automated [] 
+     | IDENT "by"; l=LIST1 constr SEP "," -> Automated l
+     | IDENT "by"; IDENT "tactic"; tac=tactic -> By_tactic tac ]]
+  ;
+  simple_cut_or_thesis :
+    [[ ls = statement_or_thesis;
+       j=justification -> {cut_stat=ls;cut_by=j} ]]
+  ;
+  simple_cut :
+    [[ ls = statement;
+       j=justification -> {cut_stat=ls;cut_by=j} ]]
+  ;
+  elim_type:
+    [[ IDENT "induction" -> ET_Induction
+     | IDENT "cases" -> ET_Case_analysis ]]
+  ;
+  block_type :
+    [[ IDENT "claim" -> B_claim
+     | IDENT "focus" -> B_focus
+     | IDENT "proof" -> B_proof
+     | et=elim_type -> B_elim et ]]
+  ;    
+  elim_obj:
+    [[ IDENT "on"; c=constr -> Real c
+     | IDENT "of"; c=simple_cut -> Virtual c ]]
+  ;    
+  elim_step:
+    [[ IDENT "consider" ; h=vars ; IDENT "from" ; c=constr -> Pconsider (c,h)
+     | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)]]
+  ;
+  rew_step :
+    [[ "~=" ;         c=simple_cut -> (Rhs,c)       
+     | "=~" ;         c=simple_cut -> (Lhs,c)]]
+  ;
+  cut_step:
+    [[ "then"; tt=elim_step -> Pthen tt
+     | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c)
+     | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) 
+     | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c)
+     | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c)
+     | tt=elim_step -> tt
+     | tt=rew_step -> let s,c=tt in Prew (s,c); 
+     | IDENT "have"; c=simple_cut_or_thesis -> Pcut c;
+     | IDENT "claim"; c=statement -> Pclaim c;
+     | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c;    
+     | "end"; bt = block_type -> Pend bt;
+     | IDENT "escape" -> Pescape ]]
+  ;
+  (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*)
+  loc_id: 
+    [[ id=ident -> fun x -> (loc,(id,x)) ]];
+  hyp:
+    [[ id=loc_id -> id None ;
+     | id=loc_id ; ":" ; c=constr -> id (Some c)]]
+  ;
+  vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=vars -> (Hvar name) :: v
+     | name=hyp; IDENT "be"; 
+       IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h
+     | name=hyp; 
+       IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h
+     ]]
+  ;
+  hyps:  
+    [[ IDENT "we"; IDENT "have"; v=vars -> v
+     | st=statement; IDENT "and"; h=hyps  -> Hprop st::h
+     | st=statement; IDENT "and"; v=vars  -> Hprop st::v
+     | st=statement -> [Hprop st]
+     ]]
+  ;
+  vars_or_thesis:
+    [[name=hyp -> [Hvar name] 
+     |name=hyp; ","; v=vars_or_thesis -> (Hvar name) :: v
+     |name=hyp; OPT[IDENT "be"]; 
+      IDENT "such"; IDENT "that"; h=hyps_or_thesis -> (Hvar name)::h
+     ]]
+  ;
+  hyps_or_thesis:  
+    [[ IDENT "we"; IDENT "have"; v=vars_or_thesis -> v
+     | st=statement_or_thesis; IDENT "and"; h=hyps_or_thesis  -> Hprop st::h
+     | st=statement_or_thesis; IDENT "and"; v=vars_or_thesis  -> Hprop st::v
+     | st=statement_or_thesis -> [Hprop st];
+     ]]
+  ;
+  intro_step:
+    [[ IDENT "suppose" ; h=hyps -> Psuppose h
+     | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
+       po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; 
+       ho=OPT[ IDENT "and" ; h=hyps_or_thesis -> h ] -> 
+	 Pcase (none_is_empty po,c,none_is_empty ho)
+     | "let" ; v=vars -> Plet v	 
+     | IDENT "take"; witnesses = LIST1 constr SEP ","  -> Ptake witnesses
+     | IDENT "assume"; h=hyps -> Passume h
+     | IDENT "given"; h=vars -> Pgiven h
+     | IDENT "define"; id=ident; args=LIST0 hyp; 
+       "as"; body=constr -> Pdefine(id,args,body)
+     | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ)
+     | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ)
+     ]]
+  ;
+  emphasis : 
+    [[ -> 0
+     | "*" -> 1
+     | "**" -> 2
+     | "***" -> 3
+     ]]
+  ;
+  bare_proof_instr:
+    [[ c = cut_step -> c ;
+     | i = intro_step -> i ]]
+  ;
+  proof_instr :
+    [[ e=emphasis;i=bare_proof_instr -> {emph=e;instr=i}]]
+  ;
+END;;
+
+ 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index a1a7030990..afa5160116 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -75,6 +75,7 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
       | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
+      | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis
       | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
 	  VernacShow (ExplainProof l)
       | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 510fe529f0..81663bb918 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,6 +15,7 @@ open Names
 open Topconstr
 open Vernacexpr
 open Pcoq
+open Decl_mode
 open Tactic
 open Decl_kinds
 open Genarg
@@ -34,13 +35,28 @@ let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
 (* compilation on PowerPC and Sun architectures *)
 
 let check_command = Gram.Entry.create "vernac:check_command"
+
+let tactic_mode = Gram.Entry.create "vernac:tactic_command"
+let proof_mode = Gram.Entry.create "vernac:proof_command"
+let noedit_mode = Gram.Entry.create "vernac:noedit_command"
+
 let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
 let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
 
+let get_command_entry () =
+  match Decl_mode.get_current_mode () with
+      Mode_proof -> proof_mode
+    | Mode_tactic -> tactic_mode
+    | Mode_none -> noedit_mode
+
+let default_command_entry =
+  Gram.Entry.of_parser "command_entry" 
+    (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm)
+
 let no_hook _ _ = ()
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext;
+  GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
   vernac:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
@@ -54,9 +70,15 @@ GEXTEND Gram
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
   ;
-  vernac: LAST
-    [ [ gln = OPT[n=natural; ":" -> n];
-        tac = subgoal_command -> tac gln ] ]
+  vernac: LAST  
+    [ [ prfcom = default_command_entry -> prfcom ] ]
+  ;
+  noedit_mode:
+    [ [ c = subgoal_command -> c None] ]
+  ;
+  tactic_mode:
+  [ [ gln = OPT[n=natural; ":" -> n];
+      tac = subgoal_command -> tac gln ] ]
   ;
   subgoal_command:
     [ [ c = check_command; "." -> c
@@ -66,6 +88,12 @@ GEXTEND Gram
             let g = match g with Some gl -> gl | _ -> 1 in
             VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
+  proof_mode:
+    [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] 
+  ;
+  proof_mode: LAST
+    [ [ c=subgoal_command -> c (Some 1) ] ]
+  ; 
   located_vernac:
     [ [ v = vernac -> loc, v ] ]
   ;
@@ -556,7 +584,9 @@ GEXTEND Gram
       | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
         -> VernacRemoveOption (SecondaryTable (table,field), v)
       | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
-	  VernacRemoveOption (PrimaryTable table, v) ] ]
+	  VernacRemoveOption (PrimaryTable table, v) 
+      | IDENT "proof" -> VernacDeclProof
+      | "return" -> VernacReturn ]]
   ;
   check_command: (* TODO: rapprocher Eval et Check *)
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
@@ -596,7 +626,7 @@ GEXTEND Gram
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
-      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]  
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 92c68ff94e..c3a571a137 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -451,6 +451,12 @@ module Vernac_ =
     let syntax = gec_vernac "syntax_command"
     let vernac = gec_vernac "Vernac_.vernac"
 
+    (* MMode *)
+
+    let proof_instr = Gram.Entry.create "proofmode:instr"
+
+    (* /MMode *)
+
     let vernac_eoi = eoi_entry vernac
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 404f3ab90d..27239599ca 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -196,6 +196,13 @@ module Vernac_ :
     val command : vernac_expr Gram.Entry.e
     val syntax : vernac_expr Gram.Entry.e
     val vernac : vernac_expr Gram.Entry.e
+    
+  (* MMode *)
+
+    val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e
+
+  (*/ MMode *)
+
     val vernac_eoi : vernac_expr Gram.Entry.e
   end
 
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
new file mode 100644
index 0000000000..7e57885cb0
--- /dev/null
+++ b/parsing/ppdecl_proof.ml
@@ -0,0 +1,180 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util 
+open Pp
+open Decl_expr
+open Names 
+open Nameops
+
+let pr_constr = Printer.pr_constr_env
+let pr_tac = Pptactic.pr_glob_tactic
+let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr 
+
+let pr_label = function
+    Anonymous -> mt ()
+  | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () 
+
+let pr_justification env = function
+    Automated [] -> mt ()
+  | Automated (_::_ as l) -> 
+      spc () ++ str "by" ++ spc () ++  
+	prlist_with_sep (fun () -> str ",") (pr_constr env) l
+  | By_tactic tac -> 
+      spc () ++ str "by" ++ spc () ++ str "tactic" ++  pr_tac env tac
+
+let pr_statement pr_it env st = 
+  pr_label st.st_label ++ pr_it env st.st_it
+
+let pr_or_thesis pr_this env = function
+    Thesis Plain -> str "thesis"
+  | Thesis (For id) -> 
+      str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id 
+  | Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]"
+  | This c -> pr_this env c
+
+let pr_cut pr_it env c = 
+  hov 1 (pr_statement pr_it env c.cut_stat) ++ 
+    pr_justification env c.cut_by
+
+let type_or_thesis = function
+    Thesis _ -> Term.mkProp
+  | This c -> c
+
+let _I x = x
+
+let rec print_hyps pconstr gtyp env _and _be hyps = 
+  let _andp = if _and then str "and" ++spc () else mt () in
+    match hyps with 
+	(Hvar _ ::_) as rest -> 
+	  spc () ++ _andp ++ str "we have" ++ 
+	    print_vars pconstr gtyp env false _be rest
+      | Hprop st :: rest -> 
+	  begin
+	    let nenv =
+	      match st.st_label with
+		  Anonymous -> env
+		| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
+	      spc() ++ _andp ++ pr_statement pconstr env st ++ 
+		print_hyps pconstr gtyp nenv true _be rest
+	  end
+      | [] -> mt ()
+
+and print_vars pconstr gtyp env _and _be vars =
+  match vars with
+    Hvar st :: rest -> 
+      begin
+	let nenv = 
+	  match st.st_label with
+	      Anonymous -> anomaly "anonymous variable"
+	    | Name id -> Environ.push_named (id,None,st.st_it) env in
+	let _andp = if _and then pr_coma () else mt () in
+		spc() ++ _andp ++
+		   pr_statement pr_constr env st ++
+		  print_vars pconstr gtyp nenv true _be rest
+      end
+   | (Hprop _ :: _) as rest ->
+      let _st =  if _be then 
+	str "be such that" 
+      else 
+	str "such that" in
+	spc() ++ _st ++  print_hyps pconstr gtyp env false _be rest
+  | [] -> mt ()
+
+let pr_elim_type = function
+    ET_Case_analysis -> str "cases"
+  | ET_Induction -> str "induction"
+
+let pr_casee env =function
+    Real c -> str "on" ++ spc () ++ pr_constr env c
+  | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr env cut
+
+let pr_side = function
+    Lhs -> str "=~"
+  | Rhs -> str "~="
+
+let rec pr_bare_proof_instr _then _thus env = function
+  | Pescape -> str "escape"
+  | Pthen i -> pr_bare_proof_instr true _thus env i 
+  | Pthus i -> pr_bare_proof_instr _then true env i 
+  | Phence i -> pr_bare_proof_instr true true env i
+  | Pcut c -> 
+      begin
+	match _then,_thus with
+	    false,false -> str "have" ++ spc () ++ 
+	      pr_cut (pr_or_thesis pr_constr) env c
+	  | false,true  -> str "thus" ++ spc () ++ 
+	      pr_cut (pr_or_thesis pr_constr) env c
+	  | true,false  -> str "then" ++ spc () ++
+	      pr_cut (pr_or_thesis pr_constr) env c
+	  | true,true   -> str "hence" ++ spc () ++ 
+	      pr_cut (pr_or_thesis pr_constr) env c
+      end
+  | Prew (sid,c) ->
+      (if _thus then str "thus" else str "    ") ++ spc () ++
+	pr_side sid ++ spc () ++ pr_cut pr_constr env c
+  | Passume hyps -> 
+      str "assume" ++ print_hyps pr_constr _I env false false hyps
+  | Plet hyps -> 
+      str "let" ++ print_vars pr_constr _I env false true hyps
+  | Pclaim st ->
+      str "claim" ++ spc () ++ pr_statement pr_constr env st
+  | Pfocus st ->
+      str "focus on" ++ spc () ++ pr_statement pr_constr env st
+  | Pconsider (id,hyps) ->
+      str "consider" ++ print_vars pr_constr _I env false false hyps 
+      ++ spc () ++ str "from " ++ pr_constr env id 
+  | Pgiven hyps ->
+      str "given" ++ print_vars pr_constr _I env false false hyps
+  | Ptake witl -> 
+      str "take" ++ spc () ++ 
+	prlist_with_sep pr_coma (pr_constr env) witl
+  | Pdefine (id,args,body) ->
+      str "define" ++ spc () ++ pr_id id ++ spc () ++ 
+	prlist_with_sep spc 
+	(fun st -> str "(" ++ 
+	   pr_statement pr_constr env st ++ str ")") args ++ spc () ++ 
+	str "as" ++ (pr_constr env body) 
+  | Pcast (id,typ) -> 
+      str "reconsider" ++ spc () ++ 
+	pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ 
+	str "as" ++ (pr_constr env typ)  
+  | Psuppose hyps -> 
+      str "suppose" ++ 
+	print_hyps pr_constr _I env false false hyps
+  | Pcase (params,pat,hyps) ->
+      str "suppose it is" ++ spc () ++ pr_pat pat ++
+	(if params = [] then mt () else 
+	   (spc () ++ str "with" ++ spc () ++ 
+	      prlist_with_sep spc 
+	      (fun st -> str "(" ++ 
+		 pr_statement pr_constr env st ++ str ")") params ++ spc ())) 
+      ++
+	(if hyps = [] then mt () else 
+	   (spc () ++ str "and" ++ 
+	      print_hyps (pr_or_thesis pr_constr) type_or_thesis
+	      env false false hyps))
+  | Pper (et,c) -> 
+      str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
+      pr_casee env c
+  | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
+  | _ -> anomaly "unprintable instruction"
+
+let pr_emph = function
+    0 -> str "    "
+  | 1 -> str "*   "
+  | 2 -> str "**  "
+  | 3 -> str "*** "
+  | _ -> anomaly "unknown emphasis"
+
+let pr_proof_instr env instr = 
+  pr_emph instr.emph ++ spc () ++ 
+    pr_bare_proof_instr false false env instr.instr
+
diff --git a/parsing/ppdecl_proof.mli b/parsing/ppdecl_proof.mli
new file mode 100644
index 0000000000..b0f0e110ce
--- /dev/null
+++ b/parsing/ppdecl_proof.mli
@@ -0,0 +1,2 @@
+
+val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds  
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 5e13a11245..c749223519 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -410,6 +410,7 @@ let rec pr_vernac = function
 	| ShowProofNames -> str"Show Conjectures"
 	| ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
 	| ShowMatch id -> str"Show Match " ++ pr_lident id
+	| ShowThesis -> str "Show Thesis"
 	| ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l
 	| ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l 
       in pr_showable s
@@ -681,6 +682,14 @@ let rec pr_vernac = function
   | VernacSolveExistential (i,c) ->
       str"Existential " ++ int i ++ pr_lconstrarg c
 
+  (* MMode *)
+ 
+  | VernacProofInstr instr -> anomaly "Not implemented"
+  | VernacDeclProof -> str "proof" 
+  | VernacReturn -> str "return"
+
+  (* /MMode *) 
+
   (* Auxiliary file and library management *)
   | VernacRequireFrom (exp,spe,f) -> hov 2
       (str"Require" ++ spc() ++ pr_require_token exp ++
diff --git a/parsing/printer.ml b/parsing/printer.ml
index e1c8b2505e..1b069c5ee1 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -23,6 +23,7 @@ open Nametab
 open Ppconstr
 open Evd
 open Proof_type
+open Decl_mode
 open Refiner
 open Pfedit
 open Ppconstr
@@ -108,6 +109,13 @@ let pr_evaluable_reference ref =
   | EvalVarRef sp -> VarRef sp in
  pr_global ref'
 
+(*let pr_rawterm t =
+  pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*)
+
+(*open Pattern
+
+let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
+
 (**********************************************************************)
 (* Contexts and declarations                                          *)
 
@@ -219,23 +227,53 @@ let pr_context_of env = match Options.print_hyps_limit () with
   | None -> hv 0 (pr_context_unlimited env)
   | Some n -> hv 0 (pr_context_limit n env)
 
+(* display goal parts (Proof mode) *)
+
+let pr_restricted_named_context among env =
+  hv 0 (fold_named_context
+	  (fun env ((id,_,_) as d) pps ->
+	     if true || Idset.mem id among then
+	       pps ++ 
+		 fnl () ++ str (emacs_str (String.make 1 (Char.chr 253))) ++
+		 pr_var_decl env d
+	     else 
+	       pps)
+          env ~init:(mt ()))
+
+let pr_subgoal_metas metas env=
+  let pr_one (meta,typ) = 
+    str "?" ++ int meta ++ str " : " ++ 
+      hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ 
+      str (emacs_str (String.make 1 (Char.chr 253))) in
+    hv 0 (prlist_with_sep mt pr_one metas)
 
 (* display complete goal *)
 let pr_goal g =
   let env = evar_env g in
-  let penv = pr_context_of env in
-  let pc = pr_ltype_env_at_top env g.evar_concl in
-  str"  " ++ hv 0 (penv ++ fnl () ++
-		   str (emacs_str (String.make 1 (Char.chr 253)))  ++
-                   str "============================" ++ fnl ()  ++
-                   str" "  ++ pc) ++ fnl ()
-
+  let preamb,penv,pc =
+    if g.evar_extra = None then
+          mt (),
+	  pr_context_of env,
+	  pr_ltype_env_at_top env g.evar_concl
+    else 
+      let {pm_subgoals=metas;pm_hyps=among} = get_info g in
+	(str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
+    pr_restricted_named_context among env,
+    pr_subgoal_metas metas env
+  in
+    preamb ++
+    str"  " ++ hv 0 (penv ++ fnl () ++
+		       str (emacs_str (String.make 1 (Char.chr 253)))  ++
+		       str "============================" ++ fnl ()  ++
+		       str" "  ++ pc) ++ fnl ()
+     
 (* display the conclusion of a goal *)
 let pr_concl n g =
   let env = evar_env g in
   let pc = pr_ltype_env_at_top env g.evar_concl in
-  str (emacs_str (String.make 1 (Char.chr 253)))  ++
-  str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
+    str (emacs_str (String.make 1 (Char.chr 253)))  ++
+      str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
+
 
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl = 
@@ -266,15 +304,22 @@ let pr_subgoal n =
   prrec n
 
 (* Print open subgoals. Checks for uninstantiated existential variables *)
-let pr_subgoals sigma = function 
+let pr_subgoals close_cmd sigma = function 
   | [] -> 
-      let exl = Evarutil.non_instantiated sigma in 
-      if exl = [] then 
-	(str"Proof completed."  ++ fnl ())
-      else
-        let pei = pr_evars_int 1 exl in
-        (str "No more subgoals but non-instantiated existential " ++
-           str "variables :"  ++fnl () ++ (hov 0 pei))
+      begin
+	match close_cmd with
+	  Some cmd ->
+	    (str "Subproof completed, now type " ++ str cmd ++ 
+	       str "." ++ fnl ())
+	| None ->
+	    let exl = Evarutil.non_instantiated sigma in 
+	      if exl = [] then 
+		(str"Proof completed."  ++ fnl ())
+	      else
+		let pei = pr_evars_int 1 exl in
+		  (str "No more subgoals but non-instantiated existential " ++
+		     str "variables :"  ++fnl () ++ (hov 0 pei))
+      end
   | [g] ->
       let pg = pr_goal g in
       v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
@@ -291,12 +336,12 @@ let pr_subgoals sigma = function
       v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
 	   ++ pg1 ++ prest ++ fnl ())
 
-
-let pr_subgoals_of_pfts pfts = 
+let pr_subgoals_of_pfts pfts =
+  let close_cmd = Decl_mode.get_end_command pfts in
   let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in 
   let sigma = (top_goal_of_pftreestate pfts).sigma in
-  pr_subgoals sigma gls
-
+    pr_subgoals close_cmd sigma gls
+      
 let pr_open_subgoals () =
   let pfts = get_pftreestate () in
   match focus() with
@@ -351,7 +396,6 @@ let pr_prim_rule = function
 	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
         | [] -> mt () in
       (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
-
   | Refine c -> 
       str(if occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
diff --git a/parsing/printer.mli b/parsing/printer.mli
index cd9b526a48..c63d7d71f0 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -87,7 +87,7 @@ val pr_context_of          : env -> std_ppcmds
 (* Proofs *)
 
 val pr_goal                : goal -> std_ppcmds
-val pr_subgoals            : evar_map -> goal list -> std_ppcmds
+val pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds
 val pr_subgoal             : int -> goal list -> std_ppcmds
 
 val pr_open_subgoals       : unit -> std_ppcmds
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index c003500533..e1cc8463c3 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -15,6 +15,7 @@ open Evd
 open Tacexpr
 open Proof_type
 open Proof_trees
+open Decl_expr
 open Logic
 open Printer
 
@@ -25,9 +26,19 @@ let pr_tactic = function
   | t -> 
       Pptactic.pr_tactic (Global.env()) t
 
+let pr_proof_instr instr = 
+    Ppdecl_proof.pr_proof_instr (Global.env()) instr
+
 let pr_rule = function
   | Prim r -> hov 0 (pr_prim_rule r)
-  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
+  | Nested(cmpd,_) ->
+      begin
+	match cmpd with 
+	    Tactic texp -> hov 0 (pr_tactic texp)
+	  | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
+      end
+  | Daimon -> str "<Daimon>"
+  | Decl_proof _ -> str "proof" 
   | Change_evars ->
       (* This is internal tactic and cannot be replayed at user-level.
          Function pr_rule_dot below is used when we want to hide
@@ -52,59 +63,145 @@ let thin_sign osign sign =
     sign ~init:Environ.empty_named_context_val
 
 let rec print_proof sigma osign pf =
-  let {evar_hyps=hyps; evar_concl=cl; 
-       evar_body=body} = pf.goal in
-  let hyps = Environ.named_context_of_val hyps in
+  let hyps = Environ.named_context_of_val pf.goal.evar_hyps in
   let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
-	hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body})
+	hov 0 (pr_goal {pf.goal with evar_hyps=hyps'})
     | Some(r,spfl) ->
     	hov 0 
-	  (hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++
+	  (hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++
 	   spc () ++ str" BY " ++
 	   hov 0 (pr_rule r) ++ fnl () ++
 	   str"  " ++
-	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
-)
+	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl))
 	  
 let pr_change gl = 
-  str"Change " ++
+  str"change " ++
   pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
 
-let rec print_script nochange sigma osign pf =
-  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
-  let sign = Environ.named_context_of_val sign in
+let rec print_decl_script tac_printer nochange sigma pf =
+  match pf.ref with
+    | None ->
+	(if nochange then 
+	   (str"<Your Proof Text here>")
+	 else 
+	   pr_change pf.goal)
+	++ fnl ()
+    | Some (Daimon,_) -> mt ()
+    | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
+	begin
+	  match instr.instr,subprfs with
+	    Pescape,[{ref=Some(_,subsubprfs)}] ->
+	      hov 7
+		(pr_rule_dot rule ++ fnl () ++
+		   prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
+		if opened then mt () else str "return."
+	  | Pclaim _,[body;cont] ->
+	      hov 2
+		(pr_rule_dot rule ++ fnl () ++
+		   print_decl_script tac_printer nochange sigma body) ++ 
+		fnl () ++
+		if opened then mt () else str "end claim." ++ fnl () ++
+		  print_decl_script tac_printer nochange sigma cont
+	  | Pfocus _,[body;cont] ->
+	      hov 2 
+		(pr_rule_dot rule ++ fnl () ++
+		   print_decl_script tac_printer nochange sigma body) ++ 
+		fnl () ++
+		if opened then mt () else str "end focus." ++ fnl () ++
+		  print_decl_script tac_printer nochange sigma cont
+	  | (Psuppose _ |Pcase (_,_,_)),[body;cont] ->
+	      hov 2 
+		(pr_rule_dot rule ++ fnl () ++
+		   print_decl_script tac_printer nochange sigma body) ++ 
+		fnl () ++
+		print_decl_script tac_printer nochange sigma cont 
+	  | _,[next] ->
+	      pr_rule_dot rule ++ fnl () ++
+		print_decl_script tac_printer nochange sigma next
+	  | _,[] ->
+	      pr_rule_dot rule		
+	  | _,_ -> anomaly "unknown branching instruction"
+	end
+    | _ -> anomaly "Not Applicable"
+
+let rec print_script nochange sigma pf =
   match pf.ref with
     | None ->
         (if nochange then 
-	  (str"<Your Tactic Text here>") 
-	else 
-	  pr_change pf.goal)
+	   (str"<Your Tactic Text here>") 
+	 else 
+	   pr_change pf.goal)
 	++ fnl ()
-    | Some(r,spfl) ->
-        ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
-           pr_rule_dot r ++ fnl () ++
-           prlist_with_sep pr_fnl
-             (print_script nochange sigma sign) spfl)
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) 
+	end ++
+	  begin
+	    hov 0 (str "proof." ++ fnl () ++ 
+		     print_decl_script (print_script nochange sigma) 
+		     nochange sigma (List.hd script))
+	  end ++ fnl () ++
+	  begin
+	    if opened then mt () else (str "end proof." ++ fnl ())
+	  end
+    | Some(Daimon,spfl) ->
+	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+	   prlist_with_sep pr_fnl
+           (print_script nochange sigma) spfl )
+    | Some(rule,spfl) ->
+	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+	   pr_rule_dot rule ++ fnl () ++
+	   prlist_with_sep pr_fnl
+           (print_script nochange sigma) spfl )	
 
 (* printed by Show Script command *)
-let print_treescript nochange sigma _osign pf =
+
+let print_treescript nochange sigma pf =
   let rec aux top pf =
     match pf.ref with
     | None ->
         if nochange then 
-	  (str"<Your Tactic Text here>") 
+	  if pf.goal.evar_extra=None then
+	    (str"<Your Tactic Text here>")
+	  else (str"<Your Proof Text here>")
 	else 
 	  (pr_change pf.goal)
+    | Some(Decl_proof opened,script) ->
+	assert (List.length script = 1);
+	begin
+	  if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())
+	end ++
+	  hov 0 
+	  begin str "proof." ++ fnl () ++
+	    print_decl_script (aux false)  
+	    nochange sigma (List.hd script) 
+	  end ++ fnl () ++ 
+	  begin
+	    if opened then mt () else (str "end proof." ++ fnl ())
+	  end
+    | Some(Daimon,spfl) ->
+	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
+	   prlist_with_sep pr_fnl
+           (print_script nochange sigma) spfl )
     | Some(r,spfl) ->
         (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
-	pr_rule_dot r ++
-	match spfl with
-	| [] -> mt ()
-	| [spf] -> fnl () ++ (if top then mt () else str "  ") ++ aux top spf
-	| _ -> fnl () ++ str " " ++
-	    hov 0 (prlist_with_sep fnl (aux false) spfl)
+	  pr_rule_dot r ++ fnl () ++
+	  begin
+	    if List.length spfl > 1 then
+	      fnl ()  ++ 
+		str " " ++  hov 0 (aux false (List.hd spfl)) ++ fnl () ++
+		hov 0 (prlist_with_sep fnl (aux false) (List.tl spfl))
+	    else
+	      match spfl with
+		| [] -> mt ()
+		| [spf] -> fnl () ++ 
+		    (if top then mt () else str "  ") ++ aux top spf
+		| _ -> fnl () ++ str " " ++
+		    hov 0 (prlist_with_sep fnl (aux false) spfl)
+	  end
   in hov 0 (aux true pf)
 
 let rec print_info_script sigma osign pf =
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index b4ad0143ef..4e78a96875 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -22,6 +22,6 @@ val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
 val pr_rule     : rule -> std_ppcmds
 val pr_tactic   : tactic_expr -> std_ppcmds
 val print_script :
-  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
+  bool -> evar_map -> proof_tree -> std_ppcmds
 val print_treescript :
-  bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
+  bool -> evar_map -> proof_tree -> std_ppcmds