इडिस

Question

में निर्भर रूप से टाइप किया गया प्रिंटफ मैं आईडीरिस को केयेन से एक उदाहरण का अनुवाद करने की कोशिश कर रहा हूं - आश्रित प्रकारpaper के साथ एक भाषा।

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])) 

मैं आदेश के रूप में मैं जल्दी से String पर मिलान पैटर्न के साथ जटिलता में भाग पैटर्न मिलान के साथ की सुविधा के लिए प्रारूप तर्क के लिए List Char उपयोग कर रहा हूँ String के बजाय:

यहाँ मैं अब तक किया है । अगर मैं 3 तत्वों ('%' :: ... अधिक हैं) को PrintfType में और printf के साथ सभी पैटर्न मैच मामलों बाहर टिप्पणी

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 

, तो:

दुर्भाग्य से मैं मैं की समझ बनाने के लिए सक्षम नहीं हूँ एक त्रुटि संदेश मिलता कोड संकलित करता है (लेकिन स्पष्ट रूप से कुछ भी दिलचस्प नहीं करता है)।

मैं अपना कोड कैसे ठीक करूं ताकि printf "the %s is %d" "answer" 42 काम करता है? ।

Answer 1

ऐसा लगता है कि इदरिस में कुछ current limitations जब कार्यों जहां पैटर्न ओवरलैप को परिभाषित कर रहे हैं की तरह (उदाहरण के लिए '%' :: 'd'c :: cs के साथ ओवरलैप हो कई की कोशिश करता के बाद, मैं अंत में बाहर एक समाधान इस के लिए लगा:

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 है प्रारूप स्ट्रिंग का प्रतिनिधित्व करने वाला एक रिकर्सिव डेटा प्रकार FInt एक int प्लेसहोल्डर है, FString एक स्ट्रिंग प्लेसहोल्डर है और FChar एक चार अक्षर है। Format का उपयोग करके मैं PrintfType परिभाषित कर सकता हूं और printFormat लागू कर सकता हूं। वहां से, मैं आसानी से विस्तार कर सकता हूं List Char या Format मान के बजाय एक स्ट्रिंग लें। और अंत परिणाम यह है:

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