source: extracted/lTL_semantics.ml @ 2829

Last change on this file since 2829 was 2829, checked in by sacerdot, 7 years ago

Semantics files committed.

File size: 1.4 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
17open ExtraGlobalenvs
18
19open I8051bis
20
21open BEMem
22
23open Events
24
25open IOMonad
26
27open IO
28
29open Extra_bool
30
31open Coqlib
32
33open Values
34
35open FrontEndVal
36
37open GenMem
38
39open FrontEndMem
40
41open Globalenvs
42
43open Joint_semantics
44
45open SemanticsUtils
46
47open String
48
49open Sets
50
51open Listb
52
53open LabelledObjects
54
55open BitVectorTrie
56
57open Graphs
58
59open I8051
60
61open Order
62
63open Registers
64
65open CostLabel
66
67open Hide
68
69open Proper
70
71open PositiveMap
72
73open Deqsets
74
75open ErrorMessages
76
77open PreIdentifiers
78
79open Errors
80
81open Extralib
82
83open Lists
84
85open Identifiers
86
87open Integers
88
89open AST
90
91open Division
92
93open Exp
94
95open Arithmetic
96
97open Setoids
98
99open Monad
100
101open Option
102
103open Extranat
104
105open Vector
106
107open Div_and_mod
108
109open Jmeq
110
111open Russell
112
113open List
114
115open Util
116
117open FoldStuff
118
119open BitVector
120
121open Types
122
123open Bool
124
125open Relations
126
127open Nat
128
129open Hints_declaration
130
131open Core_notation
132
133open Pts
134
135open Logic
136
137open Positive
138
139open Z
140
141open BitVectorZ
142
143open Pointers
144
145open ByteValues
146
147open BackEndOps
148
149open Joint
150
151open Joint_LTL_LIN
152
153open Joint_LTL_LIN_semantics
154
155open LTL
156
157(** val lTL_semantics : Joint_semantics.sem_params **)
158let lTL_semantics =
159  SemanticsUtils.sem_graph_params_to_sem_params { SemanticsUtils.sgp_pars =
160    (Joint.gp_to_p__o__stmt_pars__o__uns_pars LTL.lTL);
161    SemanticsUtils.sgp_sup = (fun _ ->
162    Joint_LTL_LIN_semantics.lTL_LIN_semantics) }
163
Note: See TracBrowser for help on using the repository browser.