let trust = true let outfname = match Sys.argv.(1) with | "-help" | "--help" | "-h" | "--h" -> print_endline ("Usage: create_environment \n" ^ " is the file where environment will be dumped\n" ^ " is the file containing the URIs, one per line,\n" ^ " that will be typechecked. Could be \"-\" for\n" ^ " standard input"); flush stdout; exit 0 | f -> f let _ = CicEnvironment.set_trust (fun _ -> trust); Helm_registry.set "getter.mode" "remote"; Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/"; Sys.catch_break true; if Sys.file_exists outfname then begin let ic = open_in outfname in CicEnvironment.restore_from_channel ic; close_in ic end let urifname = try Sys.argv.(2) with Invalid_argument _ -> "-" let ic = match urifname with | "-" -> stdin | fname -> open_in fname let _ = try while true do (* try *) let uri = input_line ic in print_endline uri; flush stdout; let uri = UriManager.uri_of_string uri in ignore (CicTypeChecker.typecheck uri CicUniv.empty_ugraph) (* with Sys.Break -> () *) done with End_of_file | Sys.Break -> let oc = open_out outfname in CicEnvironment.dump_to_channel oc; close_out oc