Skip to content

Commit f1dbdb7

Browse files
hra687261filipeom
authored andcommitted
Update colibri2_mappings to use ht_expr
1 parent ac31c0e commit f1dbdb7

File tree

1 file changed

+10
-8
lines changed

1 file changed

+10
-8
lines changed

lib/colibri2_mappings.ml

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -675,32 +675,32 @@ module Fresh = struct
675675
*)
676676
let encore_expr_aux ?(record_sym = fun _ -> ()) (e : Expr.t) : expr =
677677
let open Expr in
678-
let rec aux ({ e; ty } : t) =
679-
match e with
678+
let rec aux (hte : t) =
679+
match e.node.e with
680680
| Val v -> encode_val v
681681
| Ptr (base, offset) ->
682682
let base' = encode_val (Num (I32 base)) in
683683
let offset' = aux offset in
684684
DTerm.Bitv.add base' offset'
685685
| Unop (op, e) ->
686686
let e' = aux e in
687-
encode_unop ty op e'
687+
encode_unop hte.node.ty op e'
688688
| Binop (op, e1, e2) ->
689689
let e1' = aux e1 in
690690
let e2' = aux e2 in
691-
encode_binop ty op e1' e2'
691+
encode_binop hte.node.ty op e1' e2'
692692
| Triop (op, e1, e2, e3) ->
693693
let e1' = aux e1
694694
and e2' = aux e2
695695
and e3' = aux e3 in
696-
encode_triop ty op e1' e2' e3'
696+
encode_triop hte.node.ty op e1' e2' e3'
697697
| Relop (op, e1, e2) ->
698698
let e1' = aux e1
699699
and e2' = aux e2 in
700-
encode_relop ty op e1' e2'
700+
encode_relop hte.node.ty op e1' e2'
701701
| Cvtop (op, e) ->
702702
let e' = aux e in
703-
encode_cvtop ty op e'
703+
encode_cvtop hte.node.ty op e'
704704
| Symbol s ->
705705
let cst = tcst_of_symbol s in
706706
record_sym cst;
@@ -946,7 +946,9 @@ module Fresh = struct
946946
947947
let value (e, _) (c : Expr.t) : Value.t =
948948
let c2v = Interp.interp e (encode_expr c) in
949-
match c2value_to_value c.ty c2v with None -> assert false | Some v -> v
949+
match c2value_to_value c.node.ty c2v with
950+
| None -> assert false
951+
| Some v -> v
950952
951953
let values_of_model ?(symbols : Symbol.t list option) ((_, model) : model) :
952954
Model.t =

0 commit comments

Comments
 (0)