The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/08/2014 08:51 PM, Saulo Araujo wrote:
> Hi Jonathan,
>
> I am sending the whole file but, since changing from Some value to Some v
> did the tricky, don't bother trying to understand what is happening unless
> you are curious ;)

This file is accepted by the trunk version of Coq I'm using without any 
complaints.  So, whatever was causing that mysterious error was 
eventually fixed.

-- Jonathan

> Require Import String.
> Open Scope string_scope.
>
> Require Import List.
> Import ListNotations.
>
> Definition compareStrings x y :=
>    if string_dec x y then true else false.
>
> Inductive CLASS : Type :=
>    Class : string -> list (string * string) -> CLASS.
>
> Definition getClass classes id :=
>    List.find
>    (fun class => let 'Class id' _ := class in compareStrings id' id)
>    classes.
>
> Inductive OBJECT : Type :=
>    Object : string -> string -> list (string * list string) -> OBJECT.
>
> Definition getObject objects id :=
>    List.find
>    (fun object => let 'Object id' _ _ := object in compareStrings id' id)
>    objects.
>
> Definition getAttribute attributes name :=
>    List.find
>    (fun attribute : string * list string =>
>       let (name', _) := attribute in compareStrings name' name)
>    attributes.
>
> Definition getValue object name :=
>    let 'Object _ _ attributes := object in
>      match getAttribute attributes name with
>        | Some attribute => let (_, value) := attribute in Some value
>        | None => None
>      end.
>
> Fixpoint getValues objects name :=
>    match objects with
>      | object :: objects' =>
>        match getValue object name with
>          | Some value =>
>              match getValues objects' name with
>                | Some value' => Some (List.app value value')
>                | None => None
>              end
>          | None => None
>        end
>      | [] => Some []
>    end.
>
> Thanks again!
> Saulo
>
> On Sat, Nov 8, 2014 at 9:34 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>
> > On 11/08/2014 06:52 PM, Saulo Araujo wrote:
> >
> > > One more doubt. In the code below, the Coq compiler complains about the
> > > lines with Some value. It says "The constructor Some expects 1 argument.".
> > > When I change from Some value to Some v everything works fine. Is there
> > > something special about "Some value"?
> > >
> > > Fixpoint getValues objects name :=
> > >     match objects with
> > >       | object :: objects' =>
> > >         match getValue object name with
> > >           | Some value =>
> > >               match getValues objects' name with
> > >                 | Some value' => Some (List.app value value')
> > >                 | None => None
> > >               end
> > >           | None => None
> > >         end
> > >       | [] => Some []
> > >     end.
> > I would have to see the whole file prior to that definition to tell you
> > what is going wrong.  The use of "value" in a binding position, such as in
> > that match statement, shouldn't be a problem - but it might be the case
> > that Coq isn't inferring the types the way you expect, depending on what
> > comes before getValues.
> >
> > -- Jonathan