[nogin] Fixed some outdated links._ Mon Sep 19 03:41:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-18-116292000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-18-116292000-PDT.html [emre] This is the initial commit of the new FIR theory. This commit contains the_ Mon Sep 19 03:41:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-25-672728000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-25-672728000-PDT.html [emre] Oops. Let_s not print out theories that are not compiled in._ Mon Sep 19 03:41:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-32-437791000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-32-437791000-PDT.html [emre] Adding __fir__ to ALL_THEORIES._ Mon Sep 19 03:41:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-32-806102000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-32-806102000-PDT.html [emre] Committing some spelling corrections._ Mon Sep 19 03:41:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-33-169993000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-33-169993000-PDT.html [emre] Seems like compare_num was using a naive implementation that was subject to_ Mon Sep 19 03:41:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-33-825900000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-33-825900000-PDT.html [emre] Removed mfir_comment since it was redundant_ the functionality it provided was_ Mon Sep 19 03:41:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-34-336202000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-34-336202000-PDT.html [emre] Adding new modules to the output._ Mon Sep 19 03:41:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-35-852577000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-35-852577000-PDT.html [emre] Flushing out some work on the typing rules._ Mon Sep 19 03:41:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-38-288258000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-38-288258000-PDT.html [nogin] Removed the special_case handling for axioms _rules without arguments and without_ Mon Sep 19 03:41:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-39-910333000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-39-910333000-PDT.html [emre] Splitting typing rules into multiple files, which will be easier to manage._ Mon Sep 19 03:41:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-41-287649000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-41-287649000-PDT.html [emre] Adding new modules to the list of modules to print._ Mon Sep 19 03:41:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-42-483249000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-42-483249000-PDT.html [granicz] Added a new theory for Phobos. Eventually, I_ll migrate Phobos_related_ Mon Sep 19 03:41:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-43-672479000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-43-672479000-PDT.html [granicz] Added phobos to ALL_._ Mon Sep 19 03:41:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-44-258517000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-44-258517000-PDT.html [granicz] Makefile was missing ../phobos._ Mon Sep 19 03:41:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-44-603956000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-44-603956000-PDT.html [granicz] Rewrite was prepending not appending to the parameter._ Mon Sep 19 03:41:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-44-958537000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-44-958537000-PDT.html [granicz] I figured out why the new Phobos rewrite wasn_t working._ Mon Sep 19 03:41:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-45-331107000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-45-331107000-PDT.html [nogin] Added theories/phobos_ Mon Sep 19 03:41:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-45-686872000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-45-686872000-PDT.html [emre] This is an intermediate commit, in the sense that I have a few temporary_ Mon Sep 19 03:41:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-46-546892000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-46-546892000-PDT.html [emre] Except for values of a union type, this commit finishes an initial pass at_ Mon Sep 19 03:41:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-47-828971000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-47-828971000-PDT.html [emre] This is my pass at typing rules for union definitions. Had to add a length_ Mon Sep 19 03:41:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-48-385926000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-48-385926000-PDT.html [emre] Adding kind well_formedness judgments, though I only use them in the equality_ Mon Sep 19 03:41:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-48-899863000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-48-899863000-PDT.html [emre] Oops. Forgot about these minor changes to term operators._ Mon Sep 19 03:41:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-49-346575000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-49-346575000-PDT.html [emre] Simplifying many rules by the deletion of unnessary premises. This addresses_ Mon Sep 19 03:41:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-49-740464000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-49-740464000-PDT.html [emre] Another round of minor documentation/notes_to_myself updates before I start_ Mon Sep 19 03:41:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-50-291447000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-50-291447000-PDT.html [emre] This finishes my pass at typing rules for tyUnion, tyApply, and union_values._ Mon Sep 19 03:41:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-50-702602000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-50-702602000-PDT.html [emre] Oops, forgot to include these files _again_. At some point, I may consider_ Mon Sep 19 03:41:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-51-618891000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-41-51-618891000-PDT.html [emre] Just wanted to flush some work out before TPHOLs._ Mon Sep 19 03:42:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-42-14-775464000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-42-14-775464000-PDT.html [emre] Lots of changes here__ Mon Sep 19 03:43:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-01-567511000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-01-567511000-PDT.html [emre] Updating the list of theories to print to reflect new modules._ Mon Sep 19 03:43:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-05-964135000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-05-964135000-PDT.html [emre] This finishes my initial pass through the typing rules for allocation._ Mon Sep 19 03:43:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-06-704527000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-06-704527000-PDT.html [emre] I_ve debugged the rewrites in bool, list, and int_set. In particular,_ Mon Sep 19 03:43:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-08-384063000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-08-384063000-PDT.html [emre] Committing some stuff before I potentially kill my working copy of MetaPRL._ Mon Sep 19 03:43:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-10-511160000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-10-511160000-PDT.html [emre] An initial pass at implementing the union of two interval sets._ Mon Sep 19 03:43:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-11-038326000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-11-038326000-PDT.html [emre] This should finish up interaval sets, at least for the time being._ Mon Sep 19 03:43:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-13-739952000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-13-739952000-PDT.html [emre] Oops. Mistake on the typing rule for tuple types._ Mon Sep 19 03:43:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-16-305115000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-16-305115000-PDT.html [emre] Wrote up most of the rules for unary operations. Some unop_s_ Mon Sep 19 03:43:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-16-706395000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-16-706395000-PDT.html [emre] This finishes off the atom typing rules, for the most part. Finally sat down_ Mon Sep 19 03:43:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-17-327923000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-17-327923000-PDT.html [emre] I_ve written up half of the rules for match expressions._ Mon Sep 19 03:43:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-18-129118000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-18-129118000-PDT.html [emre] This finishes my initial pass at typing rules for match expressions._ Mon Sep 19 03:43:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-18-668200000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-18-668200000-PDT.html [emre] Some minimal documentation for the match expression typing rules._ Mon Sep 19 03:43:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-19-123666000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-19-123666000-PDT.html [emre] Committing some typing rules for subscripting rules. Haven_t dealt with_ Mon Sep 19 03:43:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-19-530033000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-19-530033000-PDT.html [emre] Minor cleanup to some terms and typing rules, corrections to typing rules, and_ Mon Sep 19 03:43:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-20-095889000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-20-095889000-PDT.html [emre] Given my current set of __test cases__, there_s no sensible reason_ Mon Sep 19 03:43:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-21-311463000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-21-311463000-PDT.html [emre] More corrections to typing rules _and a minor typo fix to a display form_._ Mon Sep 19 03:43:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-22-489744000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-08/2005-09-19-03-43-22-489744000-PDT.html