69 type calcstate |
69 type calcstate |
70 type calcstate' |
70 type calcstate' |
71 datatype appl = Appl of Tactic.T | Notappl of string |
71 datatype appl = Appl of Tactic.T | Notappl of string |
72 val nxt_specify_init_calc : Selem.fmz -> calcstate |
72 val nxt_specify_init_calc : Selem.fmz -> calcstate |
73 val specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> |
73 val specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> |
74 Ctree.pos' * (Ctree.pos' * Istate.T) * Generate.mout * Tactic.input * Istate.safe * Ctree.ctree |
74 Ctree.pos' * (Ctree.pos' * Istate.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree |
75 val nxt_specif : Tactic.input -> Ctree.state -> calcstate' |
75 val nxt_specif : Tactic.input -> Ctree.state -> calcstate' |
76 val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list -> |
76 val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list -> |
77 (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input |
77 (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input |
78 |
78 |
79 val reset_calchead : Ctree.state -> Ctree.state |
79 val reset_calchead : Ctree.state -> Ctree.state |
707 val pb = foldl and_ (true, map fst pre') |
707 val pb = foldl and_ (true, map fst pre') |
708 val (p_, nxt) = |
708 val (p_, nxt) = |
709 nxt_spec Met pb oris (dI',pI',mI') (pbl,met') |
709 nxt_spec Met pb oris (dI',pI',mI') (pbl,met') |
710 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI); |
710 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI); |
711 in ((p, p_), ((p, p_), Istate.Uistate), |
711 in ((p, p_), ((p, p_), Istate.Uistate), |
712 Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Istate.Safe, pt') |
712 Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Telem.Safe, pt') |
713 end |
713 end |
714 | Err msg => |
714 | Err msg => |
715 let |
715 let |
716 val pre' = Stool.check_preconds thy prls pre met |
716 val pre' = Stool.check_preconds thy prls pre met |
717 val pb = foldl and_ (true, map fst pre') |
717 val pb = foldl and_ (true, map fst pre') |
718 val (p_, nxt) = |
718 val (p_, nxt) = |
719 nxt_spec Met pb oris (dI',pI',mI') (pbl,met) |
719 nxt_spec Met pb oris (dI',pI',mI') (pbl,met) |
720 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI); |
720 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI); |
721 in ((p,p_), ((p,p_),Istate.Uistate), Generate.Error' msg, nxt, Istate.Safe, pt) end |
721 in ((p,p_), ((p,p_),Istate.Uistate), Generate.Error' msg, nxt, Telem.Safe, pt) end |
722 end |
722 end |
723 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt = |
723 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt = |
724 let |
724 let |
725 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of |
725 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of |
726 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...}) |
726 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...}) |
748 val (p_, nxt) = |
748 val (p_, nxt) = |
749 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) |
749 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) |
750 val ppc = if p_= Pbl then pbl' else met |
750 val ppc = if p_= Pbl then pbl' else met |
751 in |
751 in |
752 ((p, p_), ((p, p_), Istate.Uistate), |
752 ((p, p_), ((p, p_), Istate.Uistate), |
753 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Istate.Safe, pt') |
753 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Telem.Safe, pt') |
754 end |
754 end |
755 | Err msg => |
755 | Err msg => |
756 let |
756 let |
757 val pre = Stool.check_preconds thy prls where_ pbl |
757 val pre = Stool.check_preconds thy prls where_ pbl |
758 val pb = foldl and_ (true, map fst pre) |
758 val pb = foldl and_ (true, map fst pre) |
759 val (p_, nxt) = |
759 val (p_, nxt) = |
760 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) |
760 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) |
761 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) |
761 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) |
762 in ((p, p_), ((p, p_), Istate.Uistate), Generate.Error' msg, nxt, Istate.Safe,pt) end |
762 in ((p, p_), ((p, p_), Istate.Uistate), Generate.Error' msg, nxt, Telem.Safe,pt) end |
763 end |
763 end |
764 |
764 |
765 fun specify (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ = |
765 fun specify (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ = |
766 let (* either """"""""""""""" all empty or complete *) |
766 let (* either """"""""""""""" all empty or complete *) |
767 val thy = Celem.assoc_thy dI' |
767 val thy = Celem.assoc_thy dI' |
776 in |
776 in |
777 case mI' of |
777 case mI' of |
778 ["no_met"] => |
778 ["no_met"] => |
779 (([], Pbl), (([], Pbl), Istate.Uistate), |
779 (([], Pbl), (([], Pbl), Istate.Uistate), |
780 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
780 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
781 Tactic.Refine_Tacitly pI', Istate.Safe, pt) |
781 Tactic.Refine_Tacitly pI', Telem.Safe, pt) |
782 | _ => |
782 | _ => |
783 (([], Pbl), (([], Pbl), Istate.Uistate), |
783 (([], Pbl), (([], Pbl), Istate.Uistate), |
784 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
784 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
785 Tactic.Model_Problem, Istate.Safe, pt) |
785 Tactic.Model_Problem, Telem.Safe, pt) |
786 end |
786 end |
787 (* ONLY for STARTING modeling phase *) |
787 (* ONLY for STARTING modeling phase *) |
788 | specify (Tactic.Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt = |
788 | specify (Tactic.Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt = |
789 let |
789 let |
790 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of |
790 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of |
801 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) |
801 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) |
802 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI'); |
802 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI'); |
803 in |
803 in |
804 ((p, Pbl), ((p, p_), Istate.Uistate), |
804 ((p, Pbl), ((p, p_), Istate.Uistate), |
805 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
805 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
806 nxt, Istate.Safe, pt) |
806 nxt, Telem.Safe, pt) |
807 end |
807 end |
808 (* called only if no_met is specified *) |
808 (* called only if no_met is specified *) |
809 | specify (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt = |
809 | specify (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt = |
810 let |
810 let |
811 val (dI', ctxt) = case get_obj I pt p of |
811 val (dI', ctxt) = case get_obj I pt p of |
816 val ((p,_), _, _, pt) = |
816 val ((p,_), _, _, pt) = |
817 Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Istate.Uistate, ctxt) pos pt |
817 Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Istate.Uistate, ctxt) pos pt |
818 val (pbl, pre, _) = ([], [], false) |
818 val (pbl, pre, _) = ([], [], false) |
819 in ((p, Pbl), (pos, Istate.Uistate), |
819 in ((p, Pbl), (pos, Istate.Uistate), |
820 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
820 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre), |
821 Tactic.Model_Problem, Istate.Safe, pt) |
821 Tactic.Model_Problem, Telem.Safe, pt) |
822 end |
822 end |
823 | specify (Tactic.Refine_Problem' rfd) pos _ pt = |
823 | specify (Tactic.Refine_Problem' rfd) pos _ pt = |
824 let |
824 let |
825 val ctxt = get_ctxt pt pos |
825 val ctxt = get_ctxt pt pos |
826 val (pos, _, _, pt) = |
826 val (pos, _, _, pt) = |
827 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt |
827 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt |
828 in |
828 in |
829 (pos(*p,Pbl*), (pos(*p,Pbl*), Istate.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Istate.Safe, pt) |
829 (pos(*p,Pbl*), (pos(*p,Pbl*), Istate.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Telem.Safe, pt) |
830 end |
830 end |
831 (*WN110515 initialise ctxt again from itms and add preconds*) |
831 (*WN110515 initialise ctxt again from itms and add preconds*) |
832 | specify (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt = |
832 | specify (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt = |
833 let |
833 let |
834 val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of |
834 val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of |
845 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI, |
845 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI, |
846 (#ppc o Specify.get_met) mI'') (dI, pI, mI); |
846 (#ppc o Specify.get_met) mI'') (dI, pI, mI); |
847 in |
847 in |
848 ((p,Pbl), (pos,Istate.Uistate), |
848 ((p,Pbl), (pos,Istate.Uistate), |
849 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre), |
849 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre), |
850 nxt, Istate.Safe, pt) |
850 nxt, Telem.Safe, pt) |
851 end |
851 end |
852 (*WN110515 initialise ctxt again from itms and add preconds*) |
852 (*WN110515 initialise ctxt again from itms and add preconds*) |
853 | specify (Tactic.Specify_Method' (mID, _, _)) (pos as (p, _)) _ pt = |
853 | specify (Tactic.Specify_Method' (mID, _, _)) (pos as (p, _)) _ pt = |
854 let |
854 let |
855 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of |
855 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of |
882 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms) |
882 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms) |
883 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID) |
883 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID) |
884 in |
884 in |
885 (pos, (pos,Istate.Uistate), |
885 (pos, (pos,Istate.Uistate), |
886 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (Celem.assoc_thy dI'') itms pre'), |
886 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (Celem.assoc_thy dI'') itms pre'), |
887 nxt, Istate.Safe, pt) |
887 nxt, Telem.Safe, pt) |
888 end |
888 end |
889 | specify (Tactic.Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt |
889 | specify (Tactic.Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt |
890 | specify (Tactic.Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt |
890 | specify (Tactic.Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt |
891 | specify (Tactic.Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt |
891 | specify (Tactic.Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt |
892 | specify (Tactic.Specify_Theory' domID) (pos as (p,p_)) _ pt = |
892 | specify (Tactic.Specify_Theory' domID) (pos as (p,p_)) _ pt = |
911 then |
911 then |
912 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI) |
912 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI) |
913 in |
913 in |
914 ((p, p_), (pos, Istate.Uistate), |
914 ((p, p_), (pos, Istate.Uistate), |
915 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre), |
915 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre), |
916 nxt, Istate.Safe, pt) |
916 nxt, Telem.Safe, pt) |
917 end |
917 end |
918 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*) |
918 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*) |
919 let |
919 let |
920 val ((p, p_), _, _, pt) = Generate.generate1 thy (Tactic.Specify_Theory' domID) (Istate.Uistate, ctxt) (p,p_) pt |
920 val ((p, p_), _, _, pt) = Generate.generate1 thy (Tactic.Specify_Theory' domID) (Istate.Uistate, ctxt) (p,p_) pt |
921 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI) |
921 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI) |
922 in |
922 in |
923 ((p,p_), (pos,Istate.Uistate), |
923 ((p,p_), (pos,Istate.Uistate), |
924 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre), |
924 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre), |
925 nxt, Istate.Safe, pt) |
925 nxt, Telem.Safe, pt) |
926 end |
926 end |
927 end |
927 end |
928 | specify m' _ _ _ = error ("specify: not impl. for " ^ Tactic.tac_2str m') |
928 | specify m' _ _ _ = error ("specify: not impl. for " ^ Tactic.tac_2str m') |
929 |
929 |
930 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...} |
930 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...} |