From 8c721d4863551d1d2a0d7461d5d6a7fc1e26bf7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Claude=20March=C3=A9?= <Claude.Marche@inria.fr>
Date: Tue, 24 May 2011 09:20:04 +0200
Subject: [PATCH] ML example exposing bug 12244

---
 Makefile.in           |  3 ++
 examples/bts12244.ml  | 74 +++++++++++++++++++++++++++++++++++++++++++
 src/ide/session.ml    | 17 +++++-----
 tests/test-claude.why |  2 ++
 4 files changed, 87 insertions(+), 9 deletions(-)
 create mode 100644 examples/bts12244.ml

diff --git a/Makefile.in b/Makefile.in
index ca69d658a..c16b02513 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -933,6 +933,9 @@ test-api: src/why.cma
 	ocaml $(EXTCMA)	src/why.cma -I src examples/use_api.ml \
 	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
 
+bts12244: src/why.cma
+	ocaml $(EXTCMA)	src/why.cma -I src examples/bts12244.ml 
+
 
 ## Examples : Plugins ##
 
diff --git a/examples/bts12244.ml b/examples/bts12244.ml
new file mode 100644
index 000000000..6ac3cda90
--- /dev/null
+++ b/examples/bts12244.ml
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    François Bobot                                                     *)
+(*    Jean-Christophe Filliâtre                                          *)
+(*    Claude Marché                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*******************
+
+This file exposes bug 12244 directly using the API
+
+******************)
+
+open Why
+open Format
+
+
+(* reads the config file *)
+let config : Whyconf.config = Whyconf.read_config None
+
+(* the [main] section of the config file *)
+let main : Whyconf.main = Whyconf.get_main config
+
+(* builds the environment from the [loadpath] *)
+let env : Env.env = Lexer.create_env (Whyconf.loadpath main)
+
+
+let int_theory : Theory.theory = Env.find_theory env ["int"] "Int"
+
+(*
+
+An arithmetic goal: 1 = 2
+
+*)
+
+let one : Term.term = Term.t_const (Term.ConstInt "1")
+let two : Term.term = Term.t_const (Term.ConstInt "2")
+let fmla : Term.term = Term.t_equ one two
+
+let task = Task.use_export None int_theory
+let goal_id = Decl.create_prsymbol (Ident.id_fresh "G") 
+let task = Task.add_prop_decl task Decl.Pgoal goal_id fmla
+
+(*
+let () = printf "@[task:@\n%a@]@." Pretty.print_task task
+*)
+
+let inline = Trans.lookup_transform "inline_goal" env
+let split = Trans.lookup_transform_l "split_goal" env
+
+
+let task_inline = Trans.apply inline task
+
+let () = printf "@[task == task_inline ? %b@]@." (task == task_inline)
+
+let task_split = 
+  match Trans.apply split task with
+    | [t] -> t
+    | _ -> assert false
+
+let () = printf "@[task == task_split ? %b@]@." (task == task_split)
+
diff --git a/src/ide/session.ml b/src/ide/session.ml
index 1c0fabc4d..c779a7610 100644
--- a/src/ide/session.ml
+++ b/src/ide/session.ml
@@ -1486,16 +1486,15 @@ let transformation_on_goal g tr =
       let b =
  	match subgoals with
 	  | [task] ->
-              let s1 = task_checksum (get_task g) in
-              let s2 = task_checksum task in
-	      (*
-                eprintf "Transformation returned only one task. sum before = %s, sum after = %s@." (task_checksum g.task) (task_checksum task);
-                eprintf "addresses: %x %x@." (Obj.magic g.task) (Obj.magic task);
-	      *)
-              s1 <> s2
-(*
+              (* let s1 = task_checksum (get_task g) in *)
+              (* let s2 = task_checksum task in *)
+	      (* (\* *)
+              (*   eprintf "Transformation returned only one task. sum before = %s, sum after = %s@." (task_checksum g.task) (task_checksum task); *)
+              (*   eprintf "addresses: %x %x@." (Obj.magic g.task) (Obj.magic task); *)
+	      (* *\) *)
+              (* s1 <> s2 *)
+
                 task != (get_task g)
-*)
 	  | _ -> true
       in
       if b then
diff --git a/tests/test-claude.why b/tests/test-claude.why
index 1c6c308ae..1e73b6903 100644
--- a/tests/test-claude.why
+++ b/tests/test-claude.why
@@ -159,6 +159,8 @@ theory TestInline
 
   use import int.Int 
 
+  goal T : 1 = 2
+
   logic p (x:int) (y:int) = x <= 3 and y <= 7
 
   goal G : p 4 4
-- 
GitLab