378 (* Rewriting Automaton *) |
378 (* Rewriting Automaton *) |
379 |
379 |
380 datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE |
380 datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE |
381 | PROVE | POP_CS | POP_ARTR | SPLIT; |
381 | PROVE | POP_CS | POP_ARTR | SPLIT; |
382 (* |
382 (* |
383 fun pr_cntrl c = case c of STOP => prs("STOP") | MK_EQ => prs("MK_EQ") | |
383 fun pr_cntrl c = case c of STOP => std_output("STOP") | MK_EQ => std_output("MK_EQ") | |
384 ASMS i => print_int i | POP_ARTR => prs("POP_ARTR") | |
384 ASMS i => print_int i | POP_ARTR => std_output("POP_ARTR") | |
385 SIMP_LHS => prs("SIMP_LHS") | REW => prs("REW") | REFL => prs("REFL") | |
385 SIMP_LHS => std_output("SIMP_LHS") | REW => std_output("REW") | REFL => std_output("REFL") | |
386 TRUE => prs("TRUE") | PROVE => prs("PROVE") | POP_CS => prs("POP_CS") | SPLIT |
386 TRUE => std_output("TRUE") | PROVE => std_output("PROVE") | POP_CS => std_output("POP_CS") | SPLIT |
387 => prs("SPLIT"); |
387 => std_output("SPLIT"); |
388 *) |
388 *) |
389 fun simp_refl([],_,ss) = ss |
389 fun simp_refl([],_,ss) = ss |
390 | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) |
390 | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) |
391 else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); |
391 else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); |
392 |
392 |