src/parse/selftest.sml

74          add_ann_string ("Bound variable", BV (bool, fn () => ": bool")) >>
76          add_ann_string ("Free variable", FV (bool, fn () => ": bool")) >>
85                                          Ty = (Type.bool, fn () => "bool")}) >>
400 val bool = Type.bool
402 val CONS_t = mk_var("CONS", bool --> (bool --> bool))
403 val NIL_t = mk_var("NIL", bool)
418 val mk_list = mk_list0 bool NIL_t CONS_t;
443     Term.prim_new_const {Thy = "min", Name = "CONS"} (bool --> (bool --> bool))
444 val cNIL_t = Term.prim_new_const {Thy = "min", Name = "NIL"} bool
445 val cmk_list = mk_list0 bool cNIL_t cCONS_t
467                        (alpha --> (alpha --> bool) --> (alpha --> bool))
468 val cEMP_t = Term.prim_new_const{Thy = "min", Name = "EMP"} (alpha --> bool)
484 val pbmk_list = mk_list0 bool cEMP_t cINS_t
494 val fx = mk_comb(mk_var("f", alpha --> bool), mk_var("x", alpha))
495 val y = mk_var("y", bool)
496 val bINS = Term.inst[alpha |-> bool] cINS_t
497 val bEMP = Term.inst[alpha |-> bool] cEMP_t
566             (mk_comb(pbmk_list "x", mk_var("y", bool)))
570             (mk_comb(pbmk_list "xy", mk_var("z", bool)))
577 val vbool = dTyop{Tyop = "bool", Thy = SOME "min", Args = []}
619   ("p", "ty = Cons of bool;", expected1),
620   ("h", "ty = Cons bool;", expected1),
621   ("h", "ty = Cons1 bool | Cons2 bool (bool -> bool);", expected2),
622   ("h", "ty = Cons1 bool | Cons2 bool (bool->bool);", expected2),
623   ("p", "ty = Cons1 of bool | Cons2 of bool => bool -> bool;", expected2),
624   ("h", "ty = <| fld1 : bool ; fld2 : bool -> bool |>;", expected3),
625   ("h", "ty = <| fld1 : bool ; fld2 : bool -> bool; |>;", expected3),
626   ("h", "ty= <|fld1:bool;fld2:bool->bool; |>;", expected3),
631   ("h", "ty= <|fld1:bool;fld2:bool->bool; |>;ty2=N|C 'a ty",
634   ("h", "C = foo bool bool; D = bar bool|baz", expected6)
638   ("h", "C = foo bool->bool")
734                                               alpha --> bool))