From a56b79f325d6fc7e85ec0b65669047232674e98b Mon Sep 17 00:00:00 2001 From: Date: Thu, 22 Jun 2017 16:23:21 +0200 Subject: [PATCH] Updated type of terms with arities in lambda and matche --- ocaml/num.ml | 58 +++++++++++++++++++++++++-------------------------- ocaml/num.mli | 8 +++---- 2 files changed, 33 insertions(+), 33 deletions(-) diff --git a/ocaml/num.ml b/ocaml/num.ml index 6f3cae5..7f94b25 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -19,9 +19,9 @@ type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ] 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_ * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list + | `Match of 'nf i_num_var_ * (* arity of branches *) int * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list ] -type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | 'nf i_num_var_ ] +type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * (* arity of variable*) int * 'nf nf_ | 'nf i_num_var_ ] type nf = nf nf_ type i_var = nf i_var_;; type i_n_var = nf i_n_var_;; @@ -45,12 +45,12 @@ let lift m (t : nf) = `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) | `N _ as x -> x - | `Match(t,lift,bs,args) -> - `Match(aux_i_num_var l t, lift + m, bs, List.map (aux l) args) + | `Match(t,ar,lift,bs,args) -> + `Match(aux_i_num_var l t, ar,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,nf) -> `Lam (b,aux (l+1) nf) + | `Lam(b,ar,nf) -> `Lam (b,ar,aux (l+1) nf) in (aux 0 t : nf) ;; @@ -59,7 +59,7 @@ let lift m (t : nf) = let rec make_lams t = function 0 -> t - | n when n > 0 -> `Lam (false,lift 1 (make_lams t (n-1))) + | n when n > 0 -> `Lam (false,-666,lift 1 (make_lams t (n-1))) | _ -> assert false let free_vars = @@ -69,8 +69,8 @@ let free_vars = | `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 - | `Match(t,liftno,bs,args) -> + | `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) @ List.concat (List.map (aux n) args) @@ -84,7 +84,7 @@ let rec t_of_i_num_var = function | `N n -> Scott.mk_n n | `Var v -> Pure.V v - | `Match(t,liftno,bs,args) -> + | `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 @@ -93,7 +93,7 @@ let rec t_of_i_num_var = 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 @@ -104,12 +104,12 @@ let rec print ?(l=[]) = function `Var n -> print_name l n | `N n -> string_of_int n - | `Match(t,bs_lift,bs,args) -> + | `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) -> + | `Lam(_,_,nf) -> let name = string_of_var (List.length l) in "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf) ;; @@ -120,7 +120,7 @@ let rec string_of_term l = | `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 ^ ")" - | `Match(t,bs_lift,bs,args) -> + | `Match(t,_,bs_lift,bs,args) -> "(match " ^ string_of_term_no_pars l (t :> nf) ^ " 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) ^ ")" @@ -128,7 +128,7 @@ let rec string_of_term l = | `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 @@ -168,8 +168,8 @@ let rec mk_app (h : nf) (arg : nf) = 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) - | `Match(t,lift,bs,args) -> `Match(t,lift,bs,List.append args [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]) | `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*) @@ -180,7 +180,7 @@ and mk_appl h args = and mk_appx h args = Listx.fold_left mk_app h args -and mk_match t bs_lift bs args = +and mk_match t ar bs_lift bs args = (*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));*) match t with `N m -> @@ -189,8 +189,8 @@ and mk_match t bs_lift bs args = let h = lift bs_lift h in mk_appl h args with Not_found -> - `Match (t,bs_lift,bs,args)) - | `I _ | `Var _ | `Match _ -> `Match(t,bs_lift,bs,args) + `Match (t,ar,bs_lift,bs,args)) + | `I _ | `Var _ | `Match _ -> `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 = @@ -206,19 +206,19 @@ and subst delift_by_one what (with_what : nf) (where : nf) = else `Var (if delift_by_one && n >= l then n-1 else n) | `N _ as x -> x - | `Match(t,bs_lift,bs,args) -> + | `Match(t,ar,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)) bs_lift bs (List.map (aux l) args) + mk_match (cast_to_i_num_var (aux_i_num_var l t)) ar 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,nf) -> `Lam(b,aux (l+1) nf) + | `Lam(b,ar,nf) -> `Lam(b,ar,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,7 +229,7 @@ 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,aux t) + | Parser.Lam t -> `Lam (true,-666,aux t) | Parser.App (t1, t2) -> mk_app (aux t1) (aux t2) | Parser.Var v -> `Var v in let (tms, free) = Parser.parse_many strs @@ -254,11 +254,11 @@ let eta_compare x y = 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)) + | t2, `Lam(_,_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var 0)) | `N n1, `N n2 -> compare n1 n2 - | `Match(u,bs_lift,bs,args), `Match(u',bs_lift',bs',args') -> + | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') -> let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args')) @@ -276,8 +276,8 @@ 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' - | `Match(u,liftno,bs,args) -> + | `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 || List.exists (eta_subterm sub) args diff --git a/ocaml/num.mli b/ocaml/num.mli index 2f92884..0eaa5b0 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -2,13 +2,13 @@ type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ] 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 * 'nf) list ref * 'nf list + | `Match of 'nf i_num_var_ * int * int * (int * 'nf) list ref * 'nf list | `N of int | `Var of int ] type 'nf nf_ = [ `I of int * 'nf Listx.listx - | `Lam of bool * 'nf nf_ - | `Match of 'nf i_num_var_ * int * (int * 'nf) list ref * 'nf list + | `Lam of bool * int * 'nf nf_ + | `Match of 'nf i_num_var_ * int * int * (int * 'nf) list ref * 'nf list | `N of int | `Var of int ] type nf = 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 * nf) list ref -> nf list -> nf +val mk_match : nf i_num_var_ -> int -> 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