7 sig |
7 sig |
8 type calcstate |
8 type calcstate |
9 type calcstate' |
9 type calcstate' |
10 datatype appl = Appl of Ctree.tac_ | Notappl of string |
10 datatype appl = Appl of Ctree.tac_ | Notappl of string |
11 val nxt_specify_init_calc : Ctree.fmz -> calcstate |
11 val nxt_specify_init_calc : Ctree.fmz -> calcstate |
12 val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree -> |
12 val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> |
13 Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree |
13 Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree |
14 val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate' |
14 val nxt_specif : Ctree.tac -> Ctree.ctree * Ctree.pos' -> calcstate' |
15 val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list -> |
15 val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list -> |
16 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac |
16 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac |
17 |
17 |
18 val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
18 val reset_calchead : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
19 val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd |
19 val get_ocalhd : Ctree.ctree * Ctree.pos' -> Ctree.ocalhd |
20 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool |
20 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool |
21 val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
21 val all_modspec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
22 |
22 |
23 val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list |
23 val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list |
24 val insert_ppc' : itm -> itm list -> itm list |
24 val insert_ppc' : itm -> itm list -> itm list |
25 |
25 |
26 val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
26 val complete_mod : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
27 val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool |
27 val is_complete_mod : Ctree.ctree * Ctree.pos' -> bool |
28 val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
28 val complete_spec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
29 val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool |
29 val is_complete_spec : Ctree.ctree * Ctree.pos' -> bool |
30 val some_spec : spec -> spec -> spec |
30 val some_spec : spec -> spec -> spec |
31 (* these could go to Ctree ..*) |
31 (* these could go to Ctree ..*) |
32 val show_pt : Ctree.ptree -> unit |
32 val show_pt : Ctree.ctree -> unit |
33 val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list |
33 val pt_extract : Ctree.ctree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list |
34 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list |
34 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list |
35 |
35 |
36 val match_ags : theory -> pat list -> term list -> ori list |
36 val match_ags : theory -> pat list -> term list -> ori list |
37 val match_ags_msg : pblID -> term -> term list -> unit |
37 val match_ags_msg : pblID -> term -> term list -> unit |
38 val oris2fmz_vals : ori list -> string list * term list |
38 val oris2fmz_vals : ori list -> string list * term list |
39 val vars_of_pbl_' : ('a * ('b * term)) list -> term list |
39 val vars_of_pbl_' : ('a * ('b * term)) list -> term list |
66 the calc-state resulting from the application of tacis is not stored, |
66 the calc-state resulting from the application of tacis is not stored, |
67 because the tacis hold enough information for efficiently rebuilding |
67 because the tacis hold enough information for efficiently rebuilding |
68 this state just by "fun generate " |
68 this state just by "fun generate " |
69 *) |
69 *) |
70 type calcstate = |
70 type calcstate = |
71 (ptree * pos') * (* the calc-state to which the tacis could be applied *) |
71 (ctree * pos') * (* the calc-state to which the tacis could be applied *) |
72 (Generate.taci list) (* ev. several (hidden) steps; |
72 (Generate.taci list) (* ev. several (hidden) steps; |
73 in REVERSE order: first tac_ to apply is last_elem *) |
73 in REVERSE order: first tac_ to apply is last_elem *) |
74 val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate; |
74 val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate; |
75 |
75 |
76 (*the state used during one calculation within the mathengine; it contains |
76 (*the state used during one calculation within the mathengine; it contains |
84 this state just by "fun generate ".*) |
84 this state just by "fun generate ".*) |
85 type calcstate' = |
85 type calcstate' = |
86 Generate.taci list * (* cas. several (hidden) steps; |
86 Generate.taci list * (* cas. several (hidden) steps; |
87 in REVERSE order: first tac_ to apply is last_elem *) |
87 in REVERSE order: first tac_ to apply is last_elem *) |
88 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *) |
88 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *) |
89 (ptree * pos') (* the calc-state resulting from the application of tacis *) |
89 (ctree * pos') (* the calc-state resulting from the application of tacis *) |
90 val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate'; |
90 val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate'; |
91 |
91 |
92 (* FIXXXME.WN020430 intermediate hack for fun ass_up *) |
92 (* FIXXXME.WN020430 intermediate hack for fun ass_up *) |
93 fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f |
93 fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f |
94 | f_mout _ _ = error "f_mout: not called with formula"; |
94 | f_mout _ _ = error "f_mout: not called with formula"; |
695 val thy = assoc_thy dI' |
695 val thy = assoc_thy dI' |
696 val (oris, ctxt) = |
696 val (oris, ctxt) = |
697 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*) |
697 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*) |
698 then ([], e_ctxt) |
698 then ([], e_ctxt) |
699 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy |
699 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy |
700 val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec') |
700 val (pt, _) = cappend_problem e_ctree [] (e_istate, ctxt) (fmz, spec') |
701 (oris, (dI',pI',mI'), e_term) |
701 (oris, (dI',pI',mI'), e_term) |
702 val pt = update_ctxt pt [] ctxt |
702 val pt = update_ctxt pt [] ctxt |
703 val (pbl, pre) = ([], []) |
703 val (pbl, pre) = ([], []) |
704 in |
704 in |
705 case mI' of |
705 case mI' of |
949 fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) = |
949 fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) = |
950 (if dI = e_domID then odI else dI, |
950 (if dI = e_domID then odI else dI, |
951 if pI = e_pblID then opI else pI, |
951 if pI = e_pblID then opI else pI, |
952 if mI = e_metID then omI else mI) : spec |
952 if mI = e_metID then omI else mI) : spec |
953 |
953 |
954 (* find a next applicable tac (for calcstate) and update ptree |
954 (* find a next applicable tac (for calcstate) and update ctree |
955 (for ev. finding several more tacs due to hide) *) |
955 (for ev. finding several more tacs due to hide) *) |
956 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *) |
956 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *) |
957 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *) |
957 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *) |
958 (* WN.24.10.03 fun nxt_solv = ...................................?? *) |
958 (* WN.24.10.03 fun nxt_solv = ...................................?? *) |
959 fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) = |
959 fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) = |
1085 let |
1085 let |
1086 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI |
1086 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI |
1087 val dI = if dI = "" then theory2theory' thy else dI |
1087 val dI = if dI = "" then theory2theory' thy else dI |
1088 val mI = if mI = [] then hd met else mI |
1088 val mI = if mI = [] then hd met else mI |
1089 val hdl = case cas of NONE => pblterm dI pI | SOME t => t |
1089 val hdl = case cas of NONE => pblterm dI pI | SOME t => t |
1090 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI)) |
1090 val (pt,_) = cappend_problem e_ctree [] (Uistate, e_ctxt) ([], (dI, pI, mI)) |
1091 ([], (dI,pI,mI), hdl) |
1091 ([], (dI,pI,mI), hdl) |
1092 val pt = update_spec pt [] (dI, pI, mI) |
1092 val pt = update_spec pt [] (dI, pI, mI) |
1093 val pits = Generate.init_pbl' ppc |
1093 val pits = Generate.init_pbl' ppc |
1094 val pt = update_pbl pt [] pits |
1094 val pt = update_pbl pt [] pits |
1095 in ((pt, ([] , Pbl)), []) : calcstate end |
1095 in ((pt, ([] , Pbl)), []) : calcstate end |
1098 then (* from met-browser *) |
1098 then (* from met-browser *) |
1099 let |
1099 let |
1100 val {ppc, ...} = Specify.get_met mI |
1100 val {ppc, ...} = Specify.get_met mI |
1101 val dI = if dI = "" then "Isac" else dI |
1101 val dI = if dI = "" then "Isac" else dI |
1102 val (pt, _) = |
1102 val (pt, _) = |
1103 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*)) |
1103 cappend_problem e_ctree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*)) |
1104 val pt = update_spec pt [] (dI, pI, mI) |
1104 val pt = update_spec pt [] (dI, pI, mI) |
1105 val mits = Generate.init_pbl' ppc |
1105 val mits = Generate.init_pbl' ppc |
1106 val pt = update_met pt [] mits |
1106 val pt = update_met pt [] mits |
1107 in ((pt, ([], Met)), []) end |
1107 in ((pt, ([], Met)), []) end |
1108 else (* new example, pepare for interactive modeling *) |
1108 else (* new example, pepare for interactive modeling *) |
1109 let |
1109 let |
1110 val (pt, _) = |
1110 val (pt, _) = |
1111 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term) |
1111 cappend_problem e_ctree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term) |
1112 in ((pt, ([], Pbl)), []) end |
1112 in ((pt, ([], Pbl)), []) end |
1113 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = |
1113 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = |
1114 let (* both """"""""""""""""""""""""" either empty or complete *) |
1114 let (* both """"""""""""""""""""""""" either empty or complete *) |
1115 val thy = assoc_thy dI |
1115 val thy = assoc_thy dI |
1116 val (pI, (pors, pctxt), mI) = |
1116 val (pI, (pors, pctxt), mI) = |
1127 val dI = theory2theory' (maxthy thy thy') |
1127 val dI = theory2theory' (maxthy thy thy') |
1128 val hdl = case cas of |
1128 val hdl = case cas of |
1129 NONE => pblterm dI pI |
1129 NONE => pblterm dI pI |
1130 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t |
1130 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t |
1131 val (pt, _) = |
1131 val (pt, _) = |
1132 cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) |
1132 cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) |
1133 val pt = update_ctxt pt [] pctxt |
1133 val pt = update_ctxt pt [] pctxt |
1134 in |
1134 in |
1135 ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate |
1135 ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate |
1136 end |
1136 end |
1137 |
1137 |
1394 then get_formress (fs @ [formres p nd]) (lev_on p) nds *) |
1394 then get_formress (fs @ [formres p nd]) (lev_on p) nds *) |
1395 then get_forms (fs @ [formres p nd]) (lev_on p) nds |
1395 then get_forms (fs @ [formres p nd]) (lev_on p) nds |
1396 (* continue with trying 'res' only*) |
1396 (* continue with trying 'res' only*) |
1397 else get_forms (fs @ [form p nd]) (lev_on p) nds; |
1397 else get_forms (fs @ [form p nd]) (lev_on p) nds; |
1398 |
1398 |
1399 (** get an 'interval' 'from' 'to' of formulae from a ptree **) |
1399 (** get an 'interval' 'from' 'to' of formulae from a ctree **) |
1400 (* WN0401 this functionality belongs to ctree.sml *) |
1400 (* WN0401 this functionality belongs to ctree.sml *) |
1401 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2 |
1401 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2 |
1402 | eq_pos' (p1, Res) (p2, Res) = p1 = p2 |
1402 | eq_pos' (p1, Res) (p2, Res) = p1 = p2 |
1403 | eq_pos' (p1, Pbl) (p2, p2_) = |
1403 | eq_pos' (p1, Pbl) (p2, p2_) = |
1404 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false) |
1404 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false) |
1411 val get_interval = fn |
1411 val get_interval = fn |
1412 : pos' -> : from is "move_up 1st-element" to return |
1412 : pos' -> : from is "move_up 1st-element" to return |
1413 pos' -> : to the last element to be returned; from < to |
1413 pos' -> : to the last element to be returned; from < to |
1414 int -> : level: 0 gets the flattest sub-tree possible |
1414 int -> : level: 0 gets the flattest sub-tree possible |
1415 >999 gets the deepest sub-tree possible |
1415 >999 gets the deepest sub-tree possible |
1416 ptree -> : |
1416 ctree -> : |
1417 (pos' * : of the formula |
1417 (pos' * : of the formula |
1418 Term.term) : the formula |
1418 Term.term) : the formula |
1419 list *) |
1419 list *) |
1420 fun get_interval from to level pt = |
1420 fun get_interval from to level pt = |
1421 let |
1421 let |