agda-compute-normalized-maybe-toplevelが正しいタイプを示していますが、まだ `refl`が受け入れられていません。

Question

私は基本的な言語構文のためのきれいな印刷を作成しようとしています。印刷しているものとして正しく解析する必要があります。パーサが今だけのために、空の文字列リテラルとして文字列""を解析することができます

data Syntax : Set where 
    string : List Char -> Syntax 

parse : List Char → Maybe Syntax 
parse ('"' ∷ '"' ∷ _) = just (string []) 
parse _ = nothing 

、それがスタートだ:)

次に、私は私のプリティプリンタがあります：私は、次のを持って

pretty-lit : (s : Syntax) → pretty-printer-for (string l) 
pretty-lit (string []) = char '"' <> char '"', {!!} 
pretty-lit (string (x ∷ xs)) = {!!} 

を

プリティプリンタ - のためのタイプがある：

、依存のpです

pretty-printer-for : (s : Syntax) → Set 
pretty-printer-for s = Σ Doc (λ d → parse (display (render-pretty 80 d)) ≡ just s) 

Doc（ala Wadler's pretty printing）の文字列と、Docを文字列にレンダリングした結果を解析するという証拠は、本当にあなたが始めた構文です。

は今、上記pretty-litの最初の穴は、この目標があります：私は完全にpretty-litをコメントアウトしてagda-compute-normalised-maybe-toplevelを使用する場合は

Goal: parse 
     (display (render-pretty 80 (cat (char '\"') (char '\"')))) 
     ≡ just (string []) 
———————————————————————————————————————————————————————————— 

を、そしてparse (display (render-pretty 80 (cat (char '\"') (char '\"'))))は私が期待するものである、just (string [])に計算します。私は試してみて、その穴の内容としてreflを使用する場合は、私が

parse 
(display (render-pretty (fromNat 80) (char '\"' <> char '\"'))) 
!= just (string []) of type Maybe Syntax 
when checking that the expression refl has type 
parse 
(display (render-pretty (fromNat 80) (char '\"' <> char '\"'))) 
≡ just (string []) 

を取得しかし、私はちょうどチェックして、それらが等しいです！奇妙なことに、上記のような穴のあるpretty-litが範囲内にある場合、agda-computer-normalised-maybe-toplevelは（just (string [])）を計算しませんが、理由はわかりません。

完全な情報源は、https://github.com/ocharles/agda-nixfmt/commit/4df637cce0621b3d9d8a3ee0a104f46523dcc908にあります。私のかわいいプリンタの定義も含まれています。

Answer 1

{AS} on #agdaこれを投稿して問題を発見しました - 私はNON_TERMINATINGと記されていたrender-prettyを持っていました。 Agdaはこの機能が終了しているのを見ることはできませんが、私はそれがわかっています - TERMINATINGプラグマがあったことを気付かなかっただけです:)それですべてが良いです。