wneuper/isa: comparison src/Tools/isac/Specify/i-model.sml

equal deleted inserted replaced

-:1b072aab8f4e
+:ac0317936138
 val single_to_string_POS': single_POS -> string
 val to_string: Proof.context -> T -> string
 val to_string_POS: Proof.context -> T_POS -> string
 val feedback_OLD_to_POS: feedback -> feedback_POS
+val feedback_POS_to_OLD: feedback_POS -> feedback
-datatype add_single = Add of single | Err of string
+val OLD_to_POS_single: single -> single_POS
+val TEST_to_OLD_single: single_POS -> single
+datatype add_single = Add of single_POS | Err of string
 val init: Model_Pattern.T -> T
 val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
 TermC.as_string -> add_single
+(*probably unused in PIDE, thus-----v----v*)
 val add_single: theory -> single -> T -> T
 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
-(*--*)
 val descriptor: feedback -> descriptor
-(*--*)
 val descriptor_POS: feedback_POS -> descriptor
 val values: feedback -> values option
 val o_model_values: feedback -> values
 val values_POS': feedback_POS -> values
 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_POS) list -> string
 val variables: Model_Pattern.T -> Model_Def.i_model_POS -> term list
-val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
+val is_notyet_input: Proof.context -> T_POS -> O_Model.values -> O_Model.single ->
--> message * single
+Model_Pattern.T -> message * single_POS
 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
 val fill_from_o: O_Model.T -> single_POS -> single_POS option
 val add_other: variant -> T_POS -> single_POS -> single_POS
 (*/----- from isac_test for Minisubpbl*)
 val msg: variants -> feedback_POS -> string
 val transfer_terms: O_Model.single -> single_POS
-val eq1: ''a -> 'b * (''a * 'c) -> bool
 val feedback_to_string: Proof.context -> feedback -> string
 val feedback_POS_to_string: Proof.context -> feedback_POS -> string
 val descr_vals_to_string: Proof.context -> descriptor * values -> string
 val feedb_args_to_string: Proof.context -> feedback_POS -> string
-val ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> single
+val ori_2itm: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> single_POS
 val seek_ppc: int -> T -> single option
 val overwrite_ppc: theory -> single -> T -> T
 (*\----- from isac_test for Minisubpbl*)
 \<^isac_test>\<open>
-(**)
+(*copy "from isac_test for Minisubpbl" here*)
 \<close>
 end
 | feedback_OLD_to_POS (Inc ((d, ts), _)) = (Model_Def.Inc_POS (d, ts))
 | feedback_OLD_to_POS (Sup (d, ts)) = (Model_Def.Sup_POS (d, ts))
 | feedback_OLD_to_POS (Mis (d, pid)) = Model_Def.Syn_POS ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
 (UnparseC.term (ContextC.for_ERROR ()) pid))
 | feedback_OLD_to_POS (Par s) = (Model_Def.Syn_POS s)
-fun OLD_to_POS i_old =
+fun OLD_to_POS_single (a, b, c, d, e) = (a, b, c, d, (feedback_OLD_to_POS e, Position.none))
-map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_POS e, Position.none))) i_old
+fun OLD_to_POS i_old = map OLD_to_POS_single i_old
 fun feedback_POS_to_OLD (Model_Def.Cor_POS (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
 | feedback_POS_to_OLD (Model_Def.Syn_POS c) = (Syn c)
 | feedback_POS_to_OLD (Model_Def.Inc_POS (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
 | feedback_POS_to_OLD (Model_Def.Sup_POS (d, ts)) = (Sup (d, ts))
-fun TEST_to_OLD i_model =
+fun TEST_to_OLD_single (a, b, c, d, (e, _)) = (a, b, c, d, feedback_POS_to_OLD e)
-map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_POS_to_OLD e)) i_model
+fun TEST_to_OLD i_model = map TEST_to_OLD_single i_model
 type message = string;
 fun feedback_to_string ctxt (Cor ((d, ts), _)) =
 "Cor " ^ UnparseC.term  ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
 fun variables model_patt i_model =
 Pre_Conds.environment_POS model_patt i_model
 |> map snd
+(*
 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
+*)
 (* get a term from O_Model, notyet input in I_Model.
 the term from O_Model is thrown back to a string in order to reuse
 machinery for immediate input by the user. *)
 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
 (*update the itm_ already input, all..from ori*)
-fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
+fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) =
 let
-val ts' = union op = (o_model_values itm_) ts;
+val ts' = union op = (values_POS' feedb) ts;
-val pval = [Input_Descript.join'''' (d, ts')]
-	  (*WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc*)
 val complete = if eq_set op = (ts', all) then true else false
 in
-case itm_ of
+case feedb of
-(Cor _) =>
+Cor_POS _ => if fd = "#undef"
-(if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
+then (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
-	       else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
+	    else (id, vt, complete, fd, (Cor_POS (d, ts'), Position.none))
-| (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
+| Inc_POS _ => if complete
-| (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
+	  then (id, vt, true,  fd, (Cor_POS (d, ts'), Position.none))
-| (Inc _) =>
+	  else (id, vt, false, fd, (Inc_POS (d, ts'), Position.none))
-if complete
+| Sup_POS (d, ts') =>
-	  then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
+	  (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
-	  else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
+| i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)
-| (Sup (d,ts')) => (*4.9.01 lost env*)
-	  (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
-	  (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
-(* 28.1.00: not completely clear ---^^^ etc.*)
-| (Mis _) => (* 4.9.01: Mis just copied *)
-if complete
-		 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
-		 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
-| i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string (ContextC.for_ERROR ()) i)
 end
 (** find next step **)
-fun eq1 d (_, (d', _)) = (d = d')
+(*old code kept for test/*)
-fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
-case find_first (eq1 d) pbt of
+case find_first (fn (_, (d', _)) => d = d') pbt of
 SOME (_, (_, pid)) =>
-(case find_first (eq3 f d) itms of
+(case find_first (fn (_, _, _, f', (feedb, _)) =>
-SOME (_, _, _, _, itm_) =>
+f = f' andalso d = (descriptor_POS feedb)) itms of
-let val ts' = inter op = (o_model_values itm_) ts
+SOME (_, _, _, _, (feedb, _)) =>
-in
+let val ts' = inter op = (values_POS' feedb) ts
+in
 if subset op = (ts, ts')
-then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
+then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
-	          else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
+	          else ("", ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts))
-	          end
+	        end
-	    | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
+	    | NONE => ("", ori_2itm (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))
-| NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
+| NONE => ("", ori_2itm (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))
 datatype add_single =
-	Add of single   (* return-value of check_single *)
+	Add of single_POS   (* return-value of check_single *)
 | Err of string   (* error-message                *)
 (*
 Create feedback for input of TermC.as_string to m_field;
 check w.r.t. O_Model.T and Model_Pattern.T.
 val t = Syntax.read_term ctxt ct
 handle ERROR msg => error (msg (*^ Position.here pos*))
 (*\------------ replace by ParseC.term_position -----------/*)
 (*NONE => Add (i, [], false, m_field, Syn ct)*)
 val (d, ts) = Input_Descript.split t
 in
-if d = TermC.empty then
+(*if d = TermC.empty then .. *)
-Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
+(case find_first (fn (_, (d', _)) => d = d') m_patt of
-else
+NONE => Add (i, [], true, m_field, (Sup_POS (d,ts), Position.none))
-(case find_first (eq1 d) m_patt of
-NONE => Add (i, [], true, m_field, Sup (d,ts))
 | SOME (f, (_, id)) =>
-let
+case find_first (fn (i, _, _, _, feedb) => d = (descriptor feedb) andalso i <> 0) i_model of
-fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
+NONE =>
-in
+Add (i, [], true, f, (Cor_POS (d, ts), Position.none))
-case find_first (eq2 d) i_model of
+| SOME (i', _, _, _, itm_) =>
-NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
+if Input_Descript.for_list d then
-| SOME (i', _, _, _, itm_) =>
+let
-if Input_Descript.for_list d then
+val in_itm = o_model_values itm_
-let
+val ts' = union op = ts in_itm
-val in_itm = o_model_values itm_
+val i'' = if in_itm = [] then i else i'
-val ts' = union op = ts in_itm
+in Add (i'', [], true, f, (Cor_POS (d, ts'), Position.none)) end
-val i'' = if in_itm = [] then i else i'
+else Add (i', [], true, f, (Cor_POS (d, ts), Position.none)))
-in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
-else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
-end)
 end
 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
 let
 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
 "\" not for field \"" ^ m_field ^ "\"")
 else
 case O_Model.contains ctxt m_field o_model t of
 ("", ori', all) =>
-(case is_notyet_input ctxt i_model all ori' m_patt of
+(case is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt of
 ("", itm) => Add itm
 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
 end
 case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
 SOME (_, _, m_field, _, ts) =>  (m_field, ts)
 | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
 in
-(*---------------vvvvvvvvvvvvv MV if TermC-is_list all_value-----*)
+(*---------------vvvvvvvvvvvvv MV if TermC.is_list all_value-----*)
 if Model_Def.is_list_descr descr
 then
 let
 val already_input = feedb |> values_POS'
 val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)
 (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Model_Def.get_dscr_opt feedb1 of
 NONE => false
 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
 NONE =>
 (i2, [max_vnt], bool2, m_field2, (Sup_POS (descr2, ts2), pos2)) (*the present in i2_model*)
-| SOME i1_single => i1_single)                      (*shift the item from i1_model to i2_model*)
+| SOME i1_single => i1_single)                     (*shift the item from i1_model to i2_model*)
-| add_other _ _ i2_single = i2_single                     (*keep all the other items in i2_model*)
+| add_other _ _ i2_single = i2_single                    (*keep all the other items in i2_model*)
 (*fill method from items already input*)
 fun fill_method o_model (pbl_imod, met_imod) met_patt =
 let
 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod

changeset 60772	ac0317936138
parent 60771	1b072aab8f4e
child 60773	439e23525491