1.1 --- a/src/Tools/isac/CalcElements/rule.sml	Thu Apr 09 17:16:48 2020 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/rule.sml	Thu Apr 09 18:21:09 2020 +0200
     1.3 @@ -11,11 +11,9 @@
     1.4    datatype rule = datatype Rule_Def.rule
     1.5    datatype program = datatype Rule_Def.program
     1.6  
     1.7 -(*/------- to unparse.sml-------\*)
     1.8 -  eqtype cterm'
     1.9 -  type subst = (term * term) list
    1.10 -(*\------- to unparse.sml-------/*)
    1.11 -
    1.12 +  val id_rls: Rule_Def.rule_set -> string
    1.13 +  val id_rule: Rule_Def.rule -> string
    1.14 +  val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool
    1.15  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.16    (*NONE*)
    1.17  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.18 @@ -41,43 +39,19 @@
    1.19      Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)
    1.20  type eval_fn = Rule_Def.eval_fn                                                  (*..from Rule_Def*)
    1.21  
    1.22 -(*/------- to unparse.sml-------\*)
    1.23 -type cterm' = string;
    1.24 -type subst = (term * term) list;
    1.25 +fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
    1.26 +  | id_rls (Rule_Def.Repeat {id, ...}) = id
    1.27 +  | id_rls (Rule_Def.Seqence {id, ...}) = id
    1.28 +  | id_rls (Rule_Def.Rrls {id, ...}) = id;
    1.29  
    1.30 -fun term_to_string' ctxt t =
    1.31 -  let
    1.32 -    val ctxt' = Config.put show_markup false ctxt
    1.33 -  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
    1.34 -fun term_to_string'' thyID t =
    1.35 -  let
    1.36 -    val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
    1.37 -  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
    1.38 -fun term_to_string''' thy t =
    1.39 -  let
    1.40 -    val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
    1.41 -  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
    1.42 -
    1.43 -fun term2str t = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") t;
    1.44 -fun t2str thy t = term_to_string' (ThyC.thy2ctxt thy) t;
    1.45 -fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
    1.46 -fun terms2strs ts = map term2str ts;     (* terms2strs [t1,t2] = ["1 + 2", "abc"];      *)
    1.47 -val terms2str = strs2str o terms2strs;   (* terms2str  [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
    1.48 -val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]";         *)
    1.49 -fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
    1.50 -  | termopt2str NONE = "NONE";
    1.51 -
    1.52 -fun type_to_string'' (thyID : ThyC.thyID) t =
    1.53 -  let
    1.54 -    val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
    1.55 -  in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
    1.56 -fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
    1.57 -val string_of_typ = type2str; (*legacy*)
    1.58 -fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
    1.59 -
    1.60 -val e_type = Type ("empty",[]);
    1.61 -val e_term = Const ("empty", Type("'a", []));
    1.62 -(*\------- to unparse.sml-------/*)
    1.63 -
    1.64 +fun id_rule (Rule_Def.Thm (id, _)) = id
    1.65 +  | id_rule (Rule_Def.Num_Calc (id, _)) = id
    1.66 +  | id_rule (Rule_Def.Cal1 (id, _)) = id
    1.67 +  | id_rule (Rule_Def.Rls_ rls) = id_rls rls
    1.68 +  | id_rule Rule_Def.Erule = "Erule";
    1.69 +fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
    1.70 +  | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2
    1.71 +  | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2
    1.72 +  | eq_rule _ = false;
    1.73  
    1.74  (**)end(**)