Code for new style pattern-match parsing

Syntax as described in github issue #286 parses.

Examples:

    > ``case x of 0 => 3 | SUC n when n < 10 => n + 1``;
    val it =
       ``PMATCH x
        [PMATCH_ROW (λ_. 0) (K T) (λ_. 3);
         PMATCH_ROW (λn. SUC n) (λn. n < 10) (λn. n + 1)]``:
       term
    > Datatype `tree = Lf | Nd tree 'a tree`;
    <<HOL message: Defined type: "tree">>
    val it = (): unit
    > ``case t of Lf => 0 | Nd t1 x t2 => x + f t1``;
    val it =
       ``PMATCH t
        [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
         PMATCH_ROW (λ(t1,x,t2). Nd t1 x t2) (K T) (λ(t1,x,t2). x + f t1)]``:
       term
    > ``x + case t of Lf => 0 | x .| Nd t1 x t2 => f t1``;
    <<HOL message: inventing new type variable names: 'a>>
    val it =
       ``x +
      PMATCH t
        [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
         PMATCH_ROW (λx. Nd t1 x t2) (K T) (λx. f t1)]``:
       term
    > ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 => f t1``;
    val it =
       ``x +
      PMATCH t
        [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
         PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (K T) (λ(t1,t2). f t1)]``:
       term
    > ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 when g t2 > 6 => f t1``;
    val it =
       ``x +
      PMATCH t
        [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
         PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (λ(t1,t2). g t2 > 6)
           (λ(t1,t2). f t1)]``:
       term

I think we do still need a separate notation to indicate no variables
are to be bound, as

  | .| pat => rhs

won't work when .| is an infix.  Maybe

  | ..| pat => rhs

This would be needed in a situation where all of the variables in pat
have to be read as free (referring to variables occurring in a wider
context).

src/parse/GrammarSpecials.sig

@@ -34,6 +34,7 @@ sig
   val case_split_special : string
   val case_arrow_special : string
   val case_endbinding_special : string
+  val case_when_special : string
 
   val set_case_specials :
       ((Term.term -> Term.term) *

src/parse/GrammarSpecials.sml

@@ -52,6 +52,7 @@ struct
   val case_split_special = "case_split__magic"
   val case_arrow_special = "case_arrow__magic"
   val case_endbinding_special = "case_endbinding__magic"
+  val case_when_special = "case_when__magic"
 
   open HolKernel
   val compilefn = ref (NONE : (term -> term) option)

src/parse/Parse_support.sig

@@ -35,6 +35,13 @@ sig
                               preterm_in_env -> preterm_in_env ->
                               preterm_in_env
 
+  val pm_make_case_arrow    : overload_info -> locn.locn ->
+                              { bvs : Absyn.absyn option,
+                                pat : preterm_in_env,
+                                grd : preterm_in_env option,
+                                rhs : preterm_in_env } ->
+                              preterm_in_env
+
   val binder_restrictions   : unit -> (string * string) list
   val associate_restriction : locn.locn -> string * string -> unit
   val delete_restriction    : locn.locn -> string -> unit

src/parse/Parse_support.sml

@@ -467,6 +467,18 @@ fun make_set_const oinfo l fname s E =
  * will subsequently get bound in the set abstraction.
  *---------------------------------------------------------------------------*)
 
+fun mk_one_vstruct oinfo l (qvs0:(string*pretype)list) =
+  let
+    val qvs =
+        map (fn (bnd as (Name,Ty)) => fn E =>
+                ((fn b => Preterm.Abs{Bvar=Preterm.Var{Name=Name,Ty=Ty,Locn=l},
+                                      Body=b, Locn=l}),
+                 add_scope(bnd,E)))
+            (rev qvs0)
+  in
+    [make_vstruct oinfo l qvs NONE]
+  end
+
 fun make_set_abs oinfo l (tm1,tm2) (E as {scope=scope0,...}:env) = let
   val (_,(e1:env)) = tm1 empty_env
   val (_,(e2:env)) = tm2 empty_env
@@ -481,18 +493,12 @@ in
   case filter (fn (name,_) => mem name fv_names) init_fv of
     [] => raise ERRORloc "make_set_abs" l "no free variables in set abstraction"
   | quants => let
-      val quants' = map
-                      (fn (bnd as (Name,Ty)) =>
-                          fn E =>
-                             ((fn b => Preterm.Abs{Bvar=Preterm.Var{Name=Name,Ty=Ty,Locn=l(*ugh*)},
-                                                   Body=b, Locn=l}),
-                              add_scope(bnd,E)))
-                      (rev quants) (* make_vstruct expects reverse occ. order *)
       fun comma E = (gen_overloaded_const oinfo l ",", E)
     in
       list_make_comb l
                      [(make_set_const oinfo l "make_set_abs" "GSPEC"),
-                      (bind_term l [make_vstruct oinfo l quants' NONE]
+                      (bind_term l
+                                 (mk_one_vstruct oinfo l quants)
                                  (list_make_comb l [comma,tm1,tm2]))] E
     end
 end
@@ -518,6 +524,61 @@ in
                 Locn = loc}, E')
 end
 
+(* ----------------------------------------------------------------------
+    pm_make_case_arrow
+
+    If the bvs are present, the Absyn should be parsed into a var-struct
+    that will bind the remaining components.  If not, then the var-struct
+    should be built by extracting variables from the pat.  If the grd is
+    absent, then it turns into combin$K bool$T (ignoring bvs even if
+    present).
+   ---------------------------------------------------------------------- *)
+
+fun to_vstruct oinfo a =
+  let
+    open Absyn
+  in
+    case a of
+        APP(l, APP(_, IDENT(_, ","), t1), t2) =>
+          make_vstruct oinfo l (map (to_vstruct oinfo) [t1, t2]) NONE
+      | AQ (l,t) => make_aq_binding_occ l t
+      | IDENT(l,s) => make_binding_occ l s
+      | TYPED(l, t, pty) => make_vstruct oinfo l [to_vstruct oinfo t] (SOME pty)
+      | _ => raise ERRORloc "Parse_support" (locn_of_absyn a)
+                   "Bad variable structure"
+  end
+
+val unit_pty = Pretype.Tyop{Thy = "one", Tyop = "one", Args = []}
+
+fun pm_make_case_arrow oinfo loc {bvs,pat:preterm_in_env,grd,rhs} =
+  let
+    val vstruct : bvar_in_env list =
+        case bvs of
+            NONE =>
+            let
+              val (pat_ptm, patE) = pat empty_env
+              val pat_fv_names0 = #free patE
+              val qvs = case pat_fv_names0 of
+                            [] => [("_",unit_pty)]
+                          | vs => vs
+            in
+              mk_one_vstruct oinfo loc qvs
+            end
+          | SOME a => [to_vstruct oinfo a]
+    val guard =
+        case grd of
+            NONE => list_make_comb loc [make_qconst loc ("combin", "K"),
+                                        make_qconst loc ("bool", "T")]
+          | SOME g => bind_term loc vstruct g
+  in
+    list_make_comb loc [make_qconst loc ("patternMatches", "PMATCH_ROW"),
+                        bind_term loc vstruct pat,
+                        guard,
+                        bind_term loc vstruct rhs]
+  end
+
+
+
 
 (*---------------------------------------------------------------------------
  * Sequence abstractions [| tm1 | tm2 |].

src/parse/TermParse.sml

@@ -197,14 +197,15 @@ local open Parse_support Absyn
       | _ => raise ERRORloc "Term" (locn_of_absyn t)
                             "Bad variable-structure"
 in
-  fun absyn_to_preterm_in_env oinfo t = let
+  fun absyn_to_preterm_in_env TmG t = let
+    val oinfo = term_grammar.overload_info TmG
     fun binder(VIDENT (l,s))    = make_binding_occ l s
       | binder(VPAIR(l,v1,v2))  = make_vstruct oinfo l [binder v1, binder v2]
                                                NONE
       | binder(VAQ (l,x))       = make_aq_binding_occ l x
       | binder(VTYPED(l,v,pty)) = make_vstruct oinfo l [binder v] (SOME pty)
     open parse_term Absyn Parse_support
-    val to_ptmInEnv = absyn_to_preterm_in_env oinfo
+    val to_ptmInEnv = absyn_to_preterm_in_env TmG
   in
     case t of
       APP(l,APP(_,IDENT (_,"gspec special"), t1), t2) =>
@@ -216,23 +217,72 @@ in
         to_ptmInEnv (APP(l, QIDENT(l, "pred_set", "GSPEC"),
                          LAM(l, to_vstruct t2, newbody)))
       end
-    | APP(l, APP(_, t0 as IDENT (_, caseform), t1), t2) => let
+    | APP(l, APP(_, t0 as IDENT (_, caseform), t1), t2) =>
+      let
+        fun every_case sing cons base ab =
+          case ab of
+              APP(l, APP(_, t0 as IDENT (_, casesplit), t1), t2) =>
+              let
+              in
+                if casesplit = GrammarSpecials.case_split_special then let
+                  val t1' = base t1
+                  val t2' = every_case sing cons base t2
+                in
+                  list_make_comb l [cons, t1', t2']
+                end
+                else sing (base ab)
+              end
+            | _ => sing (base ab)
       in
-        if caseform = GrammarSpecials.case_special then let
-            (* handle possible arrows in t2 *)
-            fun every_case base ab =
+        if caseform = GrammarSpecials.case_special then
+          if #pmatch_on (term_grammar.specials TmG) then
+            let
+              fun splitrow_opt_kR opn k ab =
                 case ab of
-                  APP(l, APP(_, t0 as IDENT (_, casesplit), t1), t2) => let
-                  in
-                    if casesplit = GrammarSpecials.case_split_special then let
-                        val t1' = every_case base t1
-                        val t2' = every_case base t2
-                      in
-                        list_make_comb l [to_ptmInEnv t0, t1', t2']
-                      end
-                    else base ab
-                  end
-                | _ => base ab
+                    APP(_, APP(_, t0 as IDENT (_, row_opn), t1), t2) =>
+                      if row_opn = opn then (SOME t1, k t2)
+                      else (NONE, k ab)
+                  | _ => (NONE, k ab)
+              fun splitrow_opt_kL opn k ab =
+                case ab of
+                    APP(_, APP(_, IDENT(_, row_opn), t1), t2) =>
+                      if row_opn = opn then (k t1, SOME t2)
+                      else (k ab, NONE)
+                  | _ => (k ab, NONE)
+              fun splitrow_kL opn k ab =
+                case ab of
+                    APP(l, APP(_, IDENT(_, row_opn), t1), t2) =>
+                      if row_opn = opn then (k t1, t2)
+                      else raise ERRORloc "Term" l
+                                 "Mal-formed case expression (no arrow)"
+                  | _ => raise ERRORloc "Term" l
+                               "Mal-formed case expression (no arrow)"
+              fun do_row a =
+                let
+                  open GrammarSpecials
+                  val (bvsopt, ((pat_a, grd_a), rhs_a)) =
+                      splitrow_opt_kR case_endbinding_special
+                                      (splitrow_kL
+                                         case_arrow_special
+                                         (splitrow_opt_kL case_when_special I))
+                                      a
+                in
+                  pm_make_case_arrow
+                    oinfo (locn_of_absyn a)
+                    {bvs = bvsopt, pat = to_ptmInEnv pat_a,
+                     grd = Option.map to_ptmInEnv grd_a,
+                     rhs = to_ptmInEnv rhs_a}
+                end
+              val cons_pt = make_qconst l ("list", "CONS")
+              fun sing pt =
+                list_make_comb l [cons_pt, pt, make_qconst l ("list", "NIL")]
+              val rows = every_case sing cons_pt do_row t2
+              val match_pt = make_qconst l ("patternMatches", "PMATCH")
+            in
+              list_make_comb l [match_pt, to_ptmInEnv t1, rows]
+            end
+          else let
+            (* handle possible arrows in t2 *)
             fun do_arrow ab =
                 case ab of
                   APP(l, APP(_, t0 as IDENT (_, casearrow), t1), t2) => let
@@ -245,9 +295,11 @@ in
                   end
                 | _ => raise ERRORloc "Term" (locn_of_absyn ab)
                                       "Mal-formed case expression (no arrow)"
+            val row_cons =
+                to_ptmInEnv (IDENT(l, GrammarSpecials.case_split_special))
           in
             list_make_comb l [to_ptmInEnv t0, to_ptmInEnv t1,
-                              every_case do_arrow t2]
+                              every_case (fn x => x) row_cons do_arrow t2]
           end
         else if String.isPrefix GrammarSpecials.recfupd_special caseform then
           let
@@ -287,11 +339,8 @@ in
   end
 end;
 
-fun absyn_to_preterm g a = let
-  val oinfo = term_grammar.overload_info g
-in
-  a |> absyn_to_preterm_in_env oinfo |> Parse_support.make_preterm
-end
+fun absyn_to_preterm g a =
+  a |> absyn_to_preterm_in_env g |> Parse_support.make_preterm
 
 fun preterm g tyg q = q |> absyn g tyg |> absyn_to_preterm g
 

src/pattern_matches/patternMatchesScript.sml

@@ -1268,6 +1268,12 @@ val _ = add_rule{pp_elements = [HardSpace 1, TOK ".|", BreakSpace(1,2)],
                  paren_style = OnlyIfNecessary,
                  term_name = GrammarSpecials.case_endbinding_special}
 
-val _ = set_pmatch_use true
+val _ = add_rule{pp_elements = [HardSpace 1, TOK "when", BreakSpace(1,2)],
+                 fixity = Infix(NONASSOC,14),
+                 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
+                 paren_style = OnlyIfNecessary,
+                 term_name = GrammarSpecials.case_when_special}
+
+(* val _ = set_pmatch_use true *)
 
 val _ = export_theory();;

src/pattern_matches/patternMatchesSyntax.sml

@@ -701,7 +701,7 @@ fun pmatch_printer GS backend sys (ppfns:term_pp_types.ppstream_funs) gravs d t
             not (free_in vars guard) andalso
             not (free_in vars rh)) then (
           add_string "|||." >> add_break (1, 0)
-        ) else (          
+        ) else (
           add_string "|||" >>
           add_break (1, 0) >>
           sys (Top, Top, Top) (d - 1) vars >>
@@ -797,7 +797,7 @@ val PMATCH_ROW_magic_3_tm = mk_const("PMATCH_ROW_magic_3",
 val PMATCH_ROW_magic_4_tm = mk_const ("PMATCH_ROW_magic_4",
   ``:'a # bool # 'b -> 'a -> 'b option``);
 
-val _ = temp_add_rule{pp_elements = [TOK "~>"],
+(* val _ = temp_add_rule{pp_elements = [TOK "~>"],
                  fixity = Infix (NONASSOC, 3),
                  block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
                  paren_style = OnlyIfNecessary,
@@ -809,6 +809,7 @@ val _ = temp_add_rule{term_name = "PMATCH_ROW_magic_2",
       paren_style = OnlyIfNecessary,
       block_style = (AroundEachPhrase,
         (PP.INCONSISTENT, 0))};
+*)
 
 val _ = temp_add_rule{term_name = "PMATCH_ROW_magic_1",
       fixity = Binder,