Skip to content

Commit

Permalink
Update colibri2_mappings to use ht_expr
Browse files Browse the repository at this point in the history
  • Loading branch information
hra687261 authored and filipeom committed Jan 27, 2024
1 parent d161743 commit 10ee384
Showing 1 changed file with 10 additions and 8 deletions.
18 changes: 10 additions & 8 deletions lib/colibri2_mappings.ml
Original file line number Diff line number Diff line change
Expand Up @@ -675,32 +675,32 @@ module Fresh = struct
*)
let encore_expr_aux ?(record_sym = fun _ -> ()) (e : Expr.t) : expr =
let open Expr in
let rec aux ({ e; ty } : t) =
match e with
let rec aux (hte : t) =
match e.node.e with
| Val v -> encode_val v
| Ptr (base, offset) ->
let base' = encode_val (Num (I32 base)) in
let offset' = aux offset in
DTerm.Bitv.add base' offset'
| Unop (op, e) ->
let e' = aux e in
encode_unop ty op e'
encode_unop hte.node.ty op e'
| Binop (op, e1, e2) ->
let e1' = aux e1 in
let e2' = aux e2 in
encode_binop ty op e1' e2'
encode_binop hte.node.ty op e1' e2'
| Triop (op, e1, e2, e3) ->
let e1' = aux e1
and e2' = aux e2
and e3' = aux e3 in
encode_triop ty op e1' e2' e3'
encode_triop hte.node.ty op e1' e2' e3'
| Relop (op, e1, e2) ->
let e1' = aux e1
and e2' = aux e2 in
encode_relop ty op e1' e2'
encode_relop hte.node.ty op e1' e2'
| Cvtop (op, e) ->
let e' = aux e in
encode_cvtop ty op e'
encode_cvtop hte.node.ty op e'
| Symbol s ->
let cst = tcst_of_symbol s in
record_sym cst;
Expand Down Expand Up @@ -946,7 +946,9 @@ module Fresh = struct
let value (e, _) (c : Expr.t) : Value.t =
let c2v = Interp.interp e (encode_expr c) in
match c2value_to_value c.ty c2v with None -> assert false | Some v -> v
match c2value_to_value c.node.ty c2v with
| None -> assert false
| Some v -> v
let values_of_model ?(symbols : Symbol.t list option) ((_, model) : model) :
Model.t =
Expand Down

0 comments on commit 10ee384

Please sign in to comment.