Skip to content

Commit

Permalink
Update construct & numerics
Browse files Browse the repository at this point in the history
  • Loading branch information
@ShinWonho
ShinWonho committed Jan 29, 2024
1 parent b310869 commit 2ebb9d5
Show file tree
Hide file tree
Showing 2 changed files with 64 additions and 64 deletions.
54 changes: 27 additions & 27 deletions spectec/src/backend-interpreter/construct.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -323,39 +323,39 @@ let al_to_float_relop: value -> FloatOp.relop = function
let al_to_relop: value list -> relop = al_to_op al_to_int_relop al_to_float_relop

let al_to_int_cvtop: value list -> IntOp.cvtop = function
| TextV "Extend" :: args ->
| CaseV ("EXTEND", []) :: args ->
(match args with
| [ CaseV ("I32", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.ExtendSI32
| [ CaseV ("I32", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.ExtendUI32
| l -> fail_list "extend" l)
| [ TextV "Wrap"; CaseV ("I64", []); OptV None ] -> IntOp.WrapI64
| TextV "Trunc" :: args ->
| [ CaseV ("Wrap", []); CaseV ("I64", []); OptV None ] -> IntOp.WrapI64
| CaseV ("TRUNC", []) :: args ->
(match args with
| [ CaseV ("F32", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSF32
| [ CaseV ("F32", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncUF32
| [ CaseV ("F64", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSF64
| [ CaseV ("F64", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncUF64
| l -> fail_list "trunc" l)
| TextV "TruncSat" :: args ->
| CaseV ("TRUNCSAT", []) :: args ->
(match args with
| [ CaseV ("F32", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSatSF32
| [ CaseV ("F32", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncSatUF32
| [ CaseV ("F64", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSatSF64
| [ CaseV ("F64", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncSatUF64
| l -> fail_list "truncsat" l)
| [ TextV "Reinterpret"; _; OptV None ] -> IntOp.ReinterpretFloat
| [ CaseV ("REINTERPRET", []); _; OptV None ] -> IntOp.ReinterpretFloat
| l -> fail_list "integer cvtop" l
let al_to_float_cvtop : value list -> FloatOp.cvtop = function
| TextV "Convert" :: args ->
| CaseV ("CONVERT", []) :: args ->
(match args with
| [ CaseV ("I32", []); OptV (Some (CaseV (("S", [])))) ] -> FloatOp.ConvertSI32
| [ CaseV ("I32", []); OptV (Some (CaseV (("U", [])))) ] -> FloatOp.ConvertUI32
| [ CaseV ("I64", []); OptV (Some (CaseV (("S", [])))) ] -> FloatOp.ConvertSI64
| [ CaseV ("I64", []); OptV (Some (CaseV (("U", [])))) ] -> FloatOp.ConvertUI64
| l -> fail_list "convert" l)
| [ TextV "Promote"; CaseV ("F32", []); OptV None ] -> FloatOp.PromoteF32
| [ TextV "Demote"; CaseV ("F64", []); OptV None ] -> FloatOp.DemoteF64
| [ TextV "Reinterpret"; _; OptV None ] -> FloatOp.ReinterpretInt
| [ CaseV ("PROMOTE", []); CaseV ("F32", []); OptV None ] -> FloatOp.PromoteF32
| [ CaseV ("DEMOTE", []); CaseV ("F64", []); OptV None ] -> FloatOp.DemoteF64
| [ CaseV ("REINTERPRET", []); _; OptV None ] -> FloatOp.ReinterpretInt
| l -> fail_list "float cvtop" l
let al_to_cvtop: value list -> cvtop = function
| CaseV ("I32", []) :: op -> I32 (al_to_int_cvtop op)
Expand All @@ -372,12 +372,12 @@ let al_to_extension : value -> Pack.extension = function
| v -> fail "extension" v

let al_to_vop f1 f2 = function
| [ TupV [ CaseV ("I8", []); NumV 16L ]; vop ] -> V128 (V128.I8x16 (f1 vop))
| [ TupV [ CaseV ("I16", []); NumV 8L ]; vop ] -> V128 (V128.I16x8 (f1 vop))
| [ TupV [ CaseV ("I32", []); NumV 4L ]; vop ] -> V128 (V128.I32x4 (f1 vop))
| [ TupV [ CaseV ("I64", []); NumV 2L ]; vop ] -> V128 (V128.I64x2 (f1 vop))
| [ TupV [ CaseV ("F32", []); NumV 4L ]; vop ] -> V128 (V128.F32x4 (f2 vop))
| [ TupV [ CaseV ("F64", []); NumV 2L ]; vop ] -> V128 (V128.F64x2 (f2 vop))
| [ TupV [ CaseV ("I8", []); NumV 16L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I8x16 (f1 vop))
| [ TupV [ CaseV ("I16", []); NumV 8L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I16x8 (f1 vop))
| [ TupV [ CaseV ("I32", []); NumV 4L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I32x4 (f1 vop))
| [ TupV [ CaseV ("I64", []); NumV 2L ]; CaseV ("_VI", [vop]) ] -> V128 (V128.I64x2 (f1 vop))
| [ TupV [ CaseV ("F32", []); NumV 4L ]; CaseV ("_VF", [vop]) ] -> V128 (V128.F32x4 (f2 vop))
| [ TupV [ CaseV ("F64", []); NumV 2L ]; CaseV ("_VF", [vop]) ] -> V128 (V128.F64x2 (f2 vop))
| l -> fail_list "vop" l

let al_to_vvop f = function
Expand All @@ -401,14 +401,14 @@ let al_to_vbitmaskop : value list -> vec_bitmaskop = function
let al_to_int_vrelop : value -> V128Op.irelop = function
| CaseV ("EQ", []) -> V128Op.Eq
| CaseV ("NE", []) -> V128Op.Ne
| CaseV ("LTS", []) -> V128Op.LtS
| CaseV ("LTU", []) -> V128Op.LtU
| CaseV ("LES", []) -> V128Op.LeS
| CaseV ("LEU", []) -> V128Op.LeU
| CaseV ("GTS", []) -> V128Op.GtS
| CaseV ("GTU", []) -> V128Op.GtU
| CaseV ("GES", []) -> V128Op.GeS
| CaseV ("GEU", []) -> V128Op.GeU
| CaseV ("LT", [CaseV ("S", [])]) -> V128Op.LtS
| CaseV ("LT", [CaseV ("U", [])]) -> V128Op.LtU
| CaseV ("LE", [CaseV ("S", [])]) -> V128Op.LeS
| CaseV ("LE", [CaseV ("U", [])]) -> V128Op.LeU
| CaseV ("GT", [CaseV ("S", [])]) -> V128Op.GtS
| CaseV ("GT", [CaseV ("U", [])]) -> V128Op.GtU
| CaseV ("GE", [CaseV ("S", [])]) -> V128Op.GeS
| CaseV ("GE", [CaseV ("U", [])]) -> V128Op.GeU
| v -> fail "integer vrelop" v

let al_to_float_vrelop : value -> V128Op.frelop = function
Expand Down Expand Up @@ -1213,16 +1213,16 @@ let al_of_float_cvtop num_bits = function
let al_of_cvtop = function
| I32 op ->
let op', to_, ext = al_of_int_cvtop "32" op in
[ nullary "I32"; TextV op'; nullary to_; optV ext ]
[ nullary "I32"; nullary op'; nullary to_; optV ext ]
| I64 op ->
let op', to_, ext = al_of_int_cvtop "64" op in
[ nullary "I64"; TextV op'; nullary to_; optV ext ]
[ nullary "I64"; nullary op'; nullary to_; optV ext ]
| F32 op ->
let op', to_, ext = al_of_float_cvtop "32" op in
[ nullary "F32"; TextV op'; nullary to_; optV ext ]
[ nullary "F32"; nullary op'; nullary to_; optV ext ]
| F64 op ->
let op', to_, ext = al_of_float_cvtop "64" op in
[ nullary "F64"; TextV op'; nullary to_; optV ext ]
[ nullary "F64"; nullary op'; nullary to_; optV ext ]

(* Vector operator *)

Expand Down
74 changes: 37 additions & 37 deletions spectec/src/backend-interpreter/numerics.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,49 +244,49 @@ let cvtop : numerics =
name = "cvtop";
f =
(function
| [ TextV op; CaseV (t_from, []); CaseV (t_to, []); OptV sx_opt; v ] -> (
| [ CaseV (op, []); CaseV (t_from, []); CaseV (t_to, []); OptV sx_opt; v ] -> (
let sx = match sx_opt with
| None -> ""
| Some (CaseV (sx, [])) -> sx
| _ -> failwith "invalid cvtop" in
listV ([| catch_ixx_exception (fun _ -> match op, t_to, t_from, sx with
(* Conversion to I32 *)
| "Wrap", "I32", "I64", "" -> wrap_i32_cvtop_i64 I32_convert.wrap_i64 v
| "Trunc", "I32", "F32", "S" -> wrap_i32_cvtop_f32 I32_convert.trunc_f32_s v
| "Trunc", "I32", "F32", "U" -> wrap_i32_cvtop_f32 I32_convert.trunc_f32_u v
| "Trunc", "I32", "F64", "S" -> wrap_i32_cvtop_f64 I32_convert.trunc_f64_s v
| "Trunc", "I32", "F64", "U" -> wrap_i32_cvtop_f64 I32_convert.trunc_f64_u v
| "TruncSat", "I32", "F32", "S" -> wrap_i32_cvtop_f32 I32_convert.trunc_sat_f32_s v
| "TruncSat", "I32", "F32", "U" -> wrap_i32_cvtop_f32 I32_convert.trunc_sat_f32_u v
| "TruncSat", "I32", "F64", "S" -> wrap_i32_cvtop_f64 I32_convert.trunc_sat_f64_s v
| "TruncSat", "I32", "F64", "U" -> wrap_i32_cvtop_f64 I32_convert.trunc_sat_f64_u v
| "Reinterpret", "I32", "F32", "" -> wrap_i32_cvtop_f32 I32_convert.reinterpret_f32 v
(* Conversion to I64 *)
| "Extend", "I64", "I32", "S" -> wrap_i64_cvtop_i32 I64_convert.extend_i32_s v
| "Extend", "I64", "I32", "U" -> wrap_i64_cvtop_i32 I64_convert.extend_i32_u v
| "Trunc", "I64", "F32", "S" -> wrap_i64_cvtop_f32 I64_convert.trunc_f32_s v
| "Trunc", "I64", "F32", "U" -> wrap_i64_cvtop_f32 I64_convert.trunc_f32_u v
| "Trunc", "I64", "F64", "S" -> wrap_i64_cvtop_f64 I64_convert.trunc_f64_s v
| "Trunc", "I64", "F64", "U" -> wrap_i64_cvtop_f64 I64_convert.trunc_f64_u v
| "TruncSat", "I64", "F32", "S" -> wrap_i64_cvtop_f32 I64_convert.trunc_sat_f32_s v
| "TruncSat", "I64", "F32", "U" -> wrap_i64_cvtop_f32 I64_convert.trunc_sat_f32_u v
| "TruncSat", "I64", "F64", "S" -> wrap_i64_cvtop_f64 I64_convert.trunc_sat_f64_s v
| "TruncSat", "I64", "F64", "U" -> wrap_i64_cvtop_f64 I64_convert.trunc_sat_f64_u v
| "Reinterpret", "I64", "F64", "" -> wrap_i64_cvtop_f64 I64_convert.reinterpret_f64 v
(* Conversion to F32 *)
| "Demote", "F32", "F64", "" -> wrap_f32_cvtop_f64 F32_convert.demote_f64 v
| "Convert", "F32", "I32", "S" -> wrap_f32_cvtop_i32 F32_convert.convert_i32_s v
| "Convert", "F32", "I32", "U" -> wrap_f32_cvtop_i32 F32_convert.convert_i32_u v
| "Convert", "F32", "I64", "S" -> wrap_f32_cvtop_i64 F32_convert.convert_i64_s v
| "Convert", "F32", "I64", "U" -> wrap_f32_cvtop_i64 F32_convert.convert_i64_u v
| "Reinterpret", "F32", "I32", "" -> wrap_f32_cvtop_i32 F32_convert.reinterpret_i32 v
(* Conversion to F64 *)
| "Promote", "F64", "F32", "" -> wrap_f64_cvtop_f32 F64_convert.promote_f32 v
| "Convert", "F64", "I32", "S" -> wrap_f64_cvtop_i32 F64_convert.convert_i32_s v
| "Convert", "F64", "I32", "U" -> wrap_f64_cvtop_i32 F64_convert.convert_i32_u v
| "Convert", "F64", "I64", "S" -> wrap_f64_cvtop_i64 F64_convert.convert_i64_s v
| "Convert", "F64", "I64", "U" -> wrap_f64_cvtop_i64 F64_convert.convert_i64_u v
| "Reinterpret", "F64", "I64", "" -> wrap_f64_cvtop_i64 F64_convert.reinterpret_i64 v
| "WRAP", "I32", "I64", "" -> wrap_i32_cvtop_i64 I32_convert.wrap_i64 v
| "TRUNC", "I32", "F32", "S" -> wrap_i32_cvtop_f32 I32_convert.trunc_f32_s v
| "TRUNC", "I32", "F32", "U" -> wrap_i32_cvtop_f32 I32_convert.trunc_f32_u v
| "TRUNC", "I32", "F64", "S" -> wrap_i32_cvtop_f64 I32_convert.trunc_f64_s v
| "TRUNC", "I32", "F64", "U" -> wrap_i32_cvtop_f64 I32_convert.trunc_f64_u v
| "TRUNCSAT", "I32", "F32", "S" -> wrap_i32_cvtop_f32 I32_convert.trunc_sat_f32_s v
| "TRUNCSAT", "I32", "F32", "U" -> wrap_i32_cvtop_f32 I32_convert.trunc_sat_f32_u v
| "TRUNCSAT", "I32", "F64", "S" -> wrap_i32_cvtop_f64 I32_convert.trunc_sat_f64_s v
| "TRUNCSAT", "I32", "F64", "U" -> wrap_i32_cvtop_f64 I32_convert.trunc_sat_f64_u v
| "REINTERPRET", "I32", "F32", "" -> wrap_i32_cvtop_f32 I32_convert.reinterpret_f32 v
(* CONVERSION TO I64 *)
| "EXTEND", "I64", "I32", "S" -> wrap_i64_cvtop_i32 I64_convert.extend_i32_s v
| "EXTEND", "I64", "I32", "U" -> wrap_i64_cvtop_i32 I64_convert.extend_i32_u v
| "TRUNC", "I64", "F32", "S" -> wrap_i64_cvtop_f32 I64_convert.trunc_f32_s v
| "TRUNC", "I64", "F32", "U" -> wrap_i64_cvtop_f32 I64_convert.trunc_f32_u v
| "TRUNC", "I64", "F64", "S" -> wrap_i64_cvtop_f64 I64_convert.trunc_f64_s v
| "TRUNC", "I64", "F64", "U" -> wrap_i64_cvtop_f64 I64_convert.trunc_f64_u v
| "TRUNCSAT", "I64", "F32", "S" -> wrap_i64_cvtop_f32 I64_convert.trunc_sat_f32_s v
| "TRUNCSAT", "I64", "F32", "U" -> wrap_i64_cvtop_f32 I64_convert.trunc_sat_f32_u v
| "TRUNCSAT", "I64", "F64", "S" -> wrap_i64_cvtop_f64 I64_convert.trunc_sat_f64_s v
| "TRUNCSAT", "I64", "F64", "U" -> wrap_i64_cvtop_f64 I64_convert.trunc_sat_f64_u v
| "REINTERPRET", "I64", "F64", "" -> wrap_i64_cvtop_f64 I64_convert.reinterpret_f64 v
(* CONVERSION TO F32 *)
| "DEMOTE", "F32", "F64", "" -> wrap_f32_cvtop_f64 F32_convert.demote_f64 v
| "CONVERT", "F32", "I32", "S" -> wrap_f32_cvtop_i32 F32_convert.convert_i32_s v
| "CONVERT", "F32", "I32", "U" -> wrap_f32_cvtop_i32 F32_convert.convert_i32_u v
| "CONVERT", "F32", "I64", "S" -> wrap_f32_cvtop_i64 F32_convert.convert_i64_s v
| "CONVERT", "F32", "I64", "U" -> wrap_f32_cvtop_i64 F32_convert.convert_i64_u v
| "REINTERPRET", "F32", "I32", "" -> wrap_f32_cvtop_i32 F32_convert.reinterpret_i32 v
(* CONVERSION TO F64 *)
| "PROMOTE", "F64", "F32", "" -> wrap_f64_cvtop_f32 F64_convert.promote_f32 v
| "CONVERT", "F64", "I32", "S" -> wrap_f64_cvtop_i32 F64_convert.convert_i32_s v
| "CONVERT", "F64", "I32", "U" -> wrap_f64_cvtop_i32 F64_convert.convert_i32_u v
| "CONVERT", "F64", "I64", "S" -> wrap_f64_cvtop_i64 F64_convert.convert_i64_s v
| "CONVERT", "F64", "I64", "U" -> wrap_f64_cvtop_i64 F64_convert.convert_i64_u v
| "REINTERPRET", "F64", "I64", "" -> wrap_f64_cvtop_i64 F64_convert.reinterpret_i64 v
| _ -> failwith ("Invalid cvtop: " ^ op ^ t_to ^ t_from ^ sx) ) |]))
| _ -> failwith "Invalid cvtop");
}
Expand Down

0 comments on commit 2ebb9d5

Please sign in to comment.