summaryrefslogtreecommitdiff
path: root/src/main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/main.ml')
-rw-r--r--src/main.ml414
1 files changed, 0 insertions, 414 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 06:56:33 +0000