679 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k; |
679 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k; |
680 |
680 |
681 (* |
681 (* |
682 end (*struct*) |
682 end (*struct*) |
683 *) |
683 *) |
684 |
|
685 |
|
686 |
|
687 val e_rule = |
|
688 Thm ("refl", @{thm refl}); |
|
689 fun id_of_thm (Thm (id, _)) = id |
|
690 | id_of_thm _ = error "id_of_thm"; |
|
691 fun thm_of_thm (Thm (_, thm)) = thm |
|
692 | thm_of_thm _ = error "thm_of_thm"; |
|
693 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
|
694 |
|
695 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); |
|
696 fun thyID_of_derivation_name dn = hd (space_explode "." dn); |
|
697 |
|
698 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = |
|
699 (strip_thy thmid1) = (strip_thy thmid2); |
|
700 (*version typed weaker WN100910*) |
|
701 fun eq_thmI' ((thmid1, _), (thmid2, _)) = |
|
702 (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2); |
|
703 |
|
704 |
|
705 val string_of_thm = Thm.get_name_hint; (*FIXME.2009*) |
|
706 (*check for [.] as caused by "fun assoc_thm'"*) |
|
707 fun string_of_thmI thm = |
|
708 let val ct' = (de_quote o string_of_thm) thm |
|
709 val (a, b) = split_nlast (5, Symbol.explode ct') |
|
710 in case b of |
|
711 [" ", " ","[", ".", "]"] => implode a |
|
712 | _ => ct' |
|
713 end; |
|
714 |
|
715 (*.id requested for all, Rls,Seq,Rrls.*) |
|
716 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*) |
|
717 | id_rls (Rls {id,...}) = id |
|
718 | id_rls (Seq {id,...}) = id |
|
719 | id_rls (Rrls {id,...}) = id; |
|
720 val rls2str = id_rls; |
|
721 fun id_rule (Thm (id, _)) = id |
|
722 | id_rule (Calc (id, _)) = id |
|
723 | id_rule (Rls_ rls) = id_rls rls; |
|
724 |
|
725 fun get_rules (Rls {rules,...}) = rules |
|
726 | get_rules (Seq {rules,...}) = rules |
|
727 | get_rules (Rrls _) = []; |
|
728 |
|
729 fun rule2str Erule = "Erule" |
|
730 | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")" |
|
731 | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)" |
|
732 | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" |
|
733 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; |
|
734 fun rule2str' Erule = "Erule" |
|
735 | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")" |
|
736 | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)" |
|
737 | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" |
|
738 | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; |
|
739 |
|
740 (*WN080102 compare eq_rule ?!?*) |
|
741 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2 |
|
742 | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2 |
|
743 | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2 |
|
744 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*) |
|
745 | eqrule _ = false; |
|
746 |
|
747 |
|
748 type rrlsstate = (*state for reverse rewriting*) |
|
749 (term * (*the current formula: |
|
750 goes locate_gen -> next_tac via istate*) |
|
751 term * (*the final formula*) |
|
752 rule list (*of reverse rewrite set (#1#)*) |
|
753 list * (*may be serveral, eg. in norm_rational*) |
|
754 (rule * (*Thm (+ Thm generated from Calc) resulting in ...*) |
|
755 (term * (*... rewrite with ...*) |
|
756 term list)) (*... assumptions*) |
|
757 list); (*derivation from given term to normalform |
|
758 in reverse order with sym_thm; |
|
759 (#1#) could be extracted from here #1*) |
|
760 val e_type = Type("empty",[]); |
|
761 val a_type = TFree("'a",[]); |
|
762 val e_term = Const("empty",e_type); |
|
763 val a_term = Free("empty",a_type); |
|
764 val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate; |
|
765 |
|
766 |
|
767 |
|
768 |
|
769 (*22.2.02: ging auf Linux nicht (Stefan) |
|
770 val e_scr = Script ((term_of o the o (parse thy)) "e_script");*) |
|
771 val e_term = Const("empty", Type("'a", [])); |
|
772 val e_scr = Script e_term; |
|
773 |
|
774 |
|
775 (*ad thm': |
|
776 there are two kinds of theorems ... |
|
777 (1) known by isabelle |
|
778 (2) not known, eg. calc_thm, instantiated rls |
|
779 the latter have a thmid "#..." |
|
780 and thus outside isa we ALWAYS transport both (thmid,string_of_thmI) |
|
781 and have a special assoc_thm / assoc_rls in this interface *) |
|
782 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) |
|
783 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) |
|
784 type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*) |
|
785 |
|
786 fun string_of_thy thy = Context.theory_name thy: theory'; |
|
787 val theory2domID = string_of_thy; |
|
788 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID; |
|
789 val theory2theory' = string_of_thy; |
|
790 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*) |
|
791 val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy; |
|
792 (*> theory2str' (Thy_Info.get_theory "Isac"); |
|
793 al it = "Isac" : string |
|
794 *) |
|
795 |
|
796 fun thyID2theory' (thyID:thyID) = thyID; |
|
797 (* |
|
798 let val ss = Symbol.explode thyID |
|
799 val ext = implode (takelast (4, ss)) |
|
800 in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*) |
|
801 else thyID ^ ".thy" |
|
802 end; |
|
803 *) |
|
804 (* thyID2theory' "Isac" (*ok*); |
|
805 val it = "Isac" : theory' |
|
806 > thyID2theory' "Isac" (*abuse, goes ok...*); |
|
807 val it = "Isac" : theory' |
|
808 *) |
|
809 |
|
810 fun theory'2thyID (theory':theory') = theory'; |
|
811 (* |
|
812 let val ss = Symbol.explode theory' |
|
813 val ext = implode (takelast (4, ss)) |
|
814 in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID |
|
815 else theory' (*disarm abuse of theory'*) |
|
816 end; |
|
817 *) |
|
818 (* theory'2thyID "Isac"; |
|
819 val it = "Isac" : thyID |
|
820 > theory'2thyID "Isac"; |
|
821 val it = "Isac" : thyID*) |
|
822 |
|
823 |
|
824 (*. WN0509 discussion: |
|
825 ############################################################################# |
|
826 # How to manage theorys in subproblems wrt. the requirement, # |
|
827 # that scripts should be re-usable ? # |
|
828 ############################################################################# |
|
829 |
|
830 eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..' |
|
831 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script |
|
832 because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b |
|
833 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard |
|
834 (see match_ags). |
|
835 |
|
836 Preliminary solution: |
|
837 # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically, |
|
838 # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl |
|
839 # however, a thy specified by the user in the rootpbl may lead to |
|
840 errors in far-off subpbls (which are not yet reported properly !!!) |
|
841 and interactively specifiying thys in subpbl is not very relevant. |
|
842 |
|
843 Other solutions possible: |
|
844 # always parse and type-check with Thy_Info.get_theory "Isac" |
|
845 (rejected tue to the vague idea eg. to re-use equations for R in C etc.) |
|
846 # regard the subthy-relation in specifying thys of subpbls |
|
847 # specifically handle 'SubProblem (undefined, pbl, arglist)' |
|
848 # ??? |
|
849 .*) |
|
850 (*WN0509 TODO "ProtoPure" ... would be more consistent |
|
851 with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*) |
|
852 val e_domID = "e_domID":domID; |
|
853 |
|
854 (*the key into the hierarchy ob theory elements*) |
|
855 type theID = string list; |
|
856 val e_theID = ["e_theID"]; |
|
857 val theID2str = strs2str; |
|
858 (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*) |
|
859 fun theID2thyID (theID:theID) = |
|
860 if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID |
|
861 else error ("theID2thyID called with "^ theID2str theID); |
|
862 |
|
863 (*the key into the hierarchy ob problems*) |
|
864 type pblID = string list; (* domID::...*) |
|
865 val e_pblID = ["e_pblID"]:pblID; |
|
866 val pblID2str = strs2str; |
|
867 |
|
868 (*the key into the hierarchy ob methods*) |
|
869 type metID = string list; |
|
870 val e_metID = ["e_metID"]:metID; |
|
871 val metID2str = strs2str; |
|
872 |
|
873 (*either theID or pblID or metID*) |
|
874 type kestoreID = string list; |
|
875 val e_kestoreID = ["e_kestoreID"]; |
|
876 val kestoreID2str = strs2str; |
|
877 |
|
878 (*for distinction of contexts*) |
|
879 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_; |
|
880 fun ketype2str Exp_ = "Exp_" |
|
881 | ketype2str Thy_ = "Thy_" |
|
882 | ketype2str Pbl_ = "Pbl_" |
|
883 | ketype2str Met_ = "Met_"; |
|
884 fun ketype2str' Exp_ = "Example" |
|
885 | ketype2str' Thy_ = "Theory" |
|
886 | ketype2str' Pbl_ = "Problem" |
|
887 | ketype2str' Met_ = "Method"; |
|
888 |
|
889 (*see 'How to manage theorys in subproblems' at 'type thyID'*) |
|
890 val theory' = Unsynchronized.ref ([]:(theory' * theory) list); |
|
891 |
|
892 (*.all theories defined for Scripts, recorded in Scripts/Script.ML; |
|
893 in order to distinguish them from general IsacKnowledge defined later on.*) |
|
894 val script_thys = Unsynchronized.ref ([] : (theory' * theory) list); |
|
895 |
|
896 |
|
897 (*rewrite orders, also stored in 'type met' and type 'and rls' |
|
898 The association list is required for 'rewrite.."rew_ord"..' |
|
899 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
|
900 val rew_ord' = |
|
901 Unsynchronized.ref |
|
902 ([]:(rew_ord' * (*the key for the association list *) |
|
903 (subst (*the bound variables - they get high order*) |
|
904 -> (term * term) (*(t1, t2) to be compared *) |
|
905 -> bool)) (*if t1 <= t2 then true else false *) |
|
906 list); (*association list *) |
|
907 |
|
908 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), |
|
909 ("dummy_ord", dummy_ord)]); |
|
910 |
|
911 |
|
912 (*WN060120 a hack to get alltogether run again with minimal effort: |
|
913 theory' is inserted for creating thy_hierarchy; calls for assoc_rls |
|
914 need not be called*) |
|
915 val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list); |
|
916 |
|
917 (*FIXME.040207 calclist': used by prep_rls, NOT in met*) |
|
918 val calclist'= Unsynchronized.ref ([]: calc list); |
|
919 |
|
920 (*.the hierarchy of thydata.*) |
|
921 |
|
922 (*.'a is for pbt | met.*) |
|
923 (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*) |
|
924 datatype 'a ptyp = |
|
925 Ptyp of string * (*element within pblID*) |
|
926 'a list * (*several pbts with different domIDs/thy |
|
927 TODO: select by subthy (isaref.p.69) |
|
928 presently only _ONE_ elem*) |
|
929 ('a ptyp) list; (*the children nodes*) |
|
930 |
|
931 (*.datatype for collecting thydata for hierarchy.*) |
|
932 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*) |
|
933 (*WN0606 Htxt contains html which does not belong to the sml-kernel*) |
|
934 datatype thydata = Html of {guh: guh, |
|
935 coursedesign: authors, |
|
936 mathauthors: authors, |
|
937 html: string} (*html; for demos before database*) |
|
938 | Hthm of {guh: guh, |
|
939 coursedesign: authors, |
|
940 mathauthors: authors, |
|
941 thm: term} |
|
942 | Hrls of {guh: guh, |
|
943 coursedesign: authors, |
|
944 mathauthors: authors, |
|
945 (*like vvvvvvvvvvvvv val ruleset' |
|
946 WN060711 redesign together !*) |
|
947 thy_rls: (thyID * rls)} |
|
948 | Hcal of {guh: guh, |
|
949 coursedesign: authors, |
|
950 mathauthors: authors, |
|
951 calc: calc} |
|
952 | Hord of {guh: guh, |
|
953 coursedesign: authors, |
|
954 mathauthors: authors, |
|
955 ord: (subst -> (term * term) -> bool)}; |
|
956 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; |
|
957 |
|
958 type thehier = (thydata ptyp) list; |
|
959 val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*) |
|
960 |
|
961 (* an association list, gets the value once in Isac.ML. |
|
962 stores Isabelle's thms as terms for compatibility with Theory.axioms_of. |
|
963 WN1-1-28 make this data arguments and del ref ?*) |
|
964 val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list); |
|
965 |
|
966 |
|
967 type path = string; |
|
968 type filename = string; |
|
969 |
|
970 (*val xxx = fn: a b => (a,b); ??? fun-definition ???*) |
|
971 local |
|
972 fun ii (_:term) = e_rrlsstate; |
|
973 fun no (_:term) = SOME (e_term,[e_term]); |
|
974 fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))]; |
|
975 fun ne (_:rule list list) (_:term) = SOME e_rule; |
|
976 fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))]; |
|
977 in |
|
978 val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo, |
|
979 next_rule=ne,attach_form=fo}; |
|
980 end; |
|
981 |
|
982 val e_rls = |
|
983 Rls{id = "e_rls", |
|
984 preconds = [], |
|
985 rew_ord = ("dummy_ord", dummy_ord), |
|
986 erls = Erls,srls = Erls, |
|
987 calc = [], |
|
988 rules = [], scr = EmptyScr}:rls; |
|
989 val e_rrls = Rrls {id = "e_rrls", |
|
990 prepat = [], |
|
991 rew_ord = ("dummy_ord", dummy_ord), |
|
992 erls = Erls, |
|
993 calc = [], |
|
994 (*asm_thm=[],*) |
|
995 scr=e_rfuns}:rls; |
|
996 ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)), |
|
997 ("e_rrls",("Tools",e_rrls)) |
|
998 ]); |
|
999 |
|
1000 fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = |
|
1001 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, |
|
1002 (*asm_thm=asm_thm,*)rules=rules,scr=scr} |
|
1003 | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = |
|
1004 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, |
|
1005 (*asm_thm=asm_thm,*)rules=rules,scr=scr} |
|
1006 | rep_rls Erls = rep_rls e_rls |
|
1007 | rep_rls (Rrls {id,...}) = rep_rls e_rls |
|
1008 (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*); |
|
1009 (*| rep_rls (Seq {id,...}) = |
|
1010 error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id); |
|
1011 --1.7.03*) |
|
1012 fun rep_rrls |
|
1013 (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord, |
|
1014 scr=Rfuns |
|
1015 {attach_form,init_state,locate_rule, |
|
1016 next_rule,normal_form}}) = |
|
1017 {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat, |
|
1018 rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, |
|
1019 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form} |
|
1020 | rep_rrls (Rls {id,...}) = |
|
1021 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id) |
|
1022 | rep_rrls (Seq {id,...}) = |
|
1023 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id); |
|
1024 |
|
1025 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1026 rules =rs,scr=sc}) r = |
|
1027 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1028 rules = rs @ r,scr=sc}:rls) |
|
1029 | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1030 rules =rs,scr=sc}) r = |
|
1031 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1032 rules = rs @ r,scr=sc}:rls) |
|
1033 | append_rls id (Rrls _) _ = |
|
1034 error ("append_rls: not for reverse-rewrite-rule-set "^id); |
|
1035 |
|
1036 (*. are _atomic_ rules equal ?.*) |
|
1037 (*WN080102 compare eqrule ?!?*) |
|
1038 fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2 |
|
1039 | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2 |
|
1040 | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2 |
|
1041 (*id_rls checks for Rls, Seq, Rrls*) |
|
1042 | eq_rule _ = false; |
|
1043 |
|
1044 fun merge_rls _ Erls rls = rls |
|
1045 | merge_rls _ rls Erls = rls |
|
1046 | merge_rls id |
|
1047 (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, |
|
1048 (*asm_thm=at1,*)rules =rs1,scr=sc1}) |
|
1049 (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, |
|
1050 (*asm_thm=at2,*)rules =rs2,scr=sc2}) = |
|
1051 (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), |
|
1052 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), |
|
1053 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 |
|
1054 ((#srls o rep_rls) r2), |
|
1055 calc=ca1 @ ((#calc o rep_rls) r2), |
|
1056 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) |
|
1057 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), |
|
1058 scr=sc1}:rls) |
|
1059 | merge_rls id |
|
1060 (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, |
|
1061 (*asm_thm=at1,*)rules =rs1,scr=sc1}) |
|
1062 (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, |
|
1063 (*asm_thm=at2,*)rules =rs2,scr=sc2}) = |
|
1064 (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), |
|
1065 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), |
|
1066 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 |
|
1067 ((#srls o rep_rls) r2), |
|
1068 calc=ca1 @ ((#calc o rep_rls) r2), |
|
1069 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) |
|
1070 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), |
|
1071 scr=sc1}:rls) |
|
1072 | merge_rls _ _ _ = |
|
1073 error "merge_rls: not for reverse-rewrite-rule-sets\ |
|
1074 \and not for mixed Rls -- Seq"; |
|
1075 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1076 (*asm_thm=at,*)rules =rs,scr=sc}) r = |
|
1077 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1078 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), |
|
1079 scr=sc}:rls) |
|
1080 | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1081 (*asm_thm=at,*)rules =rs,scr=sc}) r = |
|
1082 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1083 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), |
|
1084 scr=sc}:rls) |
|
1085 | remove_rls id (Rrls _) _ = error |
|
1086 ("remove_rls: not for reverse-rewrite-rule-set "^id); |
|
1087 |
|
1088 (*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]); |
|
1089 val it = [1, 2] : int list*) |
|
1090 |
|
1091 (*elder version: migrated 3 calls in smtest to memrls |
|
1092 fun mem_rls id rls = |
|
1093 case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of |
|
1094 SOME _ => true | NONE => false;*) |
|
1095 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules) |
|
1096 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules) |
|
1097 | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r)); |
|
1098 fun rls_get_thm rls (id: xstring) = |
|
1099 case find_first (curry eq_rule e_rule) |
|
1100 ((#rules o rep_rls) rls) of |
|
1101 SOME thm => SOME thm | NONE => NONE; |
|
1102 |
|
1103 fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known") |
|
1104 | assoc' ((keyi, xi) :: pairs, key) = |
|
1105 if key = keyi then SOME xi else assoc' (pairs, key); |
|
1106 |
|
1107 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) |
|
1108 handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*) |
|
1109 fun assoc_thy (thy:theory') = |
|
1110 if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*) |
|
1111 else (Thy_Info.get_theory thy) |
|
1112 handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system"); |
|
1113 |
|
1114 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; |
|
1115 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle |
|
1116 overlays by re-using an identifier in different thys.*) |
|
1117 fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls)) |
|
1118 handle _ => error ("ME_Isa: '"^rls^"' not in system"); |
|
1119 (*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls)) |
|
1120 handle _ => error ("ME_Isa: '"^rls^"' not in system");*) |
|
1121 |
|
1122 (*.overwrite an element in an association list and pair it with a thyID |
|
1123 in order to create the thy_hierarchy; |
|
1124 overwrites existing rls' even if they are defined in a different thy; |
|
1125 this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*) |
|
1126 (*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that |
|
1127 they do NOT handle overlays by re-using an identifier in different thys; |
|
1128 "thyID.rlsID" would be a good solution, if the "." would be possible |
|
1129 in scripts... |
|
1130 actually a hack to get alltogether run again with minimal effort*) |
|
1131 fun insthy thy' (rls', rls) = (rls', (thy', rls)); |
|
1132 fun overwritelthy thy (al, bl:(rls' * rls) list) = |
|
1133 let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl |
|
1134 in overwritel (al, bl') end; |
|
1135 |
|
1136 fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro)) |
|
1137 handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system"); |
|
1138 (*get the string for stac from rule*) |
|
1139 fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found") |
|
1140 | assoc_calc ((calc, (keyi, xi)) :: pairs, key) = |
|
1141 if key = keyi then calc else assoc_calc (pairs, key); |
|
1142 (*only used for !calclist'...*) |
|
1143 fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key |
|
1144 ^"' not found") |
|
1145 | assoc1 ((all as (keyi, _)) :: pairs, key) = |
|
1146 if key = keyi then all else assoc1 (pairs, key); |
|
1147 |
|
1148 (*TODO.WN080102 clarify usage of type cal and type calc..*) |
|
1149 fun calID2calcID (calID : calID) = |
|
1150 let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'") |
|
1151 | ass ((calci, (cali, eval_fn))::ids) = |
|
1152 if calID = cali then calci |
|
1153 else ass ids |
|
1154 in ass (!calclist') : calcID end; |
|
1155 |
|
1156 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term |
|
1157 (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; |
|
1158 |
|
1159 fun terms2str ts = (strs2str o (map term2str )) ts; |
|
1160 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*) |
|
1161 fun terms2str' ts = (strs2str' o (map term2str )) ts; |
|
1162 (*terms2str' [t1,t2] = "[1 + 2,abc]";*) |
|
1163 fun terms2strs ts = (map term2str) ts; |
|
1164 (*terms2strs [t1,t2] = ["1 + 2", "abc"];*) |
|
1165 |
|
1166 fun termopt2str (SOME t) = "SOME " ^ term2str t |
|
1167 | termopt2str NONE = "NONE"; |
|
1168 |
|
1169 fun type2str typ = |
|
1170 Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ; |
|
1171 val string_of_typ = type2str; |
|
1172 |
|
1173 fun subst2str (s:subst) = |
|
1174 (strs2str o |
|
1175 (map (linefeed o pair2str o |
|
1176 (apsnd term2str) o |
|
1177 (apfst term2str)))) s; |
|
1178 fun subst2str' (s:subst) = |
|
1179 (strs2str' o |
|
1180 (map (pair2str o |
|
1181 (apsnd term2str) o |
|
1182 (apfst term2str)))) s; |
|
1183 (*> subst2str' [(str2term "bdv", str2term "x"), |
|
1184 (str2term "bdv_2", str2term "y")]; |
|
1185 val it = "[(bdv, x)]" : string |
|
1186 *) |
|
1187 val env2str = subst2str; |
|
1188 |
|
1189 |
|
1190 (*recursive defs:*) |
|
1191 fun scr2str (Script s) = "Script "^(term2str s) |
|
1192 | scr2str (Rfuns _) = "Rfuns"; |
|
1193 |
|
1194 |
|
1195 fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1; |
|
1196 |
|
1197 |
|
1198 (*.trace internal steps of isac's rewriter*) |
|
1199 val trace_rewrite = Unsynchronized.ref false; |
|
1200 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) |
|
1201 val depth = Unsynchronized.ref 99999; |
|
1202 (*.no of rewrites exceeding this int -> NO rewrite.*) |
|
1203 (*WN060829 still unused...*) |
|
1204 val lim_rewrite = Unsynchronized.ref 99999; |
|
1205 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*) |
|
1206 val lim_deriv = Unsynchronized.ref 100; |
|
1207 (*.switch for checking guhs unique before storing a pbl or met; |
|
1208 set true at startup (done at begin of ROOT.ML) |
|
1209 set false for editing IsacKnowledge (done at end of ROOT.ML).*) |
|
1210 val check_guhs_unique = Unsynchronized.ref false; |
|
1211 |
|
1212 |
|
1213 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) |
|
1214 L (*go left at $*) |
|
1215 | R (*go right at $*) |
|
1216 | D; (*go down at Abs*) |
|
1217 type loc_ = lrd list; |
|
1218 fun ldr2str L = "L" |
|
1219 | ldr2str R = "R" |
|
1220 | ldr2str D = "D"; |
|
1221 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k; |
|
1222 |
|
1223 (* |
|
1224 end (*struct*) |
|
1225 *) |
|
1226 |
|
1227 |
|
1228 val e_rule = |
|
1229 Thm ("refl", @{thm refl}); |
|
1230 fun id_of_thm (Thm (id, _)) = id |
|
1231 | id_of_thm _ = error "id_of_thm"; |
|
1232 fun thm_of_thm (Thm (_, thm)) = thm |
|
1233 | thm_of_thm _ = error "thm_of_thm"; |
|
1234 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
|
1235 |
|
1236 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); |
|
1237 fun thyID_of_derivation_name dn = hd (space_explode "." dn); |
|
1238 |
|
1239 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = |
|
1240 (strip_thy thmid1) = (strip_thy thmid2); |
|
1241 (*version typed weaker WN100910*) |
|
1242 fun eq_thmI' ((thmid1, _), (thmid2, _)) = |
|
1243 (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2); |
|
1244 |
|
1245 |
|
1246 val string_of_thm = Thm.get_name_hint; (*FIXME.2009*) |
|
1247 (*check for [.] as caused by "fun assoc_thm'"*) |
|
1248 fun string_of_thmI thm = |
|
1249 let val ct' = (de_quote o string_of_thm) thm |
|
1250 val (a, b) = split_nlast (5, Symbol.explode ct') |
|
1251 in case b of |
|
1252 [" ", " ","[", ".", "]"] => implode a |
|
1253 | _ => ct' |
|
1254 end; |
|
1255 |
|
1256 (*.id requested for all, Rls,Seq,Rrls.*) |
|
1257 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*) |
|
1258 | id_rls (Rls {id,...}) = id |
|
1259 | id_rls (Seq {id,...}) = id |
|
1260 | id_rls (Rrls {id,...}) = id; |
|
1261 val rls2str = id_rls; |
|
1262 fun id_rule (Thm (id, _)) = id |
|
1263 | id_rule (Calc (id, _)) = id |
|
1264 | id_rule (Rls_ rls) = id_rls rls; |
|
1265 |
|
1266 fun get_rules (Rls {rules,...}) = rules |
|
1267 | get_rules (Seq {rules,...}) = rules |
|
1268 | get_rules (Rrls _) = []; |
|
1269 |
|
1270 fun rule2str Erule = "Erule" |
|
1271 | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")" |
|
1272 | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)" |
|
1273 | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" |
|
1274 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; |
|
1275 fun rule2str' Erule = "Erule" |
|
1276 | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")" |
|
1277 | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)" |
|
1278 | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" |
|
1279 | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; |
|
1280 |
|
1281 (*WN080102 compare eq_rule ?!?*) |
|
1282 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2 |
|
1283 | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2 |
|
1284 | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2 |
|
1285 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*) |
|
1286 | eqrule _ = false; |
|
1287 |
|
1288 |
|
1289 type rrlsstate = (*state for reverse rewriting*) |
|
1290 (term * (*the current formula: |
|
1291 goes locate_gen -> next_tac via istate*) |
|
1292 term * (*the final formula*) |
|
1293 rule list (*of reverse rewrite set (#1#)*) |
|
1294 list * (*may be serveral, eg. in norm_rational*) |
|
1295 (rule * (*Thm (+ Thm generated from Calc) resulting in ...*) |
|
1296 (term * (*... rewrite with ...*) |
|
1297 term list)) (*... assumptions*) |
|
1298 list); (*derivation from given term to normalform |
|
1299 in reverse order with sym_thm; |
|
1300 (#1#) could be extracted from here #1*) |
|
1301 val e_type = Type("empty",[]); |
|
1302 val a_type = TFree("'a",[]); |
|
1303 val e_term = Const("empty",e_type); |
|
1304 val a_term = Free("empty",a_type); |
|
1305 val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate; |
|
1306 |
|
1307 |
|
1308 |
|
1309 |
|
1310 (*22.2.02: ging auf Linux nicht (Stefan) |
|
1311 val e_scr = Script ((term_of o the o (parse thy)) "e_script");*) |
|
1312 val e_term = Const("empty", Type("'a", [])); |
|
1313 val e_scr = Script e_term; |
|
1314 |
|
1315 |
|
1316 (*ad thm': |
|
1317 there are two kinds of theorems ... |
|
1318 (1) known by isabelle |
|
1319 (2) not known, eg. calc_thm, instantiated rls |
|
1320 the latter have a thmid "#..." |
|
1321 and thus outside isa we ALWAYS transport both (thmid,string_of_thmI) |
|
1322 and have a special assoc_thm / assoc_rls in this interface *) |
|
1323 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) |
|
1324 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) |
|
1325 type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*) |
|
1326 |
|
1327 fun string_of_thy thy = Context.theory_name thy: theory'; |
|
1328 val theory2domID = string_of_thy; |
|
1329 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID; |
|
1330 val theory2theory' = string_of_thy; |
|
1331 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*) |
|
1332 val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy; |
|
1333 (*> theory2str' (Thy_Info.get_theory "Isac"); |
|
1334 al it = "Isac" : string |
|
1335 *) |
|
1336 |
|
1337 fun thyID2theory' (thyID:thyID) = thyID; |
|
1338 (* |
|
1339 let val ss = Symbol.explode thyID |
|
1340 val ext = implode (takelast (4, ss)) |
|
1341 in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*) |
|
1342 else thyID ^ ".thy" |
|
1343 end; |
|
1344 *) |
|
1345 (* thyID2theory' "Isac" (*ok*); |
|
1346 val it = "Isac" : theory' |
|
1347 > thyID2theory' "Isac" (*abuse, goes ok...*); |
|
1348 val it = "Isac" : theory' |
|
1349 *) |
|
1350 |
|
1351 fun theory'2thyID (theory':theory') = theory'; |
|
1352 (* |
|
1353 let val ss = Symbol.explode theory' |
|
1354 val ext = implode (takelast (4, ss)) |
|
1355 in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID |
|
1356 else theory' (*disarm abuse of theory'*) |
|
1357 end; |
|
1358 *) |
|
1359 (* theory'2thyID "Isac"; |
|
1360 val it = "Isac" : thyID |
|
1361 > theory'2thyID "Isac"; |
|
1362 val it = "Isac" : thyID*) |
|
1363 |
|
1364 |
|
1365 (*. WN0509 discussion: |
|
1366 ############################################################################# |
|
1367 # How to manage theorys in subproblems wrt. the requirement, # |
|
1368 # that scripts should be re-usable ? # |
|
1369 ############################################################################# |
|
1370 |
|
1371 eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..' |
|
1372 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script |
|
1373 because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b |
|
1374 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard |
|
1375 (see match_ags). |
|
1376 |
|
1377 Preliminary solution: |
|
1378 # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically, |
|
1379 # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl |
|
1380 # however, a thy specified by the user in the rootpbl may lead to |
|
1381 errors in far-off subpbls (which are not yet reported properly !!!) |
|
1382 and interactively specifiying thys in subpbl is not very relevant. |
|
1383 |
|
1384 Other solutions possible: |
|
1385 # always parse and type-check with Thy_Info.get_theory "Isac" |
|
1386 (rejected tue to the vague idea eg. to re-use equations for R in C etc.) |
|
1387 # regard the subthy-relation in specifying thys of subpbls |
|
1388 # specifically handle 'SubProblem (undefined, pbl, arglist)' |
|
1389 # ??? |
|
1390 .*) |
|
1391 (*WN0509 TODO "ProtoPure" ... would be more consistent |
|
1392 with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*) |
|
1393 val e_domID = "e_domID":domID; |
|
1394 |
|
1395 (*the key into the hierarchy ob theory elements*) |
|
1396 type theID = string list; |
|
1397 val e_theID = ["e_theID"]; |
|
1398 val theID2str = strs2str; |
|
1399 (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*) |
|
1400 fun theID2thyID (theID:theID) = |
|
1401 if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID |
|
1402 else error ("theID2thyID called with "^ theID2str theID); |
|
1403 |
|
1404 (*the key into the hierarchy ob problems*) |
|
1405 type pblID = string list; (* domID::...*) |
|
1406 val e_pblID = ["e_pblID"]:pblID; |
|
1407 val pblID2str = strs2str; |
|
1408 |
|
1409 (*the key into the hierarchy ob methods*) |
|
1410 type metID = string list; |
|
1411 val e_metID = ["e_metID"]:metID; |
|
1412 val metID2str = strs2str; |
|
1413 |
|
1414 (*either theID or pblID or metID*) |
|
1415 type kestoreID = string list; |
|
1416 val e_kestoreID = ["e_kestoreID"]; |
|
1417 val kestoreID2str = strs2str; |
|
1418 |
|
1419 (*for distinction of contexts*) |
|
1420 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_; |
|
1421 fun ketype2str Exp_ = "Exp_" |
|
1422 | ketype2str Thy_ = "Thy_" |
|
1423 | ketype2str Pbl_ = "Pbl_" |
|
1424 | ketype2str Met_ = "Met_"; |
|
1425 fun ketype2str' Exp_ = "Example" |
|
1426 | ketype2str' Thy_ = "Theory" |
|
1427 | ketype2str' Pbl_ = "Problem" |
|
1428 | ketype2str' Met_ = "Method"; |
|
1429 |
|
1430 (*see 'How to manage theorys in subproblems' at 'type thyID'*) |
|
1431 val theory' = Unsynchronized.ref ([]:(theory' * theory) list); |
|
1432 |
|
1433 (*.all theories defined for Scripts, recorded in Scripts/Script.ML; |
|
1434 in order to distinguish them from general IsacKnowledge defined later on.*) |
|
1435 val script_thys = Unsynchronized.ref ([] : (theory' * theory) list); |
|
1436 |
|
1437 |
|
1438 (*rewrite orders, also stored in 'type met' and type 'and rls' |
|
1439 The association list is required for 'rewrite.."rew_ord"..' |
|
1440 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
|
1441 val rew_ord' = |
|
1442 Unsynchronized.ref |
|
1443 ([]:(rew_ord' * (*the key for the association list *) |
|
1444 (subst (*the bound variables - they get high order*) |
|
1445 -> (term * term) (*(t1, t2) to be compared *) |
|
1446 -> bool)) (*if t1 <= t2 then true else false *) |
|
1447 list); (*association list *) |
|
1448 |
|
1449 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), |
|
1450 ("dummy_ord", dummy_ord)]); |
|
1451 |
|
1452 |
|
1453 (*WN060120 a hack to get alltogether run again with minimal effort: |
|
1454 theory' is inserted for creating thy_hierarchy; calls for assoc_rls |
|
1455 need not be called*) |
|
1456 val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list); |
|
1457 |
|
1458 (*FIXME.040207 calclist': used by prep_rls, NOT in met*) |
|
1459 val calclist'= Unsynchronized.ref ([]: calc list); |
|
1460 |
|
1461 (*.the hierarchy of thydata.*) |
|
1462 |
|
1463 (*.'a is for pbt | met.*) |
|
1464 (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*) |
|
1465 datatype 'a ptyp = |
|
1466 Ptyp of string * (*element within pblID*) |
|
1467 'a list * (*several pbts with different domIDs/thy |
|
1468 TODO: select by subthy (isaref.p.69) |
|
1469 presently only _ONE_ elem*) |
|
1470 ('a ptyp) list; (*the children nodes*) |
|
1471 |
|
1472 (*.datatype for collecting thydata for hierarchy.*) |
|
1473 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*) |
|
1474 (*WN0606 Htxt contains html which does not belong to the sml-kernel*) |
|
1475 datatype thydata = Html of {guh: guh, |
|
1476 coursedesign: authors, |
|
1477 mathauthors: authors, |
|
1478 html: string} (*html; for demos before database*) |
|
1479 | Hthm of {guh: guh, |
|
1480 coursedesign: authors, |
|
1481 mathauthors: authors, |
|
1482 thm: term} |
|
1483 | Hrls of {guh: guh, |
|
1484 coursedesign: authors, |
|
1485 mathauthors: authors, |
|
1486 (*like vvvvvvvvvvvvv val ruleset' |
|
1487 WN060711 redesign together !*) |
|
1488 thy_rls: (thyID * rls)} |
|
1489 | Hcal of {guh: guh, |
|
1490 coursedesign: authors, |
|
1491 mathauthors: authors, |
|
1492 calc: calc} |
|
1493 | Hord of {guh: guh, |
|
1494 coursedesign: authors, |
|
1495 mathauthors: authors, |
|
1496 ord: (subst -> (term * term) -> bool)}; |
|
1497 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; |
|
1498 |
|
1499 type thehier = (thydata ptyp) list; |
|
1500 val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*) |
|
1501 |
|
1502 (* an association list, gets the value once in Isac.ML. |
|
1503 stores Isabelle's thms as terms for compatibility with Theory.axioms_of. |
|
1504 WN1-1-28 make this data arguments and del ref ?*) |
|
1505 val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list); |
|
1506 |
|
1507 |
|
1508 type path = string; |
|
1509 type filename = string; |
|
1510 |
|
1511 (*val xxx = fn: a b => (a,b); ??? fun-definition ???*) |
|
1512 local |
|
1513 fun ii (_:term) = e_rrlsstate; |
|
1514 fun no (_:term) = SOME (e_term,[e_term]); |
|
1515 fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))]; |
|
1516 fun ne (_:rule list list) (_:term) = SOME e_rule; |
|
1517 fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))]; |
|
1518 in |
|
1519 val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo, |
|
1520 next_rule=ne,attach_form=fo}; |
|
1521 end; |
|
1522 |
|
1523 val e_rls = |
|
1524 Rls{id = "e_rls", |
|
1525 preconds = [], |
|
1526 rew_ord = ("dummy_ord", dummy_ord), |
|
1527 erls = Erls,srls = Erls, |
|
1528 calc = [], |
|
1529 rules = [], scr = EmptyScr}:rls; |
|
1530 val e_rrls = Rrls {id = "e_rrls", |
|
1531 prepat = [], |
|
1532 rew_ord = ("dummy_ord", dummy_ord), |
|
1533 erls = Erls, |
|
1534 calc = [], |
|
1535 (*asm_thm=[],*) |
|
1536 scr=e_rfuns}:rls; |
|
1537 ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)), |
|
1538 ("e_rrls",("Tools",e_rrls)) |
|
1539 ]); |
|
1540 |
|
1541 fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = |
|
1542 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, |
|
1543 (*asm_thm=asm_thm,*)rules=rules,scr=scr} |
|
1544 | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) = |
|
1545 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, |
|
1546 (*asm_thm=asm_thm,*)rules=rules,scr=scr} |
|
1547 | rep_rls Erls = rep_rls e_rls |
|
1548 | rep_rls (Rrls {id,...}) = rep_rls e_rls |
|
1549 (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*); |
|
1550 (*| rep_rls (Seq {id,...}) = |
|
1551 error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id); |
|
1552 --1.7.03*) |
|
1553 fun rep_rrls |
|
1554 (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord, |
|
1555 scr=Rfuns |
|
1556 {attach_form,init_state,locate_rule, |
|
1557 next_rule,normal_form}}) = |
|
1558 {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat, |
|
1559 rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, |
|
1560 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form} |
|
1561 | rep_rrls (Rls {id,...}) = |
|
1562 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id) |
|
1563 | rep_rrls (Seq {id,...}) = |
|
1564 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id); |
|
1565 |
|
1566 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1567 rules =rs,scr=sc}) r = |
|
1568 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1569 rules = rs @ r,scr=sc}:rls) |
|
1570 | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1571 rules =rs,scr=sc}) r = |
|
1572 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1573 rules = rs @ r,scr=sc}:rls) |
|
1574 | append_rls id (Rrls _) _ = |
|
1575 error ("append_rls: not for reverse-rewrite-rule-set "^id); |
|
1576 |
|
1577 (*. are _atomic_ rules equal ?.*) |
|
1578 (*WN080102 compare eqrule ?!?*) |
|
1579 fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2 |
|
1580 | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2 |
|
1581 | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2 |
|
1582 (*id_rls checks for Rls, Seq, Rrls*) |
|
1583 | eq_rule _ = false; |
|
1584 |
|
1585 fun merge_rls _ Erls rls = rls |
|
1586 | merge_rls _ rls Erls = rls |
|
1587 | merge_rls id |
|
1588 (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, |
|
1589 (*asm_thm=at1,*)rules =rs1,scr=sc1}) |
|
1590 (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, |
|
1591 (*asm_thm=at2,*)rules =rs2,scr=sc2}) = |
|
1592 (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), |
|
1593 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), |
|
1594 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 |
|
1595 ((#srls o rep_rls) r2), |
|
1596 calc=ca1 @ ((#calc o rep_rls) r2), |
|
1597 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) |
|
1598 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), |
|
1599 scr=sc1}:rls) |
|
1600 | merge_rls id |
|
1601 (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, |
|
1602 (*asm_thm=at1,*)rules =rs1,scr=sc1}) |
|
1603 (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2, |
|
1604 (*asm_thm=at2,*)rules =rs2,scr=sc2}) = |
|
1605 (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), |
|
1606 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*), |
|
1607 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 |
|
1608 ((#srls o rep_rls) r2), |
|
1609 calc=ca1 @ ((#calc o rep_rls) r2), |
|
1610 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*) |
|
1611 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), |
|
1612 scr=sc1}:rls) |
|
1613 | merge_rls _ _ _ = |
|
1614 error "merge_rls: not for reverse-rewrite-rule-sets\ |
|
1615 \and not for mixed Rls -- Seq"; |
|
1616 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1617 (*asm_thm=at,*)rules =rs,scr=sc}) r = |
|
1618 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1619 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), |
|
1620 scr=sc}:rls) |
|
1621 | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1622 (*asm_thm=at,*)rules =rs,scr=sc}) r = |
|
1623 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
1624 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r), |
|
1625 scr=sc}:rls) |
|
1626 | remove_rls id (Rrls _) _ = error |
|
1627 ("remove_rls: not for reverse-rewrite-rule-set "^id); |
|
1628 |
|
1629 (*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]); |
|
1630 val it = [1, 2] : int list*) |
|
1631 |
|
1632 (*elder version: migrated 3 calls in smtest to memrls |
|
1633 fun mem_rls id rls = |
|
1634 case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of |
|
1635 SOME _ => true | NONE => false;*) |
|
1636 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules) |
|
1637 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules) |
|
1638 | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r)); |
|
1639 fun rls_get_thm rls (id: xstring) = |
|
1640 case find_first (curry eq_rule e_rule) |
|
1641 ((#rules o rep_rls) rls) of |
|
1642 SOME thm => SOME thm | NONE => NONE; |
|
1643 |
|
1644 fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known") |
|
1645 | assoc' ((keyi, xi) :: pairs, key) = |
|
1646 if key = keyi then SOME xi else assoc' (pairs, key); |
|
1647 |
|
1648 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) |
|
1649 handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*) |
|
1650 fun assoc_thy (thy:theory') = |
|
1651 if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*) |
|
1652 else (Thy_Info.get_theory thy) |
|
1653 handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system"); |
|
1654 |
|
1655 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; |
|
1656 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle |
|
1657 overlays by re-using an identifier in different thys.*) |
|
1658 fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls)) |
|
1659 handle _ => error ("ME_Isa: '"^rls^"' not in system"); |
|
1660 (*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls)) |
|
1661 handle _ => error ("ME_Isa: '"^rls^"' not in system");*) |
|
1662 |
|
1663 (*.overwrite an element in an association list and pair it with a thyID |
|
1664 in order to create the thy_hierarchy; |
|
1665 overwrites existing rls' even if they are defined in a different thy; |
|
1666 this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*) |
|
1667 (*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that |
|
1668 they do NOT handle overlays by re-using an identifier in different thys; |
|
1669 "thyID.rlsID" would be a good solution, if the "." would be possible |
|
1670 in scripts... |
|
1671 actually a hack to get alltogether run again with minimal effort*) |
|
1672 fun insthy thy' (rls', rls) = (rls', (thy', rls)); |
|
1673 fun overwritelthy thy (al, bl:(rls' * rls) list) = |
|
1674 let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl |
|
1675 in overwritel (al, bl') end; |
|
1676 |
|
1677 fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro)) |
|
1678 handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system"); |
|
1679 (*get the string for stac from rule*) |
|
1680 fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found") |
|
1681 | assoc_calc ((calc, (keyi, xi)) :: pairs, key) = |
|
1682 if key = keyi then calc else assoc_calc (pairs, key); |
|
1683 (*only used for !calclist'...*) |
|
1684 fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key |
|
1685 ^"' not found") |
|
1686 | assoc1 ((all as (keyi, _)) :: pairs, key) = |
|
1687 if key = keyi then all else assoc1 (pairs, key); |
|
1688 |
|
1689 (*TODO.WN080102 clarify usage of type cal and type calc..*) |
|
1690 fun calID2calcID (calID : calID) = |
|
1691 let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'") |
|
1692 | ass ((calci, (cali, eval_fn))::ids) = |
|
1693 if calID = cali then calci |
|
1694 else ass ids |
|
1695 in ass (!calclist') : calcID end; |
|
1696 |
|
1697 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term |
|
1698 (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; |
|
1699 |
|
1700 fun terms2str ts = (strs2str o (map term2str )) ts; |
|
1701 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*) |
|
1702 fun terms2str' ts = (strs2str' o (map term2str )) ts; |
|
1703 (*terms2str' [t1,t2] = "[1 + 2,abc]";*) |
|
1704 fun terms2strs ts = (map term2str) ts; |
|
1705 (*terms2strs [t1,t2] = ["1 + 2", "abc"];*) |
|
1706 |
|
1707 fun termopt2str (SOME t) = "SOME " ^ term2str t |
|
1708 | termopt2str NONE = "NONE"; |
|
1709 |
|
1710 fun type2str typ = |
|
1711 Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ; |
|
1712 val string_of_typ = type2str; |
|
1713 |
|
1714 fun subst2str (s:subst) = |
|
1715 (strs2str o |
|
1716 (map (linefeed o pair2str o |
|
1717 (apsnd term2str) o |
|
1718 (apfst term2str)))) s; |
|
1719 fun subst2str' (s:subst) = |
|
1720 (strs2str' o |
|
1721 (map (pair2str o |
|
1722 (apsnd term2str) o |
|
1723 (apfst term2str)))) s; |
|
1724 (*> subst2str' [(str2term "bdv", str2term "x"), |
|
1725 (str2term "bdv_2", str2term "y")]; |
|
1726 val it = "[(bdv, x)]" : string |
|
1727 *) |
|
1728 val env2str = subst2str; |
|
1729 |
|
1730 |
|
1731 (*recursive defs:*) |
|
1732 fun scr2str (Script s) = "Script "^(term2str s) |
|
1733 | scr2str (Rfuns _) = "Rfuns"; |
|
1734 |
|
1735 |
|
1736 fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1; |
|
1737 |
|
1738 |
|
1739 (*.trace internal steps of isac's rewriter*) |
|
1740 val trace_rewrite = Unsynchronized.ref false; |
|
1741 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) |
|
1742 val depth = Unsynchronized.ref 99999; |
|
1743 (*.no of rewrites exceeding this int -> NO rewrite.*) |
|
1744 (*WN060829 still unused...*) |
|
1745 val lim_rewrite = Unsynchronized.ref 99999; |
|
1746 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*) |
|
1747 val lim_deriv = Unsynchronized.ref 100; |
|
1748 (*.switch for checking guhs unique before storing a pbl or met; |
|
1749 set true at startup (done at begin of ROOT.ML) |
|
1750 set false for editing IsacKnowledge (done at end of ROOT.ML).*) |
|
1751 val check_guhs_unique = Unsynchronized.ref false; |
|
1752 |
|
1753 |
|
1754 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) |
|
1755 L (*go left at $*) |
|
1756 | R (*go right at $*) |
|
1757 | D; (*go down at Abs*) |
|
1758 type loc_ = lrd list; |
|
1759 fun ldr2str L = "L" |
|
1760 | ldr2str R = "R" |
|
1761 | ldr2str D = "D"; |
|
1762 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k; |
|
1763 |
|
1764 (* |
|
1765 end (*struct*) |
|
1766 *) |
|