The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Nice to hear that Jonathan! 

Thanks again!

Saulo

On Sat, Nov 8, 2014 at 11:37 PM, Jonathan <jonikelee AT gmail.com> wrote:

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