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 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) -> `Lam (b, aux (l+1) nf)
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) -> aux (n+1) t
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
117 | `Lam(b,f) -> Pure.L (t_of_nf f)
122 (************ Pretty-printing ************************************)
124 (* let rec string_of_term l = fun _ -> "";; *)
127 let boundvar x = "v" ^ string_of_int x in
128 let varname lev l n =
129 if n < lev then boundvar (lev-n-1)
130 else if n - lev < List.length l then List.nth l (n-lev)
131 else "`" ^ string_of_int (n-lev) in
132 let rec string_of_term_w_pars lev l = function
133 | `Var(n,ar) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
134 | `N n -> string_of_int n
135 | `I _ as t -> "(" ^ string_of_term_no_pars_app lev l t ^ ")"
136 | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
137 | `Match(t,(v,ar),bs_lift,bs,args) ->
138 (* assert (bs_lift = lev); *)
139 "(["^ varname 0 l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
140 " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
141 String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
142 and string_of_term_no_pars_app lev l = function
143 | `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))
144 | #nf as t -> string_of_term_w_pars lev l t
145 and string_of_term_no_pars_lam lev l = function
146 | `Lam(_,t) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
147 | _ as t -> string_of_term_no_pars lev l t
148 and string_of_term_no_pars lev l = function
149 | `Lam _ as t -> string_of_term_no_pars_lam lev l t
150 | #nf as t -> string_of_term_no_pars_app lev l t
151 and string_of_term t = string_of_term_no_pars 0 t in
155 let print ?(l=[]) = string_of_term l;;
156 let string_of_nf t = string_of_term [] (t:>nf);;
158 (************ Hereditary substitutions ************************************)
162 #i_var as y -> (y : i_var)
164 prerr_endline (print (t :> nf));
165 assert false (* algorithm failed *)
167 let cast_to_i_n_var =
169 #i_n_var as y -> (y : i_n_var)
171 prerr_endline (print (t :> nf));
172 assert false (* algorithm failed *)
174 let cast_to_i_num_var =
176 #i_num_var as y -> (y : i_num_var)
178 prerr_endline (print (t :> nf));
179 assert false (* algorithm failed *)
181 let rec set_arity arity = function
182 (* FIXME because onlt variables should be in branches of matches, one day *)
183 | `Var(n,_) -> `Var(n,arity)
185 | `Lam(false, t) -> `Lam(false, set_arity arity t)
186 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
187 | `I _ | `Lam _ -> assert false
189 let minus1 n = if n = min_int then n else n - 1;;
191 let rec mk_app (h : nf) (arg : nf) =
194 `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
195 | `Var v -> `I(v, Listx.Nil arg)
196 | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
197 | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
198 | `N _ -> assert false (* Numbers cannot be applied *)
199 (*in let l = ["v0";"v1";"v2"] in
200 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
203 (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
204 List.fold_left mk_app h args
206 and mk_appx h args = Listx.fold_left mk_app h args
208 and mk_match t (n,ar) bs_lift bs args =
209 (*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));*)
213 let h = List.assoc m !bs in
214 let h = set_arity (minus1 ar) h in
215 let h = lift bs_lift h in
218 `Match (t,(n,ar),bs_lift,bs,args))
219 | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
221 and subst truelam delift_by_one what (with_what : nf) (where : nf) =
222 let rec aux_propagate_arity ar = function
223 | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
224 | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
225 `Match(`I(v,args),(x,ar),liftno,bs,args')
226 | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
228 let rec aux_i_num_var l =
232 mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
234 `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
237 lift l (aux_propagate_arity ar with_what)
239 `Var((if delift_by_one && n >= l then n-1 else n), ar)
241 | `Match(t,v,bs_lift,bs,args) ->
242 let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
243 (* Warning! It now applies again the substitution in branches of matches.
244 But careful, it does it many times, for every occurrence of
245 the match. This is okay because what does not occur in with_what. *)
246 let l' = l - bs_lift in
247 let with_what' = lift l' (with_what :> nf) in
248 (* The following line should be the identity when delift_by_one = true because we
249 are assuming the ts to not contain lambda-bound variables. *)
250 bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
251 let body = cast_to_i_num_var (aux_i_num_var l t) in
252 mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
254 (*function iii -> let res = match iii with*)
256 | #i_num_var as x -> aux_i_num_var l x
257 | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
258 (*in let ll = ["v0";"v1";"v2"] in
259 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*)
264 (************** Algorithm(s) ************************)
266 let eta_compare x y =
267 (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
268 let clex aux1 aux2 (a1,a2) (b1,b2) =
269 let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
270 let rec lex aux l1 l2 =
275 | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
276 let rec aux t1 t2 = match t1, t2 with
277 | `Var(n,_) , `Var(m,_) -> compare n m
278 | `I((n1,_), l1), `I((n2,_), l2) ->
279 clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
282 | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
283 | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
284 | t2, `Lam(_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
285 | `N n1, `N n2 -> compare n1 n2
286 | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
287 let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
288 let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
289 clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
299 let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
301 let rec eta_subterm sub t =
302 if eta_eq sub t then true else
304 | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
305 | `Match(u,ar,liftno,bs,args) ->
306 eta_subterm sub (u :> nf)
307 || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
308 || List.exists (eta_subterm sub) (args :> nf list)
309 | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
310 | `Var(v',_) -> v = v'
311 | `I((v',_), args') -> v = v'
312 && Listx.length args' < Listx.length args
313 && 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'))
316 | `N _ | `Var _ -> false
319 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
322 let max_arity_tms n =
323 let max a b = match a, b with
326 | Some x, None -> Some x
327 | Some x, Some y -> Some (Pervasives.max x y) in
328 let aux_var l (m,a) = if n + l = m then Some a else None in
329 let rec aux l = function
330 | `Var v -> aux_var l v
331 | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
332 | `Lam(_,t) -> aux (l+1) t
333 | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
336 List.fold_left (fun acc t -> max acc (aux l t)) None in
337 fun tms -> aux_tms 0 (tms :> nf list)
340 let get_first_args var =
341 let rec aux l = function
342 | `Lam(_,t) -> aux (l+1) t
343 | `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
344 | `I((n,_), args) -> if n = var + l then [Listx.last args] else []
350 let compute_arities m =
355 let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in
356 let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
357 arity :: (aux (n-1) tms)
358 in fun tms -> List.rev (aux m tms)
361 let compute_arities var special_k all_tms =
362 let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
363 compute_arities special_k tms