Idris

Question

Bağımlı olarak yazdırılan printf'e,Cayenne - bağımlı türlerine sahip bir dil olan Idris'a bir örnek çevirmeye çalışıyorum.

PrintfType : (List Char) -> Type 
PrintfType Nil    = String 
PrintfType ('%' :: 'd' :: cs) = Int -> PrintfType cs 
PrintfType ('%' :: 's' :: cs) = String -> PrintfType cs 
PrintfType ('%' :: _ :: cs) = PrintfType cs 
PrintfType (_ :: cs)  = PrintfType cs 

printf : (fmt: List Char) -> PrintfType fmt 
printf fmt = rec fmt "" where 
    rec : (f: List Char) -> String -> PrintfType f 
    rec Nil acc = acc 
    rec ('%' :: 'd' :: cs) acc = \i => rec cs (acC++ (show i)) 
    rec ('%' :: 's' :: cs) acc = \s => rec cs (acC++ s) 
    rec ('%' :: _ :: cs) acc = rec cs acc -- this is line 49 
    rec (c :: cs)  acc = rec cs (acC++ (pack [c])) 

hızla desen String üzerinde eşleşen karmaşıklığı içine koşarken desen eşleştirme ile kolaylaştırmak amacıyla ben biçimi argüman için String yerine List Char kullanıyorum: Burada

Ben bugüne kadar ne olduğunu . Ben 3 PrintfType elemanların ( '%' :: ... olanlar) ve printf ile tüm desen maç davaları açıklama o zaman,

Type checking ./sprintf.idr 
sprintf.idr:49:Can't unify PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs 

Specifically: 
    Can't convert PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs 

:

Ne yazık ki ben bir anlam çıkarmaya muktedir değilim bir hata mesajı alıyorum kod derler (ama açıkçası ilginç bir şey yapmaz).

Kodumu printf "the %s is %d" "answer" 42 çalışacak şekilde nasıl düzeltirim? .

Answer 1

desenler örtüşen işlevleri tanımlarken idris bazı current limitations var gibi görünüyor ('%' :: 'd'c :: cs örtüştüğünü örneğin birçok denemeden sonra nihayet bunun için geçici bir çözüm anladım:

data Format = End | FInt Format | FString Format | FChar Char Format 
fromList : List Char -> Format 
fromList Nil    = End 
fromList ('%' :: 'd' :: cs) = FInt (fromList cs) 
fromList ('%' :: 's' :: cs) = FString (fromList cs) 
fromList (c :: cs)   = FChar c (fromList cs) 

PrintfType : Format -> Type 
PrintfType End   = String 
PrintfType (FInt rest) = Int -> PrintfType rest 
PrintfType (FString rest) = String -> PrintfType rest 
PrintfType (FChar c rest) = PrintfType rest 

printf : (fmt: String) -> PrintfType (fromList $ unpack fmt) 
printf fmt = printFormat (fromList $ unpack fmt) where 
    printFormat : (fmt: Format) -> PrintfType fmt 
    printFormat fmt = rec fmt "" where 
    rec : (f: Format) -> String -> PrintfType f 
    rec End acc   = acc 
    rec (FInt rest) acc = \i: Int => rec rest (acC++ (show i)) 
    rec (FString rest) acc = \s: String => rec rest (acC++ s) 
    rec (FChar c rest) acc = rec rest (acC++ (pack [c])) 

Format olduğunu FInt bir int yer tutucudur, FString bir dize yer tutucudur ve FChar bir char literaldir Format Kullanarak PrintfType'u tanımlayabilir ve printFormat'u uygulayabilirim. List Char veya Format değeri yerine bir dize alın. Ve sonuç:

*sprintf> printf "the %s is %d" "answer" 42 
"the answer is 42" : String