source: extracted/blocks.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 2.5 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open Graphs
12
13open I8051
14
15open Order
16
17open Registers
18
19open BitVectorTrie
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 Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
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
113type ('x, 'x0) bind_new_P = __
114
115(** val bindNewP : Monad.monadPred **)
116let bindNewP =
117  Monad.Mk_MonadPred
118
119(** val split_on_last :
120    'a1 List.list -> ('a1 List.list, 'a1) Types.prod Types.option **)
121let split_on_last x =
122  List.foldr (fun el acc ->
123    match acc with
124    | Types.None -> Types.Some { Types.fst = List.Nil; Types.snd = el }
125    | Types.Some pr ->
126      Types.Some { Types.fst = (List.Cons (el, pr.Types.fst)); Types.snd =
127        pr.Types.snd }) Types.None x
128
129type step_block =
130  (((__ -> Joint.joint_seq) List.list, __ -> Joint.joint_step) Types.prod,
131  Joint.joint_seq List.list) Types.prod
132
133type fin_block = (Joint.joint_seq List.list, Joint.joint_fin_step) Types.prod
134
135type bind_step_block = (Registers.register, step_block) Bind_new.bind_new
136
137type bind_fin_block = (Registers.register, fin_block) Bind_new.bind_new
138
139type bind_seq_list =
140  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
141
142(** val add_dummy_variance : 'a2 List.list -> ('a1 -> 'a2) List.list **)
143let add_dummy_variance x =
144  List.map (fun x0 x1 -> x0) x
145
146(** val ensure_step_block :
147    Joint.params -> AST.ident List.list -> Joint.joint_seq List.list ->
148    step_block **)
149let ensure_step_block p g0 l =
150  match split_on_last l with
151  | Types.None ->
152    { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
153      Joint.Step_seq (Joint.nOOP (Joint.stmt_pars__o__uns_pars p) g0)) };
154      Types.snd = List.Nil }
155  | Types.Some pr ->
156    { Types.fst = { Types.fst = (add_dummy_variance pr.Types.fst);
157      Types.snd = (fun x -> Joint.Step_seq pr.Types.snd) }; Types.snd =
158      List.Nil }
159
160type seq_list_in_code = __
161
162(** val map_eval : ('a1 -> 'a2) List.list -> 'a1 -> 'a2 List.list **)
163let map_eval l x =
164  List.map (fun f -> f x) l
165
166type ('x, 'x0) bind_new_instantiates = __
167
Note: See TracBrowser for help on using the repository browser.