coq.ml 12 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 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
(**************************************************************************)
(*                                                                        *)
(*  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
open Driver

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
  let n = id_unique lprinter ls.ls_name in
MARCHE Claude's avatar
MARCHE Claude committed
71 72
  (* temporary workaround *)
  let n = if n = "mod" then "bmod" else n in
MARCHE Claude's avatar
MARCHE Claude committed
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
  fprintf fmt "%s" n

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

(** Types *)

let rec print_ty drv fmt ty = match ty.ty_node with
  | Tyvar v -> print_tv fmt v
  | Tyapp (ts, tl) ->
    begin match query_ident drv ts.ts_name with
      | Syntax s -> syntax_arguments s (print_ty drv) fmt tl
      | _ ->
        begin match tl with
          | []  -> print_ts fmt ts
          | l   -> fprintf fmt "(%a@ %a)" print_ts ts
                     (print_list space (print_ty drv)) l 
        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
    | Tyvar u when u == v -> true
    | _ -> 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
113 114 115 116
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

MARCHE Claude's avatar
MARCHE Claude committed
117 118 119 120 121 122 123 124 125 126 127 128
let rec print_pat drv fmt p = match p.pat_node with
  | Pwild -> fprintf fmt "_"
  | Pvar v -> print_vs fmt v
  | Pas (p,v) -> fprintf fmt "%a as %a" (print_pat drv) p print_vs v
  | Papp (cs,pl) ->
    begin match query_ident drv cs.ls_name with
      | Syntax s -> syntax_arguments s (print_pat drv) fmt pl
      | _ -> fprintf fmt "%a%a"
          print_ls cs (print_paren_r (print_pat drv)) pl
    end

let print_vsty drv fmt v =
MARCHE Claude's avatar
MARCHE Claude committed
129
  fprintf fmt "(%a:%a)" print_vs v (print_ty drv) v.vs_ty
MARCHE Claude's avatar
MARCHE Claude committed
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166

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 "<->"

let print_label fmt l = fprintf fmt "\"%s\"" l

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

let rec print_term drv fmt t = print_lrterm false false drv fmt t
and     print_fmla drv fmt f = print_lrfmla false false drv fmt f
and print_opl_term drv fmt t = print_lrterm true  false drv fmt t
and print_opl_fmla drv fmt f = print_lrfmla true  false drv fmt f
and print_opr_term drv fmt t = print_lrterm false true  drv fmt t
and print_opr_fmla drv fmt f = print_lrfmla false true  drv fmt f

and print_lrterm opl opr drv fmt t = match t.t_label with
  | [] -> print_tnode opl opr drv fmt t
  | ll -> fprintf fmt "(%a %a)"
      (print_list space print_label) ll (print_tnode false false drv) t

and print_lrfmla opl opr drv fmt f = match f.f_label with
  | [] -> print_fnode opl opr drv fmt f
  | ll -> fprintf fmt "(%a %a)"
      (print_list space print_label) ll (print_fnode false false drv) f

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

and print_fnode opl opr drv fmt f = match f.f_node with
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
      fprintf fmt (protect_on opr "%a %a%a,@ %a") print_quant q
MARCHE Claude's avatar
MARCHE Claude committed
200
        (print_space_list (print_vsty drv)) vl
MARCHE Claude's avatar
MARCHE Claude committed
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
        (print_tl drv) tl (print_fmla drv) f;
      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")
        (print_opr_fmla drv) f1 print_binop b (print_opl_fmla drv) f2
  | Fnot f ->
      fprintf fmt (protect_on opr "~ %a") (print_opl_fmla drv) f
  | Flet (t,f) ->
      let v,f = f_open_bound f in
      fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
        print_vs v (print_opl_term drv) t (print_opl_fmla drv) f;
      forget_var v
  | Fcase (tl,bl) ->
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
        (print_list comma (print_term drv)) tl
        (print_list newline (print_fbranch drv)) bl
  | Fif (f1,f2,f3) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
        (print_fmla drv) f1 (print_fmla drv) f2 (print_opl_fmla drv) f3
  | Fapp (ps, tl) ->
    begin match query_ident drv ps.ls_name with
      | Syntax s -> syntax_arguments s (print_term drv) fmt tl
MARCHE Claude's avatar
MARCHE Claude committed
227 228
      | _ -> fprintf fmt "(%a %a)" print_ls ps
          (print_space_list (print_term drv)) tl
MARCHE Claude's avatar
MARCHE Claude committed
229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
    end

and print_tbranch drv fmt br =
  let pl,svs,t = t_open_branch br in
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
    (print_list comma (print_pat drv)) pl (print_term drv) t;
  Svs.iter forget_var svs

and print_fbranch drv fmt br =
  let pl,svs,f = f_open_branch br in
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
    (print_list comma (print_pat drv)) pl (print_fmla drv) f;
  Svs.iter forget_var svs

and print_tl drv fmt tl =
  if tl = [] then () else fprintf fmt "@ [%a]"
    (print_list alt (print_list comma (print_expr drv))) tl

and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)

(** Declarations *)

let print_constr drv fmt cs =
  fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
    (print_paren_l (print_ty drv)) cs.ls_args

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

let print_type_decl drv fmt d =
  match query_ident drv (fst d).ts_name with
    | Syntax _ -> ()
    | _ -> print_type_decl drv fmt d; forget_tvs ()

MARCHE Claude's avatar
MARCHE Claude committed
275 276 277
let print_ls_type drv fmt ls = match ls with
  | None -> fprintf fmt "Prop"
  | Some ty -> print_ty drv fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
278 279 280 281

let print_logic_decl drv fmt (ls,ld) = match ld with
  | Some ld ->
      let vl,e = open_ls_defn ld in
MARCHE Claude's avatar
MARCHE Claude committed
282 283 284
      fprintf fmt "@[<hov 2>Definition %a%a: %a :=@ %a.@]@\n@\n"
        print_ls ls (print_space_list (print_vsty drv)) vl
        (print_ls_type drv) ls.ls_value
MARCHE Claude's avatar
MARCHE Claude committed
285 286 287
        (print_expr drv) e;
      List.iter forget_var vl
  | None ->
MARCHE Claude's avatar
MARCHE Claude committed
288 289 290
      fprintf fmt "@[<hov 2>Parameter %a: %a@ -> %a.@]@\n@\n"
        print_ls ls (print_arrow_list (print_ty drv)) ls.ls_args
        (print_ls_type drv) ls.ls_value
MARCHE Claude's avatar
MARCHE Claude committed
291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314

let print_logic_decl drv fmt d =
  match query_ident drv (fst d).ls_name with
    | Syntax _ -> ()
    | _ -> print_logic_decl drv fmt d; forget_tvs ()

let print_ind drv fmt (pr,f) =
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla drv) f

let print_ind_decl drv fmt (ps,bl) =
  fprintf fmt "@[<hov 2>Inductive %a%a : Prop :=@ @[<hov>%a@].@]@\n@\n"
     print_ls ps (print_paren_l (print_ty drv)) ps.ls_args
     (print_list newline (print_ind drv)) bl

let print_ind_decl drv fmt d =
  match query_ident drv (fst d).ls_name with
    | Syntax _ -> ()
    | _ -> print_ind_decl drv fmt d; forget_tvs ()

let print_pkind fmt = function
  | Paxiom -> fprintf fmt "Axiom"
  | Plemma -> fprintf fmt "Lemma"
  | Pgoal  -> fprintf fmt "Theorem"

MARCHE Claude's avatar
MARCHE Claude committed
315 316 317 318
let print_proof fmt = function
  | Paxiom -> ()
  | Plemma | Pgoal  -> fprintf fmt "Admitted.@\n"

MARCHE Claude's avatar
MARCHE Claude committed
319
let print_prop_decl drv fmt (k,pr,f) =
MARCHE Claude's avatar
MARCHE Claude committed
320 321
  fprintf fmt "@[<hov 2>%a %a : %a.@]@\n%a@\n" print_pkind k
    print_pr pr (print_fmla drv) f print_proof k
MARCHE Claude's avatar
MARCHE Claude committed
322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338

let print_prop_decl drv fmt (k,pr,f) =
  match k, query_ident drv pr.pr_name with
    | Paxiom, Remove -> ()
    | _ -> print_prop_decl drv fmt (k,pr,f); forget_tvs ()

let print_decl drv fmt d = match d.d_node with
  | Dtype tl  -> print_list nothing (print_type_decl drv) fmt tl
  | Dlogic ll -> print_list nothing (print_logic_decl drv) fmt ll
  | Dind il   -> print_list nothing (print_ind_decl drv) fmt il
  | Dprop p   -> print_prop_decl drv fmt p

let print_decls drv fmt dl =
  fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl drv)) dl

let print_context drv fmt task =
  forget_all (); 
MARCHE Claude's avatar
MARCHE Claude committed
339
  print_decls drv fmt (Task.task_decls task)
MARCHE Claude's avatar
MARCHE Claude committed
340 341 342

let () = register_printer "coq" print_context