pgm_wp.ml 2.73 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
19
20

open Why
21
22
23
24
open Ident
open Term
open Decl
open Theory
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
25
26
27
28
open Pgm_itree

module E = Pgm_effect

29
30
let errorm = Pgm_typing.errorm

Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
31
32
33
34
35
36
37
38
(* translation to intermediate trees and effect inference *)

let rec expr e =
  let ty = e.Pgm_ttree.expr_type in
  let loc = e.Pgm_ttree.expr_loc in
  let d, ef = expr_desc loc ty e.Pgm_ttree.expr_desc in
  { expr_desc = d; expr_type = ty; expr_effect = ef; expr_loc = loc }

39
40
and expr_desc _loc _ty = function
  | Pgm_ttree.Elogic _t ->
41
      assert false (*TODO*)
42
43
44
45
  | Pgm_ttree.Eapply _ as _e ->
      assert false (*TODO*)
  | Pgm_ttree.Efun (_bl, (_p, e, _q)) ->
      let _e = expr e in
46
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
47
48
49
50
51
52
53
  | _ -> 
      assert false (*TODO*)

and recfun _ =
  assert false (*TODO*)

(* weakest preconditions *)
54

55
56
57
58
59
60
61
62
63
64
let wp _l _e = f_true (* TODO *)

let wp_recfun _l _def = f_true (* TODO *)

let add_wp_decl uc l f =
  let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
  let d = create_prop_decl Pgoal pr f in
  add_decl uc d

let decl uc = function
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
65
66
  | Pgm_ttree.Dlet (l, e) ->
      let e = expr e in
67
68
      let f = wp l e in
      add_wp_decl uc l f
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
69
70
71
72
73
74
  | Pgm_ttree.Dletrec dl ->
      let add_one uc (l, def) = 
	let def = recfun def in
	let f = wp_recfun l def in 
	add_wp_decl uc l f 
      in
75
      List.fold_left add_one uc dl
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
76
  | Pgm_ttree.Dparam _ ->
77
78
79
80
      uc

let file uc dl =
  let uc = List.fold_left decl uc dl in
81
  Theory.close_theory uc