- the connections between the intermediate language and the "bag"

[helm.git] / helm / software / lambda-delta / src / toplevel / top.ml

diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml
index b47d00725a9f056434c4523981ceb5adb4355a60..aad48387ebd1cda137b28399810e8ef9f6fc6016 100644 (file)
--- a/helm/software/lambda-delta/src/toplevel/top.ml
+++ b/helm/software/lambda-delta/src/toplevel/top.ml
@@ -31,6 +31,7 @@ module BD = BrgCrg
 module BO = BrgOutput
 module BR = BrgReduction
 module BU = BrgUntrusted
+module ZD = BagCrg
 module ZO = BagOutput
 module ZT = BagType
 module ZU = BagUntrusted
@@ -85,6 +86,8 @@ let print_counters st = function
 let xlate_entity entity = match !G.kernel, entity with
    | G.Brg, CrgEntity e -> 
       let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
+   | G.Bag, CrgEntity e -> 
+      let f e = (BagEntity e) in E.xlate f ZD.bag_of_crg e
    | _, entity          -> entity
 
 let pp_progress e =
@@ -107,7 +110,7 @@ let count_entity st = function
 let export_entity = function
    | CrgEntity e -> XL.export_entity XD.export_term e
    | BrgEntity e -> XL.export_entity BO.export_term e
-   | BagEntity _ -> ()
+   | BagEntity e -> XL.export_entity ZO.export_term e
 
 let type_check st k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in