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 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 _ -> "";; *)
126 let rec string_of_term =
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 in string_of_term_no_pars 0
154 let print ?(l=[]) = string_of_term l;;
155 let string_of_nf t = string_of_term [] (t:>nf);;
157 (************ Hereditary substitutions ************************************)
161 #i_var as y -> (y : i_var)
163 prerr_endline (print (t :> nf));
164 assert false (* algorithm failed *)
166 let cast_to_i_n_var =
168 #i_n_var as y -> (y : i_n_var)
170 prerr_endline (print (t :> nf));
171 assert false (* algorithm failed *)
173 let cast_to_i_num_var =
175 #i_num_var as y -> (y : i_num_var)
177 prerr_endline (print (t :> nf));
178 assert false (* algorithm failed *)
180 let rec set_arity arity = function
181 (* FIXME because onlt variables should be in branches of matches, one day *)
182 | `Var(n,_) -> `Var(n,arity)
184 | `Lam(false, t) -> `Lam(false, set_arity arity t)
185 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
186 | `I _ | `Lam _ -> assert false
188 let minus1 n = if n = min_int then n else n - 1;;
190 let rec mk_app (h : nf) (arg : nf) =
193 `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
194 | `Var v -> `I(v, Listx.Nil arg)
195 | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
196 | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
197 | `N _ -> assert false (* Numbers cannot be applied *)
198 (*in let l = ["v0";"v1";"v2"] in
199 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
202 (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
203 List.fold_left mk_app h args
205 and mk_appx h args = Listx.fold_left mk_app h args
207 and mk_match t (n,ar) bs_lift bs args =
208 (*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));*)
212 let h = List.assoc m !bs in
213 let h = set_arity (minus1 ar) h in
214 let h = lift bs_lift h in
217 `Match (t,(n,ar),bs_lift,bs,args))
218 | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
220 and subst truelam delift_by_one what (with_what : nf) (where : nf) =
221 let rec aux_propagate_arity ar = function
222 | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
223 | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
224 `Match(`I(v,args),(x,ar),liftno,bs,args')
225 | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
227 let rec aux_i_num_var l =
231 mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
233 `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
236 lift l (aux_propagate_arity ar with_what)
238 `Var((if delift_by_one && n >= l then n-1 else n), ar)
240 | `Match(t,v,bs_lift,bs,args) ->
241 let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
242 (* Warning! It now applies again the substitution in branches of matches.
243 But careful, it does it many times, for every occurrence of
244 the match. This is okay because what does not occur in with_what. *)
245 let l' = l - bs_lift in
246 let with_what' = lift l' (with_what :> nf) in
247 (* The following line should be the identity when delift_by_one = true because we
248 are assuming the ts to not contain lambda-bound variables. *)
249 bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
250 let body = cast_to_i_num_var (aux_i_num_var l t) in
251 mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
253 (*function iii -> let res = match iii with*)
255 | #i_num_var as x -> aux_i_num_var l x
256 | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
257 (*in let ll = ["v0";"v1";"v2"] in
258 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*)
263 (************** Algorithm(s) ************************)
265 let eta_compare x y =
266 (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
267 let clex aux1 aux2 (a1,a2) (b1,b2) =
268 let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
269 let rec lex aux l1 l2 =
274 | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
275 let rec aux t1 t2 = match t1, t2 with
276 | `Var(n,_) , `Var(m,_) -> compare n m
277 | `I((n1,_), l1), `I((n2,_), l2) ->
278 clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
281 | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
282 | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
283 | t2, `Lam(_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
284 | `N n1, `N n2 -> compare n1 n2
285 | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
286 let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
287 let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
288 clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
298 let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
300 let rec eta_subterm sub t =
301 if eta_eq sub t then true else
303 | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
304 | `Match(u,ar,liftno,bs,args) ->
305 eta_subterm sub (u :> nf)
306 || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
307 || List.exists (eta_subterm sub) (args :> nf list)
308 | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
309 | `Var(v',_) -> v = v'
310 | `I((v',_), args') -> v = v'
311 && Listx.length args' < Listx.length args
312 && 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'))
315 | `N _ | `Var _ -> false
318 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
321 let max_arity_tms n =
322 let max a b = match a, b with
325 | Some x, None -> Some x
326 | Some x, Some y -> Some (Pervasives.max x y) in
327 let aux_var l (m,a) = if n + l = m then Some a else None in
328 let rec aux l = function
329 | `Var v -> aux_var l v
330 | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
331 | `Lam(_,t) -> aux (l+1) t
332 | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
335 List.fold_left (fun acc t -> max acc (aux l t)) None in
336 fun tms -> aux_tms 0 (tms :> nf list)
339 let get_first_args var =
340 let rec aux l = function
341 | `Lam(_,t) -> aux (l+1) t
342 | `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
343 | `I((n,_), args) -> if n = var + l then [Listx.last args] else []
349 let compute_arities m =
354 let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in
355 let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
356 arity :: (aux (n-1) tms)
357 in fun tms -> List.rev (aux m tms)
360 let compute_arities var special_k all_tms =
361 let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
362 compute_arities special_k tms