Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Beginner Question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Beginner Question


Chronological Thread 
  • From: Saulo Araujo <saulo2 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Beginner Question
  • Date: Sat, 8 Nov 2014 22:51:30 -0300

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






Archive powered by MHonArc 2.6.18.

Top of Page