Skip to content

Commit

Permalink
Fixed some minor issues
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Jul 6, 2023
1 parent 8c0016c commit 17c2271
Show file tree
Hide file tree
Showing 3 changed files with 52 additions and 66 deletions.
34 changes: 9 additions & 25 deletions engine/backends/coq/coq/coq_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ struct
| TApp { ident = `TupleType n; args } when n >= 2 ->
C.AST.Product (args_ty span args)
| TApp { ident; args } ->
C.AST.AppTy (pglobal_ident ident ^ "_t", args_ty span args)
C.AST.AppTy (pglobal_ident ident, args_ty span args)
| TArrow (inputs, output) ->
List.fold_right ~init:(pty span output)
~f:(fun x y -> C.AST.Arrow (x, y))
Expand Down Expand Up @@ -377,36 +377,20 @@ struct
]
| TyAlias { name; generics; ty } ->
[ C.AST.Notation (pconcrete_ident name ^ "_t", pty span ty) ]
(* record *)
| Type { name; generics; variants = [ v ]; is_struct = true } ->
| Type { name; generics; variants; is_struct = true (* record *) } ->
[
(* TODO: generics *)
C.AST.Record
( U.Concrete_ident_view.to_definition_name name,
p_record_record span v.arguments );
p_record span variants );
]
(* enum *)
| Type { name; generics; variants } ->
| Type { name; generics; variants; is_struct = false (* enum *) } ->
[
C.AST.Inductive
( U.Concrete_ident_view.to_definition_name name,
List.map ~f:(pgeneric_param span) generics.params,
p_inductive span variants name );
]
(* TODO: this is never matched, now *)
(* | Type { name; generics; variants } -> *)
(* [ *)
(* C.AST.Notation *)
(* ( U.Concrete_ident_view.to_definition_name name, *)
(* C.AST.Product (List.map ~f:snd (p_record span variants name)) ); *)
(* C.AST.Definition *)
(* ( U.Concrete_ident_view.to_definition_name name, *)
(* [], *)
(* C.AST.Var "id", *)
(* C.AST.Arrow *)
(* ( C.AST.Name (U.Concrete_ident_view.to_definition_name name), *)
(* C.AST.Name (U.Concrete_ident_view.to_definition_name name) ) ); *)
(* ] *)
| IMacroInvokation { macro; argument; span } -> (
let unsupported () =
let id = [%show: concrete_ident] macro in
Expand Down Expand Up @@ -614,19 +598,19 @@ struct
(* :: p_inductive span xs parrent_name *)
(* | _ -> [] *)

and p_record span variants parrent_name : (string * C.AST.ty) list =
and p_record span variants : (string * C.AST.ty) list =
match variants with
| { name; arguments = [ (arg_name, arg_ty) ] } :: xs ->
(U.Concrete_ident_view.to_definition_name arg_name, pty span arg_ty)
:: p_record span xs parrent_name
:: p_record span xs
| { name; arguments = [] } :: xs ->
("TODO FIELD?", __TODO_ty__ span "TODO")
:: p_record span xs parrent_name
(U.Concrete_ident_view.to_definition_name name, C.AST.Wild)
:: p_record span xs
| { name; arguments } :: xs ->
( U.Concrete_ident_view.to_definition_name name,
C.AST.RecordTy (pconcrete_ident name, p_record_record span arguments)
)
:: p_record span xs parrent_name
:: p_record span xs
| _ -> []

and p_record_record span arguments : (string * C.AST.ty) list =
Expand Down
5 changes: 3 additions & 2 deletions engine/backends/coq/coq_ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,6 @@ functor
| AST.RecordConstructor (f, args) ->
( "Build_"
^ term_to_string_without_paren f depth
^ " "
^ record_args_to_string args depth,
true )
| AST.Type t ->
Expand Down Expand Up @@ -311,7 +310,9 @@ functor
and record_args_to_string (args : (string * AST.term) list) depth : string =
match args with
| (i, t) :: xs ->
term_to_string_with_paren t depth ^ record_args_to_string xs depth
" "
^ term_to_string_with_paren t depth
^ record_args_to_string xs depth
| _ -> ""

and args_to_string (args : AST.term list) depth : string =
Expand Down
79 changes: 40 additions & 39 deletions engine/lib/phases/phase_record_variants.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,32 +20,39 @@ module Make (FA : Features.T) = struct
Phase_utils.Metadata.make Diagnostics.Phase.RecordVariants
end)

let rec ditem (item : A.item) : B.item list =
match item.v with
| Type { name; generics; variants; is_struct = false } ->
let variants', type_defs =
List.unzip
(List.map ~f:(flatten_variants item.span generics) variants)
in
List.filter_opt type_defs
@ [
{
v =
B.Type
{
name;
generics = dgenerics item.span generics;
variants = variants';
is_struct = false;
};
span = item.span;
ident = item.ident;
};
]
| _ ->
[
{ v = ditem' item.span item.v; span = item.span; ident = item.ident };
]
let rec ditems (items : A.item list) : B.item list =
List.concat_map
~f:(fun item ->
match item.v with
| Type { name; generics; variants; is_struct = false } ->
let variants', type_defs =
List.unzip
(List.map ~f:(flatten_variants item.span generics) variants)
in
List.filter_opt type_defs
@ [
{
v =
B.Type
{
name;
generics = dgenerics item.span generics;
variants = variants';
is_struct = false;
};
span = item.span;
ident = item.ident;
};
]
| _ ->
[
{
v = ditem' item.span item.v;
span = item.span;
ident = item.ident;
};
])
items

and flatten_variants span generics (v : A.variant) : B.variant * B.item option
=
Expand All @@ -55,29 +62,23 @@ module Make (FA : Features.T) = struct
Concrete_ident.of_def_id Type
{
krate = "temp_name";
path = [ { data = TypeNs "my_temp_name"; disambiguator = 0 } ];
path = [ { data = TypeNs "my_temp_name"; disambiguator = 4 } ];
}
in
let b_v' : B.variant =
{
name = b_v.name;
arguments =
[
( new_name,
B.TParam
{
name = "my_temp_name";
id = Ast.LocalIdent.ty_param_id_of_int 0;
} );
];
[ (new_name, B.TApp { ident = `Concrete new_name; args = [] }) ];
is_record = false;
}
in
let temp n : B.variant =
let temp (n, t) : B.variant =
{
name = n;
arguments = [];
is_record = true;
arguments = [ (n, t) ];
is_record = false;
(* Should this be false? *)
(* F.record_variants option; *)
}
in
Expand All @@ -89,7 +90,7 @@ module Make (FA : Features.T) = struct
{
name = new_name;
generics = dgenerics span generics;
variants = List.map ~f:(fun (n, _) -> temp n) b_v.arguments;
variants = List.map ~f:temp b_v.arguments;
is_struct = true;
};
span;
Expand Down

0 comments on commit 17c2271

Please sign in to comment.