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 rec t_of_i_num_var =
97 | `N n -> Scott.mk_n n
98 | `Var(v,_) -> Pure.V v
99 | `Match(t,_,liftno,bs,args) ->
100 let bs = List.map (fun (n,t) -> n, t_of_nf (lift liftno t)) !bs in
101 let t = t_of_i_num_var t in
102 let m = Scott.mk_match t bs in
103 List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args
104 | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args
107 | #i_num_var as x -> t_of_i_num_var x
108 | `Lam(b,f) -> Pure.L (t_of_nf f)
113 (************ Pretty-printing ************************************)
115 (* let rec string_of_term l = fun _ -> "";; *)
117 let rec string_of_term =
118 let boundvar x = "v" ^ string_of_int x in
119 let varname lev l n =
120 if n < lev then boundvar (lev-n-1)
121 else if n - lev < List.length l then List.nth l (n-lev)
122 else "`" ^ string_of_int (n-lev) in
123 let rec string_of_term_w_pars lev l = function
124 | `Var(n,ar) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
125 | `N n -> string_of_int n
126 | `I _ as t -> "(" ^ string_of_term_no_pars_app lev l t ^ ")"
127 | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
128 | `Match(t,(v,ar),bs_lift,bs,args) ->
129 (* assert (bs_lift = lev); *)
130 "(["^ varname 0 l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
131 " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
132 String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
133 and string_of_term_no_pars_app lev l = function
134 | `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))
135 | #nf as t -> string_of_term_w_pars lev l t
136 and string_of_term_no_pars_lam lev l = function
137 | `Lam(_,t) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
138 | _ as t -> string_of_term_no_pars lev l t
139 and string_of_term_no_pars lev l = function
140 | `Lam _ as t -> string_of_term_no_pars_lam lev l t
141 | #nf as t -> string_of_term_no_pars_app lev l t
142 in string_of_term_no_pars 0
145 let print ?(l=[]) = string_of_term l;;
146 let string_of_nf t = string_of_term [] (t:>nf);;
148 (************ Hereditary substitutions ************************************)
152 #i_var as y -> (y : i_var)
154 prerr_endline (print (t :> nf));
155 assert false (* algorithm failed *)
157 let cast_to_i_n_var =
159 #i_n_var as y -> (y : i_n_var)
161 prerr_endline (print (t :> nf));
162 assert false (* algorithm failed *)
164 let cast_to_i_num_var =
166 #i_num_var as y -> (y : i_num_var)
168 prerr_endline (print (t :> nf));
169 assert false (* algorithm failed *)
171 let rec set_arity arity = function
172 (* FIXME because onlt variables should be in branches of matches, one day *)
173 | `Var(n,_) -> `Var(n,arity)
175 | `Lam(false, t) -> `Lam(false, set_arity arity t)
176 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
177 | `I _ | `Lam _ -> assert false
179 let minus1 n = if n = min_int then n else n - 1;;
181 let rec mk_app (h : nf) (arg : nf) =
184 `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
185 | `Var v -> `I(v, Listx.Nil arg)
186 | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
187 | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
188 | `N _ -> assert false (* Numbers cannot be applied *)
189 (*in let l = ["v0";"v1";"v2"] in
190 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
193 (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
194 List.fold_left mk_app h args
196 and mk_appx h args = Listx.fold_left mk_app h args
198 and mk_match t (n,ar) bs_lift bs args =
199 (*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));*)
203 let h = List.assoc m !bs in
204 let h = set_arity (minus1 ar) h in
205 let h = lift bs_lift h in
208 `Match (t,(n,ar),bs_lift,bs,args))
209 | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
211 and subst truelam delift_by_one what (with_what : nf) (where : nf) =
212 let rec aux_propagate_arity ar = function
213 | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
214 | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
215 `Match(`I(v,args),(x,ar),liftno,bs,args')
216 | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
218 let rec aux_i_num_var l =
222 mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
224 `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
227 lift l (aux_propagate_arity ar with_what)
229 `Var((if delift_by_one && n >= l then n-1 else n), ar)
231 | `Match(t,v,bs_lift,bs,args) ->
232 let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
233 (* Warning! It now applies again the substitution in branches of matches.
234 But careful, it does it many times, for every occurrence of
235 the match. This is okay because what does not occur in with_what. *)
236 let l' = l - bs_lift in
237 let with_what' = lift l' (with_what :> nf) in
238 (* The following line should be the identity when delift_by_one = true because we
239 are assuming the ts to not contain lambda-bound variables. *)
240 bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
241 let body = cast_to_i_num_var (aux_i_num_var l t) in
242 mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
244 (*function iii -> let res = match iii with*)
246 | #i_num_var as x -> aux_i_num_var l x
247 | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
248 (*in let ll = ["v0";"v1";"v2"] in
249 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*)
254 (************** Algorithm(s) ************************)
256 let eta_compare x y =
257 (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
258 let clex aux1 aux2 (a1,a2) (b1,b2) =
259 let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
260 let rec lex aux l1 l2 =
265 | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
266 let rec aux t1 t2 = match t1, t2 with
267 | `Var(n,_) , `Var(m,_) -> compare n m
268 | `I((n1,_), l1), `I((n2,_), l2) ->
269 clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
272 | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
273 | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
274 | t2, `Lam(_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
275 | `N n1, `N n2 -> compare n1 n2
276 | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
277 let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
278 let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
279 clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
289 let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
291 let rec eta_subterm sub t =
292 if eta_eq sub t then true else
294 | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
295 | `Match(u,ar,liftno,bs,args) ->
296 eta_subterm sub (u :> nf)
297 || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
298 || List.exists (eta_subterm sub) (args :> nf list)
299 | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
300 | `Var(v',_) -> v = v'
301 | `I((v',_), args') -> v = v'
302 && Listx.length args' < Listx.length args
303 && 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'))
306 | `N _ | `Var _ -> false
309 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
312 let max_arity_tms n =
313 let max a b = match a, b with
316 | Some x, None -> Some x
317 | Some x, Some y -> Some (Pervasives.max x y) in
318 let aux_var l (m,a) = if n + l = m then Some a else None in
319 let rec aux l = function
320 | `Var v -> aux_var l v
321 | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
322 | `Lam(_,t) -> aux (l+1) t
323 | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
326 List.fold_left (fun acc t -> max acc (aux l t)) None in
327 fun tms -> aux_tms 0 (tms :> nf list)
330 let get_first_args var =
331 let rec aux l = function
332 | `Lam(_,t) -> aux (l+1) t
333 | `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
334 | `I((n,_), args) -> if n = var + l then [Listx.last args] else []
340 let compute_arities m =
345 let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in
346 let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
347 arity :: (aux (n-1) tms)
348 in fun tms -> List.rev (aux m tms)
351 let compute_arities var special_k all_tms =
352 let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
353 compute_arities special_k tms