[plt-scheme] Typechecking command-line

On Tue, Apr 7, 2009 at 6:03 PM, Sam TH <samth at ccs.neu.edu> wrote:
> You are missing the parentheses around `filename'.  It should be
>
> #:args (#{filename : String})
>
> I'm not yet sure how to give a better error message here.
>

Sorry, guess I missed that! Thanks for the help.

> sam th
>
> On Tue, Apr 7, 2009 at 1:51 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>> On Fri, Apr 3, 2009 at 11:05 PM, Sam TH <samth at ccs.neu.edu> wrote:
>>> On Tue, Mar 17, 2009 at 8:44 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>>>> Hi,
>>>>
>>>> Trying to typecheck a file containing a call to command line fails.
>>>> Here's a short version exemplifying the issue:
>>>
>>> This works now, provided that you annotate the binding instance of
>>> `filename' with an appropriate type:
>>>
>>> #:args #{filename : String}
>>> --
>>> sam th
>>> samth at ccs.neu.edu
>>>
>>
>> Hi Sam,
>>
>> From SVN 14441 using this doesn't work:
>> #lang typed-scheme
>>
>> (require scheme/cmdline)
>>
>> ;; Command Line Arguments Parsing
>> (: verbose-mode (Parameter Boolean))
>> (define verbose-mode (make-parameter #t))
>>
>> (: optimize-level (Parameter Integer))
>> (define optimize-level (make-parameter 0))
>>
>> (: model-checking-mode (Parameter Symbol))
>> (define model-checking-mode (make-parameter 'sat))
>>
>> (: file-to-model-check String)
>> (define file-to-model-check
>>  (command-line
>>   #:program "eboc" ;; Should be name of executable
>>   #:once-each
>>   [("-v" "--verbose") "Compile with verbose messages"
>>                       (verbose-mode #t)]
>>   [("-m" "--mode") #{mode : String}  "Mode to run the model checker
>> on (sat, satbin)"
>>                    (model-checking-mode (string->symbol mode))]
>>   #:once-any
>>   [("-o" "--optimize-1") "Compile with optimization level 1"
>>                          (optimize-level 1)]
>>   ["--optimize-2"        (; show help on separate lines
>>                           "Compile with optimization level 2,"
>>                           "which includes all of level 1")
>>                          (optimize-level 2)]
>>   #:args #{filename : String} ; expect one command-line argument: <filename>
>>   ; return the argument as a filename to compile
>>   filename))
>>
>> I get:
>> typecheck: Polymorphic function parse-command-line could not be
>> applied to arguments:
>> Domain: (U String Path) (U (Vectorof String) (Listof String)) (Listof
>> (Pair (U 'once-each 'once-any 'multi 'final 'help-labels) (Listof
>> (Listof Any)))) (Any a ... a -> b) (Listof String)
>> Arguments: String (Vectorof String) (List (List 'once-each (List (List
>> String String) (Any -> Void) (Listof (List String))) (List (List
>> String String) (Any String -> Void) (Listof (U String (List
>> String))))) (List 'once-any (List (List String String) (Any -> Void)
>> (Listof (List String))) (List (List String) (Any -> Void) (Listof
>> (List String String))))) (Any String* -> (Listof String)) (List
>> String)
>> Result type: b
>> Expected result: String
>>  in: (define file-to-model-check (command-line #:program "eboc"
>> #:once-each (("-v" "--verbose") "Compile with verbose messages"
>> (verbose-mode #t)) (("-m" "--mode") mode "Mode to run the model
>> checker on (sat, satbin)" (model-checking-mode (string->symbol mode)))
>> #:once-any (("-o" "--optimize-1") "Compile with optimization level 1"
>> (optimize-level 1)) ("--optimize-2" ("Compile with optimization level
>> 2," "which includes all of level 1") (optimize-level 2)) #:args
>> filename filename))
>>
>> Am I missing something?
>>
>> --
>> Paulo Jorge Matos - pocmatos at gmail.com
>> Webpage: http://www.personal.soton.ac.uk/pocm
>>
>
>
>
> --
> sam th
> samth at ccs.neu.edu
>



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm