Current section
37 Versions
Jump to
Current section
37 Versions
Compare versions
9
files changed
+66
additions
-45
deletions
| @@ -111,7 +111,7 @@ in `mix.exs`: | |
| 111 111 | ```elixir |
| 112 112 | def deps do |
| 113 113 | [ |
| 114 | - {:shot_ds, "~> 0.1.0"} |
| 114 | + {:shot_ds, "~> 0.1.1"} |
| 115 115 | ] |
| 116 116 | end |
| 117 117 | ``` |
| @@ -1,6 +1,6 @@ | |
| 1 1 | {<<"links">>,[{<<"GitHub">>,<<"https://github.com/jcschuster/ShotDs">>}]}. |
| 2 2 | {<<"name">>,<<"shot_ds">>}. |
| 3 | - {<<"version">>,<<"0.1.0">>}. |
| 3 | + {<<"version">>,<<"0.1.1">>}. |
| 4 4 | {<<"description">>, |
| 5 5 | <<"Data structures for various HOL objects and TH0 parser.">>}. |
| 6 6 | {<<"elixir">>,<<"~> 1.19">>}. |
| @@ -95,8 +95,11 @@ defmodule ShotDs.Data.Declaration do | |
| 95 95 | prefix <> format_name(name) <> suffix |
| 96 96 | end |
| 97 97 | |
| 98 | - defp format_name(ref) when is_reference(ref), do: "[#{ShotDs.Util.Formatter.short_ref(ref)}]" |
| 99 | - defp format_name(name) when is_binary(name) or is_integer(name), do: Kernel.to_string(name) |
| 98 | + defp format_name(ref) when is_reference(ref), |
| 99 | + do: "[#{ShotDs.Util.Formatter.short_ref(ref)}]" |
| 100 | + |
| 101 | + defp format_name(name) when is_binary(name) or is_integer(name), |
| 102 | + do: Kernel.to_string(name) |
| 100 103 | |
| 101 104 | defp kind_prefix(:fv), do: "V" |
| 102 105 | defp kind_prefix(:co), do: "C" |
| @@ -2,8 +2,8 @@ defmodule ShotDs.Data.Term do | |
| 2 2 | @moduledoc """ |
| 3 3 | Represents a Hol term as directed acyclic graph (DAG). |
| 4 4 | |
| 5 | - All terms contain a deterministic ID assigned by `ShotDs.Stt.TermFactory`. Note |
| 6 | - that terms are in βη-normal form, i.e., fully β-reduced and η-expanded. |
| 5 | + All terms contain a deterministic ID assigned by `ShotDs.Stt.TermFactory`. |
| 6 | + Note that terms are in βη-normal form, i.e., fully β-reduced and η-expanded. |
| 7 7 | |
| 8 8 | Besides the obvious fields `:head`, `:args` and `:type`, two accessor fields |
| 9 9 | are implemented for efficiency: `:fvars` contains all free variables |
| @@ -165,7 +165,8 @@ defmodule ShotDs.Hol.Definitions do | |
| 165 165 | Constant representing equality over instances of the given type. |
| 166 166 | """ |
| 167 167 | @spec equals_const(Type.t()) :: Declaration.const_t() |
| 168 | - def equals_const(%Type{} = t), do: Declaration.new_const("=", Type.new(:o, [t, t])) |
| 168 | + def equals_const(%Type{} = t), |
| 169 | + do: Declaration.new_const("=", Type.new(:o, [t, t])) |
| 169 170 | |
| 170 171 | @doc group: :Constants |
| 171 172 | @doc """ |
| @@ -173,7 +174,8 @@ defmodule ShotDs.Hol.Definitions do | |
| 173 174 | given element type. |
| 174 175 | """ |
| 175 176 | @spec pi_const(Type.t()) :: Declaration.const_t() |
| 176 | - def pi_const(%Type{} = t), do: Declaration.new_const("Π", Type.new(:o, Type.new(:o, t))) |
| 177 | + def pi_const(%Type{} = t), |
| 178 | + do: Declaration.new_const("Π", Type.new(:o, Type.new(:o, t))) |
| 177 179 | |
| 178 180 | @doc group: :Constants |
| 179 181 | @doc """ |
| @@ -181,7 +183,8 @@ defmodule ShotDs.Hol.Definitions do | |
| 181 183 | the given element type. |
| 182 184 | """ |
| 183 185 | @spec sigma_const(Type.t()) :: Declaration.const_t() |
| 184 | - def sigma_const(%Type{} = t), do: Declaration.new_const("Σ", Type.new(:o, Type.new(:o, t))) |
| 186 | + def sigma_const(%Type{} = t), |
| 187 | + do: Declaration.new_const("Σ", Type.new(:o, Type.new(:o, t))) |
| 185 188 | |
| 186 189 | ############################################################################# |
| 187 190 | # TERMS |
| @@ -244,8 +247,12 @@ defmodule ShotDs.Hol.Definitions do | |
| 244 247 | x = Declaration.new_free_var("X", type_o()) |
| 245 248 | y = Declaration.new_free_var("Y", type_o()) |
| 246 249 | |
| 247 | - conj = and_term() |> TF.make_appl_term(TF.make_term(x)) |> TF.make_appl_term(TF.make_term(y)) |
| 248 | - neg_term() |> TF.make_appl_term(conj) |> TF.make_abstr_term(y) |> TF.make_abstr_term(x) |
| 250 | + and_term() |
| 251 | + |> TF.make_appl_term(TF.make_term(x)) |
| 252 | + |> TF.make_appl_term(TF.make_term(y)) |
| 253 | + |> then(&TF.make_appl_term(neg_term(), &1)) |
| 254 | + |> TF.make_abstr_term(y) |
| 255 | + |> TF.make_abstr_term(x) |
| 249 256 | end |
| 250 257 | |
| 251 258 | @doc group: :Terms |
| @@ -287,12 +294,12 @@ defmodule ShotDs.Hol.Definitions do | |
| 287 294 | x = Declaration.new_free_var("X", type_o()) |
| 288 295 | y = Declaration.new_free_var("Y", type_o()) |
| 289 296 | |
| 290 | - equiv = |
| 291 | - equivalent_term() |
| 292 | - |> TF.make_appl_term(TF.make_term(x)) |
| 293 | - |> TF.make_appl_term(TF.make_term(y)) |
| 294 | - |
| 295 | - neg_term() |> TF.make_appl_term(equiv) |> TF.make_abstr_term(y) |> TF.make_abstr_term(x) |
| 297 | + equivalent_term() |
| 298 | + |> TF.make_appl_term(TF.make_term(x)) |
| 299 | + |> TF.make_appl_term(TF.make_term(y)) |
| 300 | + |> then(&TF.make_appl_term(neg_term(), &1)) |
| 301 | + |> TF.make_abstr_term(y) |
| 302 | + |> TF.make_abstr_term(x) |
| 296 303 | end |
| 297 304 | |
| 298 305 | @doc group: :Terms |
| @@ -300,7 +307,8 @@ defmodule ShotDs.Hol.Definitions do | |
| 300 307 | Term representing equality over instances of the given type. |
| 301 308 | """ |
| 302 309 | @spec equals_term(Type.t()) :: Term.term_id() |
| 303 | - def equals_term(%Type{} = t), do: TF.make_const_term("=", Type.new(:o, [t, t])) |
| 310 | + def equals_term(%Type{} = t), |
| 311 | + do: TF.make_const_term("=", Type.new(:o, [t, t])) |
| 304 312 | |
| 305 313 | @doc group: :Terms |
| 306 314 | @doc """ |
| @@ -312,10 +320,12 @@ defmodule ShotDs.Hol.Definitions do | |
| 312 320 | x = Declaration.new_free_var("X", t) |
| 313 321 | y = Declaration.new_free_var("Y", t) |
| 314 322 | |
| 315 | - eq = |
| 316 | - equals_term(t) |> TF.make_appl_term(TF.make_term(x)) |> TF.make_appl_term(TF.make_term(y)) |
| 317 | - |
| 318 | - neg_term() |> TF.make_appl_term(eq) |> TF.make_abstr_term(y) |> TF.make_abstr_term(x) |
| 323 | + equals_term(t) |
| 324 | + |> TF.make_appl_term(TF.make_term(x)) |
| 325 | + |> TF.make_appl_term(TF.make_term(y)) |
| 326 | + |> then(&TF.make_appl_term(neg_term(), &1)) |
| 327 | + |> TF.make_abstr_term(y) |
| 328 | + |> TF.make_abstr_term(x) |
| 319 329 | end |
| 320 330 | |
| 321 331 | @doc group: :Terms |
| @@ -324,7 +334,8 @@ defmodule ShotDs.Hol.Definitions do | |
| 324 334 | given element type. |
| 325 335 | """ |
| 326 336 | @spec pi_term(Type.t()) :: Term.term_id() |
| 327 | - def pi_term(%Type{} = t), do: TF.make_const_term("Π", Type.new(:o, Type.new(:o, t))) |
| 337 | + def pi_term(%Type{} = t), |
| 338 | + do: TF.make_const_term("Π", Type.new(:o, Type.new(:o, t))) |
| 328 339 | |
| 329 340 | @doc group: :Terms |
| 330 341 | @doc """ |
| @@ -332,7 +343,8 @@ defmodule ShotDs.Hol.Definitions do | |
| 332 343 | the given element type. |
| 333 344 | """ |
| 334 345 | @spec sigma_term(Type.t()) :: Term.term_id() |
| 335 | - def sigma_term(%Type{} = t), do: TF.make_const_term("Σ", Type.new(:o, Type.new(:o, t))) |
| 346 | + def sigma_term(%Type{} = t), |
| 347 | + do: TF.make_const_term("Σ", Type.new(:o, Type.new(:o, t))) |
| 336 348 | |
| 337 349 | @doc """ |
| 338 350 | Constructor for Leibniz equality on the given type, which defines equality by |
| @@ -350,9 +362,11 @@ defmodule ShotDs.Hol.Definitions do | |
| 350 362 | @spec leibniz_equality(Type.t(), :equiv | :imp | :conv_imp) :: Term.term_id() |
| 351 363 | def leibniz_equality(type, connective \\ :equiv) |
| 352 364 | |
| 353 | - def leibniz_equality(%Type{} = type, :equiv), do: mk_leibniz_equality(type, equivalent_term()) |
| 365 | + def leibniz_equality(%Type{} = type, :equiv), |
| 366 | + do: mk_leibniz_equality(type, equivalent_term()) |
| 354 367 | |
| 355 | - def leibniz_equality(%Type{} = type, :imp), do: mk_leibniz_equality(type, implies_term()) |
| 368 | + def leibniz_equality(%Type{} = type, :imp), |
| 369 | + do: mk_leibniz_equality(type, implies_term()) |
| 356 370 | |
| 357 371 | def leibniz_equality(%Type{} = type, :conv_imp), |
| 358 372 | do: mk_leibniz_equality(type, implied_by_term()) |
| @@ -405,7 +419,10 @@ defmodule ShotDs.Hol.Definitions do | |
| 405 419 | |> TF.make_abstr_term(z) |
| 406 420 | |> then(&TF.make_appl_term(pi_term(type), &1)) |
| 407 421 | |
| 408 | - rhs = q_term |> TF.make_appl_term(TF.make_term(x)) |> TF.make_appl_term(TF.make_term(y)) |
| 422 | + rhs = |
| 423 | + q_term |
| 424 | + |> TF.make_appl_term(TF.make_term(x)) |
| 425 | + |> TF.make_appl_term(TF.make_term(y)) |
| 409 426 | |
| 410 427 | implies_term() |
| 411 428 | |> TF.make_appl_term(lhs) |
Loading more files…