Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Interpret/Interpret.thy
author Walther Neuper <wneuper@ist.tugraz.at>
Tue, 18 Oct 2016 12:05:03 +0200
changeset 59252 7d3dbc1171ff
parent 59250 727dff4f6b2c
child 59253 f0bb15a046ae
permissions -rw-r--r--
back-track after desing error in previous changeset

notes (the latter of 2 desastrous changesets):
# error was: in Isac thm must be accompanied with thmID,
because Thm.get_name_hint reports "unknown" after ".. RS sym"
# improved design will be: Rewrite* and Rewrite'* take arg. (thmID, thm)
# previous changeset also destroyed "fun pbl2xml" 
     1 (* Title:  collect all defitions for the Lucas-Interpreter

     2    Author: Walther Neuper 110226

     3    (c) due to copyright terms

     4  *)

     5 

     6 theory Interpret

     7 imports "~~/src/Tools/isac/ProgLang/ProgLang"

     8 begin

     9   ML_file "~~/src/Tools/isac/Interpret/mstools.sml"

    10   ML_file "~~/src/Tools/isac/Interpret/ctree.sml"

    11   ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"

    12 ML {*

    13 Rewrite';           (*thm' vvv*)

    14 fun thm'_to_thm'' ((thmID, str) : thm') = (thmID, str2term str) : thm'' (*TODO: id + remove*)

    15 fun thm''_to_thm' ((thmID, trm) : thm'') = (thmID, term2str trm) : thm' (*TODO: id + remove*);

    16 Rewrite;           (*thm'' ^^^*)

    17 *}

    18   ML_file "~~/src/Tools/isac/Interpret/generate.sml"

    19   ML_file "~~/src/Tools/isac/Interpret/calchead.sml"

    20   ML_file "~~/src/Tools/isac/Interpret/appl.sml"

    21   ML_file "~~/src/Tools/isac/Interpret/rewtools.sml"

    22   ML_file "~~/src/Tools/isac/Interpret/script.sml"

    23   ML_file "~~/src/Tools/isac/Interpret/solve.sml"

    24   ML_file "~~/src/Tools/isac/Interpret/inform.sml"

    25   ML_file "~~/src/Tools/isac/Interpret/mathengine.sml"

    26 ML {*

    27 *} ML {*

    28 *}

    29 end
wneuper/isa