Skip to content

Commit 7ac4b46

Browse files
ajreynolajreynol
committed
More
1 parent bbd13ac commit 7ac4b46

10 files changed

Lines changed: 243 additions & 191 deletions

File tree

‎plugins/lean_meta/lean_meta_smt_model.lean‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -330,14 +330,16 @@ def native_veq : SmtValue -> SmtValue -> native_Bool
330330
| x, y => decide (x = y)
331331

332332
macro_rules
333-
| `(native_veq_ext $m1 $m2) => do
333+
| `(native_veq_ext $T $U $m1 $m2) => do
334334
let lookupId := Lean.mkIdent `__smtx_msm_lookup
335+
let valueEqId := Lean.mkIdent `__smtx_value_eq
335336
`(by
336337
classical
337338
exact
338339
if hExt :
339340
∀ v : SmtValue,
340-
$lookupId $m1 v = $lookupId $m2 v then
341+
$valueEqId $U ($lookupId $T $m1 v)
342+
($lookupId $T $m2 v) = true then
341343
true
342344
else
343345
false)

‎plugins/model_smt/model_smt.eo‎

Lines changed: 24 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -470,20 +470,21 @@ $SMT_TYPE_CONSTRUCTORS$
470470
; return: The evaluation of an equality application.
471471
(program $smtx_value_=
472472
((v1 $smt_Value) (v2 $smt_Value) (f1 $smt_Value) (f2 $smt_Value)
473-
(T1 $smt_Type) (T2 $smt_Type) (m1 $smt_Map) (m2 $smt_Map)
473+
(T $smt_Type) (T1 $smt_Type) (T2 $smt_Type) (m1 $smt_Map) (m2 $smt_Map)
474474
(vs1 $smt_Seq) (vs2 $smt_Seq) (r1 $native_RegLan) (r2 $native_RegLan))
475-
:signature ($smt_Value $smt_Value) $native_Bool
475+
:signature ($smt_Type $smt_Value $smt_Value) $native_Bool
476476
(
477-
(($smtx_value_= ($vsm_map m1) ($vsm_map m2)) ($native_apply_2 "veq_ext" m1 m2))
478-
(($smtx_value_= ($vsm_set m1) ($vsm_set m2)) ($native_apply_2 "veq_ext" m1 m2))
479-
(($smtx_value_= ($vsm_fun m1) ($vsm_fun m2)) ($native_apply_2 "veq_ext" m1 m2))
480-
(($smtx_value_= ($vsm_re r1) ($vsm_re r2)) ($native_apply_2 "re_ext_eq" r1 r2))
481-
(($smtx_value_= ($vsm_seq ($ssm_empty T1)) ($vsm_seq ($ssm_empty T2))) $native_true)
482-
(($smtx_value_= ($vsm_seq ($ssm_cons v1 vs1)) ($vsm_seq ($ssm_cons v2 vs2)))
483-
($native_and ($smtx_value_= v1 v2) ($smtx_value_= ($vsm_seq vs1) ($vsm_seq vs2))))
484-
(($smtx_value_= ($vsm_apply f1 v1) ($vsm_apply f2 v2))
485-
($native_and ($smtx_value_= f1 f2) ($smtx_value_= v1 v2)))
486-
(($smtx_value_= v1 v2) ($native_veq v1 v2))
477+
(($smtx_value_= ($tsm_Map T1 T2) ($vsm_map m1) ($vsm_map m2)) ($native_apply_4 "veq_ext" T1 T2 m1 m2))
478+
(($smtx_value_= ($tsm_Set T1) ($vsm_set m1) ($vsm_set m2)) ($native_apply_4 "veq_ext" T1 $tsm_Bool m1 m2))
479+
(($smtx_value_= ($tsm_FunType T1 T2) ($vsm_fun m1) ($vsm_fun m2)) ($native_apply_4 "veq_ext" T1 T2 m1 m2))
480+
(($smtx_value_= $tsm_RegLan ($vsm_re r1) ($vsm_re r2)) ($native_apply_2 "re_ext_eq" r1 r2))
481+
(($smtx_value_= ($tsm_Seq T) ($vsm_seq ($ssm_empty T1)) ($vsm_seq ($ssm_empty T2))) $native_true)
482+
(($smtx_value_= ($tsm_Seq T) ($vsm_seq ($ssm_cons v1 vs1)) ($vsm_seq ($ssm_cons v2 vs2)))
483+
($native_and ($smtx_value_= T v1 v2) ($smtx_value_= ($tsm_Seq T) ($vsm_seq vs1) ($vsm_seq vs2))))
484+
; FIXME
485+
;(($smtx_value_= T ($vsm_apply f1 v1) ($vsm_apply f2 v2))
486+
; ($native_and ($smtx_value_= f1 f2) ($smtx_value_= v1 v2)))
487+
(($smtx_value_= T v1 v2) ($native_veq v1 v2))
487488
)
488489
)
489490

@@ -588,11 +589,11 @@ $SMT_TYPE_CONSTRUCTORS$
588589
; This program looks up the value of a term in a map.
589590
; This is used for function evaluation.
590591
(program $smtx_msm_lookup
591-
((T $smt_Type) (i $smt_Value) (j $smt_Value) (e $smt_Value) (m $smt_Map))
592-
:signature ($smt_Map $smt_Value) $smt_Value
592+
((T $smt_Type) (U $smt_Type) (i $smt_Value) (j $smt_Value) (e $smt_Value) (m $smt_Map))
593+
:signature ($smt_Type $smt_Map $smt_Value) $smt_Value
593594
(
594-
(($smtx_msm_lookup ($msm_cons j e m) i) ($native_ite ($smtx_value_= j i) e ($smtx_msm_lookup m i)))
595-
(($smtx_msm_lookup ($msm_default T e) i) e)
595+
(($smtx_msm_lookup T ($msm_cons j e m) i) ($native_ite ($smtx_value_= T j i) e ($smtx_msm_lookup T m i)))
596+
(($smtx_msm_lookup T ($msm_default U e) i) e)
596597
)
597598
)
598599

@@ -641,7 +642,7 @@ $SMT_TYPE_CONSTRUCTORS$
641642
(define $smtx_mss_mk_insert ((e $smt_Value) (m $smt_Map)) ($smtx_msm_update m e $vsm_true))
642643
(define $smtx_mss_insert ((e $smt_Value) (m $smt_Map)) ($msm_cons e $vsm_true m))
643644
(define $smtx_mss_member ((e $smt_Value) (m $smt_Map))
644-
($native_veq ($smtx_msm_lookup m e) $vsm_true))
645+
($native_veq ($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m e) $vsm_true))
645646

646647
; Helper for computing binary set operators.
647648
; Takes a flag isInter and maps m1, m2, macc.
@@ -910,7 +911,8 @@ $SMT_TYPE_CONSTRUCTORS$
910911
(program $smtx_model_eval_= ((v1 $smt_Value) (v2 $smt_Value))
911912
:signature ($smt_Value $smt_Value) $smt_Value
912913
(
913-
(($smtx_model_eval_= v1 v2) ($vsm_bool ($smtx_value_= v1 v2)))
914+
(($smtx_model_eval_= v1 v2)
915+
($vsm_bool ($smtx_value_= ($smtx_typeof_value v1) v1 v2)))
914916
)
915917
)
916918

@@ -921,8 +923,10 @@ $SMT_TYPE_CONSTRUCTORS$
921923
((v $smt_Value) (i $smt_Value) (m $smt_Map))
922924
:signature ($smt_Value $smt_Value) $smt_Value
923925
(
924-
(($smtx_map_select ($vsm_map m) i) ($smtx_msm_lookup m i))
925-
(($smtx_map_select ($vsm_set m) i) ($smtx_msm_lookup m i))
926+
(($smtx_map_select ($vsm_map m) i)
927+
($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m i))
928+
(($smtx_map_select ($vsm_set m) i)
929+
($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m i))
926930
(($smtx_map_select v i) $vsm_not_value)
927931
)
928932
)

‎plugins/smt_meta/smt_meta.smt2‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ $SM_TYPE_DECL$
214214
(declare-fun eval_tlambda (smm.SmtModel String tsm.Type sm.Term) vsm.Value)
215215
(declare-fun eval_tapply (smm.SmtModel vsm.Value vsm.Value) vsm.Value)
216216
; whether two (e.g. map) value are extensionally equal
217-
(declare-fun veq_ext (msm.Map msm.Map) Bool)
217+
(declare-fun veq_ext (tsm.Type tsm.Type msm.Map msm.Map) Bool)
218218

219219
;;; Relevant definitions
220220

@@ -295,10 +295,10 @@ $SM_DEFS$
295295
:named smtx.inhabited_type.def))
296296

297297
; whether two map values are extensionally equal
298-
(assert (! (forall ((v1 msm.Map) (v2 msm.Map))
299-
(! (= (veq_ext v1 v2)
300-
(forall ((i vsm.Value)) (= ($smtx_msm_lookup v1 i) ($smtx_msm_lookup v2 i))))
301-
:pattern ((veq_ext v1 v2))))
298+
(assert (! (forall ((T1 tsm.Type) (T2 tsm.Type) (v1 msm.Map) (v2 msm.Map))
299+
(! (= (veq_ext T1 T2 v1 v2)
300+
(forall ((i vsm.Value)) ($smtx_value_= T2 ($smtx_msm_lookup T1 v1 i) ($smtx_msm_lookup T1 v2 i))))
301+
:pattern ((veq_ext T1 T2 v1 v2))))
302302
:named smtx.veq_ext.def))
303303

304304
;;; The verification condition

‎tools/eoc/out/lean-cpc-defs.eo‎

Lines changed: 24 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -2302,20 +2302,21 @@
23022302
; return: The evaluation of an equality application.
23032303
(program $smtx_value_=
23042304
((v1 $smt_Value) (v2 $smt_Value) (f1 $smt_Value) (f2 $smt_Value)
2305-
(T1 $smt_Type) (T2 $smt_Type) (m1 $smt_Map) (m2 $smt_Map)
2305+
(T $smt_Type) (T1 $smt_Type) (T2 $smt_Type) (m1 $smt_Map) (m2 $smt_Map)
23062306
(vs1 $smt_Seq) (vs2 $smt_Seq) (r1 $native_RegLan) (r2 $native_RegLan))
2307-
:signature ($smt_Value $smt_Value) $native_Bool
2307+
:signature ($smt_Type $smt_Value $smt_Value) $native_Bool
23082308
(
2309-
(($smtx_value_= ($vsm_map m1) ($vsm_map m2)) ($native_apply_2 "veq_ext" m1 m2))
2310-
(($smtx_value_= ($vsm_set m1) ($vsm_set m2)) ($native_apply_2 "veq_ext" m1 m2))
2311-
(($smtx_value_= ($vsm_fun m1) ($vsm_fun m2)) ($native_apply_2 "veq_ext" m1 m2))
2312-
(($smtx_value_= ($vsm_re r1) ($vsm_re r2)) ($native_apply_2 "re_ext_eq" r1 r2))
2313-
(($smtx_value_= ($vsm_seq ($ssm_empty T1)) ($vsm_seq ($ssm_empty T2))) $native_true)
2314-
(($smtx_value_= ($vsm_seq ($ssm_cons v1 vs1)) ($vsm_seq ($ssm_cons v2 vs2)))
2315-
($native_and ($smtx_value_= v1 v2) ($smtx_value_= ($vsm_seq vs1) ($vsm_seq vs2))))
2316-
(($smtx_value_= ($vsm_apply f1 v1) ($vsm_apply f2 v2))
2317-
($native_and ($smtx_value_= f1 f2) ($smtx_value_= v1 v2)))
2318-
(($smtx_value_= v1 v2) ($native_veq v1 v2))
2309+
(($smtx_value_= ($tsm_Map T1 T2) ($vsm_map m1) ($vsm_map m2)) ($native_apply_4 "veq_ext" T1 T2 m1 m2))
2310+
(($smtx_value_= ($tsm_Set T1) ($vsm_set m1) ($vsm_set m2)) ($native_apply_4 "veq_ext" T1 $tsm_Bool m1 m2))
2311+
(($smtx_value_= ($tsm_FunType T1 T2) ($vsm_fun m1) ($vsm_fun m2)) ($native_apply_4 "veq_ext" T1 T2 m1 m2))
2312+
(($smtx_value_= $tsm_RegLan ($vsm_re r1) ($vsm_re r2)) ($native_apply_2 "re_ext_eq" r1 r2))
2313+
(($smtx_value_= ($tsm_Seq T) ($vsm_seq ($ssm_empty T1)) ($vsm_seq ($ssm_empty T2))) $native_true)
2314+
(($smtx_value_= ($tsm_Seq T) ($vsm_seq ($ssm_cons v1 vs1)) ($vsm_seq ($ssm_cons v2 vs2)))
2315+
($native_and ($smtx_value_= T v1 v2) ($smtx_value_= ($tsm_Seq T) ($vsm_seq vs1) ($vsm_seq vs2))))
2316+
; FIXME
2317+
;(($smtx_value_= T ($vsm_apply f1 v1) ($vsm_apply f2 v2))
2318+
; ($native_and ($smtx_value_= f1 f2) ($smtx_value_= v1 v2)))
2319+
(($smtx_value_= T v1 v2) ($native_veq v1 v2))
23192320
)
23202321
)
23212322

@@ -2420,11 +2421,11 @@
24202421
; This program looks up the value of a term in a map.
24212422
; This is used for function evaluation.
24222423
(program $smtx_msm_lookup
2423-
((T $smt_Type) (i $smt_Value) (j $smt_Value) (e $smt_Value) (m $smt_Map))
2424-
:signature ($smt_Map $smt_Value) $smt_Value
2424+
((T $smt_Type) (U $smt_Type) (i $smt_Value) (j $smt_Value) (e $smt_Value) (m $smt_Map))
2425+
:signature ($smt_Type $smt_Map $smt_Value) $smt_Value
24252426
(
2426-
(($smtx_msm_lookup ($msm_cons j e m) i) ($native_ite ($smtx_value_= j i) e ($smtx_msm_lookup m i)))
2427-
(($smtx_msm_lookup ($msm_default T e) i) e)
2427+
(($smtx_msm_lookup T ($msm_cons j e m) i) ($native_ite ($smtx_value_= T j i) e ($smtx_msm_lookup T m i)))
2428+
(($smtx_msm_lookup T ($msm_default U e) i) e)
24282429
)
24292430
)
24302431

@@ -2473,7 +2474,7 @@
24732474
(define $smtx_mss_mk_insert ((e $smt_Value) (m $smt_Map)) ($smtx_msm_update m e $vsm_true))
24742475
(define $smtx_mss_insert ((e $smt_Value) (m $smt_Map)) ($msm_cons e $vsm_true m))
24752476
(define $smtx_mss_member ((e $smt_Value) (m $smt_Map))
2476-
($native_veq ($smtx_msm_lookup m e) $vsm_true))
2477+
($native_veq ($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m e) $vsm_true))
24772478

24782479
; Helper for computing binary set operators.
24792480
; Takes a flag isInter and maps m1, m2, macc.
@@ -2742,7 +2743,8 @@
27422743
(program $smtx_model_eval_= ((v1 $smt_Value) (v2 $smt_Value))
27432744
:signature ($smt_Value $smt_Value) $smt_Value
27442745
(
2745-
(($smtx_model_eval_= v1 v2) ($vsm_bool ($smtx_value_= v1 v2)))
2746+
(($smtx_model_eval_= v1 v2)
2747+
($vsm_bool ($smtx_value_= ($smtx_typeof_value v1) v1 v2)))
27462748
)
27472749
)
27482750

@@ -2753,8 +2755,10 @@
27532755
((v $smt_Value) (i $smt_Value) (m $smt_Map))
27542756
:signature ($smt_Value $smt_Value) $smt_Value
27552757
(
2756-
(($smtx_map_select ($vsm_map m) i) ($smtx_msm_lookup m i))
2757-
(($smtx_map_select ($vsm_set m) i) ($smtx_msm_lookup m i))
2758+
(($smtx_map_select ($vsm_map m) i)
2759+
($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m i))
2760+
(($smtx_map_select ($vsm_set m) i)
2761+
($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m i))
27582762
(($smtx_map_select v i) $vsm_not_value)
27592763
)
27602764
)

‎tools/eoc/out/lean-cpc-final.eo‎

Lines changed: 32 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
; trim-defs: $eo_prog_symm $eo_prog_contra
2-
; #trim-defs: 391
2+
; #trim-defs: 392
33
(declare-const $eo_Proof Type)
44
(declare-parameterized-const $eo_pf ((F Bool :opaque)) $eo_Proof)
55
(declare-const Int Type)
@@ -659,20 +659,21 @@
659659
(program $smtx_model_lookup () :signature ($smt_Model $native_String $smt_Type) $smt_Value)
660660
(program $smtx_value_=
661661
((v1 $smt_Value) (v2 $smt_Value) (f1 $smt_Value) (f2 $smt_Value)
662-
(T1 $smt_Type) (T2 $smt_Type) (m1 $smt_Map) (m2 $smt_Map)
662+
(T $smt_Type) (T1 $smt_Type) (T2 $smt_Type) (m1 $smt_Map) (m2 $smt_Map)
663663
(vs1 $smt_Seq) (vs2 $smt_Seq) (r1 $native_RegLan) (r2 $native_RegLan))
664-
:signature ($smt_Value $smt_Value) $native_Bool
665-
(
666-
(($smtx_value_= ($vsm_map m1) ($vsm_map m2)) ($native_apply_2 "veq_ext" m1 m2))
667-
(($smtx_value_= ($vsm_set m1) ($vsm_set m2)) ($native_apply_2 "veq_ext" m1 m2))
668-
(($smtx_value_= ($vsm_fun m1) ($vsm_fun m2)) ($native_apply_2 "veq_ext" m1 m2))
669-
(($smtx_value_= ($vsm_re r1) ($vsm_re r2)) ($native_apply_2 "re_ext_eq" r1 r2))
670-
(($smtx_value_= ($vsm_seq ($ssm_empty T1)) ($vsm_seq ($ssm_empty T2))) $native_true)
671-
(($smtx_value_= ($vsm_seq ($ssm_cons v1 vs1)) ($vsm_seq ($ssm_cons v2 vs2)))
672-
($native_and ($smtx_value_= v1 v2) ($smtx_value_= ($vsm_seq vs1) ($vsm_seq vs2))))
673-
(($smtx_value_= ($vsm_apply f1 v1) ($vsm_apply f2 v2))
674-
($native_and ($smtx_value_= f1 f2) ($smtx_value_= v1 v2)))
675-
(($smtx_value_= v1 v2) ($native_veq v1 v2))
664+
:signature ($smt_Type $smt_Value $smt_Value) $native_Bool
665+
(
666+
(($smtx_value_= ($tsm_Map T1 T2) ($vsm_map m1) ($vsm_map m2)) ($native_apply_4 "veq_ext" T1 T2 m1 m2))
667+
(($smtx_value_= ($tsm_Set T1) ($vsm_set m1) ($vsm_set m2)) ($native_apply_4 "veq_ext" T1 $tsm_Bool m1 m2))
668+
(($smtx_value_= ($tsm_FunType T1 T2) ($vsm_fun m1) ($vsm_fun m2)) ($native_apply_4 "veq_ext" T1 T2 m1 m2))
669+
(($smtx_value_= $tsm_RegLan ($vsm_re r1) ($vsm_re r2)) ($native_apply_2 "re_ext_eq" r1 r2))
670+
(($smtx_value_= ($tsm_Seq T) ($vsm_seq ($ssm_empty T1)) ($vsm_seq ($ssm_empty T2))) $native_true)
671+
(($smtx_value_= ($tsm_Seq T) ($vsm_seq ($ssm_cons v1 vs1)) ($vsm_seq ($ssm_cons v2 vs2)))
672+
($native_and ($smtx_value_= T v1 v2) ($smtx_value_= ($tsm_Seq T) ($vsm_seq vs1) ($vsm_seq vs2))))
673+
674+
675+
676+
(($smtx_value_= T v1 v2) ($native_veq v1 v2))
676677
)
677678
)
678679
(declare-const $smt_RefList Type)
@@ -748,11 +749,11 @@
748749
)
749750
)
750751
(program $smtx_msm_lookup
751-
((T $smt_Type) (i $smt_Value) (j $smt_Value) (e $smt_Value) (m $smt_Map))
752-
:signature ($smt_Map $smt_Value) $smt_Value
752+
((T $smt_Type) (U $smt_Type) (i $smt_Value) (j $smt_Value) (e $smt_Value) (m $smt_Map))
753+
:signature ($smt_Type $smt_Map $smt_Value) $smt_Value
753754
(
754-
(($smtx_msm_lookup ($msm_cons j e m) i) ($native_ite ($smtx_value_= j i) e ($smtx_msm_lookup m i)))
755-
(($smtx_msm_lookup ($msm_default T e) i) e)
755+
(($smtx_msm_lookup T ($msm_cons j e m) i) ($native_ite ($smtx_value_= T j i) e ($smtx_msm_lookup T m i)))
756+
(($smtx_msm_lookup T ($msm_default U e) i) e)
756757
)
757758
)
758759
(program $smtx_typeof_map_value
@@ -767,6 +768,13 @@
767768
(($smtx_typeof_map_value ($msm_default T e)) ($tsm_Map T ($smtx_typeof_value e)))
768769
)
769770
)
771+
(program $smtx_index_typeof_map ((T $smt_Type) (U $smt_Type))
772+
:signature ($smt_Type) $smt_Type
773+
(
774+
(($smtx_index_typeof_map ($tsm_Map T U)) T)
775+
(($smtx_index_typeof_map T) $tsm_none)
776+
)
777+
)
770778
(program $smtx_map_to_set_type ((T $smt_Type))
771779
:signature ($smt_Type) $smt_Type
772780
(
@@ -941,15 +949,18 @@
941949
(program $smtx_model_eval_= ((v1 $smt_Value) (v2 $smt_Value))
942950
:signature ($smt_Value $smt_Value) $smt_Value
943951
(
944-
(($smtx_model_eval_= v1 v2) ($vsm_bool ($smtx_value_= v1 v2)))
952+
(($smtx_model_eval_= v1 v2)
953+
($vsm_bool ($smtx_value_= ($smtx_typeof_value v1) v1 v2)))
945954
)
946955
)
947956
(program $smtx_map_select
948957
((v $smt_Value) (i $smt_Value) (m $smt_Map))
949958
:signature ($smt_Value $smt_Value) $smt_Value
950959
(
951-
(($smtx_map_select ($vsm_map m) i) ($smtx_msm_lookup m i))
952-
(($smtx_map_select ($vsm_set m) i) ($smtx_msm_lookup m i))
960+
(($smtx_map_select ($vsm_map m) i)
961+
($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m i))
962+
(($smtx_map_select ($vsm_set m) i)
963+
($smtx_msm_lookup ($smtx_index_typeof_map ($smtx_typeof_map_value m)) m i))
953964
(($smtx_map_select v i) $vsm_not_value)
954965
)
955966
)

‎tools/eoc/out/lean/SmtModel.lean‎

Lines changed: 23 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -381,14 +381,16 @@ def native_veq : SmtValue -> SmtValue -> native_Bool
381381
| x, y => decide (x = y)
382382

383383
macro_rules
384-
| `(native_veq_ext $m1 $m2) => do
384+
| `(native_veq_ext $T $U $m1 $m2) => do
385385
let lookupId := Lean.mkIdent `__smtx_msm_lookup
386+
let valueEqId := Lean.mkIdent `__smtx_value_eq
386387
`(by
387388
classical
388389
exact
389390
if hExt :
390391
∀ v : SmtValue,
391-
$lookupId $m1 v = $lookupId $m2 v then
392+
$valueEqId $U ($lookupId $T $m1 v)
393+
($lookupId $T $m2 v) = true then
392394
true
393395
else
394396
false)
@@ -484,15 +486,14 @@ def __vsm_apply_arg_nth : SmtValue -> native_Nat -> native_Nat -> SmtValue
484486
| a, n, npos => SmtValue.NotValue
485487

486488

487-
def __smtx_value_eq : SmtValue -> SmtValue -> native_Bool
488-
| (SmtValue.Map m1), (SmtValue.Map m2) => (native_veq_ext m1 m2)
489-
| (SmtValue.Set m1), (SmtValue.Set m2) => (native_veq_ext m1 m2)
490-
| (SmtValue.Fun m1), (SmtValue.Fun m2) => (native_veq_ext m1 m2)
491-
| (SmtValue.RegLan r1), (SmtValue.RegLan r2) => (native_re_ext_eq r1 r2)
492-
| (SmtValue.Seq (SmtSeq.empty T1)), (SmtValue.Seq (SmtSeq.empty T2)) => true
493-
| (SmtValue.Seq (SmtSeq.cons v1 vs1)), (SmtValue.Seq (SmtSeq.cons v2 vs2)) => (native_and (__smtx_value_eq v1 v2) (__smtx_value_eq (SmtValue.Seq vs1) (SmtValue.Seq vs2)))
494-
| (SmtValue.Apply f1 v1), (SmtValue.Apply f2 v2) => (native_and (__smtx_value_eq f1 f2) (__smtx_value_eq v1 v2))
495-
| v1, v2 => (native_veq v1 v2)
489+
def __smtx_value_eq : SmtType -> SmtValue -> SmtValue -> native_Bool
490+
| (SmtType.Map T1 T2), (SmtValue.Map m1), (SmtValue.Map m2) => (native_veq_ext T1 T2 m1 m2)
491+
| (SmtType.Set T1), (SmtValue.Set m1), (SmtValue.Set m2) => (native_veq_ext T1 SmtType.Bool m1 m2)
492+
| (SmtType.FunType T1 T2), (SmtValue.Fun m1), (SmtValue.Fun m2) => (native_veq_ext T1 T2 m1 m2)
493+
| SmtType.RegLan, (SmtValue.RegLan r1), (SmtValue.RegLan r2) => (native_re_ext_eq r1 r2)
494+
| (SmtType.Seq T), (SmtValue.Seq (SmtSeq.empty T1)), (SmtValue.Seq (SmtSeq.empty T2)) => true
495+
| (SmtType.Seq T), (SmtValue.Seq (SmtSeq.cons v1 vs1)), (SmtValue.Seq (SmtSeq.cons v2 vs2)) => (native_and (__smtx_value_eq T v1 v2) (__smtx_value_eq (SmtType.Seq T) (SmtValue.Seq vs1) (SmtValue.Seq vs2)))
496+
| T, v1, v2 => (native_veq v1 v2)
496497

497498

498499
def __smtx_dt_cons_wf_rec : SmtDatatypeCons -> RefList -> native_Bool
@@ -528,9 +529,9 @@ def __smtx_typeof_guard (T : SmtType) (U : SmtType) : SmtType :=
528529
def __smtx_typeof_guard_wf (T : SmtType) (U : SmtType) : SmtType :=
529530
(native_ite (__smtx_type_wf T) U SmtType.None)
530531

531-
def __smtx_msm_lookup : SmtMap -> SmtValue -> SmtValue
532-
| (SmtMap.cons j e m), i => (native_ite (__smtx_value_eq j i) e (__smtx_msm_lookup m i))
533-
| (SmtMap.default T e), i => e
532+
def __smtx_msm_lookup (T : SmtType) : SmtMap -> SmtValue -> SmtValue
533+
| (SmtMap.cons j e m), i => (native_ite (__smtx_value_eq T j i) e (__smtx_msm_lookup T m i))
534+
| (SmtMap.default U e), i => e
534535

535536

536537
def __smtx_typeof_map_value : SmtMap -> SmtType
@@ -540,6 +541,11 @@ def __smtx_typeof_map_value : SmtMap -> SmtType
540541
| (SmtMap.default T e) => (SmtType.Map T (__smtx_typeof_value e))
541542

542543

544+
def __smtx_index_typeof_map : SmtType -> SmtType
545+
| (SmtType.Map T U) => T
546+
| T => SmtType.None
547+
548+
543549
def __smtx_map_to_set_type : SmtType -> SmtType
544550
| (SmtType.Map T SmtType.Bool) => (SmtType.Set T)
545551
| T => SmtType.None
@@ -632,11 +638,11 @@ def __smtx_model_eval_ite : SmtValue -> SmtValue -> SmtValue -> SmtValue
632638

633639

634640
def __smtx_model_eval_eq (v1 : SmtValue) (v2 : SmtValue) : SmtValue :=
635-
(SmtValue.Boolean (__smtx_value_eq v1 v2))
641+
(SmtValue.Boolean (__smtx_value_eq (__smtx_typeof_value v1) v1 v2))
636642

637643
def __smtx_map_select : SmtValue -> SmtValue -> SmtValue
638-
| (SmtValue.Map m), i => (__smtx_msm_lookup m i)
639-
| (SmtValue.Set m), i => (__smtx_msm_lookup m i)
644+
| (SmtValue.Map m), i => (__smtx_msm_lookup (__smtx_index_typeof_map (__smtx_typeof_map_value m)) m i)
645+
| (SmtValue.Set m), i => (__smtx_msm_lookup (__smtx_index_typeof_map (__smtx_typeof_map_value m)) m i)
640646
| v, i => SmtValue.NotValue
641647

642648

0 commit comments

Comments
 (0)