4 use"Scripts/term_G.sml"; |
4 use"Scripts/term_G.sml"; |
5 use"term_G.sml"; |
5 use"term_G.sml"; |
6 *) |
6 *) |
7 |
7 |
8 (* |
8 (* |
9 > (Thm.cterm thy) a_term; |
9 > (cterm_of thy) a_term; |
10 val it = "empty" : cterm *) |
10 val it = "empty" : cterm *) |
11 |
11 |
12 (*2003 fun match thy t pat = |
12 (*2003 fun match thy t pat = |
13 (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))) |
13 (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))) |
14 handle _ => []; |
14 handle _ => []; |
259 | list2isalist T (t::ts) = (list_const T) $ t $ (list2isalist T ts); |
259 | list2isalist T (t::ts) = (list_const T) $ t $ (list2isalist T ts); |
260 (* |
260 (* |
261 > val tt = (term_of o the o (parse thy)) "R=(R::real)"; |
261 > val tt = (term_of o the o (parse thy)) "R=(R::real)"; |
262 > val TT = type_of tt; |
262 > val TT = type_of tt; |
263 > val ss = list2isalist TT [tt,tt,tt]; |
263 > val ss = list2isalist TT [tt,tt,tt]; |
264 > (Thm.cterm thy) ss; |
264 > (cterm_of thy) ss; |
265 val it = "[R = R, R = R, R = R]" : cterm *) |
265 val it = "[R = R, R = R, R = R]" : cterm *) |
266 |
266 |
267 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b) |
267 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b) |
268 | isapair2pair t = |
268 | isapair2pair t = |
269 raise error ("isapair2pair called with "^term2str t); |
269 raise error ("isapair2pair called with "^term2str t); |
572 Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $ |
572 Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $ |
573 (Const (op_, T --> T) $ term_of_num T root); |
573 (Const (op_, T --> T) $ term_of_num T root); |
574 (* |
574 (* |
575 val T = (type_of o term_of o the) (parse thy "#12::real"); |
575 val T = (type_of o term_of o the) (parse thy "#12::real"); |
576 val t = mk_factroot "SqRoot.sqrt" T 2 3; |
576 val t = mk_factroot "SqRoot.sqrt" T 2 3; |
577 (Thm.cterm thy) t; |
577 (cterm_of thy) t; |
578 val it = "#2 * sqrt #3 " : cterm |
578 val it = "#2 * sqrt #3 " : cterm |
579 *) |
579 *) |
580 fun var_op_num v op_ optype ntyp n = |
580 fun var_op_num v op_ optype ntyp n = |
581 Const (op_, optype) $ v $ |
581 Const (op_, optype) $ v $ |
582 Free (str_of_int n, ntyp); |
582 Free (str_of_int n, ntyp); |
589 Const (op_,Top) $ |
589 Const (op_,Top) $ |
590 Free (str_of_int n1, T1) $ Free (str_of_int n2, T2); |
590 Free (str_of_int n1, T1) $ Free (str_of_int n2, T2); |
591 (* |
591 (* |
592 > val t = num_op_num "Int" 3 4; |
592 > val t = num_op_num "Int" 3 4; |
593 > atomty t; |
593 > atomty t; |
594 > string_of_cterm ((Thm.cterm thy) t); |
594 > string_of_cterm ((cterm_of thy) t); |
595 *) |
595 *) |
596 |
596 |
597 fun const_in str (Const _) = false |
597 fun const_in str (Const _) = false |
598 | const_in str (Free (s,_)) = if strip_thy s = str then true else false |
598 | const_in str (Free (s,_)) = if strip_thy s = str then true else false |
599 | const_in str (Bound _) = false |
599 | const_in str (Bound _) = false |
766 |
766 |
767 val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; |
767 val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; |
768 atomty t; (* 'a *) |
768 atomty t; (* 'a *) |
769 val t' = set_types al t; |
769 val t' = set_types al t; |
770 atomty t'; (*real*) |
770 atomty t'; (*real*) |
771 (Thm.cterm thy) t'; |
771 (cterm_of thy) t'; |
772 val it = "x = #0 + #-1 * #-4" : cterm |
772 val it = "x = #0 + #-1 * #-4" : cterm |
773 |
773 |
774 val t = (term_of o the o (parse thy)) |
774 val t = (term_of o the o (parse thy)) |
775 "#5 * x + x ^^^ #2 = (#2 + x) ^^^ #2"; |
775 "#5 * x + x ^^^ #2 = (#2 + x) ^^^ #2"; |
776 atomty t; |
776 atomty t; |
777 val t' = set_types al t; |
777 val t' = set_types al t; |
778 atomty t'; |
778 atomty t'; |
779 (Thm.cterm thy) t'; |
779 (cterm_of thy) t'; |
780 uncaught exception TYPE (*^^^ is new, NOT in al*) |
780 uncaught exception TYPE (*^^^ is new, NOT in al*) |
781 *) |
781 *) |
782 |
782 |
783 |
783 |
784 (** from Descript.ML **) |
784 (** from Descript.ML **) |
1108 |
1108 |
1109 > val str = "R"; |
1109 > val str = "R"; |
1110 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
1110 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
1111 val t = Free ("R","?DUMMY") : term |
1111 val t = Free ("R","?DUMMY") : term |
1112 > val t' = typ_a2real t; |
1112 > val t' = typ_a2real t; |
1113 > (Thm.cterm thy) t'; |
1113 > (cterm_of thy) t'; |
1114 val it = "R::RealDef.real" : cterm |
1114 val it = "R::RealDef.real" : cterm |
1115 |
1115 |
1116 > val str = "R=R"; |
1116 > val str = "R=R"; |
1117 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
1117 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
1118 > atomty (typ_a2real t); |
1118 > atomty (typ_a2real t); |
1119 *** ------------- |
1119 *** ------------- |
1120 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1120 *** Const ( op =, [RealDef.real, RealDef.real] => bool) |
1121 *** Free ( R, RealDef.real) |
1121 *** Free ( R, RealDef.real) |
1122 *** Free ( R, RealDef.real) |
1122 *** Free ( R, RealDef.real) |
1123 > val t' = typ_a2real t; |
1123 > val t' = typ_a2real t; |
1124 > (Thm.cterm thy) t'; |
1124 > (cterm_of thy) t'; |
1125 val it = "(R::RealDef.real) = R" : cterm |
1125 val it = "(R::RealDef.real) = R" : cterm |
1126 |
1126 |
1127 > val str = "fixed_values [R=R]"; |
1127 > val str = "fixed_values [R=R]"; |
1128 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
1128 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[])))); |
1129 > val t' = typ_a2real t; |
1129 > val t' = typ_a2real t; |
1130 > (Thm.cterm thy) t'; |
1130 > (cterm_of thy) t'; |
1131 val it = "fixed_values [(R::RealDef.real) = R]" : cterm |
1131 val it = "fixed_values [(R::RealDef.real) = R]" : cterm |
1132 *) |
1132 *) |
1133 |
1133 |
1134 (*TODO.WN0609: parse should return a term or a string |
1134 (*TODO.WN0609: parse should return a term or a string |
1135 (or even more comprehensive datastructure for error-messages) |
1135 (or even more comprehensive datastructure for error-messages) |