Talk:OMDoc

From semanticweb.org

[edit] Generating OMDoc from s-expressions

From the discussion in Talk:Semantic MathML, test code to generate OMDoc from s-expressions. Initially this will just be just OpenMath to try cut and paste into a SWiM page to render the axiom.

(define (scmToOmDoc)
  ;to do
)
(define (test5)
  (let ((expr5  '(fun commutivity_add (all (a b) (= (+ a b) (+ b a)) ))  ))
    ;(scmToSemanticMathML - previously discussed
    ;  expr5 
    ;)  
    (scmToOmDoc
      expr5
    )
  )
)
(test5)

I do have one question while trying to create the code. I can make a new page ok in SWiM for instance by copying and pasting the proof code above, but when I edit it manually and replace the <proof> tags with the example from page 18-19 in the OMDoc 1.2 document, it gives errors. See 1 Would appreciate help getting this example to work manually then I can try to follow that with the code. For reference the contents of the test page currently is shown below. --Usoy

<omdoc xmlns:swim="http://www.mathweb.org/omdoc/wiki/syntax" xml:id="elalg-group-inv.unique.proof.omdoc"
  xmlns="http://www.mathweb.org/omdoc"
  xmlns:cc="http://creativecommons.org/ns"
  xmlns:dc="http://purl.org/dc/elements/1.1/"
  xmlns:m="http://www.w3.org/1998/Math/MathML"
  version="1.2">
 
 <CDDefinition>
<Name>plus</Name>
<Description>
The symbol representing an n-ary commutative function plus.
</Description>
<CMP> for all a,b | a + b = b + a </CMP>
<FMP>
<OMOBJ>
  <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMATTR>
          <OMATP>
            <OMS cd="sts" name="type"/>
            <OMS cd="setname1" name="R"/>
          </OMATP>
          <OMV name="a"/>
        </OMATTR>
        <OMATTR>
        <OMATP>
          <OMS cd="sts" name="type"/>
          <OMS cd="setname1" name="R"/>
         </OMATP>
       <OMV name="b"/>
       </OMATTR>
     </OMBVAR>
     <OMA>
       <OMS cd="relation" name="eq"/>
       <OMA>
         <OMS cd="arith1" name="plus"/>
         <OMV name="a"/>
         <OMV name="b"/>
       </OMA>
       <OMA>
         <OMS cd="arith1" name="plus"/>
         <OMV name="b"/>
         <OMV name="a"/>
       </OMA>
     </OMA>
  </OMBIND>
</OMOBJ>
</FMP>
</CDDefinition>
</omdoc>

Hi! First of all, that document you referred to is out of date. Read the most recent version.

Second, you did not write OMDoc, but OpenMath. CDDefinition is an element of OpenMath's language module for defining content dictionaries. Chapter 2.1.2 (read the sections near the end) of the OMDoc spec explain why OpenMath CDs are not sufficient for semantically annotating mathematics. OMDoc, however, is backwards-compatible in the way that an OMDoc theory can be considered as an OpenMath CD, just with more "semantics". Have a look at the documents called omstd-... in my SWiM demo. These are the standard OpenMath content dictionaries, rewritten in OMDoc. --Langec 16:40, 28 June 2006 (CEST)

Thanks for the response. I will post the code I have so far and leave it at that. I did notice some differences in the code from 1.1 to 1.2 and have adjusted the output accordingly. Also in test6 is a start on representing a page at the theory level. Again, just some test code to see what the mappings are going from a more compact structure to OMDoc but you can see we can represent arbitrary levels of structure, not just formulae.

;OMDoc.scm


(define (printnl x)
  (display x)(newline))

(define (spaces n)
  (if (> n 0)
    (begin
    (display " ")
    (spaces (- n 1)) )))


(define (scmToOMDocTheory obj)
  (display "<theory>")(printnl (caar obj))
  (display "<theory-id>")(printnl (cdar obj))
  (scmToOMDocImports (cadr obj))
  (display "<description>")(printnl (caddr obj))
  (scmToOMDocs (cadddr obj))
)
(define (scmToOMDocImports imps)
  (if (not (eq? imps '()))
    (begin 
        (display "<import ")(display (car imps))(printnl "/>")
        (scmToOMDocImports (cdr imps))) 
  )
)
(define (scmToOMDocs exp)
  (if (not (eq? exp '()))
    (begin 
        (scmToOMDoc (car (cdar exp))) 
        (scmToOMDocs  (cdr exp)))
  )
)
(define (scmToOMDoc exp) 
  (scmToOD exp 0)
  (newline))
(define (scmToOD exp indent) ;handle indentation
  (cond 
    ((symbol? exp) 
          (spaces indent)(display "<OMV name=\"")
          (display exp)(printnl "\"/>"))
    ((number? exp) 
          (spaces indent)(display "<OMI>")
          (display exp)(printnl "</OMI>") )
    ((eq? (car exp) 'fun) 
          (display "<CMP>")
          (display (cadr exp))(printnl "</CMP>")
          (printnl "<FMP>")
          (printnl "  <OMOBJ xmlns=\"http://www.openmath.org/OpenMath\">")
          (printnl "    <OMBIND cdbase=\"http://www.openmath.org/cd\">")
          (scmToOD (caddr exp) (+ indent 4))
          (printnl "    </OMBIND>")
          (printnl "  </OMOBJ>")
          (printnl "</FMP>"))
    ((eq? (car exp) 'all) 
          (spaces (+ indent 2))(printnl "<OMS cd=\"quant1\" name=\"forall\"/>")
          (spaces (+ indent 2))(printnl "<OMBVAR>")                                       
          (scmToOMDocForall (cadr exp) (+ indent 2)) 
          (spaces (+ indent 2))(printnl "</OMBVAR>") 
          (scmToOD (caddr exp) (+ indent 2)) )
    ((eq? (car exp) '+) 
          (spaces indent)(printnl "<OMA>")
          (spaces (+ indent 2))(printnl "<OMS cd=\"arith1\" name=\"plus\"/>")
          (scmToOD (cadr exp) (+ indent 2))
          (scmToOD (caddr exp) (+ indent 2))
          (spaces indent)(printnl "</OMA>") )
    ((eq? (car exp) '*) 
          (spaces indent)(printnl "<OMA>")
          (spaces (+ indent 2))(printnl "<OMS cd=\"arith1\" name=\"times\"/>")
          (scmToOD (cadr exp) (+ indent 2))
          (scmToOD (caddr exp) (+ indent 2))
          (spaces indent)(printnl "</OMA>") )
    ((eq? (car exp) '=) 
          (spaces indent)(printnl "<OMA>")
          (spaces (+ indent 2))(printnl "<OMS cd=\"relation\" name=\"eq\"/>")
          (scmToOD (cadr exp) (+ indent 2))
          (scmToOD (caddr exp) (+ indent 2))
          (spaces indent)(printnl "</OMA>") )

    (#t (spaces indent)(printnl exp)) ;default 
  ))
(define (scmToOMDocForall exp indent)
  (if (not (eq? exp '()))
    (begin 
        (spaces (+ indent 2))(display "<OMV name=\"")(display (car exp))(printnl "\"/>")
        (scmToOMDocForall (cdr exp) indent))
  )
)
(define (scmToOMDocForallSet exp set indent)
  (if (not (eq? exp '()))
    (begin 
        (spaces (+ indent 2))(printnl "<OMATTR>")
        (spaces (+ indent 2))(printnl "  <OMATP>")
        (spaces (+ indent 2))(printnl "    <OMS cd=\"sts\" name=\"type\"/>")
        (spaces (+ indent 2))(printnl "    <OMS cd=\"setname1\" name=\"")
          (display set)(display "\"/>") 
        (spaces (+ indent 2))(printnl "  </OMATP>")
        (spaces (+ indent 2))(display "  <OMV name=\"")(display (car exp))(printnl "\"/>")
        (spaces (+ indent 2))(printnl "</OMATTR>")
        (scmToOMDocForall (cdr exp) indent))
  )
)

(define (test5)
  (let ((expr5  '(fun commutivity_add (all (a b) (= (+ a b) (+ b a)) ))  ))
    ;(scmToSemanticMathML ;output already shown on Semantic MathML Page
    ;  expr5 
    ;)  
    (scmToOMDoc
      expr5)))

(define (test5b)
  (let ((expr5b  '(fun commutivity_mult (all (a b) (= (* a b) (* b a)) ))  ))
    (scmToOMDoc
      expr5b)))

(define (test5c)
  (let ((expr5c  '(fun ident (= (* A 1) A))  ))
    (scmToOMDoc
      expr5c
    )))

(define (test6)
  (scmToOMDocTheory                 ;= one page
    '( ("Test Theory" "theory-id")
       ("from1" "from2" "from3") ;imports 
       "Description"
       ((axiom (fun commutivity_add (all (a b) (= (+ a b) (+ b a))) )) 
         ;list of statements can also be examples,lemmas,etc
        (axiom (fun ident (= (* A 1) A)))  ) )))

(test5)
(test5b)
(test5c)
(test6)