299 "~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) = |
299 "~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) = |
300 ((rev o tl) pblID, fmz, [(*match list*)], |
300 ((rev o tl) pblID, fmz, [(*match list*)], |
301 ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node)); |
301 ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node)); |
302 val {thy, model, where_, where_rls, ...} = py ; |
302 val {thy, model, where_, where_rls, ...} = py ; |
303 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model); |
303 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model); |
304 val ctxt = Proof_Context.init_global thy; |
304 val (ts, ctxt) = ContextC.build_while_parsing fmz thy; |
305 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt); |
305 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt); |
306 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
306 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
307 (_, _::_) => (Free (v,T)::get_vars vs) |
307 (_, _::_) => (Free (v,T)::get_vars vs) |
308 | (_, [] ) => get_vars vs) (*filter out nums as long as |
308 | (_, [] ) => get_vars vs) (*filter out nums as long as |
309 we have Free ("123",_)*) |
309 we have Free ("123",_)*) |