Commit Graph

808 Commits

Author SHA1 Message Date
Arne Keller
2b69a160a3 MathJax: move elements to start of line 2021-02-04 20:30:11 +01:00
Arne Keller
316d3ff7cf VarStepWithLet latex rendering split into 2 lines 2021-02-04 20:30:11 +01:00
Arne Keller
b72f6d01e3 First inference step just displays result 2021-02-04 20:30:11 +01:00
Moritz Dieing
e57907c251 Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 20:09:35 +01:00
Moritz Dieing
cab1e74490 Add language select 2021-02-04 20:09:28 +01:00
Moritz Dieing
a4659f8386 Extend language files 2021-02-04 20:09:09 +01:00
Johanna Stuber
2ccf09da5f Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 19:36:51 +01:00
Johanna Stuber
ee18a3cba1 Generate steps withLet in every sub-inference of let terms 2021-02-04 19:31:06 +01:00
ucrhh
194cbff28d Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 16:51:07 +01:00
ucrhh
acdc005ed7 limie SVG hacks to proof tree 2021-02-04 16:50:54 +01:00
Johanna Stuber
5c9f916a6c Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 16:50:46 +01:00
Johanna Stuber
49ee20baaa if mgu has no substitution for alpha1, final type is alpha1 2021-02-04 16:50:36 +01:00
ucrhh
bb300e292c implement mgu generation in LatexCreator 2021-02-04 15:31:30 +01:00
Moritz Dieing
886ea78869 Focus inputBar after selecting an example 2021-02-04 13:24:46 +01:00
Moritz Dieing
c10074b4f7 Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 13:21:37 +01:00
Moritz Dieing
dc257e4b32 JavaDoc for new methods in view 2021-02-04 13:21:29 +01:00
Johanna Stuber
ee41f42249 Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 13:16:21 +01:00
Johanna Stuber
a0e3eb34a2 LatexCreator for let and const 2021-02-04 13:16:09 +01:00
Moritz Dieing
b4499c6889 Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 12:58:16 +01:00
Moritz Dieing
8da5bf36a5 Immediately parse backslash to lambda 2021-02-04 12:58:09 +01:00
ucrhh
8885b8a059 implement constraint generation 2021-02-04 12:47:09 +01:00
Johanna Stuber
8dc7fbe725 implement let in TypeInferers 2021-02-04 11:41:08 +01:00
ucrhh
fd00b47928 change substitution sign to another arrow 2021-02-04 10:58:09 +01:00
ucrhh
1564c772d5 Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 10:49:19 +01:00
ucrhh
46dae40e74 implement typeAssumptions in LatexCreator 2021-02-04 10:49:03 +01:00
Johanna Stuber
e4e4fca350 fix compiling errors after changing TypeAbstrarction's quantifiedVariables from list to set 2021-02-04 10:25:19 +01:00
Johanna Stuber
a80d1f9059 Additional TypeAbstraction constructor, for that implement getFreeTypeVariables() on types 2021-02-04 10:17:54 +01:00
Johanna Stuber
c3d5d9147c Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-04 09:27:56 +01:00
Johanna Stuber
29ca293fce better handling of optionals 2021-02-04 09:27:46 +01:00
Arne Keller
84a9a3c5a4 Display premises always, space between premises 2021-02-03 21:43:40 +01:00
Arne Keller
2930a274ed Limit SVG hacks to proof tree and unification 2021-02-03 16:28:35 +01:00
Arne Keller
62d7c9f5e1 Fix parsing of (λx.x)λx.x 2021-02-03 16:09:58 +01:00
Arne Keller
b87e444f0b LatexCreator Unification 2021-02-03 15:45:53 +01:00
ucrhh
3fba4ae1be Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-03 15:27:30 +01:00
ucrhh
e2788a1c81 changed indexing of variables 2021-02-03 15:27:18 +01:00
Arne Keller
b1aa3e05a9 Move LatexCreatorType to own class 2021-02-03 15:22:17 +01:00
Arne Keller
0cb09b92ec Increase size of SVG to 100% 2021-02-03 15:10:51 +01:00
uogau
9e77c422f2 TypeAssumptionParser und ModelImpl angepasst 2021-02-03 13:40:56 +01:00
ucrhh
874b648caf Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-03 11:09:28 +01:00
ucrhh
cc400fc314 set URL when inferring type 2021-02-03 11:09:14 +01:00
Johanna Stuber
c44082693d Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-03 11:08:10 +01:00
Johanna Stuber
d3add97c1e Implement most of Tree::visit(letTerm), for that add EmptyStep 2021-02-03 11:07:50 +01:00
ucrhh
02f10158d6 Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc 2021-02-03 10:40:42 +01:00
ucrhh
70c4f5ce43 read lambda term from url 2021-02-03 10:40:23 +01:00
Johanna Stuber
4bc4b8a14a TypeInfererLet now implementation of TypeInfererInterface 2021-02-03 07:56:48 +01:00
Johanna Stuber
e5d29822f7 Test for TypeInferenceResult::getType(); sort mgu by kind, then index; checkstyle 2021-02-03 07:50:52 +01:00
Arne Keller
afcf8cb252 Enforce Checkstyle 2021-02-02 21:04:34 +01:00
Moritz Dieing
ee52895579 Delete useless screenshot 2021-02-02 20:48:27 +01:00
Moritz Dieing
1b943bbb02 Simple integration tests and structure for screenshot test 2021-02-02 20:42:35 +01:00
Arne Keller
9d4e225d16 Code style fixes 2021-02-02 10:55:46 +01:00