coq.ml 12.3 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Pp
open Util
open Ident
open Ty
open Term
open Decl
27
open Printer
MARCHE Claude's avatar
MARCHE Claude committed
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51

let iprinter,tprinter,lprinter,pprinter =
  let bl = [ "at"; "cofix"; "exists2"; "fix"; "IF"; "mod"; "Prop";
	     "return"; "Set"; "Type"; "using"; "where"]
  in
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  let usanitize = sanitizer char_to_ualpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
  create_ident_printer bl ~sanitizer:usanitize

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
  forget_all pprinter

let tv_set = ref Sid.empty

(* type variables *)
let print_tv fmt tv =
  tv_set := Sid.add tv.tv_name !tv_set;
MARCHE Claude's avatar
MARCHE Claude committed
52
  let n = id_unique iprinter tv.tv_name in
MARCHE Claude's avatar
MARCHE Claude committed
53 54 55 56 57 58 59 60
  fprintf fmt "%s" n

let forget_tvs () =
  Sid.iter (forget_id iprinter) !tv_set;
  tv_set := Sid.empty

(* logic variables *)
let print_vs fmt vs =
MARCHE Claude's avatar
MARCHE Claude committed
61
  let n = id_unique iprinter vs.vs_name in
MARCHE Claude's avatar
MARCHE Claude committed
62 63 64 65 66 67 68 69
  fprintf fmt "%s" n

let forget_var vs = forget_id iprinter vs.vs_name

let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)

let print_ls fmt ls =
MARCHE Claude's avatar
MARCHE Claude committed
70
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)
MARCHE Claude's avatar
MARCHE Claude committed
71 72 73 74

let print_pr fmt pr =
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)

75 76 77
(* info *)

type info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
78
  info_syn : string Mid.t;
79 80 81
  info_rem : Sid.t;
}

MARCHE Claude's avatar
MARCHE Claude committed
82 83
(** Types *)

84
let rec print_ty info fmt ty = match ty.ty_node with
MARCHE Claude's avatar
MARCHE Claude committed
85
  | Tyvar v -> print_tv fmt v
86
  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
87
      | Some s -> syntax_arguments s (print_ty info) fmt tl
88
      | None -> begin match tl with
MARCHE Claude's avatar
MARCHE Claude committed
89 90
          | []  -> print_ts fmt ts
          | l   -> fprintf fmt "(%a@ %a)" print_ts ts
91
                     (print_list space (print_ty info)) l
MARCHE Claude's avatar
MARCHE Claude committed
92 93 94 95 96 97
        end
    end

(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
  let rec lookup v ty = match ty.ty_node with
98
    | Tyvar u when tv_equal u v -> true
MARCHE Claude's avatar
MARCHE Claude committed
99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
    | _ -> ty_any (lookup v) ty
  in
  let lookup v = List.exists (lookup v) fs.ls_args in
  let rec inspect ty = match ty.ty_node with
    | Tyvar u when not (lookup u) -> false
    | _ -> ty_all inspect ty
  in
  inspect (of_option fs.ls_value)

(** Patterns, terms, and formulas *)

let lparen_l fmt () = fprintf fmt "@ ("
let lparen_r fmt () = fprintf fmt "(@,"
let print_paren_l fmt x = print_list_delim lparen_l rparen comma fmt x
let print_paren_r fmt x = print_list_delim lparen_r rparen comma fmt x

MARCHE Claude's avatar
MARCHE Claude committed
115 116 117 118
let arrow fmt () = fprintf fmt "@ -> "
let print_arrow_list fmt x = print_list arrow fmt x
let print_space_list fmt x = print_list space fmt x

119
let rec print_pat info fmt p = match p.pat_node with
MARCHE Claude's avatar
MARCHE Claude committed
120 121
  | Pwild -> fprintf fmt "_"
  | Pvar v -> print_vs fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
122 123 124 125 126 127 128 129 130 131
  | Pas (p,v) ->
      fprintf fmt "(%a as %a)" (print_pat info) p print_vs v
  | Por (p,q) ->
      fprintf fmt "(%a|%a)" (print_pat info) p (print_pat info) q
  | Papp (cs,pl) -> 
      begin match query_syntax info.info_syn cs.ls_name with
        | Some s -> syntax_arguments s (print_pat info) fmt pl
        | _ -> fprintf fmt "%a%a"
            print_ls cs (print_paren_r (print_pat info)) pl
      end
MARCHE Claude's avatar
MARCHE Claude committed
132

133 134
let print_vsty info fmt v =
  fprintf fmt "(%a:%a)" print_vs v (print_ty info) v.vs_ty
MARCHE Claude's avatar
MARCHE Claude committed
135 136 137 138 139 140 141 142 143 144 145

let print_quant fmt = function
  | Fforall -> fprintf fmt "forall"
  | Fexists -> fprintf fmt "exists"

let print_binop fmt = function
  | Fand -> fprintf fmt "/\\"
  | For -> fprintf fmt "\\/"
  | Fimplies -> fprintf fmt "->"
  | Fiff -> fprintf fmt "<->"

146
let print_label = Pretty.print_label
MARCHE Claude's avatar
MARCHE Claude committed
147 148 149

let protect_on x s = if x then "(" ^^ s ^^ ")" else s

150 151 152 153 154 155
let rec print_term info fmt t = print_lrterm false false info fmt t
and     print_fmla info fmt f = print_lrfmla false false info fmt f
and print_opl_term info fmt t = print_lrterm true  false info fmt t
and print_opl_fmla info fmt f = print_lrfmla true  false info fmt f
and print_opr_term info fmt t = print_lrterm false true  info fmt t
and print_opr_fmla info fmt f = print_lrfmla false true  info fmt f
MARCHE Claude's avatar
MARCHE Claude committed
156

157 158
and print_lrterm opl opr info fmt t = match t.t_label with
  | [] -> print_tnode opl opr info fmt t
MARCHE Claude's avatar
MARCHE Claude committed
159
  | ll -> fprintf fmt "(%a %a)"
160
      (print_list space print_label) ll (print_tnode false false info) t
MARCHE Claude's avatar
MARCHE Claude committed
161

162 163
and print_lrfmla opl opr info fmt f = match f.f_label with
  | [] -> print_fnode opl opr info fmt f
MARCHE Claude's avatar
MARCHE Claude committed
164
  | ll -> fprintf fmt "(%a %a)"
165
      (print_list space print_label) ll (print_fnode false false info) f
MARCHE Claude's avatar
MARCHE Claude committed
166

167
and print_tnode opl opr info fmt t = match t.t_node with
MARCHE Claude's avatar
MARCHE Claude committed
168 169 170 171
  | Tbvar _ ->
      assert false
  | Tvar v ->
      print_vs fmt v
MARCHE Claude's avatar
MARCHE Claude committed
172
  | Tconst (ConstInt n) -> fprintf fmt "%s%%Z" n
173
  | Tconst (ConstReal c) ->
MARCHE Claude's avatar
MARCHE Claude committed
174 175
      Print_real.print_with_integers
	"(%s)%%R" "(%s * %s)%%R" "(%s / %s)%%R" fmt c
176 177
  | Tif (f,t1,t2) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
178
        (print_fmla info) f (print_term info) t1 (print_opl_term info) t2
MARCHE Claude's avatar
MARCHE Claude committed
179 180
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
MARCHE Claude's avatar
MARCHE Claude committed
181
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
182
        print_vs v (print_opl_term info) t1 (print_opl_term info) t2;
MARCHE Claude's avatar
MARCHE Claude committed
183
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  | Tcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
185
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
186
        (print_term info) t
187
        (print_list newline (print_tbranch info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
188 189 190
  | Teps fb ->
      let v,f = f_open_bound fb in
      fprintf fmt (protect_on opr "epsilon %a.@ %a")
191
        (print_vsty info) v (print_opl_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
192 193
      forget_var v
  | Tapp (fs, tl) ->
194
    begin match query_syntax info.info_syn fs.ls_name with
195
      | Some s ->
196
          syntax_arguments s (print_term info) fmt tl
MARCHE Claude's avatar
MARCHE Claude committed
197
      | _ -> if unambig_fs fs
MARCHE Claude's avatar
MARCHE Claude committed
198
          then fprintf fmt "(%a %a)" print_ls fs
199
            (print_space_list (print_term info)) tl
MARCHE Claude's avatar
MARCHE Claude committed
200
          else fprintf fmt (protect_on opl "%a%a:%a") print_ls fs
201
            (print_paren_r (print_term info)) tl (print_ty info) t.t_ty
MARCHE Claude's avatar
MARCHE Claude committed
202 203
    end

204
and print_fnode opl opr info fmt f = match f.f_node with
MARCHE Claude's avatar
MARCHE Claude committed
205 206 207
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
      fprintf fmt (protect_on opr "%a %a%a,@ %a") print_quant q
208 209
        (print_space_list (print_vsty info)) vl
        (print_tl info) tl (print_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
210 211 212 213 214 215 216
      List.iter forget_var vl
  | Ftrue ->
      fprintf fmt "True"
  | Ffalse ->
      fprintf fmt "False"
  | Fbinop (b,f1,f2) ->
      fprintf fmt (protect_on (opl || opr) "%a %a@ %a")
217
        (print_opr_fmla info) f1 print_binop b (print_opl_fmla info) f2
MARCHE Claude's avatar
MARCHE Claude committed
218
  | Fnot f ->
219
      fprintf fmt (protect_on opr "~ %a") (print_opl_fmla info) f
MARCHE Claude's avatar
MARCHE Claude committed
220 221
  | Flet (t,f) ->
      let v,f = f_open_bound f in
MARCHE Claude's avatar
MARCHE Claude committed
222
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
223
        print_vs v (print_opl_term info) t (print_opl_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
224
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
225
  | Fcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
226
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
227
        (print_term info) t
228
        (print_list newline (print_fbranch info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
229 230
  | Fif (f1,f2,f3) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
231
        (print_fmla info) f1 (print_fmla info) f2 (print_opl_fmla info) f3
MARCHE Claude's avatar
MARCHE Claude committed
232
  | Fapp (ps, tl) ->
233
    begin match query_syntax info.info_syn ps.ls_name with
234
      | Some s -> syntax_arguments s (print_term info) fmt tl
MARCHE Claude's avatar
MARCHE Claude committed
235
      | _ -> fprintf fmt "(%a %a)" print_ls ps
236
          (print_space_list (print_term info)) tl
MARCHE Claude's avatar
MARCHE Claude committed
237 238
    end

239
and print_tbranch info fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
240
  let p,t = t_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
241
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
242 243
    (print_pat info) p (print_term info) t;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
244

245
and print_fbranch info fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
246
  let p,f = f_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
247
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
248 249
    (print_pat info) p (print_fmla info) f;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
250

251
and print_tl info fmt tl =
MARCHE Claude's avatar
MARCHE Claude committed
252
  if tl = [] then () else fprintf fmt "@ [%a]"
253
    (print_list alt (print_list comma (print_expr info))) tl
MARCHE Claude's avatar
MARCHE Claude committed
254

255
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
MARCHE Claude's avatar
MARCHE Claude committed
256 257 258

(** Declarations *)

259
let print_constr info fmt cs =
MARCHE Claude's avatar
MARCHE Claude committed
260
  fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
261
    (print_paren_l (print_ty info)) cs.ls_args
MARCHE Claude's avatar
MARCHE Claude committed
262

263
let print_type_decl info fmt (ts,def) = match def with
MARCHE Claude's avatar
MARCHE Claude committed
264 265
  | Tabstract -> begin match ts.ts_def with
      | None ->
MARCHE Claude's avatar
MARCHE Claude committed
266
          fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
267
            print_ts ts (print_arrow_list print_tv) ts.ts_args
MARCHE Claude's avatar
MARCHE Claude committed
268 269
      | Some ty ->
          fprintf fmt "@[<hov 2>Definition %a %a :=@ %a@]@\n@\n"
270
            print_ts ts (print_arrow_list print_tv) ts.ts_args
271
	    (print_ty info) ty
MARCHE Claude's avatar
MARCHE Claude committed
272 273
      end
  | Talgebraic csl ->
MARCHE Claude's avatar
MARCHE Claude committed
274
      fprintf fmt "@[<hov 2>Inductive %a %a :=@\n@[<hov>%a@].@]@\n@\n"
275
        print_ts ts (print_arrow_list print_tv) ts.ts_args
276
        (print_list newline (print_constr info)) csl
MARCHE Claude's avatar
MARCHE Claude committed
277

278 279 280
let print_type_decl info fmt d =
  if not (Sid.mem (fst d).ts_name info.info_rem) then
    (print_type_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
281

282
let print_ls_type ?(arrow=false) info fmt ls =
MARCHE Claude's avatar
MARCHE Claude committed
283 284
  if arrow then fprintf fmt " ->@ ";
  match ls with
MARCHE Claude's avatar
MARCHE Claude committed
285
  | None -> fprintf fmt "Prop"
286
  | Some ty -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
287

288
let print_logic_decl info fmt (ls,ld) = match ld with
MARCHE Claude's avatar
MARCHE Claude committed
289 290
  | Some ld ->
      let vl,e = open_ls_defn ld in
MARCHE Claude's avatar
MARCHE Claude committed
291
      fprintf fmt "@[<hov 2>Definition %a%a: %a :=@ %a.@]@\n@\n"
292 293 294
        print_ls ls (print_space_list (print_vsty info)) vl
        (print_ls_type info) ls.ls_value
        (print_expr info) e;
MARCHE Claude's avatar
MARCHE Claude committed
295 296
      List.iter forget_var vl
  | None ->
MARCHE Claude's avatar
MARCHE Claude committed
297
      fprintf fmt "@[<hov 2>Parameter %a: %a@ %a.@]@\n@\n"
298 299
        print_ls ls (print_arrow_list (print_ty info)) ls.ls_args
        (print_ls_type ~arrow:(List.length ls.ls_args > 0) info) ls.ls_value
MARCHE Claude's avatar
MARCHE Claude committed
300

301 302 303
let print_logic_decl info fmt d =
  if not (Sid.mem (fst d).ls_name info.info_rem) then 
    (print_logic_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
304

305 306
let print_ind info fmt (pr,f) =
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla info) f
MARCHE Claude's avatar
MARCHE Claude committed
307

308
let print_ind_decl info fmt (ps,bl) =
MARCHE Claude's avatar
MARCHE Claude committed
309
  fprintf fmt "@[<hov 2>Inductive %a%a : Prop :=@ @[<hov>%a@].@]@\n@\n"
310 311
     print_ls ps (print_paren_l (print_ty info)) ps.ls_args
     (print_list newline (print_ind info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
312

313 314 315
let print_ind_decl info fmt d =
  if not (Sid.mem (fst d).ls_name info.info_rem) then 
    (print_ind_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
316 317 318 319 320

let print_pkind fmt = function
  | Paxiom -> fprintf fmt "Axiom"
  | Plemma -> fprintf fmt "Lemma"
  | Pgoal  -> fprintf fmt "Theorem"
321
  | Pskip  -> assert false (* impossible *)
MARCHE Claude's avatar
MARCHE Claude committed
322

MARCHE Claude's avatar
MARCHE Claude committed
323
let print_proof fmt = function
324 325
  | Paxiom | Pskip -> ()
  | Plemma | Pgoal -> fprintf fmt "Qed.@\n"
MARCHE Claude's avatar
MARCHE Claude committed
326

327 328 329 330 331
let print_decl info fmt d = match d.d_node with
  | Dtype tl  -> print_list nothing (print_type_decl info) fmt tl
  | Dlogic ll -> print_list nothing (print_logic_decl info) fmt ll
  | Dind il   -> print_list nothing (print_ind_decl info) fmt il
  | Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem -> ()
MARCHE Claude's avatar
MARCHE Claude committed
332
  | Dprop (k,pr,f) ->
333
      fprintf fmt "@[<hov 2>%a %a : %a.@]@\n%a@\n" print_pkind k
334
        print_pr pr (print_fmla info) f print_proof k;
335
      forget_tvs ()
MARCHE Claude's avatar
MARCHE Claude committed
336

337 338
let print_decls info fmt dl =
  fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl info)) dl
MARCHE Claude's avatar
MARCHE Claude committed
339

340 341
let print_task pr thpr ?old fmt task =
  ignore old;
342
  forget_all ();
343 344
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
Andrei Paskevich's avatar
Andrei Paskevich committed
345 346 347
  let info = {
    info_syn = get_syntax_map task;
    info_rem = get_remove_set task } in
348
  print_decls info fmt (Task.task_decls task)
MARCHE Claude's avatar
MARCHE Claude committed
349

350
let () = register_printer "coq" print_task
MARCHE Claude's avatar
MARCHE Claude committed
351