Commit c84ba52e authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Add [rc::inlined_prelude] and [rc::inlined_final] comment annotation.

parent ea6a5590
......@@ -602,20 +602,26 @@ The Coq context (in spec and proof sections) using the following annotation:
## Inlined Coq code
Coq code can be inlined at the beginning (of the section) of the generated
spec file using the following syntax.
An arbitrary line of Coq code can be inlined in the generated specification
file using the following syntax (for single of multiple lines).
```c
//@rc::inlined <code line>
```
For multiple lines, use the following syntax.
```c
//@rc::inlined
//@<code line 1>
//@<code line 2>
//@<code line 3>
//@rc::end
```
With `rc::inlined`, the code is inserted at the beginning of the main section
of the specification file.
To inline Coq code at the beginning of the file (before the section) you can
use the tag `rc::inlined_prelude` instead. This is typically useful when you
want to define a notation (and want it to be available in proof files).
To inline Coq code at the end of the file (after the section) you can use the
tag `rc::inlined_final` instead.
## Type definition
......
(** Support for annotations in special comments. *)
type inlined_code =
{ ic_prelude : string list
; ic_section : string list
; ic_final : string list }
type comment_annots =
{ ca_inlined : string list
{ ca_inlined : inlined_code
; ca_requires : string list
; ca_imports : (string * string) list
; ca_proof_imports : (string * string) list
......@@ -50,86 +55,89 @@ let read_typedef : string -> Rc_annot.typedef option = fun s ->
try Some(parse_string s) with Earley.Parse_error(_,_) -> None
let parse_annots : string list -> comment_annots = fun ls ->
let error msg =
Panic.panic_no_pos "Comment annotation error: %s." msg
let error fmt =
Panic.panic_no_pos ("Comment annotation error: " ^^ fmt ^^ ".")
in
let imports = ref [] in
let requires = ref [] in
let inlined = ref [] in
let inlined_top = ref [] in
let inlined_end = ref [] in
let typedefs = ref [] in
let context = ref [] in
let rec loop inline ls =
let read_block start_tag ls =
let rec read_block acc ls =
match ls with
| AL_comm(s) :: ls -> read_block (s :: acc) ls
| AL_annot("end", None) :: ls -> (acc, ls)
| AL_annot("end", _ ) :: ls ->
error "[rc::end] does not expect a payload"
| AL_annot(_ , _ ) :: ls ->
error "unclosed [rc::%s] annotation" start_tag
| AL_none :: ls ->
error "interrupted block"
| [] ->
error "unclosed [rc::%s] annotation" start_tag
in
read_block [] ls
in
let rec loop ls =
match ls with
| [] -> if inline then error "unclosed [rc::inlined] annotation"
| l :: ls ->
match read_line l with
| AL_annot(n,p) ->
| [] -> ()
| AL_none :: ls -> loop ls
| AL_comm(_) :: ls -> error "no block has been started"
| AL_annot(n,p) :: ls ->
let get_payload () =
match p with Some(s) -> s | None ->
error "annotation [rc::%s] expects a payload" n
in
let add_inlined r p ls =
let (lines, ls) =
match p with
| Some(s) -> ([s], ls)
| None -> read_block n ls
in
r := lines @ !r; ls
in
match n with
| "inlined" -> loop (add_inlined inlined p ls)
| "inlined_prelude" -> loop (add_inlined inlined_top p ls)
| "inlined_final" -> loop (add_inlined inlined_end p ls)
| "end" -> error "no block has been started"
| "import" ->
begin
match (read_import (get_payload ())) with
| Some(i) -> imports := i :: !imports; loop ls
| None -> error "invalid [rc::%s] annotation" n
end
| "require" ->
begin
let s = String.trim (get_payload ()) in
requires := s :: !requires; loop ls
end
| "typedef" ->
begin
match (read_typedef (get_payload ())) with
| Some(t) -> typedefs := t :: !typedefs; loop ls
| None -> error ("invalid [rc::typedef] annotation")
end
| "context" ->
begin
let get_payload () =
match p with Some(s) -> s | None ->
error ("annotation [rc::" ^ n ^ "] expects a payload")
in
let no_payload () =
match p with None -> () | Some(_) ->
error ("annotation [rc::" ^ n ^ "] does not expects a payload")
in
let check_inline b =
if inline <> b then
error ("unexpected [rc::" ^ n ^ "] annotation")
in
match n with
| "inlined" ->
begin
check_inline false;
match p with
| Some(s) -> inlined := s :: !inlined; loop inline ls
| None -> loop true ls
end
| "end" ->
check_inline true; no_payload (); loop false ls
| "import" ->
begin
check_inline false;
match (read_import (get_payload ())) with
| Some(i) -> imports := i :: !imports; loop inline ls
| None ->
error ("invalid [rc::import] annotation")
end
| "require" ->
begin
check_inline false;
let s = String.trim (get_payload ()) in
requires := s :: !requires; loop inline ls
end
| "typedef" ->
begin
check_inline false;
match (read_typedef (get_payload ())) with
| Some(t) -> typedefs := t :: !typedefs; loop inline ls
| None ->
error ("invalid [rc::typedef] annotation")
end
| "context" ->
check_inline false;
context := get_payload () :: !context;
loop inline ls
| _ ->
error ("unknown annotation [rc::" ^ n ^ "]")
context := get_payload () :: !context;
loop ls
end
| AL_comm(s) ->
if not inline then error "ill-placed inlined line";
inlined := s :: !inlined;
loop inline ls
| AL_none ->
if inline then error "invalid line after a [rc::inlined] annotation";
loop inline ls
| _ ->
error "unknown annotation [rc::%s]" n
in
loop false ls;
loop (List.map read_line ls);
let imports = List.rev !imports in
let proof_imports = List.filter (fun (_,_,w) -> w = ProofsOnly) imports in
let code_imports = List.filter (fun (_,_,w) -> w = CodeOnly ) imports in
let imports = List.filter (fun (_,_,w) -> w = Default ) imports in
{ ca_inlined = List.rev !inlined
let ic_prelude = List.rev !inlined_top in
let ic_section = List.rev !inlined in
let ic_final = List.rev !inlined_end in
{ ca_inlined = { ic_prelude ; ic_section ; ic_final }
; ca_proof_imports = List.map (fun (f,m,_) -> (f,m)) proof_imports
; ca_code_imports = List.map (fun (f,m,_) -> (f,m)) code_imports
; ca_imports = List.map (fun (f,m,_) -> (f,m)) imports
......
......@@ -3,6 +3,7 @@ open Extra
open Panic
open Coq_ast
open Rc_annot
open Comment_annot
(* Flags set by CLI. *)
let print_expr_locs = ref true
......@@ -766,30 +767,45 @@ let collect_invs : func_def -> (string * loop_annot) list = fun def ->
in
SMap.fold fn def.func_blocks []
let pp_spec : string -> import list -> string list -> typedef list ->
string list -> Coq_ast.t pp =
let pp_spec : string -> import list -> inlined_code ->
typedef list -> string list -> Coq_ast.t pp =
fun import_path imports inlined typedefs ctxt ff ast ->
(* Formatting utilities. *)
let pp fmt = Format.fprintf ff fmt in
(* Print inlined code (starts with an empty line) *)
let pp_inlined extra_line_after descr ls =
if ls <> [] then pp "\n";
if ls <> [] then
begin
match descr with
| None -> pp "@;(* Inlined code. *)\n"
| Some(descr) -> pp "@;(* Inlined code (%s). *)\n" descr
end;
List.iter (fun s -> if s = "" then pp "\n" else pp "@;%s" s) ls;
if extra_line_after && ls <> [] then pp "\n";
in
(* Printing some header. *)
pp "@[<v 0>From refinedc.typing Require Import typing.@;";
pp "From %s Require Import generated_code.@;" import_path;
List.iter (pp_import ff) imports;
pp "Set Default Proof Using \"Type\".@;@;";
pp "Set Default Proof Using \"Type\".\n";
(* Printing generation data in a comment. *)
pp "(* Generated from [%s]. *)@;" ast.source_file;
pp "@;(* Generated from [%s]. *)" ast.source_file;
(* Printing inlined code (from comments). *)
pp_inlined true (Some "prelude") inlined.ic_prelude;
(* Opening the section. *)
pp "@[<v 2>Section spec.@;";
pp "@;@[<v 2>Section spec.@;";
pp "Context `{!typeG Σ} `{!globalG Σ}.";
List.iter (pp "@;%s.") ctxt;
(* Printing inlined code (from comments). *)
if inlined <> [] then pp "\n@;(* Inlined code. *)\n";
List.iter (fun s -> if s = "" then pp "\n" else pp "@;%s" s) inlined;
pp_inlined false None inlined.ic_section;
(* [Notation] data for printing sugar. *)
let sugar = ref [] in
......@@ -1101,6 +1117,9 @@ let pp_spec : string -> import list -> string list -> typedef list ->
if !opaque <> [] then pp "@;";
let pp_opaque = pp "@;Typeclasses Opaque %s." in
List.iter pp_opaque !opaque;
(* Printing inlined code (from comments). *)
pp_inlined false (Some "final") inlined.ic_final;
pp "@]"
let pp_proof : string -> func_def -> import list -> string list -> proof_kind
......@@ -1342,7 +1361,7 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
type mode =
| Code of import list
| Spec of string * import list * string list * typedef list * string list
| Spec of string * import list * inlined_code * typedef list * string list
| Fprf of string * func_def * import list * string list * proof_kind
let write : mode -> string -> Coq_ast.t -> unit = fun mode fname ast ->
......
Supports Markdown
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