pretty.ml 6.63 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21
(*                                                                        *)
(*  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
22
open Ident
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23
open Ty
24
open Term
25
open Theory
26

27 28
let print_list_paren x = print_list_delim lparen rparen x

29 30 31 32 33 34 35
let printer =
  let sanitize = sanitizer char_to_alpha char_to_alnumus in
  create_printer [] ~sanitizer:sanitize

let print_ident fmt id = Format.fprintf fmt "%s" (id_unique printer id)

let forget_var v = forget_id printer v.vs_name
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
36

37 38 39
let print_typevar fmt x =
  fprintf fmt "'%a" print_ident x

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
40 41
let rec print_ty fmt ty = match ty.ty_node with
  | Tyvar n ->
42
      fprintf fmt "'%a" print_ident n
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
  | Tyapp (s, []) -> 
44
      print_ident fmt s.ts_name
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
  | Tyapp (s, [t]) -> 
46
      fprintf fmt "%a %a" print_ty t print_ident s.ts_name
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47
  | Tyapp (s, l) -> 
48
      fprintf fmt "(%a)@ %a" (print_list comma print_ty) l print_ident s.ts_name
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
49 50 51 52 53
  
let rec print_term fmt t = match t.t_node with
  | Tbvar n -> 
      assert false
  | Tvar n -> 
54
      print_ident fmt n.vs_name
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
55 56 57 58
  | Tconst (ConstInt s) ->
      fprintf fmt "%s" s
  | Tconst (ConstReal _) ->
      fprintf fmt "<real constant>"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59
  | Tapp (s, tl) ->
60
      fprintf fmt "@[<hov>%a(%a):%a@]" 
61
	print_ident s.ls_name (print_list comma print_term) tl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62
	print_ty t.t_ty
63 64
  | Tlet (t1,tbound) -> 
      let vs,t2 = t_open_bound tbound in
65
      fprintf fmt "(let %a = %a in@ %a)"
66 67
      print_ident vs.vs_name print_term t1 print_term t2;
      forget_var vs
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68 69 70 71
  | Tcase _ ->
      assert false (*TODO*)
  | Teps _ -> 
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
72

Francois Bobot's avatar
Francois Bobot committed
73
let print_vsymbol fmt vs = 
74 75
  fprintf fmt "%a :@ %a" print_ident vs.vs_name print_ty vs.vs_ty

76 77
let rec print_fmla fmt f = match f.f_node with
  | Fapp (s,tl) -> 
78
      fprintf fmt "@[<hov>%a(%a)@]" 
79
	print_ident s.ls_name (print_list comma print_term) tl
80 81
  | Fquant (q,fquant) ->
      let vl,tl,f = f_open_quant fquant in
82
      fprintf fmt "(%s %a %a.@ %a)"
83
        (match q with Fforall -> "forall" | Fexists -> "exists")
84 85
        (print_list comma print_vsymbol) vl print_tl tl print_fmla f;
      List.iter forget_var vl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86 87 88 89
  | Ftrue -> 
      fprintf fmt "true"
  | Ffalse -> 
      fprintf fmt "false)"
90
  | Fbinop (b,f1,f2) -> 
91
      fprintf fmt "(%a@ %s@ %a)"
92 93 94 95 96
        print_fmla f1
        (match b with 
           | Fand -> "and" | For -> "or" 
           | Fimplies -> "->" | Fiff -> "<->")
        print_fmla f2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
97 98 99 100 101
  | Fnot f -> 
      fprintf fmt "(not@ %a)" print_fmla f
  | Flet (t, f) -> 
      let v,f = f_open_bound f in
      fprintf fmt "@[<hov 2>let %a = %a in@ %a@]" print_ident v.vs_name
102 103
        print_term t print_fmla f;
      forget_var v
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104 105 106 107
  | Fcase _ ->
      assert false (*TODO*)
  | Fif _ ->
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

109 110 111 112 113 114 115
and print_tl fmt tl =
  fprintf fmt "[%a]" (print_list alt (print_list comma print_tr)) tl

and print_tr fmt = function
  | TrTerm t -> print_term fmt t
  | TrFmla f -> print_fmla fmt f

116 117 118 119 120 121 122 123 124
let print_lsymbol fmt {ls_name = ls_name; ls_args = tyl; ls_value = vty } = 
  match vty with
    | Some ty ->
        fprintf fmt "%a%a :@ %a" print_ident ls_name
          (print_list_paren comma print_ty) tyl 
          print_ty ty
    | None ->
        fprintf fmt "%a%a" print_ident ls_name
          (print_list_paren comma print_ty) tyl 
125 126

let print_ty_decl fmt (ts,tydef) = match tydef,ts.ts_def with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127 128 129 130 131 132 133 134 135 136 137 138 139
  | Tabstract,None -> 
      fprintf fmt "@[<hov>type %a %a@]" 
	(print_list_paren comma print_typevar) ts.ts_args
	print_ident ts.ts_name
  | Tabstract,Some f -> 
      fprintf fmt "@[<hov>type %a %a =@ @[<hov>%a@]@]" 
	(print_list_paren comma print_typevar) ts.ts_args
	print_ident ts.ts_name
	print_ty f
  | Talgebraic d, None -> 
      fprintf fmt "@[<hov>type %a %a =@ @[<hov>%a@]@]" 
	(print_list_paren comma print_typevar) ts.ts_args
	print_ident ts.ts_name
140
	(print_list newline print_lsymbol) d
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
141 142
  | Talgebraic _, Some _ -> 
      assert false
143 144 145 146 147

let print_vsymbol fmt {vs_name = vs_name; vs_ty = vs_ty} =
  fprintf fmt "%a :@ %a" print_ident vs_name print_ty vs_ty

let print_logic_decl fmt = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148
  | Lfunction (fs,None) -> 
149
      fprintf fmt "@[<hov 2>logic %a@]" print_lsymbol fs
150
  | Lfunction (fs,Some fd) -> 
151
      fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident fs.ls_name
152
        print_fmla (fs_defn_axiom fd)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
153
  | Lpredicate (fs,None) -> 
154
      fprintf fmt "@[<hov 2>logic %a@]" print_lsymbol fs
155
  | Lpredicate (ps,Some fd) -> 
156
      fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident ps.ls_name
157
        print_fmla (ps_defn_axiom fd)
158

159
let print_decl fmt d = match d.d_node with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160
  | Dtype tl -> 
161
      fprintf fmt "@[<hov>%a@ (* *)@]" (print_list newline print_ty_decl) tl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
162
  | Dlogic ldl -> 
163
      fprintf fmt "@[<hov>%a@ (* *)@]" 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
164
	(print_list newline print_logic_decl) ldl 
165
  | Dprop (k,id,fmla) -> 
166
      fprintf fmt "%s %a :@ %a@\n" 
167 168 169
        (match k with Paxiom -> "axiom" | Pgoal -> "goal" | Plemma -> "lemma")
        print_ident id
        print_fmla fmla
170 171
  | Dind (ps, fl) -> 
      fprintf fmt "@[<hov 2>inductive %a ...@]" print_ident ps.ls_name
Francois Bobot's avatar
Francois Bobot committed
172 173 174
  | Duse u -> fprintf fmt "use export %a@\n" print_ident u.th_name
  | Dclone il -> fprintf fmt "(*@[<hov 2>clone export _ with %a@]@\n" 
      (print_list comma (print_pair_delim nothing nothing equal print_ident print_ident)) il 
175

176 177 178
let print_decl_list fmt de = 
  fprintf fmt "@[<hov>%a@]" (print_list newline print_decl) de

179 180
let print_context fmt ctxt = print_list newline print_decl fmt 
  (Context.get_decls ctxt) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181

182
let print_theory fmt t =
183
  fprintf fmt "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n" print_ident t.th_name 
184
    print_context t.th_ctxt;
185 186
  fprintf fmt "@?"