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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
(* $Id$ *)
open Names
open Term
open Sign
open Pmisc
open Putil
open Ptype
open Past
(* on redéfinit add_sign pour éviter de construire des environnements
* avec des doublons (qui font planter la résolution des implicites !) *)
(* VERY UGLY!! find some work around *)
let modify_sign id t s =
fold_named_context
(fun ((x,b,ty) as d) sign ->
if x=id then add_named_decl (x,b,t) sign else add_named_decl d sign)
s ~init:empty_named_context
let add_sign (id,t) s =
try
let _ = lookup_named id s in
modify_sign id t s
with Not_found ->
add_named_decl (id,None,t) s
let cast_set c = mkCast (c, mkSet)
let set = mkCast (mkSet, mkType Univ.prop_univ)
(* [cci_sign_of env] construit un environnement pour CIC ne comprenant que
* les objets fonctionnels de l'environnement de programes [env]
*)
let cci_sign_of ren env =
Penv.fold_all
(fun (id,v) sign ->
match v with
| Penv.TypeV (Ref _ | Array _) -> sign
| Penv.TypeV v ->
let ty = Pmonad.trad_ml_type_v ren env v in
add_sign (id,cast_set ty) sign
| Penv.Set -> add_sign (id,set) sign)
env (Global.named_context ())
(* [sign_meta ren env fadd ini]
* construit un environnement pour CIC qui prend en compte les variables
* de programme.
* pour cela, cette fonction parcours tout l'envrionnement (global puis
* local [env]) et pour chaque déclaration, ajoute ce qu'il faut avec la
* fonction [fadd] s'il s'agit d'un mutable et directement sinon,
* en partant de [ini].
*)
let sign_meta ren env fast ini =
Penv.fold_all
(fun (id,v) sign ->
match v with
| Penv.TypeV (Ref _ | Array _ as v) ->
let ty = Pmonad.trad_imp_type ren env v in
fast sign id ty
| Penv.TypeV v ->
let ty = Pmonad.trad_ml_type_v ren env v in
add_sign (id,cast_set ty) sign
| Penv.Set -> add_sign (id,set) sign)
env ini
let add_sign_d dates (id,c) sign =
let sign =
List.fold_left (fun sign d -> add_sign (at_id id d,c) sign) sign dates
in
add_sign (id,c) sign
let sign_of add ren env =
sign_meta ren env
(fun sign id c -> let c = cast_set c in add (id,c) sign)
(Global.named_context ())
let result_of sign = function
None -> sign
| Some (id,c) -> add_sign (id, cast_set c) sign
let before_after_result_sign_of res ren env =
let dates = "" :: Prename.all_dates ren in
result_of (sign_of (add_sign_d dates) ren env) res
let before_after_sign_of ren =
let dates = "" :: Prename.all_dates ren in
sign_of (add_sign_d dates) ren
let before_sign_of ren =
let dates = Prename.all_dates ren in
sign_of (add_sign_d dates) ren
let now_sign_of =
sign_of (add_sign_d [])
(* environnement après traduction *)
let trad_sign_of ren =
sign_of
(fun (id,c) sign -> add_sign (Prename.current_var ren id,c) sign)
ren
|
