Commits

Sébastien Ferré committed 7bdf173

generic parser of propositionnal languages.

Comments (0)

Files changed (1)

   fun toks ->
     pp_print_tokens Format.std_formatter toks
 
-(* fonctions generiques pour le parsing *)
-
-
 (* fonctions generiques pour le printing *)
 (* ------------------------------------- *)
 
+(* messages d'erreur syntaxique *)
+
+let error_RightPar = "Syntax error: a closing parenthesis is missing."
+let error_RightBra = "Syntax error: a closing bracket is missing."
+
 (* add parenthesis around the given t_list if op (precedence) is above the ctx (precedence) *)
 
 let add_par : int -> int -> t_list -> t_list =
   fun ctx op l -> if op > ctx then LeftPar::(l @ [RightPar]) else l
 
+(* fonctions generiques pour le parsing *)
+(* ------------------------------------ *)
+
+(* parsing of proposition-like language, where operations and atoms are parameterized *)
+
+type 'a spec_prop = { 
+    all : string; none : string; a : string; an : string; o : string; n :  string;
+    taut : 'a; cont : 'a; neg : 'a -> 'a; conj : 'a -> 'a -> 'a; disj : 'a -> 'a -> 'a;
+      atom : t_stream -> 'a
+  } 
+
+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>] -> (fun q' -> spec.conj q' q)
+  | [<'Token.Ident s when s = spec.an; q = parse_fact spec>] -> (fun q' -> spec.conj q' (spec.neg 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>] -> (fun q' -> spec.disj q' q)
+  | [<>] -> (fun q' -> q')
+and parse_fact spec = parser
+  | [<'Token.LeftPar; q = parse_prop spec; 'Token.RightPar ?? error_RightPar>] -> q
+  | [<'Token.Ident s when s = spec.n; q = parse_fact spec>] -> spec.neg q
+  | [<a = spec.atom>] -> a
 
-(* messages d'erreur syntaxique *)
-
-let error_RightPar = "Syntax error: a closing parenthesis is missing."
-let error_RightBra = "Syntax error: a closing bracket is missing."