Skip to content

Commit

Permalink
Complete redesign of concrete identifiers
Browse files Browse the repository at this point in the history
  • Loading branch information
@W95Psp
W95Psp committed Jan 15, 2025
1 parent db2b445 commit f21a709
Show file tree
Hide file tree
Showing 44 changed files with 1,928 additions and 1,166 deletions.
16 changes: 9 additions & 7 deletions engine/backends/coq/coq/coq_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,8 @@ module AST = Ast.Make (InputLanguage)
module BackendOptions = Backend.UnitBackendOptions
open Ast
module CoqNamePolicy = Concrete_ident.DefaultNamePolicy
module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy)
module U = Ast_utils.Make (InputLanguage)
module RenderId = Concrete_ident.MakeRenderAPI (CoqNamePolicy)
open AST

let hardcoded_coq_headers =
Expand Down Expand Up @@ -492,7 +493,7 @@ struct
let crate =
String.capitalize
(Option.value ~default:"(TODO CRATE)"
(Option.map ~f:fst current_namespace))
(Option.bind ~f:List.hd current_namespace))
in
let concat_capitalize l =
String.concat ~sep:"_" (List.map ~f:String.capitalize l)
Expand All @@ -509,7 +510,7 @@ struct
(crate
:: List.drop_last_exn
(Option.value ~default:[]
(Option.map ~f:snd current_namespace))
(Option.bind ~f:List.tl current_namespace))
@ xs)
| [ a ] -> a
| xs -> concat_capitalize_include xs
Expand Down Expand Up @@ -729,7 +730,7 @@ struct

method concrete_ident ~local:_ id : document =
string
(match id.definition with
(match id.name with
| "not" -> "negb"
| "eq" -> "t_PartialEq_f_eq"
| "lt" -> "t_PartialOrd_f_lt"
Expand Down Expand Up @@ -765,12 +766,13 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list =
let my_printer = make m in
U.group_items_by_namespace items
|> Map.to_alist
|> List.filter_map ~f:(fun (_, items) ->
let* first_item = List.hd items in
Some ((RenderId.render first_item.ident).path, items))
|> List.map ~f:(fun (ns, items) ->
let mod_name =
String.concat ~sep:"_"
(List.map
~f:(map_first_letter String.uppercase)
(fst ns :: snd ns))
(List.map ~f:(map_first_letter String.uppercase) ns)
in
let sourcemap, contents =
let annotated = my_printer#entrypoint_modul items in
Expand Down
30 changes: 15 additions & 15 deletions engine/backends/coq/ssprove/ssprove_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,8 @@ module AST = Ast.Make (InputLanguage)
module BackendOptions = Backend.UnitBackendOptions
open Ast
module CoqNamePolicy = Concrete_ident.DefaultNamePolicy
module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy)
module U = Ast_utils.Make (InputLanguage)
module RenderId = Concrete_ident.MakeRenderAPI (CoqNamePolicy)
open AST

module SSProveLibrary : Library = struct
Expand Down Expand Up @@ -553,7 +554,7 @@ end

module Context = struct
type t = {
current_namespace : string * string list;
current_namespace : string list;
analysis_data : StaticAnalysis.analysis_data;
}
end
Expand Down Expand Up @@ -617,10 +618,10 @@ module TransformToInputLanguage (* : PHASE *) =
(* | None -> Error.unimplemented ~details:err span *)

let pconcrete_ident (id : Ast.concrete_ident) : string =
U.Concrete_ident_view.to_definition_name id
(RenderId.render id).name

let plocal_ident (e : Local_ident.t) : string =
U.Concrete_ident_view.local_ident
RenderId.local_ident
(match String.chop_prefix ~prefix:"impl " e.name with
| Some name ->
let name = "impl_" ^ Int.to_string ([%hash: string] name) in
Expand Down Expand Up @@ -689,7 +690,7 @@ struct
| Bool b -> SSP.AST.Const_bool b

let operators =
let c = Ast.Global_ident.of_name Value in
let c = Ast.Global_ident.of_name ~value:true in
[
(c Rust_primitives__hax__array_of_list, (3, [ ""; ".a["; "]<-"; "" ]));
(c Core__ops__index__Index__index, (2, [ ""; ".a["; "]" ]));
Expand Down Expand Up @@ -1555,8 +1556,8 @@ struct
let id = [%show: concrete_ident] macro in
Error.raise { kind = UnsupportedMacro { id }; span = e.span }
in
match U.Concrete_ident_view.to_view macro with
| { crate = "hacspec_lib"; path = _; definition = name } -> (
match RenderId.render macro with
| { path = "hacspec_lib" :: _; name } -> (
match name with
| "public_nat_mod" ->
let open Hacspeclib_macro_parser in
Expand Down Expand Up @@ -1712,7 +1713,7 @@ struct
| _ -> unsupported ())
| _ -> unsupported ())
| Use { path; is_external; rename } ->
let _ns_crate, _ns_path = ctx.current_namespace in
let _ns_path = ctx.current_namespace in
if is_external then []
else
[ SSP.AST.Require (None, (* ns_crate:: ns_path @ *) path, rename) ]
Expand Down Expand Up @@ -1988,10 +1989,7 @@ let print_item (analysis_data : StaticAnalysis.analysis_data) (item : AST.item)
: SSP.AST.decl list =
let (module Print) =
make
{
current_namespace = U.Concrete_ident_view.to_namespace item.ident;
analysis_data;
}
{ current_namespace = (RenderId.render item.ident).path; analysis_data }
in
Print.pitem item

Expand Down Expand Up @@ -2421,12 +2419,14 @@ let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list)
let analysis_data = StaticAnalysis.analyse items in
U.group_items_by_namespace items
|> Map.to_alist
|> List.filter_map
~f:
(snd >> List.hd
>> Option.map ~f:(fun i -> ((RenderId.render i.ident).path, items)))
|> List.map ~f:(fun (ns, items) ->
let mod_name =
String.concat ~sep:"_"
(List.map
~f:(map_first_letter String.uppercase)
(fst ns :: snd ns))
(List.map ~f:(map_first_letter String.uppercase) ns)
in
let file_content =
hardcoded_coq_headers ^ "\n"
Expand Down
18 changes: 8 additions & 10 deletions engine/backends/easycrypt/easycrypt_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ include
module BackendOptions = Backend.UnitBackendOptions
module AST = Ast.Make (InputLanguage)
module ECNamePolicy = Concrete_ident.DefaultNamePolicy
module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (ECNamePolicy)
module U = Ast_utils.Make (InputLanguage)
module RenderId = Concrete_ident.MakeRenderAPI (ECNamePolicy)
open AST

module RejectNotEC (FA : Features.T) = struct
Expand Down Expand Up @@ -88,14 +89,11 @@ module NM = struct

{ the with subnms = Map.Poly.update ~f:update the.subnms name }

let push_using_namespace (the : nmtree) (nm : string * string list)
(item : AST.item) =
push_using_longname the (List.rev (fst nm :: snd nm)) item
let push_using_namespace (the : nmtree) (nm : string list) (item : AST.item) =
push_using_longname the (List.rev nm) item

let push (the : nmtree) (item : AST.item) =
push_using_namespace the
(U.Concrete_ident_view.to_namespace item.ident)
item
push_using_namespace the (RenderId.render item.ident).path item
end

let suffix_of_size (size : Ast.size) =
Expand Down Expand Up @@ -132,7 +130,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
match item.v with
| Fn { name; generics; body; params }
when List.is_empty generics.params ->
let name = U.Concrete_ident_view.to_definition_name name in
let name = (RenderId.render name).name in

doit_fn fmt (name, params, body)
| Fn _ -> assert false
Expand Down Expand Up @@ -166,7 +164,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
pp_param)
params doit_stmt body
and doit_concrete_ident (fmt : Formatter.t) (p : Concrete_ident.t) =
Stdlib.Format.fprintf fmt "%s" (U.Concrete_ident_view.to_definition_name p)
Stdlib.Format.fprintf fmt "%s" (RenderId.render p).name
and doit_type (fmt : Formatter.t) (typ : ty) =
match typ with
| TBool -> assert false
Expand Down Expand Up @@ -281,7 +279,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
|| eq_name Core__cmp__PartialEq__ne op
|| eq_name Core__cmp__PartialEq__eq op) ->
Stdlib.Format.fprintf fmt "(%a) %s (%a)" doit_expr e1
(match U.Concrete_ident_view.to_definition_name op with
(match (RenderId.render op).name with
| "bitxor" -> "^"
| "bitand" -> "&"
| "bitor" -> "|"
Expand Down
Loading

0 comments on commit f21a709

Please sign in to comment.