open Pure
open Num
-let bomb = ref(`Var(-1,-666));;
+let divergent = ref(`Var(-1, -666));;
(*
The number of arguments which can applied to numbers
let string_of_var l x =
try
List.nth l x
- with Failure "nth" -> "`" ^ string_of_int x
+ with Failure _ -> "`" ^ string_of_int x
;;
let string_of_term p t = print ~l:p.var_names (t :> nf);;
let rec aux = function
| `N _ -> 0
| `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
| `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
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
let rec aux = function
| `N _ -> 0
| `Var(_,ar) -> if ar = min_int then 1 else 0
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
| `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
| `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
let simple_expand_match ps =
let rec aux level = function
| #i_num_var as t -> (aux_i_num_var level t :> nf)
- | `Lam(b,t) -> `Lam(b,aux (level+1) t)
+ | `Lam(b,t,g) -> assert (g = []); `Lam(b,aux (level+1) t,[])
and aux_i_num_var level = function
| `Match(u,v,bs_lift,bs,args) as torig ->
let (u : i_num_var) = aux_i_num_var level u in
| Some div ->
if List.mem (hd_of_i_var div) inedible
then p
- else
- let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
- 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'));
- bomb := bomb';
- prerr_endline ("Just created bomb var: " ^ string_of_nf !bomb);
- let x = hd_of_i_var div in
- let inst = make_lams !bomb n in
- let p = {p with div=None} in
- (* subst_in_problem (hd_of_i_var div) inst p in *)
- {p with sigma=p.sigma@[x,inst]} in
- let dangerous_conv = showstoppers_conv in
+ else (divergent := `Var(hd_of_i_var div, -666); {p with div=None}) in
+ let dangerous_conv = showstoppers_conv in
prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
let conv =
`Continue p
let instantiate p x n =
- (if hd_of_i_var (cast_to_i_var !bomb) = x
- 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 = None then failwithProblem p "step on var non occurring in problem");
(if Util.option_get(arity_of_x) = min_int then failwithProblem p "step on fake variable");
let args = Listx.from_list (vars :> nf list) in
let bs = ref [] in
(* 666, since it will be replaced anyway during subst: *)
- let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),1,bs,[])) in
+ let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),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,g) -> assert (g = []); aux (k + if b then 1 else 0) t
| `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
| `Match(t, _, liftno, bs, args) ->
List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
| `Var _ -> 0
) in
let rec aux' top t = match t with
- | `Lam(_,t) -> aux' false t
+ | `Lam(_,t,g) -> assert (g = []); aux' false t
| `I((_,ar), tms) -> max ar
(Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
| `Match(t, _, liftno, bs, args) ->
| `N n -> `N (List.nth perm n)
| `I _ -> assert false
| `Var _ as t -> t
- | `Lam(v,t) -> `Lam(v, aux t)
+ | `Lam(v,t,g) -> assert (g = []); `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
replace_in_sigma (List.rev perm) p.sigma
;;
-let env_of_sigma freshno sigma should_explode =
- let rec aux n =
- if n > freshno then
- []
- else
- let e = aux (n+1) in
- (try
- e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
- with
- Not_found ->
- if n = hd_of_i_var (cast_to_i_var !bomb)
- then ([], Pure.omega should_explode, [])
- else ([], Pure.V n, []) ) :: e
- in aux 0
-;;
(* ************************************************************************** *)
type result = [
match check p with
| Some s -> `Unseparable s
| None ->
- bomb := `Var(-1,-666);
Console.print_hline();
let p_finale = auto p p.initialSpecialK in
let freshno,sigma = p_finale.freshno, p_finale.sigma in
(string_of_var p_finale.var_names x ^ " := " ^ string_of_term p_finale inst)) sigma;
prerr_endline "---------<PURE>---------";
+ ToScott.bomb := !divergent;
let scott_of_nf t = ToScott.t_of_nf (t :> nf) in
let div = option_map scott_of_nf p.div in
let conv = List.map scott_of_nf p.conv in
let ps = List.map scott_of_nf p.ps in
let sigma' = List.map (fun (x,inst) -> x, scott_of_nf inst) sigma in
- let e' = env_of_sigma freshno sigma' false in
- let e'' = env_of_sigma freshno sigma' true in
+ let e' = Pure.env_of_sigma freshno sigma' in
prerr_endline "--------<REDUCE>---------";
(function
| None -> ()) div;
List.iter (fun n ->
verbose ("_::: " ^ (Pure.print n));
- let t = Pure.mwhd (e'',n,[]) in
+ let t = Pure.mwhd (e',n,[]) in
verbose ("_:: " ^ (Pure.print t));
assert (not (Pure.diverged t))
) conv ;
[ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
{freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label}
;;
+
+(* assert_depends solves the problem, and checks if the result was expected *)
+let assert_depends x =
+ let c = String.sub (label_of_problem x) 0 1 in
+ match solve x with
+ | `Unseparable s when c = "!" ->
+ failwith ("assert_depends: unseparable because: " ^ s ^ ".")
+ | `Separable _ when c = "?" ->
+ failwith ("assert_depends: separable.")
+ | _ -> () in
+Problems.main (assert_depends ++ problem_of);
projects / fireball-separation.git / blobdiff