Mercurial > cpdt > repo
annotate tools/make_template.ml @ 36:9e46ade5af21
Manual Proofs About Constructors
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 12 Sep 2008 14:59:08 -0400 |
parents | c8070689f5ca |
children | d45ba7e9b266 |
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@22 | 15 if String.length line >= 2 && line.[0] = '(' && line.[1] = '*' then |
adamc@22 | 16 if line.[String.length line - 2] = '*' && line.[String.length line - 1] = ')' then |
adamc@22 | 17 initial last_was_empty |
adamc@22 | 18 else |
adamc@22 | 19 comment last_was_empty |
adamc@22 | 20 else begin |
adamc@22 | 21 print_endline line; |
adamc@22 | 22 initial false |
adamc@22 | 23 end |
adamc@22 | 24 |
adamc@22 | 25 and comment last_was_empty = |
adamc@23 | 26 match read_line () with |
adamc@22 | 27 | None -> () |
adamc@22 | 28 | Some line -> |
adamc@22 | 29 if String.length line >= 2 && line.[String.length line - 2] = '*' |
adamc@22 | 30 && line.[String.length line - 1] = ')' then |
adamc@22 | 31 initial last_was_empty |
adamc@22 | 32 else |
adamc@22 | 33 comment last_was_empty |
adamc@22 | 34 |
adamc@22 | 35 and thide last_was_empty = |
adamc@23 | 36 match read_line () with |
adamc@22 | 37 | None -> () |
adamc@22 | 38 | Some "(* end thide *)" -> initial last_was_empty |
adamc@22 | 39 | Some _ -> thide last_was_empty |
adamc@22 | 40 |
adamc@22 | 41 let () = initial false |