From: acondolu Date: Fri, 7 Jul 2017 17:16:29 +0000 (+0200) Subject: Fixes to how arities are assigned and propagated X-Git-Tag: weak-reduction-separation~70 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ffece1568ae283bde759da5e146fbbd3eda66303;p=fireball-separation.git Fixes to how arities are assigned and propagated - added truelam to subst (useless, can be removed) - TODO: to measure the problem, count the `fake` variables which are the ones with arity = min_int --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index acfec51..8498513 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -110,7 +110,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) | [] -> acc | t::todo_ps -> (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - let t = subst false x inst (t :> nf) in + let t = subst false 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,-666)::todo_ps,acc_new_ps) t @@ -124,7 +124,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) | t::todo_conv -> (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) (* try *) - let t = subst false x inst (t :> nf) in + let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t @@ -137,7 +137,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) function | None -> freshno, None, acc_new_ps | Some t -> - let t = subst false x inst (t :> nf) in + let t = subst false false x inst (t :> nf) in let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in @@ -151,7 +151,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) match u with | `N i -> acc_new_ps,i | _ -> - let ps = List.map (fun t -> cast_to_i_num_var (subst false x inst (t:> nf))) (acc_ps@acc_new_ps) in + let ps = List.map (fun t -> cast_to_i_num_var (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in let super_simplified_ps = super_simplify_ps ps ps in (*prerr_endline ("CERCO u:" ^ print (fst u :> nf)); List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps; @@ -420,16 +420,15 @@ let instantiate p x n = then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!")); let arity_of_x = max_arity_tms x (all_terms p) in (if arity_of_x < 0 then failwithProblem p "step on a var of negative arity"); - (* AC: FIXME compute arities correctly below! *) - let arities = Num.compute_arities x (n+1) (all_terms p :> nf list) in + (* AC: Once upon a time, it was: + let arities = Num.compute_arities x (n+1) (all_terms p :> nf list) in *) (* let arities = Array.to_list (Array.make (n+1) 0) in *) + let arities = Array.to_list (Array.make (n+1) min_int) 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 inst = `Lam(false,`Match(`I((0,0),Listx.map (lift 1) args),(x,arity_of_x),1,bs,[])) in + (* min_int, since it will be replaced anyway during subst: *) + let inst = `Lam(false,`Match(`I((0,n+1),Listx.map (lift 1) args),(x,min_int),1,bs,[])) in let p = {p with deltas=bs::p.deltas} in subst_in_problem x inst p ;; diff --git a/ocaml/num.ml b/ocaml/num.ml index 81bb1da..3c84f4f 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -169,7 +169,7 @@ let rec mk_app (h : nf) (arg : nf) = match h with `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 *) + | `Lam(truelam,nf) -> subst truelam 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 @@ -194,10 +194,11 @@ and mk_match t (n,ar) bs_lift bs args = `Match (t,(n,ar),bs_lift,bs,args)) | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args) -and subst delift_by_one what (with_what : nf) (where : nf) = +and subst truelam delift_by_one what (with_what : nf) (where : nf) = let aux_propagate_arity ar = function - | `Lam(false,`Match(`I(v,args),(x,_),liftno,bs,args')) -> + | `Lam(false,`Match(`I(v,args),(x,_),liftno,bs,args')) when not delift_by_one -> `Lam(false,`Match(`I(v,args),(x,ar),liftno,bs,args')) + | `Var(i,_) -> `Var(i,ar) | _ as t -> t in let rec aux_i_num_var l = function @@ -218,7 +219,7 @@ and subst delift_by_one what (with_what : nf) (where : nf) = 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 ; + bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ; 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*) diff --git a/ocaml/num.mli b/ocaml/num.mli index e06a821..c981cff 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -38,7 +38,7 @@ 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_ -> var -> int -> (int * nf) list ref -> nf list -> nf -val subst : bool -> int -> nf -> nf -> nf +val subst : bool -> bool -> int -> nf -> nf -> nf val parse' : string list -> nf list * string list val eta_compare : nf -> nf -> int val eta_eq : [< nf ] -> [< nf ] -> bool