;-*- Mode: Common-lisp; Package: lexiparse; Readtable: ytools; -*-
(in-package :lexiparse)

(depends-on %module/ ytools lexiparse)

(depends-on %lexiparse/ xml arithgram)

#+allegro
(defun allegro-case-choice ()
   (cond ((eq excl:*current-case-mode* ':case-sensitive-lower)
          ':preserve)
         (t ':up))) 

(def-grammar owl-s
    :top-tokens (define with_namespaces)
    :lex-parent standard-arith-syntax
    :syn-parent standard-arith-syntax
    :sym-case #-allegro :up #+allegro (allegro-case-choice)) 

(defvar owl-s-lexical-chars* '(#\_))

;;; These are the syntactic operators that can used to build
;;; arbitrary control structures.      
(defconstant +owl-s-control-operators+
    '(anyord split-join split semicolon))

(defconstant +owl-s-taggables+
    '(perform produce)) 

(defun typed-vars-tidier (sort)
   (\\ (this-ptree _)
      (match-cond this-ptree
         (:? ?(:^+ ?,sort (:^+ colon (:^+ group ?@decls)))
            !~(:^+ ,sort ,@decls))
         (:? ?(:^+ ?,sort (:^+ colon ?decl))
            !~(:^+ ,sort ,decl))       
         (:else (defect "'" sort "' doesn't occur in the form "
                        sort ":(...)"))))) 

(defun result-defects (exp)
   (let-fun ()
      (match-cond exp
         (:? ?(:^+ forall ?vars ?r)
            (append (decls-defects vars)
                    (forall-body-must-be-whens r)))
         (:? ?(:^+ exists ?vars ?r)
            (list (defect "Existential quantifiers are illegal in results")))
         (:? ?(:^+ when ?_ ?effect)
            (result-defects effect))
         (:? ?(:^+ and ?@conjuncts)
            (<! result-defects conjuncts))
         (:? ?(:^+ group ?elt)
            (result-defects elt))
         (:? ?(:^+ group ?@_)
            (list (defect "Can't have <comma> as a connective")))
         (:? ?(:^+ not ?elt)
            (must-be-fun-app elt))
         (:? ?(:^+ output ?@_)
            '())
         (t (must-be-fun-app exp)))

    :where

       (:def decls-defects (vl)
           (match-cond vl
              (:? ?(:^+ group ?@decls)
                 (repeat :for ((decl :in decls))
                  :nconc (decl-defects decl)))
              (:else (decl-defects vl))))

       (:def decl-defects (decl)
          (match-cond decl
             (:? ?(:^+ hyphen ?@_)
                   '())
             (:? ?(:^+ comma ?@vars)
                (and (not (is-list-of vars #'is-Symbol))
                     (list (defect "Vars in declarations are not all symbols: "
                                   vars))))
             (:? ?var
                (and (not (is-Symbol var))
                     (list (defect "Var in declaration is not a symbol: "
                                   var))))))

       (:def forall-body-must-be-whens (r)
          (match-cond r
             (:? ?(:^+ when ?_ ?e)
                (result-defects e))
             (:? ?(:^+ and ?@conjuncts)
                (<! forall-body-must-be-whens
                    conjuncts))
             (:else (list (defect "Body of 'forall' must be a '|->' or a conjunction"
                                  " of '|->' expressions"))))))) 

(defun must-be-fun-app (e)
   (match-cond e
      (:? ?(:^+ fun-app ?_ ?@_)
        '())
      (:else (list (defect "Context requires atomic formula"))))) 

(defun elim-left-braces (pt _)
   (match-cond pt
      (:? ?(:^+ ?c ?@subs)
         (multi-let (((okay defects)
                      (repeat :for ((sub :in subs)
                                    :collectors okay defects)
                       :result (values okay defects)
                         (match-cond sub
                            (:? ?(:^+ left-brace ?@subsubs)
                               (cond ((= (len subsubs) 1)
                                      (one-collect okay
                                         (first subsubs)))
                                     (t
                                      (one-collect defects
                                         (defect "Left-brace encompasses"
                                                 " strange number of subtrees")))))
                            (t (one-collect okay sub))))))

            (cond ((null defects)
                   !~(:^+ ,c ,@okay))
                  (t defects))))
      (t false)))

(defun control-composition-check (this-ptree _ _)
   (match-let ?(:^+ ?_ ?@elements)
              this-ptree
      (repeat :for ((that-ptree :in elements)
                    :collector defects)
         (check-down-to-control-constructs that-ptree)

       :where
          (:def check-down-to-control-constructs (that-ptree)
              (match-cond that-ptree
                 (:? ?(:^+ ?c ?@_)
                    (cond ((or (memq c +owl-s-control-operators+)
                               (memq c +owl-s-taggables+)
                               (eq c 'tag))
                           !())
                          ((eq c 'with_namespaces)
                           (check-down-to-control-constructs
                               (first (Parsetree-subtrees that-ptree))))
                          (t (list (defect "Illegal as element of"
                                           " composed process: "
                                           that-ptree)))))

                 (:else
                  (list (defect "Atomic expression " that-ptree
                                " not allowed as"
                                " element of composed process"))))))))

;;; This is applied one level above the tree we are actually checking,
;;; 'lo-ptree' --
(defun control-context-check (lo-ptree hi-ptree)
      (match-cond hi-ptree
         (:? ?(:^+ if ?_ ?,lo-ptree ?@_)
            !())
         (:? ?(:^+ if ?_ ?_ ?,lo-ptree)
            !())
         (:? ?(:^+ define ?sort ?_ ?_ ?body)
            (cond ((and (eq sort 'composite)
                        (eq body lo-ptree))
                   !())
                  (t (list (defect "Control construct can appear"
                                   " below 'define' only as the body of"
                                   :% " a composite process.")))))
         (:? ?(:^+ ?c ?@_)
            (cond ((memq c +owl-s-control-operators+)
                   !())
                  (t (list (defect "Control construct in illegal context (op "
                                   c ")"))))))) 

(with-grammar owl-s

;;; LEXICAL

   (def-lexical-tokens ((#\{ left-brace)
                        (#\} right-brace)
                        (#\. dot)))

   ;; ;? = choice, ; = sequence
   (def-lexical #\;
         (dispatch (#\? (token choice))
                   (:else (token semicolon)))) 

   (def-lexical #\| 
   ;; ||; = any-order, ||> = split+join, ||< = split.
   ;; '|->' becomes the token <when> --
                    (dispatch     
                       (#\| (dispatch 
                               (#\; (token anyord))
                               (#\> (token split-join))
                               (#\< (token split))))
                       (#\- (dispatch (#\> (token when)))) 
                       (:else (token or))))

   ;; '->' is ordinary if-then --
   (def-lexical #\- (dispatch
                       (#\> (token imply))
                       (:else (token minus))))

   ;; '=>' becomes the token <when>, although '|->' is now the preferred form
   (def-lexical #\= (dispatch
                       (#\> (token when))
                       (:else (token equals)))) 

   ;; '<=' becomes the token <bind-param>
   (def-lexical #\< (dispatch
                       (#\= (token bind-param))
                       (:else (token less)))) 

   ;; '::' is for step tags --
   (def-lexical #\: (dispatch
                        (#\: (token tag))
                        (:else (token colon)))) 

   (def-lexical (#\_ #\a - #\z #\A - #\Z #\?) (lex-sym owl-s-lexical-chars*)
       :name alphabetic)


;;; SYNTACTIC

   (def-syntactic with_namespaces :reserved true
                  :prefix (:precedence 15 :numargs 2)
      :tidier
         ((:? ?(:^+ with_namespaces ?spec ?e)
             (let* ((namespace-pairs (namespace-spec-listify spec))
                    (defects (<? is-Defect namespace-pairs)))
                (cond ((null defects)
                       !~(:^+ with_namespaces ,e ,@namespace-pairs))
                      (t
                       defects))))))
                  
   (defun namespace-spec-listify (spec)
      (match-cond spec
         (:? ?(:^+ uri ?s)
            (list !~(:^+ namespace+name ,false  (:^+ uri ,s))))
         (:? ?(:^+ ?(:|| equals name-wrt-space)
                   ?(:+ ?sym is-Symbol)
                   (:^+ uri ?s))
            (list !~(:^+ namespace+name ,sym (:^+ uri ,s))))
         (:? ?(:^+ group ?@specs)
            (<! namespace-spec-listify specs))
         (t
          (list (defect "Illegal namespace spec " spec))))) 

   (def-syntactic uri :reserved true
                  :prefix (:precedence 210 :numargs 1)
      :checkers
         ((:? ?(:~ ?(:^+ uri ?(:+ ?s is-String)))
           (defect "uri followed by non-string " s)))) 

   ;; Top node is of form
   ;;     ::= define [atomic | simple] <process-spec>
   ;;         | define composite <process-spec>{ stmt }
   (def-syntactic define :reserved true
                         :prefix (:precedence 5 :numargs 1)
      :tidier
      ((:? ?(:^+ define (:^+ composite 
                              ?(:^+ process ?name ?@iopr-spec)
                              ?@body-spec))
          !~(:^+ define composite ,name (:^+ iopr ,@iopr-spec) ,@body-spec))

       (:? ?(:^+ define (:^+ atomic (:^+ process ?name ?@iopr-spec)))
          !~(:^+ define atomic ,name (:^+ iopr ,@iopr-spec) nil))

       (:? ?(:^+ define (:^+ simple (:^+ process ?name ?@iopr-spec)))
          !~(:^+ define simple ,name (:^+ iopr ,@iopr-spec) nil))

       (:else (defect "Unintelligible 'define' expression")))

      :checkers

       ((:up *
          (:? ?(:^+ ?op ?@_)
             (cond ((not (memq op '(with_namespaces left-brace)))
                    (defect "'define' can't appear below " op)))))

        (:? ?(:~ ?(:^+ define ?_ ?(:+ ?name is-name) ?@_))
           (defect "Process has illegal name: " name))

        (:? ?(:^+ define ?_ ?_ (:^+ iopr ?@ioprs) ?_)
           (check-all iopr ioprs this-grammar
                  (:? ?(:^+ ?(:~ ?(:|| inputs outputs locals participants
                                       precondition result))
                            ?_)
                     (defect "Process has illegal IOPR spec: " iopr))))

        (:? ?(:^+ define ?_ ?_ (:^+ iopr ?@ioprs) ?_)
           (nconc (occ-range ioprs 0 1 ?(:^+ inputs ?@_))
                  (occ-range ioprs 0 1 ?(:^+ outputs ?@_))
                  (occ-range ioprs 0 1 ?(:^+ locals ?@_))
                  (occ-range ioprs 0 1 ?(:^+ precondition ?@_))
                  )))) 

   ;; __::= atomic <process-spec>
   (def-syntactic atomic
                  :reserved true
                  :prefix (:precedence 15 :numargs 1))

   ;; __::= simple <process-spec> 
   (def-syntactic simple :reserved true
                  :prefix (:precedence 15 :numargs 1))

   ;; __::=  composite <process-spec>... { ...
   (def-syntactic composite :reserved true
                  :prefix (:precedence 15 :numargs 2)
      :tidier
        ((:? ?(:^+ composite ?proc (:^+ left-brace ?body))
            !~(:^+ composite ,proc ,body))
         (:? ?(:^+ composite ?proc ?b)
            (defect "Ill-formed body for composite process " proc
                    :% " (must be surrounded by braces): " b)))) 

   
   ;; __::= process <name>(-IOPRs-)
   (def-syntactic process :reserved true
                  :prefix (:precedence 25 :numargs 1)  
      :tidier
         ((:? ?(:^+ process (:^+ fun-app ?name [_*_] (:^+ comma ?@ioprs)))
             !~(:^+ process ,name ,@ioprs))
          (:? ?(:^+ process (:^+ fun-app ?name [_*_] ?@subs))
            !~(:^+ process ,name ,@subs))
          (:else (defect "'process' must be followed by <name>"
                         " and IOPRs in parens")))

      :checkers

         ((:? ?(:^+ process ?@_)
             (defect "Stray occurrence of 'process'")))) 

   
   ;; <IOPR> ::= inputs : (...)
   (def-syntactic inputs :reserved true
                         :prefix (:context 1 :precedence 120
                                  :local-grammar ((1 typed-var-grammar)))
      :tidier
         (typed-vars-tidier 'inputs)

      :checkers
         ((:up 1 (:? ?(:^+ iopr ?@_)))))

   ;; <IOPR> ::= outputs : (...)
   (def-syntactic outputs :reserved true
                          :prefix (:context 1 :precedence 120
                                   :local-grammar ((1 typed-var-grammar)))
      :tidier
         (typed-vars-tidier 'outputs)

      :checkers
         ((:up 1 (:? ?(:^+ iopr ?@_)))))

   ;; <IOPR> ::= locals : (...)
   (def-syntactic locals :reserved true
                        :prefix (:context 1 :precedence 120
                                 :local-grammar ((1 typed-var-grammar)))
      :tidier
         (typed-vars-tidier 'locals)

      :checkers
      ((:up 1 (:? ?(:^+ iopr ?@_)))))

   ;; <IOPR> ::= participants : (...)
   (def-syntactic participants :reserved true
                        :prefix (:context 1 :precedence 120
                                 :local-grammar ((1 typed-var-grammar)))
      :tidier
         (typed-vars-tidier 'participants)

      :checkers
         ((:up 1 (:? ?(:^+ iopr ?@_))))) 

   ;; <IOPR> ::= precondition : ...
   (def-syntactic precondition :reserved true
                               :prefix (:context 1 :precedence 120)
      :tidier
         ((:? ?(:^+ precondition (:^+ colon ?exp))
             !~(:^+ precondition ,exp))
          (:else (defect "'precondition' not followed by ': <expression>'")))

      :checkers
         ((:up 1 (:? ?(:^+ iopr ?@_))))) 

   ;; <IOPR> ::= result : ...
   (def-syntactic result :reserved true
                          :prefix (:context 1 :precedence 120)
      :tidier
         ((:? ?(:^+ result (:^+ colon ?exp))
             !~(:^+ result ,exp))
          (:else (defect "'result' not followed by ': <expression>'")))

      :checkers
         ((:up 1 (:? ?(:^+ iopr ?@_)))
             (match-let ?(:^+ result ?exp)
                        this-ptree
                (result-defects exp)) )) 

   (def-syntactic output :reserved true
                  :prefix (:precedence 200 :numargs 1)
      :tidier
         ((:? ?(:^+ output (:^+ group ?@bindings))
             !~(:^+ output ,@bindings))
;;;;      (:? ?(:^+ output ?binding)
;;;;         !~(:^+ output ?binding))
;;;;          (:else (defect "Output must be followed by bindings in parens"))
          )

      :checkers
         ((:? ?(:^+ output ?@bindings)
             (check-all b bindings this-grammar
                (:? ?(:~ ?(:^+ bind-param ?@_))
                   (defect "Outputs must all be of form 'param <= exp', not "
                           b)))))) 

   ;; <name> ::= <name> : <name>
   ;; 
   (def-syntactic colon :lex ":" :infix (:context :binary :precedence 210)
                         ;; -- namespace construct, with high precedence
                         :prefix (:context 1 :precedence 120)
                         ;; -- Occurs only after inputs, outputs, preconditions, effects
                         ;; Low precedence, but higher than comma
      :tidier
         ((:? ?(:^+ colon ?namespace [_*_] ?name)
             !~(:^+ name-wrt-space ,namespace ,name)))

      :checkers
         ((:? ?(:^+ colon ?@_)
            (defect "Stray colon"))

          (:? ?(:^+ name-wrt-space ?namespace ?name)
             (nconc (cond ((and namespace (is-Symbol namespace)) !())
                          (t (list (defect "Namespace must be a non-nil symbol: "
                                           namespace))))
                    (cond ((is-Symbol name) !())
                          (t (list (defect "Name must be a symbol: "
                                           name)))))))) 

   (def-syntactic forall :reserved true
                         :prefix (:context 2 :precedence 90
                                  :local-grammar ((1 typed-var-grammar))))

   (def-syntactic exists :reserved true
                         :prefix (:context 2 :precedence 90
                                  :local-grammar ((1 typed-var-grammar)))) 

   (def-syntactic when :lex "=>"
                       :infix (:context :binary
                               :left-precedence 110 :right-precedence 111)) 

   (def-syntactic left-brace :lex "{"
                             :prefix (:precedence 0
                                      :context (:open \| right-brace))
      :tidier
      ((:? ?(:^+ left-brace ?sub)
          sub)))

   (def-syntactic right-brace :lex "}"
                              :suffix (:left-precedence 0 :context :close)) 

   (def-syntactic bind-param :lex "<="
                             :infix (:context :binary
                                     :precedence 110)
      :checkers
         ((:? ?(:^+ bind-param ?p ?_)
            (and (not (is-Symbol p))
                 (defect "Non-symbol to left of '<=': " p)))
          (:up 1
             (:? ?(:^+ ?(:|| output perform produce) ?@_)))        )) 

   (def-syntactic anyord :lex "||;"
                         :infix (:precedence 60 :context :grouping)
      :tidier 'elim-left-braces

      :checkers (control-composition-check

                 (:up 1 (control-context-check this-ptree that-ptree))))


   (def-syntactic split-join :lex "||>"
                             :infix (:precedence 60 :context :grouping)
       :tidier 'elim-left-braces

       :checkers (control-composition-check

                 (:up 1 (control-context-check this-ptree that-ptree))))

   (def-syntactic split :lex "||<"
                        :infix (:precedence 60 :context :grouping)
       :tidier 'elim-left-braces

       :checkers (control-composition-check

                 (:up 1 (control-context-check this-ptree that-ptree))))

   (def-syntactic choice :lex ";?"
                         :infix (:precedence 60 :context :grouping)
       :tidier 'elim-left-braces

       :checkers (control-composition-check

                 (:up 1 (control-context-check this-ptree that-ptree))))

   (def-syntactic semicolon :lex ";"
                            :infix (:precedence 80 :context :grouping)
       :tidier 'elim-left-braces

       :checkers (control-composition-check

                 (:up 1 (control-context-check this-ptree that-ptree))))

   (def-syntactic if :reserved true
                     :prefix (:numargs 2 :precedence 85)
      :tidier ((:? ?(:^+ if ?test (:^+ then (:^+ else ?iftrue ?iffalse)))
                  !~(:^+ if ,test ,iftrue ,iffalse))
               (:? ?(:^+ if ?test (:^+ then ?iftrue))
                  !~(:^+ if ?test ?iftrue))
               (t
                (defect "'if' has no 'then' part"))))

   (def-syntactic then :reserved true
                       :prefix (:precedence 87 :numargs 1))

   (def-syntactic else :reserved true
                       :infix (:precedence 88 :context :binary))

   (def-syntactic perform :reserved true
                          :prefix (:context 1 :precedence 90)
      :tidier
         ((:? ?(:^+ perform (:^+ fun-app ?name [_*_] ?@pbs))
             !~(:^+ perform ,name ,@pbs))
          (:else (defect "Unintelligible")))

      :checkers
         ((:? ?(:^+ perform ?name ?@_)
             (and (not (is-name name))
                  (defect "Perform of process with illegal name " name)))

          (:? ?(:^+ perform ?name ?@bdgs)
             (check-all b bdgs this-grammar
                (:? ?(:~ ?(:^+ bind-param ?_ ?_))
                   (defect "Illegal data input " b " to perform of " name))))

          ))

   ;; 'produce (p1 <= v1 , ...)' indicates bindings to outputs of this
   ;; process
   (def-syntactic produce :reserved true
                         :prefix (:context 1 :precedence 90)
      :tidier
         ((:? ?(:^+ produce (:^+ group ?@bindings))
             !~(:^+ produce ,@bindings))
          (:? ?(:^+ produce ?binding)
             !~(:^+ produce ,binding))
          (:else (defect "'produce' must be followed by bindings in parens")))

      :checkers
         ((:? ?(:^+ produce ?@bindings)
             (check-all b bindings this-grammar
                (:? ?(:~ ?(:^+ bind-param ?@_))
                   (defect "'produce' args must all be of form 'param <= exp', not "
                           b)))))) 

   (def-syntactic tag :lex "::" :infix (:context :binary :precedence 81)
      :checkers
         ((:? ?(:^+ tag ?name ?_)
             (and (not (is-Symbol name))
                  (defect "Illegal tag: " name)))

          (:? ?(:^+ tag ?_ ?x)
             (match-cond x
                (:? ?(:^+ ?op ?@_)
                   (cond ((memq op +owl-s-taggables+)
                          !())
                         (t (defect "Illegal as tagged element: " x))))))

          (:up 1 (control-context-check this-ptree that-ptree)))) 

   ;; Eliminate commas from parenthesized expressions
   (def-syntactic left-paren :lex "("
                             :prefix (:precedence 0
                                      :context (:open comma right-paren))
                             :infix (:left-precedence 200 :right-precedence 0
                                     :context (:open comma right-paren))
      :tidier
         ((:? ?(:^+ left-paren [*_] ?e)
             e)
          (:? ?(:^+ left-paren [*_] ?@subs)
             !~(:^+ group [*_] ,@subs))
          (:? ?(:^+ left-paren ?f [_*_] ?@args)
             !~(:^+ fun-app ,f [_*_] ,@args)))) 

   (def-syntactic \| :lex "" :infix (:precedence 3 :context :grouping))

   (def-syntactic dot :lex "." :infix (:precedence 205 :context :binary)
      :checkers
      ((:? ?(:^+ dot ?step ?output)
          (nconc (cond ((is-Symbol step) !())
                       (t (list (defect "Illegal name to left of dot in "
                                        step "." output))))
                 (cond ((is-Symbol output) !())
                       (t (list (defect "Illegal name to right of dot in "
                                        step "." output))))))))
)


;;; LOCAL GRAMMAR for type declarations

(def-grammar typed-var-grammar
    :lex-parent owl-s
    :syn-parent owl-s
    :replace ((minus hyphen))
    :sym-case #-allegro :up #+allegro (allegro-case-choice)

 :definitions
 (
   (def-syntactic \| :lex "" :infix (:precedence 16 :context :grouping))

   (def-syntactic left-paren :lex "("
                             :prefix (:left-precedence 200 :right-precedence 0
                                      :context (:open \| right-paren)))

   ;; hyphens can be generated only by replacement of <minus>
   ;; Precedence puts hyphen above comma in parsetree --
   (def-syntactic hyphen :lex "-" :infix (:precedence 17 :context :binary)
       :tidier
          ;; Eliminate commas --
          ((:? ?(:^+ hyphen (:^+ comma ?@vars) ?type)
             !~(:^+ hyphen ,@vars ,type)))

       :checkers
          ((:? ?(:^+ hyphen ?@vars ?_)
             (and (not (is-list-of vars #'is-Symbol))
                  (defect "Vars in declarations are not all symbols: "
                                  vars)))

           (:? ?(:^+ hyphen ?@_ (:^+ comma ?@_))
              (defect "Comma occurs to right of hyphen"))))
 )) 

(defun is-name (x)
   (or (is-Symbol x)
       (matchq ?(:^+ name-wrt-space ?_ ?_)
               x)))