Add a print primitive

lexer.mll

 {
   open Parser
   exception Unexpected_char of string
+  exception End_of_file_looking_for_double_quotes
+
+  let chars_read = ref ""
+  let add_char c = chars_read := Printf.sprintf "%s%c" !chars_read c
+
+  let flush () = chars_read := ""
 }
 
 let id = [ 'a'-'z' '_' '0'-'9' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']*
@@ -28,7 +34,17 @@ rule token = parse
     | "let" { VAR (Parsing.rhs_start_pos 1) }
     | "check" { CHECK (Parsing.rhs_start_pos 1) }
     | "norm" { NORM (Parsing.rhs_start_pos 1) }
+    | "print" { PRINT (Parsing.rhs_start_pos 1) }
     | id as s { ID (s) }
     | [ 'A'-'Z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s { CID (s) }
+    | '"' { flush (); string lexbuf }
     | _ as c { raise (Unexpected_char (Printf.sprintf"'%c'" c)) }
     | eof { raise End_of_file }
+
+and string = parse
+    | "\\n" { add_char '\n'; string lexbuf }
+    | '\\' (_ as c) { add_char '\\'; add_char c; string lexbuf }
+    | '\n' { Lexing.new_line lexbuf ; add_char '\n'; string lexbuf }
+    | '"'  { STRING (!chars_read) }
+    | _ as c { add_char c; string lexbuf }
+    | eof { raise End_of_file_looking_for_double_quotes }

parser.mly

@@ -25,10 +25,10 @@
 
 %}
 
-%token <string> ID CID SELECT UPDATE FUPD
+%token <string> ID CID SELECT UPDATE FUPD STRING
 %token LBRACK RBRACK COLUMN SEMICOLUMN LPAR RPAR SIGMA EQUAL DEF DOT
 %token LAMBDA ARR
-%token <Lexing.position> TYPE VAR CHECK NORM
+%token <Lexing.position> TYPE VAR CHECK NORM PRINT
 
 %right ARR
 
@@ -42,6 +42,7 @@ line:   TYPE CID DEF ty DOT                     { ($1, Typedef (Cid ($2), $4)) }
       | CHECK term COLUMN ty DOT                { ($1, Check ($2, $4)) }
       | CHECK term EQUAL term COLUMN ty DOT     { ($1, Conv ($2, $4, $6)) }
       | NORM term DOT                           { ($1, Norm ($2)) }
+      | PRINT STRING DOT                        { ($1, Print ($2)) }
 ;
 
 ty:   CID                         { Tcid (Cid ($1)) }

parsetree.mli

@@ -28,4 +28,5 @@ type line =
 | Check of term * stype
 | Conv of term * term * stype
 | Norm of term
+| Print of string
 ;;

printer.ml

@@ -133,5 +133,7 @@ let print_line out_fmter = function
   | Tnorm t ->
     Format.fprintf out_fmter "@[<h>#SNF %a.@]@\n"
       print_term t
+  | Tprint s ->
+     Format.fprintf out_fmter "@[<h>#PRINT \"%s\".@]@\n" s
 
 let print out_fmter = List.iter (print_line out_fmter)

scoper.ml

@@ -27,6 +27,7 @@ type sline =
 | Scheck of sterm * sty
 | Sconv of sterm * sterm * sty
 | Snorm of sterm
+| Sprint of string
 
 type scoped_tree = sline list
 
@@ -99,7 +100,8 @@ let scope_line ty_env const_env = function
     let sty = scope_ty ty_env ty in
     (ty_env, const_env, Sconv (st1, st2, sty))
   | Norm t ->
-    (ty_env, const_env, Snorm (scope_term ty_env const_env [] t))
+     (ty_env, const_env, Snorm (scope_term ty_env const_env [] t))
+  | Print s -> (ty_env, const_env, Sprint s)
 
 let rec scope_prog ty_env const_env = function
   | [] -> []

scoper.mli

@@ -27,6 +27,7 @@ type sline =
 | Scheck of sterm * sty
 | Sconv of sterm * sterm * sty
 | Snorm of sterm
+| Sprint of string
 
 type scoped_tree = sline list
 

typer.ml

@@ -19,6 +19,7 @@ type tline =
 | Tcheck of tterm * sty
 | Tconv of tterm * tterm * sty
 | Tnorm of tterm
+| Tprint of string
 
 type typed_tree = tline list
 
@@ -216,5 +217,6 @@ let type_line = function
     let tt2 = type_check [] ty t2 in
     Tconv (tt1, tt2, ty)
   | Snorm t -> Tnorm (type_term [] t)
+  | Sprint s -> Tprint s
 
 let type_check = List.map type_line

typer.mli

@@ -19,6 +19,7 @@ type tline =
 | Tcheck of tterm * sty
 | Tconv of tterm * tterm * sty
 | Tnorm of tterm
+| Tprint of string
 
 type typed_tree = tline list