diff --git a/examples/hello/TestFSharp.fst b/examples/hello/TestFSharp.fst new file mode 100755 index 00000000000..7dbaef10d8a --- /dev/null +++ b/examples/hello/TestFSharp.fst @@ -0,0 +1,20 @@ +(* + Copyright 2020 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module TestFSharp + +let t (a:Type) (b:Type) = list a + +let test #a #b (f:t a b) : list a = f diff --git a/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fs b/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fs new file mode 100755 index 00000000000..dc4a613d798 --- /dev/null +++ b/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fs @@ -0,0 +1,258 @@ +(* + Copyright 2020 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +#light "off" +(* -------------------------------------------------------------------- *) +module FStar.Extraction.ML.RemoveUnusedParameters +open FStar.ST +open FStar.All +open FStar +open FStar.Ident +open FStar.Util +open FStar.Const +open FStar.BaseTypes +open FStar.Extraction.ML.Syntax + +(** + This module implements a transformation on the FStar.Extraction.ML.Syntax + AST to remove unused type parameters from type abbreviations. + + This is mainly intended for use with F# code extraction, since the + F# compiler does not accept type abbreviations with unused + parameters. However, this transformation may also be useful for use + with OCaml, since it may lead to nicer code. +*) +module BU = FStar.Util + +(** + The transformation maintains an environment recording which + arguments of a type definition are to be removed, extending the + environment at the definition site of each type abbreviation and + using the environment to determine which arguments should be omitted + at each use site. + + The environment maps an mlpath, a fully qualified name of a type + definition, to a list of [Retain | Omit] tags, one for each argument + of the type definition. + *) + +type argument_tag = + | Retain + | Omit + +type entry = list + +type env_t = { + current_module:list; + tydef_map:BU.psmap; +} + +let initial_env : env_t = { + current_module = []; + tydef_map = BU.psmap_empty () +} + +let extend_env (env:env_t) (i:mlsymbol) (e:entry) : env_t = { + env with + tydef_map = BU.psmap_add env.tydef_map (string_of_mlpath (env.current_module,i)) e +} + +let lookup_tyname (env:env_t) (name:mlpath) + : option entry + = BU.psmap_try_find env.tydef_map (string_of_mlpath name) + +(** Free variables of a type: Computed to check which parameters are used *) +type var_set = BU.set +let empty_var_set = BU.new_set (fun x y -> String.compare x y) +let rec freevars_of_mlty' (vars:var_set) (t:mlty) = + match t with + | MLTY_Var i -> + BU.set_add i vars + | MLTY_Fun (t0, _, t1) -> + freevars_of_mlty' (freevars_of_mlty' vars t0) t1 + | MLTY_Named (tys, _) + | MLTY_Tuple tys -> + List.fold_left freevars_of_mlty' vars tys + | _ -> vars +let freevars_of_mlty = freevars_of_mlty' empty_var_set + +(** The main rewriting in on MLTY_Named (args, name), + which eliminates some of the args in case `name` has + parameters that are marked as Omit in the environment *) +let rec elim_mlty env mlty = + match mlty with + | MLTY_Var _ -> mlty + + | MLTY_Fun (t0, e, t1) -> + MLTY_Fun(elim_mlty env t0, e, elim_mlty env t1) + + | MLTY_Named (args, name) -> + let args = List.map (elim_mlty env) args in + begin + match lookup_tyname env name with + | None -> + MLTY_Named(args, name) + | Some entry -> + if List.length entry <> List.length args + then failwith "Impossible: arity mismatch between definition and use"; + let args = + List.fold_right2 + (fun arg tag out -> + match tag with + | Retain -> arg::out + | _ -> out) + args + entry + [] + in + MLTY_Named(args, name) + end + | MLTY_Tuple tys -> //arity of tuples do not change + MLTY_Tuple (List.map (elim_mlty env) tys) + | MLTY_Top + | MLTY_Erased -> mlty + +(** Note, the arity of expressions do not change. + So, this just traverses an expression an eliminates + type arguments in any subterm to e that is an mlty *) +let rec elim_mlexpr' (env:env_t) (e:mlexpr') = + match e with + | MLE_Const _ + | MLE_Var _ + | MLE_Name _ -> e + | MLE_Let (lb, e) -> MLE_Let(elim_letbinding env lb, elim_mlexpr env e) + | MLE_App(e, es) -> MLE_App(elim_mlexpr env e, List.map (elim_mlexpr env) es) + | MLE_TApp (e, tys) -> MLE_TApp(e, List.map (elim_mlty env) tys) + | MLE_Fun(bvs, e) -> MLE_Fun(List.map (fun (x, t) -> x, elim_mlty env t) bvs, elim_mlexpr env e) + | MLE_Match(e, branches) -> MLE_Match(elim_mlexpr env e, List.map (elim_branch env) branches) + | MLE_Coerce(e, t0, t1) -> MLE_Coerce(elim_mlexpr env e, elim_mlty env t0, elim_mlty env t1) + | MLE_CTor(l, es) -> MLE_CTor(l, List.map (elim_mlexpr env) es) + | MLE_Seq es -> MLE_Seq (List.map (elim_mlexpr env) es) + | MLE_Tuple es -> MLE_Tuple (List.map (elim_mlexpr env) es) + | MLE_Record(syms, fields) -> MLE_Record(syms, List.map (fun (s, e) -> s, elim_mlexpr env e) fields) + | MLE_Proj (e, p) -> MLE_Proj(elim_mlexpr env e, p) + | MLE_If(e, e1, e2_opt) -> MLE_If(elim_mlexpr env e, elim_mlexpr env e1, BU.map_opt e2_opt (elim_mlexpr env)) + | MLE_Raise(p, es) -> MLE_Raise (p, List.map (elim_mlexpr env) es) + | MLE_Try(e, branches) -> MLE_Try(elim_mlexpr env e, List.map (elim_branch env) branches) + +and elim_letbinding env (flavor, lbs) = + let elim_one_lb lb = + let ts = BU.map_opt lb.mllb_tysc (fun (vars, t) -> vars, elim_mlty env t) in + let expr = elim_mlexpr env lb.mllb_def in + { lb with + mllb_tysc = ts; + mllb_def = expr } + in + flavor, List.map elim_one_lb lbs + +and elim_branch env (pat, wopt, e) = + pat, BU.map_opt wopt (elim_mlexpr env), elim_mlexpr env e + +and elim_mlexpr (env:env_t) (e:mlexpr) = + { e with expr = elim_mlexpr' env e.expr; mlty = elim_mlty env e.mlty } + +(** This is the main function that actually extends the environment: + When encountering a type definition (MLTD_Abbrev), it + computes the variables that are used and marks the unused ones as Omit + in the environment and removes them from the definition here *) +let elim_one_mltydecl (env:env_t) (td:one_mltydecl) + : env_t + * one_mltydecl + = let _assumed, name, _ignored, parameters, _metadata, body = td in + let elim_td td = + match td with + | MLTD_Abbrev mlty -> + let mlty = elim_mlty env mlty in + let freevars = freevars_of_mlty mlty in + let parameters, entry = + List.fold_right + (fun p (params, entry) -> + if BU.set_mem p freevars + then p::params, Retain::entry + else params, Omit::entry) + parameters + ([], []) + in + extend_env env name entry, + parameters, + MLTD_Abbrev mlty + + | MLTD_Record fields -> + env, + parameters, + MLTD_Record (List.map (fun (name, ty) -> name, elim_mlty env ty) fields) + + | MLTD_DType inductive -> + env, + parameters, + MLTD_DType ( + List.map + (fun (i, constrs) -> + i, List.map (fun (constr, ty) -> constr, elim_mlty env ty) constrs) + inductive + ) + in + let env, parameters, body = + match body with + | None -> + env, parameters, body + | Some td -> + let env, parameters, td = elim_td td in + env, parameters, Some td + in + env, + (_assumed, name, _ignored, parameters, _metadata, body) + +let elim_module env m = + let elim_module1 env m = + match m with + | MLM_Ty td -> + let env, td = BU.fold_map elim_one_mltydecl env td in + env, MLM_Ty td + | MLM_Let lb -> + env, MLM_Let (elim_letbinding env lb) + | MLM_Exn (name, sym_tys) -> + env, MLM_Exn (name, List.map (fun (s, t) -> s, elim_mlty env t) sym_tys) + | MLM_Top e -> + env, MLM_Top (elim_mlexpr env e) + | _ -> + env, m + in + BU.fold_map elim_module1 env m + +let elim_mllib (env:env_t) (m:mllib) = + let (MLLib libs) = m in + let elim_one_lib env lib = + let name, sig_mod, _libs = lib in + let env = {env with current_module = fst name @ [snd name]} in + let sig_mod, env = + match sig_mod with + | Some (sig_, mod_) -> + //intentionally discard the environment from the module translation + let env, mod_ = elim_module env mod_ in + // The sig is currently empty + Some (sig_, mod_), env + | None -> + None, env + in + env, (name, sig_mod, _libs) + in + let env, libs = + BU.fold_map elim_one_lib env libs + in + env, MLLib libs + +let elim_mllibs (l:list) : list = + snd (BU.fold_map elim_mllib initial_env l) diff --git a/src/fstar/FStar.Universal.fs b/src/fstar/FStar.Universal.fs index b107cf7942d..3de85af02f8 100644 --- a/src/fstar/FStar.Universal.fs +++ b/src/fstar/FStar.Universal.fs @@ -234,6 +234,13 @@ let emit (mllibs:list) = | Some Options.Kremlin -> ".krml" | _ -> failwith "Unrecognized option" in + let mllibs = + match opt with + | Some Options.FSharp -> + FStar.Extraction.ML.RemoveUnusedParameters.elim_mllibs mllibs + | _ -> + mllibs + in match opt with | Some Options.FSharp | Some Options.OCaml | Some Options.Plugin -> (* When bootstrapped in F#, this will use the old printer in diff --git a/src/ocaml-output/FStar_Extraction_ML_RemoveUnusedParameters.ml b/src/ocaml-output/FStar_Extraction_ML_RemoveUnusedParameters.ml new file mode 100755 index 00000000000..1df6541f2c6 --- /dev/null +++ b/src/ocaml-output/FStar_Extraction_ML_RemoveUnusedParameters.ml @@ -0,0 +1,445 @@ +open Prims +type argument_tag = + | Retain + | Omit +let (uu___is_Retain : argument_tag -> Prims.bool) = + fun projectee -> + match projectee with | Retain -> true | uu____10 -> false + +let (uu___is_Omit : argument_tag -> Prims.bool) = + fun projectee -> match projectee with | Omit -> true | uu____21 -> false +type entry = argument_tag Prims.list +type env_t = + { + current_module: FStar_Extraction_ML_Syntax.mlsymbol Prims.list ; + tydef_map: entry FStar_Util.psmap } +let (__proj__Mkenv_t__item__current_module : + env_t -> FStar_Extraction_ML_Syntax.mlsymbol Prims.list) = + fun projectee -> + match projectee with | { current_module; tydef_map;_} -> current_module + +let (__proj__Mkenv_t__item__tydef_map : env_t -> entry FStar_Util.psmap) = + fun projectee -> + match projectee with | { current_module; tydef_map;_} -> tydef_map + +let (initial_env : env_t) = + let uu____77 = FStar_Util.psmap_empty () in + { current_module = []; tydef_map = uu____77 } +let (extend_env : + env_t -> FStar_Extraction_ML_Syntax.mlsymbol -> entry -> env_t) = + fun env -> + fun i -> + fun e -> + let uu___9_99 = env in + let uu____100 = + let uu____103 = + FStar_Extraction_ML_Syntax.string_of_mlpath + ((env.current_module), i) + in + FStar_Util.psmap_add env.tydef_map uu____103 e in + { current_module = (uu___9_99.current_module); tydef_map = uu____100 + } + +let (lookup_tyname : + env_t -> + FStar_Extraction_ML_Syntax.mlpath -> entry FStar_Pervasives_Native.option) + = + fun env -> + fun name -> + let uu____124 = FStar_Extraction_ML_Syntax.string_of_mlpath name in + FStar_Util.psmap_try_find env.tydef_map uu____124 + +type var_set = FStar_Extraction_ML_Syntax.mlident FStar_Util.set +let (empty_var_set : Prims.string FStar_Util.set) = + FStar_Util.new_set (fun x -> fun y -> FStar_String.compare x y) +let rec (freevars_of_mlty' : + var_set -> FStar_Extraction_ML_Syntax.mlty -> var_set) = + fun vars -> + fun t -> + match t with + | FStar_Extraction_ML_Syntax.MLTY_Var i -> FStar_Util.set_add i vars + | FStar_Extraction_ML_Syntax.MLTY_Fun (t0,uu____155,t1) -> + let uu____157 = freevars_of_mlty' vars t0 in + freevars_of_mlty' uu____157 t1 + | FStar_Extraction_ML_Syntax.MLTY_Named (tys,uu____159) -> + FStar_List.fold_left freevars_of_mlty' vars tys + | FStar_Extraction_ML_Syntax.MLTY_Tuple tys -> + FStar_List.fold_left freevars_of_mlty' vars tys + | uu____167 -> vars + +let (freevars_of_mlty : FStar_Extraction_ML_Syntax.mlty -> var_set) = + freevars_of_mlty' empty_var_set +let rec (elim_mlty : + env_t -> FStar_Extraction_ML_Syntax.mlty -> FStar_Extraction_ML_Syntax.mlty) + = + fun env -> + fun mlty -> + match mlty with + | FStar_Extraction_ML_Syntax.MLTY_Var uu____184 -> mlty + | FStar_Extraction_ML_Syntax.MLTY_Fun (t0,e,t1) -> + let uu____189 = + let uu____196 = elim_mlty env t0 in + let uu____197 = elim_mlty env t1 in (uu____196, e, uu____197) + in + FStar_Extraction_ML_Syntax.MLTY_Fun uu____189 + | FStar_Extraction_ML_Syntax.MLTY_Named (args,name) -> + let args1 = FStar_List.map (elim_mlty env) args in + let uu____207 = lookup_tyname env name in + (match uu____207 with + | FStar_Pervasives_Native.None -> + FStar_Extraction_ML_Syntax.MLTY_Named (args1, name) + | FStar_Pervasives_Native.Some entry1 -> + (if (FStar_List.length entry1) <> (FStar_List.length args1) + then + failwith + "Impossible: arity mismatch between definition and use" + else (); + (let args2 = + FStar_List.fold_right2 + (fun arg -> + fun tag -> + fun out -> + match tag with + | Retain -> arg :: out + | uu____233 -> out) args1 entry1 [] + in + FStar_Extraction_ML_Syntax.MLTY_Named (args2, name)))) + | FStar_Extraction_ML_Syntax.MLTY_Tuple tys -> + let uu____239 = FStar_List.map (elim_mlty env) tys in + FStar_Extraction_ML_Syntax.MLTY_Tuple uu____239 + | FStar_Extraction_ML_Syntax.MLTY_Top -> mlty + | FStar_Extraction_ML_Syntax.MLTY_Erased -> mlty + +let rec (elim_mlexpr' : + env_t -> + FStar_Extraction_ML_Syntax.mlexpr' -> FStar_Extraction_ML_Syntax.mlexpr') + = + fun env -> + fun e -> + match e with + | FStar_Extraction_ML_Syntax.MLE_Const uu____305 -> e + | FStar_Extraction_ML_Syntax.MLE_Var uu____306 -> e + | FStar_Extraction_ML_Syntax.MLE_Name uu____308 -> e + | FStar_Extraction_ML_Syntax.MLE_Let (lb,e1) -> + let uu____323 = + let uu____334 = elim_letbinding env lb in + let uu____341 = elim_mlexpr env e1 in (uu____334, uu____341) in + FStar_Extraction_ML_Syntax.MLE_Let uu____323 + | FStar_Extraction_ML_Syntax.MLE_App (e1,es) -> + let uu____354 = + let uu____361 = elim_mlexpr env e1 in + let uu____362 = FStar_List.map (elim_mlexpr env) es in + (uu____361, uu____362) in + FStar_Extraction_ML_Syntax.MLE_App uu____354 + | FStar_Extraction_ML_Syntax.MLE_TApp (e1,tys) -> + let uu____373 = + let uu____380 = FStar_List.map (elim_mlty env) tys in + (e1, uu____380) in + FStar_Extraction_ML_Syntax.MLE_TApp uu____373 + | FStar_Extraction_ML_Syntax.MLE_Fun (bvs,e1) -> + let uu____401 = + let uu____413 = + FStar_List.map + (fun uu____435 -> + match uu____435 with + | (x,t) -> + let uu____450 = elim_mlty env t in (x, uu____450)) + bvs + in + let uu____452 = elim_mlexpr env e1 in (uu____413, uu____452) in + FStar_Extraction_ML_Syntax.MLE_Fun uu____401 + | FStar_Extraction_ML_Syntax.MLE_Match (e1,branches) -> + let uu____482 = + let uu____497 = elim_mlexpr env e1 in + let uu____498 = FStar_List.map (elim_branch env) branches in + (uu____497, uu____498) in + FStar_Extraction_ML_Syntax.MLE_Match uu____482 + | FStar_Extraction_ML_Syntax.MLE_Coerce (e1,t0,t1) -> + let uu____538 = + let uu____545 = elim_mlexpr env e1 in + let uu____546 = elim_mlty env t0 in + let uu____547 = elim_mlty env t1 in + (uu____545, uu____546, uu____547) in + FStar_Extraction_ML_Syntax.MLE_Coerce uu____538 + | FStar_Extraction_ML_Syntax.MLE_CTor (l,es) -> + let uu____554 = + let uu____561 = FStar_List.map (elim_mlexpr env) es in + (l, uu____561) in + FStar_Extraction_ML_Syntax.MLE_CTor uu____554 + | FStar_Extraction_ML_Syntax.MLE_Seq es -> + let uu____569 = FStar_List.map (elim_mlexpr env) es in + FStar_Extraction_ML_Syntax.MLE_Seq uu____569 + | FStar_Extraction_ML_Syntax.MLE_Tuple es -> + let uu____575 = FStar_List.map (elim_mlexpr env) es in + FStar_Extraction_ML_Syntax.MLE_Tuple uu____575 + | FStar_Extraction_ML_Syntax.MLE_Record (syms,fields) -> + let uu____600 = + let uu____615 = + FStar_List.map + (fun uu____637 -> + match uu____637 with + | (s,e1) -> + let uu____652 = elim_mlexpr env e1 in (s, uu____652)) + fields + in + (syms, uu____615) in + FStar_Extraction_ML_Syntax.MLE_Record uu____600 + | FStar_Extraction_ML_Syntax.MLE_Proj (e1,p) -> + let uu____666 = + let uu____671 = elim_mlexpr env e1 in (uu____671, p) in + FStar_Extraction_ML_Syntax.MLE_Proj uu____666 + | FStar_Extraction_ML_Syntax.MLE_If (e1,e11,e2_opt) -> + let uu____679 = + let uu____688 = elim_mlexpr env e1 in + let uu____689 = elim_mlexpr env e11 in + let uu____690 = FStar_Util.map_opt e2_opt (elim_mlexpr env) in + (uu____688, uu____689, uu____690) in + FStar_Extraction_ML_Syntax.MLE_If uu____679 + | FStar_Extraction_ML_Syntax.MLE_Raise (p,es) -> + let uu____701 = + let uu____708 = FStar_List.map (elim_mlexpr env) es in + (p, uu____708) in + FStar_Extraction_ML_Syntax.MLE_Raise uu____701 + | FStar_Extraction_ML_Syntax.MLE_Try (e1,branches) -> + let uu____735 = + let uu____750 = elim_mlexpr env e1 in + let uu____751 = FStar_List.map (elim_branch env) branches in + (uu____750, uu____751) in + FStar_Extraction_ML_Syntax.MLE_Try uu____735 + +and (elim_letbinding : + env_t -> + (FStar_Extraction_ML_Syntax.mlletflavor * FStar_Extraction_ML_Syntax.mllb + Prims.list) -> + (FStar_Extraction_ML_Syntax.mlletflavor * + FStar_Extraction_ML_Syntax.mllb Prims.list)) + = + fun env -> + fun uu____789 -> + match uu____789 with + | (flavor,lbs) -> + let elim_one_lb lb = + let ts = + FStar_Util.map_opt lb.FStar_Extraction_ML_Syntax.mllb_tysc + (fun uu____829 -> + match uu____829 with + | (vars,t) -> + let uu____836 = elim_mlty env t in (vars, uu____836)) + in + let expr = elim_mlexpr env lb.FStar_Extraction_ML_Syntax.mllb_def + in + let uu___138_838 = lb in + { + FStar_Extraction_ML_Syntax.mllb_name = + (uu___138_838.FStar_Extraction_ML_Syntax.mllb_name); + FStar_Extraction_ML_Syntax.mllb_tysc = ts; + FStar_Extraction_ML_Syntax.mllb_add_unit = + (uu___138_838.FStar_Extraction_ML_Syntax.mllb_add_unit); + FStar_Extraction_ML_Syntax.mllb_def = expr; + FStar_Extraction_ML_Syntax.mllb_meta = + (uu___138_838.FStar_Extraction_ML_Syntax.mllb_meta); + FStar_Extraction_ML_Syntax.print_typ = + (uu___138_838.FStar_Extraction_ML_Syntax.print_typ) + } in + let uu____839 = FStar_List.map elim_one_lb lbs in + (flavor, uu____839) + +and (elim_branch : + env_t -> + (FStar_Extraction_ML_Syntax.mlpattern * FStar_Extraction_ML_Syntax.mlexpr + FStar_Pervasives_Native.option * FStar_Extraction_ML_Syntax.mlexpr) -> + (FStar_Extraction_ML_Syntax.mlpattern * + FStar_Extraction_ML_Syntax.mlexpr FStar_Pervasives_Native.option * + FStar_Extraction_ML_Syntax.mlexpr)) + = + fun env -> + fun uu____845 -> + match uu____845 with + | (pat,wopt,e) -> + let uu____869 = FStar_Util.map_opt wopt (elim_mlexpr env) in + let uu____872 = elim_mlexpr env e in (pat, uu____869, uu____872) + +and (elim_mlexpr : + env_t -> + FStar_Extraction_ML_Syntax.mlexpr -> FStar_Extraction_ML_Syntax.mlexpr) + = + fun env -> + fun e -> + let uu___147_877 = e in + let uu____878 = elim_mlexpr' env e.FStar_Extraction_ML_Syntax.expr in + let uu____879 = elim_mlty env e.FStar_Extraction_ML_Syntax.mlty in + { + FStar_Extraction_ML_Syntax.expr = uu____878; + FStar_Extraction_ML_Syntax.mlty = uu____879; + FStar_Extraction_ML_Syntax.loc = + (uu___147_877.FStar_Extraction_ML_Syntax.loc) + } + +let (elim_one_mltydecl : + env_t -> + FStar_Extraction_ML_Syntax.one_mltydecl -> + (env_t * FStar_Extraction_ML_Syntax.one_mltydecl)) + = + fun env -> + fun td -> + let uu____899 = td in + match uu____899 with + | (_assumed,name,_ignored,parameters,_metadata,body) -> + let elim_td td1 = + match td1 with + | FStar_Extraction_ML_Syntax.MLTD_Abbrev mlty -> + let mlty1 = elim_mlty env mlty in + let freevars = freevars_of_mlty mlty1 in + let uu____951 = + FStar_List.fold_right + (fun p -> + fun uu____977 -> + match uu____977 with + | (params,entry1) -> + let uu____1009 = FStar_Util.set_mem p freevars + in + if uu____1009 + then ((p :: params), (Retain :: entry1)) + else (params, (Omit :: entry1))) parameters + ([], []) + in + (match uu____951 with + | (parameters1,entry1) -> + let uu____1062 = extend_env env name entry1 in + (uu____1062, parameters1, + (FStar_Extraction_ML_Syntax.MLTD_Abbrev mlty1))) + | FStar_Extraction_ML_Syntax.MLTD_Record fields -> + let uu____1074 = + let uu____1075 = + FStar_List.map + (fun uu____1097 -> + match uu____1097 with + | (name1,ty) -> + let uu____1112 = elim_mlty env ty in + (name1, uu____1112)) fields + in + FStar_Extraction_ML_Syntax.MLTD_Record uu____1075 in + (env, parameters, uu____1074) + | FStar_Extraction_ML_Syntax.MLTD_DType inductive -> + let uu____1132 = + let uu____1133 = + FStar_List.map + (fun uu____1176 -> + match uu____1176 with + | (i,constrs) -> + let uu____1219 = + FStar_List.map + (fun uu____1241 -> + match uu____1241 with + | (constr,ty) -> + let uu____1256 = elim_mlty env ty in + (constr, uu____1256)) constrs + in + (i, uu____1219)) inductive + in + FStar_Extraction_ML_Syntax.MLTD_DType uu____1133 in + (env, parameters, uu____1132) + in + let uu____1269 = + match body with + | FStar_Pervasives_Native.None -> (env, parameters, body) + | FStar_Pervasives_Native.Some td1 -> + let uu____1289 = elim_td td1 in + (match uu____1289 with + | (env1,parameters1,td2) -> + (env1, parameters1, (FStar_Pervasives_Native.Some td2))) + in + (match uu____1269 with + | (env1,parameters1,body1) -> + (env1, + (_assumed, name, _ignored, parameters1, _metadata, body1))) + +let (elim_module : + env_t -> + FStar_Extraction_ML_Syntax.mlmodule1 Prims.list -> + (env_t * FStar_Extraction_ML_Syntax.mlmodule1 Prims.list)) + = + fun env -> + fun m -> + let elim_module1 env1 m1 = + match m1 with + | FStar_Extraction_ML_Syntax.MLM_Ty td -> + let uu____1377 = FStar_Util.fold_map elim_one_mltydecl env1 td + in + (match uu____1377 with + | (env2,td1) -> (env2, (FStar_Extraction_ML_Syntax.MLM_Ty td1))) + | FStar_Extraction_ML_Syntax.MLM_Let lb -> + let uu____1395 = + let uu____1396 = elim_letbinding env1 lb in + FStar_Extraction_ML_Syntax.MLM_Let uu____1396 in + (env1, uu____1395) + | FStar_Extraction_ML_Syntax.MLM_Exn (name,sym_tys) -> + let uu____1415 = + let uu____1416 = + let uu____1429 = + FStar_List.map + (fun uu____1451 -> + match uu____1451 with + | (s,t) -> + let uu____1466 = elim_mlty env1 t in + (s, uu____1466)) sym_tys + in + (name, uu____1429) in + FStar_Extraction_ML_Syntax.MLM_Exn uu____1416 in + (env1, uu____1415) + | FStar_Extraction_ML_Syntax.MLM_Top e -> + let uu____1477 = + let uu____1478 = elim_mlexpr env1 e in + FStar_Extraction_ML_Syntax.MLM_Top uu____1478 in + (env1, uu____1477) + | uu____1479 -> (env1, m1) in + FStar_Util.fold_map elim_module1 env m + +let (elim_mllib : + env_t -> + FStar_Extraction_ML_Syntax.mllib -> + (env_t * FStar_Extraction_ML_Syntax.mllib)) + = + fun env -> + fun m -> + let uu____1495 = m in + match uu____1495 with + | FStar_Extraction_ML_Syntax.MLLib libs -> + let elim_one_lib env1 lib = + let uu____1596 = lib in + match uu____1596 with + | (name,sig_mod,_libs) -> + let env2 = + let uu___229_1681 = env1 in + { + current_module = + (FStar_List.append (FStar_Pervasives_Native.fst name) + [FStar_Pervasives_Native.snd name]); + tydef_map = (uu___229_1681.tydef_map) + } in + let uu____1693 = + match sig_mod with + | FStar_Pervasives_Native.Some (sig_,mod_) -> + let uu____1730 = elim_module env2 mod_ in + (match uu____1730 with + | (env3,mod_1) -> + ((FStar_Pervasives_Native.Some (sig_, mod_1)), + env3)) + | FStar_Pervasives_Native.None -> + (FStar_Pervasives_Native.None, env2) + in + (match uu____1693 with + | (sig_mod1,env3) -> (env3, (name, sig_mod1, _libs))) + in + let uu____1873 = FStar_Util.fold_map elim_one_lib env libs in + (match uu____1873 with + | (env1,libs1) -> (env1, (FStar_Extraction_ML_Syntax.MLLib libs1))) + +let (elim_mllibs : + FStar_Extraction_ML_Syntax.mllib Prims.list -> + FStar_Extraction_ML_Syntax.mllib Prims.list) + = + fun l -> + let uu____2004 = FStar_Util.fold_map elim_mllib initial_env l in + FStar_Pervasives_Native.snd uu____2004 + \ No newline at end of file diff --git a/src/ocaml-output/FStar_Universal.ml b/src/ocaml-output/FStar_Universal.ml index 3310e82f71f..a2de5055b25 100644 --- a/src/ocaml-output/FStar_Universal.ml +++ b/src/ocaml-output/FStar_Universal.ml @@ -926,33 +926,38 @@ let (emit : FStar_Extraction_ML_Syntax.mllib Prims.list -> unit) = | FStar_Pervasives_Native.Some (FStar_Options.Plugin ) -> ".ml" | FStar_Pervasives_Native.Some (FStar_Options.Kremlin ) -> ".krml" | uu____972 -> failwith "Unrecognized option" in + let mllibs1 = + match opt with + | FStar_Pervasives_Native.Some (FStar_Options.FSharp ) -> + FStar_Extraction_ML_RemoveUnusedParameters.elim_mllibs mllibs + | uu____982 -> mllibs in match opt with | FStar_Pervasives_Native.Some (FStar_Options.FSharp ) -> let outdir = FStar_Options.output_dir () in FStar_List.iter (FStar_Extraction_ML_PrintML.print outdir ext) - mllibs + mllibs1 | FStar_Pervasives_Native.Some (FStar_Options.OCaml ) -> let outdir = FStar_Options.output_dir () in FStar_List.iter (FStar_Extraction_ML_PrintML.print outdir ext) - mllibs + mllibs1 | FStar_Pervasives_Native.Some (FStar_Options.Plugin ) -> let outdir = FStar_Options.output_dir () in FStar_List.iter (FStar_Extraction_ML_PrintML.print outdir ext) - mllibs + mllibs1 | FStar_Pervasives_Native.Some (FStar_Options.Kremlin ) -> let programs = - FStar_List.collect FStar_Extraction_Kremlin.translate mllibs in + FStar_List.collect FStar_Extraction_Kremlin.translate mllibs1 in let bin = (FStar_Extraction_Kremlin.current_version, programs) in (match programs with - | (name,uu____997)::[] -> - let uu____1000 = + | (name,uu____1005)::[] -> + let uu____1008 = FStar_Options.prepend_output_dir (Prims.op_Hat name ext) in - FStar_Util.save_value_to_file uu____1000 bin - | uu____1002 -> - let uu____1005 = FStar_Options.prepend_output_dir "out.krml" + FStar_Util.save_value_to_file uu____1008 bin + | uu____1010 -> + let uu____1013 = FStar_Options.prepend_output_dir "out.krml" in - FStar_Util.save_value_to_file uu____1005 bin) - | uu____1008 -> failwith "Unrecognized option" + FStar_Util.save_value_to_file uu____1013 bin) + | uu____1016 -> failwith "Unrecognized option" else () let (tc_one_file : @@ -968,91 +973,91 @@ let (tc_one_file : fun fn -> fun parsing_data -> FStar_Ident.reset_gensym (); - (let maybe_restore_opts uu____1065 = - let uu____1066 = - let uu____1068 = FStar_Options.interactive () in - Prims.op_Negation uu____1068 in - if uu____1066 + (let maybe_restore_opts uu____1073 = + let uu____1074 = + let uu____1076 = FStar_Options.interactive () in + Prims.op_Negation uu____1076 in + if uu____1074 then - let uu____1071 = FStar_Options.restore_cmd_line_options true + let uu____1079 = FStar_Options.restore_cmd_line_options true in - FStar_All.pipe_right uu____1071 (fun uu____1073 -> ()) + FStar_All.pipe_right uu____1079 (fun uu____1081 -> ()) else () in - let post_smt_encoding uu____1081 = FStar_SMTEncoding_Z3.refresh () + let post_smt_encoding uu____1089 = FStar_SMTEncoding_Z3.refresh () in let maybe_extract_mldefs tcmod env1 = - let uu____1100 = - (let uu____1104 = FStar_Options.codegen () in - uu____1104 = FStar_Pervasives_Native.None) || - (let uu____1110 = - let uu____1112 = + let uu____1108 = + (let uu____1112 = FStar_Options.codegen () in + uu____1112 = FStar_Pervasives_Native.None) || + (let uu____1118 = + let uu____1120 = FStar_Ident.string_of_lid tcmod.FStar_Syntax_Syntax.name in - FStar_Options.should_extract uu____1112 in - Prims.op_Negation uu____1110) + FStar_Options.should_extract uu____1120 in + Prims.op_Negation uu____1118) in - if uu____1100 + if uu____1108 then (FStar_Pervasives_Native.None, Prims.int_zero) else FStar_Util.record_time - (fun uu____1131 -> + (fun uu____1139 -> with_env env1 (fun env2 -> - let uu____1139 = + let uu____1147 = FStar_Extraction_ML_Modul.extract env2 tcmod in - match uu____1139 with | (uu____1148,defs) -> defs)) + match uu____1147 with | (uu____1156,defs) -> defs)) in let maybe_extract_ml_iface tcmod env1 = - let uu____1170 = - let uu____1172 = FStar_Options.codegen () in - uu____1172 = FStar_Pervasives_Native.None in - if uu____1170 + let uu____1178 = + let uu____1180 = FStar_Options.codegen () in + uu____1180 = FStar_Pervasives_Native.None in + if uu____1178 then (env1, Prims.int_zero) else FStar_Util.record_time - (fun uu____1191 -> - let uu____1192 = + (fun uu____1199 -> + let uu____1200 = with_env env1 (fun env2 -> FStar_Extraction_ML_Modul.extract_iface env2 tcmod) in - match uu____1192 with | (env2,uu____1204) -> env2) + match uu____1200 with | (env2,uu____1212) -> env2) in - let tc_source_file uu____1218 = - let uu____1219 = parse env pre_fn fn in - match uu____1219 with + let tc_source_file uu____1226 = + let uu____1227 = parse env pre_fn fn in + match uu____1227 with | (fmod,env1) -> let mii = - let uu____1235 = - let uu____1236 = + let uu____1243 = + let uu____1244 = FStar_Extraction_ML_UEnv.tcenv_of_uenv env1 in - uu____1236.FStar_TypeChecker_Env.dsenv in - FStar_Syntax_DsEnv.inclusion_info uu____1235 + uu____1244.FStar_TypeChecker_Env.dsenv in + FStar_Syntax_DsEnv.inclusion_info uu____1243 fmod.FStar_Syntax_Syntax.name in - let check_mod uu____1250 = + let check_mod uu____1258 = let check env2 = with_tcenv_of_env env2 (fun tcenv -> (match tcenv.FStar_TypeChecker_Env.gamma with | [] -> () - | uu____1290 -> + | uu____1298 -> failwith "Impossible: gamma contains leaked names"); - (let uu____1294 = + (let uu____1302 = FStar_TypeChecker_Tc.check_module tcenv fmod (FStar_Util.is_some pre_fn) in - match uu____1294 with + match uu____1302 with | (modul,env3) -> (maybe_restore_opts (); (let smt_decls = - let uu____1324 = - let uu____1326 = FStar_Options.lax () + let uu____1332 = + let uu____1334 = FStar_Options.lax () in - Prims.op_Negation uu____1326 in - if uu____1324 + Prims.op_Negation uu____1334 in + if uu____1332 then let smt_decls = FStar_SMTEncoding_Encode.encode_modul @@ -1062,25 +1067,25 @@ let (tc_one_file : else ([], []) in ((modul, smt_decls), env3))))) in - let uu____1363 = - let uu____1378 = - let uu____1382 = + let uu____1371 = + let uu____1386 = + let uu____1390 = FStar_Ident.string_of_lid fmod.FStar_Syntax_Syntax.name in - FStar_Pervasives_Native.Some uu____1382 in - FStar_Profiling.profile (fun uu____1400 -> check env1) - uu____1378 "FStar.Universal.tc_source_file" + FStar_Pervasives_Native.Some uu____1390 in + FStar_Profiling.profile (fun uu____1408 -> check env1) + uu____1386 "FStar.Universal.tc_source_file" in - match uu____1363 with + match uu____1371 with | ((tcmod,smt_decls),env2) -> let tc_time = Prims.int_zero in - let uu____1438 = maybe_extract_mldefs tcmod env2 in - (match uu____1438 with + let uu____1446 = maybe_extract_mldefs tcmod env2 in + (match uu____1446 with | (extracted_defs,extract_time) -> - let uu____1462 = + let uu____1470 = maybe_extract_ml_iface tcmod env2 in - (match uu____1462 with + (match uu____1470 with | (env3,iface_extraction_time) -> ({ FStar_CheckedFiles.checked_module = tcmod; @@ -1091,84 +1096,84 @@ let (tc_one_file : (extract_time + iface_extraction_time) }, extracted_defs, env3))) in - let uu____1482 = - (let uu____1486 = + let uu____1490 = + (let uu____1494 = FStar_Ident.string_of_lid fmod.FStar_Syntax_Syntax.name in - FStar_Options.should_verify uu____1486) && + FStar_Options.should_verify uu____1494) && ((FStar_Options.record_hints ()) || (FStar_Options.use_hints ())) in - if uu____1482 + if uu____1490 then - let uu____1497 = FStar_Parser_ParseIt.find_file fn in - FStar_SMTEncoding_Solver.with_hints_db uu____1497 + let uu____1505 = FStar_Parser_ParseIt.find_file fn in + FStar_SMTEncoding_Solver.with_hints_db uu____1505 check_mod else check_mod () in - let uu____1509 = - let uu____1511 = FStar_Options.cache_off () in - Prims.op_Negation uu____1511 in - if uu____1509 + let uu____1517 = + let uu____1519 = FStar_Options.cache_off () in + Prims.op_Negation uu____1519 in + if uu____1517 then let r = FStar_CheckedFiles.load_module_from_cache env fn in let r1 = - let uu____1528 = + let uu____1536 = (FStar_Options.force ()) && (FStar_Options.should_check_file fn) in - if uu____1528 then FStar_Pervasives_Native.None else r in + if uu____1536 then FStar_Pervasives_Native.None else r in match r1 with | FStar_Pervasives_Native.None -> - ((let uu____1544 = - let uu____1546 = FStar_Parser_Dep.module_name_of_file fn + ((let uu____1552 = + let uu____1554 = FStar_Parser_Dep.module_name_of_file fn in - FStar_Options.should_be_already_cached uu____1546 in - if uu____1544 + FStar_Options.should_be_already_cached uu____1554 in + if uu____1552 then - let uu____1549 = - let uu____1555 = + let uu____1557 = + let uu____1563 = FStar_Util.format1 "Expected %s to already be checked" fn in (FStar_Errors.Error_AlreadyCachedAssertionFailure, - uu____1555) + uu____1563) in - FStar_Errors.raise_err uu____1549 + FStar_Errors.raise_err uu____1557 else ()); - (let uu____1562 = - (let uu____1566 = FStar_Options.codegen () in - FStar_Option.isSome uu____1566) && + (let uu____1570 = + (let uu____1574 = FStar_Options.codegen () in + FStar_Option.isSome uu____1574) && (FStar_Options.cmi ()) in - if uu____1562 + if uu____1570 then - let uu____1570 = - let uu____1576 = + let uu____1578 = + let uu____1584 = FStar_Util.format1 "Cross-module inlining expects all modules to be checked first; %s was not checked" fn in (FStar_Errors.Error_AlreadyCachedAssertionFailure, - uu____1576) + uu____1584) in - FStar_Errors.raise_err uu____1570 + FStar_Errors.raise_err uu____1578 else ()); - (let uu____1582 = tc_source_file () in - match uu____1582 with + (let uu____1590 = tc_source_file () in + match uu____1590 with | (tc_result,mllib,env1) -> - ((let uu____1607 = - (let uu____1611 = FStar_Errors.get_err_count () + ((let uu____1615 = + (let uu____1619 = FStar_Errors.get_err_count () in - uu____1611 = Prims.int_zero) && + uu____1619 = Prims.int_zero) && ((FStar_Options.lax ()) || - (let uu____1616 = + (let uu____1624 = FStar_Ident.string_of_lid (tc_result.FStar_CheckedFiles.checked_module).FStar_Syntax_Syntax.name in - FStar_Options.should_verify uu____1616)) + FStar_Options.should_verify uu____1624)) in - if uu____1607 + if uu____1615 then FStar_CheckedFiles.store_module_to_cache env1 fn parsing_data tc_result @@ -1177,40 +1182,40 @@ let (tc_one_file : | FStar_Pervasives_Native.Some tc_result -> let tcmod = tc_result.FStar_CheckedFiles.checked_module in let smt_decls = tc_result.FStar_CheckedFiles.smt_decls in - ((let uu____1633 = - let uu____1635 = + ((let uu____1641 = + let uu____1643 = FStar_Ident.string_of_lid tcmod.FStar_Syntax_Syntax.name in - FStar_Options.dump_module uu____1635 in - if uu____1633 + FStar_Options.dump_module uu____1643 in + if uu____1641 then - let uu____1638 = + let uu____1646 = FStar_Syntax_Print.modul_to_string tcmod in FStar_Util.print1 "Module after type checking:\n%s\n" - uu____1638 + uu____1646 else ()); (let extend_tcenv tcmod1 tcenv = - let uu____1658 = - let uu____1663 = + let uu____1666 = + let uu____1671 = FStar_ToSyntax_ToSyntax.add_modul_to_env tcmod1 tc_result.FStar_CheckedFiles.mii (FStar_TypeChecker_Normalize.erase_universes tcenv) in FStar_All.pipe_left (with_dsenv_of_tcenv tcenv) - uu____1663 + uu____1671 in - match uu____1658 with - | (uu____1679,tcenv1) -> + match uu____1666 with + | (uu____1687,tcenv1) -> let env1 = FStar_TypeChecker_Tc.load_checked_module tcenv1 tcmod1 in (maybe_restore_opts (); - (let uu____1684 = - let uu____1686 = FStar_Options.lax () in - Prims.op_Negation uu____1686 in - if uu____1684 + (let uu____1692 = + let uu____1694 = FStar_Options.lax () in + Prims.op_Negation uu____1694 in + if uu____1692 then (FStar_SMTEncoding_Encode.encode_modul_from_cache env1 tcmod1 smt_decls; @@ -1220,44 +1225,44 @@ let (tc_one_file : in let env1 = FStar_Profiling.profile - (fun uu____1695 -> - let uu____1696 = + (fun uu____1703 -> + let uu____1704 = with_tcenv_of_env env (extend_tcenv tcmod) in - FStar_All.pipe_right uu____1696 + FStar_All.pipe_right uu____1704 FStar_Pervasives_Native.snd) FStar_Pervasives_Native.None "FStar.Universal.extend_tcenv" in let mllib = - let uu____1710 = - ((let uu____1714 = FStar_Options.codegen () in - uu____1714 <> FStar_Pervasives_Native.None) && - (let uu____1720 = + let uu____1718 = + ((let uu____1722 = FStar_Options.codegen () in + uu____1722 <> FStar_Pervasives_Native.None) && + (let uu____1728 = FStar_Ident.string_of_lid tcmod.FStar_Syntax_Syntax.name in - FStar_Options.should_extract uu____1720)) + FStar_Options.should_extract uu____1728)) && ((Prims.op_Negation tcmod.FStar_Syntax_Syntax.is_interface) || - (let uu____1723 = FStar_Options.codegen () in - uu____1723 = + (let uu____1731 = FStar_Options.codegen () in + uu____1731 = (FStar_Pervasives_Native.Some FStar_Options.Kremlin))) in - if uu____1710 + if uu____1718 then - let uu____1731 = maybe_extract_mldefs tcmod env1 in - match uu____1731 with + let uu____1739 = maybe_extract_mldefs tcmod env1 in + match uu____1739 with | (extracted_defs,_extraction_time) -> extracted_defs else FStar_Pervasives_Native.None in - let uu____1751 = maybe_extract_ml_iface tcmod env1 in - match uu____1751 with + let uu____1759 = maybe_extract_ml_iface tcmod env1 in + match uu____1759 with | (env2,_time) -> (tc_result, mllib, env2))) else - (let uu____1773 = tc_source_file () in - match uu____1773 with + (let uu____1781 = tc_source_file () in + match uu____1781 with | (tc_result,mllib,env1) -> (tc_result, mllib, env1))) let (tc_one_file_for_ide : @@ -1272,12 +1277,12 @@ let (tc_one_file_for_ide : fun fn -> fun parsing_data -> let env1 = env_of_tcenv env in - let uu____1837 = tc_one_file env1 pre_fn fn parsing_data in - match uu____1837 with - | (tc_result,uu____1851,env2) -> - let uu____1857 = FStar_Extraction_ML_UEnv.tcenv_of_uenv env2 + let uu____1845 = tc_one_file env1 pre_fn fn parsing_data in + match uu____1845 with + | (tc_result,uu____1859,env2) -> + let uu____1865 = FStar_Extraction_ML_UEnv.tcenv_of_uenv env2 in - (tc_result, uu____1857) + (tc_result, uu____1865) let (needs_interleaving : Prims.string -> Prims.string -> Prims.bool) = fun intf -> @@ -1285,11 +1290,11 @@ let (needs_interleaving : Prims.string -> Prims.string -> Prims.bool) = let m1 = FStar_Parser_Dep.lowercase_module_name intf in let m2 = FStar_Parser_Dep.lowercase_module_name impl in ((m1 = m2) && - (let uu____1880 = FStar_Util.get_file_extension intf in - FStar_List.mem uu____1880 ["fsti"; "fsi"])) + (let uu____1888 = FStar_Util.get_file_extension intf in + FStar_List.mem uu____1888 ["fsti"; "fsi"])) && - (let uu____1889 = FStar_Util.get_file_extension impl in - FStar_List.mem uu____1889 ["fst"; "fs"]) + (let uu____1897 = FStar_Util.get_file_extension impl in + FStar_List.mem uu____1897 ["fst"; "fs"]) let (tc_one_file_from_remaining : Prims.string Prims.list -> @@ -1302,32 +1307,32 @@ let (tc_one_file_from_remaining : fun remaining -> fun env -> fun deps -> - let uu____1932 = + let uu____1940 = match remaining with | intf::impl::remaining1 when needs_interleaving intf impl -> - let uu____1973 = - let uu____1982 = + let uu____1981 = + let uu____1990 = FStar_All.pipe_right impl (FStar_Parser_Dep.parsing_data_of deps) in tc_one_file env (FStar_Pervasives_Native.Some intf) impl - uu____1982 + uu____1990 in - (match uu____1973 with + (match uu____1981 with | (m,mllib,env1) -> (remaining1, (m, mllib, env1))) | intf_or_impl::remaining1 -> - let uu____2027 = - let uu____2036 = + let uu____2035 = + let uu____2044 = FStar_All.pipe_right intf_or_impl (FStar_Parser_Dep.parsing_data_of deps) in tc_one_file env FStar_Pervasives_Native.None intf_or_impl - uu____2036 + uu____2044 in - (match uu____2027 with + (match uu____2035 with | (m,mllib,env1) -> (remaining1, (m, mllib, env1))) | [] -> failwith "Impossible: Empty remaining modules" in - match uu____1932 with + match uu____1940 with | (remaining1,(nmods,mllib,env1)) -> (remaining1, nmods, mllib, env1) let rec (tc_fold_interleave : @@ -1341,31 +1346,31 @@ let rec (tc_fold_interleave : fun deps -> fun acc -> fun remaining -> - let as_list uu___0_2192 = - match uu___0_2192 with + let as_list uu___0_2200 = + match uu___0_2200 with | FStar_Pervasives_Native.None -> [] | FStar_Pervasives_Native.Some l -> [l] in match remaining with | [] -> acc - | uu____2209 -> - let uu____2213 = acc in - (match uu____2213 with + | uu____2217 -> + let uu____2221 = acc in + (match uu____2221 with | (mods,mllibs,env) -> - let uu____2245 = + let uu____2253 = tc_one_file_from_remaining remaining env deps in - (match uu____2245 with + (match uu____2253 with | (remaining1,nmod,mllib,env1) -> - ((let uu____2284 = - let uu____2286 = + ((let uu____2292 = + let uu____2294 = FStar_Options.profile_group_by_decls () in - Prims.op_Negation uu____2286 in - if uu____2284 + Prims.op_Negation uu____2294 in + if uu____2292 then - let uu____2289 = + let uu____2297 = FStar_Ident.string_of_lid (nmod.FStar_CheckedFiles.checked_module).FStar_Syntax_Syntax.name in - FStar_Profiling.report_and_clear uu____2289 + FStar_Profiling.report_and_clear uu____2297 else ()); tc_fold_interleave deps ((FStar_List.append mods [nmod]), @@ -1379,43 +1384,43 @@ let (batch_mode_tc : = fun filenames -> fun dep_graph -> - (let uu____2326 = + (let uu____2334 = FStar_Options.debug_at_level_no_module (FStar_Options.Other "Dep") in - if uu____2326 + if uu____2334 then (FStar_Util.print_endline "Auto-deps kicked in; here's some info."; FStar_Util.print1 "Here's the list of filenames we will process: %s\n" (FStar_String.concat " " filenames); - (let uu____2335 = - let uu____2337 = + (let uu____2343 = + let uu____2345 = FStar_All.pipe_right filenames (FStar_List.filter FStar_Options.should_verify_file) in - FStar_String.concat " " uu____2337 in + FStar_String.concat " " uu____2345 in FStar_Util.print1 - "Here's the list of modules we will verify: %s\n" uu____2335)) + "Here's the list of modules we will verify: %s\n" uu____2343)) else ()); (let env = - let uu____2353 = init_env dep_graph in - FStar_Extraction_ML_UEnv.new_uenv uu____2353 in - let uu____2354 = tc_fold_interleave dep_graph ([], [], env) filenames + let uu____2361 = init_env dep_graph in + FStar_Extraction_ML_UEnv.new_uenv uu____2361 in + let uu____2362 = tc_fold_interleave dep_graph ([], [], env) filenames in - match uu____2354 with + match uu____2362 with | (all_mods,mllibs,env1) -> (emit mllibs; (let solver_refresh env2 = - let uu____2398 = + let uu____2406 = with_tcenv_of_env env2 (fun tcenv -> - (let uu____2407 = + (let uu____2415 = (FStar_Options.interactive ()) && - (let uu____2410 = FStar_Errors.get_err_count () + (let uu____2418 = FStar_Errors.get_err_count () in - uu____2410 = Prims.int_zero) + uu____2418 = Prims.int_zero) in - if uu____2407 + if uu____2415 then (tcenv.FStar_TypeChecker_Env.solver).FStar_TypeChecker_Env.refresh () @@ -1424,6 +1429,6 @@ let (batch_mode_tc : ()); ((), tcenv)) in - FStar_All.pipe_left FStar_Pervasives_Native.snd uu____2398 in + FStar_All.pipe_left FStar_Pervasives_Native.snd uu____2406 in (all_mods, env1, solver_refresh)))) \ No newline at end of file