← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/dp/dp_why.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/dp/dp_why.ml
 
1
 
 
2
(* Pretty-print PFOL (see fol.mli) in Why syntax *)
 
3
 
 
4
open Format
 
5
open Fol
 
6
 
 
7
type proof = 
 
8
  | Immediate of Term.constr
 
9
  | Fun_def of string * (string * typ) list * typ * term
 
10
 
 
11
let proofs = Hashtbl.create 97
 
12
let proof_name = 
 
13
  let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r
 
14
 
 
15
let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n
 
16
 
 
17
let find_proof = Hashtbl.find proofs
 
18
 
 
19
let rec print_list sep print fmt = function
 
20
  | [] -> ()
 
21
  | [x] -> print fmt x
 
22
  | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
 
23
 
 
24
let space fmt () = fprintf fmt "@ "
 
25
let comma fmt () = fprintf fmt ",@ "
 
26
 
 
27
let is_why_keyword = 
 
28
  let h = Hashtbl.create 17 in
 
29
  List.iter 
 
30
    (fun s -> Hashtbl.add h s ())
 
31
    ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin";
 
32
     "bool"; "do"; "done"; "else"; "end"; "exception"; "exists";
 
33
     "external"; "false"; "for"; "forall"; "fun"; "function"; "goal";
 
34
     "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not";
 
35
     "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises";
 
36
     "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try";
 
37
     "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ]; 
 
38
  Hashtbl.mem h
 
39
 
 
40
let ident fmt s =
 
41
  if is_why_keyword s then fprintf fmt "coq__%s" s else fprintf fmt "%s" s
 
42
 
 
43
let rec print_typ fmt = function
 
44
  | Tvar x -> fprintf fmt "'%a" ident x
 
45
  | Tid ("int", []) -> fprintf fmt "int"
 
46
  | Tid (x, []) -> fprintf fmt "%a" ident x
 
47
  | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x
 
48
  | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x
 
49
 
 
50
let rec print_term fmt = function
 
51
  | Cst n -> 
 
52
      fprintf fmt "%d" n
 
53
  | Plus (a, b) ->
 
54
      fprintf fmt "@[(%a +@ %a)@]" print_term a print_term b
 
55
  | Moins (a, b) ->
 
56
      fprintf fmt "@[(%a -@ %a)@]" print_term a print_term b
 
57
  | Mult (a, b) ->
 
58
      fprintf fmt "@[(%a *@ %a)@]" print_term a print_term b
 
59
  | Div (a, b) ->
 
60
      fprintf fmt "@[(%a /@ %a)@]" print_term a print_term b
 
61
  | App (id, []) ->
 
62
      fprintf fmt "%a" ident id
 
63
  | App (id, tl) ->
 
64
      fprintf fmt "@[%a(%a)@]" ident id print_terms tl
 
65
 
 
66
and print_terms fmt tl = 
 
67
  print_list comma print_term fmt tl
 
68
 
 
69
let rec print_predicate fmt p = 
 
70
  let pp = print_predicate in 
 
71
  match p with
 
72
  | True ->
 
73
      fprintf fmt "true"
 
74
  | False ->
 
75
      fprintf fmt "false"
 
76
  | Fatom (Eq (a, b)) ->
 
77
      fprintf fmt "@[(%a =@ %a)@]" print_term a print_term b
 
78
  | Fatom (Le (a, b)) ->
 
79
      fprintf fmt "@[(%a <=@ %a)@]" print_term a print_term b
 
80
  | Fatom (Lt (a, b))->
 
81
      fprintf fmt "@[(%a <@ %a)@]" print_term a print_term b
 
82
  | Fatom (Ge (a, b)) ->
 
83
      fprintf fmt "@[(%a >=@ %a)@]" print_term a print_term b
 
84
  | Fatom (Gt (a, b)) ->
 
85
      fprintf fmt "@[(%a >@ %a)@]" print_term a print_term b
 
86
  | Fatom (Pred (id, [])) -> 
 
87
      fprintf fmt "%a" ident id
 
88
  | Fatom (Pred (id, tl)) -> 
 
89
      fprintf fmt "@[%a(%a)@]" ident id print_terms tl
 
90
  | Imp (a, b) ->
 
91
      fprintf fmt "@[(%a ->@ %a)@]" pp a pp b
 
92
  | Iff (a, b) ->
 
93
      fprintf fmt "@[(%a <->@ %a)@]" pp a pp b
 
94
  | And (a, b) ->
 
95
      fprintf fmt "@[(%a and@ %a)@]" pp a pp b
 
96
  | Or (a, b) ->
 
97
      fprintf fmt "@[(%a or@ %a)@]" pp a pp b
 
98
  | Not a ->
 
99
      fprintf fmt "@[(not@ %a)@]" pp a
 
100
  | Forall (id, t, p) -> 
 
101
      fprintf fmt "@[(forall %a:%a.@ %a)@]" ident id print_typ t pp p
 
102
  | Exists (id, t, p) -> 
 
103
      fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p
 
104
 
 
105
let print_query fmt (decls,concl) =
 
106
  let print_dtype = function
 
107
    | DeclType (id, 0) ->
 
108
        fprintf fmt "@[type %a@]@\n@\n" ident id
 
109
    | DeclType (id, 1) ->
 
110
        fprintf fmt "@[type 'a %a@]@\n@\n" ident id
 
111
    | DeclType (id, n) ->
 
112
        fprintf fmt "@[type (";
 
113
        for i = 1 to n do 
 
114
          fprintf fmt "'a%d" i; if i < n then fprintf fmt ", "
 
115
        done;
 
116
        fprintf fmt ") %a@]@\n@\n" ident id
 
117
    | DeclFun _ | DeclPred _ | Axiom _ ->
 
118
        ()
 
119
  in
 
120
  let print_dvar_dpred = function
 
121
    | DeclFun (id, _, [], t) ->
 
122
        fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t
 
123
    | DeclFun (id, _, l, t) ->
 
124
        fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" 
 
125
          ident id (print_list comma print_typ) l print_typ t
 
126
    | DeclPred (id, _, []) ->
 
127
        fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id
 
128
    | DeclPred (id, _, l) -> 
 
129
        fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" 
 
130
          ident id (print_list comma print_typ) l
 
131
    | DeclType _ | Axiom _ ->
 
132
        ()
 
133
  in
 
134
  let print_assert = function
 
135
    | Axiom (id, f)  -> 
 
136
        fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f
 
137
    | DeclType _ | DeclFun _ | DeclPred _ ->
 
138
        ()
 
139
  in
 
140
  List.iter print_dtype decls;
 
141
  List.iter print_dvar_dpred decls;
 
142
  List.iter print_assert decls;
 
143
  fprintf fmt "@[<hov 2>goal coq___goal: %a@]" print_predicate concl
 
144
 
 
145
let output_file f q =
 
146
  let c = open_out f in
 
147
  let fmt = formatter_of_out_channel c in
 
148
  fprintf fmt "@[%a@]@." print_query q;
 
149
  close_out c
 
150
 
 
151