Commits

Sébastien Ferré committed c15116f

Fusion of Ident, Term, and symbols.

  • Participants
  • Parent commits cab77bf

Comments (0)

Files changed (1)

 open Token
 
 (* forbidden idents in syntax of logics *)
-let keywords = ["all";"none";"and";"or";"not";"except";"implies";"only"]
+let keywords = ["thing";"nothing";"and";"or";"not";"except";"implies";"if";"then";"else";"some";"every";"only";"something";"the";"of";"by";"with";"is";"trans";"opt";"co";"share";"a";"an";"this";"that";"whose"]
 
 let not_PP t = not (Token.is_PP t)
 (*
     for i=0 to l1-1 do
       if s.[i] = '"' then Buffer.add_string buf "\\\""
       else if s.[i] = '\\' then Buffer.add_string buf "\\\\"
+      else if s.[i] = '\n' then Buffer.add_string buf "\\n"
+      else if s.[i] = '\t' then Buffer.add_string buf "\\t"
       else Buffer.add_char buf s.[i]
     done;
     Buffer.contents buf
 let wrong_fact spec s = "Syntax error: '(', '" ^ spec.n ^ "' or atom expected after '" ^ s ^ "'"
 
 let rec parse_prop spec = parser
-  | [<'Token.Ident s when s = spec.all >] -> spec.taut
-  | [<'Token.Ident s when s = spec.none>] -> spec.cont
   | [<q = parse_term spec; f = parse_suite spec>] -> f q
 and parse_suite spec = parser
-    [<'Token.Ident s when s = spec.a; q = parse_prop spec ?? wrong_prop spec s>] -> (fun q' -> spec.conj q' q)
-  | [<'Token.Ident s when s = spec.an; q = parse_fact spec ?? wrong_fact spec s>] -> (fun q' -> spec.conj q' (spec.neg q))
+  | [<'Token.Ident s when s = spec.o; q = parse_prop spec ?? wrong_prop spec s>] -> (fun q' -> spec.disj q' q)
   | [<>] -> (fun q' -> q')
 and parse_term spec = parser
   | [<q = parse_fact spec; f = parse_term_suite spec>] -> f q
 and parse_term_suite spec = parser
-  | [<'Token.Ident s when s = spec.o; q = parse_term spec ?? wrong_term spec s>] -> (fun q' -> spec.disj q' q)
+    [<'Token.Ident s when s = spec.a; q = parse_term spec ?? wrong_term spec s>] -> (fun q' -> spec.conj q' q)
+  | [<'Token.Ident s when s = spec.an; q = parse_fact spec ?? wrong_fact spec s>] -> (fun q' -> spec.conj q' (spec.neg q))
   | [<>] -> (fun q' -> q')
 and parse_fact spec = parser
   | [<'Token.LeftPar; q = parse_prop spec ?? wrong_prop spec "("; 'Token.RightPar ?? "Syntax error: missing ')' after proposition">] -> q
+  | [<'Token.Ident s when s = spec.all >] -> spec.taut
+  | [<'Token.Ident s when s = spec.none>] -> spec.cont
   | [<'Token.Ident s when s = spec.n; q = parse_fact spec ?? wrong_fact spec s>] -> spec.neg q
   | [<a = spec.atom>] -> a