matita/components/ng_extraction/ocaml.ml

   1 (************************************************************************)
   2 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
   3 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
   4 (*   \VV/  **************************************************************)
   5 (*    //   *      This file is distributed under the terms of the       *)
   6 (*         *       GNU Lesser General Public License Version 2.1        *)
   7 (************************************************************************)
   8
   9 (*i $Id: ocaml.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 (*s Production of Ocaml syntax. *)
  12
  13 open OcamlExtractionTable
  14 open Coq
  15 open Miniml
  16 open Mlutil
  17 open Common
  18
  19
  20 (*s Some utility functions. *)
  21
  22 let pp_tvar id =
  23   let s = id in
  24   if String.length s < 2 || s.[1]<>'\''
  25   then str ("'"^s)
  26   else str ("' "^s)
  27
  28 let pp_tuple_light status f = function
  29   | [] -> status,mt ()
  30   | [x] -> f status true x
  31   | l ->
  32      let status,res =
  33       prlist_with_sep_status status
  34        (fun () -> str "," ++ spc ()) (fun status -> f status false) l in
  35      status, pp_par true res
  36
  37 let pp_tuple status f = function
  38   | [] -> status,mt ()
  39   | [x] -> f status x
  40   | l ->
  41      let status,res =
  42       prlist_with_sep_status status (fun () -> str "," ++ spc ()) f l in
  43      status,pp_par true res
  44
  45 let pp_boxed_tuple f = function
  46   | [] -> mt ()
  47   | [x] -> f x
  48   | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
  49
  50 let pp_abst = function
  51   | [] -> mt ()
  52   | l  ->
  53       str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
  54       str " ->" ++ spc ()
  55
  56 let pp_parameters l =
  57   (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
  58
  59 (*s Ocaml renaming issues. *)
  60
  61 let keywords =
  62   List.fold_right Idset.add
  63   [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
  64     "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
  65     "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
  66     "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
  67     "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
  68     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
  69     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
  70     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
  71   Idset.empty
  72 ;;
  73
  74 set_keywords keywords;;
  75
  76 let pp_open status filename =
  77  let status,res = modname_of_filename status true filename in
  78  status, str ("open " ^ res  ^ "\n") ++ fnl ()
  79
  80 (*s The pretty-printer for Ocaml syntax*)
  81
  82 (* Beware of the side-effects of [pp_global] and [pp_modname].
  83    They are used to update table of content for modules. Many [let]
  84    below should not be altered since they force evaluation order.
  85 *)
  86
  87 let str_global status k r =
  88  (*CSC: if is_inline_custom r then find_custom r else*) Common.pp_global status k r
  89
  90 let pp_global status k r =
  91  let status,res = str_global status k r in
  92   status,str res
  93
  94 (*CSC
  95 let pp_modname mp = str (Common.pp_module mp)
  96
  97 let is_infix r =
  98   is_inline_custom r &&
  99   (let s = find_custom r in
 100    let l = String.length s in
 101    l >= 2 && s.[0] = '(' && s.[l-1] = ')')
 102
 103 let get_infix r =
 104   let s = find_custom r in
 105   String.sub s 1 (String.length s - 2)
 106 *)
 107
 108 let pp_one_field status _r _i r = pp_global status Term r
 109
 110 let pp_field status r fields i = pp_one_field status r i (List.nth fields i)
 111
 112 let pp_fields status r fields =
 113  list_map_i_status status (fun status -> pp_one_field status r) 0 fields
 114
 115 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
 116     are needed or not. *)
 117
 118 let pp_type status par vl t =
 119   let rec pp_rec status par = function
 120     | Tmeta _ | Tvar' _ | Taxiom -> assert false
 121     | Tvar i -> (try status,pp_tvar (List.nth vl (pred i))
 122                  with _ -> status,(str "'a" ++ int i))
 123 (*CSC:
 124     | Tglob (r,[a1;a2]) when is_infix r ->
 125         pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
 126 *)
 127     | Tglob (r,[]) -> pp_global status Type r
 128 (*CSC:
 129     | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" ->
 130         pp_tuple_light pp_rec l
 131 *)
 132     | Tglob (r,l) ->
 133        let status,res = pp_tuple_light status pp_rec l in
 134        let status,res2 = pp_global status Type r in
 135        status,res ++ spc () ++ res2
 136     | Tarr (t1,t2) ->
 137        let status,res = pp_rec status true t1 in
 138        let status,res2 = pp_rec status false t2 in
 139        status,pp_par par (res ++ spc () ++ str "->" ++ spc () ++ res2)
 140     | Tdummy _ -> status,str "__"
 141     | Tunknown -> status,str "__"
 142   in
 143   let status,res = pp_rec status par t in
 144    status,hov 0 res
 145
 146 (*s Pretty-printing of expressions. [par] indicates whether
 147     parentheses are needed or not. [env] is the list of names for the
 148     de Bruijn variables. [args] is the list of collected arguments
 149     (already pretty-printed). *)
 150
 151 let is_ifthenelse = function
 152 (*CSC:
 153   | [|(r1,[],_);(r2,[],_)|] ->
 154       (try (find_custom r1 = "true") && (find_custom r2 = "false")
 155        with Not_found -> false)*)
 156   | _ -> false
 157
 158 let expr_needs_par = function
 159   | MLlam _  -> true
 160   | MLcase (_,_,[|_|]) -> false
 161   | MLcase (_,_,pv) -> not (is_ifthenelse pv)
 162   | _        -> false
 163
 164 let rec pp_expr status par env args =
 165   let par' = args <> [] || par
 166   and apply st = pp_apply st par args in
 167   function
 168     | MLrel n ->
 169         let id = get_db_name n env in status,apply (pr_id id)
 170     | MLapp (f,args') ->
 171         let status,stl = map_status status (fun status -> pp_expr status true env []) args' in
 172         pp_expr status par env (stl @ args) f
 173     | MLlam _ as a ->
 174         let fl,a' = collect_lams a in
 175         let fl = List.map id_of_mlid fl in
 176         let fl,env' = push_vars fl env in
 177         let status,res = pp_expr status false env' [] a' in
 178         let st = (pp_abst (List.rev fl) ++ res) in
 179         status,apply (pp_par par' st)
 180     | MLletin (id,a1,a2) ->
 181         let i,env' = push_vars [id_of_mlid id] env in
 182         let pp_id = pr_id (List.hd i) in
 183         let status,pp_a1 = pp_expr status false env [] a1 in
 184         let status,pp_a2 =
 185          pp_expr status (not par && expr_needs_par a2) env' [] a2 in
 186         status,
 187         hv 0
 188           (apply
 189              (pp_par par'
 190                 (hv 0
 191                    (hov 2
 192                       (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
 193                     spc () ++ str "in") ++
 194                  spc () ++ hov 0 pp_a2)))
 195     | MLglob r ->
 196         (try
 197            let args = list_skipn (projection_arity status r) args in
 198            let record = List.hd args in
 199            let status,res = pp_global status Term r in
 200            status,pp_apply (record ++ str "." ++ res) par (List.tl args)
 201          with _ ->
 202           let status,res = pp_global status Term r in
 203            status,apply res)
 204 (*CSC:    | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c*)
 205     | MLcons ({c_kind = Coinductive},r,[]) ->
 206         assert (args=[]);
 207         let status,res = pp_global status Cons r in
 208         status,pp_par par (str "lazy " ++ res)
 209     | MLcons ({c_kind = Coinductive},r,args') ->
 210         assert (args=[]);
 211         let status,tuple =
 212          pp_tuple status (fun status -> pp_expr status true env []) args' in
 213         let status,res = pp_global status Cons r in
 214         status,
 215         pp_par par (str "lazy (" ++ res ++ spc() ++ tuple ++str ")")
 216     | MLcons (_,r,[]) ->
 217         assert (args=[]);
 218         pp_global status Cons r
 219     | MLcons ({c_kind = Record fields}, r, args') ->
 220         assert (args=[]);
 221         let status,res = pp_fields status r fields in
 222         let status,res2 =
 223          map_status status (fun status -> pp_expr status true env []) args' in
 224         status,pp_record_pat (res, res2)
 225 (*CSC:    | MLcons (_,r,[arg1;arg2]) when is_infix r ->
 226         assert (args=[]);
 227         pp_par par
 228           ((pp_expr status true env [] arg1) ++ str (get_infix r) ++
 229            (pp_expr status true env [] arg2))*)
 230     | MLcons (_,r,args') ->
 231         assert (args=[]);
 232         let status,tuple =
 233          pp_tuple status (fun status -> pp_expr status true env []) args' in
 234         let status,res = str_global status Cons r in
 235         if res = "" (* hack Extract Inductive prod *)
 236         then status,tuple
 237         else
 238          let status,res = pp_global status Cons r in
 239          status,pp_par par (res ++ spc () ++ tuple)
 240 (*CSC:    | MLcase (_, t, pv) when is_custom_match pv ->
 241         let mkfun (_,ids,e) =
 242           if ids <> [] then named_lams (List.rev ids) e
 243           else dummy_lams (ast_lift 1 e) 1
 244         in
 245         apply
 246           (pp_par par'
 247              (hov 2
 248                 (str (find_custom_match pv) ++ fnl () ++
 249                  prvect (fun tr -> pp_expr status true env [] (mkfun tr) ++ fnl ()) pv
 250                  ++ pp_expr status true env [] t)))*)
 251     | MLcase (info, t, pv) ->
 252         let status,expr = if info.m_kind = Coinductive then
 253          let status,res = pp_expr status true env [] t in
 254           status,(str "Lazy.force" ++ spc () ++ res)
 255         else
 256           (pp_expr status false env [] t)
 257         in
 258         (try
 259            (* First, can this match be printed as a mere record projection ? *)
 260            let fields =
 261              match info.m_kind with Record f -> f | _ -> raise Impossible
 262            in
 263            let (r, ids, c) = pv.(0) in
 264            let n = List.length ids in
 265            let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
 266            let proj_hd status i =
 267             let status,res = pp_expr status true env [] t in
 268             let status,res2 = pp_field status r fields i in
 269              status,res ++ str "." ++ res2
 270            in
 271            match c with
 272              | MLrel i when i <= n ->
 273                 let status,res = proj_hd status (n-i) in
 274                 status,apply (pp_par par' res)
 275              | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
 276                let _ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
 277                let status,res = proj_hd status (n-i) in
 278                let status,res2 =
 279                 map_status status (fun status -> pp_expr status true env' []) a
 280                in
 281                status,(pp_apply res par (res2 @ args))
 282              | _ -> raise Impossible
 283          with Impossible ->
 284            (* Second, can this match be printed as a let-in ? *)
 285            if Array.length pv = 1 then
 286              let status,s1,s2 = pp_one_pat status env info pv.(0) in
 287              status,
 288              apply
 289                (hv 0
 290                   (pp_par par'
 291                      (hv 0
 292                         (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr)
 293                          ++ spc () ++ str "in") ++
 294                       spc () ++ hov 0 s2)))
 295            else
 296             let status,res =
 297              try status,pp_ifthenelse par' env expr pv
 298              with Not_found ->
 299               let status,res = pp_pat status env info pv in
 300                status,
 301                 v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ res)
 302             in
 303              (* Otherwise, standard match *)
 304              status,
 305              apply (pp_par par' res))
 306     | MLfix (i,ids,defs) ->
 307         let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
 308         pp_fix status par env' i (Array.of_list (List.rev ids'),defs) args
 309     | MLexn s ->
 310         (* An [MLexn] may be applied, but I don't really care. *)
 311         status,pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
 312     | MLdummy ->
 313        status,str "__" (*An [MLdummy] may be applied, but I don't really care.*)
 314     | MLmagic a ->
 315        let status,res = pp_expr status true env [] a in
 316         status,pp_apply (str "Obj.magic") par (res :: args)
 317     | MLaxiom ->
 318         status,pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
 319
 320
 321 and pp_record_pat (fields, args) =
 322    str "{ " ++
 323    prlist_with_sep (fun () -> str ";" ++ spc ())
 324      (fun (f,a) -> f ++ str " =" ++ spc () ++ a)
 325      (List.combine fields args) ++
 326    str " }"
 327
 328 and pp_ifthenelse _par _env _expr pv = match pv with
 329 (*CSC:  | [|(tru,[],the);(fal,[],els)|] when
 330       (find_custom tru = "true") && (find_custom fal = "false")
 331       ->
 332       hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
 333             hov 2 (str "then " ++
 334                    hov 2 (pp_expr status (expr_needs_par the) env [] the)) ++ spc () ++
 335             hov 2 (str "else " ++
 336                    hov 2 (pp_expr status (expr_needs_par els) env [] els)))*)
 337   | _ -> raise Not_found
 338
 339 and pp_one_pat status env info (r,ids,t) =
 340   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
 341   let status,expr = pp_expr status (expr_needs_par t) env' [] t in
 342   let status,patt = match info.m_kind with
 343     | Record fields ->
 344       let status,res = pp_fields status r fields in
 345       status,pp_record_pat (res, List.rev_map pr_id ids)
 346     | _ -> match List.rev ids with
 347 (*CSC:  | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2*)
 348         | [] -> pp_global status Cons r
 349         | ids ->
 350           (* hack Extract Inductive prod *)
 351           let status,res = str_global status Cons r in
 352           let status,res2 =
 353            if res = "" then status,mt()
 354            else
 355             let status,res = pp_global status Cons r in
 356              status, res ++ spc () in
 357           status,res2 ++ pp_boxed_tuple pr_id ids
 358   in
 359   status, patt, expr
 360
 361 and pp_pat status env info pv =
 362   let factor_br, factor_set = try match info.m_same with
 363     | BranchFun ints ->
 364         let i = Intset.choose ints in
 365         branch_as_fun info.m_typs pv.(i), ints
 366     | BranchCst ints ->
 367         let i = Intset.choose ints in
 368         ast_pop (branch_as_cst pv.(i)), ints
 369     | BranchNone -> MLdummy, Intset.empty
 370   with _ -> MLdummy, Intset.empty
 371   in
 372   let last = Array.length pv - 1 in
 373   let status,res =
 374   prvecti_status status
 375     (fun status i x -> if Intset.mem i factor_set then status,mt () else
 376        let status,s1,s2 = pp_one_pat status env info x in
 377        status,
 378        hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
 379        if i = last && Intset.is_empty factor_set then mt () else fnl ())
 380     pv
 381   in
 382   let status,res2 =
 383    if Intset.is_empty factor_set then status,mt () else
 384    let par = expr_needs_par factor_br in
 385    match info.m_same with
 386      | BranchFun _ ->
 387          let ids, env' = push_vars [anonymous_name] env in
 388          let status,res = pp_expr status par env' [] factor_br in
 389          status,hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
 390                   hov 2 res)
 391      | BranchCst _ ->
 392          let status,res = pp_expr status par env [] factor_br in
 393           status,hv 2 (str "| _ ->" ++ spc () ++ hov 2 res)
 394      | BranchNone -> status,mt ()
 395   in
 396    status, res ++ res2
 397
 398 and pp_function status env t =
 399   let bl,t' = collect_lams t in
 400   let bl,env' = push_vars (List.map id_of_mlid bl) env in
 401   match t' with
 402     | MLcase(i,MLrel 1,pv) when
 403         i.m_kind = Standard (*CSC:&& not (is_custom_match pv)*) ->
 404         if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
 405           let status,res = pp_pat status env' i pv in
 406           status,pr_binding (List.rev (List.tl bl)) ++
 407           str " = function" ++ fnl () ++ v 0 res
 408         else
 409           let status,res = pp_pat status env' i pv in
 410           status,
 411           pr_binding (List.rev bl) ++
 412           str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
 413           v 0 res
 414     | _ ->
 415           let status,res = pp_expr status false env' [] t' in
 416           status,
 417           pr_binding (List.rev bl) ++
 418           str " =" ++ fnl () ++ str "  " ++
 419           hov 2 res
 420
 421 (*s names of the functions ([ids]) are already pushed in [env],
 422     and passed here just for convenience. *)
 423
 424 and pp_fix status par env i (ids,bl) args =
 425  let status,res =
 426   prvect_with_sep_status status
 427    (fun () -> fnl () ++ str "and ")
 428    (fun status (fi,ti) ->
 429      let status,res = pp_function status env ti in
 430      status, pr_id fi ++ res)
 431    (array_map2 (fun id b -> (id,b)) ids bl)
 432  in
 433   status,
 434   pp_par par
 435     (v 0 (str "let rec " ++ res ++ fnl () ++
 436           hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 437
 438 let pp_val status e typ =
 439  let status,res = pp_type status false [] typ in
 440   status,
 441   hov 4 (str "(** val " ++ e ++ str " :" ++ spc ()++res++ str " **)") ++ fnl ()
 442
 443 (*s Pretty-printing of [Dfix] *)
 444
 445 let pp_Dfix status (rv,c,t) =
 446   let status,names = array_map_status status
 447     (fun status r -> (*CSC:if is_inline_custom r then mt () else*) pp_global status Term r) rv
 448   in
 449   let rec pp status init i =
 450     if i >= Array.length rv then
 451       (if init then failwith "empty phrase" else status,mt ())
 452     else
 453       let void = false(*CSC:is_inline_custom rv.(i)*) ||
 454         (not false(*CSC:(is_custom rv.(i))*) && c.(i) = MLexn "UNUSED")
 455       in
 456       if void then pp status init (i+1)
 457       else
 458         let status,def =
 459           (*CSC:if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
 460           else*) pp_function status (empty_env status) c.(i) in
 461         let status,res = pp_val status names.(i) t.(i) in
 462         let status,res2 = pp status false (i+1) in
 463         status,
 464         (if init then mt () else fnl ()) ++ res ++
 465         str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ res2
 466   in pp status true 0
 467
 468 (*s Pretty-printing of inductive types declaration. *)
 469
 470 let pp_comment s = str "(* " ++ s ++ str " *)"
 471
 472 let pp_one_ind status prefix pl name cnames ctyps =
 473   let pl = rename_tvars keywords pl in
 474   let pp_constructor status i typs =
 475    let status,res =
 476     prlist_with_sep_status status
 477      (fun () -> spc () ++ str "* ") (fun status -> pp_type status true pl) typs
 478    in
 479     status,
 480     (if i=0 then mt () else fnl ()) ++
 481     hov 3 (str "| " ++ cnames.(i) ++
 482            (if typs = [] then mt () else str " of ") ++ res) in
 483   let status,res =
 484    if Array.length ctyps = 0 then status,str " unit (* empty inductive *)"
 485    else
 486     let status,res = prvecti_status status pp_constructor ctyps in
 487      status, fnl () ++ v 0 res
 488   in
 489    status,
 490    pp_parameters pl ++ str prefix ++ name ++
 491    str " =" ++ res
 492
 493 let pp_logical_ind packet =
 494   pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
 495   fnl () ++
 496   pp_comment (str "with constructors : " ++
 497               prvect_with_sep spc pr_id packet.ip_consnames) ++
 498   fnl ()
 499
 500 let pp_singleton status packet =
 501   let status,name = pp_global status Type packet.ip_reference in
 502   let l = rename_tvars keywords packet.ip_vars in
 503   let status,res = pp_type status false l (List.hd packet.ip_types.(0)) in
 504   status,
 505   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 506          res ++ fnl () ++
 507          pp_comment (str "singleton inductive, whose constructor was " ++
 508                      pr_id packet.ip_consnames.(0)))
 509
 510 let pp_record status fields packet =
 511   let ind = packet.ip_reference in
 512   let status,name = pp_global status Type ind in
 513   let status,fieldnames = pp_fields status ind fields in
 514   let l = List.combine fieldnames packet.ip_types.(0) in
 515   let pl = rename_tvars keywords packet.ip_vars in
 516   let status,res =
 517    prlist_with_sep_status status (fun () -> str ";" ++ spc ())
 518     (fun status (p,t) ->
 519       let status,res = pp_type status true pl t in
 520        status, p ++ str " : " ++ res) l in
 521   status,
 522   str "type " ++ pp_parameters pl ++ name ++ str " = { "++ hov 0 res ++ str " }"
 523
 524 let pp_coind pl name =
 525   let pl = rename_tvars keywords pl in
 526   pp_parameters pl ++ name ++ str " = " ++
 527   pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++
 528   fnl() ++ str "and "
 529
 530 let pp_ind status co ind =
 531   let prefix = if co then "__" else "" in
 532   let some = ref false in
 533   let init= ref (str "type ") in
 534   let status,names =
 535     array_map_status status
 536      (fun status p ->
 537        if p.ip_logical then status,mt ()
 538        else pp_global status Type p.ip_reference)
 539       ind.ind_packets
 540   in
 541   let status,cnames =
 542     array_map_status status
 543       (fun status p -> if p.ip_logical then status,[||] else
 544          array_mapi_status status
 545           (fun status j _ -> pp_global status Cons p.ip_consreferences.(j))
 546            p.ip_types)
 547       ind.ind_packets
 548   in
 549   let rec pp status i =
 550     if i >= Array.length ind.ind_packets then status,mt ()
 551     else
 552       let p = ind.ind_packets.(i) in
 553       (*CSC:
 554       let ip = assert false(*CSC: (mind_of_kn kn,i)*) in
 555       if is_custom (IndRef ip) then pp (i+1)
 556       else*) begin
 557         some := true;
 558         if p.ip_logical then
 559          let status,res = pp status (i+1) in
 560           status, pp_logical_ind p ++ res
 561         else
 562           let s = !init in
 563           begin
 564             init := (fnl () ++ str "and ");
 565             let status,res =
 566               pp_one_ind
 567                 status prefix p.ip_vars names.(i) cnames.(i) p.ip_types in
 568             let status,res2 = pp status (i+1) in
 569               status,
 570               s ++
 571               (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
 572               res ++ res2
 573           end
 574       end
 575   in
 576   let st = pp status 0 in if !some then st else failwith "empty phrase"
 577
 578
 579 (*s Pretty-printing of a declaration. *)
 580
 581 let pp_mind status i =
 582   match i.ind_kind with
 583     | Singleton -> pp_singleton status i.ind_packets.(0)
 584     | Coinductive -> pp_ind status true i
 585     | Record fields -> pp_record status fields i.ind_packets.(0)
 586     | Standard -> pp_ind status false i
 587
 588 let pp_decl status = function
 589 (*CSC:    | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
 590     | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"*)
 591     | Dind i -> pp_mind status i
 592     | Dtype (r, l, t) ->
 593         let status,name = pp_global status Type r in
 594         let l = rename_tvars keywords l in
 595         let ids, (status, def) =
 596 (*CSC:    try
 597             let ids,s = find_type_custom r in
 598             pp_string_parameters ids, str "=" ++ spc () ++ str s
 599           with Not_found ->*)
 600             pp_parameters l,
 601             if t = Taxiom then status, str "(* AXIOM TO BE REALIZED *)"
 602             else
 603              let status,res = pp_type status false l t in
 604               status, str "=" ++ spc () ++ res
 605         in
 606         status, hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
 607     | Dterm (r, a, t) ->
 608         let status,name = pp_global status Term r in
 609         let status,def =
 610           (*if is_custom r then str (" = " ^ find_custom r)
 611           else*) if is_projection status r then
 612             status,
 613             (prvect str (Array.make (projection_arity status r) " _")) ++
 614             str " x = x." ++ name
 615           else
 616            let status,res = pp_function status (empty_env status) a in
 617             status, res ++ mt ()
 618         in
 619         let status,res = pp_val status name t in
 620          status, res ++ hov 0 (str "let " ++ name ++ def)
 621     | Dfix (rv,defs,typs) ->
 622         pp_Dfix status (rv,defs,typs)
 623
 624 let pp_spec status = function
 625 (*  | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
 626   | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"*)
 627   | Sind i -> pp_mind status i
 628   | Sval (r,t) ->
 629       let status,def = pp_type status false [] t in
 630       let status,name = pp_global status Term r in
 631       status, hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
 632   | Stype (r,vl,ot) ->
 633       let status, name = pp_global status Type r in
 634       let l = rename_tvars keywords vl in
 635       let status, ids, def =
 636 (*CSC:
 637         try
 638           let ids, s = find_type_custom r in
 639           pp_string_parameters ids,  str "= " ++ str s
 640         with Not_found ->*)
 641           let ids = pp_parameters l in
 642           match ot with
 643             | None -> status, ids, mt ()
 644             | Some Taxiom -> status, ids, str "(* AXIOM TO BE REALIZED *)"
 645             | Some t ->
 646                let status,res = pp_type status false l t in
 647                 status, ids, str "=" ++ spc () ++ res
 648       in
 649       status, hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
 650
 651 let pp_decl status d =
 652  try pp_decl status d with Failure "empty phrase" -> status, mt ()
 653 ;;