← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/dp/dp_zenon.mll

  • 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/dp/dp_zenon.mll
 
1
 
 
2
{
 
3
 
 
4
  open Lexing 
 
5
  open Pp
 
6
  open Util
 
7
  open Names
 
8
  open Tacmach
 
9
  open Dp_why
 
10
  open Tactics
 
11
  open Tacticals
 
12
 
 
13
  let debug = ref false
 
14
  let set_debug b = debug := b
 
15
  
 
16
  let buf = Buffer.create 1024
 
17
    
 
18
  let string_of_global env ref =
 
19
    Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref)
 
20
 
 
21
  let axioms = ref []
 
22
 
 
23
  (* we cannot interpret the terms as we read them (since some lemmas
 
24
     may need other lemmas to be already interpreted) *)
 
25
  type lemma = { l_id : string; l_type : string; l_proof : string }
 
26
  type zenon_proof = lemma list * string
 
27
 
 
28
}
 
29
 
 
30
let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9' '\'']+
 
31
let space = [' ' '\t' '\r']
 
32
 
 
33
rule start = parse
 
34
| "(* BEGIN-PROOF *)" "\n" { scan lexbuf }
 
35
| _ { start lexbuf }
 
36
| eof { anomaly "malformed Zenon proof term" }
 
37
 
 
38
(* here we read the lemmas and the main proof term;
 
39
   meanwhile we maintain the set of axioms that were used *)
 
40
 
 
41
and scan = parse
 
42
| "Let" space (ident as id) space* ":"
 
43
  { let t = read_coq_term lexbuf in
 
44
    let p = read_lemma_proof lexbuf in
 
45
    let l,pr = scan lexbuf in
 
46
    { l_id = id; l_type = t; l_proof = p } :: l, pr }
 
47
| "Definition theorem:"
 
48
  { let t = read_main_proof lexbuf in [], t }
 
49
| _ | eof
 
50
  { anomaly "malformed Zenon proof term" }
 
51
 
 
52
and read_coq_term = parse
 
53
| "." "\n" 
 
54
  { let s = Buffer.contents buf in Buffer.clear buf; s }
 
55
| "coq__" (ident as id) (* a Why keyword renamed *)
 
56
  { Buffer.add_string buf id; read_coq_term lexbuf }
 
57
| ("dp_axiom__" ['0'-'9']+) as id 
 
58
  { axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf }
 
59
| _ as c 
 
60
  { Buffer.add_char buf c; read_coq_term lexbuf }
 
61
| eof 
 
62
  { anomaly "malformed Zenon proof term" }
 
63
 
 
64
and read_lemma_proof = parse
 
65
| "Proof" space
 
66
  { read_coq_term lexbuf }
 
67
| _ | eof
 
68
  { anomaly "malformed Zenon proof term" }
 
69
 
 
70
(* skip the main proof statement and then read its term *)
 
71
and read_main_proof = parse
 
72
| ":=" "\n"
 
73
  { read_coq_term lexbuf }
 
74
| _ 
 
75
  { read_main_proof lexbuf }
 
76
| eof
 
77
  { anomaly "malformed Zenon proof term" }
 
78
 
 
79
 
 
80
{
 
81
 
 
82
  let read_zenon_proof f =
 
83
    Buffer.clear buf;
 
84
    let c = open_in f in
 
85
    let lb = from_channel c in
 
86
    let p = start lb in
 
87
    close_in c;
 
88
    if not !debug then begin try Sys.remove f with _ -> () end;
 
89
    p
 
90
 
 
91
  let constr_of_string gl s = 
 
92
    let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
 
93
    Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
 
94
 
 
95
  (* we are lazy here: we build strings containing Coq terms using a *)
 
96
  (* pretty-printer Fol -> Coq *)
 
97
  module Coq = struct
 
98
    open Format
 
99
    open Fol
 
100
 
 
101
    let rec print_list sep print fmt = function
 
102
      | [] -> ()
 
103
      | [x] -> print fmt x
 
104
      | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
 
105
          
 
106
    let space fmt () = fprintf fmt "@ "
 
107
    let comma fmt () = fprintf fmt ",@ "
 
108
 
 
109
    let rec print_typ fmt = function
 
110
      | Tvar x -> fprintf fmt "%s" x
 
111
      | Tid ("int", []) -> fprintf fmt "Z"
 
112
      | Tid (x, []) -> fprintf fmt "%s" x
 
113
      | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t 
 
114
      | Tid (x,tl) -> 
 
115
          fprintf fmt "(%s %a)" x (print_list comma print_typ) tl 
 
116
          
 
117
    let rec print_term fmt = function
 
118
      | Cst n -> 
 
119
          fprintf fmt "%d" n
 
120
      | Plus (a, b) ->
 
121
          fprintf fmt "@[(Zplus %a %a)@]" print_term a print_term b
 
122
      | Moins (a, b) ->
 
123
          fprintf fmt "@[(Zminus %a %a)@]" print_term a print_term b
 
124
      | Mult (a, b) ->
 
125
          fprintf fmt "@[(Zmult %a %a)@]" print_term a print_term b
 
126
      | Div (a, b) ->
 
127
          fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b
 
128
      | App (id, []) ->
 
129
          fprintf fmt "%s" id
 
130
      | App (id, tl) ->
 
131
          fprintf fmt "@[(%s %a)@]" id print_terms tl
 
132
 
 
133
    and print_terms fmt tl = 
 
134
      print_list space print_term fmt tl
 
135
 
 
136
    (* builds the text for "forall vars, f vars = t" *)
 
137
    let fun_def_axiom f vars t =
 
138
      let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in
 
139
      fprintf str_formatter
 
140
        "@[(forall %a, %s %a = %a)@]@."
 
141
        (print_list space binder) vars f 
 
142
        (print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars
 
143
        print_term t;
 
144
      flush_str_formatter ()
 
145
                           
 
146
  end
 
147
 
 
148
  let prove_axiom id = match Dp_why.find_proof id with
 
149
    | Immediate t -> 
 
150
        exact_check t
 
151
    | Fun_def (f, vars, ty, t) -> 
 
152
        tclTHENS
 
153
          (fun gl ->
 
154
             let s = Coq.fun_def_axiom f vars t in
 
155
             if !debug then Format.eprintf "axiom fun def = %s@." s;
 
156
             let c = constr_of_string gl s in
 
157
             assert_tac (Name (id_of_string id)) c gl)
 
158
          [tclTHEN intros reflexivity; tclIDTAC]
 
159
 
 
160
  let exact_string s gl =
 
161
    let c = constr_of_string gl s in
 
162
    exact_check c gl
 
163
 
 
164
  let interp_zenon_proof (ll,p) =
 
165
    let interp_lemma l gl =
 
166
      let ty = constr_of_string gl l.l_type in
 
167
      tclTHENS
 
168
        (assert_tac (Name (id_of_string l.l_id)) ty)
 
169
        [exact_string l.l_proof; tclIDTAC]
 
170
        gl
 
171
    in
 
172
    tclTHEN (tclMAP interp_lemma ll) (exact_string p)
 
173
 
 
174
  let proof_from_file f =
 
175
    axioms := [];
 
176
    msgnl (str "proof_from_file " ++ str f);
 
177
    let zp = read_zenon_proof f in
 
178
    msgnl (str "proof term is " ++ str (snd zp));
 
179
    tclTHEN (tclMAP prove_axiom !axioms) (interp_zenon_proof zp)
 
180
 
 
181
}