annotate tools/make_template.ml @ 64:739c2818d6e2

Co-inductive evaluation example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 30 Sep 2008 17:47:59 -0400
parents 827d7e8a7d9e
children d07c77659c20
rev   line source
adamc@23 1 let read_line () =
adamc@22 2 try
adamc@23 3 Some (read_line ())
adamc@22 4 with End_of_file -> None
adamc@22 5
adamc@22 6 let rec initial last_was_empty =
adamc@23 7 match read_line () with
adamc@22 8 | None -> ()
adamc@22 9 | Some "(* begin thide *)" -> thide last_was_empty
adamc@22 10 | Some "" ->
adamc@22 11 if not (last_was_empty) then
adamc@22 12 print_newline ();
adamc@22 13 initial true
adamc@22 14 | Some line ->
adamc@41 15 let idx = try Some (String.index line '(') with Not_found -> None in
adamc@41 16 match idx with
adamc@41 17 | Some idx ->
adamc@49 18 if String.length line > idx+1 && line.[idx+1] = '*'
adamc@49 19 && not (String.length line > idx+4 && String.sub line (idx+2) 3 = " EX") then
adamc@41 20 if line.[String.length line - 2] = '*' && line.[String.length line - 1] = ')' then
adamc@41 21 initial last_was_empty
adamc@41 22 else
adamc@41 23 comment last_was_empty
adamc@41 24 else begin
adamc@41 25 print_endline line;
adamc@41 26 initial false
adamc@41 27 end
adamc@41 28 | None ->
adamc@41 29 print_endline line;
adamc@41 30 initial false
adamc@22 31
adamc@22 32 and comment last_was_empty =
adamc@23 33 match read_line () with
adamc@22 34 | None -> ()
adamc@22 35 | Some line ->
adamc@22 36 if String.length line >= 2 && line.[String.length line - 2] = '*'
adamc@22 37 && line.[String.length line - 1] = ')' then
adamc@22 38 initial last_was_empty
adamc@22 39 else
adamc@22 40 comment last_was_empty
adamc@22 41
adamc@22 42 and thide last_was_empty =
adamc@23 43 match read_line () with
adamc@22 44 | None -> ()
adamc@22 45 | Some "(* end thide *)" -> initial last_was_empty
adamc@22 46 | Some _ -> thide last_was_empty
adamc@22 47
adamc@22 48 let () = initial false