1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Apr 06 18:01:02 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Apr 07 16:31:05 2011 +0200
1.3 @@ -162,7 +162,7 @@
1.4 val pt_model : ppobj -> pos_ -> ptform
1.5 val reset_calchead : ptree * pos' -> ptree * pos'
1.6 val seek_oridts :
1.7 - theory ->
1.8 + Proof.context ->
1.9 string ->
1.10 Term.term * Term.term list ->
1.11 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.12 @@ -205,11 +205,9 @@
1.13
1.14
1.15
1.16 -(*---------------------------------------------------------------------
1.17 structure CalcHead (**): CALC_HEAD(**) =
1.18
1.19 struct
1.20 ----------------------------------------------------------------------*)
1.21
1.22 (* datatypes *)
1.23
1.24 @@ -276,18 +274,6 @@
1.25
1.26 (*.to an input (d,ts) find the according ori and insert the ts.*)
1.27 (*WN.11.03: + dont take first inter<>[]*)
1.28 -(*fun seek_oridts ctxt sel (d,ts) [] =
1.29 - ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
1.30 - (comp_dts (d,ts))) ^
1.31 - "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
1.32 - [])
1.33 - | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.34 - if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
1.35 - then ("",
1.36 - (id,vat,sel,d, inter op = ts ts'):ori,
1.37 - ts')
1.38 - else seek_oridts ctxt sel (d,ts) oris;*)
1.39 -
1.40 fun seek_oridts ctxt sel (d,ts) [] =
1.41 ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
1.42 (comp_dts (d,ts))) ^
1.43 @@ -791,10 +777,10 @@
1.44 fun appl_add ctxt sel [] ppc pbt t =
1.45 let
1.46 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
1.47 - in case parseNEW ctxt t of
1.48 + in case parse (ProofContext.theory_of ctxt) t of
1.49 NONE => Add (i, [], false, sel, Syn t)
1.50 | SOME t' =>
1.51 - let val (d, ts) = split_dts t';
1.52 + let val (d, ts) = split_dts (term_of t');
1.53 in if d = e_term then
1.54 Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
1.55 (case find_first (eq1 d) pbt of
1.56 @@ -820,9 +806,9 @@
1.57 end
1.58 end
1.59 | appl_add ctxt sel oris ppc pbt str =
1.60 - case parseNEW ctxt str of
1.61 + case parse (ProofContext.theory_of ctxt) str of
1.62 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.63 - | SOME t => case is_known ctxt sel oris t of
1.64 + | SOME t => case is_known ctxt sel oris (term_of t) of
1.65 ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
1.66 ("", itm) => Add itm
1.67 | (msg, _) => Err msg)
1.68 @@ -1066,7 +1052,7 @@
1.69 end
1.70 (* val (p,_) = p;
1.71 *)
1.72 -| specify_additem sel (ct,_) (p,p_(*Frm, Pbl*)) c pt =
1.73 +| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1.74 let
1.75 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.76 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.77 @@ -1127,10 +1113,9 @@
1.78 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.79 let (* either """"""""""""""" all empty or complete *)
1.80 val thy = assoc_thy dI';
1.81 - val (istate_, ctxt) = (#ppc o get_pbt) pI' |> prep_ori fmz thy;
1.82 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1.83 - else istate_;
1.84 - val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.85 + else pI' |> #ppc o get_pbt |> prep_ori fmz thy |> #1;
1.86 + val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
1.87 (oris,(dI',pI',mI'),e_term);
1.88 val {ppc,prls,where_,...} = get_pbt pI'
1.89 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1.90 @@ -1579,7 +1564,7 @@
1.91 let val {ppc,...} = get_met mI
1.92 val dI = if dI = "" then "Isac" else dI
1.93 val thy = assoc_thy dI;
1.94 - val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.95 + val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.96 ([], (dI,pI,mI), e_term(*FIXME met*));
1.97 val pt = update_spec pt [] (dI,pI,mI);
1.98 val mits = init_pbl' ppc;
1.99 @@ -1601,12 +1586,11 @@
1.100 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
1.101 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.102 val dI = theory2theory' (maxthy thy thy');
1.103 - val ctxt = prep_ori fmz thy ppc |> #2;
1.104 val hdl = case cas of
1.105 NONE => pblterm dI pI
1.106 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1.107 ~~~ vals_of_oris pors) t;
1.108 - val (pt, _) = cappend_problem e_ptree [] (Uistate, ctxt) (fmz, (dI, pI, mI))
1.109 + val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
1.110 (pors, (dI, pI, mI), hdl)
1.111 in ((pt, ([], Pbl)),
1.112 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.113 @@ -2081,9 +2065,6 @@
1.114 val pt = update_spec pt p e_spec
1.115 in (pt, (p,Pbl):pos') end;
1.116
1.117 -(*---------------------------------------------------------------------
1.118 end
1.119
1.120 open CalcHead;
1.121 ----------------------------------------------------------------------*)
1.122 -