Commit fa361ff1 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Progress on toplevel elements.

parent 9ded32ff
......@@ -33,6 +33,9 @@ let within =
let quote =
string "'"
let dot =
string "."
(* -------------------------------------------------------------------------- *)
(* Applications. *)
......@@ -164,7 +167,7 @@ and expr3 = function
expr3 e2
| Coq_fun ((x, e1), e2) ->
block
(string "fun" ^^ space ^^ string x ^^ colon)
(string "fun " ^^ string x ^^ colon)
(break 1 ^^ expr e1)
(break 1 ^^ doublearrow)
^/^
......@@ -177,6 +180,152 @@ and expr e =
(* -------------------------------------------------------------------------- *)
(* Typed variables: [x : T]. *)
(* Raw. *)
let var (x, t) =
string x ^^ colon ^/^ expr t
(* With parentheses and a trailing space. *)
let pvar xt =
parens (var xt) ^^ break 1
let pvars xts =
concat_map pvar xts
(* A list of field declarations, separated with semicolons. *)
let fields xts =
separate_map (semi ^^ break 1) var xts
(* -------------------------------------------------------------------------- *)
(* Toplevel elements. *)
(* A definition, without a leading keyword, but with a leading space.
[ x : d1 := d2]. *)
let definition x d1 d2 =
block
(space ^^ x ^^ colon)
(break 1 ^^ d1)
(break 1 ^^ colonequals)
^/^
d2
(* A parameter, without a leading keyword, but with a leading space.
[ x : d1]. *)
let parameter x d1 =
block
(space ^^ string x ^^ colon)
(break 1 ^^ d1)
empty
(* The right-hand side of a record declaration. [Foo { ... }]. *)
let record_rhs r =
string (r.coqind_name ^ "_of") ^^ space ^^
braces (fields r.coqind_branches)
(* The right-hand side of a sum declaration. [| x1 : T1 | x2 : T2 ...]. *)
let sum_rhs r =
concat_map (fun xt ->
hardline ^^ string "| " ^^ var xt
) r.coqind_branches
(* The left-hand side of a record or sum declaration. [ foo params : T := rhs]. *)
let inductive_lhs rhs r =
definition
(string r.coqind_name ^/^ pvars r.coqind_targs)
(expr r.coqind_ret)
(rhs r)
(* A toplevel element. *)
let top = function
| Coqtop_def ((x, e1), e2) ->
string "Definition" ^^
definition
(string x) (expr e1)
(expr e2)
| Coqtop_param (x, e1) ->
string "Parameter" ^^
parameter x (expr e1)
| Coqtop_instance ((x, e1), global) ->
string ((if global then "Global " else "") ^ "Instance") ^^
parameter x (expr e1)
| Coqtop_lemma (x, e1) ->
string "Lemma" ^^
parameter x (expr e1)
| Coqtop_proof s ->
string (Printf.sprintf "Proof. %s Qed." s) (* TEMPORARY newline problem *)
| Coqtop_record r ->
string "Record" ^^
inductive_lhs record_rhs r
| Coqtop_ind rs ->
string "Inductive" ^^
separate_map
(hardline ^^ hardline ^^ string "with")
(inductive_lhs sum_rhs)
rs
let top t =
group (top t ^^ dot)
(*
| Coqtop_ind rs ->
let show_ind r =
sprintf "%s %s : %s := %s"
r.coqind_name
(string_of_typed_vars r.coqind_targs)
(expr 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
*)
(* -------------------------------------------------------------------------- *)
let expr e : string =
let b = Buffer.create 1024 in
PPrintEngine.ToBuffer.pretty 0.9 width b (expr e);
......
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