- | _ as t -> t
- in lift (-k) (aux t)
-;;
-
-let get_arity_of_continuation p v =
- if !bomb = `Var v then 0 else (
- let bs = List.find (fun bs -> List.exists (fun (_,t) -> t = `Var v) !bs) p.deltas in
- let orig = get_var_of_match bs p in
- List.nth p.arities orig
- )
-;;
-
-let fix_arities p v freshvars =
- let all_terms = (all_terms p :> nf list) in
- let args = Util.concat_map (find_first_args v) all_terms in
- let k = List.length freshvars in
- let args = List.map (remove_lambdas k) args in
- prerr_endline ("delifted lambdas in which to look for "^ string_of_var v);
- (* List.iter (fun t -> prerr_endline(strilogng_of_nf p t)) args; *)
- (* assert (List.length args > 0); *)
- List.iter (fun v -> prerr_endline ("var to fix: fresh " ^ string_of_var v)) freshvars;
- let find_arities_args v = let i = List.fold_left (fun x t -> max x (get_arity_of_var p v t)) 0 args in prerr_endline ("found arity in args of " ^ string_of_var (List.nth (List.rev freshvars) (v+1)) ^ ": " ^ string_of_int i); i in
- (* let find_arities_all v = List.fold_left (fun x t -> max x (get_arity_of_var p v t)) 0 all_terms in *)
- let arities = List.mapi (fun var () ->
- if var < List.length p.arities
- then List.nth p.arities var
- else if List.mem var freshvars
- then 1 + find_arities_args (Util.index_of var (List.rev freshvars) - 1)
- (* else find_arities_all var *)
- else (get_arity_of_continuation p var) - 1
- ) (Array.to_list (Array.make (p.freshno+1) ())) in
- assert (List.length arities = (p.freshno + 1));
- (* prerr_endline ("arities added : " ^ string_of_int (List.length freshvars)); *)
- (* List.iter (fun (v,n) -> prerr_endline(string_of_int v ^ "=" ^ string_of_int n)) arities; *)
- {p with arities}
-;;
-
-let measure =
- let rec aux (s:state) vmap =
- let p = s.p in
- let realvar vmap v =
- (* prerr_endline ("waant " ^ string_of_int v ^ "; we have "^ string_of_int (List.length vmap)); *)
- if v < 0 then List.nth vmap (-1-v) else v in
- function
- | `Var _ | `N _-> 0
- | `I(v, tms) -> assert (List.length s.arities = (s.freshno + 1)); 1 +
- let v = realvar vmap v in
- (* prerr_endline ("lookup for arity of " ^ string_of_int v ^ "with freshno =" ^ string_of_int s.freshno ^ " and length = " ^ string_of_int (List.length s.arities)); *)
- let arity = List.nth s.arities v in
- 1 + if arity = 0 then 0 else (
- let first, rest = (match tms with
- | Listx.Nil x -> x, []
- | Listx.Cons(a,b) -> a, Listx.to_list b) in
- (
- let s, vars = mk_freshvars s (1+s.p.special_k) in
- let vmap, t = mk_apps vmap first (vars) in
- let arities = List.mapi (fun v () ->
- if v < List.length s.arities
- then List.nth s.arities v
- else get_arity_of_var p (realvar vmap v) t
- ) (Array.to_list (Array.make (s.freshno + 1) ())) in
- (* let arities = (List.map (fun v -> v, get_arity_of_var p (realvar vmap' v) t) vars) in *)
- (* let arities = arities @ s.arities in *)
- let s = {s with arities} in
- aux s vmap t
- ) + (
- let s, fresh = mk_freshvar s in
- let arities = s.arities @ [arity - 1] in
- let s = {s with arities} in
- if rest = [] then aux s vmap (`Var fresh) else
- aux s vmap (`I (fresh, Listx.from_list rest))
- )
- )
- | `Match(t, _, bs, rest) ->
- let tmp = aux s vmap (t :> nf) in
- let s, fresh = mk_freshvar s in
- let arity = List.nth s.arities (get_var_of_match bs s.p) in
- let arities = s.arities @ [arity - 1] in
- let s = {s with arities} in
- tmp + if rest = [] then aux s vmap (`Var(fresh)) else
- aux s vmap (`I(fresh, Listx.from_list rest))
- | `Lam _ -> assert false
- in fun s -> aux s []
-;;
-
-
-(* let measure p =
- let rec m = function
- | `N _ | `Var _ -> 0
- | `I(_,args) ->
- let args = Listx.to_list args in
- List.fold_left (fun acc t -> acc + m t) (1 + Listx.length args) args
- | `Lam(_,t) -> m t
- | `Match(t, lft, bs, rest) ->
- (* let var = get_var_of_match bs p in *)
- let args = rest in m (t :> nf) + List.fold_left (fun acc t -> acc + m t) (aux args) args
-
-and aux = function
- | [] -> 0
- | x::xs -> m x + if aux xs = 0 then 0 else 1 + aux xs
-in m
-;;*)
-
-let measure_many s tms = List.fold_left (fun x t -> x + (measure s t)) 0 tms;;
-
-let map_max f l = List.fold_left (fun x t -> max x (f t)) 0 l;;
-
-let measure_of_problem p =
- let tms = (all_terms p :> nf list) in
- let freshno = p.freshno in
- let arities = p.arities in
- let s = {arities; freshno; p} in
- prerr_endline (string_of_state s);
- let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
- List.iter (fun t -> prerr_endline (string_of_int (measure s t) ^ " ::" ^ print ~l t)) tms;
- let m = measure_many s tms in
- (* prerr_endline (string_of_int m); *)
- m
-;;
-end;;
-
-let measure_of_problem = ACMeasure.measure_of_problem;;
-let problem_measure = measure_of_problem;;
-(* AC MEASURE *)
-
-let print_problem label ({freshno; div; conv; ps; deltas} as p) =
- (* assert (p.steps > List.length p.sigma); *)
- let measure = try
- problem_measure p
- with
- | _ -> -1 in
- Console.print_hline ();
- prerr_endline ("\n||||| Displaying problem: " ^ label ^ " |||||");
- let nl = "\n| " in
- let deltas = String.concat nl (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
- let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
- nl ^
- (* (string_of_int (steps - List.length p.sigma)) ^ " steps left;" ^ *)
- "measure="^string_of_int measure ^" freshno = " ^ string_of_int freshno
- ^ nl ^ "\b> DISCRIMINATING SETS (deltas)"
- ^ nl ^ deltas ^ (if deltas = "" then "" else nl)
- ^ "\b> DIVERGENT" ^ nl
- ^ "*: " ^ (match div with None -> "*" | Some div -> print ~l (div :> nf)) ^ "\n| "
- ^ "\b> CONVERGENT" ^ nl
- ^ String.concat "\n| " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else print ~l (t :> nf))) conv) ^
- (if conv = [] then "" else "\n| ")
- ^ "\b> NUMERIC" ^ nl
- ^ String.concat "\n| " (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps)
- ^ nl
+ | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
+ | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many (args :> nf list)
+ and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
+ (fun t -> aux (t :> nf)), (fun l -> aux_many (l :> nf list))
+;;
+
+let sum_arities p = measure_of_terms (all_terms p)
+
+let problem_measure p = sum_arities p;;
+let string_of_measure = string_of_int;;
+
+let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
+ let aux_measure_terms t = if _measure_of_terms then "(" ^ string_of_int (measure_of_term t) ^ ") " else "" in
+ let deltas = String.concat ("\n# ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
+ let l = p.var_names in
+ String.concat "\n" ([
+ "";
+ "# DISPLAY PROBLEM (" ^ label ^ ") " ^ "measure=" ^ string_of_measure (problem_measure p);
+ if List.length p.deltas > 1 then (
+ "# Discriminating sets (deltas):\n" ^
+ "# " ^ deltas
+ ) else "# ";
+ "#";
+ "$" ^ p.label;
+ (match div with None -> "# D" | Some div -> "D " ^ aux_measure_terms div ^ print ~l (div :> nf));
+ ]
+ @ List.map (fun t -> if t = convergent_dummy then "# C" else "C " ^ aux_measure_terms t ^ print ~l (t :> nf)) conv
+ @ List.mapi (fun i t -> string_of_int i ^ " " ^ aux_measure_terms t ^ print ~l (t :> nf)) ps
+ @ [""])