bts12244.ml 2.97 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
(**************************************************************************)
(*                                                                        *)
(*  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
MARCHE Claude's avatar
MARCHE Claude committed
53
let goal_id = Decl.create_prsymbol (Ident.id_fresh "G")
54 55 56 57 58 59 60
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
61
let split = Trans.lookup_transform_l "split_goal_right" env
62 63 64 65


let task_inline = Trans.apply inline task

MARCHE Claude's avatar
MARCHE Claude committed
66
let task_split =
67 68 69 70
  match Trans.apply split task with
    | [t] -> t
    | _ -> assert false

MARCHE Claude's avatar
MARCHE Claude committed
71 72 73 74 75 76 77 78 79 80 81 82
let task_checksum t =
  fprintf str_formatter "%a@." Pretty.print_task t;
  let s = flush_str_formatter () in
  Digest.to_hex (Digest.string s)

let sum = task_checksum task

let sum_inline = task_checksum task_inline

let sum_split = task_checksum task_split

let () = printf "@[task == task_inline ? %b   same checksums ? %b@]@."
83
  (Task.task_equal task task_inline) (sum = sum_inline)
MARCHE Claude's avatar
MARCHE Claude committed
84 85

let () = printf "@[task == task_split ? %b    same checksums ? %b@]@."
86
  (Task.task_equal task task_split) (sum = sum_split)
MARCHE Claude's avatar
MARCHE Claude committed
87

88