diff options
Diffstat (limited to 'src/main.ml')
| -rw-r--r-- | src/main.ml | 407 |
1 files changed, 407 insertions, 0 deletions
diff --git a/src/main.ml b/src/main.ml new file mode 100644 index 00000000..2f256cb2 --- /dev/null +++ b/src/main.ml @@ -0,0 +1,407 @@ +(**************************************************************************) +(* 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_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");*) + ( "-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 ignore(List.map (fun f -> (parse_file f)) !opt_file_arguments) + +let _ = main() |