1.1 --- a/src/Tools/isac/ProgLang/termC.sml Fri Oct 01 10:23:38 2010 +0200
1.2 +++ b/src/Tools/isac/ProgLang/termC.sml Fri Oct 01 16:23:03 2010 +0200
1.3 @@ -980,13 +980,18 @@
1.4 in Substitute [(v_1 BOUND_1 = (rhs o hd) s_1 BOUND_0)] h_ BOUND_4
1.5 *)
1.6
1.7 -
1.8 +(* for parse and parse_patt: fix all types to real *)
1.9 fun T_a2real (Type (s, [])) =
1.10 - if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
1.11 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT
1.12 + else Type (s, [])
1.13 | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
1.14 | T_a2real (TFree (s, srt)) =
1.15 - if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)
1.16 - | T_a2real (TVar (("DUMMY",_),srt)) = HOLogic.realT;
1.17 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT
1.18 + else TFree (s, srt)
1.19 + | T_a2real (TVar ((s, i), srt)) =
1.20 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT
1.21 + else TVar ((s, i), srt)
1.22 + | T_a2real (TVar (("DUMMY",_), srt)) = HOLogic.realT;
1.23
1.24 (*FIXME .. fixes the type (+see Typefix.thy*)
1.25 fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T))
1.26 @@ -995,81 +1000,9 @@
1.27 | typ_a2real (Bound i) = (Bound i)
1.28 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
1.29 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
1.30 -(*
1.31 -----------------6.8.02---------------------------------------------------
1.32 - val str = "1";
1.33 - val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
1.34 - atomty (term_of t);
1.35 -*** -------------
1.36 -*** Const ( 1, 'a)
1.37 - val t = (app_num_tr' o term_of) t;
1.38 - atomty t;
1.39 -*** -------------
1.40 -*** Const ( 1, 'a)
1.41 - val t = typ_a2real t;
1.42 - atomty t;
1.43 -*** -------------
1.44 -*** Const ( 1, real)
1.45
1.46 - val str = "2";
1.47 - val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
1.48 - atomty (term_of t);
1.49 -*** -------------
1.50 -*** Const ( Numeral.number_of, bin => 'a)
1.51 -*** . Const ( Numeral.bin.Bit, [bin, bool] => bin)
1.52 -*** . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
1.53 -*** . . . Const ( Numeral.bin.Pls, bin)
1.54 -*** . . . Const ( True, bool)
1.55 -*** . . Const ( False, bool)
1.56 - val t = (app_num_tr' o term_of) t;
1.57 - atomty t;
1.58 -*** -------------
1.59 -*** Free ( 2, 'a)
1.60 - val t = typ_a2real t;
1.61 - atomty t;
1.62 -*** -------------
1.63 -*** Free ( 2, real)
1.64 -----------------6.8.02---------------------------------------------------
1.65
1.66 -
1.67 -> val str = "R";
1.68 -> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
1.69 -val t = Free ("R","?DUMMY") : term
1.70 -> val t' = typ_a2real t;
1.71 -> (cterm_of thy) t';
1.72 -val it = "R::RealDef.real" : cterm
1.73 -
1.74 -> val str = "R=R";
1.75 -> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
1.76 -> atomty (typ_a2real t);
1.77 -*** -------------
1.78 -*** Const ( op =, [RealDef.real, RealDef.real] => bool)
1.79 -*** Free ( R, RealDef.real)
1.80 -*** Free ( R, RealDef.real)
1.81 -> val t' = typ_a2real t;
1.82 -> (cterm_of thy) t';
1.83 -val it = "(R::RealDef.real) = R" : cterm
1.84 -
1.85 -> val str = "fixed_values [R=R]";
1.86 -> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
1.87 -> val t' = typ_a2real t;
1.88 -> (cterm_of thy) t';
1.89 -val it = "fixed_values [(R::RealDef.real) = R]" : cterm
1.90 -*)
1.91 -
1.92 -(*TODO.WN0609: parse should return a term or a string
1.93 - (or even more comprehensive datastructure for error-messages)
1.94 - i.e. in wrapping with SOME term or NONE the latter is not sufficient*)
1.95 -(*2002 fun parseold thy str =
1.96 - (let
1.97 - val sgn = sign_of thy;
1.98 - val t = ((*typ_a2real o*) app_num_tr'1 o term_of)
1.99 - (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
1.100 - in SOME (cterm_of sgn t) end)
1.101 - handle _ => NONE;*)
1.102 -
1.103 -
1.104 -
1.105 +(* before 2002 *)
1.106 fun parseold thy str =
1.107 (let val t = ((*typ_a2real o*) numbers_to_string)
1.108 (Syntax.read_term_global thy str)
1.109 @@ -1124,18 +1057,15 @@
1.110 *** Free ( R, RealDef.real)
1.111 *** Free ( R, RealDef.real) *)
1.112
1.113 -(*fun parse_patt thy str =
1.114 -(**** prep_pbt: syntax error in '#Where' of ["equation"]
1.115 -*** Exception- TOPLEVEL_ERROR raised
1.116 -*** At command "ML" (line 172 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Poly.thy").*)
1.117 - (typ_a2real o numbers_to_string o
1.118 - ProofContext.read_term_pattern (thy2ctxt thy)) str;*)
1.119 -fun parse_patt thy str =
1.120 - ProofContext.read_term_pattern (thy2ctxt thy) str;
1.121 -(*fun parse_patt thy str = (thy, str) |>> thy2ctxt
1.122 +(* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation*)
1.123 +fun parse_patt thy str = (thy, str) |>> thy2ctxt
1.124 |-> ProofContext.read_term_pattern
1.125 |> numbers_to_string
1.126 - |> typ_a2real;*)
1.127 + |> typ_a2real;
1.128 +(*
1.129 +fun parse_patt thy str = (thy, str) |>> thy2ctxt
1.130 + |-> ProofContext.read_term_pattern;
1.131 +*)
1.132
1.133 (*version for testing local to theories*)
1.134 fun str2term_ thy str = (term_of o the o (parse thy)) str;