%{^
#include "ats_counter.cats" /* only needed for [ATS/Geizella] */
#include "ats_solver_fm.cats"
%}
staload Deb = "ats_debug.sats"
staload Err = "ats_error.sats"
staload IntInf = "ats_intinf.sats"
staload Lst = "ats_list.sats"
staload "ats_staexp2.sats"
staload "ats_stadyncst2.sats"
staload "ats_patcst2.sats"
staload "ats_dynexp2.sats"
staload "ats_trans3_env.sats"
staload "ats_solver_fm.sats"
staload "ats_constraint.sats"
overload ~ with $IntInf.neg_intinf
overload + with $IntInf.add_intinf_intinf
overload - with $IntInf.sub_intinf_intinf
overload * with $IntInf.mul_intinf_intinf
overload < with $IntInf.lt_intinf_int
overload <= with $IntInf.lte_intinf_int
overload > with $IntInf.gt_intinf_int
overload >= with $IntInf.gte_intinf_int
overload = with $IntInf.eq_intinf_int
overload <> with $IntInf.neq_intinf_int
fn prerr_interror () = prerr "INTERNAL ERROR (ats_constraint)"
fn prerr_loc_interror (loc: loc_t) = begin
$Loc.prerr_location loc; prerr ": INTERNAL ERROR (ats_constraint)"
end
implement s3aexp_null = S3AEnull ()
implement s3aexp_cst (s2c) = S3AEcst (s2c)
implement s3aexp_var (s2v) = S3AEvar (s2v)
implement
s3aexp_padd (s3ae1, s3ie2) = begin
case+ s3ae1 of
| S3AEpadd (s3ae11, s3ie12) => begin
s3aexp_padd (s3ae11, s3iexp_iadd (s3ie12, s3ie2))
end | _ => S3AEpadd (s3ae1, s3ie2)
end
implement
s3aexp_psub (s3ae1, s3ie2) = begin
case+ s3ae1 of
| S3AEpadd (s3ae11, s3ie12) => begin
s3aexp_padd (s3ae11, s3iexp_isub (s3ie12, s3ie2))
end | _ => S3AEpadd (s3ae1, s3iexp_ineg s3ie2)
end
implement s3aexp_psucc (s3ae) = s3aexp_padd (s3ae, s3iexp_1)
implement s3aexp_ppred (s3ae) = s3aexp_psub (s3ae, s3iexp_1)
implement s3bexp_true = S3BEbool (true)
implement s3bexp_false = S3BEbool (false)
implement s3bexp_cst (s2c) = S3BEcst (s2c)
implement s3bexp_var (s2v) = S3BEvar (s2v)
implement
s3bexp_bneg (s3be0) = case+ s3be0 of
| S3BEbool b => S3BEbool (not b)
| S3BEbadd (s3be1, s3be2) => S3BEbmul (S3BEbneg s3be1, S3BEbneg s3be2)
| S3BEbmul (s3be1, s3be2) => S3BEbadd (S3BEbneg s3be1, S3BEbneg s3be2)
| S3BEbneg s3be => s3be
| S3BEiexp (knd, s3ie) => S3BEiexp (~knd, s3ie)
| _ => S3BEbneg s3be0
implement
s3bexp_beq (s3be1, s3be2) = begin case+ s3be1 of
| S3BEbool b1 => if b1 then s3be2 else s3bexp_bneg s3be2
| _ => begin case+ s3be2 of
| S3BEbool b2 => if b2 then s3be1 else s3bexp_bneg s3be1
| _ => let
val _s3be1 = s3bexp_bneg s3be1 and _s3be2 = s3bexp_bneg s3be2
in
S3BEbadd (S3BEbmul (s3be1, s3be2), S3BEbmul (_s3be1, _s3be2))
end end end
implement
s3bexp_bneq (s3be1, s3be2) = begin case+ s3be1 of
| S3BEbool b1 => if b1 then s3bexp_bneg s3be2 else s3be2
| _ => begin case+ s3be2 of
| S3BEbool b2 => if b2 then s3bexp_bneg s3be1 else s3be1
| _ => let
val _s3be1 = s3bexp_bneg s3be1 and _s3be2 = s3bexp_bneg s3be2
in
S3BEbadd (S3BEbmul (s3be1, _s3be2), S3BEbmul (_s3be1, s3be2))
end end end
implement
s3bexp_badd (s3be1, s3be2) = begin
case+ s3be1 of
| S3BEbool b1 => if b1 then s3bexp_true else s3be2
| _ => begin case+ s3be2 of
| S3BEbool b2 => if b2 then s3bexp_true else s3be1
| _ => S3BEbadd (s3be1, s3be2)
end end
implement
s3bexp_bmul (s3be1, s3be2) = begin
case+ s3be1 of
| S3BEbool b1 => if b1 then s3be2 else s3bexp_false
| _ => begin case+ s3be2 of
| S3BEbool b2 => if b2 then s3be1 else s3bexp_false
| _ => S3BEbmul (s3be1, s3be2)
end end
implement
s3bexp_iexp (knd, s3ie) = begin case+ s3ie of
| S3IEint i => begin case+ knd of
| 2 => if i >= 0 then s3bexp_true else s3bexp_false
| 1 => if i = 0 then s3bexp_true else s3bexp_false
| ~1 => if i <> 0 then s3bexp_true else s3bexp_false
| ~2 => if i < 0 then s3bexp_true else s3bexp_false
| _ => begin
prerr_interror ();
prerr ": s3bexp_iexp: knd = "; prerr knd; prerr_newline ();
$Err.abort {s3bexp} ()
end end | S3IEintinf i => begin case+ knd of
| 2 => if i >= 0 then s3bexp_true else s3bexp_false
| 1 => if i = 0 then s3bexp_true else s3bexp_false
| ~1 => if i <> 0 then s3bexp_true else s3bexp_false
| ~2 => if i < 0 then s3bexp_true else s3bexp_false
| _ => begin
prerr_interror ();
prerr ": s3bexp_iexp: knd = "; prerr knd; prerr_newline ();
$Err.abort {s3bexp} ()
end end | _ => S3BEiexp (knd, s3ie)
end
implement s3bexp_igt (s3ie1, s3ie2) =
s3bexp_iexp (~2, s3iexp_isub (s3ie2, s3ie1))
implement s3bexp_igte (s3ie1, s3ie2) =
s3bexp_iexp (2, s3iexp_isub (s3ie1, s3ie2))
implement s3bexp_ilt (s3ie1, s3ie2) =
s3bexp_iexp (~2, s3iexp_isub (s3ie1, s3ie2))
implement s3bexp_ilte (s3ie1, s3ie2) =
s3bexp_iexp (2, s3iexp_isub (s3ie2, s3ie1))
implement s3bexp_ieq (s3ie1, s3ie2) =
s3bexp_iexp (1, s3iexp_isub (s3ie1, s3ie2))
implement s3bexp_ineq (s3ie1, s3ie2) =
s3bexp_iexp (~1, s3iexp_isub (s3ie1, s3ie2))
implement s3bexp_pgt (s3ae1, s3ae2) =
s3bexp_iexp (~2, s3iexp_pdiff (s3ae2, s3ae1))
implement s3bexp_pgte (s3ae1, s3ae2) =
s3bexp_iexp (2, s3iexp_pdiff (s3ae1, s3ae2))
implement s3bexp_plt (s3ae1, s3ae2) =
s3bexp_iexp (~2, s3iexp_pdiff (s3ae1, s3ae2))
implement s3bexp_plte (s3ae1, s3ae2) =
s3bexp_iexp (2, s3iexp_pdiff (s3ae2, s3ae1))
implement s3bexp_peq (s3ae1, s3ae2) =
s3bexp_iexp (1, s3iexp_pdiff (s3ae1, s3ae2))
implement s3bexp_pneq (s3ae1, s3ae2) =
s3bexp_iexp (~1, s3iexp_pdiff (s3ae1, s3ae2))
fn s3iexp_is_const (s3ie: s3iexp): bool = begin
case+ s3ie of S3IEint _ => true | S3IEintinf _ => true | _ => false
end
implement s3iexp_0 = S3IEint 0
implement s3iexp_1 = S3IEint 1
implement s3iexp_neg_1 = S3IEint (~1)
implement s3iexp_cst (s2c) = S3IEcst s2c
implement s3iexp_int (i) = S3IEint i
implement s3iexp_intinf (i) = S3IEintinf i
implement s3iexp_var (s2v) = S3IEvar s2v
implement
s3iexp_ineg (s3ie) = begin
case+ s3ie of
| S3IEint i => S3IEint (~i)
| S3IEintinf i => S3IEintinf (~i)
| S3IEineg s3ie => s3ie
| _ => S3IEineg s3ie end
implement
s3iexp_iadd (s3ie1, s3ie2) = begin
case+ (s3ie1, s3ie2) of
| (S3IEint i, _) when i = 0 => s3ie2
| (_, S3IEint i) when i = 0 => s3ie1
| (S3IEintinf i, _) when i = 0 => s3ie2
| (_, S3IEintinf i) when i = 0 => s3ie1
| (S3IEintinf i1, S3IEintinf i2) => S3IEintinf (i1 + i2)
| (_, _) => S3IEiadd (s3ie1, s3ie2)
end
implement
s3iexp_isub (s3ie1, s3ie2) = begin
case+ (s3ie1, s3ie2) of
| (S3IEint i, _) when i = 0 => s3iexp_ineg s3ie2
| (_, S3IEint i) when i = 0 => s3ie1
| (S3IEintinf i, _) when i = 0 => s3iexp_ineg s3ie2
| (_, S3IEintinf i) when i = 0 => s3ie1
| (S3IEintinf i1, S3IEintinf i2) => S3IEintinf (i1 - i2)
| (_, _) => S3IEisub (s3ie1, s3ie2)
end
implement
s3iexp_imul (s3ie1, s3ie2) = begin
case+ (s3ie1, s3ie2) of
| (S3IEint i, _) when i = 0 => s3ie1 | (S3IEint i, _) when i = 1 => s3ie2
| (_, S3IEint i) when i = 0 => s3ie2 | (_, S3IEint i) when i = 1 => s3ie1
| (S3IEintinf i, _) when i = 0 => s3ie1 | (S3IEintinf i, _) when i = 1 => s3ie2
| (_, S3IEintinf i) when i = 0 => s3ie2 | (_, S3IEintinf i) when i = 1 => s3ie1
| (S3IEintinf i1, S3IEintinf i2) => S3IEintinf (i1 * i2)
| (_, _) => S3IEimul (s3ie1, s3ie2)
end
implement s3iexp_pdiff (s3ae1, s3ae2) = S3IEpdiff (s3ae1, s3ae2)
implement s3iexp_isucc (s3ie: s3iexp): s3iexp = s3iexp_iadd (s3ie, s3iexp_1)
implement s3iexp_ipred (s3ie: s3iexp): s3iexp = s3iexp_isub (s3ie, s3iexp_1)
fun s2cfdeflst_free
(fds: s2cfdeflst_vt): void = begin
case+ fds of
| ~S2CFDEFLSTcons (_, _, _, os3be, fds) => let
val () = case+ os3be of ~Some_vt _ => () | ~None_vt () => ()
in
s2cfdeflst_free (fds)
end | ~S2CFDEFLSTmark (fds) => s2cfdeflst_free (fds)
| ~S2CFDEFLSTnil () => ()
end
fn s2cfdeflst_pop
(fds0: &s2cfdeflst_vt): void = let
fun aux (fds: s2cfdeflst_vt): s2cfdeflst_vt = case+ fds of
| ~S2CFDEFLSTcons (s2c, s2es, s2v, os3be, fds) => let
val () = case+ os3be of ~Some_vt _ => () | ~None_vt () => ()
in
aux (fds)
end
| ~S2CFDEFLSTmark (fds) => fds
| ~S2CFDEFLSTnil () => S2CFDEFLSTnil ()
in
fds0 := aux (fds0)
end
fn s2cfdeflst_push (fds0: &s2cfdeflst_vt): void = begin
fds0 := S2CFDEFLSTmark (fds0)
end
fun s2cfdeflst_find
(fds0: &s2cfdeflst_vt, s2c0: s2cst_t, s2es0: s2explst)
: Option_vt s2var_t = begin case+ fds0 of
| S2CFDEFLSTcons (s2c, s2es, s2v, _, !fds) => let
val cond = (
if eq_s2cst_s2cst (s2c0, s2c) then s2explst_syneq (s2es, s2es0) else false
) : bool
in
if cond then begin
fold@ fds0; Some_vt s2v
end else let
val ans = s2cfdeflst_find (!fds, s2c0, s2es0)
in
fold@ fds0; ans
end
end | S2CFDEFLSTmark (!fds) => let
val ans = s2cfdeflst_find (!fds, s2c0, s2es0)
in
fold@ fds0; ans
end | S2CFDEFLSTnil () => begin
fold@ fds0; None_vt ()
end end
fn s2cfdeflst_add
(s2c: s2cst_t, s2es: s2explst, s2v: s2var_t,
s2cs: &s2cstlst, fds: &s2cfdeflst_vt): void = let
val s2e_s2c = s2exp_cst s2c
val s2e_s2v = s2exp_var s2v
val s2es_arg = $Lst.list_extend (s2es, s2e_s2v)
val s2e_rel = s2exp_app_srt (s2rt_bool, s2e_s2c, s2es_arg)
val os3be = s3bexp_make_s2exp (s2e_rel, s2cs, fds)
in
fds := S2CFDEFLSTcons (s2c, s2es, s2v, os3be, fds)
end
fn s2cfdeflst_add_none
(s2c: s2cst_t, s2es: s2explst, s2v: s2var_t,
s2cs: &s2cstlst, fds: &s2cfdeflst_vt): void = let
in
fds := S2CFDEFLSTcons (s2c, s2es, s2v, None_vt (), fds)
end
fn s2cfdeflst_replace (
s2t: s2rt
, s2c: s2cst_t, s2es: s2explst
, s2cs: &s2cstlst, fds: &s2cfdeflst_vt
) : s2var_t =
case+ s2cfdeflst_find (fds, s2c, s2es) of
| ~None_vt () => let
val s2v = s2var_make_srt (s2t)
val () = s2cfdeflst_add (s2c, s2es, s2v, s2cs, fds)
in
s2v
end | ~Some_vt s2v => s2v
fn s2cfdeflst_replace_none (
s2t: s2rt
, s2c: s2cst_t, s2es: s2explst
, s2cs: &s2cstlst, fds: &s2cfdeflst_vt
) : s2var_t =
case+ s2cfdeflst_find (fds, s2c, s2es) of
| ~None_vt () => let
val s2v = s2var_make_srt (s2t)
val () = s2cfdeflst_add_none (s2c, s2es, s2v, s2cs, fds)
in
s2v
end | ~Some_vt s2v => s2v
extern
fun s3aexp_make_s2cst_s2explst
(s2c: s2cst_t, s2es: s2explst, s2cs: &s2cstlst, fds: &s2cfdeflst_vt)
: s3aexpopt_vt
implement
s3aexp_make_s2cst_s2explst
(s2c, s2es, s2cs, fds) = let
fn errmsg (s2c: s2cst_t): s3aexpopt_vt = begin
prerr_interror ();
prerr ": s3aexp_make_s2cst_s2explst: s2c = "; prerr s2c; prerr_newline ();
$Err.abort {s3aexpopt_vt} ()
end in
case+ 0 of | _ when s2cstref_cst_equ (Add_addr_int_addr, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3aexp_padd (s3ae1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Sub_addr_int_addr, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3aexp_psub (s3ae1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ => let
val s2v = s2cfdeflst_replace_none (s2rt_addr, s2c, s2es, s2cs, fds)
in
Some_vt (s3aexp_var s2v)
end
end
extern
fun s3bexp_make_s2cst_s2explst
(s2c: s2cst_t, s2es: s2explst, s2cs: &s2cstlst, fds: &s2cfdeflst_vt)
: s3bexpopt_vt
implement
s3bexp_make_s2cst_s2explst
(s2c, s2es, s2cs, fds) = let
fn errmsg (s2c: s2cst_t): s3bexpopt_vt = begin
prerr_interror ();
prerr ": s3bexp_make_s2cst_s2explst: s2c = "; prerr s2c; prerr_newline ();
$Err.abort {s3bexpopt_vt} ()
end in
case+ 0 of
| _ when s2cstref_cst_equ (Neg_bool_bool, s2c) => begin
case+ s2es of
| list_cons (s2e, list_nil ()) => begin
case+ s3bexp_make_s2exp (s2e, s2cs, fds) of
| ~Some_vt s3be => Some_vt (s3bexp_bneg s3be) | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Add_bool_bool_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3bexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3be1 => begin
case+ s3bexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3be2 => Some_vt (s3bexp_badd (s3be1, s3be2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Mul_bool_bool_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3bexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3be1 => begin
case+ s3bexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3be2 => Some_vt (s3bexp_bmul (s3be1, s3be2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Eq_bool_bool_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3bexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3be1 => begin
case+ s3bexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3be2 => Some_vt (s3bexp_beq (s3be1, s3be2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Neq_bool_bool_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3bexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3be1 => begin
case+ s3bexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3be2 => Some_vt (s3bexp_bneq (s3be1, s3be2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Gt_char_char_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_igt (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Gte_char_char_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_igte (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Lt_char_char_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ilt (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Lte_char_char_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ilte (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Eq_char_char_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ieq (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Neq_char_char_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ineq (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Gt_int_int_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_igt (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Gte_int_int_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_igte (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Lt_int_int_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ilt (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Lte_int_int_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ilte (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Eq_int_int_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ieq (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Neq_int_int_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ineq (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Gt_addr_addr_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3bexp_pgt (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Gte_addr_addr_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3bexp_pgte (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Lt_addr_addr_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3bexp_plt (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Lte_addr_addr_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3bexp_plte (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Eq_addr_addr_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3bexp_peq (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Neq_addr_addr_bool, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3bexp_pneq (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Lte_cls_cls_bool, s2c) => begin
case+ s2es of
| list_cons (
s2e1, list_cons (s2e2, list_nil ())
) => let
val sgn = s2exp_subclass_test (s2e1, s2e2) in
case+ 0 of
| _ when sgn > 0 => Some_vt s3bexp_true
| _ when sgn < 0 => Some_vt s3bexp_false
| _ => let
val s2v = s2cfdeflst_replace_none (s2rt_bool, s2c, s2es, s2cs, fds)
in
Some_vt (s3bexp_var s2v)
end
end | _ => errmsg s2c
end | _ => let
val s2v = s2cfdeflst_replace_none (s2rt_bool, s2c, s2es, s2cs, fds)
in
Some_vt (s3bexp_var s2v)
end
end
extern
fun s3iexp_make_s2cst_s2explst
(s2c: s2cst_t, s2es: s2explst, s2cs: &s2cstlst, fds: &s2cfdeflst_vt)
: s3iexpopt_vt
implement
s3iexp_make_s2cst_s2explst
(s2c, s2es, s2cs, fds) = let
fn errmsg (s2c: s2cst_t): s3iexpopt_vt = begin
prerr_interror ();
prerr ": s3iexp_make_s2cst_s2explst: s2c = "; prerr s2c; prerr_newline ();
$Err.abort {s3iexpopt_vt} ()
end in
case+ 0 of
| _ when s2cstref_cst_equ (Neg_int_int, s2c) => begin
case+ s2es of
| list_cons (s2e, list_nil ()) => begin
case+ s3iexp_make_s2exp (s2e, s2cs, fds) of
| ~Some_vt s3ie => Some_vt (s3iexp_ineg s3ie) | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Add_int_int_int, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3iexp_iadd (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Sub_int_int_int, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3iexp_isub (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Mul_int_int_int, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => let
val islin = s3iexp_is_const s3ie1
in
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => let
val islin = islin orelse (s3iexp_is_const s3ie2)
in
if islin then
Some_vt (s3iexp_imul (s3ie1, s3ie2)) else let val s2v = s2cfdeflst_replace_none (s2rt_int, s2c, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end end | ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Sub_addr_addr_int, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3iexp_pdiff (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Sub_char_char_int, s2c) => begin
case+ s2es of
| list_cons (s2e1, list_cons (s2e2, list_nil ())) => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3iexp_isub (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => errmsg s2c
end | _ when s2cstref_cst_equ (Div_int_int_int, s2c) => let
val s2c_rel = s2cstref_cst_get (Div_int_int_int_bool)
val s2v = s2cfdeflst_replace (s2rt_int, s2c_rel, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end
| _ when s2cstref_cst_equ (Abs_int_int, s2c) => let
val s2c_rel = s2cstref_cst_get (Abs_int_int_bool)
val s2v = s2cfdeflst_replace (s2rt_int, s2c_rel, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end
| _ when s2cstref_cst_equ (Max_int_int_int, s2c) => let
val s2c_rel = s2cstref_cst_get (Max_int_int_int_bool)
val s2v = s2cfdeflst_replace (s2rt_int, s2c_rel, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end
| _ when s2cstref_cst_equ (Min_int_int_int, s2c) => let
val s2c_rel = s2cstref_cst_get (Min_int_int_int_bool)
val s2v = s2cfdeflst_replace (s2rt_int, s2c_rel, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end
| _ when s2cstref_cst_equ (Nsub_int_int_int, s2c) => let
val s2c_rel = s2cstref_cst_get (Nsub_int_int_int_bool)
val s2v = s2cfdeflst_replace (s2rt_int, s2c_rel, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end | _ when s2cstref_cst_equ (IntOfBool_bool_int, s2c) => let
val s2c_rel = s2cstref_cst_get (IntOfBool_bool_int_bool)
val s2v = s2cfdeflst_replace (s2rt_int, s2c_rel, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end | _ => let
val s2v = s2cfdeflst_replace_none (s2rt_int, s2c, s2es, s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end
end
local
fn aux_equal
(s2e1: s2exp, s2e2: s2exp, s2cs: &s2cstlst, fds: &s2cfdeflst_vt)
: s3bexpopt_vt = let
val s2t1 = s2e1.s2exp_srt
in
case+ 0 of | _ when s2t1 = s2rt_int => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ieq (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ when s2t1 = s2rt_addr => begin
case+ s3aexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ae1 => begin
case+ s3aexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ae2 => Some_vt (s3bexp_peq (s3ae1, s3ae2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ when s2t1 = s2rt_bool => begin
case+ s3bexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3be1 => begin
case+ s3bexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3be2 => Some_vt (s3bexp_beq (s3be1, s3be2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ when s2t1 = s2rt_char => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ieq (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ when s2rt_is_dat s2t1 => begin
case+ s3iexp_make_s2exp (s2e1, s2cs, fds) of
| ~Some_vt s3ie1 => begin
case+ s3iexp_make_s2exp (s2e2, s2cs, fds) of
| ~Some_vt s3ie2 => Some_vt (s3bexp_ieq (s3ie1, s3ie2))
| ~None_vt () => None_vt ()
end | ~None_vt () => None_vt ()
end | _ => begin
if s2exp_syneq (s2e1, s2e2) then Some_vt (s3bexp_true) else None_vt ()
end end
fn aux_bind
(loc: loc_t, s2v1: s2var_t, s2e2: s2exp, s2cs: &s2cstlst, fds: &s2cfdeflst_vt)
: s3bexpopt_vt = let
val os3be = aux_equal (s2exp_var s2v1, s2e2, s2cs, fds)
val () = trans3_env_hypo_add_bind (loc, s2v1, s2e2)
in
os3be
end
in
fun s2cstlst_add (s2cs: s2cstlst, s2c0: s2cst_t): s2cstlst = let
fun aux (s2cs: s2cstlst, s2c0: s2cst_t): bool = begin
case+ s2cs of
| S2CSTLSTcons (s2c, s2cs) =>
if eq_s2cst_s2cst (s2c0, s2c) then true else aux (s2cs, s2c0)
| S2CSTLSTnil () => false
end in
if aux (s2cs, s2c0) then s2cs else S2CSTLSTcons (s2c0, s2cs)
end
implement
s3aexp_make_s2exp
(s2e0, s2cs, fds) = let
val s2e0 = s2exp_whnf s2e0
in
case+ s2e0.s2exp_node of
| S2Eapp (s2e1, s2es2) => begin case+ s2e1.s2exp_node of
| S2Ecst s2c1 => s3aexp_make_s2cst_s2explst (s2c1, s2es2, s2cs, fds)
| _ => None_vt ()
end | S2Ecst s2c => begin case+ s2c of
| _ when s2cstref_cst_equ (Null_addr, s2c) => Some_vt (s3aexp_null)
| _ => (s2cs := s2cstlst_add (s2cs, s2c); Some_vt (s3aexp_cst s2c))
end | S2Evar s2v => Some_vt (s3aexp_var s2v)
| _ => let val () = begin
prerr "warning(3): s3aexp_make_s2exp: s2e0 = "; prerr s2e0; prerr_newline ();
end in
None_vt ()
end end
fun s2exp_synlt (s2e1: s2exp, s2e2: s2exp): bool = let
val s2e2 = s2exp_whnf s2e2
in
case+ s2e2.s2exp_node of
| S2Eapp (_, s2es2) => s2explst_synlte (s2e1, s2es2)
| _ => false
end
and s2exp_synlte (s2e1: s2exp, s2e2: s2exp): bool =
s2exp_syneq (s2e1, s2e2) orelse s2exp_synlt (s2e1, s2e2)
and s2explst_synlte
(s2e1: s2exp, s2es2: s2explst): bool = begin
case+ s2es2 of
| list_cons (s2e2, s2es2) => begin
s2exp_synlte (s2e1, s2e2) orelse s2explst_synlte (s2e1, s2es2)
end
| list_nil () => false
end
fn s2exp_metlt_reduce {n:nat}
(met: s2explst n, met_bound: s2explst n): s2exp = let
fn auxlt
(isint: bool, s2e1: s2exp, s2e2: s2exp, lt: &int >> int)
: s2exp = begin
if isint then
s2exp_lt_int_int_bool (s2e1, s2e2)
else begin
if s2exp_synlt (s2e1, s2e2) then (lt := 1; s2exp_bool true)
else (lt := ~1; s2exp_bool false)
end
end
fn auxlte
(isint: bool, s2e1: s2exp, s2e2: s2exp, lte: &int >> int)
: s2exp = begin
if isint then
s2exp_lte_int_int_bool (s2e1, s2e2)
else begin
if s2exp_synlte (s2e1, s2e2) then (lte := 1; s2exp_bool true)
else (lte := ~1; s2exp_bool false)
end
end
fun auxlst {n:nat}
(s2es1: s2explst n, s2es2: s2explst n): s2exp = begin
case+ s2es1 of
| list_cons (s2e1, s2es1) => let
var lt: int = 0 and lte: int = 0
val+ list_cons (s2e2, s2es2) = s2es2
val isint = s2rt_is_int (s2e1.s2exp_srt)
val s2p_lt = auxlt (isint, s2e1, s2e2, lt)
val s2p_lte = auxlte (isint, s2e1, s2e2, lte)
in
case+ lt of
| _ when lt = 0 => begin
s2exp_add_bool_bool_bool (
s2p_lt
, s2exp_mul_bool_bool_bool (s2p_lte, auxlst (s2es1, s2es2))
)
end | _ when lt > 0 => s2p_lt | _ => begin
if lte > 0 then auxlst (s2es1, s2es2) else s2p_lte
end end | list_nil () => s2exp_bool false
end in
auxlst (met, met_bound)
end
implement
s3bexp_make_s2exp
(s2e0, s2cs, fds) = let
val s2e0 = s2exp_whnf s2e0
in
case+ s2e0.s2exp_node of
| S2Eapp (s2e1, s2es2) => begin case+ s2e1.s2exp_node of
| S2Ecst s2c1 => s3bexp_make_s2cst_s2explst (s2c1, s2es2, s2cs, fds)
| _ => None_vt ()
end | S2Ecst s2c => begin case+ s2c of
| _ when s2cstref_cst_equ (True_bool, s2c) => Some_vt (s3bexp_true)
| _ when s2cstref_cst_equ (False_bool, s2c) => Some_vt (s3bexp_false)
| _ => (s2cs := s2cstlst_add (s2cs, s2c); Some_vt (s3bexp_cst s2c))
end | S2Evar s2v => Some_vt (s3bexp_var s2v)
| S2Eeqeq (s2e1, s2e2) => aux_equal (s2e1, s2e2, s2cs, fds)
| S2Emetlt (met, met_bound) => let
val s2e_met = s2exp_metlt_reduce (met, met_bound)
in
s3bexp_make_s2exp (s2e_met, s2cs, fds)
end | _ => let val () = begin
prerr "warning(3): s3bexp_make_s2exp: s2e0 = "; prerr s2e0; prerr_newline ();
end in
None_vt ()
end end
implement
s3bexp_make_h3ypo
(h3p, s2cs, fds) = begin
case+ h3p.h3ypo_node of
| H3YPOprop s2p => s3bexp_make_s2exp (s2p, s2cs, fds)
| H3YPObind (s2v1, s2e2) => aux_bind (h3p.h3ypo_loc, s2v1, s2e2, s2cs, fds)
| H3YPOeqeq (s2e1, s2e2) => aux_equal (s2e1, s2e2, s2cs, fds)
end
end
implement
s3iexp_make_s2exp
(s2e0, s2cs, fds) = let
val s2e0 = s2exp_whnf s2e0
in
case+ s2e0.s2exp_node of
| S2Eapp (s2e1, s2es2) => begin case+ s2e1.s2exp_node of
| S2Ecst s2c1 => s3iexp_make_s2cst_s2explst (s2c1, s2es2, s2cs, fds)
| _ => None_vt ()
end | S2Echar c => let
val i = int_of_char c in Some_vt (s3iexp_int i)
end | S2Ecst s2c => begin
s2cs := s2cstlst_add (s2cs, s2c); Some_vt (s3iexp_cst s2c)
end | S2Eint i => Some_vt (s3iexp_int i)
| S2Eintinf i => Some_vt (s3iexp_intinf i)
| S2Esize s2ze => let
val s2c_rel = s2cstref_cst_get (Size_int_int_bool)
val s2v = s2cfdeflst_replace (s2rt_int, s2c_rel, '[s2e0], s2cs, fds)
in
Some_vt (s3iexp_var s2v)
end | S2Evar s2v => Some_vt (s3iexp_var s2v)
| _ => let val () = begin
prerr "warning(3): s3iexp_make_s2exp: s2e0 = "; prerr s2e0; prerr_newline ();
end in
None_vt ()
end end
staload Map = "ats_map_lin.sats"
staload _ = "ats_map_lin.dats"
viewtypedef s2cst_index_map = $Map.map_vt (stamp_t, Pos)
viewtypedef s2var_index_map = $Map.map_vt (stamp_t, Pos)
overload compare with $Stamp.compare_stamp_stamp
fn s2cst_index_map_make (): s2cst_index_map =
$Map.map_make {stamp_t, Pos} (lam (s1, s2) => compare (s1, s2))
fn s2var_index_map_make (): s2var_index_map =
$Map.map_make {stamp_t, Pos} (lam (s1, s2) => compare (s1, s2))
fn s2cst_index_find {n:pos}
(loc0: loc_t, m: !s2cst_index_map, s2c: s2cst_t, n: int n)
: intBtw (1, n) = let
val stamp = s2cst_stamp_get s2c
in
case+ $Map.map_search (m, stamp) of
| ~Some_vt (i) => if i < n then i else begin
prerr_loc_interror (loc0);
prerr ": s2cst_index_find: the static constant [";
prerr_s2cst s2c;
prerr "] is associated with an index that is out-of-range.";
prerr_newline ();
$Err.abort {intBtw (1, n)} ()
end | ~None_vt () => begin
prerr_loc_interror (loc0);
prerr ": s2cst_index_find: the static constant [";
prerr_s2cst s2c;
prerr "] is not associated with any index.";
prerr_newline ();
$Err.abort {intBtw (1, n)} ()
end end
fn s2var_index_find {n:pos}
(loc0: loc_t, m: !s2var_index_map, s2v: s2var_t, n: int n)
: intBtw (1, n) = let
val stamp = s2var_stamp_get s2v
in
case+ $Map.map_search (m, stamp) of
| ~Some_vt (i) => if i < n then i else begin
prerr_loc_interror (loc0);
prerr ": s2var_index_find: the static variable [";
prerr_s2var s2v;
prerr "] is associated with an index that is out-of-range.";
prerr_newline ();
$Err.abort {intBtw (1, n)} ()
end | ~None_vt () => begin
prerr_loc_interror (loc0);
prerr ": s2var_index_find: the static variable [";
prerr_s2var s2v;
prerr "] is not associated with any index.";
prerr_newline ();
$Err.abort {intBtw (1, n)} ()
end end
fn s2cst_index_insert
(cim: !s2cst_index_map, s2c: s2cst_t, i: Pos): void =
$Map.map_insert (cim, s2cst_stamp_get s2c, i)
fn s2var_index_insert
(vim: !s2var_index_map, s2v: s2var_t, i: Pos): void =
$Map.map_insert (vim, s2var_stamp_get s2v, i)
staload FM = "ats_solver_fm.sats"
stadef i0nt = $FM.i0nt
stadef intvec = $FM.intvec
extern
fun s3aexp_intvec_update_err {n:pos} {l:addr} (
pf_arr: !intvec n @ l
| loc0: loc_t
, cim: !s2cst_index_map
, vim: !s2var_index_map
, ivp: ptr l, n: int n
, coef: i0nt, s3ae0: s3aexp
, errno: &int
) : void
extern
fun s3bexp_intvec_update_err {n:pos} {l:addr} (
pf_arr: !intvec n @ l
| loc0: loc_t
, cim: !s2cst_index_map
, vim: !s2var_index_map
, ivp: ptr l, n: int n
, coef: i0nt, s3be0: s3bexp
, errno: &int
) : void
extern
fun s3iexp_intvec_update_err {n:pos} {l:addr} (
pf_arr: !intvec n @ l
| loc0: loc_t
, cim: !s2cst_index_map
, vim: !s2var_index_map
, ivp: ptr l, n: int n
, coef: i0nt, s3ie0: s3iexp
, errno: &int
) : void
implement
s3aexp_intvec_update_err
(pf_arr | loc0, cim, vim, ivp, n, coef, s3ae0, errno) = let
in
case+ s3ae0 of
| S3AEcst s2c => let
val ind = s2cst_index_find (loc0, cim, s2c, n)
in
ivp->[ind] := ivp->[ind] + coef
end | S3AEvar s2v => let
val ind = s2var_index_find (loc0, vim, s2v, n)
in
ivp->[ind] := ivp->[ind] + coef
end | S3AEnull () => ()
| S3AEpadd (s3ae1, s3ie2) => begin
s3aexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ae1, errno);
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie2, errno);
end | S3AEexp _ => begin
prerr_interror ();
prerr ": s3aexp_intvec_update_err: unsupported term: s3ae0 = "; prerr s3ae0;
prerr_newline ();
$Err.abort {void} ()
end end
implement
s3iexp_intvec_update_err
(pf_arr | loc0, cim, vim, ivp, n, coef, s3ie0, errno) = let
in
case+ s3ie0 of
| S3IEcst s2c => let
val ind = s2cst_index_find (loc0, cim, s2c, n)
in
ivp->[ind] := ivp->[ind] + coef
end | S3IEvar s2v => let
val ind = s2var_index_find (loc0, vim, s2v, n)
in
ivp->[ind] := ivp->[ind] + coef
end | S3IEint (i) => let
val i0 = $FM.i0nt_of_int i in ivp->[0] := ivp->[0] + coef * i0
end | S3IEintinf (i) => begin
let val i0 = $FM.i0nt_of_intinf i in ivp->[0] := ivp->[0] + coef * i0 end
end | S3IEineg (s3ie) => begin
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, ~coef, s3ie, errno);
end | S3IEiadd (s3ie1, s3ie2) => begin
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie1, errno);
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie2, errno);
end | S3IEisub (s3ie1, s3ie2) => begin
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie1, errno);
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, ~coef, s3ie2, errno);
end | S3IEimul (s3ie1, s3ie2) => begin case+ s3ie1 of
| S3IEint i1 => let
val coef = coef * $FM.i0nt_of_int (i1)
in
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie2, errno)
end | S3IEintinf i1 => let
val coef = coef * $FM.i0nt_of_intinf (i1)
in
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie2, errno)
end | _ => begin case+ s3ie2 of
| S3IEint i2 => let
val coef = coef * $FM.i0nt_of_int (i2) in
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie1, errno)
end | S3IEintinf i2 => let
val coef = coef * $FM.i0nt_of_intinf (i2) in
s3iexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ie1, errno)
end | _ => begin
$Loc.prerr_location loc0; prerr ": error(3)";
prerr ": it is not allowed to have a nonlinear term appear in a constraint: [";
prerr s3ie0; prerr "]"; prerr_newline ();
$Err.abort {void} ()
end end
end | S3IEpdiff (s3ae1, s3ae2) => begin
s3aexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, coef, s3ae1, errno);
s3aexp_intvec_update_err (pf_arr | loc0, cim, vim, ivp, n, ~coef, s3ae2, errno);
end | S3IEexp _ => begin
prerr_interror ();
prerr ": s3iexp_intvec_update_err: unsupported term: s3ie0 = "; prerr s3ie0;
prerr_newline ();
$Err.abort {void} ()
end end
extern
fun s3bexp_icstr_make_err {n:pos} (
loc0: loc_t
, cim: !s2cst_index_map
, vim: !s2var_index_map
, n: int n
, s3be0: s3bexp
, errno: &int
) : $FM.icstr n
implement
s3bexp_icstr_make_err
(loc0, cim, vim, n, s3be0, errno) = let
macdef aux (s3be) = s3bexp_icstr_make_err (loc0, cim, vim, n, ,(s3be), errno)
in
case+ s3be0 of
| S3BEbool b => begin
if b then begin
$FM.ICveclst (0, list_vt_nil ())
end else begin
$FM.ICveclst (1, list_vt_nil ())
end end | S3BEcst s2c => let
val ind = s2cst_index_find (loc0, cim, s2c, n)
val (pf_gc, pf_arr | ivp) = $FM.intvec_ptr_make (n)
val () = (ivp->[ind] := $FM.i0nt_1; ivp->[0] := $FM.i0nt_neg_1)
in
$FM.ICvec (2, $FM.intvecptr_make_view_ptr (pf_gc, pf_arr | ivp))
end | S3BEvar s2v => let
val ind = s2var_index_find (loc0, vim, s2v, n)
val (pf_gc, pf_arr | ivp) = $FM.intvec_ptr_make (n)
val () = (ivp->[ind] := $FM.i0nt_1; ivp->[0] := $FM.i0nt_neg_1)
in
$FM.ICvec (2, $FM.intvecptr_make_view_ptr (pf_gc, pf_arr | ivp))
end | S3BEbneg s3be => $FM.icstr_negate (aux s3be)
| S3BEbadd (s3be1, s3be2) => let
val ic1 = aux s3be1 and ic2 = aux s3be2
val ics = list_vt_cons (ic1, list_vt_cons (ic2, list_vt_nil ()))
in
$FM.ICveclst (1, ics)
end | S3BEbmul (s3be1, s3be2) => let
val ic1 = aux s3be1 and ic2 = aux s3be2
val ics = list_vt_cons (ic1, list_vt_cons (ic2, list_vt_nil ()))
in
$FM.ICveclst (0, ics)
end | S3BEiexp (knd, s3ie) => let
val (pf_gc, pf_arr | ivp) = $FM.intvec_ptr_make (n)
val () = s3iexp_intvec_update_err (
pf_arr | loc0, cim, vim, ivp, n, $FM.i0nt_1, s3ie, errno
) in
$FM.ICvec (knd, $FM.intvecptr_make_view_ptr (pf_gc, pf_arr | ivp))
end | S3BEexp _ => begin
prerr_interror ();
prerr ": s3bexp_intvec_make_err: unsupported term: s3be0 = "; prerr s3be0;
prerr_newline ();
$Err.abort ()
end end
extern
fun s3bexplst_s2exp_solve_fm (
loc0: loc_t
, s2vs: s2varlst
, s3bes: s3bexplst
, s2p: s2exp
, s2cs: &s2cstlst
, fds: &s2cfdeflst_vt
, errno: &int
) : intBtw (~1, 1)
implement
s3bexplst_s2exp_solve_fm
(loc0, s2vs, s3bes, s2p, s2cs, fds, errno) = let
viewtypedef cim_vt = s2cst_index_map and vim_vt = s2var_index_map
val os3p = s3bexp_make_s2exp (s2p, s2cs, fds)
var s3bes_asmp: s3bexplst = s3bes
val () = aux (s3bes_asmp, fds) where {
fun aux (s3bes: &s3bexplst, fds: !s2cfdeflst_vt): void =
case+ fds of
| S2CFDEFLSTcons (_, _, _, !rel, !fds_nxt) => let
val () = case+ !rel of
| Some_vt s3be => begin
fold@ (!rel); s3bes := list_cons (s3be, s3bes)
end
| None_vt () => fold@ (!rel)
in
aux (s3bes, !fds_nxt); fold@ (fds)
end | S2CFDEFLSTmark (!fds_nxt) => begin
aux (s3bes, !fds_nxt); fold@ (fds)
end | S2CFDEFLSTnil () => fold@ (fds)
}
val s3p = begin case+ os3p of
| ~Some_vt s3p => s3p | ~None_vt () => let
val () = begin
$Loc.prerr_location loc0;
prerr ": warning(3)"; prerr ": the constraint ["; prerr_s2exp s2p;
prerr "] cannot be translated into a form accepted by the constraint solver.";
prerr_newline ()
end in
s3bexp_false
end end var cnt: Pos = 1
var cim = s2cst_index_map_make ()
val () = aux (cim, cnt, s2cs) where {
fun aux (cim: !cim_vt, cnt: &Pos, s2cs: s2cstlst): void =
case+ s2cs of
| S2CSTLSTcons (s2c, s2cs) => let
val () = s2cst_index_insert (cim, s2c, cnt)
in
cnt := cnt + 1; aux (cim, cnt, s2cs)
end
| S2CSTLSTnil () => ()
} var vim = s2var_index_map_make ()
val () = aux (vim, cnt, s2vs) where {
fun aux (vim: !vim_vt, cnt: &Pos, s2vs: s2varlst): void =
case+ s2vs of
| list_cons (s2v, s2vs) => let
val () = s2var_index_insert (vim, s2v, cnt)
in
cnt := cnt + 1; aux (vim, cnt, s2vs)
end
| list_nil () => ()
} val () = aux (vim, cnt, fds) where {
fun aux (vim: !vim_vt, cnt: &Pos, fds: !s2cfdeflst_vt): void =
case+ fds of
| S2CFDEFLSTcons (_, _, s2v_res, _, !fds_nxt) => let
val () = s2var_index_insert (vim, s2v_res, cnt)
in
cnt := cnt + 1; aux (vim, cnt, !fds_nxt); fold@ fds
end
| S2CFDEFLSTmark (!fds_nxt) => begin
aux (vim, cnt, !fds_nxt); fold@ (fds)
end
| S2CFDEFLSTnil () => fold@ (fds)
} val cnt = cnt val ics_asmp = ics where {
viewtypedef T = [n,s:int] $FM.icstrlst (n, s)
fun aux {n:pos} (
loc0: loc_t
, cim: !cim_vt
, vim: !vim_vt
, n: int n
, s3bes: s3bexplst
, ics: &T? >> $FM.icstrlst n
, errno: &int
) : void = begin case+ s3bes of
| list_cons (s3be, s3bes) => let
val ic = s3bexp_icstr_make_err (loc0, cim, vim, n, s3be, errno)
val+ () = ics := list_vt_cons {$FM.icstr n} {0} (ic, ?)
val+ list_vt_cons (_, !ics_nxt) = ics
in
aux (loc0, cim, vim, n, s3bes, !ics_nxt, errno); fold@ ics
end
| list_nil () => (ics := list_vt_nil ())
end var ics: T val () = aux (loc0, cim, vim, cnt, s3bes_asmp, ics, errno)
}
val ic_conc = s3bexp_icstr_make_err (loc0, cim, vim, cnt, s3p, errno)
val () = $Map.map_free cim and () = $Map.map_free vim
var ics_all = list_vt_cons ($FM.icstr_negate ic_conc, ics_asmp)
val ans = $FM.icstrlst_solve (ics_all, cnt)
val () = $FM.icstrlst_free ics_all
in
ans
end
extern
fun c3str_solve_main (
s2vs: s2varlst
, s3bes: s3bexplst
, c3t: c3str
, s2cs: &s2cstlst
, fds: &s2cfdeflst_vt
, unsolved: &uint
, errno: &int
) : intBtw (~1, 1)
extern
fun c3str_solve_prop (
loc0: loc_t
, s2vs: s2varlst
, s3bes: s3bexplst
, s2p: s2exp
, s2cs: &s2cstlst
, fds: &s2cfdeflst_vt
, errno: &int
) : intBtw (~1, 1)
extern
fun c3str_solve_itmlst (
loc0: loc_t
, s2vs: s2varlst
, s3bes: s3bexplst
, s3is: s3itemlst
, s2cs: &s2cstlst
, fds: &s2cfdeflst_vt
, unsolved: &uint
, errno: &int
) : intBtw (~1, 1)
extern
fun c3str_solve_itmlst_disj (
loc0: loc_t
, s2vs: s2varlst
, s3bes: s3bexplst
, s3is: s3itemlst
, s3iss: s3itemlstlst
, s2cs: &s2cstlst
, fds: &s2cfdeflst_vt
, unsolved: &uint
, errno: &int
) : intBtw (~1, 1)
fn pattern_match_exhaustiveness_msg
(loc0: loc_t, knd: int, p2tcs: p2atcstlst) = let
fun aux (p2tcs: p2atcstlst): void = case+ p2tcs of
| list_cons (p2tc, p2tcs) => begin
prerr p2tc; prerr_newline (); aux p2tcs
end | list_nil () => ()
in
case+ knd of
| 0 => begin
$Loc.prerr_location loc0;
prerr ": warning(3)";
prerr ": pattern match is nonexhaustive:\n";
aux p2tcs;
end
| 1 => begin
$Loc.prerr_location loc0;
prerr ": error(3)";
prerr ": pattern match is nonexhaustive:\n";
aux p2tcs;
end
| _ => () end
implement
c3str_solve_main
(s2vs, s3bes, c3t, s2cs, fds, unsolved, errno) = let
val loc0 = c3t.c3str_loc
val s2cs0 = s2cs; val () = s2cfdeflst_push (fds)
val ans = (case+ c3t.c3str_node of
| C3STRprop s2p => c3str_solve_prop
(loc0, s2vs, s3bes, s2p, s2cs, fds, errno)
| C3STRitmlst s3is => c3str_solve_itmlst
(loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno)
) : intBtw (~1, 1)
val () = s2cfdeflst_pop (fds); val () = s2cs := s2cs0
fn prerr_c3str_if (unsolved: uint, c3t: c3str): void = begin
if (unsolved > 0U) then () else (prerr ": "; prerr_c3str c3t)
end var ans: intBtw (~1, 1) = ans
val () = begin case+ ans of
| _ when ans >= 0 => begin case+ c3t.c3str_kind of
| C3STRKINDnone () => begin
if unsolved > 0U then begin
end else begin
$Loc.prerr_location loc0; prerr ": error(3)";
prerr ": unsolved constraint"; prerr_c3str_if (unsolved, c3t);
prerr_newline ()
end
end | C3STRKINDmetric_nat () => begin
$Loc.prerr_location loc0; prerr ": error(3)";
prerr ": unsolved constraint for termination metric being welfounded";
prerr_c3str_if (unsolved, c3t);
prerr_newline ()
end | C3STRKINDmetric_dec () => begin
$Loc.prerr_location loc0; prerr ": error(3)";
prerr ": unsolved constraint for termination metric being decreasing";
prerr_c3str_if (unsolved, c3t);
prerr_newline ()
end | C3STRKINDpattern_match_exhaustiveness (knd, p2tcs) => let
val () = pattern_match_exhaustiveness_msg (loc0, knd, p2tcs)
in
if knd <= 0 then ans := (~1) else ()
end | C3STRKINDvarfin (d2v, s2e, s2e_fin) => begin
$Loc.prerr_location loc0; prerr ": error(3)";
prerr ": unsolved constraint for the dynamic variable [";
prerr d2v; prerr "]";
prerr_c3str_if (unsolved, c3t);
prerr_newline ()
end | C3STRKINDloop (knd) => begin
$Loc.prerr_location loc0; prerr ": error(3)";
if knd = 0 then prerr ": unsolved constraint for loop enter";
if knd = 1 then prerr ": unsolved constraint for loop exit";
if knd = 2 then prerr ": unsolved constraint for loop repeat";
prerr_c3str_if (unsolved, c3t);
prerr_newline ()
end end
| _ => ()
end val () = if ans >= 0 then (unsolved := unsolved + 1U)
in
ans
end
implement
c3str_solve_prop
(loc0, s2vs, s3bes, s2p, s2cs, fds, errno) = let
in
s3bexplst_s2exp_solve_fm (loc0, s2vs, s3bes, s2p, s2cs, fds, errno)
end
implement
c3str_solve_itmlst
(loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno) = let
in
case+ s3is of
| list_cons (s3i, s3is) => begin case+ s3i of
| S3ITEMcstr c3t => let
val ans1 = c3str_solve_main
(s2vs, s3bes, c3t, s2cs, fds, unsolved, errno)
val ans2 = c3str_solve_itmlst
(loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno)
in
if ans1 >= 0 then 0 else ans2
end | S3ITEMcstr_ref c3t_r => let
val ans1 = (
case+ !c3t_r of
| Some c3t => c3str_solve_main
(s2vs, s3bes, c3t, s2cs, fds, unsolved, errno)
| None () => ~1
) : intBtw (~1, 1)
val ans2 = c3str_solve_itmlst
(loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno)
in
if ans1 >= 0 then 0 else ans2
end | S3ITEMdisj s3iss_disj => c3str_solve_itmlst_disj (
loc0, s2vs, s3bes, s3is, s3iss_disj, s2cs, fds, unsolved, errno
) | S3ITEMhypo h3p => let
val () = the_s2varbindmap_push ()
val s3bes = (
case+ s3bexp_make_h3ypo (h3p, s2cs, fds) of
| ~Some_vt s3be => list_cons (s3be, s3bes)
| ~None_vt () => let
in
s3bes
end ) : s3bexplst
val ans = begin
c3str_solve_itmlst (loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno)
end val () = the_s2varbindmap_pop ()
in
ans
end | S3ITEMsvar s2v => let
val s2vs = list_cons (s2v, s2vs)
in
c3str_solve_itmlst (loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno)
end | S3ITEMsVar s2V => let
in
c3str_solve_itmlst (loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno)
end end | list_nil () => ~1
end
implement
c3str_solve_itmlst_disj
(loc0, s2vs, s3bes, s3is0, s3iss_disj, s2cs, fds, unsolved, errno) = begin
case+ s3iss_disj of
| list_cons (s3is_disj, s3iss_disj) => let
val s2cs0 = s2cs; val () = s2cfdeflst_push (fds)
val s3is = $Lst.list_append (s3is_disj, s3is0)
val ans = c3str_solve_itmlst (
loc0, s2vs, s3bes, s3is, s2cs, fds, unsolved, errno
) val () = s2cfdeflst_pop (fds); val () = s2cs := s2cs0
in
c3str_solve_itmlst_disj (
loc0, s2vs, s3bes, s3is0, s3iss_disj, s2cs, fds, unsolved, errno
)
end | list_nil () => ~1
end
implement
c3str_solve (c3t) = let
val () = the_s2varbindmap_initialize ()
val s2vs0 = list_nil () and s3bes0 = list_nil ()
var s2cs: s2cstlst = S2CSTLSTnil ()
var fds: s2cfdeflst_vt = S2CFDEFLSTnil ()
var unsolved: uint = 0U
var errno: int = 0
val _ = c3str_solve_main
(s2vs0, s3bes0, c3t, s2cs, fds, unsolved, errno)
val () = s2cfdeflst_free (fds)
in
if unsolved > 0U then begin
prerr "type-checking has failed";
if unsolved <= 1U then prerr ": there is one unsolved constraint";
if unsolved >= 2U then prerr ": there are some unsolved constraints";
prerr ": please inspect the above reported error message(s) for information.";
prerr_newline ();
$Err.abort {void} ()
end else begin
end end