6 let debug_display_arities = false;;
8 (************ Syntax ************************************)
12 (* Var n = n-th De Bruijn index, 0-based *)
21 type var = int * (* arity of variable*) int;;
22 type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ]
23 type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
24 type 'nf i_num_var_ = [
26 | `Match of 'nf i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list
28 type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ * ('nf nf_) list | 'nf i_num_var_ ]
30 type i_var = nf i_var_;;
31 type i_n_var = nf i_n_var_;;
32 type i_num_var = nf i_num_var_;;
44 | `Match _ -> assert false
53 let aux_var l (n, ar) = (if n < l then n else n+m), ar in
54 let rec aux_i_num_var l =
56 `I(v,args) -> `I(aux_var l v, Listx.map (aux l) args)
57 | `Var v -> `Var(aux_var l v)
59 | `Match(t,v,lift,bs,args) ->
60 `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux l) args)
63 #i_num_var as x -> (aux_i_num_var l x :> nf)
64 | `Lam(b,nf,g) -> `Lam (b, aux (l+1) nf, List.map (aux (l+1)) g)
69 (* put t under n lambdas, lifting t accordingtly *)
73 | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)), [])
77 let rec aux n = function
79 | `Var(x,ar) -> if x < n then [] else [(x-n,ar)]
81 (if x < n then [] else [(x-n,ar)]) @
82 List.concat (List.map (aux n) (Listx.to_list args))
83 | `Lam(_,t,g) -> List.concat (List.map (aux (n+1)) (t::g))
84 | `Match(t,_,liftno,bs,args) ->
86 List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @
87 List.concat (List.map (aux n) args)
90 let free_vars = (List.map fst) ++ free_vars';;
95 let delta = let open Pure in L(A(V 0, V 0))
97 let bomb = ref(`Var(-1, -666));;
99 let rec t_of_i_num_var =
101 | `N n -> Scott.mk_n n
102 | `Var(v,_) as x -> assert (x <> !bomb); Pure.V v
103 | `Match(t,_,liftno,bs,args) ->
106 (if t = !bomb then delta
107 else Pure.L (t_of_nf (lift (liftno+1) t)))
109 let t = t_of_i_num_var t in
110 let m = Scott.mk_match t bs in
111 let m = Pure.A(m,delta) in
112 List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args
113 | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args
116 | #i_num_var as x -> t_of_i_num_var x
118 let t = t_of_nf (lift (List.length g) f) in
119 let t = List.fold_left (fun t g -> Pure.A(Pure.L t, t_of_nf g)) t g in
125 (************ Pretty-printing ************************************)
127 (* let rec string_of_term l = fun _ -> "";; *)
130 let boundvar x = "v" ^ string_of_int x in
131 let varname lev l n =
132 if n < lev then boundvar (lev-n-1)
133 else if n - lev < List.length l then List.nth l (n-lev)
134 else "`" ^ string_of_int (n-lev) in
135 let rec string_of_term_w_pars lev l = function
136 | `Var(n,ar) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
137 | `N n -> string_of_int n
138 | `I _ as t -> "(" ^ string_of_term_no_pars_app lev l t ^ ")"
139 | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
140 | `Match(t,(v,ar),bs_lift,bs,args) ->
141 (* assert (bs_lift = lev); *)
142 "(["^ varname 0 l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
143 " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
144 String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
145 and string_of_term_no_pars_app lev l = function
146 | `I((n,ar), args) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars lev l) (Listx.to_list args :> nf list))
147 | #nf as t -> string_of_term_w_pars lev l t
148 and string_of_term_no_pars_lam lev l = function
149 | `Lam(_,t,g) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
150 ^ (if g = [] then "" else String.concat ", " ("" :: List.map (string_of_term_no_pars (lev+1) l) g))
151 | _ as t -> string_of_term_no_pars lev l t
152 and string_of_term_no_pars lev l = function
153 | `Lam _ as t -> string_of_term_no_pars_lam lev l t
154 | #nf as t -> string_of_term_no_pars_app lev l t
155 and string_of_term t = string_of_term_no_pars 0 t in
159 let print ?(l=[]) = string_of_term l;;
160 let string_of_nf t = string_of_term [] (t:>nf);;
162 (************ Hereditary substitutions ************************************)
166 #i_var as y -> (y : i_var)
168 prerr_endline (print (t :> nf));
169 assert false (* algorithm failed *)
171 let cast_to_i_n_var =
173 #i_n_var as y -> (y : i_n_var)
175 prerr_endline (print (t :> nf));
176 assert false (* algorithm failed *)
178 let cast_to_i_num_var =
180 #i_num_var as y -> (y : i_num_var)
182 prerr_endline (print (t :> nf));
183 assert false (* algorithm failed *)
185 let rec set_arity arity = function
186 (* FIXME because onlt variables should be in branches of matches, one day *)
187 | `Var(n,_) -> `Var(n,arity)
189 | `Lam(false, t, []) -> `Lam(false, set_arity arity t, [])
190 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
191 | `I _ | `Lam _ -> assert false
193 let minus1 n = if n = min_int then n else n - 1;;
195 let rec mk_app (h : nf) (arg : nf) =
198 `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
199 | `Var v -> `I(v, Listx.Nil arg)
200 | `Lam(truelam,nf,g) -> assert (g = []); subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
201 | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
202 | `N _ -> assert false (* Numbers cannot be applied *)
203 (*in let l = ["v0";"v1";"v2"] in
204 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
207 (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
208 List.fold_left mk_app h args
210 and mk_appx h args = Listx.fold_left mk_app h args
212 and mk_match t (n,ar) bs_lift bs args =
213 (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*)
217 let h = List.assoc m !bs in
218 let h = set_arity (minus1 ar) h in
219 let h = lift bs_lift h in
222 `Match (t,(n,ar),bs_lift,bs,args))
223 | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
225 and subst truelam delift_by_one what (with_what : nf) (where : nf) =
226 let rec aux_propagate_arity ar = function
227 | `Lam(false,t,g) when not delift_by_one -> assert (g = []); `Lam(false,aux_propagate_arity ar t,[])
228 | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
229 `Match(`I(v,args),(x,ar),liftno,bs,args')
230 | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
232 let rec aux_i_num_var l =
236 mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
238 `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
241 lift l (aux_propagate_arity ar with_what)
243 `Var((if delift_by_one && n >= l then n-1 else n), ar)
245 | `Match(t,v,bs_lift,bs,args) ->
246 let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
247 (* Warning! It now applies again the substitution in branches of matches.
248 But careful, it does it many times, for every occurrence of
249 the match. This is okay because what does not occur in with_what. *)
250 let l' = l - bs_lift in
251 let with_what' = lift l' (with_what :> nf) in
252 (* The following line should be the identity when delift_by_one = true because we
253 are assuming the ts to not contain lambda-bound variables. *)
254 bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
255 let body = cast_to_i_num_var (aux_i_num_var l t) in
256 mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
258 (*function iii -> let res = match iii with*)
260 | #i_num_var as x -> aux_i_num_var l x
261 | `Lam(b, nf, g) -> `Lam(b, aux (l+1) nf, List.map (aux (l+1)) g)
262 (*in let ll = ["v0";"v1";"v2"] in
263 prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
268 (************** Algorithm(s) ************************)
270 let eta_compare x y =
271 (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
272 let clex aux1 aux2 (a1,a2) (b1,b2) =
273 let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
274 let rec lex aux l1 l2 =
279 | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
280 let rec aux t1 t2 = match t1, t2 with
281 | `Var(n,_) , `Var(m,_) -> compare n m
282 | `I((n1,_), l1), `I((n2,_), l2) ->
283 clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
286 | `Lam(_,t1,_), `Lam(_,t2,_) -> aux t1 t2
287 | `Lam(_,t1,_), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
288 | t2, `Lam(_,t1,_) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
289 | `N n1, `N n2 -> compare n1 n2
290 | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
291 let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
292 let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
293 clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
303 let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
305 let rec eta_subterm sub t =
306 if eta_eq sub t then true else
308 | `Lam(_,t,g) -> List.exists (eta_subterm (lift 1 sub)) (t::g)
309 | `Match(u,ar,liftno,bs,args) ->
310 eta_subterm sub (u :> nf)
311 || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
312 || List.exists (eta_subterm sub) (args :> nf list)
313 | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
314 | `Var(v',_) -> v = v'
315 | `I((v',_), args') -> v = v'
316 && Listx.length args' < Listx.length args
317 && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args)) (Listx.to_list args'))
320 | `N _ | `Var _ -> false
323 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
326 let max_arity_tms n =
327 let max a b = match a, b with
330 | Some x, None -> Some x
331 | Some x, Some y -> Some (Pervasives.max x y) in
332 let aux_var l (m,a) = if n + l = m then Some a else None in
333 let rec aux l = function
334 | `Var v -> aux_var l v
335 | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
336 | `Lam(_,t, g) -> List.fold_left (fun n t -> max n (aux (l+1) t)) None (t::g)
337 | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
340 List.fold_left (fun acc t -> max acc (aux l t)) None in
341 fun tms -> aux_tms 0 (tms :> nf list)
344 let get_first_args var =
345 let rec aux l = function
346 | `Lam(_,t,_) -> aux (l+1) t
347 | `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
348 | `I((n,_), args) -> if n = var + l then [Listx.last args] else []
354 let compute_arities m =
359 let tms = Util.filter_map (function `Lam(_,t,_) -> Some t | _ -> None ) tms in
360 let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
361 arity :: (aux (n-1) tms)
362 in fun tms -> List.rev (aux m tms)
365 let compute_arities var special_k all_tms =
366 let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
367 compute_arities special_k tms