304 (((@@ o (map (rule2stac thy))) rules) $ Celem.e_term); |
304 (((@@ o (map (rule2stac thy))) rules) $ Celem.e_term); |
305 |
305 |
306 (* prepare the input for an rls for use: |
306 (* prepare the input for an rls for use: |
307 # generate a script for stepwise execution of the rls |
307 # generate a script for stepwise execution of the rls |
308 # filter the operators for Calc out of the script ?WN111014? |
308 # filter the operators for Calc out of the script ?WN111014? |
309 !!!use this function while storing by or integrate into KEStore_Elems.add_rlss.*) |
309 !!!use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss *) |
310 fun prep_rls _ Celem.Erls = error "prep_rls' not impl. for Erls" |
310 fun prep_rls _ Celem.Erls = error "prep_rls: not required for Erls" |
311 | prep_rls thy (Celem.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) = |
311 | prep_rls thy (Celem.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) = |
312 let val sc = (rules2scr_Rls thy rules) |
312 let val sc = (rules2scr_Rls thy rules) |
313 in Celem.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, |
313 in Celem.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, |
314 srls = srls, |
314 srls = srls, |
315 calc = get_calcs thy sc, |
315 calc = get_calcs thy sc, |
316 rules = rules, |
316 rules = rules, |
317 errpatts=errpatts, |
317 errpatts = errpatts, |
318 scr = Celem.Prog sc} end |
318 scr = Celem.Prog sc} end |
319 | prep_rls thy (Celem.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) = |
319 | prep_rls thy (Celem.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) = |
320 let val sc = (rules2scr_Seq thy rules) |
320 let val sc = (rules2scr_Seq thy rules) |
321 in Celem.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, |
321 in Celem.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, |
322 srls = srls, |
322 srls = srls, |
323 calc = get_calcs thy sc, |
323 calc = get_calcs thy sc, |
324 rules = rules, |
324 rules = rules, |
325 errpatts = errpatts, |
325 errpatts = errpatts, |
326 scr = Celem.Prog sc} end |
326 scr = Celem.Prog sc} end |
327 | prep_rls _ (Celem.Rrls {id, ...}) = |
327 | prep_rls _ (Celem.Rrls {id, ...}) = |
328 error ("prep_rls' not required for Rrls \"" ^ id ^ "\""); |
328 error ("prep_rls: not required for Rrls \"" ^ id ^ "\""); |
329 |
329 |
330 end |
330 end |