1907 IConst (type_tag, T --> T, [T]) |
1907 IConst (type_tag, T --> T, [T]) |
1908 |> mangle_type_args_in_iterm format type_enc |
1908 |> mangle_type_args_in_iterm format type_enc |
1909 |> ho_term_from_iterm ctxt format mono type_enc pos |
1909 |> ho_term_from_iterm ctxt format mono type_enc pos |
1910 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]) |
1910 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]) |
1911 | _ => raise Fail "unexpected lambda-abstraction") |
1911 | _ => raise Fail "unexpected lambda-abstraction") |
1912 and ho_term_from_iterm ctxt format mono type_enc = |
1912 and ho_term_from_iterm ctxt format mono type_enc pos = |
1913 let |
1913 let |
|
1914 fun beta_red bs (IApp (IAbs ((name, _), tm), tm')) = |
|
1915 beta_red ((name, beta_red bs tm') :: bs) tm |
|
1916 | beta_red bs (IApp tmp) = IApp (pairself (beta_red bs) tmp) |
|
1917 | beta_red bs (tm as IConst (name, _, _)) = |
|
1918 (case AList.lookup (op =) bs name of |
|
1919 SOME tm' => tm' |
|
1920 | NONE => tm) |
|
1921 | beta_red bs (IAbs ((name, T), tm)) = |
|
1922 IAbs ((name, T), beta_red (AList.delete (op =) name bs) tm) |
|
1923 | beta_red _ tm = tm |
1914 fun term site u = |
1924 fun term site u = |
1915 let |
1925 let |
1916 val (head, args) = strip_iterm_comb u |
1926 val (head, args) = strip_iterm_comb u |
1917 val pos = |
1927 val pos = |
1918 case site of |
1928 case site of |
1920 | Eq_Arg pos => pos |
1930 | Eq_Arg pos => pos |
1921 | _ => NONE |
1931 | _ => NONE |
1922 val t = |
1932 val t = |
1923 case head of |
1933 case head of |
1924 IConst (name as (s, _), _, T_args) => |
1934 IConst (name as (s, _), _, T_args) => |
1925 let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere in |
1935 let |
|
1936 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere |
|
1937 in |
1926 map (term arg_site) args |> mk_aterm format type_enc name T_args |
1938 map (term arg_site) args |> mk_aterm format type_enc name T_args |
1927 end |
1939 end |
1928 | IVar (name, _) => |
1940 | IVar (name, _) => |
1929 map (term Elsewhere) args |> mk_aterm format type_enc name [] |
1941 map (term Elsewhere) args |> mk_aterm format type_enc name [] |
1930 | IAbs ((name, T), tm) => |
1942 | IAbs ((name, T), tm) => |
1939 if should_tag_with_type ctxt mono type_enc site u T then |
1951 if should_tag_with_type ctxt mono type_enc site u T then |
1940 tag_with_type ctxt format mono type_enc pos T t |
1952 tag_with_type ctxt format mono type_enc pos T t |
1941 else |
1953 else |
1942 t |
1954 t |
1943 end |
1955 end |
1944 in term o Top_Level end |
1956 in term (Top_Level pos) o beta_red [] end |
1945 and formula_from_iformula ctxt polym_constrs format mono type_enc |
1957 and formula_from_iformula ctxt polym_constrs format mono type_enc |
1946 should_guard_var = |
1958 should_guard_var = |
1947 let |
1959 let |
1948 val thy = Proof_Context.theory_of ctxt |
1960 val thy = Proof_Context.theory_of ctxt |
1949 val level = level_of_type_enc type_enc |
1961 val level = level_of_type_enc type_enc |