equal
deleted
inserted
replaced
19 let |
19 let |
20 val (_, _, metID) = Ctree.get_somespec' spec spec' |
20 val (_, _, metID) = Ctree.get_somespec' spec spec' |
21 val pre = if metID = MethodC.id_empty then [] |
21 val pre = if metID = MethodC.id_empty then [] |
22 else |
22 else |
23 let |
23 let |
24 val {prls, pre = where_, ...} = MethodC.from_store_PIDE ctxt metID |
24 val {prls, pre = where_, ...} = MethodC.from_store ctxt metID |
25 val (_, pre) = Pre_Conds.check prls where_ meth 0 |
25 val (_, pre) = Pre_Conds.check prls where_ meth 0 |
26 in pre end |
26 in pre end |
27 val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 pre)) |
27 val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 pre)) |
28 in |
28 in |
29 Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, pre, spec) |
29 Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, pre, spec) |
33 val (thy_id, pI, _) = Ctree.get_somespec' spec spec' |
33 val (thy_id, pI, _) = Ctree.get_somespec' spec spec' |
34 val ctxt = Proof_Context.init_global (ThyC.get_theory thy_id) |
34 val ctxt = Proof_Context.init_global (ThyC.get_theory thy_id) |
35 val pre = if pI = Problem.id_empty then [] |
35 val pre = if pI = Problem.id_empty then [] |
36 else |
36 else |
37 let |
37 let |
38 val {prls, where_, ...} = Problem.from_store_PIDE ctxt pI |
38 val {prls, where_, ...} = Problem.from_store ctxt pI |
39 val (_, pre) = Pre_Conds.check prls where_ probl 0 |
39 val (_, pre) = Pre_Conds.check prls where_ probl 0 |
40 in pre end |
40 in pre end |
41 val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 pre)) |
41 val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 pre)) |
42 in |
42 in |
43 Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, pre, spec) |
43 Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, pre, spec) |
47 fun pt_form (Ctree.PrfObj {form, ...}) = Ctree.Form form |
47 fun pt_form (Ctree.PrfObj {form, ...}) = Ctree.Form form |
48 | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ...}) = |
48 | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ...}) = |
49 let |
49 let |
50 val (dI, pI, _) = Ctree.get_somespec' spec spec' |
50 val (dI, pI, _) = Ctree.get_somespec' spec spec' |
51 val ctxt = Proof_Context.init_global (ThyC.get_theory dI) |
51 val ctxt = Proof_Context.init_global (ThyC.get_theory dI) |
52 val {cas, ...} = Problem.from_store_PIDE ctxt pI |
52 val {cas, ...} = Problem.from_store ctxt pI |
53 in case cas of |
53 in case cas of |
54 NONE => Ctree.Form (Auto_Prog.pblterm_PIDE dI pI) |
54 NONE => Ctree.Form (Auto_Prog.pblterm dI pI) |
55 | SOME t => Ctree.Form (subst_atomic (I_Model.environment probl) t) |
55 | SOME t => Ctree.Form (subst_atomic (I_Model.environment probl) t) |
56 end |
56 end |
57 |
57 |
58 (* pt_extract returns |
58 (* pt_extract returns |
59 # the formula at pos |
59 # the formula at pos |