assert false (* algorithm failed *)
let rec set_arity arity = function
+(* FIXME because onlt variables should be in branches of matches, one day *)
| `Var(n,_) -> `Var(n,arity)
| `N _ | `Bottom | `Pacman as t -> t
| `Lam(false, t) -> `Lam(false, set_arity arity t)
(************ Parsing ************************************)
-let parse' strs =
- let fix_arity = function
- | `I((n,_),args) -> `I((n,1+Listx.length args),args)
- | _ -> assert false in
- let (tms, free) = Parser.parse_many strs in
- (* Replace pacmans and bottoms *)
- let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in
- let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in
- let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in
- let fix lev v =
- if v = lev + n_bot then `Bottom
- else if v = lev + n_pac then `Pacman
- else if v = lev + n_bomb then `Lam(true, `Bottom)
- else `Var(v,1) in (* 1 by default when variable not applied *)
- (* Fix arity *)
- let rec aux lev = function
- | Parser.Lam t -> `Lam (true, aux (lev+1) t)
- | Parser.App (t1, t2) -> fix_arity (mk_app (aux lev t1) (aux lev t2))
- | Parser.Var v -> fix lev v in
- List.map (aux 0) tms, free
-;;
-
(************** Algorithm(s) ************************)
let eta_compare x y =
eta_subterm sub (u :> nf)
|| List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
|| List.exists (eta_subterm sub) (args :> nf list)
- | `I(v, args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
- | `Var v' -> v = v'
- | `I(v', args') -> v = v'
+ | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
+ | `Var(v',_) -> v = v'
+ | `I((v',_), args') -> v = v'
&& Listx.length args' < Listx.length args
&& List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args :> nf list)) (Listx.to_list args' :> nf list))
| _ -> false