Source file AstInduction.ml
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
open Ast
open Datatypes
open List0
open ListDef
(** val lexp_subexps : 'a1 lexp -> 'a1 exp list **)
let rec lexp_subexps = function
| LE_aux (aux, _) ->
(match aux with
| LE_deref x -> x :: []
| LE_app (_, xs) -> xs
| LE_tuple ls -> concat (map lexp_subexps ls)
| LE_vector_concat ls -> concat (map lexp_subexps ls)
| LE_vector (l0, x) -> app (lexp_subexps l0) (x :: [])
| LE_vector_range (l0, n, m) -> app (lexp_subexps l0) (n :: (m :: []))
| LE_field (l0, _) -> lexp_subexps l0
| _ -> [])
(** val take_drop : Big_int_Z.big_int -> 'a1 list -> 'a1 list * 'a1 list **)
let rec take_drop n xs =
(fun fO fS n -> if Big_int_Z.sign_big_int n <= 0 then fO ()
else fS (Big_int_Z.pred_big_int n))
(fun _ -> ([], xs))
(fun m ->
match xs with
| [] -> ([], [])
| x :: xs0 -> let (ys, zs) = take_drop m xs0 in ((x :: ys), zs))
n
(** val update_lexp_subexps :
'a1 exp list -> 'a1 lexp -> 'a1 lexp * 'a1 exp list **)
let rec update_lexp_subexps xs l = match l with
| LE_aux (aux, annot) ->
(match aux with
| LE_deref _ ->
(match xs with
| [] -> (l, xs)
| y :: ys -> ((LE_aux ((LE_deref y), annot)), ys))
| LE_app (id, args) ->
let (ys, zs) = take_drop (length args) xs in
((LE_aux ((LE_app (id, ys)), annot)), zs)
| LE_tuple ls ->
let (ls0, xs0) =
fold_left (fun acc l0 ->
let (ls0, xs0) = acc in
let (l1, xs1) = update_lexp_subexps xs0 l0 in
((app ls0 (l1 :: [])), xs1)) ls ([], xs)
in
((LE_aux ((LE_tuple ls0), annot)), xs0)
| LE_vector_concat ls ->
let (ls0, xs0) =
fold_left (fun acc l0 ->
let (ls0, xs0) = acc in
let (l1, xs1) = update_lexp_subexps xs0 l0 in
((app ls0 (l1 :: [])), xs1)) ls ([], xs)
in
((LE_aux ((LE_vector_concat ls0), annot)), xs0)
| LE_vector (l0, _) ->
let (l1, l2) = update_lexp_subexps xs l0 in
(match l2 with
| [] -> (l0, [])
| n :: xs0 -> ((LE_aux ((LE_vector (l1, n)), annot)), xs0))
| LE_vector_range (l0, _, _) ->
let (l1, l2) = update_lexp_subexps xs l0 in
(match l2 with
| [] -> (l0, [])
| n :: l3 ->
(match l3 with
| [] -> (l0, [])
| m :: xs0 -> ((LE_aux ((LE_vector_range (l1, n, m)), annot)), xs0)))
| LE_field (l0, f) ->
let (l', ys) = update_lexp_subexps xs l0 in
((LE_aux ((LE_field (l', f)), annot)), ys)
| _ -> (l, xs))