Stefan pushed to branch master at Stefan / Typer
Commits: 95330ac8 by Stefan Monnier at 2020-08-04T19:23:58-04:00 Add preliminary support for Dune
* src/tweak.ml: Remove, unused. * src/*.ml: Fix misc compiler warnings.
- - - - - 73f177d8 by Stefan Monnier at 2021-03-10T11:10:11-05:00 Merge remote-tracking branch 'gitlab/dune' into trunk
- - - - -
24 changed files:
- + dune-project - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/debug_util.ml - + src/dune - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/heap.ml - src/inverse_subst.ml - src/lexp.ml - src/log.ml - src/myers.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - − src/tweak.ml - src/unification.ml - src/util.ml
Changes:
===================================== dune-project ===================================== @@ -0,0 +1 @@ +(lang dune 2.1)
===================================== src/REPL.ml ===================================== @@ -38,18 +38,15 @@ this program. If not, see http://www.gnu.org/licenses/. *)
open Util open Fmt -open Debug
open Prelexer open Lexer open Sexp -open Pexp open Lexp
open Eval
open Grammar -open Builtin
open Env open Debruijn @@ -116,11 +113,11 @@ let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = | [] -> (List.rev dacc), (List.rev pacc) | sxp::tl -> match sxp with (* Declaration *) - | Node (Symbol (_, ("_=_" | "_:_")), [Symbol s; t]) -> + | Node (Symbol (_, ("_=_" | "_:_")), [Symbol _s; _t]) -> pxp_parse tl (sxp :: dacc) pacc
(* f arg1 arg2 = function body; *) - | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> + | Node (Symbol (_, "_=_"), [Node (Symbol _s, _args); _t]) -> pxp_parse tl (sxp :: dacc) pacc
(* Expression *) @@ -238,7 +235,7 @@ let rec repl i clxp rctx = | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( match (str_split ipt ' ') with | "%readfile"::args -> - let (i, clxp, rctx) = + let (_i, clxp, rctx) = try readfiles args (i, clxp, rctx) false with Log.Stop_Compilation msg ->
===================================== src/builtin.ml ===================================== @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2020 Free Software Foundation, Inc. + * Copyright (C) 2016-2021 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -53,10 +53,7 @@ * * ---------------------------------------------------------------------------*)
-open Util - -open Sexp (* Integer/Float *) -open Pexp (* arg_kind *) +(* open Pexp *) (* arg_kind *)
module OL = Opslexp open Lexp
===================================== src/debruijn.ml ===================================== @@ -163,7 +163,7 @@ let ectx_to_lctx (ectx : elab_context) : lexp_context = let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level = sl
-let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int +let ectx_local_scope_size ((_, (_n, _), _, (_, slen, _)) as ectx) : int = get_size ectx - slen
(* Public methods: DO USE @@ -185,7 +185,7 @@ let senv_lookup (name: string) (ctx: elab_context): int = let (_, (n, map), _, _) = ctx in try n - (SMap.find name map) - 1 with Not_found - -> let get_related_names (n : db_ridx) name map = + -> let get_related_names (_n : db_ridx) name map = let r = Str.regexp (".*"^name^".*") in let search r = SMap.fold (fun name _ names -> if (Str.string_match r name 0) then @@ -220,7 +220,7 @@ let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) = lexp_ctx_cons ctx def v t
let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = - let (loc, oname) = def in + let (_loc, oname) = def in let (grm, (n, map), env, sl) = ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), @@ -403,7 +403,7 @@ type lct_view = | CVlet of vname * varbind * ltype * lexp_context | CVfix of (vname * lexp * ltype) list * lexp_context
-let rec lctx_view lctx = +let lctx_view lctx = match lctx with | Myers.Mnil -> CVempty | Myers.Mcons ((loname, LetDef (1, def), t), lctx, _, _) @@ -414,7 +414,7 @@ let rec lctx_view lctx = -> loop (i + 1) lctx ((loname, def, t) :: defs) | _ -> CVfix (defs, lctx) in loop 2 lctx [(loname, def, t)] - | Myers.Mcons ((_, LetDef (o, def), _), _, _, _) when o > 1 + | Myers.Mcons ((_, LetDef (o, _def), _), _, _, _) when o > 1 -> fatal "Unexpected lexp_context shape!" | Myers.Mcons ((loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx) @@ -443,7 +443,7 @@ let set_hoist o (o', m) =
let set_union (o1, m1) (o2, m2) : set = if o1 = o2 then - (o1, IMap.merge (fun k _ _ -> Some ()) m1 m2) + (o1, IMap.merge (fun _k _ _ -> Some ()) m1 m2) else let o = o2 - o1 in (o1, IMap.fold (fun i2 () m1
===================================== src/debug.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -36,17 +36,12 @@ open Util open Fmt
open Prelexer -open Lexer
open Sexp -open Pexp open Lexp
-open Debruijn -open Grammar - (* Print aPretokens *) -let rec debug_pretokens_print pretoken = +let debug_pretokens_print pretoken = print_string " "; let print_info msg loc = print_string msg; @@ -66,11 +61,11 @@ let rec debug_pretokens_print pretoken = print_string (""" ^ str ^ """)
(* Print a List of Pretokens *) -let rec debug_pretokens_print_all pretokens = +let debug_pretokens_print_all pretokens = List.iter (fun pt -> debug_pretokens_print pt; print_string "\n") pretokens
(* Sexp Print *) -let rec debug_sexp_print sexp = +let debug_sexp_print sexp = let print_info msg loc = print_string msg; print_string "["; loc_print loc; print_string "]\t" in @@ -125,7 +120,7 @@ let debug_pexp_print ptop = let debug_lexp_decls decls = let sep = " : " in List.iter (fun e -> - let ((loc, name), lxp, ltp) = e in + let ((loc, _name), lxp, _ltp) = e in
print_string " "; lalign_print_string (lexp_name lxp) 15;
===================================== src/debug_util.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -37,7 +37,6 @@ open Debug
(* ASTs *) open Sexp -open Pexp open Lexp
(* AST reader *) @@ -58,7 +57,7 @@ open Env let dloc = dummy_location let dummy_decl = Imm(String(dloc, "Dummy"))
-let discard v = () +let discard _v = ()
(* Argument parsing *) let arg_print_options = ref SMap.empty @@ -245,7 +244,7 @@ let main () = let flexps = List.flatten lexps in
(if (get_p_option "lexp-merge-debug") then( - List.iter (fun ((l, s), lxp, ltp) -> + List.iter (fun ((_l, s), lxp, ltp) -> lalign_print_string (maybename s) 20; lexp_print ltp; print_string "\n";
===================================== src/dune ===================================== @@ -0,0 +1,6 @@ +;; -*- lisp-data -*- +(executable + (name REPL) + ;; (public_name typer) + (libraries "zarith" "str") + )
===================================== src/elab.ml ===================================== @@ -38,7 +38,6 @@ * -------------------------------------------------------------------------- *)
open Util -open Fmt
open Prelexer open Lexer @@ -202,7 +201,7 @@ let ctx_define (ctx: elab_context) var lxp ltype =
let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in - let _ = List.fold_left (fun n (var, lxp, ltp) + let _ = List.fold_left (fun n (var, _lxp, ltp) -> elab_check_proper_type nctx (push_susp ltp (S.shift n)) var; n - 1) @@ -312,7 +311,7 @@ let elab_varref ctx (loc, name) (* Turn metavar into plain vars after generalization. * ids: an IMap that maps metavars to their position as argument * (first arg gets position 0). *) -let rec meta_to_var ids (e : lexp) = +let meta_to_var ids (e : lexp) =
let count = IMap.cardinal ids in
@@ -521,7 +520,7 @@ let generalize (nctx : elab_context) e = let cl = Myers.length (ectx_to_lctx nctx) in let (_, (mfvs, nes)) = OL.fv e in if mfvs = IMap.empty - then (fun wrap e -> e) (* Nothing to generalize, yay! *) + then (fun _wrap e -> e) (* Nothing to generalize, yay! *) else (* Sort `mvfs' topologically, and bring typelevel args to the front *) let mfvs = sort_generalized_metavars sl cl (ectx_to_lctx nctx) mfvs in @@ -642,7 +641,7 @@ and infer_type pexp ectx var = | [] -> ()); t
-and lexp_let_decls declss (body: lexp) ctx = +and lexp_let_decls declss (body: lexp) _ctx = List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body
@@ -737,7 +736,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | None -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) - -> let (s, targs) = List.fold_left + -> let (_s, targs) = List.fold_left (fun (s, targs) (ak, name, t) -> let arg = newMetavar (ectx_to_lctx ctx) @@ -800,7 +799,7 @@ and check_case rtype (loc, target, ppatterns) ctx =
let add_branch pctor pargs = let loc = sexp_location pctor in - let lctor, ct = infer pctor ctx in + let lctor, _ct = infer pctor ctx in let rec inst_args ctx e = let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in match lexp_lexp' lxp with @@ -810,7 +809,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let nctx = ctx_extend ctx v Variable t in let body = inst_args nctx body in mkSusp body (S.substitute arg) - | e -> lxp in + | _e -> lxp in match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) -> let _ = check_uniqueness pat cons_name lbranches in @@ -842,7 +841,7 @@ and check_case rtype (loc, target, ppatterns) ctx = ^ "` have no matching fields"); make_nctx ctx s pargs cargs SMap.empty acc | [], [] -> ctx, List.rev acc - | (_, pat)::_, [] + | (_, _pat)::_, [] -> lexp_error loc lctor "Too many pattern args to the constructor"; make_nctx ctx s [] [] pe acc @@ -959,7 +958,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args largs sargs pending ltp
(* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, (l,v), arg_type, _, ret_type) + | _, Arrow ((Aerasable | Aimplicit) as ak, (_l,v), arg_type, _, ret_type) (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) @@ -1078,7 +1077,7 @@ and lexp_eval ectx e = "Exception happened during evaluation:"; raise exc
-and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) +and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) : value_type =
(* Build the function to be called *) @@ -1102,7 +1101,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) * | e -> sexp_print e; print_string "\n" *)
and lexp_decls_macro (loc, mname) sargs ctx: sexp = - try let lxp, ltp = infer (Symbol (loc, mname)) ctx in + try let lxp, _ltp = infer (Symbol (loc, mname)) ctx in
(* FIXME: Check that (conv_p ltp Macro)! *) let ret = lexp_expand_macro loc lxp sargs ctx None in @@ -1113,7 +1112,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return a IO sexp")) | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return an IO")
- with e -> + with _e -> fatal ~loc ("Macro `" ^ mname ^ "` not found")
(* Elaborate a bunch of mutually-recursive definitions. @@ -1137,7 +1136,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with - | (v', ForwardRef, t) + | (_v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in (* We elab `sexp` within the original `nctx`, i.e. * the context where the other vars don't have @@ -1146,7 +1145,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) * mutually-recursive block would not have the * proper format, e.g. for `lctx_view`! *) let e = check sexp adjusted_t nctx in - let d = (v', LetDef (i + 1, e), t) in + (* let d = (v', LetDef (i + 1, e), t) in *) (IMap.add i ((l, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty) in @@ -1194,11 +1193,11 @@ and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in let g = generalize nctx e in - let e' = g (fun ne vname t l e + let e' = g (fun ne vname t _l e -> mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e)) e in - let t' = g (fun ne name t l e + let t' = g (fun ne name t _l e -> mkArrow ((if ne then Aimplicit else Aerasable), name, t, sexp_location se, e)) t in @@ -1325,7 +1324,7 @@ and lexp_decls_1 -> recur [] (sdform_define_operator nctx l args None) pending_decls pending_defs
- | Some (Node (Symbol ((l, _) as v), sargs)) + | Some (Node (Symbol ((_l, _) as v), sargs)) -> (* expand macro and get the generated declarations *) let sdecl' = lexp_decls_macro v sargs nctx in recur [sdecl'] nctx pending_decls pending_defs @@ -1363,7 +1362,7 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = * Special forms implementation * -------------------------------------------------------------------------- *)
-and sform_declexpr ctx loc sargs ot = +and sform_declexpr ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with @@ -1374,7 +1373,7 @@ and sform_declexpr ctx loc sargs ot = sform_dummy_ret ctx loc
-let sform_decltype ctx loc sargs ot = +let sform_decltype ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) @@ -1409,9 +1408,9 @@ let sform_built_in ctx loc sargs ot = | false, _ -> error ~loc "Use of `Built-in` in user code"; sform_dummy_ret ctx loc
-let sform_datacons ctx loc sargs ot = +let sform_datacons ctx loc sargs _ot = match sargs with - | [t; Symbol ((sloc, cname) as sym)] + | [t; Symbol ((_sloc, _cname) as sym)] -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy)
@@ -1441,7 +1440,7 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = "Unrecognized formal arg"; (Anormal, (sexp_location arg, None), None)
-let sform_typecons ctx loc sargs ot = +let sform_typecons ctx loc sargs _ot = match sargs with | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs @@ -1487,7 +1486,7 @@ let sform_typecons ctx loc sargs ot = let map_ctor = lexp_parse_inductive ctors nctx in (mkInductive (loc, label, formals, map_ctor), Lazy)
-let sform_hastype ctx loc sargs ot = +let sform_hastype ctx loc sargs _ot = match sargs with | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in @@ -1495,7 +1494,7 @@ let sform_hastype ctx loc sargs ot = | _ -> sexp_error loc "##_:_ takes two arguments"; sform_dummy_ret ctx loc
-let sform_arrow kind ctx loc sargs ot = +let sform_arrow kind ctx loc sargs _ot = match sargs with | [st1; st2] -> let (v, st1) = match st1 with @@ -1513,12 +1512,12 @@ let sform_immediate ctx loc sargs ot = | [(String _) as se] -> mkImm (se), Inferred DB.type_string | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int | [(Float _) as se] -> mkImm (se), Inferred DB.type_float - | [Block (sl, pts, el)] + | [Block (_sl, pts, _el)] -> let grm = ectx_get_grammar ctx in let tokens = lex default_stt pts in let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot - | [se] + | [_se] -> (sexp_error loc ("Non-immediate passed to ##typer-immediate"); sform_dummy_ret ctx loc) | _ @@ -1590,7 +1589,7 @@ let sform_identifier ctx loc sargs ot = (* Normal identifier. *) | [Symbol id] -> elab_varref ctx id
- | [se] + | [_se] -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); sform_dummy_ret ctx loc)
@@ -1661,7 +1660,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) | _ -> alt)
- | lt + | _lt -> let (lt1, lt2) = unify_with_arrow ctx loc lp kind arg olt1 in mklam lt1 (Some lt2))
@@ -1687,7 +1686,7 @@ let rec sform_case ctx loc sargs ot = match sargs with (le, match ot with Some _ -> Checked | None -> Inferred t)
(* In case there are no branches, pretend there was a | anyway. *) - | [e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot + | [_e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot | _ -> sexp_error loc "Unrecognized case expression"; sform_dummy_ret ctx loc
@@ -1725,7 +1724,7 @@ let rec infer_level ctx se : lexp = * so it really can only be used applied to something, so it always generates * β-redexes. Furthermore, I'm not sure if my PTS definition is correct to * allow such a lambda. *) -let sform_type ctx loc sargs ot = +let sform_type ctx loc sargs _ot = match sargs with | [se] -> let l = infer_level ctx se in (mkSort (loc, Stype l), @@ -1733,7 +1732,7 @@ let sform_type ctx loc sargs ot = | _ -> (sexp_error loc "##Type_ expects one argument"; sform_dummy_ret ctx loc)
-let sform_debruijn ctx loc sargs ot = +let sform_debruijn ctx loc sargs _ot = match sargs with | [Integer (l,i)] -> let i = Z.to_int i in if i < 0 || i > get_size ctx then @@ -1746,7 +1745,7 @@ let sform_debruijn ctx loc sargs ot =
(* Only print var info *) let lexp_print_var_info ctx = - let ((m, _), env, _) = ctx in + let ((_m, _), env, _) = ctx in let n = Myers.length env in
for i = 0 to n - 1 do ( @@ -1770,7 +1769,7 @@ let in_pervasive = ref true sargs should be an array of one file name, ot is the expected type of output tuple. *) -let sform_load usr_elctx loc sargs ot = +let sform_load usr_elctx loc sargs _ot =
let read_file file_name elctx = let pres =
===================================== src/elexp.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -32,7 +32,6 @@
open Sexp (* Sexp type *) -open Pexp (* Anormal *)
module U = Util module L = Lexp
===================================== src/env.ml ===================================== @@ -78,12 +78,12 @@ let rec value_equal a b = | Vfloat (f1), Vfloat (f2) -> f1 = f2 | Vsexp (a), Vsexp (b) -> sexp_equal a b | Vin (c1), Vin (c2) -> c1 = c2 - | Vout (c1), Vout (c2) -> c2 = c2 + | Vout (_c1), Vout (c2) -> c2 = c2 | Vcommand (f1), Vcommand (f2) -> f1 = f2 | Vundefined, _ | _, Vundefined -> warning "Vundefined"; false - | Vtype e1, Vtype e2 -> warning "Vtype"; false + | Vtype _e1, Vtype _e2 -> warning "Vtype"; false
- | Closure (s1, b1, ctx1), Closure (s2, b2, ctx2) + | Closure (s1, _b1, _ctx1), Closure (s2, _b2, _ctx2) -> warning "Closure"; if (s1 != s2) then false else true
===================================== src/eval.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018, 2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2018, 2020, 2021 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -34,7 +34,7 @@ open Util open Fmt
open Sexp -open Pexp (* Arg_kind *) +(* open Pexp *) (* Arg_kind *) open Lexp (* Varbind *)
open Elexp @@ -83,7 +83,7 @@ let append_typer_trace trace (expr : elexp) = let get_trace () = !global_eval_trace
let rec_depth trace = - let (a, b) = trace in + let (_a, b) = trace in List.length b
let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg @@ -145,7 +145,7 @@ let set_getenv (ectx : elab_context) = macro_monad_elab_context := ectx (* Builtin of builtin * string * ltype *) let add_binary_iop name f = let name = "Int." ^ name in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint (v); Vint (w)] -> Vint (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in @@ -153,7 +153,7 @@ let add_binary_iop name f =
let add_binary_iop_with_loc name f = let name = "Int." ^ name in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint (v); Vint (w)] -> Vint (f loc v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in @@ -217,7 +217,7 @@ let _ = add_binary_iop_with_loc "+" add_with_overflow;
let add_binary_bool_iop name f = let name = "Int." ^ name in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint v; Vint w] -> o2v_bool (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in @@ -231,7 +231,7 @@ let _ = add_binary_bool_iop "<" (<);
let _ = let name = "Int." ^ "not" in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint v] -> Vint(lnot v) | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument") in @@ -241,7 +241,7 @@ let _ =
let add_binary_biop name f = let name = "Integer." ^ name in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vinteger v; Vinteger w] -> Vinteger (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in @@ -254,7 +254,7 @@ let _ = add_binary_biop "+" BI.add;
let add_binary_bool_biop name f = let name = "Integer." ^ name in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vinteger v; Vinteger w] -> o2v_bool (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in @@ -268,7 +268,7 @@ let _ = add_binary_bool_biop "<" BI.lt; let name = "Int->Integer" in add_builtin_function name - (fun loc (depth : eval_debug_info) (args_val: value_type list) + (fun loc (_depth : eval_debug_info) (args_val: value_type list) -> match args_val with | [Vint v] -> Vinteger (BI.of_int v) | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument")) @@ -276,7 +276,7 @@ let _ = add_binary_bool_biop "<" BI.lt; let name = "Integer->Int" in add_builtin_function name - (fun loc (depth : eval_debug_info) (args_val: value_type list) + (fun loc (_depth : eval_debug_info) (args_val: value_type list) -> match args_val with | [Vinteger v] -> (try Vint (BI.to_int v) with @@ -288,7 +288,7 @@ let _ = add_binary_bool_biop "<" BI.lt;
let add_binary_fop name f = let name = "Float." ^ name in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vfloat v; Vfloat w] -> Vfloat (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Float arguments") in @@ -301,7 +301,7 @@ let _ = add_binary_fop "+" (+.);
let add_binary_bool_fop name f = let name = "Float." ^ name in - let f loc (depth : eval_debug_info) (args_val: value_type list) = + let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vfloat v; Vfloat w] -> o2v_bool (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Float arguments") in @@ -314,17 +314,17 @@ let _ = add_binary_bool_fop "<" (<); add_binary_bool_fop "<=" (<=)
let _ = let name = "Float." ^ "trunc" in - let f loc (depth : eval_debug_info) (args_val : value_type list) = + let f loc (_depth : eval_debug_info) (args_val : value_type list) = match args_val with | [Vfloat v] -> Vfloat ( snd (modf v) ) | _ -> error loc ("`" ^ name ^ "` expects 1 Float argument") in add_builtin_function name f 1
-let make_symbol loc depth args_val = match args_val with +let make_symbol loc _depth args_val = match args_val with | [Vstring str] -> Vsexp (Symbol (loc, str)) | _ -> error loc "Sexp.symbol expects one string as argument"
-let make_node loc depth args_val = match args_val with +let make_node loc _depth args_val = match args_val with | [Vsexp (op); lst] -> let args = v2o_list lst in
@@ -339,54 +339,54 @@ let make_node loc depth args_val = match args_val with | _ -> error loc "Sexp.node expects a `Sexp` and a `List Sexp`"
-let make_string loc depth args_val = match args_val with +let make_string loc _depth args_val = match args_val with | [Vstring str] -> Vsexp (String (loc, str)) | _ -> error loc "Sexp.string expects one string as argument"
-let make_integer loc depth args_val = match args_val with +let make_integer loc _depth args_val = match args_val with | [Vinteger n] -> Vsexp (Integer (loc, n)) | _ -> error loc "Sexp.integer expects one integer as argument"
-let make_float loc depth args_val = match args_val with +let make_float loc _depth args_val = match args_val with | [Vfloat x] -> Vsexp (Float (loc, x)) | _ -> error loc "Sexp.float expects one float as argument"
-let make_block loc depth args_val = match args_val with +let make_block loc _depth args_val = match args_val with (* From what would we like to make a block? *) | [Vstring str] -> Vsexp (Block (loc, (Prelexer.prelex_string str), loc)) | _ -> error loc "Sexp.block expects one string as argument"
-let reader_parse loc depth args_val = match args_val with +let reader_parse loc _depth args_val = match args_val with | [Velabctx ectx; Vsexp (Block (_,toks,_))] -> let grm = ectx_get_grammar ectx in o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) | [Velabctx _; s] -> (warning loc "Reader.parse do nothing without a Block"; s) | _ -> error loc "Reader.parse expects an ElabContext and a Block as argument"
-let string_eq loc depth args_val = match args_val with +let string_eq loc _depth args_val = match args_val with | [Vstring s1; Vstring s2] -> o2v_bool (s1 = s2) | _ -> error loc "String.= expects 2 strings"
(* need either a character type or builtin string operation *) -let string_concat loc depth args_val = match args_val with +let string_concat loc _depth args_val = match args_val with | [Vstring s1; Vstring s2] -> Vstring (s1 ^ s2) | _ -> error loc "String.concat expects 2 strings"
-let string_sub loc depth args_val = match args_val with +let string_sub loc _depth args_val = match args_val with | [Vstring s; Vint start; Vint len] -> Vstring (String.sub s start len) | _ -> error loc "String.sub expects 1 string and 2 ints"
-let sexp_eq loc depth args_val = match args_val with +let sexp_eq loc _depth args_val = match args_val with | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) | _ -> error loc "Sexp.= expects 2 sexps"
-let sexp_debug_print loc depth args_val = match args_val with +let sexp_debug_print loc _depth args_val = match args_val with | [Vsexp (s1)] -> (let tstr = sexp_name s1 in (print_string ("\n\t"^tstr^" : ["^(sexp_string s1)^"]\n\n") ; Vcommand (fun () -> Vsexp (s1)))) | _ -> error loc "Sexp.debug_print expects 1 sexps"
-let file_open loc depth args_val = match args_val with +let file_open loc _depth args_val = match args_val with | [Vstring (file); Vstring (mode)] -> (* open file *) (* return a file handle *) Vcommand(fun () -> @@ -397,16 +397,16 @@ let file_open loc depth args_val = match args_val with
| _ -> error loc "File.open expects 2 strings"
-let file_read loc depth args_val = match args_val with +let file_read loc _depth args_val = match args_val with (* FIXME: Either rename it to "readline" and drop the second arg, * or actually pay attention to the second arg. *) - | [Vin channel; Vint n] -> Vstring (input_line channel) + | [Vin channel; Vint _n] -> Vstring (input_line channel) | _ -> error loc ~print_action:(fun _ -> List.iter (fun v -> value_print v; print_newline ()) args_val; ) "File.read expects an in_channel. Actual arguments:"
-let file_write loc depth args_val = match args_val with +let file_write loc _depth args_val = match args_val with | [Vout channel; Vstring msg] -> Vcommand (fun () -> fprintf channel "%s" msg; (* FIXME: This should be the unit value! *) @@ -482,7 +482,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) and eval_var ctx lxp v = let (name, idx) = v in try get_rte_variable name idx ctx - with e -> + with _e -> elexp_fatal (fst name) lxp ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ")
@@ -585,7 +585,7 @@ and eval_case ctx i loc target pat dflt =
and build_arg_list args ctx i = (* eval every args *) - let arg_val = List.map (fun (k, e) -> eval e ctx i) args in + let arg_val = List.map (fun (_k, e) -> eval e ctx i) args in
(* Add args inside context *) List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val @@ -661,7 +661,7 @@ and print_typer_trace' trace = and print_typer_trace trace = match trace with | Some t -> print_typer_trace' t - | None -> let (a, b) = !global_eval_trace in + | None -> let (_a, b) = !global_eval_trace in print_typer_trace' b
and print_trace title trace default = @@ -694,7 +694,7 @@ and print_trace title trace default = print_string (Fmt.make_sep '=')
and print_eval_trace trace = - let (a, b) = !global_eval_trace in + let (a, _b) = !global_eval_trace in print_trace " EVAL TRACE " trace a
let io_bind loc depth args_val = @@ -709,31 +709,31 @@ let io_bind loc depth args_val = | _ -> error loc "IO.bind second arg did not return a command") | _ -> error loc "Wrong number of args or wrong first arg value in `IO.bind`"
-let io_run loc depth args_val = match args_val with +let io_run loc _depth args_val = match args_val with | [Vcommand cmd; v] -> let _ = cmd () in v | _ -> error loc "IO.run expects a monad and a function as arguments"
-let io_return loc depth args_val = match args_val with +let io_return loc _depth args_val = match args_val with | [v] -> Vcommand (fun () -> v) | _ -> error loc "IO.return takes a single argument"
-let float_to_string loc depth args_val = match args_val with +let float_to_string loc _depth args_val = match args_val with | [Vfloat x] -> Vstring (string_of_float x) | _ -> error loc "Float->String expects one Float argument"
-let int_to_string loc depth args_val = match args_val with +let int_to_string loc _depth args_val = match args_val with | [Vint x] -> Vstring (string_of_int x) | _ -> error loc "Int->String expects one Int argument"
-let integer_to_string loc depth args_val = match args_val with +let integer_to_string loc _depth args_val = match args_val with | [Vinteger x] -> Vstring (BI.to_string x) | _ -> error loc "Integer->String expects one Integer argument"
-let sys_exit loc depth args_val = match args_val with +let sys_exit loc _depth args_val = match args_val with | [Vint n] -> Vcommand (fun _ -> exit n) | _ -> error loc "Sys.exit takes a single Int argument"
-let y_operator loc depth args = +let y_operator loc _depth args = match args with | [f] -> let yf_ref = ref Vundefined in let fname = (dloc, Some "f") in @@ -754,31 +754,31 @@ let nop_fun loc _ vs = match vs with | [v] -> v | _ -> error loc "Wrong number of argument to nop"
-let ref_make loc depth args_val = match args_val with +let ref_make loc _depth args_val = match args_val with | [v] -> Vcommand (fun () -> Vref (ref v)) | _ -> error loc "Ref.make takes a single value as argument"
-let ref_read loc depth args_val = match args_val with +let ref_read loc _depth args_val = match args_val with | [Vref (v)] -> Vcommand (fun () -> !v) | _ -> error loc "Ref.read takes a single Ref as argument"
-let ref_write loc depth args_val = match args_val with +let ref_write loc _depth args_val = match args_val with | [value; Vref (actual)] -> Vcommand (fun () -> actual := value; tunit) | _ -> error loc "Ref.write takes a value and a Ref as argument"
let gensym = let count = ref 0 in - (fun loc depth args_val -> match args_val with - | [v] -> Vcommand (fun () -> ( + (fun loc _depth args_val -> match args_val with + | [_v] -> Vcommand (fun () -> ( count := ((!count) + 1); Vsexp (Symbol (dloc,(" %gensym% no "^(string_of_int (!count))^" "))))) | _ -> error loc "gensym takes a Unit as argument")
-let getenv loc depth args_val = match args_val with - | [v] -> Vcommand (fun () -> Velabctx !macro_monad_elab_context) +let getenv loc _depth args_val = match args_val with + | [_v] -> Vcommand (fun () -> Velabctx !macro_monad_elab_context) | _ -> error loc "getenv takes a single Unit as argument"
-let debug_doc loc depth args_val = match args_val with +let debug_doc loc _depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> (try let idx = senv_lookup name ectx in let elem = lctx_lookup (ectx_to_lctx ectx) @@ -788,7 +788,7 @@ let debug_doc loc depth args_val = match args_val with with _ -> Vstring "element not found") | _ -> error loc "Elab.debug_doc takes a String and an Elab_Context as arguments"
-let is_bound loc depth args_val = match args_val with +let is_bound loc _depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (try (ignore (senv_lookup name ectx); true) with Senv_Lookup_Fail _ -> false) @@ -882,40 +882,40 @@ let ctor_arg_pos name arg ectx = | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)
-let is_constructor loc depth args_val = match args_val with +let is_constructor loc _depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx) | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments"
-let is_nth_erasable loc depth args_val = match args_val with +let is_nth_erasable loc _depth args_val = match args_val with | [Vstring name; Vint nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name nth_arg ectx) | _ -> error loc "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments"
-let is_arg_erasable loc depth args_val = match args_val with +let is_arg_erasable loc _depth args_val = match args_val with | [Vstring t; Vstring arg; Velabctx ectx] -> o2v_bool (erasable_p2 t arg ectx) | _ -> error loc "Elab.is-arg-erasable takes two String and an Elab_Context as arguments"
-let nth_arg loc depth args_val = match args_val with +let nth_arg loc _depth args_val = match args_val with | [Vstring t; Vint nth; Velabctx ectx] -> Vstring (nth_ctor_arg t nth ectx) | _ -> error loc "Elab.nth-arg takes a String, an Int and an Elab_Context as arguments"
-let arg_pos loc depth args_val = match args_val with +let arg_pos loc _depth args_val = match args_val with | [Vstring t; Vstring a; Velabctx ectx] -> Vint (ctor_arg_pos t a ectx) | _ -> error loc "Elab.arg-pos takes two String and an Elab_Context as arguments"
-let array_append loc depth args_val = match args_val with +let array_append loc _depth args_val = match args_val with | [v; Varray a] -> Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v)) | _ -> error loc "Array.append takes a value followed by an Array as arguments"
-let array_create loc depth args_val = match args_val with +let array_create loc _depth args_val = match args_val with | [Vint len; v] -> Varray (Array.make len v) | _ -> error loc "Array.make takes an Int and a value and as arguemnts"
-let array_length loc depth args_val = match args_val with +let array_length loc _depth args_val = match args_val with | [Varray a] -> Vint (Array.length a) | _ -> error loc "Array.length takes an Array as argument"
-let array_set loc depth args_val = match args_val with +let array_set loc _depth args_val = match args_val with | [Vint idx; v; Varray a] -> if (idx > (Array.length a) || idx < 0) then (warning loc "Array.set index out of bounds (array unchanged)"; @@ -925,7 +925,7 @@ let array_set loc depth args_val = match args_val with (Array.set copy idx v; Varray copy) | _ -> error loc "Array.set takes an Int, a value and an Array as arguments"
-let array_get loc depth args_val = match args_val with +let array_get loc _depth args_val = match args_val with | [dflt; Vint idx; Varray a] -> if (idx >= (Array.length a)) || (idx < 0) then dflt @@ -937,11 +937,11 @@ let array_get loc depth args_val = match args_val with (* Vundefined is used in array_empty because we have no default value ("array_create 0 0" has a default value v (Vint 0)). *) -let array_empty loc depth args_val = match args_val with +let array_empty loc _depth args_val = match args_val with | [_] -> Varray (Array.make 0 Vundefined) | _ -> error loc "Array.empty takes a Unit as single argument"
-let test_fatal loc depth args_val = match args_val with +let test_fatal loc _depth args_val = match args_val with | [Vstring section; Vstring msg] -> Vcommand (fun () -> Log.print_entry @@ -950,7 +950,7 @@ let test_fatal loc depth args_val = match args_val with ) | _ -> error loc "Test.fatal takes two String as argument"
-let test_warning loc depth args_val = match args_val with +let test_warning loc _depth args_val = match args_val with | [Vstring section; Vstring msg] -> Vcommand (fun () -> Log.print_entry @@ -958,7 +958,7 @@ let test_warning loc depth args_val = match args_val with tunit) | _ -> error loc "Test.warning takes two String as argument"
-let test_info loc depth args_val = match args_val with +let test_info loc _depth args_val = match args_val with | [Vstring section; Vstring msg] -> Vcommand (fun () -> Log.print_entry @@ -966,13 +966,13 @@ let test_info loc depth args_val = match args_val with tunit) | _ -> error loc "Test.info takes two String as argument"
-let test_location loc depth args_val = match args_val with +let test_location loc _depth args_val = match args_val with | [_] -> Vstring (loc.file ^ ":" ^ string_of_int loc.line ^ ":" ^ string_of_int loc.column) | _ -> error loc "Test.location takes a Unit as argument"
-let test_true loc depth args_val = match args_val with - | [Vstring name; Vcons ((dloc, b), [])] -> +let test_true loc _depth args_val = match args_val with + | [Vstring name; Vcons ((_dloc, b), [])] -> if b = "true" then Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); ttrue) @@ -981,8 +981,8 @@ let test_true loc depth args_val = match args_val with tfalse) | _ -> error loc "Test.true takes a String and a Bool as argument"
-let test_false loc depth args_val = match args_val with - | [Vstring name; Vcons ((dloc, b), [])] -> +let test_false loc _depth args_val = match args_val with + | [Vstring name; Vcons ((_dloc, b), [])] -> if b = "false" then Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); ttrue) @@ -991,7 +991,7 @@ let test_false loc depth args_val = match args_val with tfalse) | _ -> error loc "Test.false takes a String and a Bool as argument"
-let test_eq loc depth args_val = match args_val with +let test_eq loc _depth args_val = match args_val with | [Vstring name; v0; v1] -> if Env.value_equal v0 v1 then Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); ttrue) @@ -1000,7 +1000,7 @@ let test_eq loc depth args_val = match args_val with tfalse) | _ -> error loc "Test.eq takes a String and two values as argument"
-let test_neq loc depth args_val = match args_val with +let test_neq loc _depth args_val = match args_val with | [Vstring name; v0; v1] -> if Env.value_equal v0 v1 then Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); tfalse) @@ -1009,11 +1009,11 @@ let test_neq loc depth args_val = match args_val with ttrue) | _ -> error loc "Test.neq takes a String and two values as argument"
-let typelevel_succ loc (depth : eval_debug_info) (args_val: value_type list) = +let typelevel_succ loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint v] -> Vint(v + 1) | _ -> error loc ("`Typlevel.succ` expects 1 TypeLevel argument") -let typelevel_lub loc (depth : eval_debug_info) (args_val: value_type list) = +let typelevel_lub loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint v1; Vint v2] -> Vint(max v1 v2) | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2") @@ -1078,7 +1078,7 @@ let register_builtin_functions () = ] let _ = register_builtin_functions ()
-let builtin_constant v loc depth args_val = match args_val with +let builtin_constant v loc _depth args_val = match args_val with (* FIXME: Dummy arg because we currently can't define a Builtin * *constant* (except for cases like Eq.refl where the contant is not * actually used). *)
===================================== src/fmt.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -35,10 +35,10 @@ let str_size_int v = (int_of_float (log10 (float v))) + 1
(* print n char 'c' *) -let rec make_line c n = String.make n c +let make_line c n = String.make n c
(* Big numbers are replaced by #### *) -let cut_int (v:int) (start:int) (len:int): int = 0 +let cut_int (_v:int) (_start:int) (_len:int): int = 0
(* RALIGN * ----------------------- *)
===================================== src/heap.ml ===================================== @@ -1,4 +1,4 @@ -(* Copyright (C) 2020 Free Software Foundation, Inc. +(* Copyright (C) 2020, 2021 Free Software Foundation, Inc. * * Author: Simon Génier simon.genier@umontreal.ca * Keywords: languages, lisp, dependent types. @@ -136,7 +136,7 @@ let heap_store_cell : builtin_function = let heap_load_cell : builtin_function = fun location _ -> function - | [Vint address; Vint cell_index; value] + | [Vint address; Vint cell_index; _value] -> Vcommand (fun () -> load_cell address cell_index) | _ -> error ~location "`Heap.store-cell` expects [Int; Int]"
===================================== src/inverse_subst.ml ===================================== @@ -87,7 +87,7 @@ let transfo (s: subst) : substIR option =
(** Returns the number of element in a sequence of S.Cons *) -let rec sizeOf (s: (int * int) list): int = List.length s +let sizeOf (s: (int * int) list): int = List.length s
(** Returns a dummy variable with the db_index idx *) @@ -114,18 +114,18 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): subst option = let fill_before (l: (int * int) list) (s: subst) (nbVar: int): subst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) - | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) + | (i1, _v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): subst option = (* Fill gaps *) match l with - | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None + | (idx1, _val1)::(idx2, _val2)::_tail when (idx1 = idx2) -> None
| (idx1, val1)::(idx2, val2)::tail when (idx2 - idx1) > 1 -> (match fill_after ((idx2, val2)::tail) nbVar shift with | None -> None | Some s -> Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) idx2 s)))
- | (idx1, val1)::(idx2, val2)::tail + | (_idx1, val1)::(idx2, val2)::tail -> (match fill_after ((idx2, val2)::tail) nbVar shift with | None -> None | Some s -> Some (S.cons (mkVar val1) s)) @@ -134,7 +134,7 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): subst option = -> Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) nbVar (S.shift shift)))
- | (idx1, val1)::[] + | (_idx1, val1)::[] -> Some (S.cons (mkVar val1) (S.shift shift))
| [] @@ -260,7 +260,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = (* FIXME: use mkSLlub? *) -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) - | Sort (l, (StypeOmega | StypeLevel)) -> e + | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) | Susp (e, s') -> apply_inv_subst (push_susp e s') s
===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language.
-Copyright (C) 2011-2020 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -28,7 +28,6 @@ open Fmt open Sexp open Pexp
-open Myers open Grammar
(* open Unify *) @@ -175,8 +174,8 @@ let metavar_lookup (id : meta_id) : metavar_info * biggest bucket length: 205 / 36 * found/new lexp entries: - / 2 *)
-let lexp_lexp' (e, h) = e -let lexp_hash (e, h) = h +let lexp_lexp' (e, _h) = e +let lexp_hash (_e, h) = h
(* Hash `Lexp` using combine_hash (lxor) with hash of "sub-lexp". *) let lexp'_hash (lp : lexp') = @@ -367,14 +366,14 @@ let pred_imm l pred = | Imm s -> pred s | _ -> false
-let is_imm l = pred_imm l (fun e -> true) +let is_imm l = pred_imm l (fun _ -> true)
let pred_var l pred = match lexp_lexp' l with | Var v -> pred v | _ -> false
-let is_var l = pred_var l (fun e -> true) +let is_var l = pred_var l (fun _ -> true)
let get_var l = match lexp_lexp' l with @@ -382,10 +381,10 @@ let get_var l = | _ -> Log.log_fatal ~section:"internal" "Lexp is not Var "
let get_var_db_index v = - let (n, idx) = v in idx + let (_n, idx) = v in idx
let get_var_vname v = - let (n, idx) = v in n + let (n, _idx) = v in n
let pred_inductive l pred = match lexp_lexp' l with @@ -398,9 +397,9 @@ match lexp_lexp' l with | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive "
let get_inductive_ctor i = - let (l, n, a, cs) = i in cs + let (_l, _n, _a, cs) = i in cs
-let is_inductive l = pred_inductive l (fun e -> true) +let is_inductive l = pred_inductive l (fun _ -> true)
(********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. @@ -534,7 +533,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) - | Sort (l, _) -> e + | Sort (_, _) -> e | Builtin _ -> e
| Let (l, defs, e) @@ -602,7 +601,7 @@ let clean e = (* FIXME: The new SLlub could have `succ` on both sides! *) -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) - | Sort (l, _) -> e + | Sort (_, _) -> e | Builtin _ -> e | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in @@ -702,7 +701,7 @@ let rec lexp_unparse lxp = lexp_unparse body])
| Call(lxp, largs) -> (* (arg_kind * lexp) list *) - let sargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in + let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs)
| Inductive(loc, label, lfargs, ctors) -> @@ -737,7 +736,7 @@ let rec lexp_unparse lxp = | [] -> Ppatsym (loc, Some str), lexp_unparse bch | _ -> let pat_args - = List.map (fun (kind, ((l,oname) as name)) + = List.map (fun (_kind, ((l,oname) as name)) -> match oname with | Some vdef -> (Some (l,vdef), name) | None -> (None, name)) @@ -776,7 +775,7 @@ let rec lexp_unparse lxp = [lexp_unparse l1; lexp_unparse l2]) | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") - | Sort (l, Stype sl) + | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl])
@@ -965,9 +964,9 @@ and lexp_str ctx (exp : lexp) : string =
| Susp (e, s) -> lexp_str ctx (push_susp e s)
- | Var ((loc, name), idx) -> maybename name ^ (index idx) ; + | Var ((_loc, name), idx) -> maybename name ^ (index idx) ;
- | Metavar (idx, subst, (loc, name)) + | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with | MVal e -> lexp_str ctx (push_susp e subst) @@ -992,15 +991,15 @@ and lexp_str ctx (exp : lexp) : string = (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body)
- | Arrow(k, (_, Some name), tp, loc, expr) -> + | Arrow(k, (_, Some name), tp, _loc, expr) -> "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ (kind_str k) ^ " " ^ (lexp_str' expr)
- | Arrow(k, (_, None), tp, loc, expr) -> + | Arrow(k, (_, None), tp, _loc, expr) -> "(" ^ (lexp_str' tp) ^ " " ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")"
- | Lambda(k, (loc, name), ltype, lbody) -> + | Lambda(k, (_loc, name), ltype, lbody) -> let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in
(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ @@ -1091,7 +1090,7 @@ and lexp_str_ctor ctx ctors =
SMap.fold (fun key value str -> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in - let str = List.fold_left (fun str (k, _, arg) + let str = List.fold_left (fun str (_k, _, arg) -> str ^ " " ^ (lexp_str ctx arg)) str value in str ^ ")")
===================================== src/log.ml ===================================== @@ -1,6 +1,6 @@ (* log.ml --- User Errors/Warnings log for Typer. -*- coding: utf-8 -*-
-Copyright (C) 2019 Free Software Foundation, Inc. +Copyright (C) 2019-2020 Free Software Foundation, Inc.
Author: Jean-Alexandre Barszcz jalex_b@hotmail.com Keywords: languages, lisp, dependent types. @@ -116,7 +116,7 @@ let maybe_color_string color_opt str = | Some color -> Fmt.color_string color str | None -> str
-let string_of_log_entry {level; kind; section; loc; msg} = +let string_of_log_entry {level; kind; section; loc; msg; _} = let color = if typer_log_config.color then (level_color level) else None in let parens s = "(" ^ s ^ ")" in (option_default "" (option_map string_of_location loc) @@ -141,7 +141,7 @@ let log_entry (entry : log_entry) = )
let count_msgs (lvlp : log_level -> bool) = - let count_step count {level} = + let count_step count {level; _} = if lvlp level then count + 1 else count in List.fold_left count_step 0 !typer_log
===================================== src/myers.ml ===================================== @@ -1,6 +1,6 @@ (* myers.ml --- Myers's stacks, a.k.a random-access singly-linked lists
-Copyright (C) 2014-2016 Free Software Foundation, Inc. +Copyright (C) 2014-2020 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: list, containers @@ -98,7 +98,7 @@ let length l = (* Find the first element for which the predicate `p' is true. * "Binary" search, assuming the list is "sorted" (i.e. all elements after * this one also return true). *) -let rec find p l = +let find p l = let rec find2 l1 l2 = match l1,l2 with | _, Mcons (x, l1, _, l2) when not (p x) -> find2 l1 l2 @@ -113,7 +113,7 @@ let rec find p l = (* Find the last node for which the predicate `p' is false. * "Binary" search, assuming the list is "sorted" (i.e. all elements after * this one also return true). *) -let rec findcdr p l = +let findcdr p l = let rec findcdr2 last l1 l2 = match l1,l2 with | _, (Mcons (x, l1, _, l2) as l) when not (p x) -> findcdr2 (Some l) l1 l2
===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps
-Copyright (C) 2011-2020 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -219,7 +219,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = lexp_whnf_aux (push_susp branch subst) ctx with Not_found -> match default - with | Some (v,default) + with | Some (_v,default) -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf_aux (push_susp default subst) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l @@ -243,7 +243,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | Let (l, defs, body) -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs)) ctx
- | elem -> e + | _elem -> e
in lexp_whnf_aux e ctx
@@ -347,18 +347,18 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _ -> false) | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 - | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) + | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, _vd2, t21, _, t22)) -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') t12 (srename vd1 t22) - | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) + | (Lambda (ak1, l1, t1, e1), Lambda (ak2, _l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs') e1 e2 | (Call (f1, args1), Call (f2, args2)) - -> let rec conv_arglist_p args1 args2 : bool = + -> let conv_arglist_p args1 args2 : bool = List.fold_left2 (fun eqp (ak1,t1) (ak2,t2) -> eqp && ak1 = ak2 @@ -369,7 +369,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> let rec conv_fields ctx vs fields1 fields2 = match fields1, fields2 with | ([], []) -> true - | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) + | ((ak1,vd1,t1)::fields1, (ak2,_vd2,t2)::fields2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) (set_shift vs) @@ -381,7 +381,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (* Args checked alright, now go on with the fields, * using the new context. *) SMap.equal (conv_fields ctx vs) cases1 cases2 - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) + | ((ak1,l1,t1)::args1, (ak2,_l2,t2)::args2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs) @@ -442,8 +442,8 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let rec mkctx ctx args s i vdefs1 vdefs2 fieldtypes = match vdefs1, vdefs2, fieldtypes with | [], [], [] -> Some (ctx, List.rev args, s) - | (ak1, vdef1)::vdefs1, (ak2, vdef2)::vdefs2, - (ak', vdef', ftype)::fieldtypes + | (ak1, vdef1)::vdefs1, (ak2, _vdef2)::vdefs2, + (ak', _vdef', ftype)::fieldtypes -> if ak1 = ak2 && ak2 = ak' then mkctx (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s)) @@ -471,7 +471,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | Invalid_argument _ -> false (* If the lists have different length *) ) && (match (def1, def2) with - | (Some (v1, e1), Some (v2, e2)) -> + | (Some (v1, e1), Some (_v2, e2)) -> let nctx = DB.lctx_extend ctx v1 Variable etype in let subst = S.shift 1 in let hlxp = mkVar ((DB.dloc, None), 0) in @@ -499,7 +499,7 @@ and mkSLlub ctx e1 e2 = | (_, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) - | (e1', e2') + | (_e1', _e2') -> let ce1 = level_canon lwhnf1 in let ce2 = level_canon lwhnf2 in if level_leq ce1 ce2 then e2 @@ -523,7 +523,7 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = * ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) * ^ "\n"); *) SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) - | (StypeLevel, Stype l2) + | (StypeLevel, Stype _l2) when ak == P.Aerasable && impredicative_universe_poly (* The safety/soundness of this rule is completely unknown. * It's pretty powerful, e.g. allows tuples containing @@ -636,14 +636,14 @@ and check'' erased ctx e = | Susp (e, s) -> check erased ctx (push_susp e s) | Let (l, defs, e) -> let _ = - List.fold_left (fun ctx (v, e, t) + List.fold_left (fun ctx (v, _e, t) -> (let _ = check_type DB.set_empty ctx t in DB.lctx_extend ctx v ForwardRef t)) ctx defs in let nerased = nerased_let defs erased in let nctx = DB.lctx_extend_rec ctx defs in (* FIXME: Termination checking! Positivity-checker! *) - let _ = List.fold_left (fun n (v, e, t) + let _ = List.fold_left (fun n (_v, e, t) -> assert_type nctx e (check (if DB.set_mem (n - 1) nerased @@ -685,7 +685,7 @@ and check'' erased ctx e = -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) ctx arg in match lexp'_whnf ft ctx with - | Arrow (ak', v, t1, l, t2) + | Arrow (ak', _v, t1, _l, t2) -> if not (ak == ak') then (error_tc ~loc:(lexp_location arg) "arg kind mismatch"; ()) @@ -697,7 +697,7 @@ and check'' erased ctx e = ^ lexp_string ft ^ ")!"); ft)) ft args - | Inductive (l, label, args, cases) + | Inductive (l, _label, args, cases) -> let rec arg_loop ctx erased args = match args with | [] @@ -719,7 +719,7 @@ and check'' erased ctx e = (* FIXME: If it does refer, * we get an ugly error! *) (mkSusp level' (L.sunshift n)) - | tt -> error_tc ~loc:(lexp_location t) + | _tt -> error_tc ~loc:(lexp_location t) ~print_action:(fun _ -> DB.print_lexp_ctx ictx; print_newline () ) @@ -792,7 +792,7 @@ and check'' erased ctx e = | [], [] -> (erased, ctx, hlxp) (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) - | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes + | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) (ssink vdef s) @@ -831,9 +831,9 @@ and check'' erased ctx e = ^ string_of_int diff ^ " cases missing")) | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret - | Cons (t, (l, name)) + | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -852,7 +852,7 @@ and check'' erased ctx e = let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs + | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, buildtype fargs) in buildtype fargs @@ -1008,7 +1008,7 @@ and get_type ctx e = | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega - | Var (((_, name), idx) as v) -> lookup_type ctx v + | Var (((_, _name), _idx) as v) -> lookup_type ctx v | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1028,13 +1028,13 @@ and get_type ctx e = | Call (f, args) -> let ft = get_type ctx f in List.fold_left - (fun ft (ak,arg) + (fun ft (_ak,arg) -> match lexp'_whnf ft ctx with - | Arrow (ak', v, t1, l, t2) + | Arrow (_ak', _v, _t1, _l, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args - | Inductive (l, label, args, cases) + | Inductive (l, _label, args, cases) (* FIXME: Use `check` here but silencing errors? *) -> let rec arg_loop args ctx = match args with @@ -1054,7 +1054,7 @@ and get_type ctx e = (* We need to unshift because the final type * cannot refer to the fields! *) (mkSusp level' (L.sunshift n)) - | tt -> level), + | _tt -> level), DB.lctx_extend ictx v Variable t, n + 1)) (level, ctx, 0) @@ -1067,10 +1067,10 @@ and get_type ctx e = arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct - | Case (l, e, ret, branches, default) -> ret - | Cons (t, (l, name)) + | Case (_l, _e, ret, _branches, _default) -> ret + | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) + | Inductive (_l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -1089,7 +1089,7 @@ and get_type ctx e = let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs + | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, buildtype fargs) in buildtype fargs @@ -1140,11 +1140,11 @@ let rec erase_type (lxp: lexp): E.elexp = | L.SortLevel _ -> E.Type lxp | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp + | L.Inductive(_l, _label, _, _) -> E.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) - | MVar (_, t, _) + | MVar (_, _t, _) -> Log.internal_error "Metavar in erase_type")
and filter_arg_list lst = @@ -1174,7 +1174,7 @@ and clean_map cases = | (P.Aerasable, _)::tl -> (* Drop the variable and substitute it in the body. *) clean_arg_list tl acc (S.cons erasure_dummy subst) - | (kind, var)::tl -> + | (_ak, var)::tl -> (* Keep the variable and sink the substitution. *) clean_arg_list tl (var::acc) (ssink var subst) | [] -> @@ -1245,7 +1245,7 @@ let ctx2tup ctx nctx = types) SMap.empty), cons_label), - List.mapi (fun i (oname, t) + List.mapi (fun i (oname, _t) -> (P.Aimplicit, mkVar (oname, offset - i - 1))) types) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs)
===================================== src/pexp.ml ===================================== @@ -1,6 +1,6 @@ (* pexp.ml --- Proto lambda-expressions, half-way between Sexp and Lexp.
-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2020 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -22,8 +22,6 @@ this program. If not, see http://www.gnu.org/licenses/. *)
open Util open Sexp (* Symbol *) -open Lexer -open Grammar
let pexp_error loc = Log.log_error ~section:"PEXP" ~loc
===================================== src/prelexer.ml ===================================== @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer.
-Copyright (C) 2011-2017 Free Software Foundation, Inc. +Copyright (C) 2011-2020 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -103,7 +103,7 @@ let rec prelex (file : string) (getline : unit -> string) ln ctx acc (doc : stri | '{' -> prelex' ((ln, cpos, bpos, acc) :: ctx) (bpos+1) (cpos+1) [] doc | '}' -> (match ctx with - | ((sln, scpos, sbpos, sacc) :: ctx) -> + | ((sln, scpos, _sbpos, sacc) :: ctx) -> prelex' ctx (bpos+1) (cpos+1) (Preblock ({file=file; line=sln; column=scpos; docstr=doc}, List.rev acc, @@ -134,7 +134,7 @@ let rec prelex (file : string) (getline : unit -> string) ln ctx acc (doc : stri with End_of_file -> match ctx with | [] -> List.rev acc - | ((ln, cpos, _, _) :: ctx) -> + | ((ln, cpos, _, _) :: _ctx) -> (prelexer_error {file=file; line=ln; column=cpos; docstr=""} "Unmatched opening brace"; List.rev acc)
===================================== src/sexp.ml ===================================== @@ -1,6 +1,6 @@ (* sexp.ml --- The Lisp-style Sexp abstract syntax tree.
-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -49,7 +49,7 @@ let pred_symbol s pred = | Symbol (_, n) -> pred n | _ -> false
-let is_symbol e = pred_symbol e (fun e -> true) +let is_symbol e = pred_symbol e (fun _e -> true)
(**************** Hash-consing symbols *********************)
@@ -91,7 +91,7 @@ let rec sexp_location s = | Float (l, _) -> l | Node (s, _) -> sexp_location s
-let rec sexp_name s = +let sexp_name s = match s with | Block _ -> "Block" | Symbol (_, "") -> "ε" @@ -125,7 +125,7 @@ let rec sexp_parse (g : grammar) (rest : sexp list) : (sexp * sexp list) = let sexp_parse = sexp_parse g in
- let rec compose_symbol (ss : symbol list) = match ss with + let compose_symbol (ss : symbol list) = match ss with | [] -> (Log.internal_error "empty operator!") | (l,_)::_ -> (l, String.concat "_" (List.map (fun (_,s) -> s) (List.rev ss))) in @@ -197,7 +197,7 @@ let rec sexp_parse (g : grammar) (rest : sexp list) | _ -> false then op else (s::op)) (push_largs largs rargs true) [] - | (Some ll, None) + | (Some _ll, None) -> (mk_node (s::op) largs rargs true, rest') with Not_found -> sexp_parse rest' level op largs (e::rargs)) @@ -232,7 +232,7 @@ let sexp_parse_all grm tokens limit : sexp * token list = let sexp_p_list (s : sexp) (exceptions : string list) : sexp list = match s with | Symbol (_, "") -> [] - | Node (Symbol (_, head), tail) when List.mem head exceptions -> [s] + | Node (Symbol (_, head), _tail) when List.mem head exceptions -> [s] | Node (head, tail) -> head :: tail | _ -> [s]
===================================== src/tweak.ml deleted ===================================== @@ -1,271 +0,0 @@ -(* tweak.ml --- A tweaked version of OCaml's weak.ml - * - * Copyright (C) 2016 Free Software Foundation, Inc. - * - * The tweak consists in getting rid of `get_copy` and use `get` instead. *) - -(***********************************************************************) -(* *) -(* OCaml *) -(* *) -(* Damien Doligez, projet Para, INRIA Rocquencourt *) -(* *) -(* Copyright 1997 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU Library General Public License, with *) -(* the special exception on linking described in file ../LICENSE. *) -(* *) -(***********************************************************************) - -type 'a t = 'a Weak.t - -let create = Weak.create -let length = Weak.length -let get = Weak.get -let set = Weak.set -let check = Weak.check -let blit = Weak.blit - -module type S = Weak.S - -module Make (H : Hashtbl.HashedType) : (S with type data = H.t) = struct - - type 'a weak_t = 'a t - let weak_create = create - let emptybucket = weak_create 0 - - type data = H.t - - type t = { - mutable table : data weak_t array; - mutable hashes : int array array; - mutable limit : int; (* bucket size limit *) - mutable oversize : int; (* number of oversize buckets *) - mutable rover : int; (* for internal bookkeeping *) - } - - let get_index t h = (h land max_int) mod (Array.length t.table) - - let limit = 7 - let over_limit = 2 - - let create sz = - let sz = if sz < 7 then 7 else sz in - let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in - { - table = Array.make sz emptybucket; - hashes = Array.make sz [| |]; - limit = limit; - oversize = 0; - rover = 0; - } - - let clear t = - for i = 0 to Array.length t.table - 1 do - t.table.(i) <- emptybucket; - t.hashes.(i) <- [| |]; - done; - t.limit <- limit; - t.oversize <- 0 - - - let fold f t init = - let rec fold_bucket i b accu = - if i >= length b then accu else - match get b i with - | Some v -> fold_bucket (i+1) b (f v accu) - | None -> fold_bucket (i+1) b accu - in - Array.fold_right (fold_bucket 0) t.table init - - - let iter f t = - let rec iter_bucket i b = - if i >= length b then () else - match get b i with - | Some v -> f v; iter_bucket (i+1) b - | None -> iter_bucket (i+1) b - in - Array.iter (iter_bucket 0) t.table - - - let iter_weak f t = - let rec iter_bucket i j b = - if i >= length b then () else - match check b i with - | true -> f b t.hashes.(j) i; iter_bucket (i+1) j b - | false -> iter_bucket (i+1) j b - in - Array.iteri (iter_bucket 0) t.table - - - let rec count_bucket i b accu = - if i >= length b then accu else - count_bucket (i+1) b (accu + (if check b i then 1 else 0)) - - - let count t = - Array.fold_right (count_bucket 0) t.table 0 - - - let next_sz n = min (3 * n / 2 + 3) Sys.max_array_length - let prev_sz n = ((n - 3) * 2 + 2) / 3 - - let test_shrink_bucket t = - let bucket = t.table.(t.rover) in - let hbucket = t.hashes.(t.rover) in - let len = length bucket in - let prev_len = prev_sz len in - let live = count_bucket 0 bucket 0 in - if live <= prev_len then begin - let rec loop i j = - if j >= prev_len then begin - if check bucket i then loop (i + 1) j - else if check bucket j then begin - blit bucket j bucket i 1; - hbucket.(i) <- hbucket.(j); - loop (i + 1) (j - 1); - end else loop i (j - 1); - end; - in - loop 0 (length bucket - 1); - if prev_len = 0 then begin - t.table.(t.rover) <- emptybucket; - t.hashes.(t.rover) <- [| |]; - end else begin - Obj.truncate (Obj.repr bucket) (prev_len + 1); - Obj.truncate (Obj.repr hbucket) prev_len; - end; - if len > t.limit && prev_len <= t.limit then t.oversize <- t.oversize - 1; - end; - t.rover <- (t.rover + 1) mod (Array.length t.table) - - - let rec resize t = - let oldlen = Array.length t.table in - let newlen = next_sz oldlen in - if newlen > oldlen then begin - let newt = create newlen in - let add_weak ob oh oi = - let setter nb ni _ = blit ob oi nb ni 1 in - let h = oh.(oi) in - add_aux newt setter None h (get_index newt h); - in - iter_weak add_weak t; - t.table <- newt.table; - t.hashes <- newt.hashes; - t.limit <- newt.limit; - t.oversize <- newt.oversize; - t.rover <- t.rover mod Array.length newt.table; - end else begin - t.limit <- max_int; (* maximum size already reached *) - t.oversize <- 0; - end - - and add_aux t setter d h index = - let bucket = t.table.(index) in - let hashes = t.hashes.(index) in - let sz = length bucket in - let rec loop i = - if i >= sz then begin - let newsz = min (3 * sz / 2 + 3) (Sys.max_array_length - 1) in - if newsz <= sz then failwith "Weak.Make: hash bucket cannot grow more"; - let newbucket = weak_create newsz in - let newhashes = Array.make newsz 0 in - blit bucket 0 newbucket 0 sz; - Array.blit hashes 0 newhashes 0 sz; - setter newbucket sz d; - newhashes.(sz) <- h; - t.table.(index) <- newbucket; - t.hashes.(index) <- newhashes; - if sz <= t.limit && newsz > t.limit then begin - t.oversize <- t.oversize + 1; - for _i = 0 to over_limit do test_shrink_bucket t done; - end; - if t.oversize > Array.length t.table / over_limit then resize t; - end else if check bucket i then begin - loop (i + 1) - end else begin - setter bucket i d; - hashes.(i) <- h; - end; - in - loop 0 - - - let add t d = - let h = H.hash d in - add_aux t set (Some d) h (get_index t h) - - - let find_or t d ifnotfound = - let h = H.hash d in - let index = get_index t h in - let bucket = t.table.(index) in - let hashes = t.hashes.(index) in - let sz = length bucket in - let rec loop i = - if i >= sz then ifnotfound h index - else if h = hashes.(i) then begin - match get bucket i with - | Some v when H.equal v d -> v - | _ -> loop (i + 1) - end else loop (i + 1) - in - loop 0 - - - let merge t d = - find_or t d (fun h index -> add_aux t set (Some d) h index; d) - - - let find t d = find_or t d (fun h index -> raise Not_found) - - let find_shadow t d iffound ifnotfound = - let h = H.hash d in - let index = get_index t h in - let bucket = t.table.(index) in - let hashes = t.hashes.(index) in - let sz = length bucket in - let rec loop i = - if i >= sz then ifnotfound - else if h = hashes.(i) then begin - match get bucket i with - | Some v when H.equal v d -> iffound bucket i - | _ -> loop (i + 1) - end else loop (i + 1) - in - loop 0 - - - let remove t d = find_shadow t d (fun w i -> set w i None) () - - let mem t d = find_shadow t d (fun w i -> true) false - - let find_all t d = - let h = H.hash d in - let index = get_index t h in - let bucket = t.table.(index) in - let hashes = t.hashes.(index) in - let sz = length bucket in - let rec loop i accu = - if i >= sz then accu - else if h = hashes.(i) then begin - match get bucket i with - | Some v when H.equal v d - -> loop (i + 1) (v :: accu) - | _ -> loop (i + 1) accu - end else loop (i + 1) accu - in - loop 0 [] - - - let stats t = - let len = Array.length t.table in - let lens = Array.map length t.table in - Array.sort compare lens; - let totlen = Array.fold_left ( + ) 0 lens in - (len, count t, totlen, lens.(0), lens.(len/2), lens.(len-1)) - - -end
===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms
-Copyright (C) 2016-2020 Free Software Foundation, Inc. +Copyright (C) 2016-2021 Free Software Foundation, Inc.
Author: Vincent Bonnevalle tiv.crb@gmail.com
@@ -70,8 +70,8 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, Stype e) -> oi e | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false - | Var (_, i) -> false - | Susp (e, s) -> Log.internal_error "`e` should be "clean" here!?" + | Var (_, _i) -> false + | Susp (_e, _s) -> Log.internal_error "`e` should be "clean" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs @@ -92,10 +92,10 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with let o = match def with | None -> o | Some (_, e) -> o || oi e in SMap.fold (fun _ (_, _, e) o -> o || oi e) cases o - | Metavar (id', _, name) when id' = id -> true + | Metavar (id', _, _name) when id' = id -> true | Metavar (id', _, _) -> (match metavar_lookup id' with - | MVal e -> Log.internal_error "`e` should be "clean" here!?" + | MVal _e -> Log.internal_error "`e` should be "clean" here!?" (* ; oi e *) | MVar (sl', t, cl) -> if sl' > sl then @@ -225,8 +225,8 @@ and unify' (e1: lexp) (e2: lexp) be substituted with further reduction; 2. Calls, because they might become redexes; 3. Case expressions, for the same reason. *) - | (_, Var _) -> unify_var e2' e1' ctx vs' - | (Var _, _) -> unify_var e1' e2' ctx vs' + | (_, Var _) -> unify_var e2' e1' ctx + | (Var _, _) -> unify_var e1' e2' ctx | (_, Call _) -> unify_call e2' e1' ctx vs' | (Call _, _) -> unify_call e1' e2' ctx vs' (* FIXME: Handle `Case` expressions. *) @@ -408,7 +408,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) - Var , Var -> IF same var THEN ok ELSE constraint - Var , lexp -> Constraint *) -and unify_var (var: lexp) (lxp: lexp) ctx vs +and unify_var (var: lexp) (lxp: lexp) ctx : return_type = match (lexp_lexp' var, lexp_lexp' lxp) with | (Var _, Var _) when OL.conv_p ctx var lxp -> [] @@ -565,8 +565,8 @@ and is_same arglist arglist2 =
and unify_inductive lxp1 lxp2 ctx vs = match lexp_lexp' lxp1, lexp_lexp' lxp2 with - | (Inductive (_loc1, label1, args1, consts1), - Inductive (_loc2, label2, args2, consts2)) + | (Inductive (_loc1, _label1, args1, consts1), + Inductive (_loc2, _label2, args2, consts2)) -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2 | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]
@@ -575,7 +575,7 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) else - List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, v2, t2)) + List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, _v2, t2)) -> (DB.lexp_ctx_cons ctx v1 Variable t1, OL.set_shift vs, if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)]
===================================== src/util.ml ===================================== @@ -1,6 +1,6 @@ (* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-
-Copyright (C) 2011-2020 Free Software Foundation, Inc. +Copyright (C) 2011-2021 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -29,7 +29,7 @@ module UPDATABLE(Base : Map.S) = struct let before = find_opt key map in match before, f before with | _, Some after -> add key after map - | Some before, None -> remove key map + | Some _before, None -> remove key map | None, None -> map end
@@ -55,10 +55,10 @@ type vref = vname * db_index type bottom = | B_o_t_t_o_m_ of bottom
let get_vname_name_option vname = - let (loc, name) = vname in name + let (_loc, name) = vname in name
let get_vname_name vname = - let (loc, name) = vname in + let (_loc, name) = vname in match name with | Some n -> n | _ -> "" (* FIXME: Replace with dummy_name ? *)
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a2a6e95ebfb15d296ff3cd8f326357241...
Afficher les réponses par date