From f7ed79cb0dc07847da37b68af96f13223ce71079 Mon Sep 17 00:00:00 2001 From: acondolu Date: Tue, 29 May 2018 11:03:42 +0200 Subject: [PATCH] Removed useless `isdiv' flag --- ocaml/andrea.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml index c5ef32e..85c385e 100644 --- a/ocaml/andrea.ml +++ b/ocaml/andrea.ml @@ -98,19 +98,19 @@ let rec args_no = function | _ -> assert false ;; -let rec subst level delift fromdiv sub = +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 fromdiv sub t) + | L t -> L (subst (level + 1) delift sub t) | A (t1,t2) -> - let t1 = subst level delift fromdiv sub t1 in - let t2 = subst level delift fromdiv sub t2 in - if t1 = B || t2 = B then B else mk_app fromdiv t1 t2 + let t1 = subst level delift sub t1 in + let t2 = subst level delift sub t2 in + if t1 = B || t2 = B then B else mk_app t1 t2 | B -> B | P -> P -and mk_app fromdiv t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with +and mk_app t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with | B | _ when t2 = B -> B - | L t1 -> subst 0 true fromdiv (0, t2) t1 + | L t1 -> subst 0 true (0, t2) t1 | t1 -> A (t1, t2) and lift n = let rec aux n' = @@ -127,8 +127,8 @@ let subst = subst 0 false;; let subst_in_problem (sub: var * t) (p: problem) = print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub)); let p = {p with stepped=(fst sub)::p.stepped} in - let conv = subst false sub p.conv in - let div = subst true sub p.div in + let conv = subst sub p.conv in + let div = subst sub p.div in let p = {p with div; conv} in (* print_endline ("after sub: \n" ^ string_of_problem p); *) {p with sigma=sub::p.sigma} @@ -204,7 +204,7 @@ let parse strs = let rec aux level = function | Parser.Lam t -> L (aux (level + 1) t) | Parser.App (t1, t2) -> - if level = 0 then mk_app false (aux level t1) (aux level t2) + if level = 0 then mk_app (aux level t1) (aux level t2) else A(aux level t1, aux level t2) | Parser.Var v -> V v in let (tms, free) = Parser.parse_many strs @@ -288,7 +288,7 @@ let rec auto p = let n_args = args_no p.div in match get_subterm_with_head_and_args hd_var n_args p.conv with | None -> - (try let p = eat p in problem_fail p "Auto did not complete the problem" with Done _ -> ()) + (try problem_fail (eat p) "Auto did not complete the problem" with Done _ -> ()) | Some t -> let j = find_eta_difference p t n_args - 1 in let k = max -- 2.39.2