namespace http://cds.omdoc.org/urtheories❚

import rules scala://quotation.mmt.kwarc.info❚

/T   introduces a primitive type that exposes the type MMT terms of the underlying implementation
This can be seen as a first step towards MMT meta-programming but is used here only to represent quotations.
❚
theory TermLiterals =
  include ?TermsTypesKinds❙

  /T the type of MMT terms ❙
  termliteral: type❙

  /T makes all MMT terms (inlcudings ill-typed or ill-scoped ones) literals of type $termliteral$❙
  rule rules?TermLiteralRule❙
❚

/T   the language features of quotation
This allows quoting terms that are well-typed in the current context.

The concrete syntax uses MMT's string interpolation feature with the identifier q, i.e., q"t" is the quotation of the term t.
Quoted terms are unevaluated, i.e., q"1+1" != q"2". 

Within t, it is allowed to escape back into evaluated terms: q"1+${s}" is the quasiquotation q"1+e" where e is the result of evaluating s.
❚
theory Quotation =
  include ?LF❙ // LF is not actually needed here. But due a current bug, the comments are not type-checked correctly without LF. ❙

  include ?TermLiterals❙

  /T For any [a:type], $Q a$ is the type of quotations of terms of type $a$.❙
  Quote # Q 1❙

  /T the quotation operator
     Because of interpolation, this is not a unary operator - instead, the evaluated subterms are replaced with free variables and bundled up in a substitution.
     For example, q"1+${s}+2" is internally represented as quote(l, x/s) where l is the term literal 1+x+2.❙
  quote❙
  
  /T the evaluation operator: For [a:type, q: Q a], $eval q$ is the evaluation of $q$ of type $a$.❙
  eval # eval 1❙

  /T the concrete syntax for quotations (using string interpolation)❙
  rule rules?Lexer❙

  /T the formation rule: For [a:type], $Q a$ is a type.❙
  rule rules?QuoteFormation❙
  /T the introduction rule: In the simplest case, for [a:type, t:a], the quotation of $t$ has type $Q a$.❙
  rule rules?QuoteIntroduction❙
  /T the elimination rule: For [a:type, q: Q a], $eval q$ has type $a$.❙
  rule rules?QuoteElimination❙
  /T the type checking rule: For [a:type], we check [q: Q a] by checking that $eval q$ has type $a$.❙
  rule rules?QuoteTyping❙
  /T the beta-style reduction rule: For [a:type,t:a] the evaluation of the quotation $t$ reduces to $t$.❙
  rule rules?EvalQuote❙
  
  /T an auxiliary rule for normalizing quotations:
     For example, it reduces q"1+${q"2"}" to q"1+2".❙
  rule rules?ReduceQuote❙
❚

/T   LF with quotation❚
theory LFQ =
  include ?Quotation❙
  include ?LF❙
❚

/T   a simple test theory ❚
theory QuotingInterpolationExample : ?LFQ =
  a: type❙
  c: a❙
  f: a ⟶ a ⟶ a❙
  
  t: Q a ⟶ Q a❘ = [q] q❙
  
  q1: Q a❘ = q"f c c"❙
  q2: Q a❘ = q"f c ${q1}"❙ 
  q3: Q a❘ = q"f c ${t q1}"❙ 
  q4: Q a❘ = q"f c ${t q"f c c"}"❙ 
  q5: Q a❘ = q"f c ${t q"f c ${t q1}"}"❙ 
❚

namespace examples/Quotation❚

theory ExcludedMiddle : /urtheories?LFQ =
  bool: type❙
  ded : bool ⟶ type❘# ⊦ 1 prec -1❙
  disj: bool ⟶ bool ⟶ bool❘# 1 ∨ 2❙
  not : bool ⟶ bool❘# ¬ 1❙
  em  : {f} ⊦ (eval f) ∨ ¬ (eval f)❙ 
❚

theory PeanoInduction : /urtheories?LFQ =
  include ?ExcludedMiddle❙
  
  nat:  type❙
  zero: nat❙
  succ: nat ⟶ nat❙

  induction: {f} ⊦ (eval f) zero ⟶ ({n} ⊦ (eval f) n ⟶ ⊦ (eval f) (succ n)) ⟶ ({n} ⊦(eval f) n)❙
❚