Mercurial > cpdt > repo
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 |