MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 4a06dd7f authored by POTTIER Francois's avatar POTTIER Francois
Browse files

First (incomplete) version of printing toplevel Coq elements.

parent fa361ff1
......@@ -125,7 +125,7 @@ let _ =
(*---------------------------------------------------*)
trace "7) printing coq ast";
let result = Print_coq_old.string_of_coqtops coqtops in
let result = Print_coq.tops coqtops in
file_put_contents (debugdirBase ^ "_formulae.v") result;
file_put_contents outputfile result;
......
open PPrint
open Coq
let sprintf format =
Printf.ksprintf string format
(* TEMPORARY newline problem *)
(* -------------------------------------------------------------------------- *)
(* Global parameters. *)
......@@ -187,10 +191,10 @@ and expr e =
let var (x, t) =
string x ^^ colon ^/^ expr t
(* With parentheses and a trailing space. *)
(* With parentheses and with a leading space. *)
let pvar xt =
parens (var xt) ^^ break 1
break 1 ^^ parens (var xt)
let pvars xts =
concat_map pvar xts
......@@ -211,7 +215,7 @@ let definition x d1 d2 =
block
(space ^^ x ^^ colon)
(break 1 ^^ d1)
(break 1 ^^ colonequals)
(break 1 ^^ string ":=")
^/^
d2
......@@ -241,10 +245,21 @@ let sum_rhs r =
let inductive_lhs rhs r =
definition
(string r.coqind_name ^/^ pvars r.coqind_targs)
(string r.coqind_name ^^ pvars r.coqind_targs)
(expr r.coqind_ret)
(rhs r)
(* An implicit argument specification. *)
let implicit (x, i) =
match i with
| Coqi_maximal ->
brackets (string x)
| Coqi_implicit ->
string x
| Coqi_explicit ->
empty
(* A toplevel element. *)
let top = function
......@@ -253,55 +268,53 @@ let top = function
definition
(string x) (expr e1)
(expr e2)
^^ dot
| Coqtop_param (x, e1) ->
string "Parameter" ^^
parameter x (expr e1)
^^ dot
| Coqtop_instance ((x, e1), global) ->
string ((if global then "Global " else "") ^ "Instance") ^^
parameter x (expr e1)
^^ dot
| Coqtop_lemma (x, e1) ->
string "Lemma" ^^
parameter x (expr e1)
^^ dot
| Coqtop_proof s ->
string (Printf.sprintf "Proof. %s Qed." s) (* TEMPORARY newline problem *)
sprintf "Proof. %s Qed." s
| Coqtop_record r ->
string "Record" ^^
inductive_lhs record_rhs r
^^ dot
| 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) ->
^^ dot
| 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) ->
| Coqtop_implicit (x, xs) ->
string "Implicit Arguments " ^^
string x ^^
brackets (separate_map space implicit xs)
^^ dot
| 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_hint_constructors (xs, base) ->
string "Hint Constructors " ^^
separate_map space string xs ^^
colon ^/^
string base
^^ dot
| Coqtop_hint_unfold (xs, base) ->
string "Hint Unfold " ^^
separate_map space string xs ^^
colon ^/^
string base
^^ dot
| Coqtop_require x ->
sprintf "Require %s." x
| Coqtop_import x ->
......@@ -311,17 +324,25 @@ let top t =
| Coqtop_set_implicit_args ->
sprintf "Set Implicit Arguments."
| Coqtop_text s ->
s
sprintf "%s" s
| Coqtop_module_type_include x ->
sprintf "Include Type %s." x
| Coqtop_end x ->
sprintf "End %s." x
let top t =
group (top t)
let tops ts =
concat_map (fun t -> top t ^^ hardline ^^ hardline) ts
(*
| 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
*)
(* -------------------------------------------------------------------------- *)
......@@ -331,3 +352,8 @@ let expr e : string =
PPrintEngine.ToBuffer.pretty 0.9 width b (expr e);
Buffer.contents b
let tops ts : string =
let b = Buffer.create 1024 in
PPrintEngine.ToBuffer.pretty 0.9 width b (tops ts);
Buffer.contents b
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