1.1 --- a/src/Tools/isac/calcelems.sml Mon Jul 30 16:41:08 2012 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Tue Jul 31 15:16:47 2012 +0200
1.3 @@ -65,6 +65,25 @@
1.4 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
1.5 val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;
1.6
1.7 +(* error patterns and fill patterns *)
1.8 +type errpatID = string
1.9 +type errpat =
1.10 + errpatID (* one identifier for a list of patterns
1.11 + DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
1.12 + * term list (* error patterns *)
1.13 + * thm list (* thms related to error patterns; note that respective lhs
1.14 + do not match (which reflects student's error).
1.15 + fillpatterns are stored with these thms. *)
1.16 +
1.17 +(* for (at least) 2 kinds of access:
1.18 + (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)
1.19 + (2) given a thm, find respective fillpats *)
1.20 +type fillpatID = string
1.21 +type fillpat =
1.22 + fillpatID (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
1.23 + * term (* the pattern with fill-in gaps *)
1.24 + * errpatID; (* which the fillpat would be a help for
1.25 + DESIGN ?TODO: list for several patterns ? *)
1.26
1.27 datatype rule =
1.28 Erule (*.the empty rule .*)
1.29 @@ -111,6 +130,7 @@
1.30 srls : rls, (*for evaluation of list_fns in script *)
1.31 calc : calc list, (*for Calculate in scr, set by prep_rls *)
1.32 rules : rule list,
1.33 + errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.34 scr : scr} (*Script term: generating intermed.steps *)
1.35 | Seq of (*a sequence of rules to be tried only once *)
1.36 {id : string, (*for trace_rewrite:=true *)
1.37 @@ -122,6 +142,7 @@
1.38 srls : rls, (*for evaluation of list_fns in script *)
1.39 calc : calc list, (*for Calculate in scr, set by prep_rls *)
1.40 rules : rule list,
1.41 + errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.42 scr : scr} (*Script term (how to restrict type ???)*)
1.43 (*Rrls call SML-code and simulate an rls
1.44 difference: there is always _ONE_ redex rewritten in 1 call,
1.45 @@ -136,6 +157,7 @@
1.46 rew_ord : rew_ord, (* for rules *)
1.47 erls : rls, (* for the conditions in rules and preconds *)
1.48 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls *)
1.49 + errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.50 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
1.51 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
1.52 from rls, and then contain both Script _AND_ Rfuns !!!*)
1.53 @@ -381,26 +403,6 @@
1.54 (*FIXME.040207 calclist': used by prep_rls, NOT in met*)
1.55 val calclist'= Unsynchronized.ref ([]: calc list);
1.56
1.57 -(* error patterns and fill patterns *)
1.58 -type errpatID = string
1.59 -type errpat =
1.60 - errpatID (* one identifier for a list of patterns
1.61 - DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
1.62 - * term list (* error patterns *)
1.63 - * thm list (* thms related to error patterns; note that respective lhs
1.64 - do not match (which reflects student's error).
1.65 - fillpatterns are stored with these thms. *)
1.66 -
1.67 -(* for (at least) 2 kinds of access:
1.68 - (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)
1.69 - (2) given a thm, find respective fillpats *)
1.70 -type fillpatID = string
1.71 -type fillpat =
1.72 - fillpatID (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
1.73 - * term (* the pattern with fill-in gaps *)
1.74 - * errpatID; (* which the fillpat would be a help for
1.75 - DESIGN ?TODO: list for several patterns ? *)
1.76 -
1.77 (*.the hierarchy of thydata.*)
1.78
1.79 (*.'a is for pbt | met.*)
1.80 @@ -468,28 +470,32 @@
1.81 next_rule=ne,attach_form=fo};
1.82 end;
1.83
1.84 -val e_rls =
1.85 - Rls{id = "e_rls",
1.86 - preconds = [],
1.87 - rew_ord = ("dummy_ord", dummy_ord),
1.88 - erls = Erls,srls = Erls,
1.89 - calc = [],
1.90 - rules = [], scr = EmptyScr}:rls;
1.91 -val e_rrls = Rrls {id = "e_rrls",
1.92 - prepat = [],
1.93 - rew_ord = ("dummy_ord", dummy_ord),
1.94 - erls = Erls,
1.95 - calc = [],
1.96 - (*asm_thm=[],*)
1.97 - scr=e_rfuns}:rls;
1.98 +val e_rls = Rls {
1.99 + id = "e_rls",
1.100 + preconds = [],
1.101 + rew_ord = ("dummy_ord", dummy_ord),
1.102 + erls = Erls,srls = Erls,
1.103 + calc = [],
1.104 + rules = [],
1.105 + errpatts = [],
1.106 + scr = EmptyScr}: rls;
1.107 +
1.108 +val e_rrls = Rrls {
1.109 + id = "e_rrls",
1.110 + prepat = [],
1.111 + rew_ord = ("dummy_ord", dummy_ord),
1.112 + erls = Erls,
1.113 + calc = [],
1.114 + errpatts = [],
1.115 + scr=e_rfuns}:rls;
1.116 ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
1.117 ("e_rrls",("Tools",e_rrls))
1.118 ]);
1.119
1.120 -fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.121 +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
1.122 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.123 (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.124 - | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.125 + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
1.126 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.127 (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.128 | rep_rls Erls = rep_rls e_rls
1.129 @@ -498,13 +504,10 @@
1.130 (*| rep_rls (Seq {id,...}) =
1.131 error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.132 --1.7.03*)
1.133 -fun rep_rrls
1.134 - (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
1.135 - scr=Rfuns
1.136 - {attach_form,init_state,locate_rule,
1.137 - next_rule,normal_form}}) =
1.138 - {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
1.139 - rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
1.140 +fun rep_rrls (Rrls {id, calc, erls, prepat, rew_ord, errpatts,
1.141 + scr = Rfuns {attach_form, init_state, locate_rule, next_rule, normal_form}}) =
1.142 + {id=id, calc=calc, erls=erls, prepat=prepat,
1.143 + rew_ord=rew_ord, errpatts=errpatts, attach_form=attach_form, init_state=init_state,
1.144 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
1.145 | rep_rrls (Rls {id,...}) =
1.146 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.147 @@ -512,13 +515,13 @@
1.148 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.149
1.150 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.151 - rules =rs,scr=sc}) r =
1.152 + rules =rs, errpatts=errpatts, scr=sc}) r =
1.153 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.154 - rules = rs @ r,scr=sc}:rls)
1.155 + rules = rs @ r, errpatts=errpatts, scr=sc}:rls)
1.156 | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.157 - rules =rs,scr=sc}) r =
1.158 + rules =rs, errpatts=errpatts, scr=sc}) r =
1.159 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.160 - rules = rs @ r,scr=sc}:rls)
1.161 + rules = rs @ r, errpatts=errpatts, scr=sc}:rls)
1.162 | append_rls id (Rrls _) _ =
1.163 error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.164
1.165 @@ -534,22 +537,22 @@
1.166 | merge_rls _ rls Erls = rls
1.167 | merge_rls id
1.168 (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.169 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.170 + rules =rs1, errpatts=eps1, scr=sc1})
1.171 (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.172 - (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.173 + rules =rs2, errpatts=eps2, scr=sc2}) =
1.174 (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.175 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.176 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.177 ((#srls o rep_rls) r2),
1.178 calc=ca1 @ ((#calc o rep_rls) r2),
1.179 - (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.180 - rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.181 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.182 + errpatts = gen_union (op=) 0 (eps1, eps2),
1.183 scr=sc1}:rls)
1.184 | merge_rls id
1.185 (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.186 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.187 + rules =rs1, errpatts=eps1, scr=sc1})
1.188 (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.189 - (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.190 + rules =rs2, errpatts=eps2, scr=sc2}) =
1.191 (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.192 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.193 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.194 @@ -557,19 +560,22 @@
1.195 calc=ca1 @ ((#calc o rep_rls) r2),
1.196 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.197 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.198 + errpatts = gen_union (op=) 0 (eps1, eps2),
1.199 scr=sc1}:rls)
1.200 | merge_rls _ _ _ =
1.201 - error "merge_rls: not for reverse-rewrite-rule-sets\
1.202 - \and not for mixed Rls -- Seq";
1.203 + error "merge_rls: not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq";
1.204 +
1.205 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.206 - (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.207 + rules=rs, errpatts=eps, scr=sc}) r =
1.208 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.209 - (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.210 + rules = gen_rems eq_rule (rs, r),
1.211 + errpatts = eps(*gen_rems op= (eps, TODO)*),
1.212 scr=sc}:rls)
1.213 | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.214 - (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.215 + rules =rs, errpatts=eps, scr=sc}) r =
1.216 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.217 - (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.218 + rules = gen_rems eq_rule (rs, r),
1.219 + errpatts = eps(*gen_rems op= (eps, TODO)*),
1.220 scr=sc}:rls)
1.221 | remove_rls id (Rrls _) _ = error
1.222 ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.223 @@ -640,7 +646,11 @@
1.224 | ass ((calci, (cali, eval_fn))::ids) =
1.225 if calID = cali then calci
1.226 else ass ids
1.227 - in ass (!calclist') : calcID end;
1.228 + in ass (!calclist') (*: calcID
1.229 +Type mismatch in type constraint. Value: ass (! calclist') : string Constraint: calcID
1.230 +Reason: Can't unify string = string (*In Basis*) with calcID = int (*In Basis*) (Different type constructors)
1.231 + *)
1.232 + end;
1.233
1.234 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
1.235 (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;