285 "~~~~~ fun refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]); |
285 "~~~~~ fun refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]); |
286 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) = |
286 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) = |
287 ((rev o tl) pblID, fmz, [(*match list*)], |
287 ((rev o tl) pblID, fmz, [(*match list*)], |
288 ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): Problem.T Store.node)); |
288 ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): Problem.T Store.node)); |
289 val {thy, ppc, where_, prls, ...} = py ; |
289 val {thy, ppc, where_, prls, ...} = py ; |
290 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc); |
290 "~~~~~ fun O_Model.prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc); |
291 val ctxt = Proof_Context.init_global thy; |
291 val ctxt = Proof_Context.init_global thy; |
292 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt); |
292 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt); |
293 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
293 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
294 (_, _::_) => (Free (v,T)::get_vars vs) |
294 (_, _::_) => (Free (v,T)::get_vars vs) |
295 | (_, [] ) => get_vars vs) (*filter out nums as long as |
295 | (_, [] ) => get_vars vs) (*filter out nums as long as |