/home/laney/.irssi/irclogs/Freenode/#agda.log-20170404

--- Day changed Mon Apr 03 2017
arjen-jonathanHi all03/04 11:51
arjen-jonathanI'm looking for a mechanized semantics for pattern matching; preferably in a DeBruijn setting.03/04 13:01
arjen-jonathanAnyone have any pointers?03/04 13:02
comietekarjen-jonathan: I would like to see that as well03/04 13:29
{AS}arjen-jonathan: what type of pattern matching?03/04 13:30
{AS}arjen-jonathan: In any case https://github.com/SMLFamily/The-Mechanization-of-Standard-ML03/04 13:31
{AS}Standard ML is fully mechanized including it's pattern matching semantics :)03/04 13:31
comietek{AS}: in what?03/04 13:39
{AS}comietek: Twelf03/04 13:39
comietekin Elf?03/04 13:39
comietekhow does the Elf code relate to any particular implementation?03/04 13:40
{AS}It relates to the formal semantics of Standard ML03/04 13:41
comietekI guess we'd like to see the part of that semantics which relates to pattern-matching first03/04 13:41
{AS}comietek: https://github.com/SMLFamily/The-Mechanization-of-Standard-ML/blob/master/elaborate/pat-elab.elf is the pattern elaboration03/04 13:43
{AS}comietek: https://github.com/SMLFamily/The-Mechanization-of-Standard-ML/blob/master/il/opsem.elf#L88 is the operational semantics of case03/04 13:44
{AS}sorry it starts at https://github.com/SMLFamily/The-Mechanization-of-Standard-ML/blob/master/il/opsem.elf#L8503/04 13:44
comietekcan you actually read any of that? :)03/04 13:45
{AS}https://github.com/SMLFamily/The-Mechanization-of-Standard-ML/blob/master/correct/pat-elab.thm are the theorems that pertain to pattern elaboration03/04 13:45
{AS}comietek: Yes :D03/04 13:45
comietekhow did you get to be that way?03/04 13:45
{AS}I had Twelf in my Semantics course :)03/04 13:46
comietekah03/04 13:46
{AS}basically twelf is a derivation language03/04 13:46
{AS}so you write everything like you would with derivations03/04 13:46
{AS}but it also supports things like HOAS very well03/04 13:47
{AS}It has some checking for totality etc.03/04 13:47
{AS}and some Prolog like search functionality03/04 13:47
{AS}Basically in Twelf when you write03/04 13:48
{AS}bla : K <- ([a] P1) <- P203/04 13:48
{AS}you are really writing a constructor named bla : P2 -> (\lambda a. P1) -> K03/04 13:49
{AS}basically everything is defined relationally03/04 13:49
{AS}then you can use modes to say that some components are output components (i.e., uniquely determined by the input components)03/04 13:50
comietekwriting, as in, defining?03/04 13:51
{AS}yeah03/04 13:51
{AS}comietek: you can see http://twelf.org/w/index.php?title=POPL_Tutorial/Basics_Starter&action=raw&ctype=text/css03/04 13:51
comietekcheers03/04 13:52
{AS}basically you define the formation and introduction forms :)03/04 13:52
{AS}np03/04 13:52
{AS}http://twelf.org/wiki/POPL_Tutorial is the full tutorial03/04 13:52
arjen-jonathancomietek: I also have trouble reading twelf ;-)03/04 13:56
arjen-jonathanThanks {AS} for the references03/04 13:56
{AS}arjen-jonathan: np :)03/04 13:56
arjen-jonathanRe "what types of pattern matching": particularly dependent pattern matchin03/04 13:57
arjen-jonathanEven more particular: pattern matching for defining functions over LF types03/04 14:00
comietekLF types?03/04 14:01
comieteklogical framework?03/04 14:01
arjen-jonathanYes; first-order dep. types03/04 14:05
vorgangIs there a way to evaluate expression-at-point in emacs?03/04 19:22
vorgangright now, the only way I know is to write a main, compile and run03/04 19:23
gallaisvorgang: put it in a hole & use C-c C-n03/04 19:38
vorganggallais: thanks, I see that C-c C-n lets me write an expression in a minibuffer and evaluate. But I don't understand what you mean by "put it in a hole"03/04 20:35
comietekdo you know how to make a hole?03/04 20:38
vorgangnot really no03/04 20:38
comietekreplace "bar" in some "foo = bar" with "?" and c-C c-L03/04 20:38
comietekobserve a yellow area appear03/04 20:39
comietekthat's a hole03/04 20:39
vorgangok but how does that help me evaluate something like "ackermann 4 1"03/04 20:39
comietekit doesn't do more than a mini buffer in this scenario03/04 20:39
comietekbut using holes is indispensable to proper Agda programming03/04 20:39
comietekplace your cursor in the hole and c-C c-,03/04 20:40
comieteknow you see the available hypotheses and he goal you need to prove03/04 20:40
comietekyou can ask Agda to write code for you now03/04 20:40
vorgangok that's theorem proving, I was trying to do some basic eval-ing first03/04 20:41
vorgangI have this... foo : ℕ03/04 20:47
vorgangfoo = (suc { }0)03/04 20:48
vorgangthe "{ }0" is green and I can't modify or delete it... not sure what to do now03/04 20:48
comietekput the cursor in the hole03/04 20:48
comietektype e.g. zero03/04 20:49
comietekc-SPACE03/04 20:49
vorgangyou mean, C-c C-SPACE ?03/04 20:49
comietekyes, sorry03/04 20:49
comietekhttp://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html03/04 20:49
vorgangok, that did it03/04 20:50
vorgangtricky stuff03/04 20:50
comietekthere are many useful commands03/04 20:50
vorgangI reckon I can put ack 4 1 instead of zero: {ack 4 1}0, and fill. Sadly, that doesn't seem to evaluate it...03/04 20:55
gallaisyou can write "{!" on the left and "!}" on the right of an expression to put it in a hole03/04 21:20
gallais(you need to reload the file using "C-c C-l")03/04 21:20
gallaisOnce you have that, to normalize it you have to type "C-c C-n" as I mentioned earlier03/04 21:21
gallaisYou can prefix "C-c C-n" by one or two "C-u" to get different levels of normalisation03/04 21:22
jonsterlingDoes anyone know how to backspace over a hole or otherwise delete it? I've been using agda for years but never learned how to do this correctly.03/04 22:51
mietekjonsterling: depending on the flavour of emacs…03/04 22:51
mietekin Aquamacs, I’ve found that it’s possible to select it if you start selecting at least 1 character out03/04 22:52
mietekalso, c-C c-X c-D, edit, c-C c-L03/04 22:52
jonsterlingAh... I use Emacs for Max or something, and the only way I've found is by selecting it something03/04 22:52
jonsterlingi guess c-c c-x c-d sounds reasonable :) thanks!03/04 22:53
gallaisjonsterling: https://github.com/agda/agda/pull/191703/04 23:56

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!