Thomas has it right. The behaviour whereby dtcase prints as case is a bug that
I will try to get around to fixing at some point.
Note that this is all with respect to HOL as you check it out from master on
github, not Kananaskis-10.
Michael
On 28/07/2016, 08:54, "Thomas Tuerk" <tho...@tuerk-brechen.de> wrote:
Hi Armaël,
the syntax you use and that is still used in patternMatchesExamples.ML
was the one used before Michaels changes and the recent merge of the
branch you mention.
I'm not too sure myself, how to use the new one and what the new syntax
is exactly. From looking at Michael's commits and the source code, I
figured out the following. So no guarentees.
By default, the old case-expressions are used. However, the standard HOL
image used has the patternMatchesLib loaded and knows about PMATCH. For
example support for it is present in "std_ss". It just cannot parsed
with a nice syntax. It is always possible to use the full verbose syntax.
One can then enable parsing PMATCH expressions with a syntax close to
the existing decision tree matches via
patternMatchesLib.ENABLE_PMATCH_CASES ()
From this point on "case" is used to parse into PMATCH and "dtcase" to
parse into PMATCH. Pretty printing for both produces "case", though, it
seems.
Example
val t1 = ``case x of [] => 0 | _ => 1``
> val t1 =
``case x of [] => 0 | v2::v3 => 1``:
term
val _ = patternMatchesLib.ENABLE_PMATCH_CASES ()
val t2 = ``case x of [] => 0 | _ => 1``
> val t2 =
``case x of [] => 0 | _ => 1``:
term
val t3 = ``dtcase x of [] => 0 | _ => 1``
> val t3 =
``case x of [] => 0 | v2::v3 => 1``:
term
val _ = set_trace "use pmatch_pp" 0
val _ = set_trace "pp_cases" 0
t1
> val it =
``list_CASE x 0 (λv2 v3. 1)``:
term
t2
> val it =
``PMATCH x
[PMATCH_ROW (λ_. []) (λ_. T) (λ_. 0);
PMATCH_ROW (λ_0. _0) (λ_0. T) (λ_0. 1)]``:
term
t3
> val it =
``list_CASE x 0 (λv2 v3. 1)``:
term
For examples on how to use the new syntax I looked at the "selftest.sml"
in the pattern match directory.
Perhaps I have time during the weekend to look into it closer and update
the syntax used by "patternMatchesExamples.ML".
Best
Thomas
(and other docu I fear) is the old one. Michael changed the syntax
On 27/07/16 15:23, Armaël Guéneau wrote:
> Hi all,
>
> I'm trying to use the pattern_matches/ library of HOL4 (that has been
merged
> relatively recently). Basically, I tried running the very first examples
> of the
> example file (src/pattern_matches/patternMatchesExamples.ML), and it
> seems to
> fail to parse the custom syntax for PMATCH:
>
> ``CASE x OF [ |||. (NONE, []) ~> 0 ]``
>
> fails with the following error:
>
> Don't expect to find a > in this position after a ~
> at line 25, character 40 and at line 25, character 39.
> Exception-
> HOL_ERR
> {message =
> "at line 25, character 39:\nDon't expect to find a > in this
> position after a ~\nat line 25, character 40 and at line 25, character
> 39.\n",
> origin_function = "Absyn", origin_structure = "Absyn"} raised
>
>
> Would you have any ideas on how to enable the custom "CASE .. OF [ .. ]"
> syntax?
>
> Cheers,
> Armaël
>
>
------------------------------------------------------------------------------
> What NetFlow Analyzer can do for you? Monitors network bandwidth and
traffic
> patterns at an interface-level. Reveals which users, apps, and protocols
are
> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
> J-Flow, sFlow and other flows. Make informed decisions using capacity
planning
> reports.http://sdm.link/zohodev2dev
> _______________________________________________
> 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 mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
