Added some congruence functions and empty commands

Makefile

 RESULT := pga
-BASENAMES := types stringify parser lexer parse pga
+BASENAMES := types stringify parser lexer parse congruence pga
 
 OFILES := $(addsuffix .cmx,$(BASENAMES))
 

congruence.ml

+open Types
+
+let rec unfold_repeat = function
+  | Repeat (_, 0) as i :: _ ->
+    raise (Ins_error (i, "cannot repeat 0 times"))
+  | Repeat (i, 1) :: tl ->
+    i :: unfold_repeat tl
+  | Repeat (i, n) :: tl ->
+    i :: unfold_repeat (Repeat (i, n - 1) :: tl)
+  | hd :: tl ->
+    hd :: unfold_repeat tl
+  | [] -> []
+
+let rec norm = function
+  | [] -> N 0
+  | Repeat (i, t) :: tl -> norm [i] ** (N t) ++ norm tl
+  | Loop _ :: tl -> Infinity
+  | Concat l :: tl -> norm l ++ norm tl
+  | hd :: tl -> N 1 ++ norm tl

lexer.mll

@@ -2,7 +2,7 @@
 open Lexing
 open Parser
 
-exception SyntaxError of string
+exception Syntax_error of string
 
 let next_line lexbuf =
   let pos = lexbuf.lex_curr_p in
@@ -34,4 +34,4 @@ rule token = parse
   | [' ''\t']+            { token lexbuf }
   | eof | '\000'          { EOF }
 
-  | _ as chr { raise (SyntaxError ("unexpected '" ^ Char.escaped chr ^ "'")) }
+  | _ as chr { raise (Syntax_error ("unexpected '" ^ Char.escaped chr ^ "'")) }

parse.ml

@@ -17,7 +17,7 @@ let loc_msg lexbuf msg =
 
 let parse_with_error lexbuf =
   try Parser.program Lexer.token lexbuf with
-  | Lexer.SyntaxError msg ->
-    raise (FatalError (loc_msg lexbuf msg))
+  | Lexer.Syntax_error msg ->
+    raise (Fatal_error (loc_msg lexbuf msg))
   | Parser.Error ->
-    raise (FatalError (loc_msg lexbuf "syntax error"))
+    raise (Fatal_error (loc_msg lexbuf "syntax error"))

pga.ml

@@ -11,14 +11,17 @@ let main () =
     prerr_endline "  latex TERM   print latex source for a program";
     prerr_endline "  norm TERM    get the norm of a program";
     prerr_endline "  i I TERM     get the Ith instruction of a program";
+    prerr_endline "  canon1 TERM  transform to first canonical form";
+    prerr_endline "  canon2 TERM  transform to second canonical form";
+    prerr_endline "  eq TERM TERM check for instruction-row equivalence";
     prerr_endline "  dot TERM     generate Dot code for a flow graph";
     prerr_endline "input program syntax:";
     prerr_endline "  - write star (*) instead of omega sign";
     prerr_endline "  - write dollar sign ($) instead of pound sign";
     prerr_endline "";
-    prerr_endline "A TERM argument may also be omitted and passed on stdin";
-    prerr_endline "instead for convenient use of UNIX pipes, e.g.:";
-    prerr_endline "$ ./pga echo 'a;b;(c)*' | ./pga dot | dot -T png | display";
+    prerr_endline "A single TERM argument may also be omitted and passed on";
+    prerr_endline "stdin instead for convenient use of UNIX pipes, e.g.:";
+    prerr_endline "$ ./pga canon1 '(a)*;!' | ./pga dot | dot -T png | display";
     exit status
   in
 
@@ -45,14 +48,22 @@ let main () =
         print_endline (string_of_program_utf8 (input_term 2))
       | "latex" ->
         print_endline (string_of_program_latex (input_term 2))
-      | "norm" | "i" | "dot" ->
+      | "norm" ->
+        print_endline (string_of_natural (Congruence.norm (input_term 2)))
+      | "i" | "canon1" | "canon2" | "eq" | "dot" ->
         raise (Failure "not implemented")
       | _ ->
         usage 1
     with
-    | FatalError msg ->
+    | Fatal_error msg ->
       prerr_endline msg;
       exit 1
+    | Ins_error (i, msg) ->
+      prerr_endline ("error on " ^ string_of_ins_ascii i ^ ": " ^ msg);
+      exit 1
+    | Program_error (p, msg) ->
+      prerr_endline ("error on " ^ string_of_program_ascii p ^ ": " ^ msg);
+      exit 1
   end;
 
   exit 0

stringify.ml

@@ -44,3 +44,7 @@ let string_of_program_utf8 instrs =
 
 let string_of_program_latex instrs =
   "$" ^ String.concat ";" (List.map string_of_ins_latex instrs) ^ "$"
+
+let string_of_natural = function
+  | N i      -> string_of_int i
+  | Infinity -> "oo"

types.ml

@@ -14,4 +14,19 @@ type ins =
 
 type program = ins list
 
-exception FatalError of string
+(* Natural numbers *)
+type natural = Infinity | N of int
+
+let natural_binop binop a b =
+  match (a, b) with
+  | N i, N j -> N (binop i j)
+  | _ -> Infinity
+
+let ( ++ ) = natural_binop ( + )
+let ( -- ) = natural_binop ( - )
+let ( ** ) = natural_binop ( * )
+let ( // ) = natural_binop ( / )
+
+exception Fatal_error of string
+exception Ins_error of ins * string
+exception Program_error of program * string