Implement most of a new Datatype function with nicer syntax.

(Pair-programming with Magnus who wanted it.)  Still need to
implement change to EmitTeX.

doc/next-release.md

@@ -25,6 +25,19 @@ New features:
 
 * The `MAX_SET` function in `pred_setTheory` is now defined (to have value `0`) on the empty set.
 
+* There is an alternative syntax for specifying datatypes.  Instead of the `Hol_datatype` entry-point, one can also use `Datatype`, which takes a slightly different syntax, inspired by Haskell.  This does away with the use of the (somewhat confusing) `of` and `=>` tokens.
+
+  For example, one would define a simple type of binary tree with
+
+          Datatype`tree = Lf num | Node tree tree`
+
+  If the arguments to a constructor are not just simple types, then they need to be enclosed in parentheses.  For example:
+
+          Datatype`mytype = Constr mytype ('a -> bool) | BaseCase
+
+  The `Hol_datatype` entry-point can continue to be used.  The LaTeX output of `EmitTeX` uses the new format.
+
+
 Bugs fixed:
 -----------
 

src/datatype/Datatype.sig

@@ -48,5 +48,6 @@ sig
 
  val astHol_datatype  : AST list -> unit
  val Hol_datatype  : hol_type quotation -> unit
+ val Datatype : hol_type quotation -> unit
 
 end

src/datatype/Datatype.sml

@@ -1313,7 +1313,8 @@ fun astHol_datatype astl =
   HOL_MESG message
  end handle ? as HOL_ERR _ => Raise (wrap_exn "Datatype" "Hol_datatype" ?);
 
-val Hol_datatype = astHol_datatype o ParseDatatype.parse;
+val Hol_datatype = astHol_datatype o ParseDatatype.parse
+val Datatype = astHol_datatype o ParseDatatype.hparse
 
 val _ = Parse.temp_set_grammars ambient_grammars
 

src/parse/ParseDatatype.sig

@@ -22,7 +22,7 @@ sig
 (*---------------------------------------------------------------------------
   Grammar we're parsing is:
 
-      G            ::=  id "=" <form>
+      G            ::=  id "=" <form> (";" id "=" <form>)*
       form         ::=  <phrase> ( "|" <phrase> ) *  |  <record_defn>
       phrase       ::=  id  | id "of" <ptype> ( "=>" <ptype> ) *
       record_defn  ::=  "<|"  <idtype_pairs> "|>"
@@ -34,4 +34,17 @@ sig
   code will still work as long as the input puts the types in parentheses.
  ---------------------------------------------------------------------------*)
 
+val hparse : Type.hol_type Portable.quotation -> AST list
+
+(* The grammar for hparse is:
+
+   G        ::= id "=" <form> (";" id "=" <form>)*
+   form     ::= "|"? <phrase> ( "|" <phrase> )* | <record_defn>
+   phrase   ::= id <typarg>*
+   typarg   ::= atomic-typ | "(" <type> ")"
+
+  where record_defn is as above, and an atomic-typ is either a type variable,
+  or a type-constant of arity 0, or one of the types being defined.
+*)
+
 end

src/parse/ParseDatatype.sml

@@ -22,7 +22,7 @@ struct
 val ERR = Feedback.mk_HOL_ERR "ParseDatatype";
 val ERRloc = Feedback.mk_HOL_ERRloc "ParseDatatype";
 
-open Portable;
+open Portable Lib;
 
 datatype pretype
    = dVartype of string
@@ -170,7 +170,6 @@ in
   recurse [i1]
 end
 
-
 fun parse_record_defn qb = let
   val () = scan "<|" qb
   val result = sepby1 ";" parse_record_fld qb
@@ -192,6 +191,11 @@ in
   | _ => (constr_id, [])
 end
 
+fun optscan tok qb =
+    case qbuf.current qb of
+        (tok',_) => if tok = tok' then (qbuf.advance qb; qb)
+                    else qb
+
 fun parse_form qb =
     case pdtok_of qb of
       (_,base_tokens.BT_Ident "<|",_) => Record (parse_record_defn qb)
@@ -220,6 +224,68 @@ in
                              "Parse failed"
 end
 
+fun parse_harg qb =
+  case qbuf.current qb of
+      (base_tokens.BT_Ident s, _) =>
+      if String.sub(s,0) = #"(" then
+        let
+          val (adv,_,_) = pdtok_of qb
+          val _ = adv()
+        in
+          parse_type qb before scan ")" qb
+        end
+      else let
+        val qb' = qbuf.new_buffer [QUOTE s]
+      in
+        qbuf.advance qb; parse_type qb'
+      end
+    | (base_tokens.BT_AQ ty, _) => dAQ ty
+    | (_, locn) => raise ERRloc "parse_harg" locn
+                         "Unexpected token in constructor's argument"
+
+fun parse_hargs qb =
+  case pdtok_of qb of
+      (_, base_tokens.BT_Ident "|", _) => []
+    | (_, base_tokens.BT_Ident ";", _) => []
+    | (_, base_tokens.BT_EOI, _) => []
+    | _ => let
+      val arg = parse_harg qb
+      val args = parse_hargs qb
+    in
+      arg::args
+    end
+
+fun parse_hphrase qb = let
+  val constr_id = parse_constructor_id qb
+in
+  (constr_id, parse_hargs qb)
+end
+
+fun parse_hform qb =
+    case pdtok_of qb of
+      (_,base_tokens.BT_Ident "<|",_) => Record (parse_record_defn qb)
+    | _ => Constructors (qb |> optscan (base_tokens.BT_Ident "|")
+                            |> sepby1 "|" parse_hphrase)
+
+fun parse_HG qb = let
+  val tyname = ident qb
+  val () = scan "=" qb
+in
+  (tyname, parse_hform qb)
+end
+
+
+fun hparse q = let
+  val strm = qbuf.new_buffer q
+  val result = sepby1 ";" parse_HG strm
+  val qb = optscan (base_tokens.BT_Ident ";") strm
+in
+  case qbuf.current qb of
+      (base_tokens.BT_EOI,_) => result
+    | (_,locn) => raise ERRloc "parse" locn
+                        "Parse failed"
+end
+
 
 
 

src/parse/qbuf.sig

@@ -16,4 +16,3 @@ signature qbuf = sig
   val toString : 'a qbuf -> string
 
 end;
-