1.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu Feb 02 06:32:30 2017 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Feb 02 06:50:47 2017 +0100
1.3 @@ -41,6 +41,8 @@
1.4 val is_notyet_input : Proof.context -> itm list -> term list -> ori -> ('a * (term * term)) list
1.5 -> string * itm
1.6 val e_calcstate' : calcstate'
1.7 +(* ---- for tests only: made visible in order to remove the warning at fun.def. --------------- *)
1.8 +
1.9 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.10 val vals_of_oris : ori list -> term list
1.11 val is_error : itm_ -> bool
1.12 @@ -71,7 +73,7 @@
1.13 (ctree * pos') * (* the calc-state to which the tacis could be applied *)
1.14 (Generate.taci list) (* ev. several (hidden) steps;
1.15 in REVERSE order: first tac_ to apply is last_elem *)
1.16 -val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate;
1.17 +val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]);
1.18
1.19 (*the state used during one calculation within the mathengine; it contains
1.20 a list of [tac,istate](="tacis") which generated the the calc-state;
1.21 @@ -89,10 +91,6 @@
1.22 (ctree * pos') (* the calc-state resulting from the application of tacis *)
1.23 val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.24
1.25 -(* FIXXXME.WN020430 intermediate hack for fun ass_up *)
1.26 -fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f
1.27 - | f_mout _ _ = error "f_mout: not called with formula";
1.28 -
1.29 (* is the calchead complete ? *)
1.30 fun ocalhd_complete its pre (dI, pI, mI) =
1.31 foldl and_ (true, map #3 its) andalso
1.32 @@ -146,11 +144,10 @@
1.33
1.34 datatype appl =
1.35 Appl of Tac.tac_ (* tactic is applicable at a certain position in the Ctree *)
1.36 -| Notappl of string (* tactic is NOT applicable *)
1.37 +| Notappl of string (* tactic is NOT applicable *)
1.38
1.39 fun ppc2list ({Given = gis, Where = whs, Find = fis, With = wis, Relate = res}: 'a ppc) =
1.40 gis @ whs @ fis @ wis @ res
1.41 -fun ppc135list ({Given = gis, Find = fis, Relate = res, ...}: 'a ppc) = gis @ fis @ res
1.42
1.43 (* get the number of variants in a problem in 'original',
1.44 assumes equal descriptions in immediate sequence *)
1.45 @@ -173,8 +170,6 @@
1.46
1.47 fun is_list_type (Type ("List.list", _)) = true
1.48 | is_list_type _ = false
1.49 -fun has_list_type (Free (_, T)) = is_list_type T
1.50 - | has_list_type _ = false
1.51 fun is_parsed (Syn _) = false
1.52 | is_parsed _ = true
1.53 fun parse_ok its = foldl and_ (true, map is_parsed its)
1.54 @@ -313,11 +308,6 @@
1.55 else (Met, Tac.Apply_Method mI)))
1.56 | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
1.57
1.58 -fun is_field_correct sel d dscpbt =
1.59 - case assoc (dscpbt, sel) of
1.60 - NONE => false
1.61 - | SOME ds => member op = ds d
1.62 -
1.63 (* update the itm_ already input, all..from ori *)
1.64 fun ori_2itm itm_ pid all ((id, vt, fd, d, ts): ori) =
1.65 let
1.66 @@ -568,10 +558,6 @@
1.67 in tracing msg end
1.68
1.69 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
1.70 -fun vars_of_pbl_ pbl_ =
1.71 - let
1.72 - fun var_of_pbl_ (_, (_, t)) = t
1.73 - in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end
1.74 fun vars_of_pbl_' pbl_ =
1.75 let
1.76 fun var_of_pbl_ (_, (_, t)) = t: term
1.77 @@ -630,9 +616,9 @@
1.78 | "#Find" => Tac.Add_Find' (ct, met')
1.79 | "#Relate"=> Tac.Add_Relation'(ct, met')
1.80 | str => error ("specify_additem: uncovered case with " ^ str)
1.81 - val (p, Met, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p, Met) pt of
1.82 - ((p, Met), _, _, pt') => (p, Met, pt')
1.83 - | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
1.84 + val (p, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p, Met) pt of
1.85 + ((p, Met), _, _, pt') => (p, pt')
1.86 + | _ => error "specify_additem: uncovered case of generate1"
1.87 val pre' = check_preconds thy prls pre met'
1.88 val pb = foldl and_ (true, map fst pre')
1.89 val (p_, nxt) =
1.90 @@ -670,7 +656,9 @@
1.91 | "#Find" => Tac.Add_Find' (ct, pbl')
1.92 | "#Relate"=> Tac.Add_Relation'(ct, pbl')
1.93 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
1.94 - val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Selem.Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.95 + val (p, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p,Pbl) pt of
1.96 + ((p, Pbl), _, _, pt') => (p, pt')
1.97 + | _ => error "specify_additem: uncovered case of Generate.generate1"
1.98 val pre = check_preconds thy prls where_ pbl'
1.99 val pb = foldl and_ (true, map fst pre)
1.100 val (p_, nxt) =
1.101 @@ -764,9 +752,9 @@
1.102 (oris, dI', pI', mI', dI, mI, ctxt, met)
1.103 | _ => error "specify (Specify_Problem': uncovered case get_obj"
1.104 val thy = assoc_thy dI
1.105 - val (p, Pbl, pt) =
1.106 + val (p, pt) =
1.107 case Generate.generate1 thy (Tac.Specify_Problem' (pI, (ok, (itms, pre)))) (Selem.Uistate, ctxt) pos pt of
1.108 - ((p, Pbl), _, _, pt) => (p, Pbl, pt)
1.109 + ((p, Pbl), _, _, pt) => (p, pt)
1.110 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
1.111 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
1.112 val mI'' = if mI=e_metID then mI' else mI
1.113 @@ -861,9 +849,9 @@
1.114 | "#Find" => (Tac.Add_Find ct, Tac.Add_Find' (ct, pbl'))
1.115 | "#Relate"=> (Tac.Add_Relation ct, Tac.Add_Relation'(ct, pbl'))
1.116 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
1.117 - val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p,Pbl) pt of
1.118 - ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
1.119 - | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.120 + val (p, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p,Pbl) pt of
1.121 + ((p, Pbl), c, _, pt') => (p, c, pt')
1.122 + | _ => error "nxt_specif_additem: uncovered case generate1"
1.123 in
1.124 ([(tac, tac_, ((p, Pbl), (Selem.Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
1.125 end
1.126 @@ -890,8 +878,8 @@
1.127 | "#Find" => (Tac.Add_Find ct, Tac.Add_Find' (ct, met'))
1.128 | "#Relate"=> (Tac.Add_Relation ct, Tac.Add_Relation'(ct, met'))
1.129 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
1.130 - val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p, Met) pt of
1.131 - ((p, Met), c, _, pt') => (p, Met, c, pt')
1.132 + val (p, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p, Met) pt of
1.133 + ((p, Met), c, _, pt') => (p, c, pt')
1.134 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.135 in
1.136 ([(tac, tac_, ((p, Met), (Selem.Uistate, ctxt)))], c, (pt', (p, Met)))
1.137 @@ -1135,10 +1123,6 @@
1.138 ((pt, ([], Pbl)), fst3 (nxt_specif Tac.Model_Problem (pt, ([], Pbl)))) : calcstate
1.139 end
1.140
1.141 -fun get_spec_form m ((p, p_) : pos') pt =
1.142 - let val (_, _, f, _, _, _) = specify m (p, p_) [] pt
1.143 - in f end
1.144 -
1.145 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1.146 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
1.147 fun tag_form thy (formal, given) =
1.148 @@ -1149,10 +1133,6 @@
1.149 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1.150 " .. " ^ term_to_string''' thy formal ^ " ..types do not match")
1.151
1.152 -fun chktyp thy (n, fs, gs) =
1.153 - ((writeln o (term_to_string''' thy) o (nth n)) fs;
1.154 - (writeln o (term_to_string''' thy) o (nth n)) gs;
1.155 - tag_form thy (nth n fs, nth n gs))
1.156 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
1.157
1.158 (* check pbltypes, announces one failure a time *)