1.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Nov 30 13:05:08 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Dec 12 18:08:13 2016 +0100
1.3 @@ -11,7 +11,7 @@
1.4 type icalhd = pos' * cterm' * imodel * pos_ * spec
1.5 val fetchErrorpatterns : tac -> errpatID list
1.6 val input_icalhd : ptree -> icalhd -> ptree * ocalhd
1.7 - val inform : calcstate' -> string -> string * calcstate'
1.8 + val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
1.9 val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list
1.10 val is_exactly_equal : ptree * (pos * pos_) -> string -> string * tac
1.11
1.12 @@ -19,7 +19,7 @@
1.13 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
1.14 val cas_input : term -> (ptree * ocalhd) option
1.15 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
1.16 - val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * calcstate'
1.17 + val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
1.18 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
1.19 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
1.20 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
1.21 @@ -182,9 +182,9 @@
1.22 case parseNEW ctxt ct of
1.23 NONE => (0,[],false,sel, Syn ct):itm
1.24 | SOME t =>
1.25 - (case is_known ctxt sel oris t of
1.26 + (case Chead.is_known ctxt sel oris t of
1.27 ("", ori', all) =>
1.28 - (case is_notyet_input ctxt ppc all ori' pbt of
1.29 + (case Chead.is_notyet_input ctxt ppc all ori' pbt of
1.30 ("",itm) => itm
1.31 | (msg,_) => error ("appl_add': " ^ msg))
1.32 | (_, (i, v, _, d, ts), _) =>
1.33 @@ -232,7 +232,7 @@
1.34 | appl_adds _ _ ppc _ [] = ppc
1.35 | appl_adds dI oris ppc pbt (selct :: ss) =
1.36 let val itm = appl_add' dI oris ppc pbt selct;
1.37 - in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end
1.38 + in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
1.39
1.40 fun oris2itms _ _ [] = ([] : itm list) (* WN161130: similar in ptyps ?!? *)
1.41 | oris2itms pbt vat ((i, v, f, d, ts) :: (os: ori list)) =
1.42 @@ -273,38 +273,38 @@
1.43 if dI <> sdI
1.44 then let val its = map (parsitm (assoc_thy dI)) probl;
1.45 val (its, trms) = filter_sep is_Par its;
1.46 - val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
1.47 + val pbt = (#ppc o get_pbt) (#2 (Chead.some_spec ospec sspec))
1.48 in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
1.49 else
1.50 if pI <> spI
1.51 then if pI = snd3 ospec then (Pbl, probl, meth)
1.52 else
1.53 let val pbt = (#ppc o get_pbt) pI
1.54 - val dI' = #1 (some_spec ospec spec)
1.55 + val dI' = #1 (Chead.some_spec ospec spec)
1.56 val oris = if pI = #2 ospec then oris
1.57 else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.58 in (Pbl, appl_adds dI' oris probl pbt
1.59 (map itms2fstr probl), meth) end
1.60 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.61 then let val met = (#ppc o get_met) mI
1.62 - val mits = complete_metitms oris probl meth met
1.63 + val mits = Chead.complete_metitms oris probl meth met
1.64 in if foldl and_ (true, map #3 mits)
1.65 then (Pbl, probl, mits) else (Met, probl, mits)
1.66 end
1.67 - else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
1.68 - ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
1.69 + else (Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
1.70 + ((#ppc o get_pbt) (#2 (Chead.some_spec ospec spec)))
1.71 (imodel2fstr imodel), meth)
1.72 val pt = update_spec pt p spec;
1.73 in if pos_ = Pbl
1.74 - then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1.75 + then let val {prls,where_,...} = get_pbt (#2 (Chead.some_spec ospec spec))
1.76 val pre =check_preconds(assoc_thy"Isac")prls where_ pits
1.77 in (update_pbl pt p pits,
1.78 - (ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
1.79 + (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
1.80 end
1.81 - else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1.82 + else let val {prls,pre,...} = get_met (#3 (Chead.some_spec ospec spec))
1.83 val pre = check_preconds (assoc_thy"Isac") prls pre mits
1.84 in (update_met pt p mits,
1.85 - (ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec):ocalhd)
1.86 + (Chead.ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec) : ocalhd)
1.87 end
1.88 end
1.89 end
1.90 @@ -374,7 +374,7 @@
1.91 (* structure copied from complete_solve
1.92 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
1.93 all_modspec etc. has to be inserted at Subproblem'*)
1.94 -fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo =
1.95 +fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =
1.96 let
1.97 val fo =
1.98 case p_ of
1.99 @@ -393,21 +393,21 @@
1.100 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
1.101 else
1.102 if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
1.103 - then ("no derivation found", (tacis, c, ptp): calcstate')
1.104 + then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
1.105 else
1.106 let
1.107 val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
1.108 val (tacis, c'', ptp) = case tacis of
1.109 ((Subproblem _, _, _)::_) =>
1.110 let
1.111 - val ptp as (pt, (p,_)) = all_modspec ptp (*<--------------------*)
1.112 + val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
1.113 val mI = get_obj g_metID pt p
1.114 in
1.115 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.116 end
1.117 | _ => cs';
1.118 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.119 - end;
1.120 + end
1.121
1.122 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
1.123 fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
1.124 @@ -455,7 +455,7 @@
1.125 collect all the tacs applied by the way;
1.126 if "no derivation found" then check_error_patterns.
1.127 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
1.128 -fun inform (cs as (_, _, (pt, pos as (p, _))): calcstate') istr =
1.129 +fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
1.130 case parse (assoc_thy "Isac") istr of
1.131 SOME f_in =>
1.132 let
1.133 @@ -492,7 +492,7 @@
1.134 | _ => msg_calcstate'
1.135 end
1.136 end
1.137 - | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate')
1.138 + | NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
1.139
1.140 (* fill-in patterns an forms.
1.141 returns thm required by "fun in_fillform *)
1.142 @@ -545,8 +545,8 @@
1.143 val tac = get_obj g_tac pt p';
1.144 in
1.145 case applicable_in pos pt tac of
1.146 - Notappl msg => (msg, Tac "")
1.147 - | Appl rew =>
1.148 + Chead.Notappl msg => (msg, Tac "")
1.149 + | Chead.Appl rew =>
1.150 let
1.151 val res = case rew of
1.152 Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res