1structure ParseDatatype_dtype =
2struct
3
4 datatype pretype =
5   dVartype of string
6 | dTyop of {Tyop : string, Thy : string option, Args : pretype list}
7 | dAQ of Type.hol_type
8
9 type field       = string * pretype
10 type constructor = string * pretype list
11
12 datatype datatypeForm =
13   Constructors of constructor list
14 | Record of field list
15
16 type AST = string * datatypeForm
17
18 fun str s = "\"" ^ s ^ "\""
19 fun pr (f1,f2) (a,b) = "(" ^ f1 a ^ "," ^ f2 b ^ ")"
20 fun list_toString ef l = "[" ^ String.concatWith "," (map ef l) ^ "]"
21 fun pt_toString pt =
22   case pt of
23       dVartype s => s
24     | dTyop{Tyop,Thy,Args} =>
25       let
26         val thy = case Thy of NONE => "" | SOME s => s
27       in
28         thy ^ "$" ^ Tyop ^ list_toString pt_toString Args
29       end
30     | dAQ _ => "<AQ-type>"
31 val c_toString = pr (str, list_toString pt_toString)
32 val fld_toString = pr (str, pt_toString)
33 fun dtF_toString dtf =
34   case dtf of
35       Constructors cl => "Constructors" ^ list_toString c_toString cl
36     | Record fl => "Record" ^ list_toString fld_toString fl
37 val toString = pr (str, dtF_toString)
38
39
40end
41