From dc3d76330323f0eba348377062934481c763d450 Mon Sep 17 00:00:00 2001 From: Date: Mon, 26 Jun 2017 12:26:43 +0200 Subject: [PATCH] New representation of arities in variables --- ocaml/lambda4.ml | 87 ++++++++++++++++++++++++---------------------- ocaml/num.ml | 90 +++++++++++++++++++++++++----------------------- ocaml/num.mli | 22 ++++++------ 3 files changed, 102 insertions(+), 97 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 3e9f1ef..f71f360 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -3,7 +3,7 @@ open Util.Vars open Pure open Num -let bomb = ref(`Var ~-1);; +let bomb = ref(`Var(-1,-666));; type problem = { freshno: int @@ -21,7 +21,7 @@ for all head (* let ($) f x = f x;; *) -let subterms tms freshno = +(* let subterms tms freshno = let apply_var = let no = ref freshno in function t -> incr no; mk_app t (`Var !no) in @@ -42,7 +42,7 @@ let subterms tms freshno = in let tms' = (* Util.sort_uniq ~compare:eta_compare*) (Util.concat_map aux tms) in tms @ tms' (* List.map (fun (t, v) -> match t with `N _ -> t | _ -> mk_app t v) (List.combine tms (List.mapi (fun i _ -> `Var(freshno+i)) tms)) *) -;; +;; *) let all_terms p = (match p.div with None -> [] | Some t -> [(t :> i_n_var)]) @@ -77,39 +77,39 @@ let failwithProblem p reason = failwith reason ;; -let make_fresh_var p = +let make_fresh_var p arity = let freshno = p.freshno + 1 in - {p with freshno}, `Var freshno + {p with freshno}, `Var(freshno,arity) ;; -let make_fresh_vars p m = - Array.fold_left +let make_fresh_vars p arities = + List.fold_right (* fold_left vs. fold_right hides/shows the bug in problem q7 *) - (fun (p, vars) _ -> let p, var = make_fresh_var p in p, var::vars) + (fun arity (p, vars) -> let p, var = make_fresh_var p arity in p, var::vars) + arities (p, []) - (Array.make m ()) ;; let simple_expand_match ps = let rec aux level = function | #i_num_var as t -> aux_i_num_var level t - | `Lam(b,ar,t) -> `Lam(b,ar,aux (level+1) t) + | `Lam(b,t) -> `Lam(b,aux (level+1) t) and aux_i_num_var level = function - | `Match(u,ar,bs_lift,bs,args) as torig -> + | `Match(u,v,bs_lift,bs,args) as torig -> let u = aux_i_num_var level u in bs := List.map (fun (n, x) -> n, aux 0 x) !bs; (try (match u with | #i_n_var as u -> let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *) - in let t = mk_match (`N i) ar bs_lift bs args in + in let t = mk_match (`N i) v bs_lift bs args in if t <> torig then aux level (t :> nf) else raise Not_found | _ -> raise Not_found) with Not_found -> - `Match(cast_to_i_num_var u,ar,bs_lift,bs,List.map (aux level) args)) - | `I(k,args) -> `I(k,Listx.map (aux level) args) + `Match(cast_to_i_num_var u,v,bs_lift,bs,List.map (aux level) args)) + | `I(v,args) -> `I(v,Listx.map (aux level) args) | `N _ | `Var _ as t -> t in aux_i_num_var 0;; @@ -143,7 +143,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) let t = subst false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) let freshno,new_t,acc_new_ps = - expand_match (freshno,acc_ps@`Var(max_int/3)::todo_ps,acc_new_ps) t + expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t in aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps @@ -175,7 +175,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t = match t with - | `Match(u',ar,bs_lift,bs,args) -> + | `Match(u',orig,bs_lift,bs,args) -> let freshno,u,acc_new_ps = expand_match acc (u' :> nf) in let acc_new_ps,i = match u with @@ -194,11 +194,11 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif if List.exists (fun (j,_) -> i=j) !bs then freshno else - let freshno,v = freshno+1, `Var (freshno+1) in (* make_fresh_var freshno in *) + let freshno,v = freshno+1, `Var (freshno+1, snd orig - 1) in (* make_fresh_var freshno in *) bs := !bs @ [i, v] ; freshno in (*prerr_endlie ("t DA RIDURRE:" ^ print (`Match(`N i,arity,bs_lift,bs,args) :> nf) ^ " more_args=" ^ string_of_int more_args);*) - let t = mk_match (`N i) ar bs_lift bs args in + let t = mk_match (`N i) orig bs_lift bs args in (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*) expand_match (freshno,acc_ps,acc_new_ps) t | `Lam _ -> raise ExpandedToLambda @@ -243,10 +243,10 @@ let rec dangerous arities showstoppers = (match t with `N _ -> List.iter (dangerous arities showstoppers) args | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args - | `Var x -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *) - | `I(x,args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) + | `Var(x,_) -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *) + | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) ) - | `I(k,args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0 + | `I((k,_),args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0 and dangerous_inert arities showstoppers k args more_args = List.iter (dangerous arities showstoppers) args ; @@ -268,10 +268,10 @@ let rec dangerous_conv arities showstoppers = (match t with `N _ -> concat_map (dangerous_conv arities showstoppers) args | `Match _ as t -> dangerous_conv arities showstoppers t @ concat_map (dangerous_conv arities showstoppers) args - | `Var x -> dangerous_inert_conv arities showstoppers x args 2 (* 2 coming from Scott's encoding *) - | `I(x,args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) + | `Var(x,_) -> dangerous_inert_conv arities showstoppers x args 2 (* 2 coming from Scott's encoding *) + | `I((x,_),args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) ) - | `I(k,args) -> dangerous_inert_conv arities showstoppers k (Listx.to_list args) 0 + | `I((k,_),args) -> dangerous_inert_conv arities showstoppers k (Listx.to_list args) 0 and dangerous_inert_conv arities showstoppers k args more_args = concat_map (dangerous_conv arities showstoppers) args @ @@ -345,7 +345,7 @@ let critical_showstoppers p = let showstoppers_eat = let heads_and_arities = List.sort (fun (k,_) (h,_) -> compare k h) - (filter_map (function `Var k -> Some (k,0) | `I(k,args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in + (filter_map (function `Var(k,_) -> Some (k,0) | `I((k,_),args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in let rec multiple_arities = function [] @@ -397,8 +397,8 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst)); then p else let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in - let p, bomb' = make_fresh_var p in - (if !bomb <> `Var (-1) then + let p, bomb' = make_fresh_var p (-666) in + (if !bomb <> `Var (-1,-666) then failwithProblem p ("Bomb was duplicated! It was " ^ string_of_nf !bomb ^ ", tried to change it to " ^ string_of_nf bomb')); @@ -446,25 +446,28 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) `Continue p let instantiate p x n = - (if `Var x = !bomb + (if hd_of_i_var (cast_to_i_var !bomb) = x then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!")); - let p,vars = make_fresh_vars p n in - let p,zero = make_fresh_var p in - let zero = Listx.Nil zero in - let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in + (* ACL FIXME compute arity of x correctly below! *) + let arity_of_x = -666 in + (* AC: FIXME compute arities correctly below! *) + let arities = Array.to_list (Array.make (n+1) 0) in + let p,vars = make_fresh_vars p arities in + (* let p,zero = make_fresh_var p in *) + (* let zero = Listx.Nil zero in *) + (* let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in *) + let args = Listx.from_list (vars :> nf list) in let bs = ref [] in - let arity1 = (*assert false; -666*) 0 in - let arity2 = (*assert false; -666*) 0 in - let inst = `Lam(false,arity1,`Match(`I(0,Listx.map (lift 1) args),arity2,1,bs,[])) in + let inst = `Lam(false,`Match(`I((0,0),Listx.map (lift 1) args),(x,arity_of_x),1,bs,[])) in let p = {p with deltas=bs::p.deltas} in subst_in_problem x inst p ;; let compute_special_k tms = let rec aux k (t: nf) = Pervasives.max k (match t with - | `Lam(b,_,t) -> aux (k + if b then 1 else 0) t + | `Lam(b,t) -> aux (k + if b then 1 else 0) t | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms) - | `Match(t,_,liftno, bs, args) -> + | `Match(t, _, liftno, bs, args) -> List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs)) | `N _ -> 0 | `Var _ -> 0 @@ -590,7 +593,7 @@ let optimize_numerals p = | `N n -> `N (List.nth perm n) | `I _ -> assert false | `Var _ as t -> t - | `Lam(v,ar,t) -> `Lam(v, ar, aux t) + | `Lam(v,t) -> `Lam(v, aux t) | `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t in List.map (fun (n,t) -> (n,aux t)) in @@ -617,7 +620,7 @@ let env_of_sigma freshno sigma should_explode = e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[] with Not_found -> - if should_explode && `Var n = !bomb + if should_explode && n = hd_of_i_var (cast_to_i_var !bomb) then ([], (let f t = Pure.A(t,t) in f (Pure.L (f (Pure.V 0)))), []) else ([],Pure.V n,[]))::e in aux 0 @@ -657,7 +660,7 @@ let main problems = List.iter (fun (p,n,cmds) -> Console.print_hline(); - bomb := `Var (-1); + bomb := `Var (-1,-666); let p_finale = aux p n cmds in let freshno,sigma = p_finale.freshno, p_finale.sigma in prerr_endline ("------- ------\n "); @@ -727,7 +730,7 @@ in (********************** problems *******************) -let zero = `Var 0;; +let zero = `Var(0,-1);; let append_zero = function @@ -760,7 +763,7 @@ let magic_conv ~div ~conv ~nums cmds = let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *) let freshno = List.length var_names in let deltas = - let dummy = `Var (max_int / 2) in + let dummy = `Var (max_int / 2, -666) in [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in {freshno; div; conv; ps; sigma=[] ; deltas}, special_k, cmds diff --git a/ocaml/num.ml b/ocaml/num.ml index 7f94b25..9d80313 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -15,13 +15,14 @@ open Pure and i = | I of int * nf listx ;;*) -type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ] +type var = int * (* arity of variable*) int;; +type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ] type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ] type 'nf i_num_var_ = [ | 'nf i_n_var_ - | `Match of 'nf i_num_var_ * (* arity of branches *) int * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list + | `Match of 'nf i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list ] -type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * (* arity of variable*) int * 'nf nf_ | 'nf i_num_var_ ] +type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | 'nf i_num_var_ ] type nf = nf nf_ type i_var = nf i_var_;; type i_n_var = nf i_n_var_;; @@ -29,28 +30,29 @@ type i_num_var = nf i_num_var_;; let hd_of_i_var = function - `I (v,_) - | `Var v -> v + `I ((v,_),_) + | `Var (v,_) -> v let hd_of = function - `I (v,_) - | `Var v -> Some v + `I ((v,_),_) + | `Var(v,_) -> Some v | `N _ -> None | `Match _ -> assert false let lift m (t : nf) = + let aux_var l (n, ar) = (if n < l then n else n+m), ar in let rec aux_i_num_var l = function - `I(n,args) -> (`I((if n < l then n else n+m),Listx.map (aux l) args) : i_num_var) - | `Var n -> `Var (if n < l then n else n+m) + `I(v,args) -> `I(aux_var l v, Listx.map (aux l) args) + | `Var v -> `Var(aux_var l v) | `N _ as x -> x - | `Match(t,ar,lift,bs,args) -> - `Match(aux_i_num_var l t, ar,lift + m, bs, List.map (aux l) args) + | `Match(t,v,lift,bs,args) -> + `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux l) args) and aux l = function #i_num_var as x -> (aux_i_num_var l x :> nf) - | `Lam(b,ar,nf) -> `Lam (b,ar,aux (l+1) nf) + | `Lam(b,nf) -> `Lam (b, aux (l+1) nf) in (aux 0 t : nf) ;; @@ -59,17 +61,17 @@ let lift m (t : nf) = let rec make_lams t = function 0 -> t - | n when n > 0 -> `Lam (false,-666,lift 1 (make_lams t (n-1))) + | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1))) | _ -> assert false let free_vars = let rec aux n = function `N _ -> [] - | `Var x -> if x < n then [] else [x-n] - | `I(x,args) -> + | `Var(x,_) -> if x < n then [] else [x-n] + | `I((x,_),args) -> (if x < n then [] else [x-n]) @ List.concat (List.map (aux n) (Listx.to_list args)) - | `Lam(_,_,t) -> aux (n+1) t + | `Lam(_,t) -> aux (n+1) t | `Match(t,_,liftno,bs,args) -> aux n (t :> nf) @ List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @ @@ -83,17 +85,17 @@ struct let rec t_of_i_num_var = function | `N n -> Scott.mk_n n - | `Var v -> Pure.V v + | `Var(v,_) -> Pure.V v | `Match(t,_,liftno,bs,args) -> let bs = List.map (fun (n,t) -> n, t_of_nf (lift liftno t)) !bs in let t = t_of_i_num_var t in let m = Scott.mk_match t bs in List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args - | `I(v, args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args + | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args and t_of_nf = function | #i_num_var as x -> t_of_i_num_var x - | `Lam(b,_,f) -> Pure.L (t_of_nf f) + | `Lam(b,f) -> Pure.L (t_of_nf f) end @@ -102,21 +104,21 @@ end let rec print ?(l=[]) = function - `Var n -> print_name l n + `Var(n,_) -> print_name l n | `N n -> string_of_int n | `Match(t,_,bs_lift,bs,args) -> "([" ^ print ~l (t :> nf) ^ " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^ String.concat " " (List.map (print ~l) args) ^ ")" - | `I(n,args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")" - | `Lam(_,_,nf) -> + | `I((n,_),args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")" + | `Lam(_,nf) -> let name = string_of_var (List.length l) in "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf) ;; let rec string_of_term l = let rec string_of_term_w_pars l = function - | `Var n -> print_name l n + | `Var(n,_) -> print_name l n | `N n -> string_of_int n | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")" | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")" @@ -125,10 +127,10 @@ let rec string_of_term l = " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^ String.concat " " (List.map (string_of_term l) args) ^ ")" and string_of_term_no_pars_app l = function - | `I(n, args) -> print_name l n ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args)) + | `I((n,_), args) -> print_name l n ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args)) | #nf as t -> string_of_term_w_pars l t and string_of_term_no_pars_lam l = function - | `Lam(_,_,t) -> let name = string_of_var (List.length l) in + | `Lam(_,t) -> let name = string_of_var (List.length l) in "λ" ^ name ^ ". " ^ (string_of_term_no_pars_lam (name::l) t) | _ as t -> string_of_term_no_pars l t and string_of_term_no_pars l : nf -> string = function @@ -166,10 +168,10 @@ let cast_to_i_num_var = let rec mk_app (h : nf) (arg : nf) = (*let res =*) match h with - `I(n,args) -> `I(n,Listx.append (Listx.Nil arg) args) - | `Var n -> `I(n, Listx.Nil arg) - | `Lam(_,_,nf) -> subst true 0 arg (nf : nf) (* AC FIXME sanity check on arity *) - | `Match(t,ar,lift,bs,args) -> `Match(t,ar,lift,bs,List.append args [arg]) + `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args) + | `Var v -> `I(v, Listx.Nil arg) + | `Lam(_,nf) -> subst true 0 arg (nf : nf) (* AC FIXME sanity check on arity *) + | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg]) | `N _ -> assert false (* Numbers cannot be applied *) (*in let l = ["v0";"v1";"v2"] in prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*) @@ -195,30 +197,30 @@ and mk_match t ar bs_lift bs args = and subst delift_by_one what (with_what : nf) (where : nf) = let rec aux_i_num_var l = function - `I(n,args) -> + `I((n,ar),args) -> if n = what + l then mk_appx (lift l with_what) (Listx.map (aux l) args) else - `I ((if delift_by_one && n >= l then n-1 else n), Listx.map (aux l) args) - | `Var n -> + `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args) + | `Var(n,ar) -> if n = what + l then lift l with_what else - `Var (if delift_by_one && n >= l then n-1 else n) + `Var((if delift_by_one && n >= l then n-1 else n), ar) | `N _ as x -> x - | `Match(t,ar,bs_lift,bs,args) -> + | `Match(t,v,bs_lift,bs,args) -> let bs_lift = bs_lift + if delift_by_one then -1 else 0 in let l' = l - bs_lift in let with_what' = lift l' with_what in (* The following line should be the identity when delift_by_one = true because we are assuming the ts to not contain lambda-bound variables. *) bs := List.map (fun (n,t) -> n,subst false what with_what' t) !bs ; - mk_match (cast_to_i_num_var (aux_i_num_var l t)) ar bs_lift bs (List.map (aux l) args) + mk_match (cast_to_i_num_var (aux_i_num_var l t)) v bs_lift bs (List.map (aux l) args) and aux l(*lift*) = (*function iii -> let res = match iii with*) function | #i_num_var as x -> aux_i_num_var l x - | `Lam(b,ar,nf) -> `Lam(b,ar,aux (l+1) nf) + | `Lam(b, nf) -> `Lam(b, aux (l+1) nf) (*in let ll = ["v0";"v1";"v2"] in 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*) in @@ -229,9 +231,9 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool let parse' strs = let rec aux = function - | Parser.Lam t -> `Lam (true,-666,aux t) + | Parser.Lam t -> `Lam (true, aux t) | Parser.App (t1, t2) -> mk_app (aux t1) (aux t2) - | Parser.Var v -> `Var v + | Parser.Var v -> `Var(v,-666) in let (tms, free) = Parser.parse_many strs in (List.map aux tms, free) ;; @@ -249,14 +251,14 @@ let eta_compare x y = | _, [] -> 1 | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in let rec aux t1 t2 = match t1, t2 with - | `Var n , `Var m -> compare n m - | `I(n1, l1), `I(n2, l2) -> + | `Var(n,_) , `Var(m,_) -> compare n m + | `I((n1,_), l1), `I((n2,_), l2) -> clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2) | `Lam _, `N _ -> -1 | `N _, `Lam _ -> 1 - | `Lam(_,_,t1), `Lam(_,_,t2) -> aux t1 t2 - | `Lam(_,_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var 0)) - | t2, `Lam(_,_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var 0)) + | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2 + | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666))) + | t2, `Lam(_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666))) | `N n1, `N n2 -> compare n1 n2 | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') -> let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in @@ -276,7 +278,7 @@ let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;; let rec eta_subterm sub t = if eta_eq sub t then true else match t with - | `Lam(_,_,t') -> eta_subterm (lift 1 sub) t' + | `Lam(_,t') -> eta_subterm (lift 1 sub) t' | `Match(u,ar,liftno,bs,args) -> eta_subterm sub (u :> nf) || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs diff --git a/ocaml/num.mli b/ocaml/num.mli index 0eaa5b0..c1ad8f0 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -1,23 +1,23 @@ -type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ] +type var = int * int +type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ] type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ] type 'nf i_num_var_ = - [ `I of int * 'nf Listx.listx - | `Match of 'nf i_num_var_ * int * int * (int * 'nf) list ref * 'nf list + [ `I of var * 'nf Listx.listx + | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list | `N of int - | `Var of int ] + | `Var of var ] type 'nf nf_ = - [ `I of int * 'nf Listx.listx - | `Lam of bool * int * 'nf nf_ - | `Match of 'nf i_num_var_ * int * int * (int * 'nf) list ref * 'nf list + [ `I of var * 'nf Listx.listx + | `Lam of bool * 'nf nf_ + | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list | `N of int - | `Var of int ] + | `Var of var ] type nf = nf nf_ type i_var = nf i_var_ type i_n_var = nf i_n_var_ type i_num_var = nf i_num_var_ val hd_of_i_var : i_var -> int -val hd_of : - [< `I of 'a * 'b | `Match of 'c | `N of 'd | `Var of 'a ] -> 'a option +val hd_of : i_n_var -> int option (* put t under n lambdas, lifting t accordingtly *) val make_lams : nf -> int -> nf val lift : int -> nf -> nf @@ -35,7 +35,7 @@ val cast_to_i_num_var : [< nf > `I `N `Match `Var] -> i_num_var val mk_app : nf -> nf -> nf val mk_appl : nf -> nf list -> nf val mk_appx : nf -> nf Listx.listx -> nf -val mk_match : nf i_num_var_ -> int -> int -> (int * nf) list ref -> nf list -> nf +val mk_match : nf i_num_var_ -> var -> int -> (int * nf) list ref -> nf list -> nf val subst : bool -> int -> nf -> nf -> nf val parse' : string list -> nf list * string list val eta_compare : nf -> nf -> int -- 2.39.2