core.ml 9.84 KB
Newer Older
Frontull Samuel's avatar
Frontull Samuel committed
1
2
module L = List

3
let _ROOT = "e"
Frontull Samuel's avatar
Frontull Samuel committed
4

5
6
7
8
9
10
11
let _APP_L = "1"

let _APP_R = "2"

let _LAM = "1"

type term = Var of string | Lam of string * term | App of term * term
Frontull Samuel's avatar
Frontull Samuel committed
12

13
14
15
16
17
18
let label = ref 0

let next_label () =
  label := !label + 1;
  "C" ^ string_of_int !label

Frontull Samuel's avatar
Frontull Samuel committed
19
20
type var = string

21
22
23
type label = string

(** labeled lambda term  *)
24
type l_term =
Frontull Samuel's avatar
Frontull Samuel committed
25
  | LVar of var
26
  | LLam of label * var * l_term
27
28
  | LApp of l_term * l_term

29
(** lambda term to labeled lambda term *)
Frontull Samuel's avatar
Frontull Samuel committed
30
let rec term_to_l_term = function
31
  | Var x -> LVar x
32
  | Lam (x, e) -> LLam (next_label (), x, term_to_l_term e)
33
34
  | App (e1, e2) -> LApp (term_to_l_term e1, term_to_l_term e2)

35
(** labeled lambda term to lambda term  *)
Frontull Samuel's avatar
Frontull Samuel committed
36
37
let rec l_term_to_term = function
  | LVar v -> Var v
Frontull Samuel's avatar
Frontull Samuel committed
38
  | LLam (_, v, t) -> Lam (v, l_term_to_term t)
Frontull Samuel's avatar
Frontull Samuel committed
39
40
  | LApp (e1, e2) -> App (l_term_to_term e1, l_term_to_term e2)

41
(** rename the free occurrences of variable {e x} in {e term} to {e y}  *)
Frontull Samuel's avatar
Frontull Samuel committed
42
let rec rename term x y =
Frontull Samuel's avatar
Frontull Samuel committed
43
  match term with
44
  | LVar s -> if s = x then LVar y else term
Frontull Samuel's avatar
Frontull Samuel committed
45
46
  | LLam (l, s, t) -> if s = x then term else LLam (l, s, rename t x y)
  | LApp (e1, e2) -> LApp (rename e1 x y, rename e2 x y)
Frontull Samuel's avatar
Frontull Samuel committed
47

48
(** assign default names (depending on the position of their binder) to each variable  *)
Frontull Samuel's avatar
Frontull Samuel committed
49
let rec default_names_r pos = function
50
  | LVar v -> LVar v
Frontull Samuel's avatar
Frontull Samuel committed
51
  | LLam (l, v, t) ->
Frontull Samuel's avatar
Frontull Samuel committed
52
      let vf = "x_" ^ pos in
Frontull Samuel's avatar
Frontull Samuel committed
53
      LLam (l, vf, default_names_r (pos ^ _LAM) (rename t v vf))
54
  | LApp (e1, e2) ->
Frontull Samuel's avatar
Frontull Samuel committed
55
      LApp (default_names_r (pos ^ _APP_L) e1, default_names_r (pos ^ _APP_R) e2)
Frontull Samuel's avatar
Frontull Samuel committed
56

Frontull Samuel's avatar
Frontull Samuel committed
57
let default_names term = default_names_r _ROOT term
Frontull Samuel's avatar
Frontull Samuel committed
58

59
60
61
(** remove element {e x} from list {e l1}  *)
let remove l1 x =
  L.fold_left (fun acc hd -> if hd = x then acc else hd :: acc) [] l1
Frontull Samuel's avatar
Frontull Samuel committed
62
63
64

(** Extract the free variables in a {e a_term}  *)
let rec free_variables = function
65
  | LVar x -> [ LVar x ]
66
  | LLam (_, x, e) -> remove (free_variables e) (LVar x)
67
  | LApp (e1, e2) -> free_variables e1 @ free_variables e2
Frontull Samuel's avatar
Frontull Samuel committed
68
69
70
71
72
73
74

let counter = ref 0

let next_fresh () =
  counter := !counter + 1;
  "p_" ^ string_of_int !counter

Frontull Samuel's avatar
cleanup    
Frontull Samuel committed
75
(** replace every var x occurrence by var y  *)
Frontull Samuel's avatar
Frontull Samuel committed
76
77
let rec subst m x y =
  match m with
78
  | LVar z -> if z = x then LVar y else m
Frontull Samuel's avatar
Frontull Samuel committed
79
  | LLam (l, z, e) ->
Frontull Samuel's avatar
Frontull Samuel committed
80
      let z' = if z = x then y else z in
Frontull Samuel's avatar
Frontull Samuel committed
81
      LLam (l, z', subst e x y)
82
  | LApp (e1, e2) -> LApp (subst e1 x y, subst e2 x y)
Frontull Samuel's avatar
Frontull Samuel committed
83
84

(** capture-avoiding substitution  *)
85
let rec casubst m x n =
Frontull Samuel's avatar
Frontull Samuel committed
86
  match m with
87
  | LVar y -> if x = y then n else m
88
89
  | LApp (e1, e2) -> LApp (casubst e1 x n, casubst e2 x n)
  | LLam (l, y, e) ->
Frontull Samuel's avatar
Frontull Samuel committed
90
      if y = x then m
91
92
93
94
95
      else if L.mem (LVar y) (free_variables n) then
        let f = next_fresh () in
        let m' = subst m y f in
        casubst m' x n
      else LLam (l, y, casubst e x n)
Frontull Samuel's avatar
Frontull Samuel committed
96

97
(** apply a beta step  *)
Frontull Samuel's avatar
Frontull Samuel committed
98
let beta = function
Frontull Samuel's avatar
cleanup    
Frontull Samuel committed
99
  | LApp (LLam (_, x, m), n) -> casubst m x n
Frontull Samuel's avatar
Frontull Samuel committed
100
101
  | _ -> failwith "beta: Not a redex."

102
(** compute the intersection of the lists {e l1} and {e l2}  *)
Frontull Samuel's avatar
Frontull Samuel committed
103
104
let intersect l1 l2 = L.filter (fun z -> L.mem z l2) l1

105
(** determine a position of a weak redex in {e term}  *)
106
let rec _weak_redexpos term pos bvs =
Frontull Samuel's avatar
Frontull Samuel committed
107
  match term with
108
  | LApp (LLam (l, v, b), arg) -> (
109
      let fvs = free_variables term in
Frontull Samuel's avatar
Frontull Samuel committed
110
      let f_bvs = intersect fvs bvs in
111
112
      match f_bvs with
      | [] -> pos
113
      | _ ->
114
          let posl = _weak_redexpos (LLam (l, v, b)) (pos ^ _APP_L) bvs in
Frontull Samuel's avatar
Frontull Samuel committed
115
          if posl <> "" then posl else _weak_redexpos arg (pos ^ _APP_R) bvs )
116
  | LApp (e1, e2) ->
117
118
119
      let posl = _weak_redexpos e1 (pos ^ _APP_L) bvs in
      if posl <> "" then posl else _weak_redexpos e2 (pos ^ _APP_R) bvs
  | LLam (_, x, e) -> _weak_redexpos e (pos ^ _LAM) (LVar x :: bvs)
Frontull Samuel's avatar
Frontull Samuel committed
120
121
  | _ -> ""

122
let weak_redexpos term = _weak_redexpos term _ROOT []
Frontull Samuel's avatar
Frontull Samuel committed
123

124
(** check whether {e p} is a prefix of the string {e s}  *)
125
126
127
128
129
let starts_with p s =
  if String.length p <= String.length s then
    String.sub s 0 (String.length p) = p
  else false

130
(** compute a weak reduction step at position {e pos}  *)
Frontull Samuel's avatar
Frontull Samuel committed
131
132
let rec _weak_step term pos p =
  match term with
133
134
  | LApp (LLam (l, v, b), arg) ->
      if p = pos then beta term
135
136
137
      else if starts_with (p ^ _APP_L) pos then
        LApp (_weak_step (LLam (l, v, b)) pos (p ^ _APP_L), arg)
      else LApp (LLam (l, v, b), _weak_step arg pos (p ^ _APP_R))
138
  | LApp (e1, e2) ->
139
140
      LApp (_weak_step e1 pos (p ^ _APP_L), _weak_step e2 pos (p ^ _APP_R))
  | LLam (l, x, e) -> LLam (l, x, _weak_step e pos (p ^ _LAM))
Frontull Samuel's avatar
Frontull Samuel committed
141
142
  | _ -> term

143
let weak_step term pos = _weak_step term pos _ROOT
144

145
(** TRS term  *)
Frontull Samuel's avatar
Frontull Samuel committed
146
147
type trs_term =
  | TVar of string
148
  | TCon of string * (trs_term * string) list
Frontull Samuel's avatar
Frontull Samuel committed
149
150
151
152
153
  | TDes of trs_term * trs_term

(** Extract the name of a variable from a {e a_term}  *)
let vtname = function TVar n -> n | _ -> ""

154
(** compute free variables in a {e trs_term}  *)
Frontull Samuel's avatar
Frontull Samuel committed
155
156
let rec fvar_trsterm = function
  | TVar v -> [ TVar v ]
157
158
159
  | TDes (e1, e2) -> fvar_trsterm e1 @ fvar_trsterm e2
  | TCon (_, fvs) -> L.flatten (L.map (fun x -> fvar_trsterm (fst x)) fvs)

160
let rec maximal_free_subterms xs pos lterm =
161
  if free_variables lterm = [] then [ (lterm, pos) ]
162
163
  else
    match lterm with
164
    | LVar _ -> if L.mem lterm xs then [] else [ (lterm, pos) ]
165
    | LApp (e1, e2) -> (
Frontull Samuel's avatar
Frontull Samuel committed
166
167
168
        (* check if abstracted variables occur in left/right argument *)
        let e1_fvs = intersect xs (free_variables e1) in
        let e2_fvs = intersect xs (free_variables e2) in
169
170
171
        match (e1_fvs, e2_fvs) with
        | [], [] -> [ (lterm, pos) ]
        | [], _ ->
172
            [ (e1, pos ^ _APP_L) ] @ maximal_free_subterms xs (pos ^ _APP_R) e2
173
        | _, [] ->
174
            maximal_free_subterms xs (pos ^ _APP_L) e1 @ [ (e2, pos ^ _APP_R) ]
175
        | _, _ ->
176
177
178
            maximal_free_subterms xs (pos ^ _APP_L) e1
            @ maximal_free_subterms xs (pos ^ _APP_R) e2 )
    | LLam (_, y, e) -> maximal_free_subterms (LVar y :: xs) (pos ^ _LAM) e
Frontull Samuel's avatar
Frontull Samuel committed
179

Frontull Samuel's avatar
Frontull Samuel committed
180
let rec l_term_to_trsterm = function
Frontull Samuel's avatar
Frontull Samuel committed
181
  | LVar x -> TVar x
Frontull Samuel's avatar
Frontull Samuel committed
182
  | LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
Frontull Samuel's avatar
Frontull Samuel committed
183
  | LLam (l, x, e) ->
184
      let cmps = maximal_free_subterms [ LVar x ] _LAM e in
Frontull Samuel's avatar
Frontull Samuel committed
185
      TCon (l, L.map (fun (t, p) -> (l_term_to_trsterm t, p)) cmps)
Frontull Samuel's avatar
Frontull Samuel committed
186

187
188
189
190
191
192
193
194
195
let rec _term_to_pattern lterm ps p =
  if L.mem p ps then LVar ("v_" ^ p) else
  match lterm with
  | LVar _ -> lterm
  | LApp (e1, e2) ->
      LApp (_term_to_pattern e1 ps (p ^ _APP_L),
            _term_to_pattern e2 ps (p ^ _APP_R))
  | LLam (l, x, e) ->
      LLam (l, x, _term_to_pattern e ps (p ^ _LAM))
196

197
198
199
200
let term_to_pattern lterm xs =
  let fs = maximal_free_subterms xs _ROOT lterm in
  let ps = L.map snd fs in
   _term_to_pattern lterm ps _ROOT
201

Frontull Samuel's avatar
Frontull Samuel committed
202
203
type trs_rule = RR of trs_term * trs_term

Frontull Samuel's avatar
Frontull Samuel committed
204
let rec rules = function
205
206
207
  | LVar _ -> []
  | LApp (e1, e2) -> rules e1 @ rules e2
  | LLam (l, x, e) ->
208
209
210
211
      let p = term_to_pattern e [ LVar x ] in
      let rhs = l_term_to_trsterm p in
      let lhs = l_term_to_trsterm (LLam (l, x, p)) in
      RR (TDes (lhs, TVar x), rhs) :: rules e
212

Frontull Samuel's avatar
Frontull Samuel committed
213
let rec _redexpos pos = function
Frontull Samuel's avatar
Frontull Samuel committed
214
215
  | TDes (TCon (_, _), _) -> pos
  | TDes (e1, e2) ->
Frontull Samuel's avatar
Frontull Samuel committed
216
217
      let posl = _redexpos (pos ^ _APP_L) e1 in
      if posl != "" then posl else _redexpos (pos ^ _APP_R) e2
218
219
  | TCon (_, tcs) ->
      if tcs = [] then ""
220
221
222
223
      else
        let xs =
          L.filter
            (fun y -> y != "")
224
            (L.map (fun x -> _redexpos (pos ^ snd x) (fst x)) tcs)
225
226
        in
        if L.length xs > 0 then L.hd xs else ""
Frontull Samuel's avatar
Frontull Samuel committed
227
228
  | _ -> ""

Frontull Samuel's avatar
Frontull Samuel committed
229
let redexpos trsterm = _redexpos _ROOT trsterm
Frontull Samuel's avatar
Frontull Samuel committed
230

231
let rec zip_c a b =
Frontull Samuel's avatar
Frontull Samuel committed
232
233
  match (a, b) with
  | TVar _, _ -> [ (a, b) ]
234
  | TDes (a1, a2), TDes (b1, b2) -> zip_c a1 b1 @ zip_c a2 b2
235
  | TCon (_, a1), TCon (_, b1) ->
Frontull Samuel's avatar
Frontull Samuel committed
236
237
      L.flatten
        (L.map
238
           (fun x -> zip_c (fst x) (snd x))
Frontull Samuel's avatar
Frontull Samuel committed
239
           (L.combine (L.map fst a1) (L.map fst b1)))
240
  | _, _ -> failwith "zip_c not same structure."
241

242
243
244
let rec zip_cs rcs tcs =
  match (rcs, tcs) with
  | r :: rs, t :: ts -> zip_c (fst r) (fst t) @ zip_cs rs ts
245
  | [], [] -> []
246
  | _, _ -> failwith "zip_cs not same length."
247

248
249
let rec subst_var v = function
  | (x, n) :: xs -> if v = x then n else subst_var v xs
Frontull Samuel's avatar
Frontull Samuel committed
250
251
  | [] -> v

252
253
254
255
256
257
258
259
260
let rec subst tterm s_pairs =
  match tterm with
  | TVar _ -> subst_var tterm s_pairs
  | TDes (e1, e2) -> TDes (subst e1 s_pairs, subst e2 s_pairs)
  | TCon (l, tcs) ->
      TCon (l, L.map (fun z -> (subst (fst z) s_pairs, snd z)) tcs)

let rec rewrite rules term =
  match (rules, term) with
Frontull Samuel's avatar
Frontull Samuel committed
261
262
  | RR (TDes (TCon (l1, rcs), x), r) :: xs, TDes (TCon (l2, tcs), arg) ->
      if l1 = l2 then subst r ((x, arg) :: zip_cs rcs tcs) else rewrite xs term
263
  | [], _ -> term
Frontull Samuel's avatar
Frontull Samuel committed
264
  | _, _ -> failwith "Not a rule or not a trsterm redex."
Frontull Samuel's avatar
Frontull Samuel committed
265

Frontull Samuel's avatar
Frontull Samuel committed
266
let rec _rewrite_step tterm rules pos p =
267
268
  match tterm with
  | TDes (TCon (_, _), _) -> if p = pos then rewrite rules tterm else tterm
Frontull Samuel's avatar
Frontull Samuel committed
269
  | TDes (e1, e2) ->
Frontull Samuel's avatar
Frontull Samuel committed
270
271
272
      TDes
        ( _rewrite_step e1 rules pos (p ^ _APP_L),
          _rewrite_step e2 rules pos (p ^ _APP_R) )
273
274
  | TCon (l, fvs) ->
      TCon
Frontull Samuel's avatar
Frontull Samuel committed
275
276
277
278
        ( l,
          L.map
            (fun z -> (_rewrite_step (fst z) rules pos (p ^ snd z), snd z))
            fvs )
279
  | _ -> tterm
Frontull Samuel's avatar
Frontull Samuel committed
280

281
let rewrite_step xs t pos = _rewrite_step t xs pos _ROOT
282

Frontull Samuel's avatar
Frontull Samuel committed
283
let rec find_rule rules label =
284
  match rules with
285
  | RR (TDes (TCon (l, _), _), _) :: xs ->
Frontull Samuel's avatar
Frontull Samuel committed
286
287
      if l = label then L.hd rules else find_rule xs label
  | _ :: xs -> find_rule xs label
Frontull Samuel's avatar
Frontull Samuel committed
288
289
  | [] -> failwith "No rule with such label."

290
291
292
293
let counter_projection = ref 0

let next_fresh_2 () =
  counter_projection := !counter_projection + 1;
294
  "v" ^ string_of_int !counter_projection
295

Frontull Samuel's avatar
Frontull Samuel committed
296
let rec trsterm_to_lterm xs = function
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
  | TVar x -> LVar x
  | TDes (e1, e2) -> LApp (trsterm_to_lterm xs e1, trsterm_to_lterm xs e2)
  | TCon (l, tcs) -> (
      let rule = find_rule xs l in
      match rule with
      | RR (TDes (TCon (_, rcs), var), rhs) ->
          if L.mem var (L.flatten (L.map (fun f -> fvar_trsterm (fst f)) tcs))
          then
            let f = next_fresh_2 () in
            let r' = subst rhs [ (var, TVar f) ] in
            LLam (l, f, trsterm_to_lterm xs (subst r' (zip_cs rcs tcs)))
          else
            LLam
              (l, vtname var, trsterm_to_lterm xs (subst rhs (zip_cs rcs tcs)))
      | _ -> failwith "No rule with such label." )