[Hol-info] Element assignment in structures
The following data structure is defined in HOL4. val _ = Datatype ` my = <| r: num; b: num; dis: real |>`; Given a mylist(:my list), if a certain condition is met, modify the dist value in my, otherwise the dis value in my will not change. How to define such an operation in HOL4?___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Element assignment in structures
I recommend learning about the syntax of HOL a bit more. Also, as Michael suggested (to you or someone else) maybe write the code up first as an SML program and then translate to HOL. In any case, here are some nonsense definitions that HOL allows. They should help you get further. load "realLib"; val _ = Datatype ` coordinate = <| x_axis: real; y_axis: real; z_axis: real |> `; val _ = Datatype ` chromosome = <| r: num; b: num; distance: real; rx: coordinate; path: coordinate list; bx: coordinate |> `; val ch = ``ch: chromosome``; val pop = ``pop: chromosome list``; val get_def = Define ` get E pop = case E pop of SOME ch => (ch with <| distance := ch.distance + 145 |>) | NONE => (HD pop with <| distance := (HD pop).distance |>)`; val getA_def = Define ` getA pop = case pop of [] => ARB | ch::t => if ch.r < ch.b then (ch with <| distance := ch.distance + 145 |>) else ch`; On Wed, Dec 19, 2018 at 9:09 PM 幻＠未来 <849678...@qq.com> wrote: > The following data types are defined in HOL4. > >val _ = Datatype ` > > coordinate = <| > > x_axis: real; > > y_axis: real; > > z_axis: real > > |> `; > >val _ = Datatype ` > >chromosome = <| > >r: num; > >b: num; > >distance: real; > >rx: coordinate; > >path: coordinate list; > >bx: coordinate > >|> `; > val ch = ``ch: chromosome``; > val pop = ``pop: chromosome list``; > > > Given a pop(:chromosome list), I want to achieve a goal : If if-condition > is met, the distance value of the ch in the pop is assigned to other values, > otherwise the distance value of ch is unchanged. How to solve this problem? > How to define such an operation? > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Element assignment in structures
The following data types are defined in HOL4.val _ = Datatype ` coordinate = <| x_axis: real; y_axis: real; z_axis: real |> `; val _ = Datatype `chromosome = <| r: num;b: num;distance: real; rx: coordinate;path: coordinate list;bx: coordinate |> `; val ch = ``ch: chromosome``; val pop = ``pop: chromosome list``; Given a pop(:chromosome list), I want to achieve a goal : If if-condition is met, the distance value of the ch in the pop is assigned to other values, otherwise the distance value of ch is unchanged. How to solve this problem? How to define such an operation?___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Element assignment in structures
There seems to be some problems with the syntax. For one, the !ch ... on the right hand side of the definition means that the rhs is boolean, which conflicts with the record values being returned by the if-then-else. Konrad. On Wed, Dec 19, 2018 at 8:04 PM 幻＠未来 <849678...@qq.com> wrote: > The following data types are defined in HOL4. > >val _ = Datatype ` > > coordinate = <| > > x_axis: real; > > y_axis: real; > > z_axis: real > > |> `; > >val _ = Datatype ` > >chromosome = <| > >r: num; > >b: num; > >distance: real; > >rx: coordinate; > >path: coordinate list; > >bx: coordinate > >|> `; > val ch = ``ch: chromosome``; > val pop = ``pop: chromosome list``; > val get_def = Define ` > get pop = !ch if (Certain condition) then (ch with <| distance > := ch.distance + max_distance pop |>) >else (ch with <| distance := ch.distance |>)`; > > > Given a pop(:chromosome list), I want to achieve a goal : If if-condition > is met, the distance value of the ch in the pop is assigned to other values, > otherwise the distance value of ch is unchanged. How to solve this problem? > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Element assignment in structures
The following data types are defined in HOL4.val _ = Datatype ` coordinate = <| x_axis: real; y_axis: real; z_axis: real |> `; val _ = Datatype `chromosome = <| r: num;b: num;distance: real; rx: coordinate;path: coordinate list;bx: coordinate |> `; val ch = ``ch: chromosome``; val pop = ``pop: chromosome list``; val get_def = Define ` get pop = !ch if (Certain condition) then (ch with <| distance := ch.distance + max_distance pop |>) else (ch with <| distance := ch.distance |>)`; Given a pop(:chromosome list), I want to achieve a goal : If if-condition is met, the distance value of the ch in the pop is assigned to other values, otherwise the distance value of ch is unchanged. How to solve this problem?___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Element assignment in structures
As written (and with a definition provided for max_distance), your script works fine. Your error message must be for some other problem. From your description, it sounds as if you want to use MAP to alter all ch values in a pop (which is a chromosome list). As it seems very computational, I’d recommend trying to write your algorithm in SML (or Haskell, or OCaml), and then translating it to HOL. Michael From: 幻＠未来 <849678...@qq.com> Date: Thursday, 20 December 2018 at 12:38 To: hol-info Subject: [Hol-info] Element assignment in structures The following data types are defined in HOL4. val _ = Datatype ` coordinate = <| x_axis: real; y_axis: real; z_axis: real |> `; val _ = Datatype ` chromosome = <| r: num; b: num; distance: real; rx: coordinate; path: coordinate list; bx: coordinate |> `; val ch = ``ch: chromosome``; val pop = ``pop: chromosome list``; val get_def = Define ` get pop ch = if MEM ch pop then (ch with <| distance := ch.distance + max_distance pop |>) else (ch with <| distance := ch.distance |>)`; val get1_def = Define ` get1 pop = !ch. if MEM ch pop then (ch.distance = ch.distance + max_distance pop) else ch.distance = ch.distance`; The definition of get_def is successful, but the definition of get1_def is unsuccessful. Defining get1_def will report an error: Exception raised at Preterm.type-analysis: roughly between line 878, character 19 and line 879, character 58: Type inference failure: unable to infer a type for the application of ($! :(α -> bool) -> bool) :(α -> bool) -> bool on line 878, characters 14-17 to λ(ch :chromosome). if MEM ch (pop :chromosome list) then ch with distance := ch.distance + max_distance pop else ch with distance := ch.distance roughly between line 878, character 19 and line 879, character 58 which has type :chromosome -> chromosome unification failure message: Attempt to unify different type operators: min$bool and scratch$chromosome What I want to do is to give a pop(:chromosome list), for any ch(:chromosome) in the pop , if some conditions are met, then the distance value in ch is modified. How to solve this problem? ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Element assignment in structures
The following data types are defined in HOL4. val _ = Datatype ` coordinate = <| x_axis: real; y_axis: real; z_axis: real |> `;val _ = Datatype ` chromosome = <|r: num; b: num;distance: real;rx: coordinate; path: coordinate list;bx: coordinate|> `; val ch = ``ch: chromosome``; val pop = ``pop: chromosome list``; val get_def = Define ` get pop ch = if MEM ch pop then (ch with <| distance := ch.distance + max_distance pop |>) else (ch with <| distance := ch.distance |>)`; val get1_def = Define ` get1 pop = !ch. if MEM ch pop then (ch.distance = ch.distance + max_distance pop) else ch.distance = ch.distance`; The definition of get_def is successful, but the definition of get1_def is unsuccessful. Defining get1_def will report an error: Exception raised at Preterm.type-analysis: roughly between line 878, character 19 and line 879, character 58: Type inference failure: unable to infer a type for the application of ($! :(?? -> bool) -> bool) :(?? -> bool) -> bool on line 878, characters 14-17 to ??(ch :chromosome). if MEM ch (pop :chromosome list) then ch with distance := ch.distance + max_distance pop else ch with distance := ch.distance roughly between line 878, character 19 and line 879, character 58 which has type :chromosome -> chromosome unification failure message: Attempt to unify different type operators: min$bool and scratch$chromosome What I want to do is to give a pop(:chromosome list), for any ch(:chromosome) in the pop , if some conditions are met, then the distance value in ch is modified. How to solve this problem?___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Element assignment in structures
Thank you for your answer. I made the following attempt in HOL4. open realLib; val _ = Datatype ` coordinate = <| x_axis: real; y_axis: real; z_axis: real |> `; val _ = Datatype ` chromosome = <| r: num; b: num; distance: real; rx: coordinate; path: coordinate list; bx: coordinate |> `; ``ch with <| b := 3; distance := 10.6 |> ``; Can I print out the values of b and distance in ch? How can I print? In addition, I made the following definition in HOL4 val robot_judge_def = Define ` robot_judge pop = !ch RB robot. is_robot_object RB /\ MEM ch pop /\ MEM robot RB.robotpoint /\ robot.r < ch.r ==> if MEM robot.point ch.path then (ch with <| distance := ch.distance + 1000 |>) else (ch with <| distance := ch.distance |>) `; First of all, when certain conditions are met, I want to increase the distance value in ch by 1000 based on the original value. Is Term ``ch with <| distance := ch.distance + 1000 |>`` feasible? In addition, this definition is wrong. Is there any way to do what I want to do? QIN___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Element assignment in structures
HOL is not an imperative language, so you can’t “assign” fields of a record. However, you can write things like My_record with <| b := 3; rx := x’; distance := 10.6 |> to denote a chromosome value that is the same as My_record except that fields b, rx and distance have different values. Michael From: 幻＠未来 <849678...@qq.com> Date: Tuesday, 18 December 2018 at 13:57 To: hol-info Subject: [Hol-info] Element assignment in structures Hello! I defined the following data structure in HOL4. Datatype ` chromosome = <| r: num; b: num; distance: real; rx: coordinate; path: coordinate list; bx: coordinate |>`; So, how do you assign values and modify values to elements in a structure? ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Element assignment in structures
Hello! I defined the following data structure in HOL4. Datatype ` chromosome = <| r: num; b: num; distance: real; rx: coordinate; path: coordinate list; bx: coordinate |>`; So, how do you assign values and modify values to elements in a structure?___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
