[07:55:20] *** Joins: bluemanblue (~manjaro-g@2605:e000:1520:8b89::a18) [07:55:33] Hey, so I've got an idea and I'm asking for help on identify relevant research that can help inform what I'm trying to do and opinions about its value and potential. [07:55:33] I want to design a grammar to translate from "natural language" mathematics (or alternatively substitute logical formualas, inference rules, typing judgements, operational semantics, etc) texts (presumably latex with interspersed commentary) to code for a theorem prover (agda,coq,..). [07:55:33] Initially I was kind of just imagining how to build a parser for simple programming languages. [07:55:33] I was thinking of doing just a raw lambda calculus, with perhaps two linearizations like de brujn & classical syntax (and further, typed ) just to get my hands dirty. [07:55:36] this is kind of a sketch. comments would be welcome [07:55:38] fun [07:55:40] Lit : (Str/Int) -> Val ; --should this just be something else just to hide the String info (e.g. some kind of invariant variable tracking mechanism)? [07:55:43] Var : Val -> Exp ; --should this just be something else just to hide the String info (e.g. some kind of invariant variable tracking mechanism)? [07:55:48] --Var : (Str/Int) -> Exp ; --should this just be something else just to hide the String info (e.g. some kind of invariant variable tracking mechanism)? [07:55:51] Abstract : Val -> Exp -> Exp ; [07:55:53] --Abstract : Str -> Exp -> Exp ; [07:55:55] Apply : Exp -> Exp -> Exp ; [07:55:57] where your ast would be something like (still not understanding how to use the literals in the context of an application without lambdas [07:56:00] Abstract (Lit "y") (Abstract (Lit "x") (Apply (Var (Lit "x")) (Var (Lit "y")))) [07:56:02] lin [07:56:04] Lit s = s ; [07:56:06] Var v = v ; [07:56:08] Abstract v e = "\" ++ v.s ++ e [07:56:10] App e1 e2 = "(" ++ e1 ++ ")" ++ "(" ++ e2 ++ ")" [07:56:12] Obviously I assume there are better tools for general parsing and linearization of programming languages, but would it be preferable to generate the two ASTs in GF anyways? Like, has there been any hybrid work with BNFC & GF whereby one can execute code from the other in a program? Is there any paper which details the contrast between the two projects? [07:56:19] Is the information in the tutorial still consdiered idiomatic as concerns parsing programming languages? Is there anything like a grammar for a full (or significant subset) programming language available in GF (ex. System T?)? [07:56:22] The hardest questions I can think of off the top of my head are : how to deal with type signatures and function names. (ii) how to do deal with, in haskell, the seperate constructors used in pattern matching (e.g. f :: ... ;f 0 = ... ; f n = ... (n-1) ... ;) as they tell different things about f. [07:56:26] Additionally, I was confusedgoing through the tutorial: [07:56:28] Suppose I want to parse an expression in the Calculator abstract file found in gf/gf-core/gf-book/examples/chapter8 [07:56:31] Calculator> p "( 3 + 4 ) * 230320" [07:56:33] ETimes (EPlus (EInt 3) (EInt 4)) (EInt 230320) [07:56:35] the more compact is never output in linearization [07:56:37] Calculator> l ETimes (EPlus (EInt 3) (EInt 4)) (EInt 230320) [07:56:39] ( 3 + ( 4 ) ) * ( 230320 ) [07:56:41] Why is this, and how can we specify the grammar such that least number of necessary parens are used in linearization? [07:56:46] Also, am back in america, 10 hours behind y'all. so expect 12-24 hours delays in response [09:06:03] *** Quits: bluemanblue (~manjaro-g@2605:e000:1520:8b89::a18) (Ping timeout: 248 seconds) [12:47:31] *** Quits: proteusguy (~proteusgu@cm-58-10-154-77.revip7.asianet.co.th) (Ping timeout: 246 seconds) [12:59:55] *** Joins: proteusguy (~proteusgu@cm-58-10-154-77.revip7.asianet.co.th) [18:06:08] *** Joins: bluemanblue (~manjaro-g@2605:e000:1520:8b89::a18) [18:17:52] *** Quits: bluemanblue (~manjaro-g@2605:e000:1520:8b89::a18) (Remote host closed the connection) [19:04:34] *** Joins: bluemanblue (~manjaro-g@cpe-104-172-252-152.socal.res.rr.com) [20:23:06] *** Joins: drbean_ (~drbean@TC210-63-209-58.static.apol.com.tw) [20:23:54] *** Quits: drbean (~drbean@TC210-63-209-200.static.apol.com.tw) (Read error: Connection reset by peer) [21:00:30] *** Quits: bluemanblue (~manjaro-g@cpe-104-172-252-152.socal.res.rr.com) (Ping timeout: 244 seconds) [22:20:18] *** Joins: bluemanblue (~manjaro-g@2605:e000:1520:8b89::a18)