1 files changed, 218 insertions, 30 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 76430e1c4..6dd9211bb 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -1,25 +1,26 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                          The Coq Proof Assistant                         *)
-(*                                                                          *)
-(*                                 Projet Coq                               *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(****************************************************************************)
-
-(* $:Id$ *)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
+(* $Id$ *)
+
+(*i*)
 open Ast
+open Util
 open Pp
 open Nametab
 open Names
 open Nameops
 open Libnames
 open Coqast
-open Extend
-open Util
+open Ppextend
+open Topconstr
+open Term
+(*i*)
 
 let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
 
@@ -70,25 +71,190 @@ let wrap_exception = function
       str"<PP error: non-printable term>"
   | s -> raise s
 
-let constr_syntax_universe = "constr"
-(* This is starting precedence for printing constructions or tactics *)
-(* Level 9 means no parentheses except for applicative terms (at level 10) *)
-let constr_initial_prec = Some ((constr_syntax_universe,(9,0,0)),Extend.L)
+let latom = 0
+let lannot = 1
+let lprod = 8
+let lcast = 9
+let lapp = 10
+let ltop = (8,E)
 
-let gentermpr_fail gt =
-  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt
+let prec_less child (parent,assoc) =
+  (if assoc = E then (<=) else (<)) child parent
 
-let gentermpr gt =
-  try gentermpr_fail gt
-  with s -> wrap_exception s
+let env_assoc_value v env =
+  try List.assoc v env
+  with Not_found ->
+    anomaly ("Printing metavariable "^(string_of_id v)^" is unbound")
 
-(* [at_top] means ids of env must be avoided in bound variables *)
-let gentermpr_core at_top env t =
-  gentermpr (Termast.ast_of_constr at_top env t)
+open Symbols
+
+let rec print_hunk pr env = function
+  | UnpMetaVar (e,prec) -> pr prec (env_assoc_value e env)
+  | UnpTerminal s -> str s
+  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk pr env) sub)
+  | UnpCut cut -> ppcmd_of_cut cut
+
+let pr_notation pr s env =
+  let unpl, level = find_notation_printing_rule s in
+  prlist (print_hunk pr env) unpl, level
+
+let pr_delimiters x = failwith "pr_delimiters: TODO"
+
+open Rawterm
+
+let pr_opt pr = function
+  | None -> mt ()
+  | Some x -> spc () ++ pr x
+
+let pr_universe u = str "<univ>"
+
+let pr_sort = function
+  | RProp Term.Null -> str "Prop"
+  | RProp Term.Pos -> str "Set"
+  | RType u -> str "Type" ++ pr_opt pr_universe u
+
+let pr_explicitation = function
+  | None -> mt ()
+  | Some n -> int n ++ str "!"
+
+let pr_expl_args pr (a,expl) =
+  pr_explicitation expl ++ pr (latom,E) a
+
+let pr_opt_type pr = function
+  | CHole _ -> mt ()
+  | t -> cut () ++ str ":" ++ pr ltop t
+
+let pr_tight_coma () = str "," ++ cut ()
+
+let pr_name = function
+  | Anonymous -> mt ()
+  | Name id -> pr_id id
+
+let pr_located pr (loc,x) = pr x
 
-let pr_constr = gentermpr
+let pr_let_binder pr x a =
+  hv 0 (
+    str "[" ++ brk(0,1) ++
+    pr_name x ++ brk(0,1) ++
+    str ":=" ++ brk(0,1) ++
+    pr ltop a ++ brk(0,1) ++
+    str "]")
 
-let pr_pattern = gentermpr
+let pr_binder pr (nal,t) =
+  hov 0 (
+    prlist_with_sep pr_tight_coma (pr_located pr_name) nal ++
+    pr_opt_type pr t)
+
+let pr_binders pr bl =
+  hv 0 (prlist_with_sep pr_semicolon (pr_binder pr) bl)
+
+let pr_recursive_decl pr id b t c =
+  pr_id id ++
+  brk (1,2) ++ str ": " ++ pr ltop t ++ str ":=" ++
+  brk (1,2) ++ pr ltop c
+
+let pr_fixdecl pr (id,bl,t,c) =
+  pr_recursive_decl pr id 
+    (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c
+
+let pr_cofixdecl pr (id,t,c) =
+  pr_recursive_decl pr id (mt ()) t c
+
+let pr_recursive s pr_decl id = function
+  | [] -> anomaly "(co)fixpoint with no definition"
+  | d1::dl ->
+      hov 0 (
+	str "Fix " ++ pr_id id ++ brk (0,2) ++ str "{" ++
+	(v 0 (
+	  (hov 0 (pr_decl d1)) ++
+	  (prlist (fun fix -> fnl () ++ hov 0 (str "with" ++ pr_decl fix))
+	    dl))) ++
+	str "}")
+
+let pr_fix pr = pr_recursive "Fix" (pr_fixdecl pr)
+let pr_cofix pr = pr_recursive "Fix" (pr_cofixdecl pr)
+
+let rec pr_arrow pr = function
+  | CArrow (_,a,b) -> pr (lprod,L) a ++ cut () ++ str "->" ++ pr_arrow pr b
+  | a -> pr (lprod,E) a
+
+let pr_annotation pr t = str "<" ++ pr ltop t ++ str ">"
+
+let pr_cases _ _ _ = str "<CASES(TODO)>"
+
+let rec pr inherited a =
+  let (strm,prec) = match a with
+  | CRef r -> pr_reference r, latom
+  | CFix (_,id,fix) -> pr_fix pr (snd id) fix, latom
+  | CCoFix (_,id,cofix) -> pr_cofix pr (snd id) cofix, latom
+  | CArrow _ -> hv 0 (pr_arrow pr a), lprod
+  | CProdN (_,bl,a) ->
+      hov 0 (
+	str "(" ++ pr_binders pr bl ++ str ")" ++ brk(0,1) ++ pr ltop a), lprod
+  | CLambdaN (_,bl,a) ->
+      hov 0 (
+	str "[" ++ pr_binders pr bl ++ str "]" ++ brk(0,1) ++ pr ltop a), lprod
+  | CLetIn (_,x,a,b) ->
+      hov 0 (pr_let_binder pr (snd x) a ++ cut () ++ pr ltop b), lprod
+  | CAppExpl (_,f,l) ->
+      hov 0 (
+	str "!" ++ pr_reference f ++ 
+	prlist (fun a -> brk (1,1) ++ pr (latom,E) a) l), lapp
+  | CApp (_,a,l) ->
+      hov 0 (
+	pr (latom,E) a ++ 
+	prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp
+  | CCases (_,po,c,eqns) ->
+      pr_cases po c eqns, lannot
+  | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
+      (* On force les parenthèses autour d'un "if" sous-terme (même si le
+	 parsing est lui plus tolérant) *)
+      hov 0 (
+	pr_opt (pr_annotation pr) po ++
+	hv 0 (
+	  str "if" ++ pr ltop c ++ spc () ++
+	  hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
+	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lapp
+  | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,_ as bd],b)]) ->
+      hov 0 (
+	pr_opt (pr_annotation pr) po ++
+	hv 0 (
+          str "let" ++ brk (1,1) ++
+	  hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++
+	  str "=" ++ brk (1,1) ++
+	  pr ltop c ++ spc () ++
+	  str "in " ++ pr ltop b)), lapp
+  | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
+      hov 0 (
+	hov 0 (
+	pr_opt (pr_annotation pr) po ++ brk (0,2) ++
+	  hov 0 (
+	    str (if style=RegularStyle then "Case" else "Match") ++ 
+	    brk (1,1) ++ pr ltop c ++ spc () ++
+	    str (if style=RegularStyle then "of" else "with") ++
+	  brk (1,3) ++
+	  hov 0 (prlist (fun b -> pr ltop b ++ fnl ()) bl)) ++
+	str "end")), lannot
+  | COrderedCase (_,_,_,_,_) -> 
+      anomaly "malformed if or destructuring let"
+  | CHole _ -> str "?", latom
+  | CMeta (_,p) -> str "?" ++ int p, latom
+  | CSort (_,s) -> pr_sort s, latom
+  | CCast (_,a,b) ->
+      hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast
+  | CNotation (_,s,env) -> pr_notation pr s env
+  | CGrammar _ -> failwith "CGrammar: TODO"
+  | CNumeral (_,p) -> Bignat.pr_bigint p, latom
+  | CDelimiters (_,sc,a) -> failwith "pr_delim: TODO"
+(*      pr_delimiters (find_delimiters) (pr_constr_expr a)*)
+  | CDynamic _ -> str "<dynamic>", latom
+  in
+  if prec_less prec inherited then strm
+  else str"(" ++ strm ++ str")"
+  
+let pr_constr = pr ltop
+
+let pr_pattern x = (* gentermpr*) failwith "pr_pattern: TODO"
 
 let pr_qualid qid = str (string_of_qualid qid)
 
@@ -110,7 +276,7 @@ let pr_red_flag pr r =
 open Genarg
 
 let pr_metanum pr = function
-  | AN (_,x) -> pr x
+  | AN x -> pr x
   | MetaNum (_,n) -> str "?" ++ int n
 
 let pr_red_expr (pr_constr,pr_ref) = function
@@ -139,7 +305,7 @@ let pr_red_expr (pr_constr,pr_ref) = function
 let rec pr_may_eval pr = function
   | ConstrEval (r,c) ->
       hov 0
-        (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr_metanum pr_qualid) r ++
+        (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr_metanum pr_reference) r ++
 	 spc () ++ str "in" ++ brk (1,1) ++ pr c)
   | ConstrContext ((_,id),c) ->
       hov 0
@@ -147,3 +313,25 @@ let rec pr_may_eval pr = function
 	 str "[" ++ pr c ++ str "]")
   | ConstrTypeOf c -> hov 0 (str "Check " ++ brk (1,1) ++ pr c)
   | ConstrTerm c -> pr c
+
+(**********************************************************************)
+let constr_syntax_universe = "constr"
+(* This is starting precedence for printing constructions or tactics *)
+(* Level 9 means no parentheses except for applicative terms (at level 10) *)
+let constr_initial_prec = Some (9,Ppextend.L)
+
+let gentermpr_fail gt =
+  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt
+
+let gentermpr gt =
+  try gentermpr_fail gt
+  with s -> wrap_exception s
+
+(* [at_top] means ids of env must be avoided in bound variables *)
+let gentermpr_core at_top env t =
+  gentermpr (Termast.ast_of_constr at_top env t)
+(*
+let gentermpr_core at_top env t =
+  pr_constr (Constrextern.extern_constr at_top env t)
+*)
+