From 4674dd787b5141c8aa22339d497ba671f4435da5 Mon Sep 17 00:00:00 2001 From: acondolu Date: Sat, 22 Jul 2017 21:34:23 +0200 Subject: [PATCH] Simplified arity_of, precompute_edible_data, critical_showsteppers (cherry picked from commit 4c81587c5f911c4d5f818765106bb5373967d715) --- ocaml/lambda4.ml | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 9c92c71..e56a496 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -254,10 +254,9 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif exception Dangerous -let arity_of arities k = - let _,pos,y = List.find (fun (v,_,_) -> v=k) arities in - let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | `N _ -> assert false in - arity + if pos = -1 then - 1 else 0 +let arity_of arities hd = + let pos,_,nargs = List.find (fun (_,hd',_) -> hd=hd') arities in + nargs + if pos = -1 then - 1 else 0 ;; let rec dangerous arities showstoppers = @@ -356,11 +355,14 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p. ;; let precompute_edible_data {ps; div} xs = - (match div with None -> [] | Some div -> [hd_of_i_var div, -1, (div :> i_n_var)]) @ - List.map (fun hd -> + let aux t = match t with `Var _ -> 0 | `I(_, args) -> Listx.length args | `N _ -> assert false in + (fun l -> match div with + | None -> l + | Some div -> (-1, hd_of_i_var div, aux div) :: l) + (List.map (fun hd -> let i, tm = Util.findi (fun y -> hd_of y = Some hd) ps in - hd, i, tm - ) xs + i, hd, aux tm + ) xs) ;; let critical_showstoppers p = @@ -402,23 +404,21 @@ let eat p = let showstoppers = showstoppers_step @ showstoppers_eat in let heads = List.sort compare (filter_map hd_of ps) in let arities = precompute_edible_data p (uniq heads) in - let showstoppers, showstoppers_conv = - edible p arities showstoppers in - let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in + let showstoppers, showstoppers_conv = edible p arities showstoppers in + let l = List.filter (fun (_,hd,_) -> not (List.mem hd showstoppers)) arities in let p = - List.fold_left (fun p (x,pos,(xx : i_n_var)) -> if pos = -1 then p else - let n = match xx with `I(_,args) -> Listx.length args | _ -> 0 in + List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else let v = `N(pos) in - let inst = make_lams v n in -prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names x ^ " := " ^ string_of_term p inst); - { p with sigma = p.sigma @ [x,inst] } + let inst = make_lams v nargs in +prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst); + { p with sigma = p.sigma @ [hd,inst] } ) p l in (* to avoid applied numbers in safe positions that trigger assert failures subst_in_problem x inst p*) let ps = List.map (fun t -> try - let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in + let j,_,_ = List.find (fun (_,hd,_) -> hd_of t = Some hd) l in `N j with Not_found -> t ) ps in -- 2.39.2