-
Notifications
You must be signed in to change notification settings - Fork 13
/
parse.clj
108 lines (94 loc) · 4.41 KB
/
parse.clj
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
;;{
;; # Parsing tools
;;
;; In this namespace all the user-facing syntactic artefacts of LaTTe
;; are checked for well-formedness. This is not concerned with term-level parsing.
;; The emphasis is on precision and clarity of (potential) error messages
;;}
(ns latte.parse
)
(declare check-def-name
parse-def-params)
(defn parse-definition [def-kind args]
(let [[def-Descr def-descr] (case def-kind
:definition ["Definition" "definition"]
:theorem ["Theorem" "theorem"]
:lemma ["Lemma" "lemma"]
:axiom ["Axiom" "axiom"]
(throw (ex-info "No such definition kind." {:def-kind def-kind})))]
(if (< (count args) 3)
[:ko (str def-Descr " form requires at least 3 arguments.") {:nb-args (count args)}]
(let [def-name (first args)
[status msg infos] (check-def-name def-name)]
(if (= status :ko)
[status msg infos]
(let [def-doc (if (string? (second args))
(second args)
nil)]
(if (and def-doc
(< (count args) 4))
[:ko (str def-Descr " form (with docstring) requires at least 4 arguments.")
{:name def-name
:nb-args (count args)}]
(let [params (if def-doc
(nth args 2)
(second args))
[status def-params infos] (parse-def-params params)]
(if (= status :ko)
[:ko "Cannot parse parameter list" {:name def-name
:from (assoc infos :msg def-params)}]
(if (or (and def-doc (> (count args) 4))
(and (nil? def-doc) (> (count args) 3)))
[:ko (str "Too many arguments for " def-descr ".") {:name def-name
:nb-args (count args)
:garbage (drop 4 args)}]
;; everything's fine
[:ok "" {:name def-name
:doc def-doc
:params def-params
:body (if def-doc
(nth args 3)
(nth args 2))}]))))))))))
(defn check-def-name [name]
(if (symbol? name)
[:ok name nil]
[:ko "Definition name must be a symbol." {:name name}]))
(defn parse-def-params [params]
(if (not (vector? params))
[:ko "Parameters must be specifed as a vector." {:params params}]
(loop [params params, pname nil, def-params []]
(if (seq params)
(cond
(vector? (first params))
(let [param (first params)]
(cond
(not (nil? pname))
[:ko "Expecting a parameter type, not a pair." {:param-name pname
:param-type param}]
(< (count param) 2)
[:ko "Wrong parameter syntax." {:param param}]
:else
(let [ptype (last param)
[status msg res]
(loop [names (butlast param), nparams def-params]
(if (seq names)
(if (not (symbol? (first names)))
[:ko "Parameter name must be a symbol." {:param param
:name (first names)}]
(recur (rest names) (conj nparams [(first names) ptype])))
;; no more names
[:ok "" nparams]))]
(if (= status :ko)
[:ko msg res]
(recur (rest params) nil res)))))
;; a non-vector parameter
(nil? pname)
(if (not (symbol? (first params)))
[:ko "Expecting a parameter name as a symbol." {:param (first params)}]
(recur (rest params) (first params) def-params))
:else ;; type part
(recur (rest params) nil (conj def-params [pname (first params)])))
;; no more parameters
(if (not (nil? pname))
[:ko "Parameter is without a type." {:param-name pname}]
[:ok def-params nil])))))