diff --git a/packages/preview/derive-it/0.1.3/LICENSE b/packages/preview/derive-it/0.1.3/LICENSE new file mode 100644 index 000000000..bd536c0b0 --- /dev/null +++ b/packages/preview/derive-it/0.1.3/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2024 0rphee + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/packages/preview/derive-it/0.1.3/README.md b/packages/preview/derive-it/0.1.3/README.md new file mode 100644 index 000000000..65d5b95ba --- /dev/null +++ b/packages/preview/derive-it/0.1.3/README.md @@ -0,0 +1,95 @@ +# derive-it + +A Typst package to create Fitch-style natural deductions. Available on [Typst Universe](https://typst.app/universe/package/derive-it). + + + +## Usage + +This package provides two functions: + +`ded-nat` is a function that expects 2 parameters: +- `stcolor`: the stroke color of the indentation guides. The default is `black`. +- `arr`: an array with the shape, it can be provided in two shapes. + - 4 items: (dependency: text content, indentation: integer starting from 0, formula: text content, rule: text content). + - 3 items: the same as above, but without the dependency. + +`ded-nat-boxed` is a function that expects 4 parameters, and returns the deduction in a `box`: +- `stcolor`: the stroke color of the indentation guides. The default is `black`. +- `premises-and-conclusion`: bool, whether to automatically insert or not the premises and conclusion of the derivation above the lines. The default is `true`. +- `premise-rule-text`: text content, used for finding the premises' formulas when `premises-and-conclusion` is set to `true`. The default is `"PR"`. +- `arr`: an array with the shape, it can be provided in two shapes. + - 4 items: (dependency: text content, indentation: integer starting from 0, formula: text content, rule: text content). + - 3 items: the same as above, but without the dependency. + + +> Note: depending on your layout, this functions may fail to compile due to a high enough amount of indentation (due to the recursive implementation of the layout). +> In my tests, depending on the content of the line, the compiler will panic at around 15-20 indentation levels. +> ```typst +> ("1", 16, $forall y ((Q y a and R y a) -> not Q a y)$, "TEST") +> ``` +>  + + +### Example + +```typ +#import "@preview/derive-it:0.1.3": * + +#ded-nat(stcolor: black, arr:( + ("1", 0, $forall x (P x) and forall x (Q x)$, "PR"), + ("2", 0, $forall x (P x -> R x)$, "PR"), + + ("1", 0, $forall x (P x)$, "S 1"), + ("1", 0, $P a$, "IU 3"), + ("2", 0, $P a -> R a$, "IU 2"), + ("1,2", 0, $R a$, "MP 4, 5"), + + ("1,2", 0, $forall x (R x)$, "GU 6"), +)) + +#ded-nat-boxed(stcolor: black, premises-and-conclusion: false, arr: ( + ("1", 0, $forall x (S x b) and not forall y (P y -> Q b y)$, "PR"), + ("2", 0, $forall x forall y (Q x y -> not Q y x)$, "PR"), + ("3", 1, $not forall x (not P x) -> forall y (S y b -> Q b y)$, "Sup. RAA"), + ("1", 1, $not forall y (P y -> Q b y)$, "S 1"), + ("1", 1, $exists y not (P y -> Q b y)$, "EMC 4"), + ("6", 2, $not (P a -> Q b a)$, "Sup. IE 5"), + ("7", 3, $not (P a and not Q b a)$, "Sup. RAA"), + ("7", 3, $not P a or not not Q b a$, "DM 7"), + ("9", 4, $not P a$, "Sup. PC"), + ("9", 4, $not P a or Q b a$, "Disy. 9"), + ("", 3, $not P a -> (not P a or Q b a)$, "PC 9-10"), + ("12", 4, $not not Q b a$, "Sup. PC"), + ("12", 4, $Q b a$, "DN 12"), + ("12", 4, $not P a or Q b a$, "Disy. 13"), + ("", 3, $not not Q b a -> (not P a or Q b a)$, "PC 12-14"), + ("7", 3, $not P a or Q b a$, "Dil. 8,11,15"), + ("7", 3, $P a -> Q b a$, "IM 16"), + ("6,7", 3, $(P a -> Q b a) and not (P a -> Q b a)$, "Conj. 6, 17"), + ("6", 2, $P a and not Q b a$, "RAA 7-18"), + ("6", 2, $P a$, "S 19"), + ("6", 2, $exists x (P x)$, "GE 20"), + ("6", 2, $not forall x (not P x)$, "EMC 21"), + ("3,6", 2, $forall y (S y b -> Q b y)$, "MP 3, 22"), + ("3,6", 2, $S a b -> Q b a$, "IU 23"), + ("1", 2, $forall x (S x b)$, "S 1"), + ("1", 2, $S a b$, "IU 25"), + ("1,3,6", 2, $Q b a$, "MP 24, 25"), + ("6", 2, $not Q b a$, "S 19"), + ("1,3,6", 2, $Q b a or not exists y not (P y -> Q b y)$, "Disy. 27"), + ("1,3,6", 2, $not exists y not (P y -> Q b y)$, "MTP 28, 29"), + ("1,3", 1, $not exists y not (P y -> Q b y)$, "IE 5, 6, 30"), + ("1,3", 1, $not exists y not (P y -> Q b y) and exists y not (P y -> Q b y)$, "Conj. 5, 31"), + + ("1", 0, $not (not forall x (not P x) -> forall y ( S y b -> Q b y))$, "RAA 3-32"), +)) +``` + +# Development + +In order to compile locally `examples/example.typ` the command is: + +```sh +typst compile examples/example.typ -root . +``` diff --git a/packages/preview/derive-it/0.1.3/examples/example.png b/packages/preview/derive-it/0.1.3/examples/example.png new file mode 100644 index 000000000..cc0e5619c Binary files /dev/null and b/packages/preview/derive-it/0.1.3/examples/example.png differ diff --git a/packages/preview/derive-it/0.1.3/examples/example.typ b/packages/preview/derive-it/0.1.3/examples/example.typ new file mode 100644 index 000000000..412e8964b --- /dev/null +++ b/packages/preview/derive-it/0.1.3/examples/example.typ @@ -0,0 +1,333 @@ +#import "../lib.typ": * + +#set text(lang: "es") + +#let then = $arrow$ +#let bithen = $arrow.l.r$ +#let eqt = $eq.triple$ +#let ex = $exists$ + +#let hi(content) = { + text(content, weight: "bold", fill: gradient.linear(red, blue)) +} + += Deducción natural +Elegir 10 ejercicios del libro de Falguera y Vidal, de las páginas 318, 319, 320 y 321; y hacer su prueba con deducción natural. + ++ pg. 318, ejercicios VI, I. 1) + + This is written using `ded-nat-boxed`. The coloring of the text is done by wrapping that function with `text(content, weight: "bold", fill: gradient.linear(red, blue))`, and the color of the box stroke is done with `stcolor: gradient.linear(red, blue)`. + + #hi[ + #ded-nat-boxed(stcolor: gradient.linear(red, blue), arr:( + ("1", 0, $forall x (P x) and forall x (Q x)$, "PR"), + ("2", 0, $forall x (P x -> R x)$, "PR"), + + ("1", 0, $forall x (P x)$, "S 1"), + ("1", 0, $P a$, "IU 3"), + ("2", 0, $P a -> R a$, "IU 2"), + ("1,2", 0, $R a$, "MP 4, 5"), + + ("1,2", 0, $forall x (R x)$, "GU 6"), + )) + ] + + This is using `ded-nat`, and it is a repetition of the last one but without the boxing and without dependencies (inputting an array of 3 items). + + #ded-nat(stcolor: black, arr: ( + (0, $forall x (P x) and forall x (Q x)$, "PR"), + (0, $forall x (P x -> R x)$, "PR"), + + (0, $forall x (P x)$, "S 1"), + (0, $P a$, "IU 3"), + (0, $P a -> R a$, "IU 2"), + (0, $R a$, "MP 4, 5"), + (0, $forall x (R x)$, "GU 6"), + )) + + This is using `ded-nat-boxed`, without dependencies (inputting an array of 3 items) and without the premises and conclusion of the deduction automatically put over the lines. + + #ded-nat-boxed(stcolor: black, premises-and-conclusion: false, arr: ( + (0, $forall x (P x) and forall x (Q x)$, "PR"), + (0, $forall x (P x -> R x)$, "PR"), + + (0, $forall x (P x)$, "S 1"), + (0, $P a$, "IU 3"), + (0, $P a -> R a$, "IU 2"), + (0, $R a$, "MP 4, 5"), + (0, $forall x (R x)$, "GU 6"), + )) + ++ pg. 321, ejercicios VI, I. 62) + + #ded-nat-boxed(stcolor: black, arr: ( + ("1", 0, $forall x (S x b) and not forall y (P y -> Q b y)$, "PR"), + ("2", 0, $forall x forall y (Q x y -> not Q y x)$, "PR"), + + ("3", 1, $not forall x (not P x) -> forall y (S y b -> Q b y)$, "Sup. RAA"), + ("1", 1, $not forall y (P y -> Q b y)$, "S 1"), + ("1", 1, $exists y not (P y -> Q b y)$, "EMC 4"), + ("6", 2, $not (P a -> Q b a)$, "Sup. IE 5"), + ("7", 3, $not (P a and not Q b a)$, "Sup. RAA"), + ("7", 3, $not P a or not not Q b a$, "DM 7"), + ("9", 4, $not P a$, "Sup. PC"), + ("9", 4, $not P a or Q b a$, "Disy. 9"), + ("", 3, $not P a -> (not P a or Q b a)$, "PC 9-10"), + ("12", 4, $not not Q b a$, "Sup. PC"), + ("12", 4, $Q b a$, "DN 12"), + ("12", 4, $not P a or Q b a$, "Disy. 13"), + ("", 3, $not not Q b a -> (not P a or Q b a)$, "PC 12-14"), + ("7", 3, $not P a or Q b a$, "Dil. 8,11,15"), + ("7", 3, $P a -> Q b a$, "IM 16"), + ("6,7", 3, $(P a -> Q b a) and not (P a -> Q b a)$, "Conj. 6, 17"), + ("6", 2, $P a and not Q b a$, "RAA 7-18"), + ("6", 2, $P a$, "S 19"), + ("6", 2, $exists x (P x)$, "GE 20"), + ("6", 2, $not forall x (not P x)$, "EMC 21"), + ("3,6", 2, $forall y (S y b -> Q b y)$, "MP 3, 22"), + ("3,6", 2, $S a b -> Q b a$, "IU 23"), + ("1", 2, $forall x (S x b)$, "S 1"), + ("1", 2, $S a b$, "IU 25"), + ("1,3,6", 2, $Q b a$, "MP 24, 25"), + ("6", 2, $not Q b a$, "S 19"), + ("1,3,6", 2, $Q b a or not exists y not (P y -> Q b y)$, "Disy. 27"), + ("1,3,6", 2, $not exists y not (P y -> Q b y)$, "MTP 28, 29"), + ("1,3", 1, $not exists y not (P y -> Q b y)$, "IE 5, 6, 30"), + ("1,3", 1, $not exists y not (P y -> Q b y) and exists y not (P y -> Q b y)$, "Conj. 5, 31"), + + ("1", 0, $not (not forall x (not P x) -> forall y ( S y b -> Q b y))$, "RAA 3-32"), + )) + + ++ pg. 320, ejercicios VI, I. 51) + + #hi[ + #box( + stroke: gradient.linear(red, blue), inset: 8pt, radius: 8pt, + )[ + #align(center)[ + $ + not (M a b -> (S a and S b)), \ + not (not exists x Q x or forall x not R a b x) \ + tack forall x ((S a and S b) -> (R a b x -> not Q x)) + $ + + #ded-nat(stcolor: gradient.linear(red,blue), arr: ( + ("1", 0, $not (M a b -> (S a and S b))$, "PR"), + ("2", 0, $not (not exists x Q x or forall x not R a b x)$, "PR"), + + ("3", 1, $not (M a b and not (S a and S b))$, "Sup. RAA"), + ("3", 1, $not M a b or not not (S a and S b)$, "DM 3"), + ("5", 2, $not M a b$, "Sup. PC"), + ("5", 2, $not M a b or (S a and S b)$, "Adj. 5"), + ("5", 2, $M a b -> (S a and S b)$, "IM 6"), + ("", 1, $not M a b -> (M a b -> (S a and S b))$, "PC 5-7"), + ("9", 2, $not not (S a and S b)$, "Sup. PC"), + ("9", 2, $S a and S b$, "DN 9"), + ("9", 2, $not M a b or (S a and S b)$, "Adj. 10"), + ("9", 2, $M a b -> (S a and S b)$, "IM 11"), + ("", 1, $not not (S a and S b) -> (M a b -> (S a and S b))$, "PC 9-12"), + ("3", 1, $M a b -> (S a and S b)$, "Dil. 4, 8, 13"), + ("1,3", 1, $not(M a b -> (S a and S b)) and (M a b -> (S a and S b))$, "Conj. 1, 14"), + ("1", 0, $M a b and not (S a and S b)$, "RAA 3-15"), + ("17", 1, $S and S b$, "Sup. PC"), + ("17", 1, $(S and S b) or (R a b c -> not Q c)$, "Adj. 17"), + ("1", 1, $not (S and S b)$, "S 16"), + ("1,17", 1, $R a b c -> not Q c$, "MTP 18, 19"), + ("1", 0, $(S a and S b) -> (R a b c -> not Q c)$, "PC 17-20"), + + ("1", 0, $forall x ((S a and S b) -> (R a b x -> not Q x))$, "GU 21"), + )) + ] + ] + ] + +#pagebreak() +4. pg. 320, ejercicios VI, I. 41) + + #ded-nat-boxed(stcolor: black, arr: ( + ("1", 0, $forall x forall y ((Q y x and R y x) -> not Q x y)$, "PR"), + ("2", 0, $Q a b and P b$, "PR"), + + ("3", 1, $R b a$, "Sup. PC"), + ("1", 1, $forall y ((Q y a and R y a) -> not Q a y)$, "IU 1"), + ("1", 1, $(Q b a and R b a) -> not Q a b$, "IU 4"), + ("2", 1, $Q a b$, "S 2"), + ("2", 1, $not not Q a b$, "DN 6"), + ("1,2", 1, $not (Q b a and R b a)$, "MT 5, 7"), + ("1,2", 1, $not Q b a or not R b a$, "DM 8"), + ("3", 1, $not not R b a$, "DN 3"), + ("1,2,3", 1, $not Q b a$, "MTP 9, 10"), + ("2", 1, $P b$, "S 2"), + ("1,2,3", 1, $not Q b a and P b$, "Conj. 11, 12"), + ("1,2,3", 1, $exists x (not Q b x and P b)$, "GE 13"), + + ("1,2", 0, $R b a -> exists x (not Q b x and P b)$, "PC 3-14"), + )) + +#pagebreak() +5. pg. 319, ejercicios VI, I. 30) + + #hi[ + #box( + stroke: gradient.linear(red, blue), inset: 8pt, radius: 8pt, + )[ + #align(center)[ + $ + not ex x ex y (not T x y and not T y x), \ + forall x (T x a -> (Q a and R a)), \ + not forall x (T a x) \ + tack exists x (Q x and R x) + $ + + #ded-nat(stcolor: gradient.linear(red,blue), arr: ( + ("1", 0, $not ex x ex y ( not T x y and not T y x)$, "PR"), + ("2", 0, $forall x (T x a -> (Q a and R a))$, "PR"), + ("3", 0, $not forall x (T a x)$, "PR"), + + ("3", 0, $ex x not(T a x)$, "EMC 3"), + ("5", 1, $not T a b$, "Sup. IE 4"), + ("1", 1, $forall x not ex y (not T x y and not T y x)$, "EMC 1"), + ("1", 1, $not ex y (not T b y and not T y b)$, "IU 6"), + ("1", 1, $forall y not (not T b y and not T y b)$, "EMC 7"), + ("1", 1, $not (not T b a and not T a b)$, "IU 8"), + ("1", 1, $not not T b a or not not T a b)$, "DM 9"), + ("5", 1, $not not not T a b$, "DN 5"), + ("1,5", 1, $not not T b a$, "MTP 10, 11"), + ("1,5", 1, $T b a$, "DN 12"), + ("2", 1, $T b a -> (Q a and R a)$, "IU 2"), + ("1,2,5", 1, $Q a and R a$, "MP 13, 14"), + ("1,2,5", 1, $ex x (Q x and R x)$, "GE 15"), + + ("1,2,3", 0, $ex x (Q x and R x)$, "IE 4, 5, 16"), + )) + ] + ] + ] + + ++ pg. 319, ejercicios VI, I. 20) + + #hi[ + #box( + stroke: gradient.linear(red, blue), inset: 8pt, radius: 8pt, + )[ + #align(center)[ + $ + not ex x (S x) or (Q a and T a), \ + ex x (Q x and T x) -> forall x (R x), \ + S a \ + tack R b + $ + + #ded-nat(stcolor: gradient.linear(red,blue), arr: ( + ("1", 0, $not ex x (S x) or (Q a and T a)$, "PR"), + ("2", 0, $ex x (Q x and T x) -> forall x (R x)$, "PR"), + ("3", 0, $S a$, "PR"), + + ("3", 0, $ex x (S x)$, "GE 3"), + ("3", 0, $not not ex x (S x)$, "DN 4"), + ("1,3", 0, $Q a and T a$, "MTP 1, 5"), + ("1,3", 0, $ex x (Q x and T x)$, "GE 6"), + ("1,2,3", 0, $forall x (R x)$, "MP 2, 7"), + + ("1,2,3", 0, $R b$, "IU 8"), + )) + ] + ] + ] + ++ pg. 318, ejercicios VI, I. 10) + + #hi[ + #box( + stroke: gradient.linear(red, blue), inset: 8pt, radius: 8pt, + )[ + #align(center)[ + $ + forall x (T x -> Q x), \ + forall x not (P x or not T x) \ + tack + ex x ( not P x and Q x) + $ + + #ded-nat(stcolor: gradient.linear(red,blue), arr: ( + ("1", 0, $forall x (T x -> Q x)$, "PR"), + ("2", 0, $forall x not (P x or not T x)$, "PR"), + + ("2", 0, $not (P a or not T a)$, "IU 2"), + ("2", 0, $not P a and not not T a$, "DM 3"), + ("2", 0, $not not T a$, "S 4"), + ("2", 0, $T a$, "DN 5"), + ("1", 0, $T a -> Q a$, "IU 1"), + ("1,2", 0, $Q a$, "MP 6, 7"), + ("2", 0, $not P a$, "S 4"), + ("1,2", 0, $not P a and Q a$, "Conj. 8, 9"), + + ("1,2", 0, $ex x ( not P x and Q x)$, "GE 10"), + )) + ] + ] + ] + +#pagebreak() +8. pg. 318, ejercicios VI, I. 5) + + #hi[ + #ded-nat-boxed(stcolor: gradient.linear(red, blue), arr: ( + ("1", 0, $forall x (P x) -> forall x (Q x)$, "PR"), + ("2", 0, $not Q a$, "PR"), + + ("2", 0, $ex x not (Q x)$, "GE 2"), + ("2", 0, $not forall x (Q x)$, "EMC 3"), + + ("1,2", 0, $not forall x (P x)$, "MT 1, 4"), + )) + ] + ++ pg. 318, ejercicios VI, I. 6) + + #hi[ + #ded-nat-boxed(stcolor: gradient.linear(red, blue), arr: ( + ("1", 0, $forall x (P x -> Q x)$, "PR"), + ("2", 0, $forall x ( not S x -> not Q x)$, "PR"), + ("3", 0, $not forall x (S x)$, "PR"), + + ("3", 0, $ex x not (S x)$, "EMC 3"), + ("5", 1, $not S a$, "Sup. IE 4"), + ("2", 1, $not S a -> not Q a$, "IU 2"), + ("2,5", 1, $not Q a$, "MP 5, 6"), + ("1", 1, $P a -> Q a$, "IU 1"), + ("1,2,5", 1, $not P a$, "MT 7, 8"), + ("1,2,5", 1, $ex x (not P x)$, "GE 9"), + + ("1,2,3", 0, $ex x (not P x)$, "IE 4, 5, 10"), + )) + ] + +#pagebreak() +10. pg. 318, ejercicios VI, I. 7) + + #ded-nat-boxed(stcolor: black, arr: ( + ("1", 0, $forall x (T x -> M x)$, "PR"), + ("2", 0, $forall x not (M x and R x)$, "PR"), + ("3", 0, $forall x ( T x -> (P x -> R x))$, "PR"), + + ("4", 1, $T a$, "Sup. PC"), + ("1", 1, $T a -> M a$, "IU 1"), + ("1,4", 1, $M a$, "MP 4,5"), + ("2", 1, $not (M a and R a)$, "IU 2"), + ("2", 1, $not M a or not R a$, "DM 7"), + ("1,4", 1, $not not M a$, "DN 6"), + ("1,2,4", 1, $not R a$, "MTP 8, 9"), + ("3", 1, $T a -> (P a -> R a)$, "IU 3"), + ("3,4", 1, $P a -> R a$, "MP 4, 11"), + ("1,2,3,4", 1, $not P a$, "MT 10, 12"), + ("14", 2, $M a -> P a$, "Sup. RAA"), + ("1,4,14", 2, $P a$, "MP 6, 14"), + ("1,2,3,4,14", 2, $P a and not P a$, "Conj. 13, 15"), + ("1,2,3,4", 1, $not (M a -> P a)$, "RAA 14-16"), + ("1,2,3", 0, $T a -> not ( M a -> P a)$, "PC 4-17"), + + ("1,2,3", 0, $forall x ( T x -> not (M x -> P x))$, "GU 18"), + )) diff --git a/packages/preview/derive-it/0.1.3/examples/indentation-test.png b/packages/preview/derive-it/0.1.3/examples/indentation-test.png new file mode 100644 index 000000000..9d429b94c Binary files /dev/null and b/packages/preview/derive-it/0.1.3/examples/indentation-test.png differ diff --git a/packages/preview/derive-it/0.1.3/lib.typ b/packages/preview/derive-it/0.1.3/lib.typ new file mode 100644 index 000000000..dfdf954de --- /dev/null +++ b/packages/preview/derive-it/0.1.3/lib.typ @@ -0,0 +1,193 @@ +/* + +`ded-nat` is a function that expects 2 parameters: +- `stcolor`: the stroke color of the indentation guides. Default is `black`. +- `arr`: an array with the shape, it can be provided in two shapes. + - 4 items: (dependency: text content, indentation: integer starting from 0, formula: text content, rule: text content). + - 3 items: the same as above, but without the dependency. + +*/ + + +// internal function that stringifies a line array (of a natural deduction table) +// this may be removed at any time +#let derive-it-internal-stringify-line(line-arr) = { + let to-string(cntnt) = { + if type(cntnt) != content { + str(cntnt) + } else if cntnt.has("text") { + cntnt.text + } else if cntnt.has("children") { + cntnt.children.map(to-string).join("") + } else if cntnt.has("body") { + to-string(cntnt.body) + } else if cntnt == [ ] { + " " + } + } + + if type(line-arr) == str or type(line-arr) == int or type(line-arr) == float { + str(line-arr) + } else if type(line-arr) == array{ + line-arr.map(to-string).intersperse(", ").sum() + } else { + repr(line-arr) + } +} + +// internal function to validate that each line given by the user is correct, with a descriptive error otherwise +// this may be removed at any time +#let derive-it-internal-validate-line(line, line-num, line-size: none) = { + let line-text = "[At line: " + str(line-num+1) + "]: " + let stringified = "'" + derive-it-internal-stringify-line(line) + "'" + let ty = type(line) + if ty != array { + panic(line-text + "Line is a '" + ty + "' instead of an array of 3 or 4 elements: " + stringified) + } else { + // if the linesize is not the provided in the arguments or its not 3 or 4 + if (line-size != none) and (line.len() != line-size){ + panic(line-text + "Line (array) has an incorrect number of elements: " + str(line.len()) + ". It should have " + str(line-size) + ": " + stringified) + } else if line-size == none and (line.len() != 3 and line.len() != 4) { + panic(line-text + "Line (array) has an incorrect number of elements: " + str(line.len()) + ". It should have 3 or 4 elements: "+ stringified) + } + + let ruleVal = line.last() + if type(ruleVal) != str and type(ruleVal) != content { + panic(line-text + "Line (array) should receive a 'string' or 'content' as the rule, instead it received '" + type(ruleVal) + "': " + stringified) + } + + let indentVal = if line.len() == 3 { + line.at(0) + } else { + line.at(1) + } + if type(indentVal) != int { + panic( line-text + "Line (array) should receive an 'integer' as the indentation, instead it received '" + type(indentVal) + "': " + stringified) + } + } +} + + +#let ded-nat(stcolor: black, arr: array) = context { + let strart = ( top: 0em, right: 0em, bottom: 0em,left: 1pt + stcolor ) + let strend = ( top: 0em, right: 0em, bottom: 1pt + stcolor, left: 1pt + stcolor ) + + // check if the first line's array has 4 items (w/dependencies) or not + let (hasDependencies, lineSize) = if arr.at(0).len() == 4 {(true, 4)} else {(false, 3)} + + let maxDepWidth = if hasDependencies { + arr.fold(0pt, (accum, it) => { + let sz = measure[#it.at(0)].width + if sz > accum {sz} else {accum} + } ) + } else { + 0pt + } + + let maxWidth = 0pt + let tupArr = () + + for (i, line) in arr.enumerate(start: 0) { + if i == 0 { + derive-it-internal-validate-line(line, i+1) + } + + let (dep, indent, formula, rule) = if hasDependencies { + line + } else { + ("", line.at(0), line.at(1), line.at(2)) + } + + + let isLastIndented = (arr.len() > i+1) and ({ + let ix = if hasDependencies {1} else {0} + let next-line = arr.at(i+1) + derive-it-internal-validate-line(next-line, i+1, line-size: lineSize) + next-line.at(ix) + } < indent) + + let bl = formula + + for i in range(0, indent){ + let inset = if i != 0 {0pt} else {0pt} + + let str = if i == 0 and isLastIndented { + strend + } else{ strart } + + if indent > 0 and i < indent - 1{ + inset = -5pt + } + + bl = [#h(1em) #box(inset: inset)[#rect(stroke: str)[#bl]]] + } + let index = box(width: 1.5em,)[#(i+1).] + + let tmpWidth = 0pt + let dependency = "" + if hasDependencies { + dependency = text(style: "italic", weight: "regular", box(width: maxDepWidth + 1em)[#dep]) + tmpWidth = measure[#dependency #index #bl].width + } else { + tmpWidth = measure[#index #bl].width + } + + if tmpWidth > maxWidth { + maxWidth = tmpWidth + } + + let ins = if indent == 0 {(x: 0pt, y: 0.5em)} else {(x: 0pt, y: 0pt)} + let numInset = if indent == 0 {(x: 0pt, y: 0.0pt)} else {(x: 0pt, y: 5pt)} + + let line = "" + if hasDependencies { + line = box(inset: ins)[#box(inset: numInset)[#dependency #index] #bl] + } else { + line = box(inset: ins)[#box(inset: numInset)[#index] #bl] + } + + rule = box(baseline: -0.5em , rule) + tupArr.push((line, rule)) + } + tupArr = tupArr.map(a => [#box(width: maxWidth + 0em, a.at(0)) #h(1em) #a.at(1)]) + + text(weight: "bold", + block( + align(start, + stack(dir: ttb, spacing: 0em, ..tupArr) + ) + ) + ) +} + +/* + +`ded-nat-boxed` is a function that expects 4 parameters, and returns the deduction in a `box`: +- `stcolor`: the stroke color of the indentation guides. Default is `black`. +- `premises-and-conclusion`: bool, whether to automatically insert or not the premises and conclusion of the derivation above the lines. Default is `true`. +- `premise-rule-text`: text content, used for finding the premises' formulas when `premises-and-conclusion` is set to `true`. Default is `"PR"`. +- `arr`: an array with the shape, it can be provided in two shapes. + - 4 items: (dependency: text content, indentation: integer starting from 0, formula: text content, rule: text content). + - 3 items: the same as above, but without the dependency. + +*/ +#let ded-nat-boxed(stcolor: black, premises-and-conclusion: true, premise-rule-text: "PR", arr: array) ={ + let premConcText = "" + if premises-and-conclusion { + let premises = arr.filter( x => x.last() == premise-rule-text).map(x => x.at(2)) + let conclusion = arr.last().at(2) + let joinedPremises = [#premises.join([$, $ \ ] )] + premConcText = [ $\ #joinedPremises \ tack #conclusion$ ] + } + + box( + stroke: stcolor, inset: 8pt, radius: 8pt + )[ + #align(center)[ + #if premises-and-conclusion { + premConcText + } #ded-nat(stcolor: stcolor, arr: arr) + ] + ] +} + diff --git a/packages/preview/derive-it/0.1.3/typst.toml b/packages/preview/derive-it/0.1.3/typst.toml new file mode 100644 index 000000000..986509795 --- /dev/null +++ b/packages/preview/derive-it/0.1.3/typst.toml @@ -0,0 +1,12 @@ +[package] +name = "derive-it" +version = "0.1.3" +entrypoint = "lib.typ" +authors = ["0rphee <@0rphee>"] +license = "MIT" +description = "Simple functions for creating fitch-style natural deduction proofs and derivations." +repository = "https://github.com/0rphee/derive-it" +keywords = ["math", "logic", "fitch", "proof", "derivation", "natural deduction", "deduction"] +categories = ["layout", "visualization"] +disciplines = ["mathematics", "philosophy"] +exclude = ["examples/", "*.pdf"]