Commit 8d4d446d authored by POTTIER Francois's avatar POTTIER Francois

Removed the old Coq printer.

parent de7d6200
open Printf
open Mytools
open Coq
(*#########################################################################*)
(* ** Printing of Coq expressions *)
(** Print a Coq expression *)
let rec string_of_coq c =
let aux = string_of_coq in
match c with
| Coq_var s -> s
| Coq_int n -> "(" ^ (string_of_int n) ^ ")%Z"
| Coq_app (c1,c2) -> sprintf "(%s %s)" (aux c1) (aux c2)
| Coq_impl (c1,c2) -> sprintf "(%s -> %s)" (aux c1) (aux c2)
| Coq_lettuple (cs,c2,c3) -> sprintf "(let '(%s) := %s in %s)" (show_list aux "," cs) (aux c2) (aux c3)
| Coq_forall ((n,c1),c2) -> sprintf "(forall %s : %s, %s)" n (aux c1) (aux c2)
| Coq_fun ((n,c1),c2) -> sprintf "(fun %s : %s => %s)" n (aux c1) (aux c2)
| Coq_wild -> "_"
| Coq_prop -> "Prop"
| Coq_type -> "Type"
| Coq_tuple [] -> aux coq_tt
| Coq_tuple cs -> sprintf "(%s)" (show_list aux "," cs)
| Coq_record lcs -> assert false (* todo: connaitre le constructeur, via une table
sprintf "make_%s" (show_list (fun (l,c) -> sprintf "%s=%s" *)
| Coq_tag (tag, lab, term) ->
let slab = match lab with
| None -> "_"
| Some x -> sprintf "(Label_create '%s)" x
in
sprintf "(%sCFPrint.tag %s %s _ %s)" "@" tag slab (aux term)
| Coq_annot (c1,c2) -> sprintf "(%s : %s)" (aux c1) (aux c2)
let string_of_coq c =
Print_coq.expr c
(** Print a typed identifier [(x:T)] *)
let string_of_typed_var ?(par=true) (x,c) =
show_par par (sprintf "%s : %s" x (string_of_coq c))
(** Print a list of typed identifier [(x1:T1) (x2:T2) .. (xN:TN)] *)
let string_of_typed_vars ?(par=true) tvs =
show_list (string_of_typed_var ~par:par) " " tvs
(** Print a top-level declarations *)
let rec string_of_coqtop ct =
let aux = string_of_coq in
match ct with
| Coqtop_def ((n,c1),c2) -> sprintf "Definition %s : %s := %s." n (aux c1) (aux c2)
| Coqtop_param (n,c1) -> sprintf "Parameter %s :\n%s." n (aux c1)
| Coqtop_instance ((n,c1),g) -> sprintf "%sInstance %s : %s." (if g then "Global " else "") n (aux c1)
| Coqtop_lemma (n,c1) -> sprintf "Lemma %s : %s." n (aux c1)
| Coqtop_proof s -> sprintf "Proof. %s Qed." s
| Coqtop_record r -> sprintf "Record %s %s : %s := %s { \n %s }."
r.coqind_name
(string_of_typed_vars r.coqind_targs)
(aux r.coqind_ret)
(r.coqind_name ^ "_of")
(show_list (string_of_typed_var ~par:false) ";\n" r.coqind_branches)
| Coqtop_ind rs ->
let show_ind r =
sprintf "%s %s : %s := %s"
r.coqind_name
(string_of_typed_vars r.coqind_targs)
(aux r.coqind_ret)
(show_listp (string_of_typed_var ~par:false) "\n | " r.coqind_branches) in
sprintf "Inductive %s." (show_list show_ind "\n\nwith " rs)
| Coqtop_label (x,n) ->
sprintf "Notation \"''%s'\" := (%s) (at level 0) : atom_scope." x (value_variable n)
| Coqtop_implicit (x,xs) ->
let show_implicit (x,i) =
match i with
| Coqi_maximal -> sprintf "[%s]" x
| Coqi_implicit -> sprintf "%s" x
| Coqi_explicit -> sprintf ""
in
sprintf "Implicit Arguments %s [ %s]." x (show_list show_implicit " " xs)
| Coqtop_register (db,x,v) ->
sprintf "Hint Extern 1 (Register %s %s) => Provide %s." db x v
| Coqtop_hint_constructors (xs,base) ->
sprintf "Hint Constructors %s : %s." (show_list show_str " " xs) base
| Coqtop_hint_unfold (xs,base) ->
sprintf "Hint Unfold %s : %s." (show_list show_str " " xs) base
| Coqtop_require x ->
sprintf "Require %s." x
| Coqtop_import x ->
sprintf "Import %s." x
| Coqtop_require_import x ->
sprintf "Require Import %s." x
| Coqtop_set_implicit_args ->
sprintf "Set Implicit Arguments."
| Coqtop_text s ->
s
| Coqtop_declare_module (x,mt) ->
sprintf "Declare Module %s : %s." x (string_of_mod_typ mt)
| Coqtop_module (x,bs,c,d) ->
sprintf "Module %s %s %s %s" x (string_of_mod_bindings bs) (string_of_mod_cast c) (string_of_mod_def x d)
| Coqtop_module_type (x,bs,d) ->
sprintf "Module Type %s %s %s" x (string_of_mod_bindings bs) (string_of_mod_def x d)
| Coqtop_module_type_include x ->
sprintf "Include Type %s." x
| Coqtop_end x ->
sprintf "End %s." x
and string_of_coqtops cts =
show_list string_of_coqtop "\n\n" cts
(** Printing for modules *)
and string_of_mod_def x d =
match d with
| Mod_def_inline m -> sprintf ":= %s." (string_of_mod_expr m)
| Mod_def_declare -> sprintf "."
and string_of_mod_cast c =
match c with
| Mod_cast_exact mt -> sprintf " : %s " (string_of_mod_typ mt)
| Mod_cast_super mt -> sprintf " <: %s " (string_of_mod_typ mt)
| Mod_cast_free -> ""
and string_of_mod_typ mt =
match mt with
| Mod_typ_var x ->
x
| Mod_typ_app xs ->
show_list (fun x ->x) " " xs (* todo: pb si nest ! *)
| Mod_typ_with_def (mt',x,c) ->
sprintf " %s with Definition %s := %s " (string_of_mod_typ mt') x (string_of_coq c)
| Mod_typ_with_mod (mt',x,y) ->
sprintf " %s with Module %s := %s " (string_of_mod_typ mt') x y
and string_of_mod_expr vs =
show_list (fun x ->x) " " vs
and string_of_mod_binding (vs,mt) =
sprintf "(%s : %s)" (show_list (fun x -> x) " " vs) (string_of_mod_typ mt)
and string_of_mod_bindings bs =
show_list string_of_mod_binding " " bs
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment