From 461dcd3dc0bf5090be9980548bc1874a423dc6cc Mon Sep 17 00:00:00 2001 From: acondolu Date: Wed, 30 May 2018 12:36:15 +0200 Subject: [PATCH] Clean up --- ocaml/andrea.ml | 95 ++++++++++++++++++++++--------------------------- 1 file changed, 43 insertions(+), 52 deletions(-) diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml index c8710f4..affdcad 100644 --- a/ocaml/andrea.ml +++ b/ocaml/andrea.ml @@ -35,24 +35,23 @@ type problem = { exception Done of (var * t) list (* substitution *);; exception Fail of int * string;; -let string_of_t p = - let bound_vars = ["x"; "y"; "z"; "w"; "q"] in +let string_of_t = + let string_of_bvar = + let bound_vars = ["x"; "y"; "z"; "w"; "q"] in + let bvarsno = List.length bound_vars in + fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in let rec string_of_term_w_pars level = function | V v -> if v >= level then "`" ^ string_of_int (v-level) else - let nn = level - v-1 in - if nn < 5 then List.nth bound_vars nn else "x" ^ (string_of_int (nn-4)) + string_of_bvar (level - v-1) | A _ - | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")" + | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")" | B -> "BOT" | P -> "PAC" and string_of_term_no_pars_app level = function - | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2) + | A(t1,t2) -> string_of_term_no_pars_app level t1 ^ " " ^ string_of_term_w_pars level t2 | _ as t -> string_of_term_w_pars level t - and string_of_term_no_pars_lam level = function - | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t) - | _ as t -> string_of_term_no_pars level t and string_of_term_no_pars level = function - | L _ as t -> string_of_term_no_pars_lam level t + | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t | _ as t -> string_of_term_no_pars_app level t in string_of_term_no_pars 0 ;; @@ -60,8 +59,8 @@ let string_of_t p = let string_of_problem p = let lines = [ "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped); - "[DV] " ^ (string_of_t p p.div); - "[CV] " ^ (string_of_t p p.conv); + "[DV] " ^ string_of_t p.div; + "[CV] " ^ string_of_t p.conv; ] in String.concat "\n" lines ;; @@ -86,15 +85,9 @@ let rec is_inert = let is_var = function V _ -> true | _ -> false;; let is_lambda = function L _ -> true | _ -> false;; -let rec head_of_inert = function - | V n -> n - | A(t, _) -> head_of_inert t - | _ -> assert false -;; - -let rec args_no = function - | V _ -> 0 - | A(t, _) -> 1 + args_no t +let rec get_inert = function + | V n -> (n,0) + | A(t, _) -> let hd,args = get_inert t in hd,args+1 | _ -> assert false ;; @@ -105,7 +98,7 @@ let rec subst level delift sub = | A (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 + mk_app t1 t2 | B -> B | P -> P and mk_app t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with @@ -113,11 +106,11 @@ and mk_app t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with | L t1 -> subst 0 true (0, t2) t1 | t1 -> A (t1, t2) and lift n = - let rec aux n' = + let rec aux lev = function - | V m -> V (if m >= n' then m + n else m) - | L t -> L (aux (n'+1) t) - | A (t1, t2) -> A (aux n' t1, aux n' t2) + | V m -> V (if m >= lev then m + n else m) + | L t -> L (aux (lev+1) t) + | A (t1, t2) -> A (aux lev t1, aux lev t2) | B -> B | P -> P in aux 0 @@ -125,13 +118,12 @@ and lift n = 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 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} +print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub)); + {p with + div=subst sub p.div; + conv=subst sub p.conv; + stepped=(fst sub)::p.stepped; + sigma=sub::p.sigma} ;; let get_subterm_with_head_and_args hd_var n_args = @@ -139,7 +131,8 @@ let get_subterm_with_head_and_args hd_var n_args = | V _ | B | P -> None | L t -> aux (lev+1) t | A(t1,t2) as t -> - if head_of_inert t1 = hd_var + lev && n_args <= 1 + args_no t1 (* why `1+' ?*) + let hd_var', n_args' = get_inert t1 in + if hd_var' = hd_var + lev && n_args <= 1 + n_args' then Some (lift ~-lev t) else match aux lev t2 with | None -> aux lev t1 @@ -156,11 +149,9 @@ let get_subterm_with_head_and_args hd_var n_args = let sanity p = print_endline (string_of_problem p); (* non cancellare *) - if p.div = B then raise (Done p.sigma); - if not (is_inert p.div) then problem_fail p "p.div converged"; if p.conv = B then problem_fail p "p.conv diverged"; - (* let p = if is_var p.div then simple_explode p else p in *) - p + if p.div = B then raise (Done p.sigma); + if not (is_inert p.div) then problem_fail p "p.div converged" ;; let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);; @@ -169,20 +160,20 @@ let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);; It does NOT perform any check, may fail if done unsafely *) let eat p = print_cmd "EAT" ""; - let var = head_of_inert p.div in - let n = args_no p.div in + let var, n = get_inert p.div in let rec aux m t = if m = 0 then lift n t else L (aux (m-1) t) in let subst = var, aux n B in - sanity (subst_in_problem subst p) + let p = subst_in_problem subst p in + sanity p; p ;; (* step on the head of div, on the k-th argument, with n fresh vars *) let step k n p = - let var = head_of_inert p.div in - print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")"); + let var, _ = get_inert p.div in + print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")"); let rec aux' p m t = if m < 0 then p, t @@ -198,7 +189,8 @@ let step k n p = else L (aux (m-1) t) in let t = aux k t in let subst = var, t in - sanity (subst_in_problem subst p) + let p = subst_in_problem subst p in + sanity p; p ;; let parse strs = @@ -230,7 +222,7 @@ let problem_of div conv = (print_endline ("after subst in problem " ^ string_of_problem p); p) with Not_found -> p in (* initial sanity check *) - sanity p + sanity p; p ;; let exec div conv cmds = @@ -258,7 +250,7 @@ let find_eta_difference p t n_args = let rec aux t u k = match t, u with | V _, V _ -> assert false (* div subterm of conv *) | A(t1,t2), A(u1,u2) -> - if not (eta_eq t2 u2) then (print_endline((string_of_t p t2) ^ " <> " ^ (string_of_t p u2)); k) + if not (eta_eq t2 u2) then (print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2)); k) else aux t1 u1 (k-1) | _, _ -> assert false in aux p.div t n_args @@ -272,10 +264,10 @@ let rec no_leading_lambdas = function let compute_max_lambdas_at hd_var j = let rec aux hd = function | A(t1,t2) -> - (if head_of_inert t1 = hd && args_no t1 = j - then max ( - if is_inert t2 && head_of_inert t2 = hd - then j - args_no t2 + (if get_inert t1 = (hd, j) + then max ( (*FIXME*) + if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd + then let hd', j' = get_inert t2 in j - j' else no_leading_lambdas t2) else id) (max (aux hd t1) (aux hd t2)) | L t -> aux (hd+1) t @@ -285,8 +277,7 @@ let compute_max_lambdas_at hd_var j = ;; let rec auto p = - let hd_var = head_of_inert p.div in - let n_args = args_no p.div in + let hd_var, n_args = get_inert p.div in match get_subterm_with_head_and_args hd_var n_args p.conv with | None -> (try problem_fail (eat p) "Auto did not complete the problem" with Done _ -> ()) -- 2.39.2