From ade21b2ea3af70e54e030c62f8b46a996f9ca8fb Mon Sep 17 00:00:00 2001 From: acondolu Date: Wed, 30 May 2018 18:46:04 +0200 Subject: [PATCH] Made bombs more explosive (strongly) --- ocaml/andrea.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml index 41b7372..07cf670 100644 --- a/ocaml/andrea.ml +++ b/ocaml/andrea.ml @@ -106,16 +106,17 @@ let rec get_inert = function let rec subst level delift sub = function | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v) - | L t -> L (subst (level + 1) delift sub t) + | L t -> let t = subst (level + 1) delift sub t in if t = B then B else L t | A (t1,t2) -> let t1 = subst level delift sub t1 in let t2 = subst level delift sub t2 in mk_app t1 t2 | B -> B -and mk_app t1 t2 = if t1 = delta && t2 = delta then B else match t1 with - | B | _ when t2 = B -> B +and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B + else match t1 with + | B -> B | L t1 -> subst 0 true (0, t2) t1 - | t1 -> A (t1, t2) + | _ -> A (t1, t2) and lift n = let rec aux lev = function @@ -158,6 +159,7 @@ let rec purify = function ;; let check p sigma = + print_endline "Checking..."; let div = purify p.div in let conv = purify p.conv in let sigma = List.map (fun (v,t) -> v, purify t) sigma in -- 2.39.2