blob: facff72697c919544ca4a5d7582e9305a4732669 (
plain)
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, Collège de France and Inria Paris *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 of *)
(* the License, or (at your option) any later version. *)
(* This file is also distributed under the terms of the *)
(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Known built-in functions *)
Require Import String Coqlib.
Require Import AST Integers Floats Values.
Require Export Builtins0 Builtins1.
Inductive builtin_function : Type :=
| BI_standard (b: standard_builtin)
| BI_platform (b: platform_builtin).
Definition builtin_function_sig (b: builtin_function) : signature :=
match b with
| BI_standard b => standard_builtin_sig b
| BI_platform b => platform_builtin_sig b
end.
Definition builtin_function_sem (b: builtin_function) : builtin_sem (sig_res (builtin_function_sig b)) :=
match b with
| BI_standard b => standard_builtin_sem b
| BI_platform b => platform_builtin_sem b
end.
Definition lookup_builtin_function (name: string) (sg: signature) : option builtin_function :=
match lookup_builtin standard_builtin_sig name sg standard_builtin_table with
| Some b => Some (BI_standard b)
| None =>
match lookup_builtin platform_builtin_sig name sg platform_builtin_table with
| Some b => Some (BI_platform b)
| None => None
end end.
Lemma lookup_builtin_function_sig:
forall name sg b, lookup_builtin_function name sg = Some b -> builtin_function_sig b = sg.
Proof.
unfold lookup_builtin_function; intros.
destruct (lookup_builtin standard_builtin_sig name sg standard_builtin_table) as [bs|] eqn:E.
inv H. simpl. eapply lookup_builtin_sig; eauto.
destruct (lookup_builtin platform_builtin_sig name sg platform_builtin_table) as [bp|] eqn:E'.
inv H. simpl. eapply lookup_builtin_sig; eauto.
discriminate.
Qed.
|
