From 0a258c03bc49b4d3d89b3ce0f73b1c57e38f4eeb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 12 Apr 2024 16:47:40 +0200 Subject: Start adding integer functions to the Lean library --- backends/lean/Base/Primitives.lean | 2 +- backends/lean/Base/Primitives/Core.lean | 43 +++++ backends/lean/Base/Primitives/CoreOps.lean | 35 ---- backends/lean/Base/Primitives/Scalar.lean | 255 +++++++++++++++++++++++++++++ compiler/Extract.ml | 13 +- compiler/ExtractBuiltin.ml | 189 +++++++++++++++------ compiler/ExtractTypes.ml | 15 +- compiler/TranslateCore.ml | 19 +++ 8 files changed, 480 insertions(+), 91 deletions(-) create mode 100644 backends/lean/Base/Primitives/Core.lean delete mode 100644 backends/lean/Base/Primitives/CoreOps.lean diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index 7196d2ec..ad8f2501 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -4,4 +4,4 @@ import Base.Primitives.Scalar import Base.Primitives.ArraySlice import Base.Primitives.Vec import Base.Primitives.Alloc -import Base.Primitives.CoreOps +import Base.Primitives.Core diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean new file mode 100644 index 00000000..f67da7d7 --- /dev/null +++ b/backends/lean/Base/Primitives/Core.lean @@ -0,0 +1,43 @@ +import Lean +import Base.Primitives.Base + +open Primitives +open Result + +namespace core + +/- Trait declaration: [core::convert::From] -/ +structure convert.From (Self T : Type) where + from_ : T → Result Self + +namespace ops -- core.ops + +namespace index -- core.ops.index + +/- Trait declaration: [core::ops::index::Index] -/ +structure Index (Self Idx : Type) where + Output : Type + index : Self → Idx → Result Output + +/- Trait declaration: [core::ops::index::IndexMut] -/ +structure IndexMut (Self Idx : Type) where + indexInst : Index Self Idx + index_mut : Self → Idx → Result (indexInst.Output × (indexInst.Output → Result Self)) + +end index -- core.ops.index + +namespace deref -- core.ops.deref + +structure Deref (Self : Type) where + Target : Type + deref : Self → Result Target + +structure DerefMut (Self : Type) where + derefInst : Deref Self + deref_mut : Self → Result (derefInst.Target × (Self → Result Self)) + +end deref -- core.ops.deref + +end ops -- core.ops + +end core diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/CoreOps.lean deleted file mode 100644 index 1736bfa6..00000000 --- a/backends/lean/Base/Primitives/CoreOps.lean +++ /dev/null @@ -1,35 +0,0 @@ -import Lean -import Base.Primitives.Base - -open Primitives -open Result - -namespace core.ops - -namespace index -- core.ops.index - -/- Trait declaration: [core::ops::index::Index] -/ -structure Index (Self Idx : Type) where - Output : Type - index : Self → Idx → Result Output - -/- Trait declaration: [core::ops::index::IndexMut] -/ -structure IndexMut (Self Idx : Type) where - indexInst : Index Self Idx - index_mut : Self → Idx → Result (indexInst.Output × (indexInst.Output → Result Self)) - -end index -- core.ops.index - -namespace deref -- core.ops.deref - -structure Deref (Self : Type) where - Target : Type - deref : Self → Result Target - -structure DerefMut (Self : Type) where - derefInst : Deref Self - deref_mut : Self → Result (derefInst.Target × (Self → Result Self)) - -end deref -- core.ops.deref - -end core.ops diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 8de2b3f2..0ba538b7 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -2,6 +2,7 @@ import Lean import Lean.Meta.Tactic.Simp import Mathlib.Tactic.Linarith import Base.Primitives.Base +import Base.Primitives.Core import Base.Diverge.Base import Base.Progress.Base import Base.Arith.Int @@ -1393,4 +1394,258 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) := @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by simp [eq_equiv] +-- Conversions +def core.convert.num.FromUsizeBool.from (b : Bool) : Usize := + if b then 1#usize else 0#usize + +def core.convert.num.FromU8Bool.from (b : Bool) : U8 := + if b then 1#u8 else 0#u8 + +def core.convert.num.FromU16Bool.from (b : Bool) : U16 := + if b then 1#u16 else 0#u16 + +def core.convert.num.FromU32Bool.from (b : Bool) : U32 := + if b then 1#u32 else 0#u32 + +def core.convert.num.FromU64Bool.from (b : Bool) : U64 := + if b then 1#u64 else 0#u64 + +def core.convert.num.FromU128Bool.from (b : Bool) : U128 := + if b then 1#u128 else 0#u128 + +def core.convert.num.FromIsizeBool.from (b : Bool) : Isize := + if b then 1#isize else 0#isize + +def core.convert.num.FromI8Bool.from (b : Bool) : I8 := + if b then 1#i8 else 0#i8 + +def core.convert.num.FromI16Bool.from (b : Bool) : I16 := + if b then 1#i16 else 0#i16 + +def core.convert.num.FromI32Bool.from (b : Bool) : I32 := + if b then 1#i32 else 0#i32 + +def core.convert.num.FromI64Bool.from (b : Bool) : I64 := + if b then 1#i64 else 0#i64 + +def core.convert.num.FromI128Bool.from (b : Bool) : I128 := + if b then 1#i128 else 0#i128 + +def core.convert.num.FromUsizeU8.from (x : U8) : Usize := sorry +def core.convert.num.FromUsizeU16.from (x : U16) : Usize := sorry +def core.convert.num.FromUsizeU32.from (x : U32) : Usize := sorry +def core.convert.num.FromUsizeUsize.from (x : Usize) : Usize := sorry + +def core.convert.num.FromU8U8.from (x : U8) : U8 := sorry + +def core.convert.num.FromU16U8.from (x : U8) : U16 := sorry +def core.convert.num.FromU16U16.from (x : U16) : U16 := sorry + +def core.convert.num.FromU32U8.from (x : U8) : U32 := sorry +def core.convert.num.FromU32U16.from (x : U16) : U32 := sorry +def core.convert.num.FromU32U32.from (x : U32) : U32 := sorry + +def core.convert.num.FromU64U8.from (x : U8) : U64 := sorry +def core.convert.num.FromU64U16.from (x : U16) : U64 := sorry +def core.convert.num.FromU64U32.from (x : U32) : U64 := sorry +def core.convert.num.FromU64U64.from (x : U64) : U64 := sorry + +def core.convert.num.FromU128U8.from (x : U8) : U128 := sorry +def core.convert.num.FromU128U16.from (x : U16) : U128 := sorry +def core.convert.num.FromU128U32.from (x : U32) : U128 := sorry +def core.convert.num.FromU128U64.from (x : U64) : U128 := sorry +def core.convert.num.FromU128U128.from (x : U128) : U128 := sorry + +def core.convert.num.FromIsizeI8.from (x : I8) : Isize := sorry +def core.convert.num.FromIsizeI16.from (x : I16) : Isize := sorry +def core.convert.num.FromIsizeI32.from (x : I32) : Isize := sorry +def core.convert.num.FromIsizeIsize.from (x : Isize) : Isize := sorry + +def core.convert.num.FromI8I8.from (x : I8) : I8 := sorry + +def core.convert.num.FromI16I8.from (x : I8) : I16 := sorry +def core.convert.num.FromI16I16.from (x : I16) : I16 := sorry + +def core.convert.num.FromI32I8.from (x : I8) : I32 := sorry +def core.convert.num.FromI32I16.from (x : I16) : I32 := sorry +def core.convert.num.FromI32I32.from (x : I32) : I32 := sorry + +def core.convert.num.FromI64I8.from (x : I8) : I64 := sorry +def core.convert.num.FromI64I16.from (x : I16) : I64 := sorry +def core.convert.num.FromI64I32.from (x : I32) : I64 := sorry +def core.convert.num.FromI64I64.from (x : I64) : I64 := sorry + +def core.convert.num.FromI128I8.from (x : I8) : I128 := sorry +def core.convert.num.FromI128I16.from (x : I16) : I128 := sorry +def core.convert.num.FromI128I32.from (x : I32) : I128 := sorry +def core.convert.num.FromI128I64.from (x : I64) : I128 := sorry +def core.convert.num.FromI128I128.from (x : I128) : I128 := sorry + +def core.convert.FromUsizeU8 : core.convert.From Usize U8 := { + from_ := fun x => ok (core.convert.num.FromUsizeU8.from x) +} + +def core.convert.FromUsizeU16 : core.convert.From Usize U16 := { + from_ := fun x => ok (core.convert.num.FromUsizeU16.from x) +} + +def core.convert.FromUsizeU32 : core.convert.From Usize U32 := { + from_ := fun x => ok (core.convert.num.FromUsizeU32.from x) +} + +def core.convert.FromUsizeUsize : core.convert.From Usize Usize := { + from_ := fun x => ok (core.convert.num.FromUsizeUsize.from x) +} + +def core.convert.FromU8U8 : core.convert.From U8 U8 := { + from_ := fun x => ok (core.convert.num.FromU8U8.from x) +} + +def core.convert.FromU16U8 : core.convert.From U16 U8 := { + from_ := fun x => ok (core.convert.num.FromU16U8.from x) +} + +def core.convert.FromU16U16 : core.convert.From U16 U16 := { + from_ := fun x => ok (core.convert.num.FromU16U16.from x) +} + +def core.convert.FromU32U8 : core.convert.From U32 U8 := { + from_ := fun x => ok (core.convert.num.FromU32U8.from x) +} + +def core.convert.FromU32U16 : core.convert.From U32 U16 := { + from_ := fun x => ok (core.convert.num.FromU32U16.from x) +} + +def core.convert.FromU32U32 : core.convert.From U32 U32 := { + from_ := fun x => ok (core.convert.num.FromU32U32.from x) +} + +def core.convert.FromU64U8 : core.convert.From U64 U8 := { + from_ := fun x => ok (core.convert.num.FromU64U8.from x) +} + +def core.convert.FromU64U16 : core.convert.From U64 U16 := { + from_ := fun x => ok (core.convert.num.FromU64U16.from x) +} + +def core.convert.FromU64U32 : core.convert.From U64 U32 := { + from_ := fun x => ok (core.convert.num.FromU64U32.from x) +} + +def core.convert.FromU64U64 : core.convert.From U64 U64 := { + from_ := fun x => ok (core.convert.num.FromU64U64.from x) +} + +def core.convert.FromU128U8 : core.convert.From U128 U8 := { + from_ := fun x => ok (core.convert.num.FromU128U8.from x) +} + +def core.convert.FromU128U16 : core.convert.From U128 U16 := { + from_ := fun x => ok (core.convert.num.FromU128U16.from x) +} + +def core.convert.FromU128U32 : core.convert.From U128 U32 := { + from_ := fun x => ok (core.convert.num.FromU128U32.from x) +} + +def core.convert.FromU128U64 : core.convert.From U128 U64 := { + from_ := fun x => ok (core.convert.num.FromU128U64.from x) +} + +def core.convert.FromU128U128 : core.convert.From U128 U128 := { + from_ := fun x => ok (core.convert.num.FromU128U128.from x) +} + +def core.convert.FromIsizeI8 : core.convert.From Isize I8 := { + from_ := fun x => ok (core.convert.num.FromIsizeI8.from x) +} + +def core.convert.FromIsizeI16 : core.convert.From Isize I16 := { + from_ := fun x => ok (core.convert.num.FromIsizeI16.from x) +} + +def core.convert.FromIsizeI32 : core.convert.From Isize I32 := { + from_ := fun x => ok (core.convert.num.FromIsizeI32.from x) +} + +def core.convert.FromIsizeIsize : core.convert.From Isize Isize := { + from_ := fun x => ok (core.convert.num.FromIsizeIsize.from x) +} + +def core.convert.FromI8I8 : core.convert.From I8 I8 := { + from_ := fun x => ok (core.convert.num.FromI8I8.from x) +} + +def core.convert.FromI16I8 : core.convert.From I16 I8 := { + from_ := fun x => ok (core.convert.num.FromI16I8.from x) +} + +def core.convert.FromI16I16 : core.convert.From I16 I16 := { + from_ := fun x => ok (core.convert.num.FromI16I16.from x) +} + +def core.convert.FromI32I8 : core.convert.From I32 I8 := { + from_ := fun x => ok (core.convert.num.FromI32I8.from x) +} + +def core.convert.FromI32I16 : core.convert.From I32 I16 := { + from_ := fun x => ok (core.convert.num.FromI32I16.from x) +} + +def core.convert.FromI32I32 : core.convert.From I32 I32 := { + from_ := fun x => ok (core.convert.num.FromI32I32.from x) +} + +def core.convert.FromI64I8 : core.convert.From I64 I8 := { + from_ := fun x => ok (core.convert.num.FromI64I8.from x) +} + +def core.convert.FromI64I16 : core.convert.From I64 I16 := { + from_ := fun x => ok (core.convert.num.FromI64I16.from x) +} + +def core.convert.FromI64I32 : core.convert.From I64 I32 := { + from_ := fun x => ok (core.convert.num.FromI64I32.from x) +} + +def core.convert.FromI64I64 : core.convert.From I64 I64 := { + from_ := fun x => ok (core.convert.num.FromI64I64.from x) +} + +def core.convert.FromI128I8 : core.convert.From I128 I8 := { + from_ := fun x => ok (core.convert.num.FromI128I8.from x) +} + +def core.convert.FromI128I16 : core.convert.From I128 I16 := { + from_ := fun x => ok (core.convert.num.FromI128I16.from x) +} + +def core.convert.FromI128I32 : core.convert.From I128 I32 := { + from_ := fun x => ok (core.convert.num.FromI128I32.from x) +} + +def core.convert.FromI128I64 : core.convert.From I128 I64 := { + from_ := fun x => ok (core.convert.num.FromI128I64.from x) +} + +def core.convert.FromI128I128 : core.convert.From I128 I128 := { + from_ := fun x => ok (core.convert.num.FromI128I128.from x) +} + +-- Leading zeros +def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry +def core.num.U8.leading_zeros (x : U8) : U32 := sorry +def core.num.U16.leading_zeros (x : U16) : U32 := sorry +def core.num.U32.leading_zeros (x : U32) : U32 := sorry +def core.num.U64.leading_zeros (x : U64) : U32 := sorry +def core.num.U128.leading_zeros (x : U128) : U32 := sorry + +def core.num.Isize.leading_zeros (x : Isize) : U32 := sorry +def core.num.I8.leading_zeros (x : I8) : U32 := sorry +def core.num.I16.leading_zeros (x : I16) : U32 := sorry +def core.num.I32.leading_zeros (x : I32) : U32 := sorry +def core.num.I64.leading_zeros (x : I64) : U32 := sorry +def core.num.I128.leading_zeros (x : I128) : U32 := sorry + end Primitives diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 6eeef772..8efb59fb 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2644,14 +2644,19 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - (let name = + (let name, generics = if !Config.extract_external_name_patterns && not impl.is_local then - Some impl.llbc_name - else None + let decl_id = impl.impl_trait.trait_decl_id in + let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in + let decl_ref = impl.llbc_impl_trait in + ( Some trait_decl.llbc_name, + Some (trait_decl.llbc_generics, decl_ref.decl_generics) ) + else (None, None) in extract_comment_with_span ctx fmt [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ] - name impl.meta.span); + (* TODO: why option option for the generics? Looks like a bug in OCaml!? *) + name ?generics:(Some generics) impl.meta.span); F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 3ba8d11d..ac7a4a24 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -10,6 +10,22 @@ include ExtractName (* TODO: only open? *) let log = Logging.builtin_log +let all_int_names = + [ + "usize"; + "u8"; + "u16"; + "u32"; + "u64"; + "u128"; + "isize"; + "i8"; + "i16"; + "i32"; + "i64"; + "i128"; + ] + (** Small utility to memoize some computations *) let mk_memoized (f : unit -> 'a) : unit -> 'a = let r = ref None in @@ -215,6 +231,28 @@ let builtin_types_map = mk_memoized mk_builtin_types_map type builtin_fun_info = { extract_name : string } [@@deriving show] +let int_and_smaller_list : (string * string) list = + let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in + let int_names = List.rev [ "i8"; "i16"; "i32"; "i64"; "i128" ] in + let rec compute_pairs l = + match l with + | [] -> [] + | x :: l -> List.map (fun y -> (x, y)) (x :: l) @ compute_pairs l + in + [ + (* Usize *) + ("usize", "u8"); + ("usize", "u16"); + ("usize", "u32"); + ("usize", "usize"); + (* Isize *) + ("isize", "i8"); + ("isize", "i16"); + ("isize", "i32"); + ("isize", "isize"); + ] + @ compute_pairs uint_names @ compute_pairs int_names + (** The assumed functions. The optional list of booleans is filtering information for the type @@ -245,20 +283,7 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = (pattern * bool list option * builtin_fun_info) list = List.map (fun ty -> mk_fun (rust_name ty) (Some (extract_name ty)) None) - [ - "usize"; - "u8"; - "u16"; - "u32"; - "u64"; - "u128"; - "isize"; - "i8"; - "i16"; - "i32"; - "i64"; - "i128"; - ] + all_int_names in [ mk_fun "core::mem::replace" None None; @@ -353,6 +378,32 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = (fun ty -> StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op)) [ "add"; "sub"; "mul"; "div"; "rem" ]) + (* From *) + @ mk_scalar_fun + (fun ty -> + "core::convert::num::{core::convert::From<" ^ ty ^ ", bool>}::from") + (fun ty -> + "core.convert.num.From" + ^ StringUtils.capitalize_first_letter ty + ^ "Bool.from") + (* From *) + @ List.map + (fun (big, small) -> + mk_fun + ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small + ^ ">}::from") + (Some + ("core.convert.num.From" + ^ StringUtils.capitalize_first_letter big + ^ StringUtils.capitalize_first_letter small + ^ ".from")) + None) + int_and_smaller_list + (* Leading zeros *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") + (fun ty -> + "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros") let mk_builtin_funs_map () = let m = @@ -370,36 +421,44 @@ let builtin_funs_map = mk_memoized mk_builtin_funs_map type effect_info = { can_fail : bool; stateful : bool } let builtin_fun_effects = - let int_names = - [ - "usize"; - "u8"; - "u16"; - "u32"; - "u64"; - "u128"; - "isize"; - "i8"; - "i16"; - "i32"; - "i64"; - "i128"; - ] - in let int_ops = [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ] in let int_funs = List.map (fun int_name -> + List.map (fun op -> "core::num::" ^ "{" ^ int_name ^ "}::" ^ op) int_ops) + all_int_names + @ List.map + (fun op -> + List.map + (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op) + all_int_names) + [ "add"; "sub"; "mul"; "div"; "rem" ] + (* From *) + @ [ + List.map + (fun int_name -> + "core::convert::num::{core::convert::From<" ^ int_name + ^ ", bool>}::from") + all_int_names; + ] + (* From *) + @ [ + List.map + (fun (big, small) -> + "core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small + ^ ">}::from") + int_and_smaller_list; + ] + (* Leading zeros *) + @ [ List.map - (fun op -> - "core::num::" ^ "{" - ^ StringUtils.capitalize_first_letter int_name - ^ "}::" ^ op) - int_ops) - int_names + (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") + all_int_names; + ] in + let int_funs = List.concat int_funs in let no_fail_no_state_funs = [ @@ -454,7 +513,9 @@ type builtin_trait_decl_info = { let builtin_trait_decls_info () = let mk_trait (rust_name : string) ?(extract_name : string option = None) ?(parent_clauses : string list = []) ?(types : string list = []) - ?(methods : string list = []) () : builtin_trait_decl_info = + ?(methods : string list = []) + ?(methods_with_extract : (string * string) list option = None) () : + builtin_trait_decl_info = let rust_name = parse_pattern rust_name in let extract_name = match extract_name with @@ -482,16 +543,22 @@ let builtin_trait_decls_info () = List.map mk_type types in let methods = - let mk_method item_name = - (* TODO: factor out with builtin_funs_info *) - let basename = - if !record_fields_short_names then item_name - else extract_name ^ "_" ^ item_name - in - let fwd = { extract_name = basename } in - (item_name, fwd) - in - List.map mk_method methods + match methods_with_extract with + | None -> + let mk_method item_name = + (* TODO: factor out with builtin_funs_info *) + let basename = + if !record_fields_short_names then item_name + else extract_name ^ "_" ^ item_name + in + let fwd = { extract_name = basename } in + (item_name, fwd) + in + List.map mk_method methods + | Some methods -> + List.map + (fun (item_name, extract_name) -> (item_name, { extract_name })) + methods in { rust_name; @@ -531,6 +598,10 @@ let builtin_trait_decls_info () = "index_mut"; ] (); + (* From *) + mk_trait "core::convert::From" + ~methods_with_extract:(Some [ ("from", "from_") ]) + (); ] let mk_builtin_trait_decls_map () = @@ -602,6 +673,30 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = ~filter:(Some [ true; true; false ]) (); ] + (* From *) + @ List.map + (fun ty -> + fmt + ("core::convert::From<" ^ ty ^ ", bool>") + ~extract_name: + (Some + ("core.convert.From" + ^ StringUtils.capitalize_first_letter ty + ^ "Bool")) + ()) + all_int_names + (* From *) + @ List.map + (fun (big, small) -> + fmt + ("core::convert::From<" ^ big ^ ", " ^ small ^ ">") + ~extract_name: + (Some + ("core.convert.From" + ^ StringUtils.capitalize_first_letter big + ^ StringUtils.capitalize_first_letter small)) + ()) + int_and_smaller_list let mk_builtin_trait_impls_map () = let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 1c3657a3..c2eb8da0 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1141,7 +1141,9 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit = F.pp_close_box fmt () let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter) - (sl : string list) (name : Types.name option) (span : Meta.span) : unit = + (sl : string list) (name : Types.name option) + ?(generics : (Types.generic_params * Types.generic_args) option = None) + (span : Meta.span) : unit = let file = match span.file with Virtual s | Local s -> s in let loc_to_string (l : Meta.loc) : string = string_of_int l.line ^ ":" ^ string_of_int l.col @@ -1151,10 +1153,15 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter) ^ loc_to_string span.end_loc in let name = - match name with - | None -> [] - | Some name -> + match (name, generics) with + | None, _ -> [] + | Some name, None -> [ "Name pattern: " ^ name_to_pattern_string ctx.trans_ctx name ] + | Some name, Some (params, args) -> + [ + "Name pattern: " + ^ name_with_generics_to_pattern_string ctx.trans_ctx name params args; + ] in extract_comment fmt (sl @ [ span ] @ name) diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index 3e4c7375..688cbe34 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -91,3 +91,22 @@ let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string = in let pat = Charon.NameMatcher.name_to_pattern mctx c n in Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat + +let name_with_generics_to_pattern_string (ctx : trans_ctx) (n : Types.name) + (params : Types.generic_params) (args : Types.generic_args) : string = + let mctx : Charon.NameMatcher.ctx = + { + type_decls = ctx.type_ctx.type_decls; + global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; + trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; + } + in + let c : Charon.NameMatcher.to_pat_config = + { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs } + in + let pat = + Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args + in + Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat -- cgit v1.2.3 From 386311bc3077d9118ca363cf9dc5c91cb77a2e6d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 12 Apr 2024 16:57:42 +0200 Subject: Reorganize the files in the Lean backend a bit --- backends/lean/Base/Primitives.lean | 1 + backends/lean/Base/Primitives/Alloc.lean | 2 +- backends/lean/Base/Primitives/ArraySlice.lean | 2 +- backends/lean/Base/Primitives/CoreConvertNum.lean | 263 ++++++++++++++++++++++ backends/lean/Base/Primitives/Scalar.lean | 239 -------------------- 5 files changed, 266 insertions(+), 241 deletions(-) create mode 100644 backends/lean/Base/Primitives/CoreConvertNum.lean diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index ad8f2501..f80c2004 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -5,3 +5,4 @@ import Base.Primitives.ArraySlice import Base.Primitives.Vec import Base.Primitives.Alloc import Base.Primitives.Core +import Base.Primitives.CoreConvertNum diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean index 15fe1ff9..1b15d36d 100644 --- a/backends/lean/Base/Primitives/Alloc.lean +++ b/backends/lean/Base/Primitives/Alloc.lean @@ -1,6 +1,6 @@ import Lean import Base.Primitives.Base -import Base.Primitives.CoreOps +import Base.Primitives.Core open Primitives open Result diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index 91ca7284..157f9df1 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -6,7 +6,7 @@ import Mathlib.Tactic.Linarith import Base.IList import Base.Primitives.Scalar import Base.Primitives.Range -import Base.Primitives.CoreOps +import Base.Primitives.Core import Base.Arith import Base.Progress.Base diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean new file mode 100644 index 00000000..d76fba37 --- /dev/null +++ b/backends/lean/Base/Primitives/CoreConvertNum.lean @@ -0,0 +1,263 @@ +import Lean +import Lean.Meta.Tactic.Simp +import Init.Data.List.Basic +import Mathlib.Tactic.Linarith +import Base.IList +import Base.Primitives.Scalar +import Base.Primitives.ArraySlice +import Base.Arith +import Base.Progress.Base + +namespace Primitives + +open Result Error + +namespace core.convert + +namespace num -- core.convert.num + +-- Conversions +def FromUsizeBool.from (b : Bool) : Usize := + if b then 1#usize else 0#usize + +def FromU8Bool.from (b : Bool) : U8 := + if b then 1#u8 else 0#u8 + +def FromU16Bool.from (b : Bool) : U16 := + if b then 1#u16 else 0#u16 + +def FromU32Bool.from (b : Bool) : U32 := + if b then 1#u32 else 0#u32 + +def FromU64Bool.from (b : Bool) : U64 := + if b then 1#u64 else 0#u64 + +def FromU128Bool.from (b : Bool) : U128 := + if b then 1#u128 else 0#u128 + +def FromIsizeBool.from (b : Bool) : Isize := + if b then 1#isize else 0#isize + +def FromI8Bool.from (b : Bool) : I8 := + if b then 1#i8 else 0#i8 + +def FromI16Bool.from (b : Bool) : I16 := + if b then 1#i16 else 0#i16 + +def FromI32Bool.from (b : Bool) : I32 := + if b then 1#i32 else 0#i32 + +def FromI64Bool.from (b : Bool) : I64 := + if b then 1#i64 else 0#i64 + +def FromI128Bool.from (b : Bool) : I128 := + if b then 1#i128 else 0#i128 + +def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromUsizeU16.from (x : U16) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromUsizeU32.from (x : U32) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromUsizeUsize.from (x : Usize) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU8U8.from (x : U8) : U8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU16U8.from (x : U8) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU16U16.from (x : U16) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU32U8.from (x : U8) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU32U16.from (x : U16) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU32U32.from (x : U32) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU64U8.from (x : U8) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU64U16.from (x : U16) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU64U32.from (x : U32) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU64U64.from (x : U64) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU128U8.from (x : U8) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U16.from (x : U16) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U32.from (x : U32) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U64.from (x : U64) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U128.from (x : U128) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromIsizeI8.from (x : I8) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromIsizeI16.from (x : I16) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromIsizeI32.from (x : I32) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromIsizeIsize.from (x : Isize) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI8I8.from (x : I8) : I8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI16I8.from (x : I8) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI16I16.from (x : I16) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI32I8.from (x : I8) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI32I16.from (x : I16) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI32I32.from (x : I32) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI64I8.from (x : I8) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI64I16.from (x : I16) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI64I32.from (x : I32) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI64I64.from (x : I64) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI128I8.from (x : I8) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I16.from (x : I16) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I32.from (x : I32) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I64.from (x : I64) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I128.from (x : I128) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +end num -- core.convert.num + +def FromUsizeU8 : core.convert.From Usize U8 := { + from_ := fun x => ok (num.FromUsizeU8.from x) +} + +def FromUsizeU16 : core.convert.From Usize U16 := { + from_ := fun x => ok (num.FromUsizeU16.from x) +} + +def FromUsizeU32 : core.convert.From Usize U32 := { + from_ := fun x => ok (num.FromUsizeU32.from x) +} + +def FromUsizeUsize : core.convert.From Usize Usize := { + from_ := fun x => ok (num.FromUsizeUsize.from x) +} + +def FromU8U8 : core.convert.From U8 U8 := { + from_ := fun x => ok (num.FromU8U8.from x) +} + +def FromU16U8 : core.convert.From U16 U8 := { + from_ := fun x => ok (num.FromU16U8.from x) +} + +def FromU16U16 : core.convert.From U16 U16 := { + from_ := fun x => ok (num.FromU16U16.from x) +} + +def FromU32U8 : core.convert.From U32 U8 := { + from_ := fun x => ok (num.FromU32U8.from x) +} + +def FromU32U16 : core.convert.From U32 U16 := { + from_ := fun x => ok (num.FromU32U16.from x) +} + +def FromU32U32 : core.convert.From U32 U32 := { + from_ := fun x => ok (num.FromU32U32.from x) +} + +def FromU64U8 : core.convert.From U64 U8 := { + from_ := fun x => ok (num.FromU64U8.from x) +} + +def FromU64U16 : core.convert.From U64 U16 := { + from_ := fun x => ok (num.FromU64U16.from x) +} + +def FromU64U32 : core.convert.From U64 U32 := { + from_ := fun x => ok (num.FromU64U32.from x) +} + +def FromU64U64 : core.convert.From U64 U64 := { + from_ := fun x => ok (num.FromU64U64.from x) +} + +def FromU128U8 : core.convert.From U128 U8 := { + from_ := fun x => ok (num.FromU128U8.from x) +} + +def FromU128U16 : core.convert.From U128 U16 := { + from_ := fun x => ok (num.FromU128U16.from x) +} + +def FromU128U32 : core.convert.From U128 U32 := { + from_ := fun x => ok (num.FromU128U32.from x) +} + +def FromU128U64 : core.convert.From U128 U64 := { + from_ := fun x => ok (num.FromU128U64.from x) +} + +def FromU128U128 : core.convert.From U128 U128 := { + from_ := fun x => ok (num.FromU128U128.from x) +} + +def FromIsizeI8 : core.convert.From Isize I8 := { + from_ := fun x => ok (num.FromIsizeI8.from x) +} + +def FromIsizeI16 : core.convert.From Isize I16 := { + from_ := fun x => ok (num.FromIsizeI16.from x) +} + +def FromIsizeI32 : core.convert.From Isize I32 := { + from_ := fun x => ok (num.FromIsizeI32.from x) +} + +def FromIsizeIsize : core.convert.From Isize Isize := { + from_ := fun x => ok (num.FromIsizeIsize.from x) +} + +def FromI8I8 : core.convert.From I8 I8 := { + from_ := fun x => ok (num.FromI8I8.from x) +} + +def FromI16I8 : core.convert.From I16 I8 := { + from_ := fun x => ok (num.FromI16I8.from x) +} + +def FromI16I16 : core.convert.From I16 I16 := { + from_ := fun x => ok (num.FromI16I16.from x) +} + +def FromI32I8 : core.convert.From I32 I8 := { + from_ := fun x => ok (num.FromI32I8.from x) +} + +def FromI32I16 : core.convert.From I32 I16 := { + from_ := fun x => ok (num.FromI32I16.from x) +} + +def FromI32I32 : core.convert.From I32 I32 := { + from_ := fun x => ok (num.FromI32I32.from x) +} + +def FromI64I8 : core.convert.From I64 I8 := { + from_ := fun x => ok (num.FromI64I8.from x) +} + +def FromI64I16 : core.convert.From I64 I16 := { + from_ := fun x => ok (num.FromI64I16.from x) +} + +def FromI64I32 : core.convert.From I64 I32 := { + from_ := fun x => ok (num.FromI64I32.from x) +} + +def FromI64I64 : core.convert.From I64 I64 := { + from_ := fun x => ok (num.FromI64I64.from x) +} + +def FromI128I8 : core.convert.From I128 I8 := { + from_ := fun x => ok (num.FromI128I8.from x) +} + +def FromI128I16 : core.convert.From I128 I16 := { + from_ := fun x => ok (num.FromI128I16.from x) +} + +def FromI128I32 : core.convert.From I128 I32 := { + from_ := fun x => ok (num.FromI128I32.from x) +} + +def FromI128I64 : core.convert.From I128 I64 := { + from_ := fun x => ok (num.FromI128I64.from x) +} + +def FromI128I128 : core.convert.From I128 I128 := { + from_ := fun x => ok (num.FromI128I128.from x) +} + +end core.convert + +end Primitives diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 0ba538b7..9eb5a794 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1394,245 +1394,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) := @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by simp [eq_equiv] --- Conversions -def core.convert.num.FromUsizeBool.from (b : Bool) : Usize := - if b then 1#usize else 0#usize - -def core.convert.num.FromU8Bool.from (b : Bool) : U8 := - if b then 1#u8 else 0#u8 - -def core.convert.num.FromU16Bool.from (b : Bool) : U16 := - if b then 1#u16 else 0#u16 - -def core.convert.num.FromU32Bool.from (b : Bool) : U32 := - if b then 1#u32 else 0#u32 - -def core.convert.num.FromU64Bool.from (b : Bool) : U64 := - if b then 1#u64 else 0#u64 - -def core.convert.num.FromU128Bool.from (b : Bool) : U128 := - if b then 1#u128 else 0#u128 - -def core.convert.num.FromIsizeBool.from (b : Bool) : Isize := - if b then 1#isize else 0#isize - -def core.convert.num.FromI8Bool.from (b : Bool) : I8 := - if b then 1#i8 else 0#i8 - -def core.convert.num.FromI16Bool.from (b : Bool) : I16 := - if b then 1#i16 else 0#i16 - -def core.convert.num.FromI32Bool.from (b : Bool) : I32 := - if b then 1#i32 else 0#i32 - -def core.convert.num.FromI64Bool.from (b : Bool) : I64 := - if b then 1#i64 else 0#i64 - -def core.convert.num.FromI128Bool.from (b : Bool) : I128 := - if b then 1#i128 else 0#i128 - -def core.convert.num.FromUsizeU8.from (x : U8) : Usize := sorry -def core.convert.num.FromUsizeU16.from (x : U16) : Usize := sorry -def core.convert.num.FromUsizeU32.from (x : U32) : Usize := sorry -def core.convert.num.FromUsizeUsize.from (x : Usize) : Usize := sorry - -def core.convert.num.FromU8U8.from (x : U8) : U8 := sorry - -def core.convert.num.FromU16U8.from (x : U8) : U16 := sorry -def core.convert.num.FromU16U16.from (x : U16) : U16 := sorry - -def core.convert.num.FromU32U8.from (x : U8) : U32 := sorry -def core.convert.num.FromU32U16.from (x : U16) : U32 := sorry -def core.convert.num.FromU32U32.from (x : U32) : U32 := sorry - -def core.convert.num.FromU64U8.from (x : U8) : U64 := sorry -def core.convert.num.FromU64U16.from (x : U16) : U64 := sorry -def core.convert.num.FromU64U32.from (x : U32) : U64 := sorry -def core.convert.num.FromU64U64.from (x : U64) : U64 := sorry - -def core.convert.num.FromU128U8.from (x : U8) : U128 := sorry -def core.convert.num.FromU128U16.from (x : U16) : U128 := sorry -def core.convert.num.FromU128U32.from (x : U32) : U128 := sorry -def core.convert.num.FromU128U64.from (x : U64) : U128 := sorry -def core.convert.num.FromU128U128.from (x : U128) : U128 := sorry - -def core.convert.num.FromIsizeI8.from (x : I8) : Isize := sorry -def core.convert.num.FromIsizeI16.from (x : I16) : Isize := sorry -def core.convert.num.FromIsizeI32.from (x : I32) : Isize := sorry -def core.convert.num.FromIsizeIsize.from (x : Isize) : Isize := sorry - -def core.convert.num.FromI8I8.from (x : I8) : I8 := sorry - -def core.convert.num.FromI16I8.from (x : I8) : I16 := sorry -def core.convert.num.FromI16I16.from (x : I16) : I16 := sorry - -def core.convert.num.FromI32I8.from (x : I8) : I32 := sorry -def core.convert.num.FromI32I16.from (x : I16) : I32 := sorry -def core.convert.num.FromI32I32.from (x : I32) : I32 := sorry - -def core.convert.num.FromI64I8.from (x : I8) : I64 := sorry -def core.convert.num.FromI64I16.from (x : I16) : I64 := sorry -def core.convert.num.FromI64I32.from (x : I32) : I64 := sorry -def core.convert.num.FromI64I64.from (x : I64) : I64 := sorry - -def core.convert.num.FromI128I8.from (x : I8) : I128 := sorry -def core.convert.num.FromI128I16.from (x : I16) : I128 := sorry -def core.convert.num.FromI128I32.from (x : I32) : I128 := sorry -def core.convert.num.FromI128I64.from (x : I64) : I128 := sorry -def core.convert.num.FromI128I128.from (x : I128) : I128 := sorry - -def core.convert.FromUsizeU8 : core.convert.From Usize U8 := { - from_ := fun x => ok (core.convert.num.FromUsizeU8.from x) -} - -def core.convert.FromUsizeU16 : core.convert.From Usize U16 := { - from_ := fun x => ok (core.convert.num.FromUsizeU16.from x) -} - -def core.convert.FromUsizeU32 : core.convert.From Usize U32 := { - from_ := fun x => ok (core.convert.num.FromUsizeU32.from x) -} - -def core.convert.FromUsizeUsize : core.convert.From Usize Usize := { - from_ := fun x => ok (core.convert.num.FromUsizeUsize.from x) -} - -def core.convert.FromU8U8 : core.convert.From U8 U8 := { - from_ := fun x => ok (core.convert.num.FromU8U8.from x) -} - -def core.convert.FromU16U8 : core.convert.From U16 U8 := { - from_ := fun x => ok (core.convert.num.FromU16U8.from x) -} - -def core.convert.FromU16U16 : core.convert.From U16 U16 := { - from_ := fun x => ok (core.convert.num.FromU16U16.from x) -} - -def core.convert.FromU32U8 : core.convert.From U32 U8 := { - from_ := fun x => ok (core.convert.num.FromU32U8.from x) -} - -def core.convert.FromU32U16 : core.convert.From U32 U16 := { - from_ := fun x => ok (core.convert.num.FromU32U16.from x) -} - -def core.convert.FromU32U32 : core.convert.From U32 U32 := { - from_ := fun x => ok (core.convert.num.FromU32U32.from x) -} - -def core.convert.FromU64U8 : core.convert.From U64 U8 := { - from_ := fun x => ok (core.convert.num.FromU64U8.from x) -} - -def core.convert.FromU64U16 : core.convert.From U64 U16 := { - from_ := fun x => ok (core.convert.num.FromU64U16.from x) -} - -def core.convert.FromU64U32 : core.convert.From U64 U32 := { - from_ := fun x => ok (core.convert.num.FromU64U32.from x) -} - -def core.convert.FromU64U64 : core.convert.From U64 U64 := { - from_ := fun x => ok (core.convert.num.FromU64U64.from x) -} - -def core.convert.FromU128U8 : core.convert.From U128 U8 := { - from_ := fun x => ok (core.convert.num.FromU128U8.from x) -} - -def core.convert.FromU128U16 : core.convert.From U128 U16 := { - from_ := fun x => ok (core.convert.num.FromU128U16.from x) -} - -def core.convert.FromU128U32 : core.convert.From U128 U32 := { - from_ := fun x => ok (core.convert.num.FromU128U32.from x) -} - -def core.convert.FromU128U64 : core.convert.From U128 U64 := { - from_ := fun x => ok (core.convert.num.FromU128U64.from x) -} - -def core.convert.FromU128U128 : core.convert.From U128 U128 := { - from_ := fun x => ok (core.convert.num.FromU128U128.from x) -} - -def core.convert.FromIsizeI8 : core.convert.From Isize I8 := { - from_ := fun x => ok (core.convert.num.FromIsizeI8.from x) -} - -def core.convert.FromIsizeI16 : core.convert.From Isize I16 := { - from_ := fun x => ok (core.convert.num.FromIsizeI16.from x) -} - -def core.convert.FromIsizeI32 : core.convert.From Isize I32 := { - from_ := fun x => ok (core.convert.num.FromIsizeI32.from x) -} - -def core.convert.FromIsizeIsize : core.convert.From Isize Isize := { - from_ := fun x => ok (core.convert.num.FromIsizeIsize.from x) -} - -def core.convert.FromI8I8 : core.convert.From I8 I8 := { - from_ := fun x => ok (core.convert.num.FromI8I8.from x) -} - -def core.convert.FromI16I8 : core.convert.From I16 I8 := { - from_ := fun x => ok (core.convert.num.FromI16I8.from x) -} - -def core.convert.FromI16I16 : core.convert.From I16 I16 := { - from_ := fun x => ok (core.convert.num.FromI16I16.from x) -} - -def core.convert.FromI32I8 : core.convert.From I32 I8 := { - from_ := fun x => ok (core.convert.num.FromI32I8.from x) -} - -def core.convert.FromI32I16 : core.convert.From I32 I16 := { - from_ := fun x => ok (core.convert.num.FromI32I16.from x) -} - -def core.convert.FromI32I32 : core.convert.From I32 I32 := { - from_ := fun x => ok (core.convert.num.FromI32I32.from x) -} - -def core.convert.FromI64I8 : core.convert.From I64 I8 := { - from_ := fun x => ok (core.convert.num.FromI64I8.from x) -} - -def core.convert.FromI64I16 : core.convert.From I64 I16 := { - from_ := fun x => ok (core.convert.num.FromI64I16.from x) -} - -def core.convert.FromI64I32 : core.convert.From I64 I32 := { - from_ := fun x => ok (core.convert.num.FromI64I32.from x) -} - -def core.convert.FromI64I64 : core.convert.From I64 I64 := { - from_ := fun x => ok (core.convert.num.FromI64I64.from x) -} - -def core.convert.FromI128I8 : core.convert.From I128 I8 := { - from_ := fun x => ok (core.convert.num.FromI128I8.from x) -} - -def core.convert.FromI128I16 : core.convert.From I128 I16 := { - from_ := fun x => ok (core.convert.num.FromI128I16.from x) -} - -def core.convert.FromI128I32 : core.convert.From I128 I32 := { - from_ := fun x => ok (core.convert.num.FromI128I32.from x) -} - -def core.convert.FromI128I64 : core.convert.From I128 I64 := { - from_ := fun x => ok (core.convert.num.FromI128I64.from x) -} - -def core.convert.FromI128I128 : core.convert.From I128 I128 := { - from_ := fun x => ok (core.convert.num.FromI128I128.from x) -} - -- Leading zeros def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry def core.num.U8.leading_zeros (x : U8) : U32 := sorry -- cgit v1.2.3 From 43ff0300e97ad275fa9b62e89577c754f12e3aa3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 12 Apr 2024 18:01:59 +0200 Subject: Add more definitions to the Lean library --- backends/lean/Base/Primitives/Core.lean | 11 ++++ backends/lean/Base/Primitives/CoreConvertNum.lean | 14 +++++ backends/lean/Base/Primitives/Scalar.lean | 63 +++++++++++++++++++ backends/lean/Base/Primitives/Vec.lean | 39 ++++++++++++ compiler/ExtractBuiltin.ml | 73 +++++++++++++++++++++++ 5 files changed, 200 insertions(+) diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean index f67da7d7..99f65985 100644 --- a/backends/lean/Base/Primitives/Core.lean +++ b/backends/lean/Base/Primitives/Core.lean @@ -40,4 +40,15 @@ end deref -- core.ops.deref end ops -- core.ops +/- Trait declaration: [core::clone::Clone] -/ +structure clone.Clone (Self : Type) where + clone : Self → Result Self + +/- [core::clone::impls::{(core::clone::Clone for bool)#19}::clone] -/ +def clone.impls.CloneBool.clone (b : Bool) : Bool := b + +def clone.CloneBool : clone.Clone Bool := { + clone := fun b => ok (clone.impls.CloneBool.clone b) +} + end core diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean index d76fba37..eb456a96 100644 --- a/backends/lean/Base/Primitives/CoreConvertNum.lean +++ b/backends/lean/Base/Primitives/CoreConvertNum.lean @@ -258,6 +258,20 @@ def FromI128I128 : core.convert.From I128 I128 := { from_ := fun x => ok (num.FromI128I128.from x) } +-- to_le_bytes +def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry +def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry +def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry +def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry +def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry + +-- to_be_bytes +def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry +def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry +def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry +def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry +def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry + end core.convert end Primitives diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 9eb5a794..b8d93d30 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1409,4 +1409,67 @@ def core.num.I32.leading_zeros (x : I32) : U32 := sorry def core.num.I64.leading_zeros (x : I64) : U32 := sorry def core.num.I128.leading_zeros (x : I128) : U32 := sorry +-- Clone +def core.clone.impls.CloneUsize.clone (x : Usize) : Usize := x +def core.clone.impls.CloneU8.clone (x : U8) : U8 := x +def core.clone.impls.CloneU16.clone (x : U16) : U16 := x +def core.clone.impls.CloneU32.clone (x : U32) : U32 := x +def core.clone.impls.CloneU64.clone (x : U64) : U64 := x +def core.clone.impls.CloneU128.clone (x : U128) : U128 := x + +def core.clone.impls.CloneIsize.clone (x : Isize) : Isize := x +def core.clone.impls.CloneI8.clone (x : I8) : I8 := x +def core.clone.impls.CloneI16.clone (x : I16) : I16 := x +def core.clone.impls.CloneI32.clone (x : I32) : I32 := x +def core.clone.impls.CloneI64.clone (x : I64) : I64 := x +def core.clone.impls.CloneI128.clone (x : I128) : I128 := x + +def core.clone.CloneUsize : core.clone.Clone Usize := { + clone := fun x => ok (core.clone.impls.CloneUsize.clone x) +} + +def core.clone.CloneU8 : core.clone.Clone U8 := { + clone := fun x => ok (core.clone.impls.CloneU8.clone x) +} + +def core.clone.CloneU16 : core.clone.Clone U16 := { + clone := fun x => ok (core.clone.impls.CloneU16.clone x) +} + +def core.clone.CloneU32 : core.clone.Clone U32 := { + clone := fun x => ok (core.clone.impls.CloneU32.clone x) +} + +def core.clone.CloneU64 : core.clone.Clone U64 := { + clone := fun x => ok (core.clone.impls.CloneU64.clone x) +} + +def core.clone.CloneU128 : core.clone.Clone U128 := { + clone := fun x => ok (core.clone.impls.CloneU128.clone x) +} + +def core.clone.CloneIsize : core.clone.Clone Isize := { + clone := fun x => ok (core.clone.impls.CloneIsize.clone x) +} + +def core.clone.CloneI8 : core.clone.Clone I8 := { + clone := fun x => ok (core.clone.impls.CloneI8.clone x) +} + +def core.clone.CloneI16 : core.clone.Clone I16 := { + clone := fun x => ok (core.clone.impls.CloneI16.clone x) +} + +def core.clone.CloneI32 : core.clone.Clone I32 := { + clone := fun x => ok (core.clone.impls.CloneI32.clone x) +} + +def core.clone.CloneI64 : core.clone.Clone I64 := { + clone := fun x => ok (core.clone.impls.CloneI64.clone x) +} + +def core.clone.CloneI128 : core.clone.Clone I128 := { + clone := fun x => ok (core.clone.impls.CloneI128.clone x) +} + end Primitives diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index 8e2d65a8..5ed7b606 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -182,4 +182,43 @@ theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) : end alloc.vec +/-- [alloc::slice::{@Slice}::to_vec] -/ +def alloc.slice.Slice.to_vec + (T : Type) (cloneInst : core.clone.Clone T) (s : Slice T) : Result (alloc.vec.Vec T) := + -- TODO: we need a monadic map + sorry + +/-- [core::slice::{@Slice}::reverse] -/ +def core.slice.Slice.reverse (T : Type) (s : Slice T) : Slice T := + ⟨ s.val.reverse, by sorry ⟩ + +def alloc.vec.Vec.with_capacity (T : Type) (s : Usize) : alloc.vec.Vec T := Vec.new T + +/- [alloc::vec::{(core::ops::deref::Deref for alloc::vec::Vec)#9}::deref]: + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2624:4-2624:27 + Name pattern: alloc::vec::{core::ops::deref::Deref>}::deref -/ +def alloc.vec.DerefVec.deref (T : Type) (v : Vec T) : Slice T := + ⟨ v.val, v.property ⟩ + +def core.ops.deref.DerefVec (T : Type) : core.ops.deref.Deref (alloc.vec.Vec T) := { + Target := Slice T + deref := fun v => ok (alloc.vec.DerefVec.deref T v) +} + +/- [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec)#10}::deref_mut]: + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2632:4-2632:39 + Name pattern: alloc::vec::{core::ops::deref::DerefMut>}::deref_mut -/ +def alloc.vec.DerefMutVec.deref_mut (T : Type) (v : alloc.vec.Vec T) : + Result ((Slice T) × (Slice T → Result (alloc.vec.Vec T))) := + ok (⟨ v.val, v.property ⟩, λ s => ok ⟨ s.val, s.property ⟩) + +/- Trait implementation: [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec)#10}] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2630:0-2630:49 + Name pattern: core::ops::deref::DerefMut> -/ +def core.ops.deref.DerefMutVec (T : Type) : + core.ops.deref.DerefMut (alloc.vec.Vec T) := { + derefInst := core.ops.deref.DerefVec T + deref_mut := alloc.vec.DerefMutVec.deref_mut T +} + end Primitives diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index ac7a4a24..a9b939b5 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -369,6 +369,20 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = "core::slice::index::{core::slice::index::SliceIndex}::index_mut" (Some "core_slice_index_Slice_index_mut") None; + mk_fun "alloc::slice::{[@T]}::to_vec" (Some "alloc.slice.Slice.to_vec") None; + mk_fun + "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity" + (Some "alloc.vec.Vec.with_capacity") None; + mk_fun "core::slice::{[@T]}::reverse" (Some "core.slice.Slice.reverse") None; + mk_fun + "alloc::vec::{core::ops::deref::Deref>}::deref" + (Some "alloc.vec.DerefVec.deref") + (Some [ true; false ]); + mk_fun + "alloc::vec::{core::ops::deref::DerefMut>}::deref_mut" + (Some "alloc.vec.DerefMutVec.deref_mut") + (Some [ true; false ]); ] @ List.flatten (List.map @@ -404,6 +418,26 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") (fun ty -> "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros") + (* to_le_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes") + (fun ty -> + "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes") + (* to_be_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes") + (fun ty -> + "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes") + (* Clone *) + @ [ + mk_fun "core::clone::impls::{core::clone::Clone}::clone" + (Some "core.clone.CloneBool.clone") None; + ] + (* Clone *) + @ mk_scalar_fun + (fun ty -> "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone") + (fun ty -> + "core.clone.Clone" ^ StringUtils.capitalize_first_letter ty ^ ".clone") let mk_builtin_funs_map () = let m = @@ -457,6 +491,19 @@ let builtin_fun_effects = (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") all_int_names; ] + (* to_{le,be}_bytes *) + @ List.map + (fun ty -> + let pre = "core::num::{" ^ ty ^ "}::" in + [ pre ^ "to_le_bytes"; pre ^ "to_be_bytes" ]) + all_int_names + (* clone *) + @ [ + List.map + (fun ty -> + "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone") + all_int_names; + ] in let int_funs = List.concat int_funs in @@ -468,6 +515,10 @@ let builtin_fun_effects = "alloc::vec::{alloc::vec::Vec<@T, @A>}::len"; "core::mem::replace"; "core::mem::take"; + "core::clone::impls::{core::clone::Clone}::clone"; + "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity"; + "core::slice::{[@T]}::reverse"; + "alloc::vec::{core::ops::deref::Deref>}::deref"; ] @ int_funs in @@ -602,6 +653,8 @@ let builtin_trait_decls_info () = mk_trait "core::convert::From" ~methods_with_extract:(Some [ ("from", "from_") ]) (); + (* Clone *) + mk_trait "core::clone::Clone" ~methods:[ "clone" ] (); ] let mk_builtin_trait_decls_map () = @@ -672,6 +725,17 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = ~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexMutInst") ~filter:(Some [ true; true; false ]) (); + (* core::clone::impls::{core::clone::Clone for bool} *) + fmt "core::clone::Clone" ~extract_name:(Some "core::clone::CloneBool") + (); + fmt "core::ops::deref::Deref>" + ~extract_name:(Some "alloc.vec.DerefVec") + ~filter:(Some [ true; false ]) + (); + fmt "core::ops::deref::DerefMut>" + ~extract_name:(Some "alloc.vec.DerefMutVec") + ~filter:(Some [ true; false ]) + (); ] (* From *) @ List.map @@ -697,6 +761,15 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = ^ StringUtils.capitalize_first_letter small)) ()) int_and_smaller_list + (* Clone *) + @ List.map + (fun ty -> + fmt + ("core::clone::Clone<" ^ ty ^ ">") + ~extract_name: + (Some ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names let mk_builtin_trait_impls_map () = let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in -- cgit v1.2.3