wneuper/isa: comparison src/Tools/isac/Specify/step-specify.sml

equal deleted inserted replaced

-:273ffde50058
+:7184a26ac7d5
 NONE => (pbl, [])
 		| _ => complete_mod_ (oris, mpc, ppc, probl)
 (*----------------------------------------------------------------*)
 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
 val (pos,c,_,pt) = Generate.generate1 tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
-in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end
+in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)) end
 | by_tactic_input (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
 | by_tactic_input (Tactic.Add_Find  ct) ptp = nxt_specif_additem "#Find"  ct ptp
 | by_tactic_input (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
 (*. called only if no_met is specified .*)
 | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =
 val thy = Celem.assoc_thy dI
 	          val (pos, c, _, pt) =
 		          Generate.generate1 (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
 	        in
 	          ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
-	              (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
+	              (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))
 end
 	    | NONE => ([], [], ptp)
 end
 | by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
 let
 	      NONE => ([], [], ptp)
 	    | SOME rfd =>
 	      let
 val (pos,c,_,pt) = Generate.generate1 (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
 	      in
-	        ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
+	        ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))
 end
 end
 | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =
 let
 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
 	    val (c, pt) =
 	      case Generate.generate1 (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
 	      ((_, Pbl), c, _, pt) => (c, pt)
 	    | _ => error ""
 in
-([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
+([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))
 end
 (* transfers oris (not required in pbl) to met-model for script-env
 FIXME.WN.8.03: application of several mIDs to SAME model?       *)
 | by_tactic_input (Tactic.Specify_Method mID) (pt, pos as (p,_)) =
 let
 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
 val itms = Specify.hack_until_review_Specify_2 mID itms
 val (pos, c, _, pt) =
 	      Generate.generate1 (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
 in
-([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
+([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))
 end
 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
 let
 val ctxt = get_ctxt pt pos
 	    val (pos, c, _, pt) =
 val ctxt = get_ctxt pt pos
 	    val (pos, c, _, pt) = Generate.generate1 (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
 in  (*FIXXXME: check if met can still be parsed*)
 	    ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))
 end
-| by_tactic_input m' _ = error ("by_tactic_input: not impl. for " ^ Tactic.tac2str m')
+| by_tactic_input m' _ = error ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')
 (* was fun Math_Engine.nxt_specify_ *)
 (* was fun Chead.specify *)
 fun by_tactic (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ =
 let          (* either """"""""""""""" all empty or complete *)
 val thy = Celem.assoc_thy dI'
 val (oris, ctxt) =
 if dI' = Rule.e_domID orelse pI' = Celem.e_pblID  (*andalso? WN110511*)
-then ([], ContextC.e_ctxt)
+then ([], ContextC.empty)
 	    else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
 (* these are deprecated                vvvvvvvvvvvvvvvvvvvvvvvvvv*)
-val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) (fmz, spec')
+val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) (fmz, spec')
 			(oris, (dI',pI',mI'), Rule.e_term, ctxt)
-val pt = update_loc' pt [] (SOME (Istate_Def.e_istate, ctxt), NONE)
+val pt = update_loc' pt [] (SOME (Istate_Def.empty, ctxt), NONE)
 in
 case mI' of
 	    ["no_met"] => ("Refine_Tacitly", ([], [], (pt, ([], Pbl))))
 | _ => ("ok", ([], [], (pt, ([], Pbl))))
 end
 | _ => error "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
 val {met, thy,...} = Specify.get_pbt pIre
 val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
 val ((p,_), _, _, pt) =
 	        Generate.generate1 (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
-(Istate_Def.Uistate, ContextC.e_ctxt) (pt, pos)
+(Istate_Def.Uistate, ContextC.empty) (pt, pos)
 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
 (*     val (pbl, pre, _) = ([], [], false)*)
 in
 ("ok", ([], [], (pt,(p, Pbl))))
 end
 	    let
 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
 	      val dI = if dI = "" then Rule.theory2theory' thy else dI
 	      val mI = if mI = [] then hd met else mI
 	      val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
-	      val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
+	      val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
-				  ([], (dI,pI,mI), hdl, ContextC.e_ctxt)
+				  ([], (dI,pI,mI), hdl, ContextC.empty)
 	      val pt = update_spec pt [] (dI, pI, mI)
 	      val pits = Generate.init_pbl' ppc
 	      val pt = update_pbl pt [] pits
 	    in ((pt, ([] , Pbl)), []) end
 else
 if mI <> []
 then (* from met-browser *)
 	      let
 val {ppc, ...} = Specify.get_met mI
 	        val dI = if dI = "" then "Isac_Knowledge" else dI
-	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt)
+	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
-	          ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term, ContextC.e_ctxt)
+	          ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term, ContextC.empty)
 	        val pt = update_spec pt [] (dI, pI, mI)
 	        val mits = Generate.init_pbl' ppc
 	        val pt = update_met pt [] mits
 	      in ((pt, ([], Met)), []) end
 else (* new example, pepare for interactive modeling *)
 	      let
-	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt)
+	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
-	          ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.e_ctxt)
+	          ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.empty)
 	      in ((pt, ([], Pbl)), []) end
 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
 let           (* both """"""""""""""""""""""""" either empty or complete *)
 	    val thy = Celem.assoc_thy dI
 	    val (pI, (pors, pctxt), mI) =
 	    val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
 	    val dI = Rule.theory2theory' (Stool.common_subthy (thy, thy'))
 	    val hdl = case cas of
 		    NONE => Auto_Prog.pblterm dI pI
 		  | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
-val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, pctxt)
+val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
 (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
 in
 ((pt, ([], Pbl)), fst3 (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
 end

changeset 59846	7184a26ac7d5
parent 59819	74ad911c10b9
child 59854	c20d08e01ad2