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
78
79
80
81
type var = Lang.F.var
type tau = Lang.F.tau
type field = Lang.field
type lfun = Lang.lfun
type term = Lang.F.term
type pred = Lang.F.pred
type repr =
| True
| False
| And of term list
| Or of term list
| Not of term
| Imply of term list * term
| If of term * term * term
| Var of var
| Int of Z.t
| Real of Q.t
| Add of term list
| Mul of term list
| Div of term * term
| Mod of term * term
| Eq of term * term
| Neq of term * term
| Lt of term * term
| Leq of term * term
| Times of Z.t * term
| Call of lfun * term list
| Field of term * field
| Record of (field * term) list
| Cst of tau * term
| Get of term * term
| Set of term * term * term
| HigherOrder
module L = Qed.Logic
let term e : repr =
match Lang.F.repr e with
| L.True -> True
| L.False -> False
| L.And ts -> And ts
| L.Or ts -> Or ts
| L.Not t -> Not t
| L.If(a,b,c) -> If(a,b,c)
| L.Imply(hs,p) -> Imply(hs,p)
| L.Kint z -> Int z
| L.Kreal r -> Real r
| L.Add ts -> Add ts
| L.Mul ts -> Mul ts
| L.Div(a,b) -> Div(a,b)
| L.Mod(a,b) -> Mod(a,b)
| L.Eq(a,b) -> Eq(a,b)
| L.Neq(a,b) -> Neq(a,b)
| L.Lt(a,b) -> Lt(a,b)
| L.Leq(a,b) -> Leq(a,b)
| L.Times(k,t) -> Times(k,t)
| L.Fun(f,ts) -> Call(f,ts)
| L.Rget(r,f) -> Field(r,f)
| L.Rdef fvs -> Record fvs
| L.Acst(t,v) -> Cst(t,v)
| L.Aget(a,k) -> Get(a,k)
| L.Aset(a,k,v) -> Set(a,k,v)
| L.Fvar x -> Var x
| L.Bvar _ | L.Bind _ | L.Apply _
-> HigherOrder
let pred p = term (Lang.F.e_prop p)
let lfun = Lang.name_of_lfun
let field = Lang.name_of_field