source: extracted/blocks.ml @ 2797

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 2.5 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open State
108
109open Bind_new
110
111open BindLists
112
113(** val bindNewP : Monad.monadPred **)
114let bindNewP =
115  Monad.Mk_MonadPred
116
117(** val split_on_last :
118    'a1 List.list -> ('a1 List.list, 'a1) Types.prod Types.option **)
119let split_on_last x =
120  List.foldr (fun el acc ->
121    match acc with
122    | Types.None -> Types.Some { Types.fst = List.Nil; Types.snd = el }
123    | Types.Some pr ->
124      Types.Some { Types.fst = (List.Cons (el, pr.Types.fst)); Types.snd =
125        pr.Types.snd }) Types.None x
126
127type step_block =
128  (((__ -> Joint.joint_seq) List.list, __ -> Joint.joint_step) Types.prod,
129  Joint.joint_seq List.list) Types.prod
130
131type fin_block = (Joint.joint_seq List.list, Joint.joint_fin_step) Types.prod
132
133type bind_step_block = (Registers.register, step_block) Bind_new.bind_new
134
135type bind_fin_block = (Registers.register, fin_block) Bind_new.bind_new
136
137type bind_seq_list =
138  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
139
140(** val add_dummy_variance : 'a2 List.list -> ('a1 -> 'a2) List.list **)
141let add_dummy_variance x =
142  List.map (fun x0 x1 -> x0) x
143
144(** val ensure_step_block :
145    Joint.params -> AST.ident List.list -> Joint.joint_seq List.list ->
146    step_block **)
147let ensure_step_block p g l =
148  match split_on_last l with
149  | Types.None ->
150    { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
151      Joint.Step_seq
152      (Joint.nOOP (Joint.stmt_pars__o__uns_pars__o__u_pars p) g)) };
153      Types.snd = List.Nil }
154  | Types.Some pr ->
155    { Types.fst = { Types.fst = (add_dummy_variance pr.Types.fst);
156      Types.snd = (fun x -> Joint.Step_seq pr.Types.snd) }; Types.snd =
157      List.Nil }
158
159(** val map_eval : ('a1 -> 'a2) List.list -> 'a1 -> 'a2 List.list **)
160let map_eval l x =
161  List.map (fun f -> f x) l
162
Note: See TracBrowser for help on using the repository browser.