Skip to content

Commit

Permalink
Fixing backend
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Oct 7, 2024
1 parent 20faeb3 commit 2c468ca
Show file tree
Hide file tree
Showing 4 changed files with 64 additions and 35 deletions.
63 changes: 35 additions & 28 deletions engine/backends/coq/coq/coq_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -106,17 +106,17 @@ struct
id.definition
else
(* id.crate ^ "_" ^ *)
(* List.fold_left ~init:"" ~f:(fun x y -> x ^ "_" ^ y) *)
(* List.fold_left ~init:"" ~f:(fun x y -> x ^ "_" ^ y) id.path ^ *)
id.definition

let pglobal_ident (id : global_ident) : string =
match id with
| `Projector (`Concrete cid) | `Concrete cid -> pconcrete_ident cid
| `Concrete cid -> pconcrete_ident cid
| `Projector (`Concrete cid) -> pconcrete_ident cid ^ "_ci"
| `Primitive p_id -> primitive_to_string p_id
| `TupleType _i -> "TODO (global ident) tuple type"
| `TupleCons _i -> "TODO (global ident) tuple cons"
| `Projector (`TupleField _) | `TupleField _ ->
"TODO (global ident) tuple field"
| `Projector (`TupleField _) | `TupleField _ -> "TODO (global ident) tuple field"
| _ -> .

module TODOs_debug = struct
Expand Down Expand Up @@ -167,7 +167,7 @@ struct
| TBool -> C.AST.Bool
| TChar -> __TODO_ty__ span "char"
| TInt k -> C.AST.Int (pint_kind k)
| TStr -> __TODO_ty__ span "str"
| TStr -> C.AST.NameTy "string"
| TApp { ident = `TupleType 0; args = [] } -> C.AST.Unit
| TApp { ident = `TupleType 1; args = [ GType ty ] } -> pty span ty
| TApp { ident = `TupleType n; args } when n >= 2 ->
Expand All @@ -183,7 +183,11 @@ struct
C.AST.ArrayTy (pty span typ, "TODO: Int.to_string length")
| TSlice { ty; _ } -> C.AST.SliceTy (pty span ty)
| TParam i -> C.AST.NameTy i.name
| TAssociatedType _ -> C.AST.WildTy
| TAssociatedType { impl = Self; item } -> C.AST.NameTy (U.Concrete_ident_view.to_definition_name item)
| TAssociatedType { impl = Dyn; item } -> __TODO_ty__ span "pty: Dyn"
| TAssociatedType { impl = Concrete _; item } -> __TODO_ty__ span "pty: Concrete"
| TAssociatedType { impl = LocalBound _; item } -> __TODO_ty__ span "pty: LocalBound"
| TAssociatedType { impl = goal; item } -> __TODO_ty__ span "pty: LocalBound"
| TOpaque _ -> __TODO_ty__ span "pty: TAssociatedType/TOpaque"
| _ -> .

Expand All @@ -194,7 +198,7 @@ struct
(match arg with
| GLifetime _ -> __TODO_ty__ span "lifetime"
| GType x -> pty span x
| GConst _ -> __TODO_ty__ span "const")
| GConst { typ } -> pty span typ)
:: args_ty span xs
| [] -> []

Expand Down Expand Up @@ -254,6 +258,7 @@ struct
(c Core__ops__arith__Rem__rem, (2, [ ""; ".%"; "" ]));
(c Core__ops__bit__Shl__shl, (2, [ ""; " shift_left "; "" ]));
(c Core__ops__bit__Shr__shr, (2, [ ""; " shift_right "; "" ]));
(c Core__ops__bit__Not__not, (1, [ " negb "; "" ]));
(* TODO: those two are not notations/operators at all, right? *)
(* (c "secret_integers::rotate_left", (2, [ "rol "; " "; "" ])); *)
(* (c "hacspec::lib::foldi", (4, [ "foldi "; " "; " "; " "; "" ])); *)
Expand All @@ -275,7 +280,7 @@ struct
let span = e.span in
match e.e with
| Literal l -> C.AST.Const (pliteral e.span l)
| LocalVar local_ident -> C.AST.NameTerm local_ident.name
| LocalVar local_ident -> C.AST.NameTerm (local_ident.name)
| GlobalVar (`TupleCons 0)
| Construct { constructor = `TupleCons 0; fields = []; _ } ->
C.AST.UnitTerm
Expand All @@ -297,8 +302,8 @@ struct
(* __TODO_term__ span "GLOBAL APP?" *)
| App { f; args; _ } ->
let base = pexpr f in
let args = List.map ~f:pexpr args in
C.AST.App (base, args)
let args = List.map ~f:(fun x -> C.AST.TypedTerm (pexpr x, pty span x.typ)) args in
C.AST.TypedTerm (C.AST.App (base, args), pty span e.typ)
| If { cond; then_; else_ } ->
C.AST.If
( pexpr cond,
Expand Down Expand Up @@ -340,8 +345,8 @@ struct
| Construct { is_record = true; constructor; fields; _ } ->
(* TODO: handle base *)
C.AST.RecordConstructor
( pglobal_ident constructor,
List.map ~f:(fun (f, e) -> (pglobal_ident f, pexpr e)) fields )
( "t_" ^ pglobal_ident constructor,
List.map ~f:(fun (f, e) -> (pglobal_ident constructor, pexpr e)) fields )
| Construct { is_record = false; constructor; fields = [ (_f, e) ]; _ } ->
C.AST.App (C.AST.Var (pglobal_ident constructor), [ pexpr e ])
| Construct { constructor; _ } ->
Expand Down Expand Up @@ -392,15 +397,13 @@ struct
("'" ^ pconcrete_ident name ^ "'", C.AST.Type (pty span ty), None);
]
(* record *)
| Type { name; generics; variants = [ v ]; is_struct = true } ->
| Type { name; generics; variants = [ { arguments; is_record = true; _ } ]; is_struct = true } ->
[
(* TODO: generics *)
C.AST.Record
( U.Concrete_ident_view.to_definition_name name,
List.map ~f:(pgeneric_param_as_argument span) generics.params,
List.map
~f:(fun (x, y) -> C.AST.Named (x, y))
(p_record_record span v.arguments) );
List.map ~f:(fun (x, y) -> C.AST.Named (U.Concrete_ident_view.to_definition_name name ^ "_" ^ x, y)) (p_record_record span arguments) );
]
(* enum *)
| Type { name; generics; variants; _ } ->
Expand Down Expand Up @@ -573,7 +576,13 @@ struct
match x.ti_v with
| TIFn fn_ty -> pty span fn_ty
| TIDefault _ -> .
| _ -> __TODO_ty__ span "field_ty" ))
| TIType impl_list ->
C.AST.TypeTy
(* C.AST.Product *)
(* (List.map *)
(* ~f:(fun { goal = { trait; args }; name } -> C.AST.NameTy (U.Concrete_ident_view.to_definition_name trait)) *)
(* impl_list) *)
))
items );
]
| Impl { generics; self_ty; of_trait = name, gen_vals; items } ->
Expand All @@ -583,26 +592,24 @@ struct
List.map ~f:(pgeneric_param_as_argument span) generics.params,
pty span self_ty,
args_ty span gen_vals,
List.map
~f:(fun x ->
match x.ii_v with
List.fold_left ~init:[]
~f:(fun y x ->
y @ (match x.ii_v with
| IIFn { body; params } ->
( U.Concrete_ident_view.to_definition_name x.ii_ident,
[( U.Concrete_ident_view.to_definition_name x.ii_ident,
List.map
~f:(fun { pat; typ; _ } ->
C.AST.Explicit (ppat pat, pty span typ))
params,
pexpr body,
pty span body.typ )
| _ ->
( "todo_name",
[],
__TODO_term__ span "body",
__TODO_ty__ span "typ" ))
pty span body.typ )]
| IIType { typ; parent_bounds } ->
[] (* TODO: Is this just Self? *)))
items );
]
| _ -> .

and p_inductive span variants _parrent_name : C.AST.inductive_case list =
and p_inductive span variants parrent_name : C.AST.inductive_case list =
List.map variants ~f:(fun { name; arguments; is_record; _ } ->
if is_record then
C.AST.InductiveCase
Expand Down
13 changes: 7 additions & 6 deletions engine/backends/coq/coq_ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,15 +163,15 @@ functor
| AST.Product [] | AST.Unit ->
(Lib.Notation.unit_str, false (* TODO: might need paren *))
| AST.TypeTy -> (Lib.Notation.type_str, false (* TODO: might need paren *))
| AST.Int { size = AST.USize; _ } -> ("uint_size", false)
| AST.Int { size; _ } -> ("int" ^ int_size_to_string size, false)
| AST.Int { size = AST.USize; _ } -> ("t_usize", false)
| AST.Int { size; _ } -> ("t_u" ^ int_size_to_string size, false)
| AST.NameTy s -> (s, false)
| AST.RecordTy (name, _fields) ->
(* [ AST.Record (name, fields) ] *) (name, false)
| AST.Product l ->
let ty_str =
String.concat
~sep:(" " ^ "×" ^ " ")
~sep:(" " ^ "*" ^ " ") (* TODO, notations differ for SSProve '×' *)
(List.map ~f:ty_to_string_without_paren l)
in
(ty_str, true)
Expand Down Expand Up @@ -297,7 +297,7 @@ functor
^ ")" (* TODO: Should this be true of false? *)
| AST.DisjunctivePat pats ->
let f pat = pat_to_string pat true depth in
String.concat ~sep:" | " @@ List.map ~f pats
"(" ^ (String.concat ~sep:" | " @@ List.map ~f pats) ^ ")"

and tick_if is_top_expr = if is_top_expr then "'" else ""

Expand Down Expand Up @@ -370,8 +370,8 @@ functor
^ (if List.length args > 0 then " " else "")
^ String.concat ~sep:" "
(List.map
~f:(fun (n, t) ->
"(" ^ n ^ " " ^ ":=" ^ " "
~f:(fun (_n, t) ->
"(" (* ^ n ^ " " ^ ":=" *) ^ " "
^ term_to_string_without_paren t depth
^ ")")
args),
Expand Down Expand Up @@ -423,6 +423,7 @@ functor
^ "]",
true )
| AST.Array [] -> ("!TODO empty array!", false)
| AST.TypedTerm (AST.TypedTerm (e, t), _) -> term_to_string (AST.TypedTerm (e, t)) depth
| AST.TypedTerm (e, t) ->
( term_to_string_without_paren e depth
^ " " ^ ":" ^ " " ^ ty_to_string_with_paren t,
Expand Down
21 changes: 21 additions & 0 deletions hax-lib-macros/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -382,6 +382,27 @@ pub fn ensures(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream
.into()
}

/// Exclude this item from the Hax translation.
#[proc_macro_error]
#[proc_macro_attribute]
pub fn interface(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
let item: ItemFn = parse_macro_input!(item);
let ItemFn {
// The function signature
sig,
// The visibility specifier of this function
vis,
// The function block or body
block,
// Other attributes applied to this function
attrs,
} = item.clone();

quote! {
#(#attrs)* #vis #sig { todo!() }
}.into()
}

mod kw {
syn::custom_keyword!(hax_lib);
syn::custom_keyword!(decreases);
Expand Down
2 changes: 1 addition & 1 deletion hax-lib/src/proc_macros.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
//! proc-macro crate cannot export anything but procedural macros.
pub use hax_lib_macros::{
attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type,
attributes, ensures, exclude, impl_fn_decoration, include, interface, lemma, loop_invariant, opaque_type,
refinement_type, requires, trait_fn_decoration,
};

Expand Down

0 comments on commit 2c468ca

Please sign in to comment.