← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/extraction/scheme.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:
contrib/extraction/scheme.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
(*i $Id: scheme.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
 
10
 
 
11
(*s Production of Scheme syntax. *)
 
12
 
 
13
open Pp
 
14
open Util
 
15
open Names
 
16
open Nameops
 
17
open Libnames
 
18
open Miniml
 
19
open Mlutil
 
20
open Table
 
21
open Common
 
22
 
 
23
(*s Scheme renaming issues. *)
 
24
 
 
25
let keywords =     
 
26
  List.fold_right (fun s -> Idset.add (id_of_string s))
 
27
    [ "define"; "let"; "lambda"; "lambdas"; "match"; 
 
28
      "apply"; "car"; "cdr"; 
 
29
      "error"; "delay"; "force"; "_"; "__"] 
 
30
    Idset.empty
 
31
 
 
32
let preamble _ _ usf = 
 
33
  str ";; This extracted scheme code relies on some additional macros\n" ++ 
 
34
  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
 
35
  str "(load \"macros_extr.scm\")\n\n" ++
 
36
  (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
37
 
 
38
let pr_id id = 
 
39
  let s = string_of_id id in
 
40
  for i = 0 to String.length s - 1 do 
 
41
    if s.[i] = '\'' then s.[i] <- '~'
 
42
  done; 
 
43
  str s
 
44
 
 
45
let paren = pp_par true
 
46
 
 
47
let pp_abst st = function 
 
48
  | [] -> assert false
 
49
  | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
 
50
  | l -> paren 
 
51
        (str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
 
52
 
 
53
let pp_apply st _ = function 
 
54
  | [] -> st 
 
55
  | [a] -> hov 2 (paren (st ++ spc () ++ a))
 
56
  | args -> hov 2 (paren (str "@ " ++ st ++ 
 
57
                          (prlist_strict (fun x -> spc () ++ x) args)))
 
58
 
 
59
(*s The pretty-printer for Scheme syntax *)
 
60
 
 
61
let pp_global k r = str (Common.pp_global k r)
 
62
 
 
63
(*s Pretty-printing of expressions.  *)
 
64
 
 
65
let rec pp_expr env args = 
 
66
  let apply st = pp_apply st true args in 
 
67
  function
 
68
    | MLrel n -> 
 
69
        let id = get_db_name n env in apply (pr_id id)
 
70
    | MLapp (f,args') ->
 
71
        let stl = List.map (pp_expr env []) args' in
 
72
        pp_expr env (stl @ args) f
 
73
    | MLlam _ as a -> 
 
74
        let fl,a' = collect_lams a in
 
75
        let fl,env' = push_vars fl env in
 
76
        apply (pp_abst (pp_expr env' [] a') (List.rev fl))
 
77
    | MLletin (id,a1,a2) ->
 
78
        let i,env' = push_vars [id] env in
 
79
        apply 
 
80
          (hv 0 
 
81
             (hov 2 
 
82
                (paren 
 
83
                   (str "let " ++ 
 
84
                    paren 
 
85
                      (paren 
 
86
                         (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
 
87
                    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
 
88
    | MLglob r -> 
 
89
        apply (pp_global Term r)
 
90
    | MLcons (i,r,args') ->
 
91
        assert (args=[]);
 
92
        let st = 
 
93
          str "`" ++ 
 
94
          paren (pp_global Cons r ++ 
 
95
                 (if args' = [] then mt () else spc ()) ++
 
96
                 prlist_with_sep spc (pp_cons_args env) args')
 
97
        in 
 
98
        if i = Coinductive then paren (str "delay " ++ st) else st 
 
99
    | MLcase ((i,_),t, pv) ->
 
100
        let e = 
 
101
          if i <> Coinductive then pp_expr env [] t     
 
102
          else paren (str "force" ++ spc () ++ pp_expr env [] t)
 
103
        in 
 
104
        apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
 
105
    | MLfix (i,ids,defs) ->
 
106
        let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
 
107
        pp_fix env' i (Array.of_list (List.rev ids'),defs) args
 
108
    | MLexn s -> 
 
109
        (* An [MLexn] may be applied, but I don't really care. *)
 
110
        paren (str "error" ++ spc () ++ qs s)
 
111
    | MLdummy ->
 
112
        str "__" (* An [MLdummy] may be applied, but I don't really care. *)
 
113
    | MLmagic a ->
 
114
        pp_expr env args a
 
115
    | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
 
116
 
 
117
and pp_cons_args env = function 
 
118
  | MLcons (i,r,args) when i<>Coinductive -> 
 
119
      paren (pp_global Cons r ++ 
 
120
             (if args = [] then mt () else spc ()) ++
 
121
             prlist_with_sep spc (pp_cons_args env) args)
 
122
  | e -> str "," ++ pp_expr env [] e
 
123
        
 
124
 
 
125
and pp_one_pat env (r,ids,t) = 
 
126
  let ids,env' = push_vars (List.rev ids) env in
 
127
  let args = 
 
128
    if ids = [] then mt () 
 
129
    else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
 
130
  in 
 
131
  (pp_global Cons r ++ args), (pp_expr env' [] t)
 
132
  
 
133
and pp_pat env pv = 
 
134
  prvect_with_sep fnl  
 
135
    (fun x -> let s1,s2 = pp_one_pat env x in 
 
136
     hov 2 (str "((" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv
 
137
 
 
138
(*s names of the functions ([ids]) are already pushed in [env],
 
139
    and passed here just for convenience. *)
 
140
 
 
141
and pp_fix env j (ids,bl) args =
 
142
    paren 
 
143
      (str "letrec " ++
 
144
       (v 0 (paren 
 
145
               (prvect_with_sep fnl
 
146
                  (fun (fi,ti) -> 
 
147
                     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
 
148
                  (array_map2 (fun id b -> (id,b)) ids bl)) ++
 
149
             fnl () ++
 
150
             hov 2 (pp_apply (pr_id (ids.(j))) true args))))
 
151
 
 
152
(*s Pretty-printing of a declaration. *)
 
153
 
 
154
let pp_decl = function
 
155
  | Dind _ -> mt ()
 
156
  | Dtype _ -> mt () 
 
157
  | Dfix (rv, defs,_) ->
 
158
      let ppv = Array.map (pp_global Term) rv in 
 
159
      prvect_with_sep fnl 
 
160
        (fun (pi,ti) -> 
 
161
           hov 2 
 
162
             (paren (str "define " ++ pi ++ spc () ++ 
 
163
                     (pp_expr (empty_env ()) [] ti)) 
 
164
              ++ fnl ()))
 
165
        (array_map2 (fun p b -> (p,b)) ppv defs) ++
 
166
      fnl ()
 
167
  | Dterm (r, a, _) ->
 
168
      if is_inline_custom r then mt () 
 
169
      else 
 
170
        if is_custom r then 
 
171
          hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ 
 
172
                          str (find_custom r))) ++ fnl () ++ fnl () 
 
173
        else 
 
174
          hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
 
175
                          pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
 
176
 
 
177
let pp_structure_elem = function 
 
178
  | (l,SEdecl d) -> pp_decl d
 
179
  | (l,SEmodule m) -> 
 
180
      failwith "TODO: Scheme extraction of modules not implemented yet"
 
181
  | (l,SEmodtype m) -> 
 
182
      failwith "TODO: Scheme extraction of modules not implemented yet"
 
183
 
 
184
let pp_struct = 
 
185
  let pp_sel (mp,sel) = 
 
186
    push_visible mp None; 
 
187
    let p = prlist_strict pp_structure_elem sel in 
 
188
    pop_visible (); p
 
189
  in
 
190
  prlist_strict pp_sel
 
191
 
 
192
let scheme_descr = {
 
193
  keywords = keywords;  
 
194
  file_suffix = ".scm"; 
 
195
  capital_file = false;  
 
196
  preamble = preamble; 
 
197
  pp_struct = pp_struct; 
 
198
  sig_suffix = None;
 
199
  sig_preamble = (fun _ _ _ -> mt ()); 
 
200
  pp_sig = (fun _ -> mt ()); 
 
201
  pp_decl = pp_decl; 
 
202
}