From b86ea3ceb5267f83d45ee7e4d59f3178258d5f2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= Date: Sat, 15 Feb 2025 17:05:13 +0000 Subject: [PATCH] Lean: improve handling of arguments 1. We handle irrefutable patterns in argument positions by adding an equivalent let in the prelude of the function. 2. We handle `atom` types deep inside the type of the arguments. We translate the pattern in the argument as above as a variable, and we replace the sail type variable by `tuple.2.1` in the return type. This path and the variable bound in the let binding in the prelude are definitionally equal. 3. As a side fix, we use more unique names for the autogenerated variable names by numbering them, which should avoid some spurious shadowing. --- src/sail_lean_backend/pretty_print_lean.ml | 81 ++++++++++++++++------ test/lean/SailTinyArm.expected.lean | 68 +++++++++--------- test/lean/bitfield.expected.lean | 4 +- test/lean/bitvec_operation.expected.lean | 4 +- test/lean/enum.expected.lean | 4 +- test/lean/errors.expected.lean | 4 +- test/lean/extern.expected.lean | 6 +- test/lean/extern_bitvec.expected.lean | 4 +- test/lean/implicit.expected.lean | 4 +- test/lean/ite.expected.lean | 4 +- test/lean/let.expected.lean | 4 +- test/lean/loop.expected.lean | 4 +- test/lean/mapping.expected.lean | 4 +- test/lean/match.expected.lean | 6 +- test/lean/match_bv.expected.lean | 4 +- test/lean/option.expected.lean | 8 +-- test/lean/range.expected.lean | 4 +- test/lean/register_vector.expected.lean | 4 +- test/lean/registers.expected.lean | 4 +- test/lean/struct.expected.lean | 4 +- test/lean/struct_of_enum.expected.lean | 4 +- test/lean/typedef.expected.lean | 4 +- test/lean/typquant.expected.lean | 68 ++++++++++++++++-- test/lean/typquant.sail | 56 ++++++++++++++- test/lean/union.expected.lean | 4 +- 25 files changed, 259 insertions(+), 106 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index f5382ff4f..3e4777a9d 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -22,7 +22,7 @@ type context = { global : global_context; env : Type_check.env; (** The typechecking environment of the current function. This environment is reset using [initial_context] when - we start processing a new function. *) + we start processing a new function. Note that we use it to store paths of the form id.x.y.z. *) kid_id_renames : id option KBindings.t; (** Associates a kind variable to the corresponding argument of the function, used for implicit arguments. *) kid_id_renames_rev : kid Bindings.t; (** Inverse of the [kid_id_renames] mapping. *) @@ -67,19 +67,22 @@ let doc_kid ctx (Kid_aux (Var x, _) as ki) = let is_enum env id = match Env.lookup_id id env with Enum _ -> true | _ -> false -let pat_is_plain_binder env (P_aux (p, _)) = +let pat_is_plain_binder ?(suffix = "") env (P_aux (p, _)) = match p with | P_id id when not (is_enum env id) -> Some (Some id, None) + | P_id _ -> Some (Some (Id_aux (Id ("id" ^ suffix), Unknown)), None) | P_typ (typ, P_aux (P_id id, _)) when not (is_enum env id) -> Some (Some id, Some typ) | P_wild | P_typ (_, P_aux (P_wild, _)) -> Some (None, None) - | P_var (_, _) -> Some (Some (Id_aux (Id "var", Unknown)), None) - | P_app (_, _) -> Some (Some (Id_aux (Id "app", Unknown)), None) - | P_vector _ -> Some (Some (Id_aux (Id "vect", Unknown)), None) - | P_tuple _ -> Some (Some (Id_aux (Id "tuple", Unknown)), None) - | P_list _ -> Some (Some (Id_aux (Id "list", Unknown)), None) - | P_cons (_, _) -> Some (Some (Id_aux (Id "cons", Unknown)), None) + | P_var (_, _) -> Some (Some (Id_aux (Id ("var" ^ suffix), Unknown)), None) + | P_app (_, _) -> Some (Some (Id_aux (Id ("app" ^ suffix), Unknown)), None) + | P_vector _ -> Some (Some (Id_aux (Id ("vect" ^ suffix), Unknown)), None) + | P_tuple _ -> Some (Some (Id_aux (Id ("tuple" ^ suffix), Unknown)), None) + | P_list _ -> Some (Some (Id_aux (Id ("list" ^ suffix), Unknown)), None) + | P_cons (_, _) -> Some (Some (Id_aux (Id ("cons" ^ suffix), Unknown)), None) | P_lit (L_aux (L_unit, _)) -> Some (Some (Id_aux (Id "_", Unknown)), None) - | P_lit _ -> Some (Some (Id_aux (Id "lit", Unknown)), None) + | P_lit _ -> Some (Some (Id_aux (Id ("lit" ^ suffix), Unknown)), None) + | P_typ _ -> Some (Some (Id_aux (Id ("typ" ^ suffix), Unknown)), None) + | P_struct _ -> Some (Some (Id_aux (Id ("struct_pat" ^ suffix), Unknown)), None) | _ -> None (* Copied from the Coq PP *) @@ -434,7 +437,8 @@ let rec doc_pat ?(in_vector = false) (P_aux (p, (l, annot)) as pat) = | P_vector pats -> concat (List.map (doc_pat ~in_vector:true) pats) | P_vector_concat pats -> separate (string ",") (List.map (doc_pat ~in_vector:true) pats) |> brackets | P_app (Id_aux (Id "None", _), p) -> string "none" - | P_app (cons, pats) -> doc_id_ctor (fixup_match_id cons) ^^ space ^^ separate_map (string ", ") doc_pat pats + | P_app (cons, pats) -> + string "." ^^ doc_id_ctor (fixup_match_id cons) ^^ space ^^ separate_map (string ", ") doc_pat pats | P_var (p, _) -> doc_pat p | P_as (pat, id) -> doc_pat pat | P_struct (pats, _) -> @@ -668,7 +672,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = and doc_fexp with_arrow ctx (FE_aux (FE_fexp (field, e), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp false ctx e let doc_binder ctx i t = - let paranthesizer = + let parenthesizer = match t with | Typ_aux (Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]), _) -> implicit_parens @@ -676,7 +680,39 @@ let doc_binder ctx i t = in (* Overwrite the id if it's captured *) let ctx = match captured_typ_var (i, t) with Some (i, ki) -> add_single_kid_id_rename ctx i ki | _ -> ctx in - (ctx, separate space [doc_id_ctor i; colon; doc_typ ctx t] |> paranthesizer) + (ctx, separate space [doc_id_ctor i; colon; doc_typ ctx t] |> parenthesizer) + +(** Find all patterns in the arguments of the sail function that Lean cannot handle in a [def], +and add them as let bindings in the prelude of the translation of the function. This assumes +that the pattern is irrefutable. *) +let add_function_pattern ctx fixup_binders (P_aux (pat, pat_annot) as pat_full) var typ = + match pat with + | P_id _ | P_typ (_, P_aux (P_id _, _)) | P_tuple [] | P_lit _ | P_wild -> fixup_binders + | _ -> + fun (E_aux (_, body_annot) as body : tannot exp) -> + E_aux + ( E_let (LB_aux (LB_val (pat_full, E_aux (E_id var, (Unknown, mk_tannot ctx.env typ))), pat_annot), body), + body_annot + ) + |> fixup_binders + +(** Find all the [int] and [atom] types in the function pattern and express them as paths that use the +lean variables, so that we can use them in the return type of the function. For example, see the function +[two_tuples_atom] in the test case test/lean/typquant.sail. +*) +let rec add_path_renamings ~path ctx (P_aux (pat, pat_annot)) (Typ_aux (typ, typ_annot) as typ_full) = + match (pat, typ) with + | P_tuple pats, Typ_tuple typs -> + List.fold_left + (fun (ctx, i) (pat, typ) -> (add_path_renamings ~path:(Printf.sprintf "%s.%i" path i) ctx pat typ, i + 1)) + (ctx, 1) (List.combine pats typs) + |> fst + | P_id id, typ -> ( + match captured_typ_var (id, typ_full) with + | Some (_, kid) -> add_single_kid_id_rename ctx (mk_id path) kid + | None -> ctx + ) + | _ -> ctx let doc_funcl_init global (FCL_aux (FCL_funcl (id, pexp), annot)) = let env = env_of_tannot (snd annot) in @@ -688,23 +724,26 @@ let doc_funcl_init global (FCL_aux (FCL_funcl (id, pexp), annot)) = in let pat, _, exp, _ = destruct_pexp pexp in let pats, fixup_binders = untuple_args_pat arg_typs pat in - let binders : (id * typ) list = + let binders : (tannot pat * id * typ) list = pats - |> List.map (fun (pat, typ) -> - match pat_is_plain_binder env pat with - | Some (Some id, _) -> (id, typ) - | Some (None, _) -> (Id_aux (Id "x", l), typ) (* TODO fresh name or wildcard instead of x *) + |> List.mapi (fun i (pat, typ) -> + match pat_is_plain_binder ~suffix:(Printf.sprintf "_%i" i) env pat with + | Some (Some id, _) -> (pat, id, typ) + | Some (None, _) -> + (pat, mk_id ~loc:l (Printf.sprintf "x_%i" i), typ) (* TODO fresh name or wildcard instead of x *) | _ -> failwith "Argument pattern not translatable yet." ) in let ctx = context_init env global in - let ctx, binders = + let ctx, binders, fixup_binders = List.fold_left - (fun (ctx, bs) (i, t) -> + (fun (ctx, bs, fixup_binders) (pat, i, t) -> let ctx, d = doc_binder ctx i t in - (ctx, bs @ [d]) + let fixup_binders = add_function_pattern ctx fixup_binders pat i t in + let ctx = add_path_renamings ~path:(string_of_id i) ctx pat t in + (ctx, bs @ [d], fixup_binders) ) - (ctx, []) binders + (ctx, [], fixup_binders) binders in let typ_quant_comment = doc_typ_quant_in_comment ctx tq_all in (* Use auto-implicits for type quanitifiers for now and see if this works *) diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean index 3f4e73f73..fdb38c291 100644 --- a/test/lean/SailTinyArm.expected.lean +++ b/test/lean/SailTinyArm.expected.lean @@ -554,13 +554,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ @@ -1846,11 +1846,11 @@ def wMem (addr : (BitVec 64)) (value : (BitVec 64)) : SailM Unit := do value := (some value) tag := none } match (← (sail_mem_write req)) with - | Ok _ => (pure ()) - | Err _ => throw Error.Exit + | .Ok _ => (pure ()) + | .Err _ => throw Error.Exit -/-- Type quantifiers: x : Nat, x ∈ {32, 64} -/ -def sail_address_announce (x : Nat) (x : (BitVec x)) : Unit := +/-- Type quantifiers: x_0 : Nat, x_0 ∈ {32, 64} -/ +def sail_address_announce (x_0 : Nat) (x_1 : (BitVec x_0)) : Unit := () def wMem_Addr (addr : (BitVec 64)) : Unit := @@ -1878,8 +1878,8 @@ def rMem (addr : (BitVec 64)) : SailM (BitVec 64) := do size := 8 tag := false } match (← (sail_mem_read req)) with - | Ok (value, _) => (pure value) - | Err _ => throw Error.Exit + | .Ok (value, _) => (pure value) + | .Err _ => throw Error.Exit /-- Type quantifiers: m : Nat, n : Nat, t : Nat, 0 ≤ t ∧ t ≤ 31, 0 ≤ n ∧ n ≤ 31, 0 ≤ m ∧ m ≤ 31 -/ @@ -1919,11 +1919,11 @@ def execute_CompareAndBranch (t : Nat) (offset : (BitVec 64)) : SailM Unit := do def execute (merge_var : ast) : SailM Unit := do match merge_var with - | LoadRegister (t, n, m) => (execute_LoadRegister t n m) - | StoreRegister (t, n, m) => (execute_StoreRegister t n m) - | ExclusiveOr (d, n, m) => (execute_ExclusiveOr d n m) - | DataMemoryBarrier arg0 => (execute_DataMemoryBarrier arg0) - | CompareAndBranch (t, offset) => (execute_CompareAndBranch t offset) + | .LoadRegister (t, n, m) => (execute_LoadRegister t n m) + | .StoreRegister (t, n, m) => (execute_StoreRegister t n m) + | .ExclusiveOr (d, n, m) => (execute_ExclusiveOr d n m) + | .DataMemoryBarrier arg0 => (execute_DataMemoryBarrier arg0) + | .CompareAndBranch (t, offset) => (execute_CompareAndBranch t offset) def decode (v__0 : (BitVec 32)) : (Option ast) := if (Bool.and (Eq (Sail.BitVec.extractLsb v__0 31 24) (0xF8 : (BitVec 8))) @@ -1964,52 +1964,52 @@ def iFetch (addr : (BitVec 64)) : SailM (BitVec 32) := do size := 4 tag := false } match (← (sail_mem_read req)) with - | Ok (value, _) => (pure value) - | Err _ => throw Error.Exit + | .Ok (value, _) => (pure value) + | .Err _ => throw Error.Exit def fetch_and_execute (_ : Unit) : SailM Unit := do let machineCode ← do (iFetch (← readReg _PC)) let instr := (decode machineCode) match instr with - | some instr => (execute instr) + | .some instr => (execute instr) | none => assert false "Unsupported Encoding" /-- Type quantifiers: k_a : Type, k_b : Type -/ def is_ok (r : (Result k_a k_b)) : Bool := match r with - | Ok _ => true - | Err _ => false + | .Ok _ => true + | .Err _ => false /-- Type quantifiers: k_a : Type, k_b : Type -/ def is_err (r : (Result k_a k_b)) : Bool := match r with - | Ok _ => false - | Err _ => true + | .Ok _ => false + | .Err _ => true /-- Type quantifiers: k_a : Type, k_b : Type -/ def ok_option (r : (Result k_a k_b)) : (Option k_a) := match r with - | Ok x => (some x) - | Err _ => none + | .Ok x => (some x) + | .Err _ => none /-- Type quantifiers: k_a : Type, k_b : Type -/ def err_option (r : (Result k_a k_b)) : (Option k_b) := match r with - | Ok _ => none - | Err err => (some err) + | .Ok _ => none + | .Err err => (some err) /-- Type quantifiers: k_a : Type, k_b : Type -/ def unwrap_or (r : (Result k_a k_b)) (y : k_a) : k_a := match r with - | Ok x => x - | Err _ => y + | .Ok x => x + | .Err _ => y /-- Type quantifiers: k_n : Nat, k_n > 0 -/ -def sail_instr_announce (x : (BitVec k_n)) : Unit := +def sail_instr_announce (x_0 : (BitVec k_n)) : Unit := () -/-- Type quantifiers: x : Nat, x ∈ {32, 64} -/ -def sail_branch_announce (x : Nat) (x : (BitVec x)) : Unit := +/-- Type quantifiers: x_0 : Nat, x_0 ∈ {32, 64} -/ +def sail_branch_announce (x_0 : Nat) (x_1 : (BitVec x_0)) : Unit := () def sail_reset_registers (_ : Unit) : Unit := @@ -2019,11 +2019,11 @@ def sail_synchronize_registers (_ : Unit) : Unit := () /-- Type quantifiers: k_a : Type -/ -def sail_mark_register (x : (RegisterRef RegisterType k_a)) (x : String) : Unit := +def sail_mark_register (x_0 : (RegisterRef RegisterType k_a)) (x_1 : String) : Unit := () /-- Type quantifiers: k_a : Type, k_b : Type -/ -def sail_mark_register_pair (x : (RegisterRef RegisterType k_a)) (x : (RegisterRef RegisterType k_b)) (x : String) : Unit := +def sail_mark_register_pair (x_0 : (RegisterRef RegisterType k_a)) (x_1 : (RegisterRef RegisterType k_b)) (x_2 : String) : Unit := () /-- Type quantifiers: k_a : Type -/ @@ -2078,7 +2078,7 @@ def undefined_Explicit_access_kind (_ : Unit) : SailM Explicit_access_kind := do : Type, k_n > 0 ∧ k_vasize > 0 -/ def mem_read_request_is_exclusive (request : Mem_read_request k_n k_vasize k_pa k_translation_summary k_arch_ak) : Bool := match request.access_kind with - | AK_explicit eak => + | .AK_explicit eak => match eak.variety with | AV_exclusive => true | _ => false @@ -2088,7 +2088,7 @@ def mem_read_request_is_exclusive (request : Mem_read_request k_n k_vasize k_pa : Type, k_n > 0 ∧ k_vasize > 0 -/ def mem_read_request_is_ifetch (request : Mem_read_request k_n k_vasize k_pa k_translation_summary k_arch_ak) : Bool := match request.access_kind with - | AK_ifetch () => true + | .AK_ifetch () => true | _ => false def __monomorphize_reads : Bool := false @@ -2099,7 +2099,7 @@ def __monomorphize_writes : Bool := false : Type, k_n > 0 ∧ k_vasize > 0 -/ def mem_write_request_is_exclusive (request : Mem_write_request k_n k_vasize k_pa k_translation_summary k_arch_ak) : Bool := match request.access_kind with - | AK_explicit eak => + | .AK_explicit eak => match eak.variety with | AV_exclusive => true | _ => false diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index a828c5edd..e1c7fb69d 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -76,13 +76,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean index e74ac5da8..bdaf9f98e 100644 --- a/test/lean/bitvec_operation.expected.lean +++ b/test/lean/bitvec_operation.expected.lean @@ -63,13 +63,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index e38aa2194..a0f7cfd73 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -68,13 +68,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/errors.expected.lean b/test/lean/errors.expected.lean index 8c3975e3b..3cda3a78e 100644 --- a/test/lean/errors.expected.lean +++ b/test/lean/errors.expected.lean @@ -74,13 +74,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean index 259e7808b..354ec8adb 100644 --- a/test/lean/extern.expected.lean +++ b/test/lean/extern.expected.lean @@ -21,7 +21,7 @@ def spc_forwards (_ : Unit) : String := def spc_forwards_matches (_ : Unit) : Bool := true -def spc_backwards (x : String) : Unit := +def spc_backwards (x_0 : String) : Unit := () def spc_backwards_matches (s : String) : Bool := @@ -34,7 +34,7 @@ def opt_spc_forwards (_ : Unit) : String := def opt_spc_forwards_matches (_ : Unit) : Bool := true -def opt_spc_backwards (x : String) : Unit := +def opt_spc_backwards (x_0 : String) : Unit := () def opt_spc_backwards_matches (s : String) : Bool := @@ -46,7 +46,7 @@ def def_spc_forwards (_ : Unit) : String := def def_spc_forwards_matches (_ : Unit) : Bool := true -def def_spc_backwards (x : String) : Unit := +def def_spc_backwards (x_0 : String) : Unit := () def def_spc_backwards_matches (s : String) : Bool := diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean index 6b5de429e..338dbb3c4 100644 --- a/test/lean/extern_bitvec.expected.lean +++ b/test/lean/extern_bitvec.expected.lean @@ -63,13 +63,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean index 5d4de1f85..ce874e4a7 100644 --- a/test/lean/implicit.expected.lean +++ b/test/lean/implicit.expected.lean @@ -63,13 +63,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean index 49097f25f..a1615b6d6 100644 --- a/test/lean/ite.expected.lean +++ b/test/lean/ite.expected.lean @@ -78,13 +78,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean index 7288b144a..8228d7e81 100644 --- a/test/lean/let.expected.lean +++ b/test/lean/let.expected.lean @@ -63,13 +63,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/loop.expected.lean b/test/lean/loop.expected.lean index 752800b3e..053aa4928 100644 --- a/test/lean/loop.expected.lean +++ b/test/lean/loop.expected.lean @@ -74,13 +74,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/mapping.expected.lean b/test/lean/mapping.expected.lean index 9dad1840b..5b73f3864 100644 --- a/test/lean/mapping.expected.lean +++ b/test/lean/mapping.expected.lean @@ -68,13 +68,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean index 12030138d..62cf22054 100644 --- a/test/lean/match.expected.lean +++ b/test/lean/match.expected.lean @@ -83,13 +83,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ @@ -111,7 +111,7 @@ def match_enum (x : E) : (BitVec 1) := def match_option (x : (Option (BitVec 1))) : (BitVec 1) := match x with - | some x => x + | .some x => x | none => 0#1 /-- Type quantifiers: y : Int, x : Int -/ diff --git a/test/lean/match_bv.expected.lean b/test/lean/match_bv.expected.lean index 30b8a5d2c..eca42cf36 100644 --- a/test/lean/match_bv.expected.lean +++ b/test/lean/match_bv.expected.lean @@ -63,13 +63,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean index 89e81385f..5daa64903 100644 --- a/test/lean/option.expected.lean +++ b/test/lean/option.expected.lean @@ -63,13 +63,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ @@ -82,12 +82,12 @@ def concat_str_dec (str : String) (x : Int) : String := def match_option (x : (Option (BitVec 1))) : (BitVec 1) := match x with - | some x => x + | .some x => x | none => 0#1 def option_match (x : (Option Unit)) (y : (BitVec 1)) : (Option (BitVec 1)) := match x with - | some () => (some y) + | .some () => (some y) | none => none def initialize_registers (_ : Unit) : Unit := diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean index e320a5b8f..431edc962 100644 --- a/test/lean/range.expected.lean +++ b/test/lean/range.expected.lean @@ -63,13 +63,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean index 59344a4ab..64494dbea 100644 --- a/test/lean/register_vector.expected.lean +++ b/test/lean/register_vector.expected.lean @@ -138,13 +138,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index 84739c7f0..6360c6357 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -92,13 +92,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index a3a512bbb..d4275191f 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -80,13 +80,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean index 4cdc80aea..34e87629a 100644 --- a/test/lean/struct_of_enum.expected.lean +++ b/test/lean/struct_of_enum.expected.lean @@ -72,13 +72,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean index 4a58ab788..f416a39a0 100644 --- a/test/lean/typedef.expected.lean +++ b/test/lean/typedef.expected.lean @@ -71,13 +71,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean index 14191e2a6..539bad94c 100644 --- a/test/lean/typquant.expected.lean +++ b/test/lean/typquant.expected.lean @@ -13,6 +13,12 @@ inductive option (k_a : Type) where open option + +inductive virtaddr where + | virtaddr (_ : (BitVec 32)) + +open virtaddr + abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit /-- Type quantifiers: x : Int -/ @@ -63,13 +69,13 @@ def fmod_int (n : Int) (m : Int) : Int := /-- Type quantifiers: k_a : Type -/ def is_none (opt : (Option k_a)) : Bool := match opt with - | some _ => false + | .some _ => false | none => true /-- Type quantifiers: k_a : Type -/ def is_some (opt : (Option k_a)) : Bool := match opt with - | some _ => true + | .some _ => true | none => false /-- Type quantifiers: k_n : Int -/ @@ -80,14 +86,68 @@ def concat_str_bits (str : String) (x : (BitVec k_n)) : String := def concat_str_dec (str : String) (x : Int) : String := (HAppend.hAppend str (Int.repr x)) -/-- Type quantifiers: n : Int -/ -def foo (n : Int) : (BitVec 4) := +/-- Type quantifiers: n : Nat, n > 0 -/ +def foo (n : Nat) : (BitVec 4) := (0xF : (BitVec 4)) +/-- Type quantifiers: n : Nat, n > 0 -/ +def foo2 (n : Nat) : (BitVec n) := + (BitVec.zero n) + /-- Type quantifiers: k_n : Int -/ def bar (x : (BitVec k_n)) : (BitVec k_n) := x +def two_tuples (tuple_0 : (String × String)) (tuple_1 : (String × String)) : String := + let (x, y) := tuple_0 + let (z, t) := tuple_1 + y + +/-- Type quantifiers: tuple_0.2 : Nat, tuple_0.2 ≥ 0 -/ +def two_tuples_atom (tuple_0 : (String × Nat)) (tuple_1 : (String × String)) : (BitVec tuple_0.2) := + let (x, y) := tuple_0 + let (z, t) := tuple_1 + (BitVec.zero y) + +def tuple_of_tuple (tuple_0 : (String × String)) : String := + let (s1, s2) := tuple_0 + s1 + +def use_tuple_of_tuple (s : String) : String := + (tuple_of_tuple (s, s)) + +/-- Type quantifiers: k_nn : Nat, k_nn > 0 -/ +def hex_bits_signed2_forwards (bv : (BitVec k_nn)) : (Nat × String) := + let len := (Sail.BitVec.length bv) + let s := + if (Eq (BitVec.access bv (HSub.hSub len 1)) 1#1) + then "stub1" + else "stub2" + ((Sail.BitVec.length bv), s) + +/-- Type quantifiers: k_nn : Nat, k_nn > 0 -/ +def hex_bits_signed2_forwards_matches (bv : (BitVec k_nn)) : Bool := + true + +/-- Type quantifiers: tuple_0.1 : Nat, tuple_0.1 > 0 -/ +def hex_bits_signed2_backwards (tuple_0 : (Nat × String)) : (BitVec tuple_0.1) := + let (notn, str) := tuple_0 + if (Eq str "-") + then (BitVec.zero notn) + else let parsed := (BitVec.zero notn) + if (Eq (BitVec.access parsed (HSub.hSub notn 1)) 0#1) + then parsed + else (BitVec.zero notn) + +/-- Type quantifiers: tuple_0.1 : Nat, tuple_0.1 > 0 -/ +def hex_bits_signed2_backwards_matches (tuple_0 : (Nat × String)) : Bool := + let (n, str) := tuple_0 + true + +def test_constr (app_0 : virtaddr) : (BitVec 32) := + let .virtaddr addr := app_0 + addr + def initialize_registers (_ : Unit) : Unit := () diff --git a/test/lean/typquant.sail b/test/lean/typquant.sail index 7362c390e..e70be26c6 100644 --- a/test/lean/typquant.sail +++ b/test/lean/typquant.sail @@ -2,14 +2,68 @@ default Order dec $include -val foo : forall 'n. int('n) -> bits(4) +val foo : forall 'n, 'n > 0. int('n) -> bits(4) function foo(n) = { 0xF } +val foo2 : forall 'n, 'n > 0. int('n) -> bits('n) + +function foo2(n) = { + sail_zeros(n) +} + val bar : forall 'n. bits('n) -> bits('n) function bar(x) = { x } + +val two_tuples : ((string, string), (string, string)) -> string +function two_tuples((x, y), (z, t)) = y + +val two_tuples_atom : forall 'n, 'n >= 0. ((string, int('n)), (string, string)) -> bits('n) +function two_tuples_atom((x, y), (z, t)) = sail_zeros(y) + +val tuple_of_tuple : ((string, string)) -> string +function tuple_of_tuple(s1, s2) = s1 + +function use_tuple_of_tuple(s : string) -> string = { + // tutuple(s, s); + tuple_of_tuple((s, s)) +} + + +val hex_bits_signed2 : forall 'nn, 'nn > 0. bits('nn) <-> (int('nn), string) + +function hex_bits_signed2_forwards(bv) = { + let len = length(bv); + let s = if bv[len - 1] == bitone then { + "stub1" + } else { + "stub2" + }; + (length(bv), s) +} + +function hex_bits_signed2_forwards_matches(bv) = true + +function hex_bits_signed2_backwards(notn, str) = { + if str == "-" then { + sail_zeros(notn) + } else { + let parsed = sail_zeros(notn); + if parsed[notn - 1] == bitzero then { + parsed + } else { + sail_zeros(notn) + } + } +} + +function hex_bits_signed2_backwards_matches(n, str) = true + + newtype virtaddr = virtaddr : bits(32) + +function test_constr (virtaddr(addr) : virtaddr) -> bits(32) = addr diff --git a/test/lean/union.expected.lean b/test/lean/union.expected.lean index 925e739cf..32314d670 100644 --- a/test/lean/union.expected.lean +++ b/test/lean/union.expected.lean @@ -39,8 +39,8 @@ def undefined_circle (_ : Unit) : SailM circle := do /-- Type quantifiers: k_a : Type -/ def is_none (opt : my_option k_a) : Bool := match opt with - | MySome _ => false - | MyNone () => true + | .MySome _ => false + | .MyNone () => true /-- Type quantifiers: k_a : Type -/ def use_is_none (opt : my_option k_a) : Bool :=