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