From dc58a00179b68ece69df84b32123fa44cc75a17c Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Fri, 24 Aug 2012 15:47:12 +0200
Subject: [PATCH] OCaml (non-)extraction of ghost code
---
src/whyml/mlw_ocaml.ml | 16 ++++++++++++----
1 file changed, 12 insertions(+), 4 deletions(-)
diff --git a/src/whyml/mlw_ocaml.ml b/src/whyml/mlw_ocaml.ml
index 59c176c14a..431b556693 100644
--- a/src/whyml/mlw_ocaml.ml
+++ b/src/whyml/mlw_ocaml.ml
@@ -540,7 +540,9 @@ open Mlw_decl
open Mlw_module
let print_its info fmt ts = print_ts info fmt ts.its_pure
-let print_pv info fmt pv = print_lident info fmt pv.pv_vs.vs_name
+let print_pv info fmt pv =
+ if pv.pv_vtv.vtv_ghost then fprintf fmt "((* ghost *))" else
+ print_lident info fmt pv.pv_vs.vs_name
let print_ps info fmt ps = print_lident info fmt ps.ps_name
let print_lv info fmt = function
| LetV pv -> print_pv info fmt pv
@@ -591,6 +593,7 @@ let print_ity info = print_ity_node false info
let print_vtv info fmt vtv = print_ity info fmt vtv.vtv_ity
let print_pvty info fmt pv =
+ if pv.pv_vtv.vtv_ghost then fprintf fmt "((* ghost *))" else
fprintf fmt "@[(%a:@ %a)@]"
(print_lident info) pv.pv_vs.vs_name (print_vtv info) pv.pv_vtv
@@ -607,7 +610,10 @@ let ity_mark = ity_pur Mlw_wp.ts_mark []
let rec print_expr info fmt e = print_lexpr 0 info fmt e
-and print_lexpr pri info fmt e = match e.e_node with
+and print_lexpr pri info fmt e =
+ if vty_ghost e.e_vty then
+ fprintf fmt "((* ghost *))"
+ else match e.e_node with
| Elogic t ->
fprintf fmt "(%a)" (print_term info) t
| Evalue v ->
@@ -616,6 +622,8 @@ and print_lexpr pri info fmt e = match e.e_node with
print_ps info fmt a
| Eapp (e,v,_) ->
fprintf fmt "(%a@ %a)" (print_lexpr pri info) e (print_pv info) v
+ | Elet ({ let_expr = e1 }, e2) when vty_ghost e1.e_vty ->
+ print_expr info fmt e2
| Elet ({ let_sym = LetV pv }, e2)
when ity_equal pv.pv_vtv.vtv_ity ity_mark ->
print_expr info fmt e2
@@ -656,9 +664,9 @@ and print_lexpr pri info fmt e = match e.e_node with
| Eabsurd ->
fprintf fmt "assert false (* absurd *)"
| Eassert _ ->
- fprintf fmt "() (* assert *)"
+ fprintf fmt "((* assert *))"
| Eghost _ ->
- fprintf fmt "() (* ghost *)"
+ assert false
| Eany _ ->
fprintf fmt "@[(%a :@ %a)@]" to_be_implemented "any"
(print_vty info) e.e_vty
--
GitLab