From fe28d6a93686eca649c3a8db7eb3c4b6e363e511 Mon Sep 17 00:00:00 2001 From: Gabriel Kerneis Date: Wed, 23 Apr 2014 14:58:34 +0100 Subject: Rename main to sail, build pretty_printer lib --- src/Makefile | 11 +- src/main.ml | 414 ---------------------------------------------------- src/myocamlbuild.ml | 4 +- src/sail.ml | 414 ++++++++++++++++++++++++++++++++++++++++++++++++++++ src/sail.odocl | 2 +- 5 files changed, 424 insertions(+), 421 deletions(-) delete mode 100644 src/main.ml create mode 100644 src/sail.ml (limited to 'src') diff --git a/src/Makefile b/src/Makefile index e6849b07..a1ce3583 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,14 +1,14 @@ -.PHONY: all test clean doc update_lem_lib test_power +.PHONY: all test clean doc lib test_power -all: - ocamlbuild -classic-display main.native test/run_tests.native +all: lib doc + ocamlbuild -classic-display sail.native test/run_tests.native test: all ./run_tests.native test_power: #../../../rsem/idl/power/binary/run.sh - SAIL_OPTS=-skip_constraints ocamlbuild -classic-display main.native test/run_power.native + SAIL_OPTS=-skip_constraints ocamlbuild -classic-display sail.native test/run_power.native ./run_power.native --file ../../../rsem/idl/power/binary/main.bin clean: @@ -21,3 +21,6 @@ clean: doc: ocamlbuild sail.docdir/index.html + +lib: + ocamlbuild pretty_print.cmxa pretty_print.cma diff --git a/src/main.ml b/src/main.ml deleted file mode 100644 index b0957f91..00000000 --- a/src/main.ml +++ /dev/null @@ -1,414 +0,0 @@ -(**************************************************************************) -(* Lem *) -(* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) -(* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) -(* *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) -(**************************************************************************) - -open Process_file -(*open Debug - -let backends = ref [] -let opt_print_types = ref false -let opt_print_version = ref false -let opt_library = ref (Some (Build_directory.d^"/library")) -let lib = ref [] -let ocaml_lib = ref [] -let hol_lib = ref [] -let coq_lib = ref [] -let isa_lib = ref [] -let isa_theory = ref None -let opt_file_arguments = ref ([]:string list) - -let options = Arg.align ([ - ( "-i", - Arg.String (fun l -> lib := l::!lib), - " treat the file as input only and generate no output for it"); - ( "-tex", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then - backends := Some(Typed_ast.Target_tex)::!backends), - " generate LaTeX"); - ( "-html", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then - backends := Some(Typed_ast.Target_html)::!backends), - " generate Html"); - ( "-hol", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then - backends := Some(Typed_ast.Target_hol)::!backends), - " generate HOL"); - ( "-ocaml", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then - backends := Some(Typed_ast.Target_ocaml)::!backends), - " generate OCaml"); - ( "-isa", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_isa)) !backends) then - backends := Some(Typed_ast.Target_isa)::!backends), - " generate Isabelle"); - ( "-coq", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_coq)) !backends) then - backends := Some(Typed_ast.Target_coq)::!backends), - " generate Coq"); - ( "-ident", - Arg.Unit (fun b -> if not (List.mem None !backends) then - backends := None::!backends), - " generate input on stdout"); - ( "-print_types", - Arg.Unit (fun b -> opt_print_types := true), - " print types on stdout"); - ( "-lib", - Arg.String (fun l -> opt_library := Some l), - " library path"^match !opt_library with None->"" | Some s -> " (default "^s^")"); - ( "-ocaml_lib", - Arg.String (fun l -> ocaml_lib := l::!ocaml_lib), - " add to OCaml library"); - ( "-hol_lib", - Arg.String (fun l -> hol_lib := l::!hol_lib), - " add to HOL library"); - ( "-isa_lib", - Arg.String (fun l -> isa_lib := l::!isa_lib), - " add to Isabelle library"); - ( "-isa_theory", - Arg.String (fun l -> isa_theory := Some l), - " Isabelle Lem theory"); - ( "-coq_lib", - Arg.String (fun l -> coq_lib := l::!coq_lib), - " add to Coq library"); - ( "-v", - Arg.Unit (fun b -> opt_print_version := true), - " print version"); - ( "-ident_pat_compile", - Arg.Unit (fun b -> Target_trans.ident_force_pattern_compile := true; Reporting.ignore_pat_compile_warnings()), - " activates pattern compilation for the identity backend. This is used for debugging."); - ( "-only_changed_output", - Arg.Unit (fun b -> Process_file.always_replace_files := false), - " generate only output files, whose content really changed compared to the existing file"); - ( "-extra_level", - Arg.Symbol (["none"; "auto"; "all"], (fun s -> - Backend.gen_extra_level := (match s with - | "none" -> 0 - | "auto" -> 1 - | _ -> 2))), - " generate no (none) extra-information, only extras that can be handled automatically (auto) or all (all) extra information") -] @ Reporting.warn_opts) - -let usage_msg = - ("Lem " ^ Version.v ^ "\n" - ^ "example usage: lem -hol -ocaml -lib ../lem/library test.lem\n" - ) - -let _ = - Arg.parse options - (fun s -> - opt_file_arguments := (!opt_file_arguments) @ [s]) - usage_msg - - -let check_modules (def_info,env) modules = - (* The checks. Modify these lists to add more. *) - let exp_checks env = [Patterns.check_match_exp_warn env] in - let pat_checks env = [] in - let def_checks env = [Patterns.check_match_def_warn env] in - - (* Use the Macro_expander to execute these checks *) - let (d,_) = def_info in - let module Ctxt = struct let avoid = None let check = Some(d) end in - let module M = Macro_expander.Expander(Ctxt) in - let exp_mac env = Macro_expander.list_to_mac (List.map (fun f e -> (let _ = f e in None)) (exp_checks env)) in - let exp_ty env ty = ty in - let exp_src_ty env src_t = src_t in - let exp_pat env = Macro_expander.list_to_bool_mac (List.map (fun f x p -> (let _ = f x p in None)) (pat_checks env)) in - let check_defs env defs = begin - let _ = M.expand_defs (List.rev defs) (exp_mac env, exp_ty env, exp_src_ty env, exp_pat env) in - let _ = List.map (fun d -> List.map (fun c -> c d) (def_checks env)) defs in - () - end in - let check_module m = (let (defs, _) = m.Typed_ast.typed_ast in check_defs env defs) in - let _ = List.map check_module modules in - () - - -(* Do the transformations for a given target, and then generate the output files - * *) -let per_target libpath isa_thy modules (def_info,env) consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum targ = - let consts = List.assoc targ consts in - let module C = struct - let (d,i) = def_info - end - in - let module T = Target_trans.Make(C) in - let (trans,avoid) = T.get_transformation targ consts in - try - let (_,transformed_m) = - List.fold_left - (fun (env,new_mods) old_mod -> - let (env,m) = trans env old_mod in - (env,m::new_mods)) - (env,[]) - modules - in - let consts' = T.extend_consts targ consts transformed_m in - let transformed_m' = T.rename_def_params targ consts' transformed_m in - output libpath isa_thy targ (avoid consts') def_info (List.rev transformed_m') alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum - with - | Trans.Trans_error(l,msg) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans (l, msg))) - | Ident.No_type(l,msg) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal (l, msg))) - | Typed_ast.Renaming_error(ls,msg) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_rename (ls, msg))) - - -let main () = - let _ = if !opt_print_version then print_string ("Lem " ^ Version.v ^ "\n") in - let lib_path = - match !opt_library with - | None -> (try - let lp = Sys.getenv("LEMLIB") in - if Filename.is_relative lp - then Filename.concat (Sys.getcwd ()) lp - else lp - with - | Not_found -> raise (Failure("must specify a -lib argument or have a LEMLIB environment variable"))) - | Some lp -> - if Filename.is_relative lp then - Filename.concat (Sys.getcwd ()) lp - else - lp - in - let isa_thy = - match !isa_theory with - | None -> Filename.concat lib_path "../isabelle-lib/Lem" - | Some thy -> thy - in - let _ = - List.iter - (fun f -> - try - if String.compare ".lem" (String.sub f (String.length f - 4) 4) <> 0 then - raise (Failure("Files must have .lem extension")) - with - | Invalid_argument _ -> - raise (Failure("Files must have .lem extension"))) - (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib) - in - let _ = - List.iter - (fun f -> - if not (Str.string_match (Str.regexp "[A-Za-z]") (Filename.basename f) 0) then - raise (Failure(".lem filenames must start with a letter"))) - (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib) - in - let init = - try - let inchannel = open_in (Filename.concat lib_path "lib_cache") in - let v = input_value inchannel in - close_in inchannel; - v - with - | Sys_error _ -> - let module I = Initial_env.Initial_libs(struct let path = lib_path end) in - let outchannel = open_out (Filename.concat lib_path "lib_cache") in - output_value outchannel I.init; - close_out outchannel; - I.init - in - (* TODO: These should go into the sets of top-level constant names *) - let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_hol) !hol_lib init in - let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_ocaml) !ocaml_lib init in - let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_isa) !isa_lib init in - let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_coq) !coq_lib init in - - let consts = - List.map - (fun (targ,cL) -> - let consts = List.fold_left - (fun s c -> Typed_ast.NameSet.add (Name.from_rope c) s) - Typed_ast.NameSet.empty - cL in - (targ,consts)) - (snd init) - in - let type_info : (Types.type_defs * instances) * Typed_ast.env = fst init in - (* Parse and typecheck all of the .lem sources *) - let (modules, type_info, _) = - List.fold_left - (fun (mods, (def_info,env), previously_processed_modules) (f, add_to_modules) -> - let ast = parse_file f in - let f' = Filename.basename (Filename.chop_extension f) in - let mod_name = String.capitalize f' in - let mod_name_name = Name.from_rope (Ulib.Text.of_latin1 mod_name) in - let backend_set = - List.fold_right - (fun x s -> - match x with - | None -> s - | Some(Typed_ast.Target_tex) -> s - | Some(Typed_ast.Target_html) -> s - | Some(t) -> Typed_ast.Targetset.add t s) - !backends - Typed_ast.Targetset.empty - in - let ((tdefs,instances,new_instances),new_env,tast) = - check_ast backend_set [mod_name_name] (def_info,env) ast - in - let md = { Typed_ast.mod_env = new_env; Typed_ast.mod_binding = Path.mk_path [] mod_name_name } in - let e = { env with Typed_ast.m_env = Typed_ast.Nfmap.insert env.Typed_ast.m_env (mod_name_name,md) } in - let module_record = - { Typed_ast.filename = f; - Typed_ast.module_name = mod_name; - Typed_ast.predecessor_modules = previously_processed_modules; - Typed_ast.untyped_ast = ast; - Typed_ast.typed_ast = tast; } - in - if !opt_print_types then - begin - (* - Format.fprintf Format.std_formatter "%s@\nlibrary:@\n" f; - Typed_ast.pp_env Format.std_formatter (snd type_info); - *) - Format.fprintf Format.std_formatter "%s@\nenvironment:@\n" f; - Typed_ast.pp_env Format.std_formatter new_env; - Format.fprintf Format.std_formatter "@\ninstances:@\n"; - Typed_ast.pp_instances Format.std_formatter new_instances; - Format.fprintf Format.std_formatter "@\n@\n" - end; - ((if add_to_modules then - module_record::mods - else - mods), - ((tdefs,instances),e), mod_name::previously_processed_modules)) - ([],type_info,[]) - (* We don't want to add the files in !lib to the resulting module ASTs, - * because we don't want to put them throught the back end *) - (List.map (fun x -> (x, false)) (List.rev !lib) @ - List.map (fun x -> (x, true)) !opt_file_arguments) - in - - (* Check the parsed source and produce warnings for various things. Currently: - - non-exhaustive and redundant patterns - *) - let _ = check_modules type_info modules in - - let alldoc_accum = ref ([] : Ulib.Text.t list) in - let alldoc_inc_accum = ref ([] : Ulib.Text.t list) in - let alldoc_inc_usage_accum = ref ([] : Ulib.Text.t list) in - ignore (List.iter (per_target lib_path isa_thy (List.rev modules) type_info consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) !backends); - (if List.mem (Some(Typed_ast.Target_tex)) !backends then - output_alldoc "alldoc" (String.concat " " !opt_file_arguments) alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) - -let _ = - try - begin - try ignore(main ()) - with Failure(s) -> raise (Reporting_basic.err_general false Ast.Unknown ("Failure "^s)) - end - with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e - -*) - -let lib = ref [] -let opt_print_version = ref false -let opt_print_verbose = ref false -let opt_print_lem = ref false -let opt_file_arguments = ref ([]:string list) -let options = Arg.align ([ - ( "-i", - Arg.String (fun l -> lib := l::!lib), - " treat the file as input only and generate no output for it"); - (*( "-tex", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then - backends := Some(Typed_ast.Target_tex)::!backends), - " generate LaTeX"); - ( "-html", - Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then - backends := Some(Typed_ast.Target_html)::!backends), - " generate Html"); - ( "-ident", - Arg.Unit (fun b -> if not (List.mem None !backends) then - backends := None::!backends), - " generate input on stdout");*) - ( "-verbose", - Arg.Unit (fun b -> opt_print_verbose := true), - " pretty-print out the file"); - ( "-lem_ast", - Arg.Unit (fun b -> opt_print_lem := true), - " pretty-print a Lem AST representation of the file"); - ( "-skip_constraints", - Arg.Clear Type_internal.do_resolve_constraints, - " skip constraint resolution in type-checking"); - ( "-v", - Arg.Unit (fun b -> opt_print_version := true), - " print version"); -] ) - -let usage_msg = - ("L2 " ^ "pre alpha" ^ "\n" - ^ "example usage: l2 test.ltwo\n" - ) - -let _ = - Arg.parse options - (fun s -> - opt_file_arguments := (!opt_file_arguments) @ [s]) - usage_msg - -let main() = - if !(opt_print_version) - then Printf.printf "L2 pre alpha \n" - else let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in - let asts = (List.map (fun (f,past) -> (f,convert_ast past)) parsed) in - let chkedasts = (List.map (fun (f,(ast,kenv)) -> (f,check_ast ast kenv)) asts) in - begin - (if !(opt_print_verbose) - then ((Pretty_print.pp_defs Format.std_formatter) (snd (List.hd chkedasts))) - else ()); - (if !(opt_print_lem) - then output "" Lem_ast_out chkedasts - else ()); - end - -let _ = try - begin - try ignore(main ()) - with Failure(s) -> raise (Reporting_basic.err_general Parse_ast.Unknown ("Failure "^s)) - end - with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml index ecd86adc..70e2b633 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -46,7 +46,7 @@ dispatch begin function rule "sail -> lem" ~prod: "%.lem" - ~deps: ["%.sail"; "main.native"] + ~deps: ["%.sail"; "sail.native"] (fun env builder -> let sail_opts = List.map (fun s -> A s) ( "-lem_ast" :: @@ -54,7 +54,7 @@ dispatch begin function split ',' (Sys.getenv "SAIL_OPTS") with Not_found -> []) in Seq [ - Cmd (S ([ P "./main.native"] @ sail_opts @ [P (env "%.sail")])); + Cmd (S ([ P "./sail.native"] @ sail_opts @ [P (env "%.sail")])); mv (basename (env "%.lem")) (dirname (env "%.lem")) ]); diff --git a/src/sail.ml b/src/sail.ml new file mode 100644 index 00000000..b0957f91 --- /dev/null +++ b/src/sail.ml @@ -0,0 +1,414 @@ +(**************************************************************************) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(**************************************************************************) + +open Process_file +(*open Debug + +let backends = ref [] +let opt_print_types = ref false +let opt_print_version = ref false +let opt_library = ref (Some (Build_directory.d^"/library")) +let lib = ref [] +let ocaml_lib = ref [] +let hol_lib = ref [] +let coq_lib = ref [] +let isa_lib = ref [] +let isa_theory = ref None +let opt_file_arguments = ref ([]:string list) + +let options = Arg.align ([ + ( "-i", + Arg.String (fun l -> lib := l::!lib), + " treat the file as input only and generate no output for it"); + ( "-tex", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then + backends := Some(Typed_ast.Target_tex)::!backends), + " generate LaTeX"); + ( "-html", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then + backends := Some(Typed_ast.Target_html)::!backends), + " generate Html"); + ( "-hol", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then + backends := Some(Typed_ast.Target_hol)::!backends), + " generate HOL"); + ( "-ocaml", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then + backends := Some(Typed_ast.Target_ocaml)::!backends), + " generate OCaml"); + ( "-isa", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_isa)) !backends) then + backends := Some(Typed_ast.Target_isa)::!backends), + " generate Isabelle"); + ( "-coq", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_coq)) !backends) then + backends := Some(Typed_ast.Target_coq)::!backends), + " generate Coq"); + ( "-ident", + Arg.Unit (fun b -> if not (List.mem None !backends) then + backends := None::!backends), + " generate input on stdout"); + ( "-print_types", + Arg.Unit (fun b -> opt_print_types := true), + " print types on stdout"); + ( "-lib", + Arg.String (fun l -> opt_library := Some l), + " library path"^match !opt_library with None->"" | Some s -> " (default "^s^")"); + ( "-ocaml_lib", + Arg.String (fun l -> ocaml_lib := l::!ocaml_lib), + " add to OCaml library"); + ( "-hol_lib", + Arg.String (fun l -> hol_lib := l::!hol_lib), + " add to HOL library"); + ( "-isa_lib", + Arg.String (fun l -> isa_lib := l::!isa_lib), + " add to Isabelle library"); + ( "-isa_theory", + Arg.String (fun l -> isa_theory := Some l), + " Isabelle Lem theory"); + ( "-coq_lib", + Arg.String (fun l -> coq_lib := l::!coq_lib), + " add to Coq library"); + ( "-v", + Arg.Unit (fun b -> opt_print_version := true), + " print version"); + ( "-ident_pat_compile", + Arg.Unit (fun b -> Target_trans.ident_force_pattern_compile := true; Reporting.ignore_pat_compile_warnings()), + " activates pattern compilation for the identity backend. This is used for debugging."); + ( "-only_changed_output", + Arg.Unit (fun b -> Process_file.always_replace_files := false), + " generate only output files, whose content really changed compared to the existing file"); + ( "-extra_level", + Arg.Symbol (["none"; "auto"; "all"], (fun s -> + Backend.gen_extra_level := (match s with + | "none" -> 0 + | "auto" -> 1 + | _ -> 2))), + " generate no (none) extra-information, only extras that can be handled automatically (auto) or all (all) extra information") +] @ Reporting.warn_opts) + +let usage_msg = + ("Lem " ^ Version.v ^ "\n" + ^ "example usage: lem -hol -ocaml -lib ../lem/library test.lem\n" + ) + +let _ = + Arg.parse options + (fun s -> + opt_file_arguments := (!opt_file_arguments) @ [s]) + usage_msg + + +let check_modules (def_info,env) modules = + (* The checks. Modify these lists to add more. *) + let exp_checks env = [Patterns.check_match_exp_warn env] in + let pat_checks env = [] in + let def_checks env = [Patterns.check_match_def_warn env] in + + (* Use the Macro_expander to execute these checks *) + let (d,_) = def_info in + let module Ctxt = struct let avoid = None let check = Some(d) end in + let module M = Macro_expander.Expander(Ctxt) in + let exp_mac env = Macro_expander.list_to_mac (List.map (fun f e -> (let _ = f e in None)) (exp_checks env)) in + let exp_ty env ty = ty in + let exp_src_ty env src_t = src_t in + let exp_pat env = Macro_expander.list_to_bool_mac (List.map (fun f x p -> (let _ = f x p in None)) (pat_checks env)) in + let check_defs env defs = begin + let _ = M.expand_defs (List.rev defs) (exp_mac env, exp_ty env, exp_src_ty env, exp_pat env) in + let _ = List.map (fun d -> List.map (fun c -> c d) (def_checks env)) defs in + () + end in + let check_module m = (let (defs, _) = m.Typed_ast.typed_ast in check_defs env defs) in + let _ = List.map check_module modules in + () + + +(* Do the transformations for a given target, and then generate the output files + * *) +let per_target libpath isa_thy modules (def_info,env) consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum targ = + let consts = List.assoc targ consts in + let module C = struct + let (d,i) = def_info + end + in + let module T = Target_trans.Make(C) in + let (trans,avoid) = T.get_transformation targ consts in + try + let (_,transformed_m) = + List.fold_left + (fun (env,new_mods) old_mod -> + let (env,m) = trans env old_mod in + (env,m::new_mods)) + (env,[]) + modules + in + let consts' = T.extend_consts targ consts transformed_m in + let transformed_m' = T.rename_def_params targ consts' transformed_m in + output libpath isa_thy targ (avoid consts') def_info (List.rev transformed_m') alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum + with + | Trans.Trans_error(l,msg) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans (l, msg))) + | Ident.No_type(l,msg) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal (l, msg))) + | Typed_ast.Renaming_error(ls,msg) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_rename (ls, msg))) + + +let main () = + let _ = if !opt_print_version then print_string ("Lem " ^ Version.v ^ "\n") in + let lib_path = + match !opt_library with + | None -> (try + let lp = Sys.getenv("LEMLIB") in + if Filename.is_relative lp + then Filename.concat (Sys.getcwd ()) lp + else lp + with + | Not_found -> raise (Failure("must specify a -lib argument or have a LEMLIB environment variable"))) + | Some lp -> + if Filename.is_relative lp then + Filename.concat (Sys.getcwd ()) lp + else + lp + in + let isa_thy = + match !isa_theory with + | None -> Filename.concat lib_path "../isabelle-lib/Lem" + | Some thy -> thy + in + let _ = + List.iter + (fun f -> + try + if String.compare ".lem" (String.sub f (String.length f - 4) 4) <> 0 then + raise (Failure("Files must have .lem extension")) + with + | Invalid_argument _ -> + raise (Failure("Files must have .lem extension"))) + (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib) + in + let _ = + List.iter + (fun f -> + if not (Str.string_match (Str.regexp "[A-Za-z]") (Filename.basename f) 0) then + raise (Failure(".lem filenames must start with a letter"))) + (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib) + in + let init = + try + let inchannel = open_in (Filename.concat lib_path "lib_cache") in + let v = input_value inchannel in + close_in inchannel; + v + with + | Sys_error _ -> + let module I = Initial_env.Initial_libs(struct let path = lib_path end) in + let outchannel = open_out (Filename.concat lib_path "lib_cache") in + output_value outchannel I.init; + close_out outchannel; + I.init + in + (* TODO: These should go into the sets of top-level constant names *) + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_hol) !hol_lib init in + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_ocaml) !ocaml_lib init in + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_isa) !isa_lib init in + let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_coq) !coq_lib init in + + let consts = + List.map + (fun (targ,cL) -> + let consts = List.fold_left + (fun s c -> Typed_ast.NameSet.add (Name.from_rope c) s) + Typed_ast.NameSet.empty + cL in + (targ,consts)) + (snd init) + in + let type_info : (Types.type_defs * instances) * Typed_ast.env = fst init in + (* Parse and typecheck all of the .lem sources *) + let (modules, type_info, _) = + List.fold_left + (fun (mods, (def_info,env), previously_processed_modules) (f, add_to_modules) -> + let ast = parse_file f in + let f' = Filename.basename (Filename.chop_extension f) in + let mod_name = String.capitalize f' in + let mod_name_name = Name.from_rope (Ulib.Text.of_latin1 mod_name) in + let backend_set = + List.fold_right + (fun x s -> + match x with + | None -> s + | Some(Typed_ast.Target_tex) -> s + | Some(Typed_ast.Target_html) -> s + | Some(t) -> Typed_ast.Targetset.add t s) + !backends + Typed_ast.Targetset.empty + in + let ((tdefs,instances,new_instances),new_env,tast) = + check_ast backend_set [mod_name_name] (def_info,env) ast + in + let md = { Typed_ast.mod_env = new_env; Typed_ast.mod_binding = Path.mk_path [] mod_name_name } in + let e = { env with Typed_ast.m_env = Typed_ast.Nfmap.insert env.Typed_ast.m_env (mod_name_name,md) } in + let module_record = + { Typed_ast.filename = f; + Typed_ast.module_name = mod_name; + Typed_ast.predecessor_modules = previously_processed_modules; + Typed_ast.untyped_ast = ast; + Typed_ast.typed_ast = tast; } + in + if !opt_print_types then + begin + (* + Format.fprintf Format.std_formatter "%s@\nlibrary:@\n" f; + Typed_ast.pp_env Format.std_formatter (snd type_info); + *) + Format.fprintf Format.std_formatter "%s@\nenvironment:@\n" f; + Typed_ast.pp_env Format.std_formatter new_env; + Format.fprintf Format.std_formatter "@\ninstances:@\n"; + Typed_ast.pp_instances Format.std_formatter new_instances; + Format.fprintf Format.std_formatter "@\n@\n" + end; + ((if add_to_modules then + module_record::mods + else + mods), + ((tdefs,instances),e), mod_name::previously_processed_modules)) + ([],type_info,[]) + (* We don't want to add the files in !lib to the resulting module ASTs, + * because we don't want to put them throught the back end *) + (List.map (fun x -> (x, false)) (List.rev !lib) @ + List.map (fun x -> (x, true)) !opt_file_arguments) + in + + (* Check the parsed source and produce warnings for various things. Currently: + - non-exhaustive and redundant patterns + *) + let _ = check_modules type_info modules in + + let alldoc_accum = ref ([] : Ulib.Text.t list) in + let alldoc_inc_accum = ref ([] : Ulib.Text.t list) in + let alldoc_inc_usage_accum = ref ([] : Ulib.Text.t list) in + ignore (List.iter (per_target lib_path isa_thy (List.rev modules) type_info consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) !backends); + (if List.mem (Some(Typed_ast.Target_tex)) !backends then + output_alldoc "alldoc" (String.concat " " !opt_file_arguments) alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) + +let _ = + try + begin + try ignore(main ()) + with Failure(s) -> raise (Reporting_basic.err_general false Ast.Unknown ("Failure "^s)) + end + with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e + +*) + +let lib = ref [] +let opt_print_version = ref false +let opt_print_verbose = ref false +let opt_print_lem = ref false +let opt_file_arguments = ref ([]:string list) +let options = Arg.align ([ + ( "-i", + Arg.String (fun l -> lib := l::!lib), + " treat the file as input only and generate no output for it"); + (*( "-tex", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then + backends := Some(Typed_ast.Target_tex)::!backends), + " generate LaTeX"); + ( "-html", + Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then + backends := Some(Typed_ast.Target_html)::!backends), + " generate Html"); + ( "-ident", + Arg.Unit (fun b -> if not (List.mem None !backends) then + backends := None::!backends), + " generate input on stdout");*) + ( "-verbose", + Arg.Unit (fun b -> opt_print_verbose := true), + " pretty-print out the file"); + ( "-lem_ast", + Arg.Unit (fun b -> opt_print_lem := true), + " pretty-print a Lem AST representation of the file"); + ( "-skip_constraints", + Arg.Clear Type_internal.do_resolve_constraints, + " skip constraint resolution in type-checking"); + ( "-v", + Arg.Unit (fun b -> opt_print_version := true), + " print version"); +] ) + +let usage_msg = + ("L2 " ^ "pre alpha" ^ "\n" + ^ "example usage: l2 test.ltwo\n" + ) + +let _ = + Arg.parse options + (fun s -> + opt_file_arguments := (!opt_file_arguments) @ [s]) + usage_msg + +let main() = + if !(opt_print_version) + then Printf.printf "L2 pre alpha \n" + else let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in + let asts = (List.map (fun (f,past) -> (f,convert_ast past)) parsed) in + let chkedasts = (List.map (fun (f,(ast,kenv)) -> (f,check_ast ast kenv)) asts) in + begin + (if !(opt_print_verbose) + then ((Pretty_print.pp_defs Format.std_formatter) (snd (List.hd chkedasts))) + else ()); + (if !(opt_print_lem) + then output "" Lem_ast_out chkedasts + else ()); + end + +let _ = try + begin + try ignore(main ()) + with Failure(s) -> raise (Reporting_basic.err_general Parse_ast.Unknown ("Failure "^s)) + end + with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e diff --git a/src/sail.odocl b/src/sail.odocl index 65935655..0872c3f9 100644 --- a/src/sail.odocl +++ b/src/sail.odocl @@ -2,7 +2,7 @@ ast finite_map initial_check lexer -main +sail parse_ast parser pp -- cgit v1.2.3