I'm still undecided about accepting unicode on input as opposed to latex-style input (e.g. \pi vs the unicode pi character).
The logic syntax would really benefit from using things like \forall as a unicode character on input. It makes the math I/O much prettier but it makes parsing much harder. What does one do with a function (code-char 958)(x:INT) == aka (greek small letter xi).... Some experiments are "in the thought pipeline".... Tim On 11/27/19, Tim Daly <axiom...@gmail.com> wrote: > The new Sane compiler is also being tested with the Fricas > algebra code. The compiler knows about the language but > does not depend on the algebra library (so far). It should be > possible, by design, to load different algebra towers. > > In particular, one idea is to support the "tiny theories" > algebra from Carette and Farmer. This would allow much > finer grain separation of algebra and axioms. > > This "flexible algebra" design would allow things like the > Lean theorem prover effort in a more natural style. > > Tim > > > On 11/26/19, Tim Daly <axiom...@gmail.com> wrote: >> The current design and code base (in bookvol15) supports >> multiple back ends. One will clearly be a common lisp. >> >> Another possible design choice is to target the GNU >> GCC intermediate representation, making Axiom "just >> another front-end language" supported by GCC. >> >> The current intermediate representation does not (yet) >> make any decision about the runtime implementation. >> >> Tim >> >> >> On 11/26/19, Tim Daly <axiom...@gmail.com> wrote: >>> Jason Gross and Adam Chlipala ("Parsing Parses") developed >>> a dependently typed general parser for context free grammar >>> in Coq. >>> >>> They used the parser to prove its own completeness. >>> >>> Unfortunately Spad is not a context-free grammar. >>> But it is an intersting thought exercise to consider >>> an "Axiom on Coq" implementation. >>> >>> Tim >>> >> >