357 (* Rewriting Automaton *) |
357 (* Rewriting Automaton *) |
358 |
358 |
359 datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE |
359 datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE |
360 | PROVE | POP_CS | POP_ARTR | IF; |
360 | PROVE | POP_CS | POP_ARTR | IF; |
361 (* |
361 (* |
362 fun pr_cntrl c = case c of STOP => prs("STOP") | MK_EQ => prs("MK_EQ") | |
362 fun pr_cntrl c = case c of STOP => std_output("STOP") | MK_EQ => std_output("MK_EQ") | |
363 ASMS i => print_int i | POP_ARTR => prs("POP_ARTR") | |
363 ASMS i => print_int i | POP_ARTR => std_output("POP_ARTR") | |
364 SIMP_LHS => prs("SIMP_LHS") | REW => prs("REW") | REFL => prs("REFL") | |
364 SIMP_LHS => std_output("SIMP_LHS") | REW => std_output("REW") | REFL => std_output("REFL") | |
365 TRUE => prs("TRUE") | PROVE => prs("PROVE") | POP_CS => prs("POP_CS") | IF |
365 TRUE => std_output("TRUE") | PROVE => std_output("PROVE") | POP_CS => std_output("POP_CS") | IF |
366 => prs("IF"); |
366 => std_output("IF"); |
367 *) |
367 *) |
368 fun simp_refl([],_,ss) = ss |
368 fun simp_refl([],_,ss) = ss |
369 | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) |
369 | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) |
370 else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); |
370 else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); |
371 |
371 |