Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Removing duplicate prose #69

Closed
wants to merge 3 commits into from
Closed

Removing duplicate prose #69

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c13e1e9
Rename algo to prose in splice backend
jaehyun1ee Feb 5, 2024
e3c8ae0
Union instead of concatenating, translated and manual algos
jaehyun1ee Feb 5, 2024
6c1c19f
Prefix validation of reinterpret, convert with cvtop-
jaehyun1ee Feb 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions spectec/spec/wasm-1.0/6-typing.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -223,17 +223,17 @@ rule Instr_ok/relop:
C |- RELOP t relop : t t -> I32


rule Instr_ok/reinterpret:
C |- CVTOP t_1 REINTERPRET t_2 : t_2 -> t_1
-- if t_1 =/= t_2
-- if $size(t_1) = $size(t_2)
rule Instr_ok/cvtop-reinterpret:
C |- CVTOP nt_1 REINTERPRET nt_2 : nt_2 -> nt_1
-- if nt_1 =/= nt_2
-- if $size(nt_1) = $size(nt_2)

rule Instr_ok/convert-i:
rule Instr_ok/cvtop-convert-i:
C |- CVTOP inn_1 CONVERT inn_2 sx? : inn_2 -> inn_1
-- if inn_1 =/= inn_2
-- if sx? = eps <=> $size(inn_1) > $size(inn_2)

rule Instr_ok/convert-f:
rule Instr_ok/cvtop-convert-f:
C |- CVTOP fnn_1 CONVERT fnn_2 : fnn_2 -> fnn_1
-- if fnn_1 =/= fnn_2

Expand Down
6 changes: 3 additions & 3 deletions spectec/spec/wasm-2.0/6-typing.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,17 +273,17 @@ rule Instr_ok/extend:
C |- EXTEND nt n : nt -> nt
-- if n <= $size(nt)

rule Instr_ok/reinterpret:
rule Instr_ok/cvtop-reinterpret:
C |- CVTOP nt_1 REINTERPRET nt_2 : nt_2 -> nt_1
-- if nt_1 =/= nt_2
-- if $size(nt_1) = $size(nt_2)

rule Instr_ok/convert-i:
rule Instr_ok/cvtop-convert-i:
C |- CVTOP inn_1 CONVERT inn_2 sx? : inn_2 -> inn_1
-- if inn_1 =/= inn_2
-- if sx? = eps <=> $size(inn_1) > $size(inn_2)

rule Instr_ok/convert-f:
rule Instr_ok/cvtop-convert-f:
C |- CVTOP fnn_1 CONVERT fnn_2 : fnn_2 -> fnn_1
-- if fnn_1 =/= fnn_2

Expand Down
6 changes: 3 additions & 3 deletions spectec/spec/wasm-3.0/6-typing.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -697,17 +697,17 @@ rule Instr_ok/extend:
C |- EXTEND nt n : nt -> nt
-- if n <= $size(nt)

rule Instr_ok/reinterpret:
rule Instr_ok/cvtop-reinterpret:
C |- CVTOP nt_1 REINTERPRET nt_2 : nt_2 -> nt_1
-- if nt_1 =/= nt_2
-- if $size(nt_1) = $size(nt_2)

rule Instr_ok/convert-i:
rule Instr_ok/cvtop-convert-i:
C |- CVTOP inn_1 CONVERT inn_2 sx? : inn_2 -> inn_1
-- if inn_1 =/= inn_2
-- if sx? = eps <=> $size(inn_1) > $size(inn_2)

rule Instr_ok/convert-f:
rule Instr_ok/cvtop-convert-f:
C |- CVTOP fnn_1 CONVERT fnn_2 : fnn_2 -> fnn_1
-- if fnn_1 =/= fnn_2

Expand Down
24 changes: 12 additions & 12 deletions spectec/src/backend-splice/splice.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,8 @@ type syntax = {sdef : El.Ast.def; sfragments : (string * El.Ast.def * use) list}
type grammar = {gdef : El.Ast.def; gfragments : (string * El.Ast.def * use) list}
type relation = {rdef : El.Ast.def; rules : (string * El.Ast.def * use) list}
type definition = {fdef : El.Ast.def; clauses : El.Ast.def list; use : use}
type relation_prose = {ralgos : (string * Backend_prose.Prose.def * use) list}
type definition_prose = {falgo : Backend_prose.Prose.def; use : use}
type relation_prose = {rprose : (string * Backend_prose.Prose.def * use) list}
type definition_prose = {fprose : Backend_prose.Prose.def; use : use}

type env =
{ elab : Frontend.Elab.env;
Expand Down Expand Up @@ -97,14 +97,14 @@ let env_prose env prose =
match prose with
| Pred ((id, _), _, _) ->
let relation = Map.find valid_id env.rel_prose in
let ralgos = (normalize_id id, prose, ref 0) :: relation.ralgos in
env.rel_prose <- Map.add valid_id {ralgos} env.rel_prose
let rprose = (normalize_id id, prose, ref 0) :: relation.rprose in
env.rel_prose <- Map.add valid_id {rprose} env.rel_prose
| Algo (Al.Ast.RuleA ((id, _), _, _)) ->
let relation = Map.find exec_id env.rel_prose in
let ralgos = (normalize_id id, prose, ref 0) :: relation.ralgos in
env.rel_prose <- Map.add exec_id {ralgos} env.rel_prose
let rprose = (normalize_id id, prose, ref 0) :: relation.rprose in
env.rel_prose <- Map.add exec_id {rprose} env.rel_prose
| Algo (Al.Ast.FuncA (id, _, _)) ->
env.def_prose <- Map.add id {falgo = prose; use = ref 0} env.def_prose
env.def_prose <- Map.add id {fprose = prose; use = ref 0} env.def_prose

let env (config : config) pdsts odsts elab el pr : env =
let latex = Backend_latex.Render.env config.latex el in
Expand All @@ -115,7 +115,7 @@ let env (config : config) pdsts odsts elab el pr : env =
gram = Map.empty;
rel = Map.empty;
def = Map.empty;
rel_prose = Map.(add valid_id {ralgos = []} (add exec_id {ralgos = []} empty));
rel_prose = Map.(add valid_id {rprose = []} (add exec_id {rprose = []} empty));
def_prose = Map.empty;
}
in
Expand Down Expand Up @@ -145,8 +145,8 @@ let warn_math env =
) env.def

let warn_prose env =
Map.iter (fun id1 {ralgos} ->
List.iter (fun (id2, _, use) -> warn_use use "rule prose" id1 id2) ralgos
Map.iter (fun id1 {rprose} ->
List.iter (fun (id2, _, use) -> warn_use use "rule prose" id1 id2) rprose
) env.rel_prose;
Map.iter (fun id1 ({use; _} : definition_prose) ->
warn_use use "definition prose" id1 ""
Expand Down Expand Up @@ -210,13 +210,13 @@ let find_def env src id1 id2 =
let find_rule_prose env src id1 id2 =
match Map.find_opt id1 env.rel_prose with
| None -> error src ("unknown prose relation identifier `" ^ id1 ^ "`")
| Some relation -> find_entry "prose rule" src id1 id2 relation.ralgos
| Some relation -> find_entry "prose rule" src id1 id2 relation.rprose

let find_def_prose env src id1 id2 =
find_nosub "definition" src id1 id2;
match Map.find_opt id1 env.def_prose with
| None -> error src ("unknown prose definition identifier `" ^ id1 ^ "`")
| Some definition -> incr definition.use; definition.falgo
| Some definition -> incr definition.use; definition.fprose


(* Parsing *)
Expand Down
15 changes: 14 additions & 1 deletion spectec/src/exe-watsup/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,20 @@ let () =
let al =
if !target = Check || not (PS.mem Animate !selected_passes) then [] else (
log "Translating to AL...";
(Il2al.Translate.translate il @ Backend_interpreter.Manual.manual_algos)
let get_name = function
| Al.Ast.RuleA ((id, _), _, _) -> id
| Al.Ast.FuncA (id, _, _) -> id
in
let al_manual = Backend_interpreter.Manual.manual_algos in
let names_manual = List.map get_name al_manual in
let al_translated =
List.filter
(fun algo ->
let name_translated = get_name algo in
not (List.mem name_translated names_manual))
(Il2al.Translate.translate il)
in
al_translated @ al_manual
Comment on lines +197 to +210
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This workaround shouldn't be in main. Can you move it to the backend somehow? Also, add a comment explaining why this is needed, and that (supposedly?) it's a TODO to get rid of the workaround eventually.

)
in

Expand Down
6 changes: 3 additions & 3 deletions spectec/test-frontend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2764,19 +2764,19 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= $size(nt <: valtype))

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([(nt_2 <: valtype)], [(nt_1 <: valtype)]))
-- if (nt_1 =/= nt_2)
-- if ($size(nt_1 <: valtype) = $size(nt_2 <: valtype))

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
`%|-%:%`(C, CVTOP_instr((inn_1 <: numtype), CONVERT_cvtop, (inn_2 <: numtype), sx?{sx}), `%->%`([(inn_2 <: valtype)], [(inn_1 <: valtype)]))
-- if (inn_1 =/= inn_2)
-- if ((sx?{sx} = ?()) <=> ($size(inn_1 <: valtype) > $size(inn_2 <: valtype)))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr((fnn_1 <: numtype), CONVERT_cvtop, (fnn_2 <: numtype), ?()), `%->%`([(fnn_2 <: valtype)], [(fnn_1 <: valtype)]))
-- if (fnn_1 =/= fnn_2)

Expand Down
6 changes: 3 additions & 3 deletions spectec/test-latex/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3030,7 +3030,7 @@ $$
{|{\mathit{nt}}_{{1}}|} = {|{\mathit{nt}}_{{2}}|}
}{
{\mathit{C}} \vdash \mathsf{cvtop}~{\mathit{nt}}_{{1}}~\mathsf{reinterpret}~{\mathit{nt}}_{{2}} : {\mathit{nt}}_{{2}} \rightarrow {\mathit{nt}}_{{1}}
} \, {[\textsc{\scriptsize T{-}reinterpret}]}
} \, {[\textsc{\scriptsize T{-}cvtop{-}reinterpret}]}
\qquad
\end{array}
$$
Expand All @@ -3043,7 +3043,7 @@ $$
{{\mathit{sx}}^?} = \epsilon \Leftrightarrow {|{{\mathsf{i}}{{\mathit{n}}}}_{{1}}|} > {|{{\mathsf{i}}{{\mathit{n}}}}_{{2}}|}
}{
{\mathit{C}} \vdash {{\mathsf{i}}{{\mathit{n}}}}_{{1}} . {{{{\mathsf{convert}}{\mathsf{\_}}}{{{\mathsf{i}}{{\mathit{n}}}}_{{2}}}}{\mathsf{\_}}}{{{\mathit{sx}}^?}} : {{\mathsf{i}}{{\mathit{n}}}}_{{2}} \rightarrow {{\mathsf{i}}{{\mathit{n}}}}_{{1}}
} \, {[\textsc{\scriptsize T{-}convert{-}i}]}
} \, {[\textsc{\scriptsize T{-}cvtop{-}convert{-}i}]}
\qquad
\end{array}
$$
Expand All @@ -3054,7 +3054,7 @@ $$
{{\mathsf{f}}{{\mathit{n}}}}_{{1}} \neq {{\mathsf{f}}{{\mathit{n}}}}_{{2}}
}{
{\mathit{C}} \vdash \mathsf{cvtop}~{{\mathsf{f}}{{\mathit{n}}}}_{{1}}~\mathsf{convert}~{{\mathsf{f}}{{\mathit{n}}}}_{{2}} : {{\mathsf{f}}{{\mathit{n}}}}_{{2}} \rightarrow {{\mathsf{f}}{{\mathit{n}}}}_{{1}}
} \, {[\textsc{\scriptsize T{-}convert{-}f}]}
} \, {[\textsc{\scriptsize T{-}cvtop{-}convert{-}f}]}
\qquad
\end{array}
$$
Expand Down
42 changes: 21 additions & 21 deletions spectec/test-middlend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2627,19 +2627,19 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= $size(nt <: valtype))

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([(nt_2 <: valtype)], [(nt_1 <: valtype)]))
-- if (nt_1 =/= nt_2)
-- if ($size(nt_1 <: valtype) = $size(nt_2 <: valtype))

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
`%|-%:%`(C, CVTOP_instr((inn_1 <: numtype), CONVERT_cvtop, (inn_2 <: numtype), sx?{sx}), `%->%`([(inn_2 <: valtype)], [(inn_1 <: valtype)]))
-- if (inn_1 =/= inn_2)
-- if ((sx?{sx} = ?()) <=> ($size(inn_1 <: valtype) > $size(inn_2 <: valtype)))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr((fnn_1 <: numtype), CONVERT_cvtop, (fnn_2 <: numtype), ?()), `%->%`([(fnn_2 <: valtype)], [(fnn_1 <: valtype)]))
-- if (fnn_1 =/= fnn_2)

Expand Down Expand Up @@ -7551,19 +7551,19 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= $size($valtype_numtype(nt)))

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([$valtype_numtype(nt_2)], [$valtype_numtype(nt_1)]))
-- if (nt_1 =/= nt_2)
-- if ($size($valtype_numtype(nt_1)) = $size($valtype_numtype(nt_2)))

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
`%|-%:%`(C, CVTOP_instr($numtype_inn(inn_1), CONVERT_cvtop, $numtype_inn(inn_2), sx?{sx}), `%->%`([$valtype_inn(inn_2)], [$valtype_inn(inn_1)]))
-- if (inn_1 =/= inn_2)
-- if ((sx?{sx} = ?()) <=> ($size($valtype_inn(inn_1)) > $size($valtype_inn(inn_2))))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr($numtype_fnn(fnn_1), CONVERT_cvtop, $numtype_fnn(fnn_2), ?()), `%->%`([$valtype_fnn(fnn_2)], [$valtype_fnn(fnn_1)]))
-- if (fnn_1 =/= fnn_2)

Expand Down Expand Up @@ -12478,19 +12478,19 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= !($size($valtype_numtype(nt))))

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([$valtype_numtype(nt_2)], [$valtype_numtype(nt_1)]))
-- if (nt_1 =/= nt_2)
-- if (!($size($valtype_numtype(nt_1))) = !($size($valtype_numtype(nt_2))))

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?}:
`%|-%:%`(C, CVTOP_instr($numtype_inn(inn_1), CONVERT_cvtop, $numtype_inn(inn_2), sx?{sx}), `%->%`([$valtype_inn(inn_2)], [$valtype_inn(inn_1)]))
-- if (inn_1 =/= inn_2)
-- if ((sx?{sx} = ?()) <=> (!($size($valtype_inn(inn_1))) > !($size($valtype_inn(inn_2)))))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr($numtype_fnn(fnn_1), CONVERT_cvtop, $numtype_fnn(fnn_2), ?()), `%->%`([$valtype_fnn(fnn_2)], [$valtype_fnn(fnn_1)]))
-- if (fnn_1 =/= fnn_2)

Expand Down Expand Up @@ -17406,23 +17406,23 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= o0)

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([$valtype_numtype(nt_2)], [$valtype_numtype(nt_1)]))
-- if ($size($valtype_numtype(nt_1)) = ?(o0))
-- if ($size($valtype_numtype(nt_2)) = ?(o1))
-- if (nt_1 =/= nt_2)
-- if (o0 = o1)

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr($numtype_inn(inn_1), CONVERT_cvtop, $numtype_inn(inn_2), sx?{sx}), `%->%`([$valtype_inn(inn_2)], [$valtype_inn(inn_1)]))
-- if ($size($valtype_inn(inn_1)) = ?(o0))
-- if ($size($valtype_inn(inn_2)) = ?(o1))
-- if (inn_1 =/= inn_2)
-- if ((sx?{sx} = ?()) <=> (o0 > o1))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr($numtype_fnn(fnn_1), CONVERT_cvtop, $numtype_fnn(fnn_2), ?()), `%->%`([$valtype_fnn(fnn_2)], [$valtype_fnn(fnn_1)]))
-- if (fnn_1 =/= fnn_2)

Expand Down Expand Up @@ -22358,23 +22358,23 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= o0)

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([$valtype_numtype(nt_2)], [$valtype_numtype(nt_1)]))
-- if ($size($valtype_numtype(nt_1)) = ?(o0))
-- if ($size($valtype_numtype(nt_2)) = ?(o1))
-- if (nt_1 =/= nt_2)
-- if (o0 = o1)

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr($numtype_inn(inn_1), CONVERT_cvtop, $numtype_inn(inn_2), sx?{sx}), `%->%`([$valtype_inn(inn_2)], [$valtype_inn(inn_1)]))
-- if ($size($valtype_inn(inn_1)) = ?(o0))
-- if ($size($valtype_inn(inn_2)) = ?(o1))
-- if (inn_1 =/= inn_2)
-- if ((sx?{sx} = ?()) <=> (o0 > o1))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr($numtype_fnn(fnn_1), CONVERT_cvtop, $numtype_fnn(fnn_2), ?()), `%->%`([$valtype_fnn(fnn_2)], [$valtype_fnn(fnn_1)]))
-- if (fnn_1 =/= fnn_2)

Expand Down Expand Up @@ -27343,23 +27343,23 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= o0)

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([$valtype_numtype(nt_2)], [$valtype_numtype(nt_1)]))
-- if ($size($valtype_numtype(nt_1)) = ?(o0))
-- if ($size($valtype_numtype(nt_2)) = ?(o1))
-- if (nt_1 =/= nt_2)
-- if (o0 = o1)

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr($numtype_inn(inn_1), CONVERT_cvtop, $numtype_inn(inn_2), sx?{sx}), `%->%`([$valtype_inn(inn_2)], [$valtype_inn(inn_1)]))
-- if ($size($valtype_inn(inn_1)) = ?(o0))
-- if ($size($valtype_inn(inn_2)) = ?(o1))
-- if (inn_1 =/= inn_2)
-- if ((sx?{sx} = ?()) <=> (o0 > o1))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr($numtype_fnn(fnn_1), CONVERT_cvtop, $numtype_fnn(fnn_2), ?()), `%->%`([$valtype_fnn(fnn_2)], [$valtype_fnn(fnn_1)]))
-- if (fnn_1 =/= fnn_2)

Expand Down Expand Up @@ -32457,23 +32457,23 @@ relation Instr_ok: `%|-%:%`(context, instr, functype)
-- if (n <= o0)

;; 6-typing.watsup:700.1-703.34
rule reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
rule cvtop-reinterpret {C : context, nt_1 : numtype, nt_2 : numtype, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr(nt_1, REINTERPRET_cvtop, nt_2, ?()), `%->%`([$valtype_numtype(nt_2)], [$valtype_numtype(nt_1)]))
-- if (nt_1 =/= nt_2)
-- where ?(o1) = $size($valtype_numtype(nt_2))
-- where o0 = o1
-- if ($size($valtype_numtype(nt_1)) = ?(o0))

;; 6-typing.watsup:705.1-708.50
rule convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
rule cvtop-convert-i {C : context, inn_1 : inn, inn_2 : inn, sx? : sx?, o0 : nat, o1 : nat}:
`%|-%:%`(C, CVTOP_instr($numtype_inn(inn_1), CONVERT_cvtop, $numtype_inn(inn_2), sx?{sx}), `%->%`([$valtype_inn(inn_2)], [$valtype_inn(inn_1)]))
-- if (inn_1 =/= inn_2)
-- where ?(o0) = $size($valtype_inn(inn_1))
-- where ?(o1) = $size($valtype_inn(inn_2))
-- if ((sx?{sx} = ?()) <=> (o0 > o1))

;; 6-typing.watsup:710.1-712.24
rule convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
rule cvtop-convert-f {C : context, fnn_1 : fnn, fnn_2 : fnn}:
`%|-%:%`(C, CVTOP_instr($numtype_fnn(fnn_1), CONVERT_cvtop, $numtype_fnn(fnn_2), ?()), `%->%`([$valtype_fnn(fnn_2)], [$valtype_fnn(fnn_1)]))
-- if (fnn_1 =/= fnn_2)

Expand Down
Loading
Loading