From 257c93f6b3eb29209a6ae87e8836a7cfc7a870a6 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Thu, 17 Oct 2024 20:14:57 -0300 Subject: [PATCH] match syntax sugar (emulates Agda's with) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Consider Agda programs that match on intermediate values: main : ∀(P : Bool -> Set) -> (F : Bool -> Bool) -> (x : Bool) -> P (F x) main P F x with F x main P F x | True = {!!} -- GOAL: P True main P F x | False = {!!} -- GOAL: P False Previously, to emulate it on Kind, we needed to use an explicit 'Bool/match' function, and annotate both the type of the matched argument, and the return type. Now, we can use 'match' instead: use Base/Pair/ as P/ use Base/Bool/ as B/ Main : ∀(P: ∀(x: B/Bool) *) ∀(F: ∀(x: B/Bool) B/Bool) ∀(x: B/Bool) (P (F x)) = λP λF λx match (F x) { #True: ?a // GOAL: (P #True{}) #False: ?b // GOAL: (P #False{}) } This will correctly specialize the goal to the concrete values. Note that, to do so, we need an ugly "search-and-replace" type level computation. Seems like that is how it is done in Agda too. I don't think this is healthy and I believe it can be extremely slow, so, I'd recommend avoiding 'match', but that's not really practical (we need it even to project pairs, maybes, etc.). See this log to understand: https://gist.github.com/VictorTaelin/48eed41a8eca3500721c06dfec72d48c NOTE: (match x {...}) merely desugars to: (λ{...} x) which is now treated by the type checker (previously it would complain of not enough annotations) --- src/Kind/Check.hs | 8 +++ src/Kind/Equal.hs | 164 ++++++++++++++++++++++++++++++++++++++++++++- src/Kind/Parse.hs | 23 ++++++- src/Kind/Reduce.hs | 35 ---------- 4 files changed, 193 insertions(+), 37 deletions(-) diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index 972fa0985..10972632a 100644 --- a/src/Kind/Check.hs +++ b/src/Kind/Check.hs @@ -129,6 +129,14 @@ infer term dep = debug ("infer: " ++ termShower False term dep) $ go term dep wh check :: Maybe Cod -> Term -> Term -> Int -> Env () check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n :: " ++ termShower True typ dep) $ go src val typ dep where + + -- Case-Of: `(λ{...} x)`. NOTE: this is probably very slow due to 'replace' + go src (App (Src _ val) arg) typx dep = go src (App val arg) typx dep + go src (App (Mat cse) arg) typx dep = do + arg_ty <- infer arg dep + infer (App (Ann True (Mat cse) (All "x" arg_ty (\x -> replace arg x typx dep))) arg) dep + return () + go src (Lam nam bod) typx dep = do book <- envGetBook fill <- envGetFill diff --git a/src/Kind/Equal.hs b/src/Kind/Equal.hs index 6bd1a4ecf..f319db4e2 100644 --- a/src/Kind/Equal.hs +++ b/src/Kind/Equal.hs @@ -12,7 +12,6 @@ import Kind.Show import qualified Data.Map.Strict as M import qualified Data.IntMap.Strict as IM - -- Equality -- -------- @@ -311,3 +310,166 @@ occur book fill uid term dep = go term dep where let o_typ = go typ dep o_bod = goTele (bod (Var nam dep)) (dep + 1) in o_typ || o_bod + +-- Substitution +-- ------------ + +-- This is the ugly / slow part of Kind. See: https://gist.github.com/VictorTaelin/48eed41a8eca3500721c06dfec72d48c + +-- Behaves like 'identical', except it is pure and returns a Bool. +same :: Term -> Term -> Int -> Bool +same (All aNam aInp aBod) (All bNam bInp bBod) dep = + let sInp = same aInp bInp dep + sBod = same (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1) + in sInp && sBod +same (Lam aNam aBod) (Lam bNam bBod) dep = + let sBod = same (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1) + in sBod +same (App aFun aArg) (App bFun bArg) dep = + let sFun = same aFun bFun dep + sArg = same aArg bArg dep + in sFun && sArg +same (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep = + let sTyp = same aTyp bTyp dep + in sTyp +same (Ins aVal) b dep = + same aVal b dep +same a (Ins bVal) dep = + same a bVal dep +same (Dat aScp aCts) (Dat bScp bCts) dep = + let sSlf = and $ zipWith (\ax bx -> same ax bx dep) aScp bScp + sCts = length aCts == length bCts && and (zipWith (\ a b -> sameCtr a b dep) aCts bCts) + in sSlf && sCts +same (Con aNam aArg) (Con bNam bArg) dep = + let sNam = aNam == bNam + sArg = length aArg == length bArg && and (zipWith (\(_, aVal) (_, bVal) -> same aVal bVal dep) aArg bArg) + in sNam && sArg +same (Mat aCse) (Mat bCse) dep = + let sCse = length aCse == length bCse && and (zipWith (\ a b -> sameCse a b dep) aCse bCse) + in sCse +same (Let aNam aVal aBod) b dep = + same (aBod aVal) b dep +same a (Let bNam bVal bBod) dep = + same a (bBod bVal) dep +same (Use aNam aVal aBod) b dep = + same (aBod aVal) b dep +same a (Use bNam bVal bBod) dep = + same a (bBod bVal) dep +same Set Set dep = + True +same (Ann chk aVal aTyp) b dep = + same aVal b dep +same a (Ann chk bVal bTyp) dep = + same a bVal dep +same (Met aUid aSpn) b dep = + False +same a (Met bUid bSpn) dep = + False +same (Hol aNam aCtx) b dep = + True +same a (Hol bNam bCtx) dep = + True +same U32 U32 dep = + True +same (Num aVal) (Num bVal) dep = + aVal == bVal +same (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep = + same aFst bFst dep && same aSnd bSnd dep +same (Swi aZer aSuc) (Swi bZer bSuc) dep = + same aZer bZer dep && same aSuc bSuc dep +same (Txt aTxt) (Txt bTxt) dep = + aTxt == bTxt +same (Nat aVal) (Nat bVal) dep = + aVal == bVal +same (Src aSrc aVal) b dep = + same aVal b dep +same a (Src bSrc bVal) dep = + same a bVal dep +same (Ref aNam) (Ref bNam) dep = + aNam == bNam +same (Var aNam aIdx) (Var bNam bIdx) dep = + aIdx == bIdx +same _ _ _ = False + +-- Auxiliary functions +sameCtr :: Ctr -> Ctr -> Int -> Bool +sameCtr (Ctr aCNm aTele) (Ctr bCNm bTele) dep = + if aCNm == bCNm + then goTele aTele bTele dep + else False + +sameCse :: (String, Term) -> (String, Term) -> Int -> Bool +sameCse (aCNam, aCBod) (bCNam, bCBod) dep = + if aCNam == bCNam + then same aCBod bCBod dep + else False + +goTele :: Tele -> Tele -> Int -> Bool +goTele (TRet aTerm) (TRet bTerm) dep = same aTerm bTerm dep +goTele (TExt aNam aTyp aBod) (TExt bNam bTyp bBod) dep = + let sTyp = same aTyp bTyp dep + sBod = goTele (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1) + in sTyp && sBod +goTele _ _ _ = False + +-- Substitutes a Bruijn level variable by a neo value in term. +subst :: Int -> Term -> Term -> Term +subst lvl neo term = go term where + go (All nam inp bod) = All nam (go inp) (\x -> go (bod x)) + go (Lam nam bod) = Lam nam (\x -> go (bod x)) + go (App fun arg) = App (go fun) (go arg) + go (Ann chk val typ) = Ann chk (go val) (go typ) + go (Slf nam typ bod) = Slf nam (go typ) (\x -> go (bod x)) + go (Ins val) = Ins (go val) + go (Dat scp cts) = Dat (map go scp) (map goCtr cts) + go (Con nam arg) = Con nam (map (\(f, t) -> (f, go t)) arg) + go (Mat cse) = Mat (map goCse cse) + go (Swi zer suc) = Swi (go zer) (go suc) + go (Ref nam) = Ref nam + go (Let nam val bod) = Let nam (go val) (\x -> go (bod x)) + go (Use nam val bod) = Use nam (go val) (\x -> go (bod x)) + go (Met uid spn) = Met uid (map go spn) + go (Hol nam ctx) = Hol nam (map go ctx) + go Set = Set + go U32 = U32 + go (Num n) = Num n + go (Op2 opr fst snd) = Op2 opr (go fst) (go snd) + go (Txt txt) = Txt txt + go (Nat val) = Nat val + go (Var nam idx) = if lvl == idx then neo else Var nam idx + go (Src src val) = Src src (go val) + goCtr (Ctr nm tele) = Ctr nm (goTele tele) + goCse (cnam, cbod) = (cnam, go cbod) + goTele (TRet term) = TRet (go term) + goTele (TExt k t b) = TExt k (go t) (\x -> goTele (b x)) + +-- Replaces a term by another +replace :: Term -> Term -> Term -> Int -> Term +replace old neo term dep = if same old term dep then neo else go term where + go (All nam inp bod) = All nam (replace old neo inp dep) (\x -> replace old neo (bod x) (dep+1)) + go (Lam nam bod) = Lam nam (\x -> replace old neo (bod x) (dep+1)) + go (App fun arg) = App (replace old neo fun dep) (replace old neo arg dep) + go (Ann chk val typ) = Ann chk (replace old neo val dep) (replace old neo typ dep) + go (Slf nam typ bod) = Slf nam (replace old neo typ dep) (\x -> replace old neo (bod x) (dep+1)) + go (Ins val) = Ins (replace old neo val dep) + go (Dat scp cts) = Dat (map (\x -> replace old neo x (dep+1)) scp) (map goCtr cts) + go (Con nam arg) = Con nam (map (\(f, t) -> (f, replace old neo t dep)) arg) + go (Mat cse) = Mat (map goCse cse) + go (Swi zer suc) = Swi (replace old neo zer dep) (replace old neo suc dep) + go (Ref nam) = Ref nam + go (Let nam val bod) = Let nam (replace old neo val dep) (\x -> replace old neo (bod x) (dep+1)) + go (Use nam val bod) = Use nam (replace old neo val dep) (\x -> replace old neo (bod x) (dep+1)) + go (Met uid spn) = Met uid (map (\x -> replace old neo x (dep+1)) spn) + go (Hol nam ctx) = Hol nam (map (\x -> replace old neo x (dep+1)) ctx) + go Set = Set + go U32 = U32 + go (Num n) = Num n + go (Op2 opr fst snd) = Op2 opr (replace old neo fst dep) (replace old neo snd dep) + go (Txt txt) = Txt txt + go (Nat val) = Nat val + go (Var nam idx) = Var nam idx + go (Src src val) = Src src (replace old neo val dep) + goCtr (Ctr nm tele) = Ctr nm (goTele tele dep) + goCse (cnam, cbod) = (cnam, replace old neo cbod dep) + goTele (TRet term) d = TRet (replace old neo term d) + goTele (TExt k t b) d = TExt k (replace old neo t d) (\x -> goTele (b x) (d+1)) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index 407d4bcea..3d51d5444 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -134,7 +134,8 @@ parseTerm = (do , parseCon , parseUse , parseLet - , parseDo + , parseDo -- sugar + , parseMatch -- sugar , parseSet , parseNum , parseTxt @@ -481,3 +482,23 @@ desugarDo (DoBlck name stmts wrap ret) = do parseDo :: Parser Term parseDo = parseDoSugar >>= desugarDo + +-- Let's now implement the 'parseMatch' sugar. The following syntax: +-- 'match x { #Foo: foo #Bar: bar ... }' +-- desugars to: +-- '(λ{ #Foo: foo #Bar: bar ... } x) +-- it parses the cases identically to parseMat. +parseMatch :: Parser Term +parseMatch = withSrc $ do + P.try $ string "match " + x <- parseTerm + char '{' + parseTrivia + cse <- P.many $ do + char '#' + cnam <- parseName + char ':' + cbod <- parseTerm + return (cnam, cbod) + char '}' + return $ App (Mat cse) x diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index bd14da48c..685b98da8 100644 --- a/src/Kind/Reduce.hs +++ b/src/Kind/Reduce.hs @@ -306,38 +306,3 @@ genMetas term = fst (go term 0) where let (typ', c1) = go typ c (bod', c2) = goTele (bod (Var nam 0)) c1 in (TExt nam typ' (\_ -> bod'), c2) - - --- Substitution --- ------------ - --- Substitutes a Bruijn level variable by a neo value in term. -subst :: Int -> Term -> Term -> Term -subst lvl neo term = go term where - go (All nam inp bod) = All nam (go inp) (\x -> go (bod x)) - go (Lam nam bod) = Lam nam (\x -> go (bod x)) - go (App fun arg) = App (go fun) (go arg) - go (Ann chk val typ) = Ann chk (go val) (go typ) - go (Slf nam typ bod) = Slf nam (go typ) (\x -> go (bod x)) - go (Ins val) = Ins (go val) - go (Dat scp cts) = Dat (map go scp) (map goCtr cts) - go (Con nam arg) = Con nam (map (\(f, t) -> (f, go t)) arg) - go (Mat cse) = Mat (map goCse cse) - go (Swi zer suc) = Swi (go zer) (go suc) - go (Ref nam) = Ref nam - go (Let nam val bod) = Let nam (go val) (\x -> go (bod x)) - go (Use nam val bod) = Use nam (go val) (\x -> go (bod x)) - go (Met uid spn) = Met uid (map go spn) - go (Hol nam ctx) = Hol nam (map go ctx) - go Set = Set - go U32 = U32 - go (Num n) = Num n - go (Op2 opr fst snd) = Op2 opr (go fst) (go snd) - go (Txt txt) = Txt txt - go (Nat val) = Nat val - go (Var nam idx) = if lvl == idx then neo else Var nam idx - go (Src src val) = Src src (go val) - goCtr (Ctr nm tele) = Ctr nm (goTele tele) - goCse (cnam, cbod) = (cnam, go cbod) - goTele (TRet term) = TRet (go term) - goTele (TExt nam typ bod) = TExt nam (go typ) (\x -> goTele (bod x))