core.ml 28.3 KB
Newer Older
Frontull Samuel's avatar
Frontull Samuel committed
1
module L = List
2
open Set
Frontull Samuel's avatar
Frontull Samuel committed
3
open Util
Frontull Samuel's avatar
Frontull Samuel committed
4
open Log
Frontull Samuel's avatar
Frontull Samuel committed
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

(** Simple types  *)
type simple_type =
  | O  (** the base type O *)
  | Imp of simple_type * simple_type
  | UnT  (** untyped *)

(** Syntactic sugar  *)
let imp a b = Imp (a, b)

(** Calculates the order of a type. *)
let rec ord = function
  | UnT -> -1
  | O -> 0
  | Imp (s, t) -> max (ord s + 1) (ord t)

(** Checks if a type is homogeneous.
  A type is said to be homogeneous if for each implication,
  the order of the type on the left hand side is greater equal
  the order of the type on the right hand side.
*)
let rec homogeneous = function
  | O -> true
  | Imp (s, t) -> ord s >= ord t && homogeneous s && homogeneous t
  | UnT -> true

(** Retuns a typ as string *)
let rec typ_to_string = function
  | O -> "o"
  | Imp (l, r) -> "(" ^ typ_to_string l ^ "→" ^ typ_to_string r ^ ")"
  | UnT -> "UnT"

(** Type definition of the a term.
  Each abstraction, application and variable has additional information
  about the type and the position in the term.
*)
type a_term =
42
  | AVar of string * simple_type
43
44
  | ALam of ((string * simple_type) * a_term) * simple_type
  | AApp of a_term * a_term * simple_type
Frontull Samuel's avatar
Frontull Samuel committed
45
46

(* | Beta of (string * simple_type) * a_term * a_term *)
Frontull Samuel's avatar
Frontull Samuel committed
47
48
49
50
51
52
53

(** Returns a list of pairs of type string * typ as string *)
let rec ctx_to_string = function
  | [] -> ""
  | [ x ] -> fst x ^ ":" ^ typ_to_string (snd x)
  | x :: xs -> fst x ^ ":" ^ typ_to_string (snd x) ^ ", " ^ ctx_to_string xs

54
let rec _a_term_to_string term =
Frontull Samuel's avatar
Frontull Samuel committed
55
  match term with
56
  | AVar (s, _) -> s
57
58
59
60
61
62
63
64
65
66
  | ALam (((s, vt), t), tp) -> (
      match vt with
      | UnT -> "λ" ^ s ^ "." ^ _a_term_to_string t
      | _ -> "λ" ^ s ^ "^" ^ typ_to_string vt ^ "." ^ _a_term_to_string t )
  | AApp (x, y, tp) -> (
      match (x, y) with
      | AVar _, AVar _ -> _a_term_to_string x ^ " " ^ _a_term_to_string y
      | AVar _, _ -> _a_term_to_string x ^ " (" ^ _a_term_to_string y ^ ")"
      | _, AVar _ -> "(" ^ _a_term_to_string x ^ ") " ^ _a_term_to_string y
      | _, _ -> "(" ^ _a_term_to_string x ^ ") (" ^ _a_term_to_string y ^ ")" )
Frontull Samuel's avatar
Frontull Samuel committed
67
68

(** Convert a {e a_term} to string  *)
69
let a_term_to_string term = _a_term_to_string term
Frontull Samuel's avatar
Frontull Samuel committed
70

71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
(* let rec _a_term_to_string2 term =
  match term with
  | AVar (s, _) -> s
  | ALam (((s, vt), t), tp) ->
      (String.make 1 '\\') ^ s ^ " -> " ^ _a_term_to_string2 t
  | AApp (x, y, tp) -> (
      match (x, y) with
      | AVar _, AVar _ -> _a_term_to_string2 x ^ " " ^ _a_term_to_string2 y
      | AVar _, _ -> _a_term_to_string2 x ^ " (" ^ _a_term_to_string2 y ^ ")"
      | _, AVar _ -> "(" ^ _a_term_to_string2 x ^ ") " ^ _a_term_to_string2 y
      | _, _ -> "(" ^ _a_term_to_string2 x ^ ") (" ^ _a_term_to_string2 y ^ ")" )

(** Convert a {e a_term} to string  *)
let a_term_to_string2 term = _a_term_to_string2 term *)

Frontull Samuel's avatar
Frontull Samuel committed
86
(** Extract the name of a variable from a {e a_term}  *)
87
let vname = function AVar (n, _) -> n | _ -> ""
Frontull Samuel's avatar
Frontull Samuel committed
88
89
90

(** Extract the type from a {e a_term}  *)
let ttyp = function
91
92
  | AVar (_, typ) -> typ
  | ALam (_, typ) -> typ
93
  | AApp (_, _, typ) -> typ
Frontull Samuel's avatar
Frontull Samuel committed
94
95
96

let rec _assignments tterm =
  match tterm with
97
  | AVar (v, t) -> [ (v, t) ]
98
  | ALam ((xs, t), _) -> xs :: _assignments t
99
  | AApp (x, y, t) -> _assignments x @ _assignments y
Frontull Samuel's avatar
Frontull Samuel committed
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119

(** Extract all the type assignments in a term attached to a given context  *)
let assignments ctx tterm = ctx @ _assignments tterm

let rec _order_consistent ass =
  match ass with
  | [] -> true
  | x :: xs ->
      let fl =
        List.find_all (fun y -> fst y = fst x && ord (snd y) != ord (snd x)) xs
      in
      if fl = [] then _order_consistent xs else false

(** Checks if a term satisfies the safe typing convention (order consistent).
    The type assignments in a term are said to be order consistent,
    if all the types assigned to a variable are of the same order *)
let order_consistent tterm = _order_consistent (_assignments tterm)

(** Extract the free variables in a {e a_term}  *)
let rec free_variables = function
120
  | AVar (x, t) -> [ AVar (x, t) ]
121
122
  | ALam ((x, e), t) -> remove (free_variables e) vname (fst x)
  | AApp (x, y, t) -> free_variables x @ free_variables y
Frontull Samuel's avatar
Frontull Samuel committed
123
124
125
126
127

(** Extract the free variables in a list of {e a_term}s  *)
let rec free_variables_list = function
  | [] -> []
  | x :: xs -> free_variables x @ free_variables_list xs
128

129
130
let rec binders = function
  | AVar (x, t) -> []
Frontull Samuel's avatar
Frontull Samuel committed
131
  | ALam ((x, e), t) -> x :: binders e
132
133
134
135
  | AApp (x, y, t) -> binders x @ binders y

let rec _safe_naming = function
  | [] -> true
Frontull Samuel's avatar
Frontull Samuel committed
136
  | x :: xs -> (not (List.exists (( = ) x) xs)) && _safe_naming xs
137
138
139
140
141
142
143
144
145

let safe_naming tterm =
  let fvs = L.map vname (free_variables tterm) in
  let binders = L.map fst (binders tterm) in
  let vars = fvs @ binders in
  _safe_naming vars

let rec _make_closed fvs term =
  match fvs with
Frontull Samuel's avatar
Frontull Samuel committed
146
147
  | [] -> term
  | x :: xs -> _make_closed xs (ALam ((x, term), UnT))
148
149
150

let make_closed term =
  let fvs = free_variables term in
Frontull Samuel's avatar
Frontull Samuel committed
151
152
153
154
155
156
157
158
  _make_closed
    (L.map
       (fun x ->
         match x with
         | AVar (x, t) -> (x, t)
         | _ -> failwith "Not var type tuple")
       fvs)
    term
159

Frontull Samuel's avatar
Frontull Samuel committed
160
161
162
163
164
165
let rec issafe tterm =
  let fvs = free_variables tterm in
  let minord = L.fold_left min 100 (L.map ord (L.map ttyp fvs)) in
  (* Printf.printf "%d %s:%d\n" minord (a_term_to_string tterm) (ord (ttyp tterm)); *)
  match tterm with
  | AVar _ -> true
166
  | AApp (x, y, typ) -> issafe x && issafe y
167
168
  | ALam ((vs, st), typ) -> (
      minord >= ord typ
169
      && match st with AApp (x, y, _) -> issafe x && issafe y | _ -> issafe st )
Frontull Samuel's avatar
Frontull Samuel committed
170
171

(** Symbols as used in the AST. *)
172
type symbol = VS of string | LS of (string * simple_type) | AS of string
Frontull Samuel's avatar
Frontull Samuel committed
173

174
175
let rec term_nodes_r tterm pos =
  match tterm with
176
177
  | AVar (s, typ) -> [ (pos, VS s, typ) ]
  | ALam ((xs, t), typ) -> (pos, LS xs, typ) :: term_nodes_r t (pos ^ "0")
178
  | AApp (x, y, typ) ->
179
      let app_node = (pos, AS "@", typ) in
180
      app_node :: (term_nodes_r x (pos ^ "0") @ term_nodes_r y (pos ^ "1"))
Frontull Samuel's avatar
Frontull Samuel committed
181

182
let term_nodes tterm = term_nodes_r tterm "e"
Frontull Samuel's avatar
Frontull Samuel committed
183
184

(** Extract the free variables in a {e a_term}  *)
185
let rec _free_variables_pos tterm pos =
Frontull Samuel's avatar
Frontull Samuel committed
186
187
  match tterm with
  | AVar (x, t) -> [ (pos, x) ]
188
  | ALam ((x, y), t) -> remove (_free_variables_pos y (pos ^ "0")) snd (fst x)
189
  | AApp (x, y, t) ->
190
      _free_variables_pos x (pos ^ "0") @ _free_variables_pos y (pos ^ "1")
Frontull Samuel's avatar
Frontull Samuel committed
191
192
193
194
195
196

let free_variables_pos tterm = _free_variables_pos tterm "e"

let rec gentuples pos fvs =
  match fvs with [] -> [] | x :: xs -> [ x; pos ] :: gentuples pos xs

197
let rec b_edges_r tterm pos =
Frontull Samuel's avatar
Frontull Samuel committed
198
199
200
  match tterm with
  | AVar _ -> []
  | ALam ((xs, t), _) ->
201
202
      let fvs = _free_variables_pos t (pos ^ "0") in
      let vs = fst xs in
Frontull Samuel's avatar
Frontull Samuel committed
203
      let bfvs =
204
        L.map fst (L.filter (fun (p, x) -> if x = vs then true else false) fvs)
Frontull Samuel's avatar
Frontull Samuel committed
205
206
      in
      let bpairs = gentuples pos bfvs in
207
      bpairs @ b_edges_r t (pos ^ "0")
208
  | AApp (x, y, typ) -> b_edges_r x (pos ^ "0") @ b_edges_r y (pos ^ "1")
Frontull Samuel's avatar
Frontull Samuel committed
209

210
let b_edges tterm = b_edges_r tterm "e"
Frontull Samuel's avatar
Frontull Samuel committed
211

212
let rec c_edges_r tterm pos =
Frontull Samuel's avatar
Frontull Samuel committed
213
214
215
  match tterm with
  | AVar _ -> []
  | ALam ((xs, t), _) ->
216
217
      let fvs = _free_variables_pos t (pos ^ "0") in
      let vs = fst xs in
Frontull Samuel's avatar
Frontull Samuel committed
218
      let cfvs =
219
        L.map fst (L.filter (fun (p, x) -> if x = vs then false else true) fvs)
Frontull Samuel's avatar
Frontull Samuel committed
220
221
      in
      let cpairs = gentuples pos cfvs in
222
      cpairs @ c_edges_r t (pos ^ "0")
223
  | AApp (x, y, typ) -> c_edges_r x (pos ^ "0") @ c_edges_r y (pos ^ "1")
224
225
226
227
228
229
230
231
232

let c_edges tterm = c_edges_r tterm "e"

let rec a_edges_r tterm pos =
  match tterm with
  | AVar _ -> []
  | ALam ((xs, t), _) -> a_edges_r t (pos ^ "0")
  | AApp (x, y, typ) ->
      let fvs = L.map fst (_free_variables_pos y (pos ^ "1")) in
Frontull Samuel's avatar
Frontull Samuel committed
233
      let pairs = gentuples pos fvs in
234
      pairs @ a_edges_r x (pos ^ "0") @ a_edges_r y (pos ^ "1")
Frontull Samuel's avatar
Frontull Samuel committed
235

236
let a_edges tterm = a_edges_r tterm "e"
Frontull Samuel's avatar
Frontull Samuel committed
237
238
239

let get_node pos nodes = L.filter (fun (p, _, _) -> p = pos) nodes

240
241
(** first n elements of list *)
let rec cutlist l n =
Frontull Samuel's avatar
Frontull Samuel committed
242
243
  match (l, n) with
  | [], _ -> []
244
  | _, 0 -> []
245
  | x :: xs, _ -> x :: cutlist xs (n - 1)
Frontull Samuel's avatar
Frontull Samuel committed
246
247

let node_tostring = function
248
249
250
  | p, AS s, _ -> p ^ "-@"
  | p, LS vs, _ -> p ^ "-λ" ^ fst vs
  | p, VS s, _ -> p ^ "-" ^ s
Frontull Samuel's avatar
Frontull Samuel committed
251

252
type wbp = Empty | Node of string * symbol * simple_type | Comp of wbp list
Frontull Samuel's avatar
Frontull Samuel committed
253

254
let posymtyp_to_node = function p, s, t -> Node (p, s, t)
Frontull Samuel's avatar
Frontull Samuel committed
255
256
257
258
259
260

let append_wbp p n =
  match p with
  | Empty -> n
  | Node _ -> Comp [ p; n ]
  | Comp xs -> Comp (xs @ [ n ])
261
262

(* | Comp xs -> Comp ([p; n]) *)
Frontull Samuel's avatar
Frontull Samuel committed
263
264
265

let rec wbp_tolist = function
  | Empty -> []
266
  | Node (pos, sym, typ) -> [ pos ]
Frontull Samuel's avatar
Frontull Samuel committed
267
  | Comp [] -> []
268
  | Comp (x :: xs) -> wbp_tolist x @ wbp_tolist (Comp xs)
Frontull Samuel's avatar
Frontull Samuel committed
269

270
271
272
273
let rec wbp_tosymlevellist level = function
  | Empty -> []
  | Node (pos, sym, typ) -> [ (pos, sym, level) ]
  | Comp [] -> []
274
275
  | Comp (x :: xs) ->
      wbp_tosymlevellist (level + 1) x @ wbp_tosymlevellist level (Comp xs)
276

277
let wbp_tosymlevellist wbp = wbp_tosymlevellist 0 wbp
278

Frontull Samuel's avatar
Frontull Samuel committed
279
280
let rec wbp_tosymlist = function
  | Empty -> []
281
  | Node (pos, sym, typ) -> [ (pos, sym) ]
Frontull Samuel's avatar
Frontull Samuel committed
282
  | Comp [] -> []
283
  | Comp (x :: xs) -> wbp_tosymlist x @ wbp_tosymlist (Comp xs)
Frontull Samuel's avatar
Frontull Samuel committed
284

285
let sym_tostring = function AS s -> "@" | LS vs -> "λ" ^ fst vs | VS s -> s
Frontull Samuel's avatar
Frontull Samuel committed
286

287
let isapp = function AS _ -> true | _ -> false
Frontull Samuel's avatar
Frontull Samuel committed
288
289

let rec _wbp_tostring path flag =
290
  match (path, flag) with
Frontull Samuel's avatar
Frontull Samuel committed
291
  | Empty, _ -> ""
292
  | Node (pos, sym, typ), _ -> sym_tostring sym ^ "-" ^ pos
Frontull Samuel's avatar
Frontull Samuel committed
293
294
  | Comp _, false -> "[" ^ _wbp_tostring path true ^ "]"
  | Comp [], _ -> ""
295
296
297
  | Comp [ x ], _ -> _wbp_tostring x false
  | Comp (x :: xs), _ ->
      _wbp_tostring x false ^ ", " ^ _wbp_tostring (Comp xs) true
Frontull Samuel's avatar
Frontull Samuel committed
298
299
300
301

let wbp_tostring path = _wbp_tostring path false

let rec _reverse_wbp p flag =
302
  match (p, flag) with
Frontull Samuel's avatar
Frontull Samuel committed
303
  | Empty, _ -> Empty
304
  | Node (pos, sym, typ), _ -> Node (pos, sym, typ)
305
  | Comp xs, false -> _reverse_wbp (Comp (L.rev xs)) true
Frontull Samuel's avatar
Frontull Samuel committed
306
307
308
309
  | Comp xs, _ -> Comp (L.map (fun x -> _reverse_wbp x false) xs)

let reverse_wbp p = _reverse_wbp p false

310
311
312
313
let rec wbp_tail p =
  match p with
  | Empty -> Empty
  | Node (pos, sym, typ) -> Empty
314
315
316
  | Comp (Node _ :: xs) -> Comp xs
  | Comp (x :: xs) -> append_wbp (wbp_tail x) (Comp xs)
  | Comp [] -> Empty
317

Frontull Samuel's avatar
Frontull Samuel committed
318
319
let rec last_wbp = function
  | Empty -> Empty
320
  | Node (pos, sym, typ) -> Node (pos, sym, typ)
Frontull Samuel's avatar
Frontull Samuel committed
321
322
323
324
325
326
  | Comp [ x ] -> last_wbp x
  | Comp (x :: xs) -> last_wbp (Comp xs)
  | _ -> failwith "Wbp wrong."

let rec first_wbp = function
  | Empty -> Empty
327
  | Node (pos, sym, typ) -> Node (pos, sym, typ)
Frontull Samuel's avatar
Frontull Samuel committed
328
329
330
331
  | Comp [ x ] -> first_wbp x
  | Comp (x :: _) -> first_wbp x
  | _ -> failwith "Wbp wrong."

332
let rec wbp_length = function
333
  | Empty -> 0
334
  | Node (pos, sym, typ) -> 1
Frontull Samuel's avatar
Frontull Samuel committed
335
  | Comp [] -> 0
336
  | Comp (x :: xs) -> wbp_length x + wbp_length (Comp xs)
Frontull Samuel's avatar
Frontull Samuel committed
337
338
339

let rec _wbp_sarting_at path i n =
  match path with
340
341
342
343
344
345
  | Comp (x :: xs) ->
      let len = wbp_length x in
      if i + len = n then path
      else if i + len < n then _wbp_sarting_at (Comp xs) (i + len) n
      else _wbp_sarting_at x i n
  | _ -> failwith "wbp_sarting_at not found."
Frontull Samuel's avatar
Frontull Samuel committed
346
347
348
349
350

let wbp_sarting_at path n = _wbp_sarting_at path 0 n

let rec wbp_ending_at path i =
  match path with
351
352
353
354
355
356
  | Comp (x :: xs) ->
      let len = wbp_length x in
      if len = i then x
      else if len < i then wbp_ending_at (Comp xs) (i - len)
      else wbp_ending_at x i
  | _ -> failwith "wbp_ending_at not found."
Frontull Samuel's avatar
Frontull Samuel committed
357
358

let decompose path s e =
359
360
361
  let path_l = wbp_tolist path in
  let w1 = wbp_ending_at path (s + 1) in
  let w1_l = wbp_tolist w1 in
Frontull Samuel's avatar
Frontull Samuel committed
362
  let w1_len = wbp_length w1 in
363
  let l1_idx = s - w1_len in
Frontull Samuel's avatar
Frontull Samuel committed
364
  let l1 = L.nth path_l l1_idx in
365
366
  let w2 = wbp_sarting_at path (e + 1) in
  let w2_l = wbp_tolist w2 in
Frontull Samuel's avatar
Frontull Samuel committed
367
  let w2_len = wbp_length w2 in
368
  let l2_idx = e + w2_len in
Frontull Samuel's avatar
Frontull Samuel committed
369
  let l2 = L.nth path_l l2_idx in
370
371
  let legal = l1 = l2 && w1_l = L.rev w2_l in
  legal
372

373
374
(* if not legal then (
  Printf.printf "\nl1 (%d): %s\n" l1_idx l1;
375
376
377
378
   Printf.printf "w1 (%d): %s\n" s (wbp_tostring w1);
   Printf.printf "cycle: %s\n" (list_tostring (sublist path_l s e) (fun x -> x));
   Printf.printf "w2 (%d): %s\n" e (wbp_tostring w2);
   Printf.printf "l2 (%d): %s\n\n" l2_idx l2;
379
380
   legal
 )
381
382
   else
     legal *)
383
384

let rec find_cycle path pa pb level s e idx =
Frontull Samuel's avatar
Frontull Samuel committed
385
  match path with
386
387
388
  | (px, _, lx) :: (py, sy, ly) :: xs ->
      if px = pa && py = pb then
        find_cycle ((py, sy, ly) :: xs) pa pb level s (e + 1) (idx + 1)
389
390
      else if px = pb && py = pa && level = lx && idx = 0 then [ (s, e + 1) ]
      else if px = pb && py = pa && level = lx && idx = 0 then
391
        find_cycle ((py, sy, ly) :: xs) pa pb level s (e + 1) (idx - 1)
392
      else find_cycle ((py, sy, ly) :: xs) pa pb level s (e + 1) idx
Frontull Samuel's avatar
Frontull Samuel committed
393
394
395
396
397
398
399
400
  | _ -> []

(* iterate over path, check if any cycle
  if no then legal
  otherwise check if call and return paths and discriminants are equal
 *)
let rec detect_cycles path idx =
  match path with
401
402
  | (pa, sa, _) :: (pb, sb, lb) :: xs ->
      let cxs = detect_cycles ((pb, sb, lb) :: xs) (idx + 1) in
Frontull Samuel's avatar
Frontull Samuel committed
403
      if isapp sa && pa ^ "1" = pb then
404
        let c = find_cycle ((pb, sb, lb) :: xs) pa pb lb idx (idx + 1) 0 in
Frontull Samuel's avatar
Frontull Samuel committed
405
        c @ cxs
406
      else cxs
Frontull Samuel's avatar
Frontull Samuel committed
407
408
  | _ -> []

409
let check_cycle path = function s, e -> decompose path s e
Frontull Samuel's avatar
Frontull Samuel committed
410

411
let is_legal = function
412
413
  | Empty -> false
  | path ->
414
415
416
417
418
419
420
      (* Printf.printf "Checking: %s\n" (wbp_tostring path); *)
      let cs = detect_cycles (wbp_tosymlevellist path) 0 in
      (* Printf.printf "Cycles found: %d\n" (L.length cs); *)
      let legal = L.fold_left ( && ) true (L.map (check_cycle path) cs) in
      (* Printf.printf "------------------------------------------------------------------------------------\n\n"; *)
      legal

421
let isvar_node = function Node (_, VS _, _) -> true | _ -> false
422

423
let islam_node = function Node (_, LS _, _) -> true | _ -> false
424

425
let isapp_node = function Node (_, AS _, _) -> true | _ -> false
426

427
428
429
let node_type = function
  | Node (_, x, _) -> x
  | _ -> failwith "node_type: not a node."
430

431
432
433
let node_pos = function
  | Node (p, _, _) -> p
  | _ -> failwith "node_pos: not a node."
434

435
let uniq_cons x xs = if L.mem x xs then xs else x :: xs
436

437
438
439
let linear_list xs = L.fold_right uniq_cons xs []

let rec lambda_composition_1 nodes varpath p_list =
Frontull Samuel's avatar
Frontull Samuel committed
440
  (* Printf.printf "\nlambda_composition_1: (%s)\n\n"  ((wbp_tostring) varpath); *)
441
442
443
444
445
  match p_list with
  | w :: ws ->
      let arg =
        posymtyp_to_node (L.hd (get_node (node_pos (first_wbp w) ^ "1") nodes))
      in
Frontull Samuel's avatar
Frontull Samuel committed
446
447
      (* Printf.printf "arg: (%s)\n"  (wbp_tostring arg);
         Printf.printf "append result: (%s)\n"  ((wbp_tostring) (append_wbp (append_wbp varpath (reverse_wbp w)) arg)); *)
448
      append_wbp (append_wbp varpath (reverse_wbp w)) arg
449
450
451
452
      :: lambda_composition_1 nodes varpath ws
  | [] -> [ Empty ]

let rec lambda_composition_2 nodes lampath p_list =
Frontull Samuel's avatar
Frontull Samuel committed
453
  (* Printf.printf "\nlambda_composition_2: (%s)\n\n"  ((wbp_tostring) lampath); *)
454
455
456
  match p_list with
  | w :: ws ->
      let arg =
457
458
        posymtyp_to_node
          (L.hd (get_node (node_pos (first_wbp lampath) ^ "1") nodes))
459
      in
Frontull Samuel's avatar
Frontull Samuel committed
460
461
      (* Printf.printf "arg: (%s)\n"  (wbp_tostring arg);
         Printf.printf "append result: (%s)\n"  ((wbp_tostring) (append_wbp (append_wbp w (reverse_wbp lampath)) arg)); *)
462
      append_wbp (append_wbp w (reverse_wbp lampath)) arg
463
464
465
      :: lambda_composition_2 nodes lampath ws
  | [] -> [ Empty ]

Frontull Samuel's avatar
Frontull Samuel committed
466
467
468
let rec app_composition nodes appapp applam_list =
  (* Printf.printf "\app_composition: (%s)\n\n"  ((wbp_tostring) p1); *)
  match applam_list with
469
470
471
472
  | y :: ys ->
      let body =
        posymtyp_to_node (L.hd (get_node (node_pos (last_wbp y) ^ "0") nodes))
      in
Frontull Samuel's avatar
Frontull Samuel committed
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
      let newpath = append_wbp (append_wbp appapp (wbp_tail y)) body in
      (* let newpath = append_wbp (append_wbp (reverse_wbp (wbp_tail (reverse_wbp appapp))) y) body in *)
      (* Printf.printf "APP_COMPOSITION\nAA: %s\nAL: %s\nRS: %s\n\n" (wbp_tostring appapp) (wbp_tostring y) (wbp_tostring newpath); *)
      newpath :: app_composition nodes appapp ys
  | [] -> [ Empty ]

let rec app_composition_2 nodes appapp_list applam =
  (* Printf.printf "\app_composition: (%s)\n\n"  ((wbp_tostring) p1); *)
  match appapp_list with
  | y :: ys ->
      let body =
        posymtyp_to_node
          (L.hd (get_node (node_pos (last_wbp applam) ^ "0") nodes))
      in
      let newpath = append_wbp (append_wbp y (wbp_tail applam)) body in
      (* Printf.printf "APP_COMPOSITION 2\nAA: %s\nAL: %s\nRS: %s\n\n" (wbp_tostring y) (wbp_tostring applam) (wbp_tostring newpath); *)
      newpath :: app_composition_2 nodes ys applam
490
491
492
493
  | [] -> [ Empty ]

let composition newpaths acc nodes bedges =
  let comp =
494
495
    L.map
      (fun x ->
496
        let lastnode = last_wbp x in
497
        match node_type lastnode with
498
499
        | VS _ -> (
            let bound = L.filter (fun y -> L.hd y = node_pos lastnode) bedges in
500
            match bound with
501
502
503
504
            | y :: _ ->
                let binder =
                  posymtyp_to_node (L.hd (get_node (llast y) nodes))
                in
Frontull Samuel's avatar
Frontull Samuel committed
505
                let wbps = L.filter (fun z -> last_wbp z = binder) newpaths in
506
                lambda_composition_1 nodes x wbps
507
508
            | [] -> [ Empty ] )
        | LS _ -> (
509
            (* get variables bound by lam node *)
510
511
512
            let vars =
              L.filter (fun y -> L.hd (L.rev y) = node_pos lastnode) bedges
            in
513
514
            let appapp = L.filter (fun x -> isapp_node (last_wbp x)) newpaths in
            let wbps = L.filter (fun y -> last_wbp y = first_wbp x) appapp in
Frontull Samuel's avatar
Frontull Samuel committed
515
            let app_comps = app_composition_2 nodes wbps x in
516
            match vars with
517
            | [] -> app_comps
518
            | _ ->
519
                let vars_pos = L.map (fun x -> L.hd x) vars in
520
                let wbps =
Frontull Samuel's avatar
Frontull Samuel committed
521
522
523
                  L.filter
                    (fun x -> L.mem (node_pos (last_wbp x)) vars_pos)
                    newpaths
524
                in
525
                app_comps @ lambda_composition_2 nodes x wbps )
526
        | AS _ ->
Frontull Samuel's avatar
Frontull Samuel committed
527
            let applam = L.filter (fun z -> islam_node (last_wbp z)) newpaths in
528
            let wbps = L.filter (fun y -> lastnode = first_wbp y) applam in
Frontull Samuel's avatar
Frontull Samuel committed
529
            (* wbps are the @-/x paths starting with an app other end with *)
530
            app_composition nodes x wbps)
Frontull Samuel's avatar
Frontull Samuel committed
531
      acc
532
  in
533
534
  L.filter is_legal (linear_list (L.flatten comp))

535
let rec similar_redex wbp = function
536
  | x :: xs ->
Frontull Samuel's avatar
Frontull Samuel committed
537
538
539
540
      first_wbp wbp = first_wbp x
      && last_wbp wbp = last_wbp x
      && islam_node (last_wbp x)
      || similar_redex wbp xs
541
542
  | [] -> false

543
let rec _well_balanced_paths newpaths acc nodes bedges n =
Frontull Samuel's avatar
Frontull Samuel committed
544
545
  (* Printf.printf "newpaths (%d)\n" (L.length newpaths);
     L.map (fun x -> Printf.printf "newpaths: (%s)\n" x) (L.map (wbp_tostring) newpaths); *)
546
547
  (* Printf.printf "newpaths (%d)\n" (L.length newpaths);
     Printf.printf "accpaths (%d)\n" (L.length acc); *)
Frontull Samuel's avatar
Frontull Samuel committed
548
  (* Printf.printf "---------------------------------------[%d]------------------------------------------\n\n" n; *)
549
550
551
  if n <= 0 then (false, acc)
  else
    let paths = composition newpaths acc nodes bedges in
Frontull Samuel's avatar
Frontull Samuel committed
552
553
554
555
556
557
558
559
    let newpaths =
      L.filter
        (fun x ->
          (not (L.mem x acc))
          && (not (first_wbp x = last_wbp x))
          && not (similar_redex x acc))
        paths
    in
560
561
562
563
    let newacc = acc @ newpaths in
    match newpaths with
    | [] -> (true, acc)
    | _ -> _well_balanced_paths newpaths newacc nodes bedges (n - 1)
564
565
566
567
568
569
570
571
572
573
574

let well_balanced_paths term =
  let nodes = term_nodes term in
  let bedges = b_edges term in
  let apps =
    L.filter (fun x -> match x with _, AS _, _ -> true | _ -> false) nodes
  in
  let acc =
    L.map
      (fun x ->
        match x with
575
576
577
578
579
580
581
        | pa, AS s, typ ->
            Comp
              [
                Node (pa, AS s, typ);
                posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes));
              ]
        | _ -> Empty)
582
583
      apps
  in
Frontull Samuel's avatar
Frontull Samuel committed
584
  let max_compositions = 10 in
585
  let compose = _well_balanced_paths acc acc nodes bedges max_compositions in
Frontull Samuel's avatar
Frontull Samuel committed
586
587
  (* let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd compose) in *)
  (fst compose, snd compose)
588

Frontull Samuel's avatar
Frontull Samuel committed
589
let well_balanced_paths_al term =
590
  let wbp = well_balanced_paths term in
Frontull Samuel's avatar
Frontull Samuel committed
591
592
593
594
595
  let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd wbp) in
  (fst wbp, applam)

let legal_paths term =
  let wbp = well_balanced_paths_al term in
596
597
  (* let wbp = L.filter is_legal wbp in *)
  (fst wbp, L.map wbp_tolist (snd wbp))
Frontull Samuel's avatar
Frontull Samuel committed
598
599
600
601
602
603

let is_scc nodes path =
  let f = get_node (L.hd path) nodes in
  let l = get_node (L.hd (L.rev path)) nodes in
  match f with
  | (_, VS x, _) :: _ -> (
604
      match l with (_, LS vs, _) :: _ -> x = fst vs | _ -> false )
Frontull Samuel's avatar
Frontull Samuel committed
605
606
  | _ -> false

Frontull Samuel's avatar
Frontull Samuel committed
607
let arb_paths ae re be = melt_ll (melt_ll ae re) (L.map L.rev be)
Frontull Samuel's avatar
Frontull Samuel committed
608
609

let rec _scc arb cc stack i max_depth =
Frontull Samuel's avatar
Frontull Samuel committed
610
  if i > max_depth then (false, stack)
Frontull Samuel's avatar
Frontull Samuel committed
611
612
  else
    match cc with
613
    | [] -> (true, stack)
Frontull Samuel's avatar
Frontull Samuel committed
614
    | x :: xs ->
615
        let nl = melt_ll_neq arb [ x ] in
Frontull Samuel's avatar
Frontull Samuel committed
616
617
        _scc arb (xs @ nl) (stack @ nl) (i + 1) max_depth

618
619
620
621
622
let _sim_scc flag re path =
  let p_ra = L.nth (L.rev path) 3 in
  let p_cl = llast path in
  let r_cl = L.filter (fun x -> llast x = p_cl) re in
  match r_cl with
Frontull Samuel's avatar
Frontull Samuel committed
623
  | x :: _ ->
624
625
626
627
628
      let p_ca = lfst x in
      let len_p_ca = String.length p_ca in
      let len_p_ra = String.length p_ra in
      if len_p_ca < len_p_ra then
        let pre = String.sub p_ra 0 len_p_ca in
Frontull Samuel's avatar
Frontull Samuel committed
629
        let suf = String.sub p_ra len_p_ca (len_p_ra - len_p_ca) in
630
        not (flag && pre = p_ca && not (String.contains suf '1'))
631
632
633
      else true
  | _ -> true

Frontull Samuel's avatar
Frontull Samuel committed
634
635
636
637
let harmless_scc sccpath be =
  let first = lfst sccpath in
  let binder = L.filter (fun x -> lfst x = first) be in
  match binder with
Frontull Samuel's avatar
Frontull Samuel committed
638
  | [] -> false
Frontull Samuel's avatar
Frontull Samuel committed
639
  | l :: _ ->
Frontull Samuel's avatar
Frontull Samuel committed
640
      let lam = llast l in
641
      L.mem lam (cutlist sccpath (L.length sccpath - 3))
Frontull Samuel's avatar
Frontull Samuel committed
642

643
let scc tterm max_depth sim =
Frontull Samuel's avatar
Frontull Samuel committed
644
  let ae = a_edges tterm in
645
646
647
  let lp = legal_paths tterm in
  let re = snd lp in
  let normalizing = fst lp in
Frontull Samuel's avatar
Frontull Samuel committed
648
649
650
651
652
  let be = b_edges tterm in
  let arb = arb_paths ae re be in
  let ce = c_edges tterm in
  let cc = melt_ll arb ce in
  let scc_l = _scc arb cc cc 0 max_depth in
Frontull Samuel's avatar
Frontull Samuel committed
653
654
  let paths =
    L.filter
655
      (fun x -> is_scc (term_nodes tterm) x && not (harmless_scc x be))
Frontull Samuel's avatar
Frontull Samuel committed
656
657
      (snd scc_l)
  in
658
  ((fst scc_l, normalizing), L.filter (_sim_scc sim re) paths)
Frontull Samuel's avatar
Frontull Samuel committed
659
660
661
662
663
664
665

let unavoidable_scc sccpath =
  let first = lfst sccpath in
  let last = llast sccpath in
  let first_len = String.length first in
  let last_len = String.length last in
  if first_len < last_len then false else String.sub first 0 last_len = last
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685

(* beta-reduction *)

(** replace every var occurrence by fresh var  *)
let rec subst var fresh term =
  match term with
  | AVar (x, t) -> if x = var then AVar (fresh, t) else term
  | ALam ((xs, e), t) ->
      let xsn = if fst xs = var then (fresh, snd xs) else xs in
      ALam ((xsn, subst var fresh e), t)
  | AApp (e1, e2, t) -> AApp (subst var fresh e1, subst var fresh e2, t)

(** capture-permitting substitution  *)
let rec cpsubst var ex term =
  match term with
  | AVar (x, t) -> if x = var then ex else term
  | ALam ((xs, e), t) ->
      if var = fst xs then term else ALam ((xs, cpsubst var ex e), t)
  | AApp (e1, e2, t) -> AApp (cpsubst var ex e1, cpsubst var ex e2, t)

Frontull Samuel's avatar
Frontull Samuel committed
686
let counter = ref 0
687

Frontull Samuel's avatar
Frontull Samuel committed
688
689
690
let next_fresh () =
  counter := !counter + 1;
  "p_" ^ string_of_int !counter
691

692
(** capture-avoiding substitution  *)
693
let rec _casubst var ex term fvex =
694
  (* Printf.printf "_casubst: %s[%s:=%s]\n" (a_term_to_string term) var (a_term_to_string ex); *)
695
696
697
  match term with
  | AVar (x, t) -> if x = var then ex else term
  | ALam ((xs, e), t) ->
698
      if fst xs = var then term
Frontull Samuel's avatar
Frontull Samuel committed
699
700
      else if L.mem (fst xs) fvex && L.mem var (L.map vname (free_variables e))
      then
701
        (* rename x to fresh *)
Frontull Samuel's avatar
Frontull Samuel committed
702
        let f = next_fresh () in
703
        let rnterm = subst (fst xs) f term in
704
705
706
707
        _casubst var ex rnterm fvex
      else ALam ((xs, _casubst var ex e fvex), t)
  | AApp (e1, e2, t) ->
      AApp (_casubst var ex e1 fvex, _casubst var ex e2 fvex, t)
708
709

let casubst var ex term =
710
  (* Printf.printf "casubst: %s[%s:=%s]\n" (a_term_to_string term) var (a_term_to_string ex); *)
Frontull Samuel's avatar
Frontull Samuel committed
711
  _casubst var ex term (L.map vname (free_variables ex))
712
713
714
715
716
717

(** capture-permitting substitution  *)
let rec cpsubst var ex term =
  match term with
  | AVar (x, t) -> if x = var then ex else term
  | ALam ((xs, e), t) ->
Frontull Samuel's avatar
Frontull Samuel committed
718
719
      if fst xs = var then term else ALam ((xs, cpsubst var ex e), t)
  | AApp (e1, e2, t) -> AApp (cpsubst var ex e1, cpsubst var ex e2, t)
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744

(* Alpha equivalence *)

let rec rename_free_var term x new_name =
  match term with
  | AVar (s, t) -> if s = x then AVar (new_name, t) else term
  | ALam ((xs, e), t) ->
      if x = fst xs then term else ALam ((xs, rename_free_var e x new_name), t)
  | AApp (e1, e2, t) ->
      AApp (rename_free_var e1 x new_name, rename_free_var e2 x new_name, t)

let rec default_names_r term pos =
  match term with
  | AVar (s, t) -> AVar (s, t)
  | ALam ((xs, e), t) ->
      ALam
        ( ( ("x_" ^ pos, snd xs),
            default_names_r (rename_free_var e (fst xs) ("x_" ^ pos)) (pos ^ "0")
          ),
          t )
  | AApp (e1, e2, t) ->
      AApp (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"), t)

let default_names term = default_names_r term "e"

745
let beta subst term =
746
  (* Printf.printf "beta: %s\n" (a_term_to_string term); *)
747
  match term with
748
749
750
751
752
  | AApp (ALam (((var,_), e1), _), e2, _) ->
    (* Printf.printf "subst: %s by %s in %s\n" var (a_term_to_string e2) (a_term_to_string e1); *)
    let res = subst var e2 e1 in
    (* Printf.printf "res: %s\n" (a_term_to_string res); *)
    res
753
754
  | _ -> failwith "beta: Not a redex."

755
let rec _reduce_at_pos subst term pos current =
756
  (* Printf.printf "reduce at pos %s, current %s\n" pos current; *)
757
758
  match term with
  | AVar (s, t) -> term
Frontull Samuel's avatar
Frontull Samuel committed
759
760
  | ALam ((xs, e), t) ->
      ALam ((xs, _reduce_at_pos subst e pos (current ^ "0")), t)
761
  | AApp (e1, e2, t) ->
762
      if pos = current then beta subst term
763
      else if is_prefix (current ^ "0") pos then
764
765
766
767
768
769
        AApp (_reduce_at_pos subst e1 pos (current ^ "0"), e2, t)
      else AApp (e1, _reduce_at_pos subst e2 pos (current ^ "1"), t)

let reduce_at_pos subst term pos = _reduce_at_pos subst term pos "e"

let rec _reduce_lo subst term =
770
771
  match term with
  | AVar (s, t) -> term
772
  | ALam ((xs, e), t) -> ALam ((xs, _reduce_lo subst e), t)
773
774
  | AApp (e1, e2, t) -> (
      match e1 with
775
      | ALam _ -> beta subst term
776
      | _ ->
777
          let left = _reduce_lo subst e1 in
Frontull Samuel's avatar
Frontull Samuel committed
778
779
          if left = e1 then AApp (e1, _reduce_lo subst e2, t)
          else AApp (left, e2, t) )
780

781
let reduce_lo subst term = _reduce_lo subst term
782

783
let rec _extract_first_redex_pos path =
784
785
  match path with
  | [] -> []
786
  | (pa, AS _, _) :: (pl, LS _, _) :: xs ->
787
      if pa ^ "0" = pl then [ pa ] else _extract_first_redex_pos xs
788
  | (pl, LS _, _) :: (pa, AS _, _) :: xs ->
789
      if pa ^ "0" = pl then [ pa ] else _extract_first_redex_pos xs
790
  | x :: xs -> _extract_first_redex_pos xs
791

792
let extract_first_redex_pos path = _extract_first_redex_pos path
793
794

let reduce_scc term scc_path =
795
  (* Printf.printf "reduce_scc %s \n" (a_term_to_string term); *)
796
  let rpos = extract_first_redex_pos scc_path in
797
  let subst = casubst in
798
  match rpos with
799
  | [] -> term
800
  | x :: _ ->
801
802
803
804
      (* Printf.printf "Reduce at %s \n" x; *)
      let red = reduce_at_pos subst term x in
      (* Printf.printf "reduce_scc: %s\n" (a_term_to_string red) ; *)
      red
805

806
807
808
let rec _sn_reduce_to_nf subst term =
  let new_term = reduce_lo subst term in
  if new_term = term then [] else new_term :: _sn_reduce_to_nf subst new_term
Frontull Samuel's avatar
Frontull Samuel committed
809

810
let sn_reduce_to_nf subst term = term :: _sn_reduce_to_nf subst term
811

812
813
814
815
816
817
let rec _reduce_to_nf term max_depth i =
  let subst = casubst in
  let new_term = reduce_lo subst term in
  if new_term = term || max_depth < i then []
  else new_term :: _reduce_to_nf new_term max_depth (i + 1)

Frontull Samuel's avatar
Frontull Samuel committed
818
let reduce_to_nf term max_depth = term :: _reduce_to_nf term max_depth 0
819

820
821
822
let rec reduce_with_paths term max_depth sim =
  let nodes = term_nodes term in
  let paths = scc term max_depth sim in
823
  (* Printf.printf "reduce_with_paths: %s %d\n" (a_term_to_string term) (L.length (snd paths)); *)
824
  match paths with
825
  | _, [] -> [ term ]
826
  | _, x :: _ ->
827
      let sym_x = L.map (fun pos -> L.hd (get_node pos nodes)) x in
828
      let newterm = reduce_scc term sym_x in
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
      if newterm = term then []
      else term :: reduce_with_paths newterm (max_depth - 1) sim

let rec sn_reduce_with_paths_to_nf term max_depth sim =
  let nodes = term_nodes term in
  let paths = scc term max_depth sim in
  let subst = casubst in
  match paths with
  | _, [] -> sn_reduce_to_nf subst term
  | _, x :: _ ->
      let sym_x = L.map (fun pos -> L.hd (get_node pos nodes)) x in
      let newterm = reduce_scc term sym_x in
      if newterm = term then []
      else term :: sn_reduce_with_paths_to_nf newterm max_depth sim

Frontull Samuel's avatar
Frontull Samuel committed
844
845
846
847
848
849
let rec size term =
  match term with
  | AVar (s, t) -> 0
  | ALam ((xs, e), t) -> 1 + size e
  | AApp (e1, e2, t) -> 1 + size e1 + size e2

850
let rec nf subst term =
Frontull Samuel's avatar
Frontull Samuel committed
851
  (* Printf.printf "%d\n" (size term); *)
852
853
  let new_term = reduce_lo subst term in
  if new_term = term then term else nf subst new_term
854
855
856
857

let is_linear term =
  let be = b_edges term in
  not (Util.duplicates (List.map (fun x -> List.hd (List.rev x)) be))