The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

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

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