module Printer

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

1 files changed, 238 insertions, 0 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
new file mode 100644
index 0000000000..ba4d06e810
--- /dev/null
+++ b/parsing/printer.ml
@@ -0,0 +1,238 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Sign
+open Global
+open Declare
+open Coqast
+
+let print_arguments = ref false
+let print_casts = ref false
+let print_emacs = ref false
+
+let emacs_str s =
+  if !print_emacs then s else "" 
+
+let section_path sl s =
+  let sl = List.rev sl in
+  make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)
+
+let with_implicits f x =
+  let oimpl = !Termast.print_implicits in
+  Termast.print_implicits := true; 
+  try
+    let r = f x in
+    Termast.print_implicits := oimpl;
+    r
+  with e -> 
+    Termast.print_implicits := oimpl; raise e
+
+let pr_global dflt k oper =
+  try 
+    let id = id_of_global oper in
+    if is_existential_oper oper then
+      [< 'sTR (string_of_id id) >]
+    else 
+      let (oper',_) = global_operator (Nametab.sp_of_id k id) id in 
+      if oper = oper' then
+        [< 'sTR(string_of_id id) >]
+      else 
+	dflt
+  with 
+    | Failure _ | Not_found ->
+	[< 'sTR"[Error printing " ; dflt ; 'sTR"]" >]
+    | _ -> 
+	[< 'sTR"Error [Nasty error printing " ; dflt ; 'sTR"]" >]
+
+let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >]
+
+let globpr k gt = match gt with
+  | Nvar(_,s) -> [< 'sTR s >]
+  | Node(_,"CONST",(Path(_,sl,s))::_) ->
+      if !print_arguments then 
+	dfltpr gt
+      else 
+	pr_global (dfltpr gt) k (Const (section_path sl s))
+  | Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) ->
+      if !print_arguments then 
+	(dfltpr gt)
+      else 
+	pr_global (dfltpr gt) k (MutInd(section_path sl s,tyi))
+  | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) ->
+      if !print_arguments then 
+	(dfltpr gt)
+      else 
+	pr_global (dfltpr gt) k (MutConstruct((section_path sl s,tyi),i))
+  | gt -> dfltpr gt
+
+let apply_prec = Some (("Term",(9,0,0)),Extend.L)
+let apply_tacprec = Some (("Tactic",(9,0,0)),Extend.L)
+
+let rec gencompr k gt =
+  let uni = match k with
+    | CCI | FW -> "constr"
+    | _ -> "<undefined>" 
+  in
+  let rec gpr gt =
+    Esyntax.genprint uni
+      (function
+         | Node(_,"PPUNI$COMMAND",[Str(_,"CCI");c]) -> gencompr CCI c
+         | Node(_,"PPUNI$COMMAND",[c]) -> gencompr CCI c
+         | Node(_,"PPUNI$COMMAND",[Str(_,"FW");c]) -> gencompr FW c
+         | gt -> globpr k gt)
+      apply_prec
+      gt
+  in 
+  gpr gt
+
+(* [at_top] means ids of env must be avoided in bound variables *)
+let gentermpr_core at_top k env t =
+  let uenv = unitize_env env in
+  try 
+    let ogt = 
+      if !print_casts then 
+	Termast.bdize at_top uenv t
+      else 
+	Termast.bdize_no_casts at_top uenv t
+    in 
+    gencompr k ogt
+  with Failure _ | Anomaly _ | UserError _ | Not_found ->
+    [< 'sTR"<PP error: non-printable term>" >]
+
+let term0_at_top a = gentermpr_core true CCI a
+let gentermpr a = gentermpr_core false a
+
+let term0 a = gentermpr CCI a
+let prterm = term0 (gLOB nil_sign)
+let fterm0 a = gentermpr FW a
+let fprterm = fterm0 (gLOB nil_sign)
+
+let prtype_env env typ =
+  if !print_casts then 
+    term0 env (mkCast typ.body (mkSort typ.typ))
+  else 
+    prterm typ.body
+
+let prtype = prtype_env (gLOB nil_sign)
+
+let fprtype_env env typ =
+  if !print_casts then 
+    fterm0 env (mkCast typ.body (mkSort typ.typ))
+  else 
+    fterm0 env typ.body
+
+let fprtype = fprtype_env (gLOB nil_sign)
+
+let gentacpr gt =
+  let rec gpr gt =
+    Esyntax.genprint "tactic"
+      (function 
+         | Nvar(_,s) -> [< 'sTR s >]
+         | Node(_,"PPUNI$COMMAND",[Str(_,"CCI");c]) -> gencompr CCI c
+         | Node(_,"PPUNI$COMMAND",[c]) -> gencompr CCI c
+         | Node(_,"PPUNI$COMMAND",[Str(_,"FW");c]) -> gencompr FW c
+         | gt -> default_tacpr gt)
+      apply_tacprec
+      gt
+  and default_tacpr = function
+    | Node(_,s,[]) -> [< 'sTR s >]
+    | Node(_,s,ta) ->
+	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gpr ta) >]
+    | gt -> dfltpr gt
+  in 
+  gpr gt
+
+let print_decl k sign (s,typ) =
+  let ptyp = gentermpr k (gLOB sign) typ.body in
+  [< print_id s ; 'sTR" : "; ptyp >]
+
+let print_binding k env (na,typ) =
+  let ptyp = gentermpr k env typ.body in
+  match na with
+    | Anonymous -> [< 'sTR"<>" ; 'sTR" : " ; ptyp >]
+    | Name id -> [< print_id id ; 'sTR" : "; ptyp >]
+
+
+(* Prints out an "env" in a nice format.  We print out the
+ * signature,then a horizontal bar, then the debruijn environment.
+ * It's printed out from outermost to innermost, so it's readable. *)
+
+let sign_it_with f sign e =
+  snd (sign_it (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e))
+         sign (nil_sign,e))
+
+let sign_it_with_i f sign e =
+  let (_,_,e') = 
+    (sign_it (fun id t (i,sign,e) -> (i+1,add_sign (id,t) sign,
+				      f i id t sign e))
+       sign (0,nil_sign,e))
+  in 
+  e'
+
+let dbenv_it_with f env e =
+  snd (dbenv_it (fun na t (env,e) -> (add_rel (na,t) env, f na t env e))
+         env (gLOB(get_globals env),e))
+
+(* Prints a signature, all declarations on the same line if possible *)
+let pr_sign sign =
+  hV 0 [< (sign_it_with (fun id t sign pps ->
+                           [<  pps ; 'wS 2 ; print_decl CCI sign (id,t) >])
+             sign) [< >] >]
+
+(* Prints an env (variables and de Bruijn). Separator: newline *)
+let pr_env k env =
+  let sign_env =
+    sign_it_with
+      (fun id t sign pps ->
+         let pidt =  print_decl k sign (id,t) in [<  pps ; 'fNL ; pidt >])
+      (get_globals env) [< >] 
+  in
+  let db_env =
+    dbenv_it_with 
+      (fun na t env pps ->
+         let pnat = print_binding k env (na,t) in [<  pps ; 'fNL ; pnat >])
+      env [< >]
+  in 
+  [< sign_env; db_env >]
+
+let pr_ne_env header k = function
+  | ENVIRON (([],[]),[]) -> [< >]
+  | env -> let penv = pr_env k env in [< header; penv >]
+
+let pr_env_limit n env =
+  let sign = get_globals env in
+  let lgsign = sign_length sign in
+  if n >= lgsign then 
+    pr_env CCI env
+  else
+    let k = lgsign-n in
+    let sign_env =
+      sign_it_with_i
+        (fun i id t sign pps -> 
+           if i < k then 
+	     [< pps ;'sTR "." >] 
+	   else
+             let pidt = print_decl CCI sign (id,t) in
+	     [< pps ; 'fNL ;
+		'sTR (emacs_str (String.make 1 (Char.chr 253)));
+		pidt >])
+        (get_globals env) [< >] 
+    in
+    let db_env =
+      dbenv_it_with
+        (fun na t env pps ->
+           let pnat = print_binding CCI env (na,t) in
+	   [< pps ; 'fNL ;
+	      'sTR (emacs_str (String.make 1 (Char.chr 253)));
+	      pnat >])
+        env [< >]
+    in 
+    [< sign_env; db_env >]
+
+let pr_env_opt env =  match Options.print_hyps_limit () with 
+  | None -> hV 0 (pr_env CCI env)
+  | Some n -> hV 0 (pr_env_limit n env)