Skip to content

Commit

Permalink
Generic printer for coq
Browse files Browse the repository at this point in the history 
Remove proof lib
  • Loading branch information
@cmester0
cmester0 committed Oct 29, 2024
1 parent 381bd0f commit d52ce43
Show file tree
Hide file tree
Showing 18 changed files with 3,821 additions and 947 deletions.
2,886 changes: 2,305 additions & 581 deletions engine/backends/coq/coq/coq_backend.ml
View file

Large diffs are not rendered by default.

879 changes: 879 additions & 0 deletions engine/lib/ast_utils.ml
View file

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions engine/lib/backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ module Make (InputLanguage : Features.T) (M : BackendMetadata) = struct
("[TODO: this error uses failwith, and thus leads to bad error \
messages, please update it using [Diagnostics.*] helpers] " ^ msg)
span
[@@ocaml.deprecated
"Use more precise errors: Error.unimplemented, Error.assertion_failure \
or a raw Error.t (with Error.raise)"]
(* [@@ocaml.deprecated *)
(* "Use more precise errors: Error.unimplemented, Error.assertion_failure \ *)
(* or a raw Error.t (with Error.raise)"] *)
end
21 changes: 13 additions & 8 deletions engine/lib/concrete_ident/concrete_ident.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -346,7 +346,10 @@ module View = struct
path
in
let sep = "__" in
let subst = String.substr_replace_all ~pattern:sep ~with_:(sep ^ "_") in
let subst =
String.substr_replace_all ~pattern:sep ~with_:(sep ^ "_")
>> String.substr_replace_all ~pattern:"___" ~with_:""
in
let fake_path, real_path =
(* Detects paths of nested items *)
List.rev def_id.path |> List.tl_exn
Expand Down Expand Up @@ -472,7 +475,7 @@ module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct
else escape name
| Constructor { is_struct } ->
let name =
if start_lowercase name || is_reserved_word name then "C_" ^ name
if start_lowercase name || is_reserved_word name then "t_" ^ name
else escape name
in
if is_struct then NP.struct_constructor_name_transform name
Expand All @@ -498,17 +501,19 @@ module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct
|> Option.some
with _ -> None
in
let path, definition =
let path, definition, extra =
match kind with
| Constructor { is_struct = false } ->
( List.drop_last_exn path,
Option.value_exn type_name ^ "_" ^ definition )
Option.value_exn type_name ^ "_" ^ definition,
"t_" (* ^ List.last_exn path ^ "_" *) )
| Field when List.last path |> [%equal: string option] type_name ->
(List.drop_last_exn path, definition)
| AssociatedItem _ -> (List.drop_last_exn path, definition)
| _ -> (path, definition)
(List.drop_last_exn path, definition, "t_" ^ List.last_exn path ^ "_")
| AssociatedItem _ ->
(List.drop_last_exn path, definition, "t_" ^ List.last_exn path ^ "_")
| _ -> (path, definition, "")
in
let definition = rename_definition path definition kind type_name in
let definition = extra ^ rename_definition path definition kind type_name in
View.{ crate; path; definition }

and to_view ({ def_id; kind } : t) : view =
Expand Down
281 changes: 211 additions & 70 deletions engine/lib/generic_printer/generic_printer.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -281,10 +281,10 @@ module Make (F : Features.T) = struct

method virtual pat'_PConstruct_inductive
: super:pat ->
constructor:concrete_ident lazy_doc ->
constructor:global_ident lazy_doc ->
is_record:bool ->
is_struct:bool ->
fields:(concrete_ident lazy_doc * pat lazy_doc) list ->
fields:(global_ident lazy_doc * pat lazy_doc) list ->
document

method virtual pat'_PConstruct_tuple
Expand Down Expand Up @@ -435,37 +435,69 @@ module Make (F : Features.T) = struct
self#expr'_App_field_projection ~super ~field ~e)
| _ -> self#assertion_failure "Primitive app of arity 0"

method _do_not_override_expr'_Construct ~super ~constructor ~is_record
method _do_not_override_expr'_Construct ~super:_ ~constructor ~is_record
~is_struct ~fields ~base =
match constructor with
| `Concrete constructor ->
let constructor =
self#_do_not_override_lazy_of_concrete_ident
AstPos_expr'_Construct_constructor constructor
in
let fields =
List.map
~f:(fun field ->
let name, expr = field#v in
let name =
match name with
| `Concrete name -> name
| _ ->
self#assertion_failure
"expr'.Construct: field: non-`Concrete"
in
( self#_do_not_override_lazy_of_concrete_ident
AstPos_expr'_Construct_fields name,
expr ))
fields
in
self#expr'_Construct_inductive ~super ~constructor ~is_record
~is_struct ~fields ~base
| `TupleCons _ ->
let components = List.map ~f:(fun field -> snd field#v) fields in
self#expr'_Construct_tuple ~super ~components
| `Primitive _ | `TupleType _ | `TupleField _ | `Projector _ ->
self#assertion_failure "Construct unexpected constructors"
let fields_or_empty add_space =
if List.is_empty fields then empty
else
add_space
^^ parens
(separate_map (comma ^^ space) (fun x -> (snd x#v)#p) fields)
in
match (constructor, fields, base) with
| `TupleCons 0, [], _ -> string "tt"
| `TupleCons 1, [ e ], _ ->
let _, e' = e#v in
string "(* tuple_cons 1 *)" ^^ e'#p
| `TupleCons _, _, None -> fields_or_empty empty
| _, _, _ ->
if is_record && is_struct then
match base with
| Some x ->
(* string "(\* record base *\)" ^^ *)
string "Build_" ^^ x#p ^^ fields_or_empty space
| None ->
(* string "(\* record none *\)" ^^ *)
string "Build_t_"
^^ (self#_do_not_override_lazy_of_global_ident
Generated_generic_printer_base
.AstPos_pat'_PConstruct_constructor constructor)
#p ^^ fields_or_empty space
(* string "(TODO: Record 1? *\)" *)
(* F.AST.Record *)
(* ( Option.map ~f:(fst >> pexpr) base, *)
(* List.map *)
(* ~f:(fun (f, e) -> (pfield_ident e.span f, pexpr e)) *)
(* fields ) *)
else if not is_record then
if is_struct then
string "Build_t_"
^^ (self#_do_not_override_lazy_of_global_ident
Generated_generic_printer_base
.AstPos_pat'_PConstruct_constructor constructor)
#p ^^ fields_or_empty space
else
(self#_do_not_override_lazy_of_global_ident
Generated_generic_printer_base
.AstPos_pat'_PConstruct_constructor constructor)
#p ^^ fields_or_empty space
(* if [%matches? Some _] base then *)
(* Diagnostics.failure ~context:(Backend FStar) ~span:e.span *)
(* (AssertionFailure { details = "non-record type with base present" }); *)
(* F.mk_e_app (F.term @@ F.AST.Name (pglobal_ident e.span constructor)) *)
(* @@ List.map ~f:(snd >> pexpr) fields *)
else string "(* TODO: Record? *)"
(* let r = *)
(* F.term *)
(* @@ F.AST.Record *)
(* ( Option.map ~f:(fst >> pexpr) base, *)
(* List.map *)
(* ~f:(fun (f, e') -> (pglobal_ident e.span f, pexpr e')) *)
(* fields ) *)
(* in *)
(* F.mk_e_app *)
(* (F.term @@ F.AST.Name (pglobal_ident e.span constructor)) *)
(* [ r ] *)

method _do_not_override_expr'_GlobalVar ~super global_ident =
match global_ident with
Expand All @@ -477,51 +509,128 @@ module Make (F : Features.T) = struct
self#expr'_GlobalVar_concrete ~super concrete
| `Primitive primitive ->
self#expr'_GlobalVar_primitive ~super primitive
| `TupleCons 0 -> string "tt"
| _ ->
self#assertion_failure
@@ "GlobalVar: expected a concrete or primitive global ident, got:"
^ [%show: global_ident] global_ident

method _do_not_override_pat'_PConstruct ~super ~constructor ~is_record
~is_struct ~fields =
match constructor with
| `Concrete constructor ->
let constructor =
self#_do_not_override_lazy_of_concrete_ident
AstPos_pat'_PConstruct_constructor constructor
in
let fields =
List.map
~f:(fun field ->
let { field; pat } = field#v in
let field =
match field with
| `Concrete field -> field
| _ ->
self#assertion_failure
"expr'.Construct: field: non-`Concrete"
in
let pat =
self#_do_not_override_lazy_of_pat AstPos_field_pat__pat pat
in
( self#_do_not_override_lazy_of_concrete_ident
AstPos_pat'_PConstruct_fields field,
pat ))
fields
in
self#pat'_PConstruct_inductive ~super ~constructor ~is_record
~is_struct ~fields
| `TupleCons _ ->
let components =
List.map
~f:(fun field ->
self#_do_not_override_lazy_of_pat AstPos_field_pat__pat
field#v.pat)
fields
in
self#pat'_PConstruct_tuple ~super ~components
| `Primitive _ | `TupleType _ | `TupleField _ | `Projector _ ->
self#assertion_failure "Construct unexpected constructors"
match (constructor, fields) with
| `TupleCons 0, [] -> string "'tt (* const unit *)" (* Unit pat *)
| `TupleCons 1, [ p ] -> p#p
| `TupleCons _n, _ ->
parens (separate_map (comma ^^ space) (fun x -> x#p) fields)
| _, _ ->
if is_record then
(self#_do_not_override_lazy_of_global_ident
Generated_generic_printer_base
.AstPos_pat'_PConstruct_constructor constructor)
#p ^^ space
^^ parens (separate_map (comma ^^ space) (fun x -> x#p) fields)
(* self#assertion_failure *)
(* "pat'_Construct (record): field: non-`Concrete" *)
else
(* let constructor = *)
(* self#_do_not_override_lazy_of_concrete_ident *)
(* AstPos_pat'_PConstruct_constructor constructor *)
(* in *)

(* self#assertion_failure *)
(* "pat'_Construct (default / enum): field: non-`Concrete" *)
self#pat'_PConstruct_inductive ~super
~constructor:
(self#_do_not_override_lazy_of_global_ident
Generated_generic_printer_base
.AstPos_pat'_PConstruct_constructor constructor)
~is_record ~is_struct
~fields:
(List.map
~f:(fun field ->
let { field; pat } = field#v in
let pat =
self#_do_not_override_lazy_of_pat
Generated_generic_printer_base
.AstPos_pat'_PConstruct_fields pat
in
let field =
self#_do_not_override_lazy_of_global_ident
Generated_generic_printer_base
.AstPos_pat'_PConstruct_fields field
in
(field, pat))
fields)

(* SSP.AST.ConstructorPat *)
(* ( pglobal_ident constructor, *)
(* match fields with *)
(* | [] -> [] *)
(* | _ -> *)
(* [ SSP.AST.TuplePat (List.map ~f:(fun p -> ppat p.pat) fields) ] *)
(* ) *)

(* match constructor with *)
(* | `Concrete constructor -> *)
(* let constructor = *)
(* self#_do_not_override_lazy_of_concrete_ident *)
(* AstPos_pat'_PConstruct_constructor constructor *)
(* in *)
(* let fields = *)
(* List.concat_map *)
(* ~f:(fun field -> *)
(* let { field; pat } = field#v in *)
(* let pat = *)
(* self#_do_not_override_lazy_of_pat AstPos_field_pat__pat pat *)
(* in *)
(* self#_do_not_override_lazy_of_glo _ident *)
(* match field with *)
(* | `Concrete field *)
(* | `Projector (`Concrete field) -> *)
(* [( self#_do_not_override_lazy_of_concrete_ident *)
(* AstPos_pat'_PConstruct_fields field, *)
(* pat )] *)
(* | `Primitive Deref -> *)
(* self#assertion_failure *)
(* "pat'_Construct_Deref: field: non-`Concrete" *)
(* | `Primitive Cast -> *)
(* self#assertion_failure *)
(* "pat'_Construct_Cast: field: non-`Concrete" *)
(* | `Primitive (LogicalOp _) -> *)
(* self#assertion_failure *)
(* "pat'_Construct_LogicalOp: field: non-`Concrete" *)
(* | `TupleCons 0 -> *)
(* self#assertion_failure *)
(* "pat'_Construct_TupleCons0: (tt) field: non-`Concrete" *)
(* | `TupleCons _n -> *)
(* self#assertion_failure *)
(* "pat'_Construct_TupleConsn: (n) field: non-`Concrete" *)
(* | `TupleType _n -> *)
(* self#assertion_failure *)
(* "pat'_Construct_TupleTypen: (n) field: non-`Concrete" *)
(* | `TupleField (_a,_b) -> *)
(* [( pat, concat_map )] *)
(* (* self#assertion_failure *) *)
(* (* "pat'_Construct_TupleField: (a,b) field: non-`Concrete" *) *)
(* | _ -> *)
(* self#assertion_failure *)
(* "pat'_PConstruct: field: non-`Concrete" *)
(* ) *)
(* fields *)
(* in *)
(* self#pat'_PConstruct_inductive ~super ~constructor ~is_record *)
(* ~is_struct ~fields *)
(* | `TupleCons _ -> *)
(* let components = *)
(* List.map *)
(* ~f:(fun field -> *)
(* self#_do_not_override_lazy_of_pat AstPos_field_pat__pat *)
(* field#v.pat) *)
(* fields *)
(* in *)
(* self#pat'_PConstruct_tuple ~super ~components *)
(* | `Primitive _ | `TupleType _ | `TupleField _ | `Projector _ -> *)
(* self#assertion_failure "Construct unexpected constructors" *)

method _do_not_override_ty_TApp ~ident ~args =
match ident with
Expand All @@ -546,6 +655,7 @@ module Make (F : Features.T) = struct

method _do_not_override_item'_Type ~super ~name ~generics ~variants
~is_struct =
let generics, _, _ = generics#v in
if is_struct then
match variants with
| [ variant ] ->
Expand Down Expand Up @@ -594,6 +704,37 @@ module Make (F : Features.T) = struct
self#concrete_ident ~local id)
ast_position id

method _do_not_override_lazy_of_global_ident ast_position
(id : global_ident) : global_ident lazy_doc =
lazy_doc
(fun (id : global_ident) ->
match id with
| `Concrete cid ->
(self#_do_not_override_lazy_of_concrete_ident ast_position cid)
#p
| `Primitive _prim_id -> string "(*TODO*) prim_id"
| `TupleType 0 -> string "unit"
(* | `TupleCons n when n <= 1 -> *)
(* Error.assertion_failure span *)
(* ("Got a [TupleCons " ^ string_of_int n ^ "]") *)
(* | `TupleType n when n <= 14 -> *)
(* F.lid [ "FStar"; "Pervasives"; "tuple" ^ string_of_int n ] *)
(* | `TupleCons n when n <= 14 -> *)
(* F.lid [ "FStar"; "Pervasives"; "Mktuple" ^ string_of_int n ] *)
(* | `TupleType n | `TupleCons n -> *)
(* let reason = "F* doesn't support tuple of size greater than 14" in *)
(* Error.raise *)
(* { *)
(* kind = UnsupportedTupleSize { tuple_size = Int64.of_int n; reason }; *)
(* span; *)
(* } *)
(* | `TupleField _ | `Projector _ -> *)
(* Error.assertion_failure span *)
(* ("pglobal_ident: expected to be handled somewhere else: " *)
(* ^ show_global_ident id) *)
| _ -> string "(* TODO *) error global ident type?")
ast_position id

method _do_not_override_lazy_of_quote ast_position (value : quote)
: quote lazy_doc =
lazy_doc (fun (value : quote) -> self#quote value) ast_position value
Expand Down
3 changes: 0 additions & 3 deletions engine/lib/generic_printer/generic_printer_template.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -233,9 +233,6 @@ struct
method item'_TyAlias ~super:_ ~name:_ ~generics:_ ~ty:_ =
default_document_for "item'_TyAlias"

method item'_Type ~super:_ ~name:_ ~generics:_ ~variants:_ ~is_struct:_ =
default_document_for "item'_Type"

method item'_Type_enum ~super:_ ~name:_ ~generics:_ ~variants:_ =
default_document_for "item'_Type_enum"

Expand Down
Loading

0 comments on commit d52ce43

Please sign in to comment.