← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to parsing/printmod.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
parsing/printmod.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
open Pp
 
10
open Util
 
11
open Names
 
12
open Declarations
 
13
open Nameops
 
14
open Libnames
 
15
 
 
16
let get_new_id locals id = 
 
17
  let rec get_id l id = 
 
18
    let dir = make_dirpath [id] in
 
19
      if not (Nametab.exists_module dir) then
 
20
        id
 
21
      else
 
22
        get_id (id::l) (Nameops.next_ident_away id l)
 
23
  in
 
24
    get_id (List.map snd locals) id
 
25
 
 
26
let rec print_local_modpath locals = function
 
27
  | MPbound mbid -> pr_id (List.assoc mbid locals)
 
28
  | MPdot(mp,l) ->
 
29
      print_local_modpath locals mp ++ str "." ++ pr_lab l
 
30
  | MPself _ | MPfile _ -> raise Not_found
 
31
 
 
32
let print_modpath locals mp = 
 
33
  try (* must be with let because streams are lazy! *)
 
34
    let qid = Nametab.shortest_qualid_of_module mp in 
 
35
      pr_qualid qid
 
36
  with
 
37
    | Not_found -> print_local_modpath locals mp
 
38
 
 
39
let print_kn locals kn = 
 
40
  try
 
41
    let qid = Nametab.shortest_qualid_of_modtype kn in 
 
42
      pr_qualid qid
 
43
  with
 
44
      Not_found -> 
 
45
        try
 
46
          print_local_modpath locals kn
 
47
        with
 
48
            Not_found -> print_modpath locals kn
 
49
 
 
50
let rec flatten_app mexpr l = match mexpr with
 
51
  | SEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
 
52
  | mexpr -> mexpr::l
 
53
 
 
54
let rec print_module name locals with_body mb =
 
55
  let body = match with_body, mb.mod_expr with 
 
56
    | false, _ 
 
57
    | true, None -> mt()
 
58
    | true, Some mexpr -> 
 
59
        spc () ++ str ":= " ++ print_modexpr locals mexpr
 
60
  in
 
61
  let modtype = match mb.mod_type with
 
62
      None -> str ""
 
63
    | Some t -> spc () ++ str": " ++ 
 
64
        print_modtype locals t
 
65
  in
 
66
    hv 2 (str "Module " ++ name ++ modtype ++ body)
 
67
 
 
68
and print_modtype locals mty = 
 
69
  match mty with
 
70
    | SEBident kn -> print_kn locals kn
 
71
    | SEBfunctor (mbid,mtb1,mtb2) ->
 
72
      (*    let env' = Modops.add_module (MPbid mbid) 
 
73
            (Modops.body_of_type mtb) env 
 
74
            in *) 
 
75
      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))
 
76
        ::locals in
 
77
        hov 2 (str "Funsig" ++ spc () ++ str "(" ++ 
 
78
                 pr_id (id_of_mbid mbid) ++ str " : " ++ 
 
79
                 print_modtype locals mtb1.typ_expr ++ 
 
80
                 str ")" ++ spc() ++ print_modtype locals' mtb2)
 
81
  | SEBstruct (msid,sign) -> 
 
82
      hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End")
 
83
  | SEBapply (mexpr,marg,_) -> 
 
84
      let lapp = flatten_app mexpr [marg] in
 
85
      let fapp = List.hd lapp in
 
86
      let mapp = List.tl lapp in
 
87
        hov 3 (str"(" ++ (print_modtype locals fapp) ++ spc () ++ 
 
88
                 prlist_with_sep spc (print_modexpr locals) mapp ++ str")")
 
89
  | SEBwith(seb,With_definition_body(idl,cb))->
 
90
      let s = (String.concat "." (List.map string_of_id idl)) in
 
91
      hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ 
 
92
               str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
 
93
  | SEBwith(seb,With_module_body(idl,mp,_,_))->
 
94
      let s =(String.concat "." (List.map string_of_id idl)) in
 
95
      hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ 
 
96
               str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
 
97
 
 
98
and print_sig locals msid sign = 
 
99
  let print_spec (l,spec) = (match spec with
 
100
    | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
 
101
    | SFBconst {const_body=None}
 
102
    | SFBconst {const_opaque=true} -> str "Parameter "
 
103
    | SFBmind _ -> str "Inductive "
 
104
    | SFBmodule _ -> str "Module "
 
105
    | SFBalias (mp,_,_) -> str "Module "
 
106
    | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
 
107
  in
 
108
    prlist_with_sep spc print_spec sign
 
109
 
 
110
and print_struct locals msid struc = 
 
111
  let print_body (l,body) = (match body with
 
112
    | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
 
113
    | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem "
 
114
    | SFBconst {const_body=None} -> str "Parameter "
 
115
    | SFBmind _ -> str "Inductive "
 
116
    | SFBmodule _ -> str "Module "
 
117
    | SFBalias (mp,_,_) -> str "Module "
 
118
    | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
 
119
  in
 
120
    prlist_with_sep spc print_body struc
 
121
 
 
122
and print_modexpr locals mexpr = match mexpr with 
 
123
  | SEBident mp -> print_modpath locals mp
 
124
  | SEBfunctor (mbid,mty,mexpr) ->
 
125
(*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
 
126
      in *)
 
127
      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
 
128
      hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ 
 
129
             str ":" ++ print_modtype locals mty.typ_expr ++ 
 
130
      str ")" ++ spc () ++ print_modexpr locals' mexpr)
 
131
  | SEBstruct (msid, struc) -> 
 
132
      hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
 
133
  | SEBapply (mexpr,marg,_) -> 
 
134
      let lapp = flatten_app mexpr [marg] in
 
135
        hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")
 
136
  | SEBwith (_,_)-> anomaly "Not avaible yet"
 
137
 
 
138
 
 
139
let rec printable_body dir =     
 
140
  let dir = dirpath_prefix dir in
 
141
    dir = empty_dirpath || 
 
142
    try 
 
143
      match Nametab.locate_dir (qualid_of_dirpath dir) with
 
144
          DirOpenModtype _ -> false
 
145
        | DirModule _ | DirOpenModule _ -> printable_body dir
 
146
        | _ -> true
 
147
    with 
 
148
        Not_found -> true
 
149
 
 
150
 
 
151
let print_module with_body mp = 
 
152
  let name = print_modpath [] mp in
 
153
    print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
 
154
 
 
155
let print_modtype kn = 
 
156
  let mtb = Global.lookup_modtype kn in
 
157
  let name = print_kn [] kn in
 
158
      str "Module Type " ++ name ++ str " = " ++ 
 
159
        print_modtype [] mtb.typ_expr ++ fnl ()