- Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][main] In elaboration, check residues only under certain conditions.
by Stefan (＠monnier) 03 Dec '24

03 Dec '24

Stefan pushed to branch main at Stefan / Typer Commits: 8ba2cf0f by Maxim Bernard at 2024-12-03T14:19:27-05:00 In elaboration, check residues only under certain conditions. * src/elab.ml (infer_and_generalize_def): Check only for residues that contain no uninstantiated metavariables in an outer scope. Also perform such a check after elaboration of top-level definitions, although this should not be absolutely necessary. * src/unification.ml (check_no_residues): Replace with a function that signals errors for residues that have no chance of being solvable later during elaboration. - - - - - 2 changed files: - src/elab.ml - src/unification.ml Changes: ===================================== src/elab.ml ===================================== @@ -1434,8 +1434,9 @@ and infer_and_generalize_type (ctx : elab_context) se name = and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in - Unif.check_no_residues (location e); - Unif.clean_residues (); + Unif.raise_errors_on_out_of_scope_residues + (sexp_location se) + (ectx_to_scope_level ctx); let g = resolve_instances_and_generalize nctx e in let e' = g wrapLambda e in let t' = g (fun ne name t _l e @@ -1447,8 +1448,8 @@ and infer_and_generalize_def (ctx : elab_context) se = and lexp_decls_1 (sdecls : sexp list) (* What's already parsed *) (tokens : token list) (* Rest of input *) - (ectx : elab_context) (* External ctx. *) - (nctx : elab_context) (* New context. *) + (ectx : elab_context) (* External ctx. *) + (nctx : elab_context) (* New context. *) (pending_decls : location SMap.t) (* Pending type decls. *) (pending_defs : (symbol * sexp) list) (* Pending definitions. *) : (vname * lexp * ltype) list * sexp list * token list * elab_context = @@ -1594,7 +1595,10 @@ and lexp_decls_1 to each other (i.e. they can be mutually recursive). - hence the overall "list of lists" is a sequence of such blocs of mutually-recursive definitions. *) -and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) +and lexp_p_decls ?(check_residues = true) + (sdecls : sexp list) + (tokens : token list) + (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = let rec impl sdecls tokens ctx = match (sdecls, tokens) with @@ -1602,6 +1606,11 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) | _ -> let decls, sdecls, tokens, nctx = lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in + if check_residues then + (* This is merely a sanity check. No residues should remain after + * the elaboration of a top-level definition (i.e. not in a `let` + * statement). *) + Unif.raise_error_on_all_residues (); Log.stop_on_error (); let declss, nnctx = impl sdecls tokens nctx in decls :: declss, nnctx in @@ -1865,7 +1874,7 @@ let rec sform_case ctx sinfo sargs ot = match sargs with let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] - -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in + -> let declss, nctx = lexp_p_decls ~check_residues:false [sdecls] [] ctx in let s, off = List.fold_left (fun (s, off) decls -> (OL.lexp_defs_subst loc s decls, off + List.length decls)) ===================================== src/unification.ml ===================================== @@ -21,6 +21,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Ir open Lexp +open Util module OL = Opslexp module DB = Debruijn @@ -52,19 +53,43 @@ let current_residues = ref ([] : (lexp_context * lexp * lexp) list) let add_residue (ctx : lexp_context) (e1 : lexp) (e2 : lexp) = current_residues := (ctx, e1, e2) :: !current_residues -let check_no_residues (first_def_loc : Source.Location.t) : unit = - (* Raises an error for every remaining residue. *) +let signal_residue (loc : location) (e1 : lexp) (e2 : lexp) = + Log.log_error + ~section:"UNIF" + ~loc:loc + ("@[<v>Remaining residue. Can't unify:" + ^^ "@, @[<hov 2>%a@]" + ^^ "@,with:" + ^^ "@, @[<hov 2>%a@]@]") + pp_print_clean_lexp e1 + pp_print_clean_lexp e2 + +let raise_errors_on_out_of_scope_residues + (location : location) + (scope_level : scope_level) = + (* For each residue that caused an error to be logged, remove it from + * `current_residues`. *) + let new_residue_list = List.filter + (fun (_ctx, e1, e2) -> + let (_, e1_free_mv) = OL.fv e1 in + let (_, e2_free_mv) = OL.fv e2 in + let (free_mv_map, _) = OL.mv_set_union e1_free_mv e2_free_mv in + (* Only raise an error if no metavariables appear outside of + * `scope_level`. *) + let to_flag = IMap.for_all + (fun _ (mv_scope_level, _, _, _) -> + mv_scope_level >= scope_level) + free_mv_map in + if to_flag then + signal_residue location e1 e2; + not to_flag) + !current_residues in + current_residues := new_residue_list + +let raise_error_on_all_residues () : unit = List.iter - (fun (_ctx, lxp1, lxp2) -> - Log.log_error - ~section:"UNIF" - ~loc:first_def_loc - ("@[<v>Remaining residue. Can't unify:" - ^^ "@, @[<hov 2>%a@]" - ^^ "@,with:" - ^^ "@, @[<hov 2>%a@]@]") - Fmt.pp_print_lexp (clean lxp1) - Fmt.pp_print_lexp (clean lxp2)) + (fun (_ctx, e1, e2) -> + signal_residue dummy_location e1 e2) !current_residues let clean_residues () : unit = View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8ba2cf0f847e40905cde3e14478e6be50… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8ba2cf0f847e40905cde3e14478e6be50… You're receiving this email because of your account on gitlab.com.

1 0

residues-elab
by Stefan Monnier 13 Nov '24

13 Nov '24

Salut Maxim, Commentaires et questions: > In elaboration, check residues only under certain conditions. > > * src/elab.ml: > In `infer_and_generalize_def`, only check for residues if the definition > contains no uninstantiated metavariables in an outer scope. Also, > restrict analysis to residues created for this particular definiton > (hence the `pre_residues` parameter). > > * src/unification.ml: > Change `check_no_residues` to run on a given list instead of all current > residues, and remove residues from the list once an error has been > logged. [ FWIW, le format que j'utilise habituellement dans Typer est celui du "GNU Coding Standard": https://www.gnu.org/prep/standards/html_node/Change-Logs.html C'était écrit à l'origine pour les fichiers ChangeLog plutot que pour les "commit message" des systèmes de contrôle de révision, donc il y a un petit peu d'ajustement à faire. ] > +let check_def_residues (e : lexp) > + (t : lexp) > + (scope_level : scope_level) > + (pre_residues : Unif.residue_list) = > + let (_, e_free_mv) = OL.fv e in > + let (_, t_free_mv) = OL.fv t in > + let (free_mv_map, _) = OL.mv_set_union e_free_mv t_free_mv in > + (* Only check residues if no metavariables appear outside of this > + * definition's scope level. *) > + if IMap.for_all > + (fun _ (mv_scope_level, _, _, _) -> > + mv_scope_level >= scope_level) > + free_mv_map > + then > + let this_def_residues = Unif.filter_residues pre_residues in > + Unif.raise_errors_on_residues (location e) this_def_residues Hmm... ça correspond pas tout à fait à l'idée que j'avais. Je pensais plutôt qcch comme: for all (_, e1, e2) in !current_residues do let (_, e1_free_mv) = OL.fv e1 in let (_, e2_free_mv) = OL.fv e2 in (* Check if the reside includes vars which can still be instantiated *) if IMap.for_all (fun _ (mv_scope_level, _, _, _) -> mv_scope_level > scope_level) free_mv_map then Unif.raise_errors_on_residues ... else ; (* All good: there's still hope to resolve this later. *) Et ma question est: si je comprends bien tu as testé que le code passe, maintenant, mais je ne vois plus de test que `current_residues` est vide "eventually". Est-on sûr qu'on ne va pas des fois accepter du code alors qu'il reste des résidus insatisfaits? Stefan

1 0

[Git][monnier/typer][main] 2 commits: Miscellanious bug fixes and code cleanups.
by Stefan (＠monnier) 12 Nov '24

12 Nov '24

Stefan pushed to branch main at Stefan / Typer Commits: 9c6d2169 by Maxim Bernard at 2024-10-31T15:26:08-04:00 Miscellanious bug fixes and code cleanups. * typer.ml: Flush standard output when loading file (otherwise line is not printed at the right time) and update copyright years. * typer.sh: Fix with right executable path. * src/fmt.ml: Flush standand output after printing lexp. * src/sexp.ml: Remove obsolete `location` function, since it's now in src/ir.ml. * src/unification.ml: Add rule in unification of sort levels for unifying lub with level zero. In default case of unifying two sort levels, return a residue instead of an impossible constraint. * src/lexp.ml: In `subst_eq`, support comparing identity substitution with `Cons`. * All files: Replace `Sexp.location` with `sexp_location` following changes in sexp.ml. - - - - - 5bf23466 by Stefan Monnier at 2024-11-12T15:17:46-05:00 Merge remote-tracking branch 'gitlab/misc-fixes' - - - - - 15 changed files: - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/fmt.ml - src/instargs.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/sexp.ml - src/unification.ml - typer.ml - typer.sh Changes: ===================================== src/builtin.ml ===================================== @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2021 Free Software Foundation, Inc. + * Copyright (C) 2016-2024 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -149,7 +149,6 @@ let register_builtin_csts () = OL.add_builtin_cst "Type0" 0 DB.type0; OL.add_builtin_cst "Type1" 0 DB.type1; OL.add_builtin_cst "Integer" 0 DB.type_integer; - OL.add_builtin_cst "Int" 0 DB.type_int; OL.add_builtin_cst "Float" 0 DB.type_float; OL.add_builtin_cst "String" 0 DB.type_string; OL.add_builtin_cst "Eq" 0 DB.type_eq; ===================================== src/debruijn.ml ===================================== @@ -441,7 +441,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc:(Sexp.location loc) ~print_action + ~loc:(sexp_location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name @@ -451,7 +451,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = with | Not_found -> fatal - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2023 Free Software Foundation, Inc. + * Copyright (C) 2011-2024 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -149,14 +149,14 @@ let log_proper_type_error var t s = match var with | (l, None) -> lexp_error - (Sexp.location l) + (sexp_location l) t "@[<v>Expression:@, @[<hov 2>%a@]@,of type :@, @[<hov 2>%a@]@,is not a proper type.@]" pp_print_clean_lexp t pp_print_clean_lexp s | (l, Some name) -> lexp_error - (Sexp.location l) + (sexp_location l) t "@[<v>Expression %s:@, @[<hov 2>%a@]@,of type :@, @[<hov 2>%a@]@,is not a proper type.@]" name @@ -208,7 +208,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = print_lexp_ctx (ectx_to_lctx ctx); print_newline () ) - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) "Error while type-checking"; raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' @@ -216,7 +216,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = | e -> info ~print_action:(lexp_print_details lxp) - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) "@[<v>Exception while conversion-checking types:@, @[<hov 2>%a@]@,and:@, @[<hov 2>%a@]@]" pp_print_clean_lexp ltype pp_print_clean_lexp ltype'; @@ -225,7 +225,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = elab_check_proper_type ctx ltype var else fatal - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) ("@[<v>Type check error (ctx_define error):" ^^ "@, @[<hov 2>%s = %a@]" ^^ "@,is not of type:" @@ -358,13 +358,13 @@ let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = -> let level s = match s with | Symbol (_, "") -> None | Integer (_, n) -> Some (Z.to_int n) - | _ -> sexp_error (Sexp.location s) "Expecting an integer or ()"; None in + | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in let grm = ectx_get_grammar ctx in ectx_set_grammar (Grammar.add name (level l, level r) grm) ctx | [o; _; _] - -> sexp_error (Sexp.location o) "Expecting a string"; ctx + -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ - -> sexp_error (Sexp.location loc) "define-operator expects 3 argument"; ctx + -> sexp_error (sexp_location loc) "define-operator expects 3 argument"; ctx let sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in @@ -384,7 +384,7 @@ let elab_varref ctx (loc, name) if ((List.length xs) > 0) then ". Did you mean: " ^ (String.concat " or " xs) ^" ?" else "" in - sexp_error (Sexp.location loc) {|The variable "%s" was not declared%s|} name relateds; + sexp_error (sexp_location loc) {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc) (* Turn metavar into plain vars after generalization. @@ -635,10 +635,10 @@ let rec sform_immediate ctx loc sargs ot = let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot | [_se] - -> sexp_error (Sexp.location loc) "Non-immediate passed to ##typer-immediate"; + -> sexp_error (sexp_location loc) "Non-immediate passed to ##typer-immediate"; sform_dummy_ret ctx loc | _ - -> sexp_error (Sexp.location loc) "Too many args to ##typer-immediate"; + -> sexp_error (sexp_location loc) "Too many args to ##typer-immediate"; sform_dummy_ret ctx loc @@ -680,7 +680,7 @@ and sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc:(Sexp.location loc) ("Bug in the elaboration of a metavar" + fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" ^^ " repeated at a different scope level!") else let t = match ot with @@ -693,7 +693,7 @@ and sform_identifier ctx loc sargs ot = let idx = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc:(Sexp.location loc) "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in rmmap := SMap.add name (idx, sl) (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy) @@ -702,11 +702,11 @@ and sform_identifier ctx loc sargs ot = -> elab_varref ctx (loc, name) | [_se] - -> sexp_error (Sexp.location loc) "Non-symbol passed to ##typer-identifier"; + -> sexp_error (sexp_location loc) "Non-symbol passed to ##typer-identifier"; sform_dummy_ret ctx loc | _ - -> sexp_error (Sexp.location loc) "Too many args to ##typer-identifier"; + -> sexp_error (sexp_location loc) "Too many args to ##typer-identifier"; sform_dummy_ret ctx loc and elab_via head default ctx se ot = @@ -730,7 +730,7 @@ and elaborate ctx se ot = (* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) - -> let l = Sexp.location se in + -> let l = sexp_location se in elaborate ctx (Node (l, Symbol (l, "typer-immediate"), [se])) ot | Node (_, se, []) -> elaborate ctx se ot @@ -765,7 +765,7 @@ and elaborate ctx se ot = and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with - | (_, Checked) -> fatal ~loc:(Sexp.location p) "`infer` got Checked!" + | (_, Checked) -> fatal ~loc:(sexp_location p) "`infer` got Checked!" | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) | (e, Inferred t) -> (e, t) @@ -778,7 +778,7 @@ and elab_special_form ctx f args ot = | _ -> lexp_error - (Sexp.location loc) + (sexp_location loc) f "@[<v>Unknown special-form:@, @[<hov 2>%a@]@]" pp_print_clean_lexp f; @@ -791,7 +791,7 @@ and elab_special_decl_form ctx f args = (* Special form. *) (get_special_decl_form name) ctx loc args | _ -> lexp_error - (Sexp.location loc) + (sexp_location loc) f "@[<v>Unknown special-decl-form:@, @[<hov 2>%a@]@]" pp_print_clean_lexp f; @@ -873,7 +873,7 @@ and unify_with_arrow ctx tloc lxp kind var aty match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error - (Sexp.location tloc) + (sexp_location tloc) lxp "@[<v>Type mismatch between:@, @[<hov 2>%a@]@,and:@, @[<hov 2>%a@]@]" pp_print_lexp t1 @@ -953,7 +953,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) -> lexp_error - (Sexp.location loc) + (sexp_location loc) lctor "@[<v>Expected pattern of type:@, @[<hov 2>%a@]@,but got:@, @[<hov 2>%a@]@]" pp_print_clean_lexp expected @@ -991,7 +991,7 @@ and check_case rtype (loc, target, ppatterns) ctx = constructors | _ -> lexp_error - (Sexp.location target) + (sexp_location target) tlxp "@[<v>Can't \"case\" on objects of type@, @[<hov 2>%a@]@]" pp_print_clean_lexp tltp; @@ -1030,7 +1030,7 @@ and check_case rtype (loc, target, ppatterns) ctx = lbranches, Some (v, lexp) in let add_branch pctor pargs = - let loc = Sexp.location pctor in + let loc = sexp_location pctor 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 @@ -1129,7 +1129,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) -> if Eval.constructor_p name ctx then - add_branch (Symbol (Sexp.location l, name)) [] + add_branch (Symbol (sexp_location l, name)) [] else add_default var (* A named default branch. *) | Ppatcons (_, pctor, pargs) -> add_branch pctor pargs in @@ -1156,17 +1156,17 @@ and elab_macro_call if !macro_tracing_enabled then (trace_macro - ~location:(Sexp.location location) + ~location:(sexp_location location) "@[<v>Expanding:@, @[<hov 2>%a@]@]" pp_print_clean_lexp func; List.iteri (fun i arg -> - arg |> string_of_sexp |> trace_macro ~location:(Sexp.location location) {|input %d: %s|} i) + arg |> string_of_sexp |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) args); let sxp = lexp_expand_macro location func args ctx (Some t) in if !macro_tracing_enabled - then trace_macro ~location:(Sexp.location location) "@[<v>Output:@,@[<hov>%s@]@]" (string_of_sexp sxp); + then trace_macro ~location:(sexp_location location) "@[<v>Output:@,@[<hov>%s@]@]" (string_of_sexp sxp); elaborate ctx sxp ot @@ -1220,7 +1220,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = -> (if not (SMap.is_empty pending) then let pending = SMap.bindings pending in let loc = match pending with - | (_, sarg)::_ -> Sexp.location sarg + | (_, sarg)::_ -> sexp_location sarg | _ -> assert false in lexp_error loc func {|Explicit actual args "%s" have no matching formal args.|} @@ -1338,15 +1338,15 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - let value = EV.eval_call (Sexp.location loc) (Evar ((dsinfo, Some "expand_macro"), 0)) + let value = EV.eval_call (sexp_location loc) (Evar ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args in match value with | Vcommand cmd -> (match cmd () with | Vsexp sxp -> sxp - | v -> value_fatal (Sexp.location loc) v "@[<v>Macro should return an IO sexp:@, @[<hov 2>%a@]@]" + | v -> value_fatal (sexp_location loc) v "@[<v>Macro should return an IO sexp:@, @[<hov 2>%a@]@]" pp_print_clean_lexp macro_funct) - | v -> value_fatal (Sexp.location loc) v "@[<v>Macro should return an IO:@, @[<hov 2>%a@]@]" + | v -> value_fatal (sexp_location loc) v "@[<v>Macro should return an IO:@, @[<hov 2>%a@]@]" pp_print_clean_lexp macro_funct @@ -1555,7 +1555,7 @@ and lexp_decls_1 head, [Symbol s; Node (location, - Symbol (Sexp.location d, "lambda_->_"), + Symbol (sexp_location d, "lambda_->_"), [sexp_u_list args location; body])])] nctx pending_decls pending_defs @@ -1579,7 +1579,7 @@ and lexp_decls_1 let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in recur [sdecl'] nctx pending_decls pending_defs else ( - error ~loc:(Sexp.location sxp) "Invalid declaration syntax"; + error ~loc:(sexp_location sxp) "Invalid declaration syntax"; recur [] nctx pending_decls pending_defs ) @@ -1623,9 +1623,9 @@ and sform_declexpr ctx loc sargs _ot = | [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 | Some lxp -> (lxp, Lazy) - | None -> error ~loc:(Sexp.location loc) "no expr available"; + | None -> error ~loc:(sexp_location loc) "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc:(Sexp.location loc) "declexpr expects one argument"; + | _ -> error ~loc:(sexp_location loc) "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1633,7 +1633,7 @@ 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) - | _ -> error ~loc:(Sexp.location loc) "decltype expects one argument"; + | _ -> error ~loc:(sexp_location loc) "decltype expects one argument"; sform_dummy_ret ctx loc @@ -1648,21 +1648,21 @@ let sform_built_in ctx loc sargs ot = (* FIXME: This `L.clean` is one of the last remaining uses of the * function. It's not indispensible, tho it might still be useful for * performance of type-inference (at least until we have proper - * memoization of push_susp and/or whnf). *) + * memoization of push_susp and/or whnf). *) -> let ltp' = Lexp.clean ltp in - let bi = mkBuiltin ((Sexp.location loc, name), ltp') in + let bi = mkBuiltin ((sexp_location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions) || List.mem name DB.builtin_axioms) then - sexp_error (Sexp.location loc) {|Unknown built-in "%s"|} name; + sexp_error (sexp_location loc) {|Unknown built-in "%s"|} name; OL.add_builtin_cst name (DB.get_size ctx) bi; (bi, Checked) - | None -> error ~loc:(Sexp.location loc) "Built-in's type not provided by context!"; + | None -> error ~loc:(sexp_location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error ~loc:(Sexp.location loc) "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc:(sexp_location loc) "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error ~loc:(Sexp.location loc) "Use of `Built-in` in user code"; + | false, _ -> error ~loc:(sexp_location loc) "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs _ot = @@ -1671,9 +1671,9 @@ let sform_datacons ctx loc sargs _ot = -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy) - | [_;_] -> sexp_error (Sexp.location loc) "Second arg of ##constr should be a symbol"; + | [_;_] -> sexp_error (sexp_location loc) "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc - | _ -> sexp_error (Sexp.location loc) "##constr requires two arguments"; + | _ -> sexp_error (sexp_location loc) "##constr requires two arguments"; sform_dummy_ret ctx loc let elab_colon_to_ak k = match k with @@ -1693,20 +1693,20 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = (arg, Some name), Some e) | Symbol (_l, name) -> (Anormal, (arg, Some name), None) | _ -> sexp_error ~print_action:(fun _ -> print_sexp arg; print_newline ()) - (Sexp.location arg) + (sexp_location arg) "Unrecognized formal arg"; (Anormal, (arg, None), None) let sform_typecons ctx loc sargs _ot = match sargs with - | [] -> sexp_error (Sexp.location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) + | [] -> sexp_error (sexp_location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (_, label, formals) -> (label, formals) | _ -> (formals, []) in let label = match label with | Symbol label -> label - | _ -> let loc = Sexp.location label in + | _ -> let loc = sexp_location label in sexp_error loc "Unrecognized inductive type name"; (loc, "<error>") in @@ -1735,7 +1735,7 @@ let sform_typecons ctx loc sargs _ot = (* This is a constructor with no args *) | Symbol s -> (s, [])::pcases - | _ -> sexp_error (Sexp.location case) + | _ -> sexp_error (sexp_location case) "Unrecognized constructor declaration"; pcases) constrs [] in @@ -1748,7 +1748,7 @@ let sform_hastype ctx loc sargs _ot = | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) - | _ -> sexp_error (Sexp.location loc) "##_:_ takes two arguments"; + | _ -> sexp_error (sexp_location loc) "##_:_ takes two arguments"; sform_dummy_ret ctx loc let sform_arrow kind ctx loc sargs _ot = @@ -1761,7 +1761,7 @@ let sform_arrow kind ctx loc sargs _ot = let nctx = ectx_extend ctx v Variable lt1 in let lt2 = infer_type st2 nctx (st2, None) in (mkArrow (loc, kind, v, lt1, lt2), Lazy) - | _ -> sexp_error (Sexp.location loc) "##_->_ takes two arguments"; + | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc let rec sform_lambda kind ctx loc sargs ot = @@ -1770,7 +1770,7 @@ let rec sform_lambda kind ctx loc sargs ot = -> let (arg, ost1) = match sarg with | Node (_, Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st) | Symbol arg -> (elab_p_id arg, None) - | _ -> sexp_error (Sexp.location sarg) + | _ -> sexp_error (sexp_location sarg) "Unrecognized lambda argument"; ((dsinfo, None), None) in @@ -1833,7 +1833,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> sexp_error - (Sexp.location loc) "##lambda_%s_ takes two arguments" + (sexp_location loc) "##lambda_%s_ takes two arguments" (match kind with | Anormal -> "->" | Aimplicit -> "=>" @@ -1845,7 +1845,7 @@ let rec sform_case ctx sinfo sargs ot = match sargs with -> let parse_case branch = match branch with | Node (_, Symbol (_, "_=>_"), [pat; code]) -> (pexp_p_pat pat, code) - | _ -> let l = (Sexp.location branch) in + | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; (Ppatsym (se, None), Symbol (l, "?")) in let pcases = List.map parse_case scases in @@ -1857,10 +1857,10 @@ let rec sform_case ctx sinfo sargs ot = match sargs with (* In case there are no branches, pretend there was a | anyway. *) | [_e] - -> let loc = Sexp.location sinfo in + -> let loc = sexp_location sinfo in sform_case ctx sinfo [Node (loc, Symbol (loc, "_|_"), sargs)] ot | _ - -> sexp_error (Sexp.location sinfo) "Unrecognized case expression"; + -> sexp_error (sexp_location sinfo) "Unrecognized case expression"; sform_dummy_ret ctx sinfo let sform_letin ctx loc sargs ot = match sargs with @@ -1876,7 +1876,7 @@ let sform_letin ctx loc sargs ot = match sargs with | Inferred t -> Inferred (mkSusp t s) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) - | _ -> sexp_error (Sexp.location loc) "Unrecognized let_in_ expression"; + | _ -> sexp_error (sexp_location loc) "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc let sform_proj ctx loc sargs _ = @@ -1886,9 +1886,9 @@ let sform_proj ctx loc sargs _ = let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) | [_;_] - -> sexp_error (Sexp.location loc) "Second argument is not a Symbol!"; + -> sexp_error (sexp_location loc) "Second argument is not a Symbol!"; sform_dummy_ret ctx loc - | _ -> sexp_error (Sexp.location loc) "Wrong arg number!"; + | _ -> sexp_error (sexp_location loc) "Wrong arg number!"; sform_dummy_ret ctx loc let rec infer_level ctx se : lexp = @@ -1899,7 +1899,7 @@ let rec infer_level ctx se : lexp = -> mkSortLevel (SLsucc (infer_level ctx se)) | Node (_, Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) - | _ -> let l = (Sexp.location se) in + | _ -> let l = (sexp_location se) in (sexp_error l "Unrecognized TypeLevel: %s" (string_of_sexp se); newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) se) @@ -1914,7 +1914,7 @@ let sform_type ctx loc sargs _ot = | [se] -> let l = infer_level ctx se in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) - | _ -> (sexp_error (Sexp.location loc) "##Type_ expects one argument"; + | _ -> (sexp_error (sexp_location loc) "##Type_ expects one argument"; sform_dummy_ret ctx loc) let sform_debruijn ctx loc sargs _ot = @@ -1925,7 +1925,7 @@ let sform_debruijn ctx loc sargs _ot = sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy) - | _ -> (sexp_error (Sexp.location loc) "##DeBruijn expects one integer argument"; + | _ -> (sexp_error (sexp_location loc) "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc) (* Only print var info *) @@ -1961,7 +1961,7 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc:(Sexp.location loc) {|Could not load "%s": file not found.|} file_name; [] + -> error ~loc:(sexp_location loc) {|Could not load "%s": file not found.|} file_name; [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx @@ -1973,7 +1973,7 @@ let sform_load usr_elctx loc sargs _ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error ~loc:(Sexp.location loc) "argument to load should be one file name (String)"; + | _ -> (error ~loc:(sexp_location loc) "argument to load should be one file name (String)"; !sform_default_ectx) in (* get lexp_context *) ===================================== src/elexp.ml ===================================== @@ -36,11 +36,11 @@ module SMap = Util.SMap let rec location : elexp -> Source.Location.t = function | Eimm (l, _) -> l - | Evar ((l, _), _) -> Sexp.location l + | Evar ((l, _), _) -> sexp_location l | Eproj (l, _, _) -> l | Ebuiltin ((l, _)) -> l | Elet (l, _, _) -> l - | Elambda ((l, _), _) -> Sexp.location l + | Elambda ((l, _), _) -> sexp_location l | Ecall (f, _) -> location f | Econs (_, (l, _)) -> l | Ecase (l, _, _, _) -> l ===================================== src/eval.ml ===================================== @@ -488,7 +488,7 @@ and eval_var ctx lxp v = try get_rte_variable vname idx ctx with | _e -> Log.log_fatal - ~loc:(Sexp.location sinfo) + ~loc:(sexp_location sinfo) "Variable: %s[%d] was not found\n%s" (maybename name) idx (trace_elexp lxp) ===================================== src/fmt.ml ===================================== @@ -537,7 +537,8 @@ and pp_print_lexp_decls (f : Format.formatter) (ldecls : ldecls list) : unit = ldecls and print_lexp (l : lexp) : unit = - Format.printf "%a" pp_print_lexp l + Format.printf "%a" pp_print_lexp l; + Format.print_flush () and string_of_lexp (l : lexp) : string = Format.asprintf "%a" pp_print_lexp l ===================================== src/instargs.ml ===================================== @@ -119,7 +119,7 @@ let search_instance : lexp option = Log.log_debug - ~loc:(Sexp.location sinfo) + ~loc:(sexp_location sinfo) "@[<v>Resolving type:@, @[<hov 2>%a@]@]" L.pp_print_clean_lexp t; let lctx = DB.ectx_to_lctx ctx in @@ -141,7 +141,7 @@ let search_instance let var = L.mkVar ((sinfo, namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in - Log.log_debug ~loc:(Sexp.location sinfo) + Log.log_debug ~loc:(sexp_location sinfo) ("@[<v>Considering potential instance:" ^^ "@, @[<hov 2>%a@]" ^^ "@,of type:" @@ -164,7 +164,7 @@ let search_instance | Possible -> (match !log_skipped_uncertain_matches with | Some level -> - Log.log_msg ignore level ~loc:(Sexp.location sinfo) + Log.log_msg ignore level ~loc:(sexp_location sinfo) ("@[<v>Skipping potential instance:" ^^ "@, @[<hov 2>%a@]" ^^ "@,of type:@, @[<hov 2>%a@]" @@ -200,7 +200,7 @@ let search_instance | None -> None | Some (i, (vname, _, t'), e) -> let t' = L.mkSusp t' (S.shift (i + 1)) in - Log.log_debug ~loc:(Sexp.location sinfo) + Log.log_debug ~loc:(sexp_location sinfo) ("@[<v>Found instance for:" ^^ "@, @[<hov 2>%a@]" ^^ "@,at index %i:" @@ -236,7 +236,7 @@ let resolve_instances instantiate_implicit e = and cause an error. *) | None -> Log.log_info - ~loc:(Sexp.location sinfo) + ~loc:(sexp_location sinfo) "@[<v>No instance found for type:@, @[<hov 2>%a@]@]" L.pp_print_clean_lexp t; false) ===================================== src/lexer.ml ===================================== @@ -150,9 +150,9 @@ let lex_symbol in let location s = s - |> Sexp.location + |> sexp_location |> Source.Location.extend op_location - |> Source.Location.extend (Sexp.location left) + |> Source.Location.extend (sexp_location left) in let lf' = if prec' > prec ===================================== src/lexp.ml ===================================== @@ -426,13 +426,13 @@ let rec lexp_sinfo s = | Proj (l,_,_) -> l let location (e : lexp) : Source.Location.t = - Sexp.location (lexp_sinfo e) + sexp_location (lexp_sinfo e) (********* Normalizing a term *********) let vdummy = (dummy_sinfo, None) let sname (sinfo, n : vname) : symbol = - (Sexp.location sinfo, U.maybename n) + (sexp_location sinfo, U.maybename n) let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -636,6 +636,12 @@ and subst_eq s1 s2 = let o = o2 - o1 in eq e1 (mkSusp e2 (S.shift o)) && subst_eq s1 (S.mkShift s2 o) + | ((S.Identity n, S.Cons (e, s, o)) + | (S.Cons (e, s, o), S.Identity n)) + -> (* ↑n ≃ Var n · ↑(n+1), so unfold Identity when needed. *) + match lexp_lexp' e with + | Var (_, n') when n' == n + o + -> subst_eq (S.Identity (n + 1)) (S.mkShift s o) | _ -> false (* Print a clean version of an lexp. Should be preferred to `pp_print_lexp` ===================================== src/opslexp.ml ===================================== @@ -229,7 +229,7 @@ let rec lexp_whnf e (ctx : lexp_context) : lexp = -> let subst = S.cons (mk_eq_witness l e' ctx) (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:(Sexp.location l) + ~section:"WHNF" ~loc:(sexp_location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with @@ -255,17 +255,17 @@ let rec lexp_whnf e (ctx : lexp_context) : lexp = _ -> []) in let rec getfield label args fields = match args, fields with - | _ , [] -> Log.log_error ~loc:(Sexp.location loc) + | _ , [] -> Log.log_error ~loc:(sexp_location loc) "Tuple does not have the field `%s`" label; e | (_, arg)::_, (_, (_, Some fn), _)::_ when fn = label -> (* Reduce to the argument corresponding to the field *) lexp_whnf arg ctx | _::args, _::fields -> getfield label args fields | [], _ -> (* This case should be impossible through typing *) - Log.log_fatal ~loc:(Sexp.location loc) + Log.log_fatal ~loc:(sexp_location loc) "Projected tuple has fewer arguments than fields" in getfield label (drop (List.length targs) args) fields - | _ -> Log.log_error ~loc:(Sexp.location loc) "Proj on a non-tuple in WHNF!"; e) + | _ -> Log.log_error ~loc:(sexp_location loc) "Proj on a non-tuple in WHNF!"; e) | _ -> e) (* Not a proj of a cons: don't reduce. *) | Metavar (idx, s, _) @@ -710,7 +710,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (U.maybename name) ; lookup_type ctx v @@ -743,7 +743,7 @@ and check'' erased ctx e = match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc:(Sexp.location loc) "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType -> log_tc_error ~loc:(Lexp.location t1) "Not a proper type"; @@ -850,20 +850,20 @@ and check'' erased ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(Sexp.location l) + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(Sexp.location l) "Tuple has no field named: %s" label; + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(Sexp.location l) "Can't Proj an erasable field: %s" + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -875,10 +875,10 @@ and check'' erased ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(Sexp.location l) + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:(Sexp.location l) "Proj on a non-inductive type!" ; etype) + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) @@ -905,7 +905,7 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:(Sexp.location l) "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = @@ -936,10 +936,10 @@ and check'' erased ctx e = (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _ - -> log_tc_error ~loc:(Sexp.location l) "Wrong number of args to constructor!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (l, mkCons (it, (Sexp.location l, name)), + mkCall (l, mkCons (it, (sexp_location l, name)), List.map (fun (_, a) -> (Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in @@ -953,7 +953,7 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 - then log_tc_warning ~loc:(Sexp.location l) "Redundant default clause"; + then log_tc_warning ~loc:(sexp_location l) "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -966,8 +966,8 @@ and check'' erased ctx e = -> if diff > 0 then log_tc_error - ~loc:(Sexp.location l) "Non-exhaustive match: %d cases missing" diff) - | _,_ -> log_tc_error ~loc:(Sexp.location l) "Case on a non-inductive type!"); + ~loc:(sexp_location l) "Non-exhaustive match: %d cases missing" diff) + | _,_ -> log_tc_error ~loc:(sexp_location l) "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -996,7 +996,7 @@ and check'' erased ctx e = buildtype fargs with | Not_found - -> log_tc_error ~loc:(Sexp.location l) {|Constructor "%s" does not exist|} name; + -> log_tc_error ~loc:(sexp_location l) {|Constructor "%s" does not exist|} name; type_dummy) | _ -> log_tc_error ~loc:(Lexp.location e) @@ -1166,21 +1166,21 @@ and get_type ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(Sexp.location l) + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(Sexp.location l) "Tuple has no field named: %s" + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(Sexp.location l) + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -1192,10 +1192,10 @@ and get_type ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(Sexp.location l) + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:(Sexp.location l) "Proj on a non-inductive type!" ; + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) @@ -1371,12 +1371,12 @@ let pos_of_label lctx label e : int = let rec erase_type (lctx : lexp_context) (lxp: lexp) : elexp = match lexp_lexp' lxp with - | Imm (l, s) -> Eimm (Sexp.location l, s) + | Imm (l, s) -> Eimm (sexp_location l, s) | Builtin (v, _) -> Ebuiltin (v) | Var (v) -> Evar (v) | Proj (l, exp, label) -> let t = get_type lctx exp in - Eproj (Sexp.location l, erase_type lctx exp, pos_of_label lctx label t) + Eproj (sexp_location l, erase_type lctx exp, pos_of_label lctx label t) | Cons (ty, s) -> Econs (arity_of_cons lctx ty s, s) | Lambda (Aerasable, _, _, body) @@ -1388,7 +1388,7 @@ let rec erase_type (lctx : lexp_context) (lxp: lexp) : elexp = | Let (l, decls, body) -> let lctx', edecls = clean_decls lctx decls in - Elet (Sexp.location l, edecls, erase_type lctx' body) + Elet (sexp_location l, edecls, erase_type lctx' body) | Call (_, fct, args) -> Ecall (erase_type lctx fct, List.filter_map (clean_arg lctx) args) @@ -1396,7 +1396,7 @@ let rec erase_type (lctx : lexp_context) (lxp: lexp) : elexp = | Case (location, target, _, branches, default) -> let etarget = erase_type lctx target in let ebranches = clean_branch_map lctx branches in - Ecase (Sexp.location location, etarget, ebranches, clean_default lctx default) + Ecase (sexp_location location, etarget, ebranches, clean_default lctx default) | Susp (l, s) -> erase_type lctx (L.push_susp l s) @@ -1445,7 +1445,7 @@ and clean_branch_map lctx cases = in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (Sexp.location l, eargs, erase_type lctx' (L.push_susp expr subst)) + (sexp_location l, eargs, erase_type lctx' (L.push_susp expr subst)) in SMap.map clean_branch cases @@ -1461,7 +1461,7 @@ let erase_type lctx lxp = IMap.iter (fun i (_, t, _, (l, n)) -> Format.printf "%s ?%s[%i] : @[<hov 2>%a@]@," - (Source.Location.to_string (Sexp.location l)) + (Source.Location.to_string (sexp_location l)) (Option.value ~default:"" n) i pp_print_clean_lexp t) @@ -1497,8 +1497,8 @@ let ctx2tup ctx nctx = match blocs with | [] -> let cons_name = "cons" in - let cons_label = (Sexp.location loc, cons_name) in - let type_label = (Sexp.location loc, "record") in + let cons_label = (sexp_location loc, cons_name) in + let type_label = (sexp_location loc, "record") in let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) ===================================== src/pexp.ml ===================================== @@ -36,7 +36,7 @@ type ppat = | Ppatcons of Source.Location.t * sexp * (symbol option * vname) list let pexp_pat_location : ppat -> Source.Location.t = function - | Ppatsym (l, _) -> Sexp.location l + | Ppatsym (l, _) -> sexp_location l | Ppatcons (l, _, _) -> l let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = @@ -49,7 +49,7 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | Anormal -> ":") in let ty = match t with Some e -> e | None -> Symbol (l, "_") in - let location = Source.Location.extend l (Sexp.location ty) in + let location = Source.Location.extend l (sexp_location ty) in Node (location, head, [Symbol s; ty]) let pexp_p_pat_arg (s : sexp) = match s with @@ -57,12 +57,12 @@ let pexp_p_pat_arg (s : sexp) = match s with | Node (_, Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) -> (Some f, (s, Some n)) | _ - -> let loc = Sexp.location s in + -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; (None, (s, None)) let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (Sexp.location l, match oname with None -> "_" | Some n -> n) in + let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l, _) as n) -> Node (l, Symbol (l, "_:=_"), [Symbol n; pname]) @@ -71,10 +71,10 @@ let pexp_p_pat (s : sexp) : ppat = match s with | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) | Node (l, c, args) -> Ppatcons (l, c, List.map pexp_p_pat_arg args) | _ - -> let l = Sexp.location s in + -> let l = sexp_location s in pexp_error l "Unknown pattern"; Ppatsym (s, None) let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (Sexp.location l, "_") - | Ppatsym (l, Some n) -> Symbol (Sexp.location l, n) + | Ppatsym (l, None) -> Symbol (sexp_location l, "_") + | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) | Ppatcons (l, c, args) -> Node (l, c, List.map pexp_u_pat_arg args) ===================================== src/sexp.ml ===================================== @@ -52,22 +52,14 @@ module Sym = struct && name l = name r end -let location : sexp -> location = function - | Block (l, _) -> l - | Symbol (l, _) -> l - | String (l, _) -> l - | Integer (l, _) -> l - | Float (l, _) -> l - | Node (l, _, _) -> l - let symbol ~(location : Source.Location.t) (name : string) : sexp = Symbol (Sym.intern ~location name) let node (head : sexp) (tail : sexp list) : sexp = let location = List.fold_left - (fun l e -> Source.Location.extend l (location e)) - (location head) + (fun l e -> Source.Location.extend l (sexp_location e)) + (sexp_location head) tail in Node (location, head, tail) ===================================== src/unification.ml ===================================== @@ -626,7 +626,12 @@ and unify_sortlvl (matching : scope_level option) when OL.conv_p ctx l1 l2 (* Arbitrarily selected `l1` over `l2` *) -> unify' l1 (mkSortLevel other) ctx vs matching - | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) + | SLlub (l1, l2), SLz | SLz, SLlub (l1, l2) + (* In this case, both `l1` and `l2` must be `SLz` *) + -> (unify' l1 (mkSortLevel SLz) ctx vs matching) + @(unify' l2 (mkSortLevel SLz) ctx vs matching) + | _, _ -> (add_residue ctx sortlvl lxp; + [(CKresidual, ctx, sortlvl, lxp)])) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)] (** Unify a Sort and a lexp ===================================== typer.ml ===================================== @@ -73,7 +73,7 @@ let repl_main argv = parse_args argv usage; print_string (Fmt.make_title " TYPER REPL "); - print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; + print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2024"; print_newline (); print_endline " %quit (%q) : leave REPL"; print_endline " %help (%h) : print help"; @@ -85,6 +85,7 @@ let repl_main argv = let load_file (ectx, i) file_name = printf " In[% 2d] >> %%readfile %s\n" i file_name; + flush stdout; Elab.process_file backend ectx file_name, i + 1 in let ectx, i = List.fold_left load_file (ectx, 0) (list_input_files ()) in ===================================== typer.sh ===================================== @@ -9,6 +9,6 @@ # complete-filenames is useful for "%readfile ..." command # history-no-dupes just make it faster to search history with up and down key -rlwrap --complete-filenames --history-no-dupes 1 ./_build/typer $* +rlwrap --complete-filenames --history-no-dupes 1 ./_build/default/typer.bc $* # if not specified history must be kept in "~/.typer_history" View it on GitLab: https://gitlab.com/monnier/typer/-/compare/10d4fafcb572a8cbe9ec22ecad2436de… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/10d4fafcb572a8cbe9ec22ecad2436de… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Don't transform builtins' types into closed form.
by Stefan (＠monnier) 12 Nov '24

12 Nov '24

Stefan pushed to branch main at Stefan / Typer Commits: 10d4fafc by Maxim Bernard at 2024-10-29T18:10:32-04:00 Don't transform builtins' types into closed form. * src/opslexp.ml: Add DB offset to `lmap`, and use it in `get_builtin` to shift all DB indices accordingly. Add context parameter to `get_builtin` (used to compute shift). Make necessary adaptations in `check` and `fv` now that builtin types aren't in closed form. * src/lexp.ml: Make necessary adaptations in `mkSusp`, `push_susp` and `clean`. * src/inverse_subst.ml: Make necessary adaptations in `apply_inv_subst`. * src/builtin.ml: Remove `kind` parameter from `new_builtin_type` since it shouldn't be anything else than `type0` (especially with the hardcoded DB offset). Provide new argument to `add_builtin_cst`. * src/elab.ml: Remove obsolete argument from `new_builtin_type` calls. Provide new argument to `add_builtin_cst`. Make necessary adaptations in `meta_to_var`, `sform_identifier`, `sform_built_in` and `default_ectx`. In `sform_built_in`, remove transformation to closed form. - - - - - 5 changed files: - src/builtin.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml Changes: ===================================== src/builtin.ml ===================================== @@ -131,21 +131,28 @@ let v2o_list v = in v2o_list [] v -let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind) in - OL.add_builtin_cst name t; +let new_builtin_type name = + let t = mkBuiltin ((dloc, name), DB.type0) in + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `DB.type0` doesn't + * reference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 t; t let register_builtin_csts () = - OL.add_builtin_cst "TypeLevel" DB.type_level; - OL.add_builtin_cst "TypeLevel_z" DB.level0; - OL.add_builtin_cst "Type" DB.type0; - OL.add_builtin_cst "Type0" DB.type0; - OL.add_builtin_cst "Type1" DB.type1; - OL.add_builtin_cst "Integer" DB.type_integer; - OL.add_builtin_cst "Float" DB.type_float; - OL.add_builtin_cst "String" DB.type_string; - OL.add_builtin_cst "Eq" DB.type_eq; - OL.add_builtin_cst "I" DB.type_interval + (* Although the current context may not be empty when adding these builtins, + * we still provide 0 as the types' DB offset, since none of these types + * reference any var/metavar, so the offset doesn't matter in these cases. *) + OL.add_builtin_cst "TypeLevel" 0 DB.type_level; + OL.add_builtin_cst "TypeLevel_z" 0 DB.level0; + OL.add_builtin_cst "Type" 0 DB.type0; + OL.add_builtin_cst "Type0" 0 DB.type0; + OL.add_builtin_cst "Type1" 0 DB.type1; + OL.add_builtin_cst "Integer" 0 DB.type_integer; + OL.add_builtin_cst "Int" 0 DB.type_int; + OL.add_builtin_cst "Float" 0 DB.type_float; + OL.add_builtin_cst "String" 0 DB.type_string; + OL.add_builtin_cst "Eq" 0 DB.type_eq; + OL.add_builtin_cst "I" 0 DB.type_interval let _ = register_builtin_csts () ===================================== src/elab.ml ===================================== @@ -118,15 +118,21 @@ type special_decl_forms_map = let special_forms : special_forms_map ref = ref SMap.empty let special_decl_forms : special_decl_forms_map ref = ref SMap.empty -let type_special_form = BI.new_builtin_type "Special-Form" type0 -let type_special_decl_form = BI.new_builtin_type "Special-Decl-Form" type0 +let type_special_form = BI.new_builtin_type "Special-Form" +let type_special_decl_form = BI.new_builtin_type "Special-Decl-Form" let add_special_form (name, func) = - OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `type_special_form` + * doesn'treference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms) let add_special_decl_form (name, func) = - OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_decl_form)); + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `type_special_decl_form` + * doesn'treference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 (mkBuiltin ((dloc, name), type_special_decl_form)); special_decl_forms := SMap.add name func (!special_decl_forms) let get_special_form name = @@ -494,7 +500,7 @@ let meta_to_var ids (e : lexp) = | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, loop o t) | Var (n,i) -> if i < o then e else mkVar (n, i + count) | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) @@ -642,7 +648,7 @@ and sform_identifier ctx loc sargs ot = when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then let name = string_sub name 2 (String.length name) in - try let e = OL.get_builtin name in + try let e = OL.get_builtin (ectx_to_lctx ctx) name in (e, Inferred (OL.get_type (ectx_to_lctx ctx) e)) with | Not_found @@ -1639,16 +1645,16 @@ let sform_built_in ctx loc sargs ot = | true, [String (_, name)] -> (match ot with | Some ltp - (* FIXME: This `L.clean` is basically the last remaining use of the - * function. It's not indispensible, tho it might still be useful for + (* FIXME: This `L.clean` is one of the last remaining uses of the + * function. It's not indispensible, tho it might still be useful for * performance of type-inference (at least until we have proper - * memoization of push_susp and/or whnf). *) - -> let ltp' = Lexp.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in + * memoization of push_susp and/or whnf). *) + -> let ltp' = Lexp.clean ltp in let bi = mkBuiltin ((Sexp.location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions) || List.mem name DB.builtin_axioms) then sexp_error (Sexp.location loc) {|Unknown built-in "%s"|} name; - OL.add_builtin_cst name bi; + OL.add_builtin_cst name (DB.get_size ctx) bi; (bi, Checked) | None -> error ~loc:(Sexp.location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) @@ -2065,7 +2071,7 @@ let default_ectx (* Empty context *) let ectx = empty_elab_context in - let ectx = SMap.fold (fun key e ctx + let ectx = SMap.fold (fun key (_o, e) ctx -> if String.get key 0 = '-' then ctx else ctx_define ctx (dsinfo, Some key) e (OL.get_type (ectx_to_lctx ectx) e)) ===================================== src/inverse_subst.ml ===================================== @@ -271,7 +271,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = -> 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 - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, apply_inv_subst t s) | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s ===================================== src/lexp.ml ===================================== @@ -345,7 +345,7 @@ let rec mkSusp e s = * it just seemed like a good idea to do it eagerly when it's easy. *) match lexp_lexp' e with | Imm _ -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, mkSusp t s) | Susp (e, s') -> mkSusp_memo e (scompose s' s) | Var (l,v) -> slookup s l v | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) @@ -443,8 +443,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> mkSortLevel (mkSLlub' (push_susp e1 s, push_susp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (_, _) -> e - | Builtin _ -> e - + | Builtin (sym, t) -> mkBuiltin (sym, mkSusp t s) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let rec loop s defs = match defs with @@ -512,7 +511,7 @@ let clean e = -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (_, _) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, clean s t) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) ===================================== src/opslexp.ml ===================================== @@ -131,28 +131,21 @@ let rec lctx_to_subst lctx = (List.rev defs) in L.scompose s2 s1 -(* Map of lexp builtin elements accessible via (## <name>). *) -let lmap = ref (SMap.empty : lexp SMap.t) - -let add_builtin_cst (name : string) (e : lexp) +(* Map of lexp builtin elements accessible via (## <name>). + * Values are pairs consisting of : + * - the type's De Bruijn offset (i.e. the context's size when the builtin + * was added) + * - the builtin's type *) +let lmap = ref (SMap.empty : (S.db_offset * lexp) SMap.t) + +let add_builtin_cst (name : string) (offset : S.db_offset) (e : lexp) = let map = !lmap in assert (not (SMap.mem name map)); - lmap := SMap.add name e map - -let get_builtin (name) = SMap.find name !lmap - -(* Take an expression `e` that is "closed" relatively to context lctx - * and return an equivalent expression valid in the empty context. - * By "closed" I mean that it only refers to elements of the context which - * are LetDef. *) -let lexp_close lctx e = - (* There are many different ways to skin this cat. - * This is definitely not the best one: - * - it inlines all the definitions everywhere they're used - * - It turns the lctx (of O(log N) access time) into a subst - * (of O(N) access time) - * Oh well! *) - mkSusp e (lctx_to_subst lctx) + lmap := SMap.add name (offset, e) map + +let get_builtin (ctx : lexp_context) (name) = + let (offset, btl) = SMap.find name !lmap in + mkSusp btl (S.shift ((M.length ctx) - offset)) let type_dummy = DB.type_integer @@ -568,7 +561,7 @@ and mk_eq_witness sinfo e ctx = | _ -> Log.internal_error "" in (* FIXME: Doesn't `e` need a "shift" here? *) let fn = mkLambda (Aerasable, (sinfo, None), etype, e) in - mkCall (sinfo, get_builtin "Eq.eq", + mkCall (sinfo, get_builtin ctx "Eq.eq", [Aerasable, elevel; Aerasable, etype; Anormal, fn]) @@ -711,7 +704,7 @@ and check'' erased ctx e = * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t) - -> let _ = check_type DB.set_empty Myers.nil t in + -> let _ = check_type erased ctx t in t (* FIXME: Check recursive references. *) | Var (((loc, name), idx) as v) @@ -1065,7 +1058,7 @@ and fv (e : lexp) : (db_set * mv_set) = | SortLevel (SLlub (e1, e2)) -> fv_union (fv e1) (fv e2) | Sort (_, Stype e) -> fv e | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty - | Builtin _ -> fv_empty + | Builtin (_, t) -> fv t | Var (_, i) -> (DB.set_singleton i, mv_set_empty) | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/10d4fafcb572a8cbe9ec22ecad2436dee… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/10d4fafcb572a8cbe9ec22ecad2436dee… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Fix `<-` macro not handling nested tuples properly.
by Stefan (＠monnier) 29 Oct '24

29 Oct '24

Stefan pushed to branch main at Stefan / Typer Commits: 3855c3d2 by Maxim Bernard at 2024-10-28T00:18:33-04:00 Fix `<-` macro not handling nested tuples properly. * btl/assign-datacons.typer: Convert `_,_` forms to the corresponding `tupleN` form for nested patterns as well as the top-level one. Add test that covers this case. * btl/tuple.typer: Add `get-name-from-list` function for use in assign-datacons.typer. - - - - - 2 changed files: - btl/assign-datacons.typer - btl/tuple.typer Changes: ===================================== btl/assign-datacons.typer ===================================== @@ -36,12 +36,12 @@ get-subpatterns pattern-sexp = (lambda _ -> nil) (lambda _ -> nil); -% If `pattern-sexp` is of the form `a,b,c,...`, converts in into the appropriate -% tuple (e.g. `tuple3 a b c`). -expand-tuple pattern-sexp = - if String_eq "_,_" (get-constructor-name pattern-sexp) - then tuple-lib.make-tuple-impl (get-subpatterns pattern-sexp) - else pattern-sexp; +% If the constructor is the "comma" tuple constructor (for tuples of the form +% `(a, b, c, ...)`, return the corresponding datacons name. +normalize-tuple-name cstr-name nb-params = + if String_eq "_,_" cstr-name + then tuple-lib.get-name-from-list (tuple-lib.tuple-cstr-names) nb-params + else cstr-name; % E.g. with argument `(a (b x y) z)`, returns `["x", "y", "z"]` get-newvars-names : List Sexp -> List String; @@ -83,7 +83,8 @@ make-single-case subject cstr-name nb-params var-idx var-sym ret-val = in if Int_< i nb-params then cons current-sym (mk-pat-params (Int_+ 1 i)) else nil; - pattern = (Sexp_node (Sexp_symbol cstr-name) (mk-pat-params 0)); + pattern = (Sexp_node (Sexp_symbol (normalize-tuple-name cstr-name nb-params)) + (mk-pat-params 0)); branch-node = (Sexp_node (Sexp_symbol "_=>_") (cons pattern (cons ret-val nil))) in Sexp_node (Sexp_symbol "##case_") @@ -134,7 +135,7 @@ make-case-for-var var-name cstr-name subpatterns subject temp-matching-var = (lambda _ -> Sexp_error)) | none => % Logically should not occur - Sexp_symbol "error none"; + Sexp_symbol "Internal error in assing-datacons"; assign-datacons = macro (lambda args -> @@ -142,10 +143,8 @@ assign-datacons = macro pattern-sexp = List_nth 0 args Sexp_error; % e.g. `(a (b x y) z)` value-sexp = List_nth 1 args Sexp_error; % e.g. `someFunction 1 2 3` - pattern-sexp-norm = expand-tuple pattern-sexp; - - cstr-name = get-constructor-name pattern-sexp-norm; - subpatterns = get-subpatterns pattern-sexp-norm; + cstr-name = get-constructor-name pattern-sexp; + subpatterns = get-subpatterns pattern-sexp; new-bound-variables = get-newvars-names subpatterns; % `["x", "y", "z"]` @@ -200,6 +199,16 @@ test1 = cons (quote (a (b x y) z)) test2 = cons (quote (a, (b x _ z), c)) (cons (quote sometuple) nil); +% `(a (b (x, y, z) w) z) <- somevalue` +test3 = cons (quote (a (b (x, y, z) w) v)) + (cons (quote sometuple) nil); + +t = cons (quote (exists (hp, hqr) (pf-p-hp, + pf-qr-hqr, + pf-hp-hqr-disjoint, + pf-heap-eq-hp-hqr))) + (cons (quote pf-hyp) nil); + runtest test = IO_run (do { ===================================== btl/tuple.typer ===================================== @@ -65,13 +65,20 @@ tuple-type-names = (cons "Tuple9" (cons "Tuple10" nil)))))))); +excess-items-message = "<ERROR: limit 10 items per tuple>"; + +get-name-from-list name-list nb-args = + List_nth (Int_- nb-args 2) + name-list + excess-items-message; + make-sexp-from-names : List String -> List Sexp -> Sexp; make-sexp-from-names name-list args = let nb-args = List_length args; - tuple-name = List_nth (Int_- nb-args 2) name-list "" + tuple-name = get-name-from-list name-list nb-args in if Int_<= nb-args 10 then Sexp_node (Sexp_symbol tuple-name) args - else Sexp_symbol "<ERROR: limit 10 items per tuple>"; + else Sexp_symbol excess-items-message; make-tuple-impl = make-sexp-from-names tuple-cstr-names; tuple-type-impl = make-sexp-from-names tuple-type-names; View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3855c3d23d0dbd161076651301251e198… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3855c3d23d0dbd161076651301251e198… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Change tuple implementation and behavior of the `_<-_` operator.
by Stefan (＠monnier) 26 Aug '24

26 Aug '24

Stefan pushed to branch main at Stefan / Typer Commits: 9da75535 by Maxim Bernard at 2024-08-09T16:20:11-04:00 Change tuple implementation and behavior of the `_<-_` operator. This operator is now used to unpack any `datacons`, possibly with nested patterns. It also supports the tuple notation. * btl/assign-datacons.typer: Implementation of the `assign-datacons` macro, which generates a series of assignments, each corresponding to a specific value in the provided datacons. * btl/pervasive.typer: Set `_<-_` to newly defined `assign-datacons` macro. Add `List_filter` function (required by `assign-datacons` module). Remove definitions: `tuple-nth` macro, pair and triplet (which have been moved to the tuple module) and `BoolMod`. Move do-lib definitions and certain List functions further in the file, since they require definitions in tuple-lib. * btl/tuple.typer: Redesign and simplify how Typer implements tuples. Tuples are now one of the nine predefined ADTs, containing up to 10 items. The comma operator (defined in `pervasive.typer`) now simply calls the approprate constructor based on the number of arguments. * btl/case.typer: * btl/qcase.typer: Make necessary adaptations required by changes in tuple implementation. - - - - - 5 changed files: - + btl/assign-datacons.typer - btl/case.typer - btl/pervasive.typer - btl/qcase.typer - btl/tuple.typer Changes: ===================================== btl/assign-datacons.typer ===================================== @@ -0,0 +1,210 @@ +get-symbol-name sexp = + let error-msg = "<ERROR: not a symbol>" + in Sexp_dispatch sexp + (lambda _ _ -> error-msg) % node + (lambda name -> name) % symbol + (lambda _ -> error-msg) % string + (lambda _ -> error-msg) % int + (lambda _ -> error-msg) % float + (lambda _ -> error-msg); % block + +get-constructor-name pattern-sexp = + let error-msg = "<ERROR: invalid constructor name>" + in Sexp_dispatch pattern-sexp + % Must be a node... + (lambda head _ -> + Sexp_dispatch head + (lambda _ _ -> error-msg) + % ...whose head is a symbol. + (lambda name -> name) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg)) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg); + +get-subpatterns pattern-sexp = + Sexp_dispatch pattern-sexp + (lambda _ args -> args) + (lambda sym-name -> (cons (Sexp_symbol sym-name) nil)) + (lambda _ -> nil) + (lambda _ -> nil) + (lambda _ -> nil) + (lambda _ -> nil); + +% If `pattern-sexp` is of the form `a,b,c,...`, converts in into the appropriate +% tuple (e.g. `tuple3 a b c`). +expand-tuple pattern-sexp = + if String_eq "_,_" (get-constructor-name pattern-sexp) + then tuple-lib.make-tuple-impl (get-subpatterns pattern-sexp) + else pattern-sexp; + +% E.g. with argument `(a (b x y) z)`, returns `["x", "y", "z"]` +get-newvars-names : List Sexp -> List String; +get-newvars-names subpatterns = + List_foldl + (lambda acc pat -> + Sexp_dispatch pat + % node + (lambda _head tail -> + List_concat acc (get-newvars-names tail)) + % symbol + (lambda name -> List_concat acc (cons name nil)) + % all other cases should not occur + (lambda _ -> acc) + (lambda _ -> acc) + (lambda _ -> acc) + (lambda _ -> acc)) + nil + subpatterns; + +pattern-has-var pat var-name = + case List_find + (lambda candidate -> String_eq var-name candidate) + (get-newvars-names (get-subpatterns pat)) + | some _ => true + | none => false; + +% Generates a `case` matching over `subject`, which is supposed to have a single +% constructor `cstr-name` with `nb-params` operands, but only accesses the +% `var-idx`-th operand, under the bound variable `var-sym`. The branch returns +% `ret-val`. +make-single-case : Sexp -> String -> Int -> Int -> Sexp -> Sexp -> Sexp; +make-single-case subject cstr-name nb-params var-idx var-sym ret-val = + let mk-pat-params : Int -> List Sexp; + mk-pat-params i = + let current-sym = if Int_eq i var-idx + then var-sym + else (Sexp_symbol "_") + in if Int_< i nb-params + then cons current-sym (mk-pat-params (Int_+ 1 i)) + else nil; + pattern = (Sexp_node (Sexp_symbol cstr-name) (mk-pat-params 0)); + branch-node = (Sexp_node (Sexp_symbol "_=>_") + (cons pattern (cons ret-val nil))) + in Sexp_node (Sexp_symbol "##case_") + (cons (Sexp_node (Sexp_symbol "_|_") + (cons subject (cons branch-node nil))) + nil); + +% Generates the `case` cascade that accesses and returns the `var-name` value +% in `subpatterns`, matching over `subject`. +make-case-for-var : String -> String -> List Sexp -> Sexp -> Sexp -> Sexp; +make-case-for-var var-name cstr-name subpatterns subject temp-matching-var = + let nb-params = List_length subpatterns; + in case List_find (lambda pat-idx-pair -> + case pat-idx-pair + | pair pat _ => pattern-has-var pat var-name) + (List_mapi pair subpatterns) + | some found-subpattern => + % There is a corresponding subpattern with a variable named `var-name`. + (case found-subpattern + | pair pat idx => + Sexp_dispatch + pat + % node case : has subpatterns + (lambda sub-cstr-name sub-subpatterns -> + let body = make-case-for-var var-name + (get-symbol-name sub-cstr-name) + sub-subpatterns + temp-matching-var + temp-matching-var + in make-single-case subject + cstr-name + nb-params + idx + temp-matching-var + body) + % symbol case : is the variable we're looking for + (lambda _ -> + make-single-case subject + cstr-name + nb-params + idx + temp-matching-var + temp-matching-var) + % other cases : error (cannot occur) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error)) + | none => + % Logically should not occur + Sexp_symbol "error none"; + +assign-datacons = macro + (lambda args -> + let + pattern-sexp = List_nth 0 args Sexp_error; % e.g. `(a (b x y) z)` + value-sexp = List_nth 1 args Sexp_error; % e.g. `someFunction 1 2 3` + + pattern-sexp-norm = expand-tuple pattern-sexp; + + cstr-name = get-constructor-name pattern-sexp-norm; + subpatterns = get-subpatterns pattern-sexp-norm; + + new-bound-variables = get-newvars-names subpatterns; % `["x", "y", "z"]` + + make-bound-var-asgn-list datacons-var temp-matching-var = + List_map + (lambda var-name -> + make-decl + (Sexp_symbol var-name) + (make-case-for-var var-name + cstr-name + subpatterns + datacons-var + temp-matching-var)) + % Only consider variables not named `_` + (List_filter + (lambda var-name -> not (String_eq var-name "_")) + new-bound-variables); + + % Final list of assignments, which contains : + % - an unnamed variable with the value being filtered over + % - every bound variable from the pattern (`x`, `y` and `z` from the above + % example), whose value is a cascade of `case`s returning the appropriate + % element from `tuple-varname` + % e.g. + % gensym0 = someFunction 1 2 3; + % x = case gensym0 + % | a gensym1 _ => + % case gensym1 + % | b gensym1 _ => gensym1; + % y = case gensym0 + % | a gensym1 _ => + % case gensym1 + % | b _ gensym1 => gensym1; + % z = case gensym0 + % | a _ gensym1 => + % gensym1; + make-defs-list = lambda datacons-var temp-matching-var -> + cons (make-decl datacons-var value-sexp) + (make-bound-var-asgn-list datacons-var temp-matching-var) + in do { + datacons-var <- gensym (); + temp-matching-var <- gensym (); + IO_return (Sexp_node (Sexp_symbol "_;_") + (make-defs-list datacons-var temp-matching-var)); + }); + +% `(a (b x y) z) <- somevalue` +test1 = cons (quote (a (b x y) z)) + (cons (quote somevalue) nil); + +% `a, (b x _ z), c <- sometuple` +test2 = cons (quote (a, (b x _ z), c)) + (cons (quote sometuple) nil); + +runtest test = + IO_run + (do { + res <- Macro_expand assign-datacons test; + Sexp_debug_print res; + IO_return unit + }) + (); ===================================== btl/case.typer ===================================== @@ -610,7 +610,7 @@ in do { %% Take note that "renamed pattern" correspond to all pattern in list "B" %% and list "C" is the childs of list "B" in the same order. %% -part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); +part-type = Pair (Tuple Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); %% %% Takes a list of branches (pair of (patterns, body)) @@ -716,7 +716,7 @@ partition-branches branches = let rvars <- gen-vars ivars; rpat <- renamed-pat pat rvars; vars <- List_foldl (ff rvars) (IO_return nil) pp; - IO_return (pair (triplet rpat rvars (List_merge pp vars)) tt); + IO_return (pair (rpat, rvars, (List_merge pp vars)) tt); }; in io-list (List_map mf pre-parts); @@ -730,7 +730,7 @@ in do { %% reminder %% %% part-type = Pair -%% (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) +%% (Tuple Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) %% (List (Pair Pats Code)); %% @@ -763,8 +763,9 @@ merge-dflt parts odflt = let preppend : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; preppend pat vars branches part = case part - | pair p b => (case p | triplet _ lv v => - pair (triplet pat lv (List_concat vars v)) (List_concat branches b)); + | pair p b => + let (_, lv, v) <- p + in pair (pat, lv, (List_concat vars v)) (List_concat branches b); %% %% Append child branches if we see more than one default branches @@ -780,21 +781,22 @@ merge-dflt parts odflt = let append : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; append pat vars branches part = case part - | pair p b => (case p | triplet _ lv v => - pair (triplet pat lv (List_concat v vars)) (List_concat b branches)); + | pair p b => + let (_, lv, v) <- p + in pair (pat, lv, (List_concat v vars)) (List_concat b branches); in case parts | cons part parts => (case part | pair p pp => - (case p | triplet pat _ vars => - if (dflt? pat) then - (case odflt - | some dflt => merge-dflt parts (some (append pat vars pp dflt)) - | none => merge-dflt parts (some part)) - else - (case odflt - %% merge previous default to all branches - | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt) - | none => cons part (merge-dflt parts odflt)))) + let (pat, _, vars) <- p + in if (dflt? pat) then + (case odflt + | some dflt => merge-dflt parts (some (append pat vars pp dflt)) + | none => merge-dflt parts (some part)) + else + (case odflt + %% merge previous default to all branches + | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt) + | none => cons part (merge-dflt parts odflt))) | nil => (case odflt | some dflt => (cons dflt nil) | none => nil); @@ -840,7 +842,7 @@ in List_map (preppend-dflt max-len) branches; %% reminder %% %% part-type = Pair -%% (Triplet +%% (Tuple %% Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) %% (List (Pair Pats Code)); %% @@ -952,11 +954,12 @@ compile-case subjects branches = let %% translate-part : part-type -> IO Code; translate-part branch = case branch - | pair patterns branches => (case patterns - | triplet pat rvars pats-vars => do { - sub-cases <- translate-sub-pats rvars pats-vars branches; - IO_return (quote (_=>_ (uquote pat) (uquote sub-cases))); - }); + | pair patterns branches => + let (pat, rvars, pats-vars) <- patterns + in do { + sub-cases <- translate-sub-pats rvars pats-vars branches; + IO_return (quote (_=>_ (uquote pat) (uquote sub-cases))); + }; %% %% Generate code from all partition ===================================== btl/pervasive.typer ===================================== @@ -185,6 +185,16 @@ List_fold2 f o xs ys = case xs List_empty : List ?a -> Bool; List_empty xs = Int_eq (List_length xs) (Integer->Int 0); +% Only keeps items whose `f` predicate returns true +List_filter : (?a -> Bool) -> List ?a -> List ?a; +List_filter f l = + case l + | nil => nil + | cons x xs => + (case (f x) + | true => cons x (List_filter f xs) + | false => List_filter f xs); + %%% Good 'ol combinators id x = x; @@ -410,55 +420,6 @@ type Sexp_wrapper Sexp_wrap s = Sexp_dispatch s node symbol string integer float block; -%%%% Tuples - -%% Sample tuple: a module holding Bool and its constructors. -BoolMod = (##datacons - %% We need the `?` metavars to be lexically outside of the - %% `typecons` expression, otherwise they end up generalized, so - %% we end up with a type constructor like - %% - %% typecons _ (cons (τ₁ : Type) (t : τ₁) - %% (τ₂ : Type) (true : τ₂) - %% (τ₃ : Type) (false : τ₃)) - %% - %% And it's actually even worse because it tries to generalize - %% over the level of those `Type`s, so we end up with an invalid - %% inductive type. - ((lambda t1 t2 t3 - -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) - ? ? ?) - cons) - (_ := Bool) (_ := true) (_ := false); - -Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); -pair = datacons Pair pair; - -%% Triplet (tuple with 3 values) -type Triplet (a : Type) (b : Type) (c : Type) - | triplet (x : a) (y : b) (z : c); - -%%%% List with tuple - -%% Merge two List to a List of Pair -%% Both List must be of same length -List_merge : List ?a -> List ?b -> List (Pair ?a ?b); -List_merge xs ys = case xs - | cons x xs => ( case ys - | cons y ys => cons (pair x y) (List_merge xs ys) - | nil => nil ) % error - | nil => nil; - -%% `Unmerge` a List of Pair -%% The two functions name said it all -List_map-fst xs = let - mf p = case p | pair x _ => x; -in List_map mf xs; - -List_map-snd xs = let - mf p = case p | pair _ y => y; -in List_map mf xs; - %%%% Logic %% `False` should be one of the many empty types. @@ -600,52 +561,83 @@ typeclass Monad; define-operator "<-" 80 96; %% -%% `List` is the type and `list` is the module +%% Module containing tuple definitions, including the macro used for expanding +%% the comma (`_,_`) operator. +%% Used by `case_` and by `_<-_` %% -list = load "btl/list.typer"; +tuple-lib = load "btl/tuple.typer"; + +Pair = tuple-lib.Pair; +Tuple3 = tuple-lib.Tuple3; +Tuple4 = tuple-lib.Tuple4; +Tuple5 = tuple-lib.Tuple5; +Tuple6 = tuple-lib.Tuple6; +Tuple7 = tuple-lib.Tuple7; +Tuple8 = tuple-lib.Tuple8; +Tuple9 = tuple-lib.Tuple9; +Tuple10 = tuple-lib.Tuple10; + +pair = tuple-lib.pair; +tuple3 = tuple-lib.tuple3; +tuple4 = tuple-lib.tuple4; +tuple5 = tuple-lib.tuple5; +tuple6 = tuple-lib.tuple6; +tuple7 = tuple-lib.tuple7; +tuple8 = tuple-lib.tuple8; +tuple9 = tuple-lib.tuple9; +tuple10 = tuple-lib.tuple10; %% -%% Macro `do` for easier series of IO operation +%% Instantiate a tuple from expressions %% %% e.g.: -%% do { IO_return true; }; +%% tup = (x,y,z); %% -do-lib = load "btl/do.typer"; -do-impl = do-lib.do-impl; -do = do-lib.do; -do* = do-lib.do*; +_\,_ = tuple-lib.make-tuple; -%% -%% Module containing various macros for tuple -%% Used by `case_` -%% -tuple-lib = load "btl/tuple.typer"; +Tuple = tuple-lib.tuple-type; %% -%% Get the nth element of a tuple +%% Functions over lists of tuples %% -%% e.g.: -%% tuple-nth tup 0; -%% -tuple-nth = tuple-lib.tuple-nth; + +%% Merge two List to a List of Pair +%% Both List must be of same length +List_merge : List ?a -> List ?b -> List (Pair ?a ?b); +List_merge xs ys = case xs + | cons x xs => ( case ys + | cons y ys => cons (pair x y) (List_merge xs ys) + | nil => nil ) % error + | nil => nil; + +%% `Unmerge` a List of Pair +%% The two functions name said it all +List_map-fst xs = let + mf p = case p | pair x _ => x; +in List_map mf xs; + +List_map-snd xs = let + mf p = case p | pair _ y => y; + in List_map mf xs; %% -%% Affectation of tuple -%% -%% e.g.: -%% (x,y,z) <- tup; +%% `List` is the type and `list` is the module %% -_<-_ = tuple-lib.assign-tuple; +list = load "btl/list.typer"; + %% -%% Instantiate a tuple from expressions +%% Macro `do` for easier series of IO operation %% %% e.g.: -%% tup = (x,y,z); +%% do { IO_return true; }; %% -_\,_ = tuple-lib.make-tuple; +do-lib = load "btl/do.typer"; +do-impl = do-lib.do-impl; +do = do-lib.do; +do* = do-lib.do*; -Tuple = tuple-lib.tuple-type; +_<-_ = let lib = load "btl/assign-datacons.typer" in lib.assign-datacons; %% %% Macro `case` for a some more complex pattern matching ===================================== btl/qcase.typer ===================================== @@ -59,12 +59,12 @@ qcase_impl = lambda (sexps : List Sexp) -> %% Triple of the expression to eliminate, the underlying type A %% and the relation R %% A and R are optional - elim_expr_details : Triplet Sexp (Option Sexp) (Option Sexp); + elim_expr_details : Tuple Sexp (Option Sexp) (Option Sexp); elim_expr_details = let - kerr = K (triplet Sexp_error none none); + kerr = K (Sexp_error, none, none); extract_from_annotated_e : Sexp -> List Sexp -> - Triplet Sexp (Option Sexp) (Option Sexp); + Tuple Sexp (Option Sexp) (Option Sexp); extract_from_annotated_e _ xs = if (Int_eq (List_length xs) 2) then @@ -82,10 +82,10 @@ qcase_impl = lambda (sexps : List Sexp) -> a = List_nth 0 sexps Sexp_error; r = List_nth 1 sexps Sexp_error; in - triplet e (some a) (some r) + (e, (some a), (some r)) else - triplet e (some Sexp_error) (some Sexp_error); - kerr' = K (triplet e (some Sexp_error) (some Sexp_error)); + (e, (some Sexp_error), (some Sexp_error)); + kerr' = K (e, (some Sexp_error), (some Sexp_error)); in Sexp_dispatch e_type extract_type % Nodes @@ -95,9 +95,9 @@ qcase_impl = lambda (sexps : List Sexp) -> kerr' % Float kerr' % List of Sexp else - triplet Sexp_error none none; + (Sexp_error, none, none); extract_targ_from_node : Sexp -> List Sexp -> - Triplet Sexp (Option Sexp) (Option Sexp); + Tuple Sexp (Option Sexp) (Option Sexp); extract_targ_from_node x xs = %% Check if annotation is present if (is_sym x "_:_") @@ -107,12 +107,12 @@ qcase_impl = lambda (sexps : List Sexp) -> else %% No annotation was given, return the entire %% expresson as the elimination target - triplet x none none; + (x, none, none); in Sexp_dispatch elim_targ_sexp extract_targ_from_node % Nodes - (lambda _ -> triplet elim_targ_sexp - none none) % Symbol + (lambda _ -> (elim_targ_sexp, + none, none)) % Symbol kerr % String kerr % Integer kerr % Float @@ -262,18 +262,18 @@ qcase_impl = lambda (sexps : List Sexp) -> kerr % Float kerr; % List of Sexp qelim_args : List Sexp; - qelim_args = case elim_expr_details - | triplet e a r => - let - res = (cons elim_fn - (cons elim_compat - (cons e nil))); - res' = (case r - | none => res - | some r' => - (cons (build_explicit_arg "R" r') res)); - in - res'; + qelim_args = + let + (e, a, r) <- elim_expr_details; + res = (cons elim_fn + (cons elim_compat + (cons e nil))); + res' = (case r + | none => res + | some r' => + (cons (build_explicit_arg "R" r') res)); + in + res'; qelim_sexp = Sexp_node (Sexp_symbol "Quotient_elim") qelim_args; in ===================================== btl/tuple.typer ===================================== @@ -1,246 +1,81 @@ %%% tuple.typer --- Notation `_,_` for tuples -%% Here's an example similar to tuple from `load` -%% -%% Sample tuple: a module holding Bool and its constructors. -%% -%% We need the `?` metavars to be lexically outside of the -%% `typecons` expression, otherwise they end up generalized, so -%% we end up with a type constructor like -%% -%% typecons _ (cons (τ₁ : Type) (t : τ₁) -%% (τ₂ : Type) (true : τ₂) -%% (τ₃ : Type) (false : τ₃)) -%% -%% And it's actually even worse because it tries to generalize -%% over the level of those `Type`s, so we end up with an invalid -%% inductive type. -%% -%% BoolMod = (##datacons -%% ((lambda t1 t2 t3 -%% -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) -%% ? ? ?) -%% cons) -%% (_ := Bool) (_ := true) (_ := false); -%% - -%% List_nth = list.nth; -%% List_map = list.map; -%% List_mapi = list.mapi; -%% List_map2 = list.map2; -%% List_concat = list.concat; - -%% -%% Move IO outside List (from element to List) -%% (The function's type explain everything) -%% -io-list : List (IO ?a) -> IO (List ?a); -io-list l = let - ff : IO (List ?a) -> IO ?a -> IO (List ?a); - ff o v = do { - o <- o; - v <- v; - IO_return (cons v o); - }; -in do { - l <- (List_foldl ff (IO_return nil) l); - IO_return (List_reverse l nil); -}; - -%% -%% Generate a List of pseudo-unique symbol -%% -%% Takes a List of Sexp and generate a List of new name of the same length -%% whatever are the element of the List -%% -gen-vars : List Sexp -> IO (List Sexp); -gen-vars vars = io-list (List_map - (lambda _ -> gensym ()) - vars); - -%% -%% Reference for tuple's implicit field name -%% -%% Takes a list of vars (it could actually only takes a length) -%% Returns symbol `%n` with n in [0,length) (integer only, obviously) -%% -gen-tuple-names : List Sexp -> List Sexp; -gen-tuple-names vars = List_mapi - (lambda _ i -> Sexp_symbol (String_concat "%" (Int->String i))) - vars; - -%% -%% Takes a list -%% Returns a list of the same length with every element set to "?" symbol -%% -gen-deduce : List Sexp -> List Sexp; -gen-deduce vars = List_map - (lambda _ -> Sexp_symbol "?") - vars; - -%%% -%%% Access one tuple's element -%%% - -%% -%% This is a macro with conceptualy this signature: -%% tuple-nth : (tup-type : Type) ≡> (elem-type : Type) ≡> tup-type -> Int -> elem-type; -%% -%% Returns the n'th element of the tuple -%% -tuple-nth = macro (lambda args -> let - - nerr = lambda _ -> (Int->Integer (-1)); - - %% argument `n` of this macro - n : Integer; - n = Sexp_dispatch (List_nth 1 args Sexp_error) - (lambda _ _ -> nerr ()) - nerr nerr - (lambda n -> n) - nerr nerr; - - %% implicit tuple field name - elem-sym : Sexp; - elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); - - %% tuple, argument of this macro - tup : Sexp; - tup = List_nth 0 args Sexp_error; - -in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) -); - -%%% -%%% Affectation, unwraping tuple -%%% - -%% -%% syntax: -%% (x, y, z) <- p; -%% -%% and then `x`, `y`, `z` are defined as tuple's element 0, 1, 2 -%% -assign-tuple = macro (lambda args -> let - - xserr = lambda _ -> (nil : List Sexp); - - %% Expect a ","-node - %% Returns variables - get-tup-elem : Sexp -> List Sexp; - get-tup-elem sexp = Sexp_dispatch sexp - (lambda s ss -> - if (Sexp_eq s (Sexp_symbol "_,_")) then - (ss) - else - (nil)) - xserr xserr xserr xserr xserr; - - %% map every tuple's variable - %% using `tuple-nth` to assign element to variable - mf : Sexp -> Sexp -> Int -> Sexp; - mf t arg i = Sexp_node (Sexp_symbol "_=_") - (cons arg (cons (Sexp_node (Sexp_symbol "tuple-nth") - (cons t (cons (Sexp_integer (Int->Integer i)) nil))) nil)); - -in do { - IO_return (Sexp_node (Sexp_symbol "_;_") (List_mapi - (mf (List_nth 1 args Sexp_error)) - (get-tup-elem (List_nth 0 args Sexp_error)))); -}); - -%% -%% Wrap the third argument `fun` with a `let` definition for each variables -%% Names are taken from `rvars` and definition are taken from `ivars` -%% - -wrap-vars : List Sexp -> List Sexp -> Sexp -> Sexp; -wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> - %% - %% I prefer `let` definition because a lambda function would need a type - %% (quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1)))) - %% - (quote (let (uquote v1) = (uquote v0) in (uquote fun)))) - fun ivars rvars; - -%% -%% Takes a list of values (expressions) as Sexp (like a variable, 1, 1.0, "str", etc) -%% Returns a tuple containing those values -%% -make-tuple-impl : List Sexp -> IO Sexp; -make-tuple-impl values = let - - %% map tuple element declaration - mf1 : Sexp -> Sexp -> Sexp; - mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil)); - - %% map tuple element value - mf2 : Sexp -> Sexp -> Sexp; - mf2 value nth = Sexp_node (Sexp_symbol "_:=_") (cons nth (cons value nil)); - - ff1 : Sexp -> Sexp -> Sexp -> Sexp; - ff1 body arg arg-t = Sexp_node (Sexp_symbol "lambda_->_") - (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons arg-t nil))) - (cons body nil)); - - ff2 : Sexp -> Sexp -> Sexp; - ff2 body arg = Sexp_node (Sexp_symbol "lambda_≡>_") - (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons (Sexp_symbol "Type") nil))) - (cons body nil)); - -in do { - args-t <- gen-vars values; - - args <- gen-vars values; - - names <- IO_return (gen-tuple-names values); - - tuple-t <- IO_return (Sexp_node (Sexp_symbol "typecons") - (cons (Sexp_symbol "Tuple") - (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args-t)) nil))); - - tuple <- IO_return (Sexp_node (Sexp_node (Sexp_symbol "datacons") - (cons tuple-t (cons (Sexp_symbol "cons") nil))) - (List_map2 mf2 args names)); - - fun <- IO_return (List_foldl ff2 - (List_fold2 ff1 tuple (List_reverse args nil) - (List_reverse args-t nil)) - (List_reverse args-t nil)); - - values <- IO_return (List_reverse values nil); - - affect <- IO_return (Sexp_node fun (List_reverse values nil)); - - IO_return affect; -}; - -%% -%% Macro to instantiate a tuple -%% -make-tuple = macro (lambda args -> do { - r <- make-tuple-impl args; - r <- IO_return r; - IO_return r; -}); - -%% -%% Macro returning the type of a tuple -%% -%% Takes element's type as argument -%% -tuple-type = macro (lambda args -> let - - mf : Sexp -> Sexp -> Sexp; - mf n t = Sexp_node (Sexp_symbol "_::_") - (cons n (cons t nil)); - -in do { - names <- IO_return (gen-tuple-names args); - - r <- IO_return (Sexp_node (Sexp_symbol "typecons") (cons - (Sexp_symbol "Tuple") (cons (Sexp_node (Sexp_symbol "cons") - (List_map2 mf names args)) nil))); - - IO_return r; -}); +type Pair (a : Type) (b : Type) + | pair (fst : a) (snd : b); + +type Tuple3 (a : Type) (b : Type) (c : Type) + | tuple3 (v1 : a) (v2 : b) (v3 : c); + +type Tuple4 (a : Type) (b : Type) (c : Type) (d : Type) + | tuple4 (v1 : a) (v2 : b) (v3 : c) (v4 : d); + +type Tuple5 (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + | tuple5 (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e); + +type Tuple6 (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) (f : Type) + | tuple6 (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) (v6 : f); + +type Tuple7 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) + | tuple7 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g); + +type Tuple8 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) (h : Type) + | tuple8 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g) (v8 : h); + +type Tuple9 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) (h : Type) (i : Type) + | tuple9 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g) (v8 : h) (v9 : i); + +type Tuple10 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) (h : Type) (i : Type) (j : Type) + | tuple10 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g) (v8 : h) (v9 : i) (v10 : j); + +tuple-cstr-names = + cons "pair" + (cons "tuple3" + (cons "tuple4" + (cons "tuple5" + (cons "tuple6" + (cons "tuple7" + (cons "tuple8" + (cons "tuple9" + (cons "tuple10" nil)))))))); + +tuple-type-names = + cons "Pair" + (cons "Tuple3" + (cons "Tuple4" + (cons "Tuple5" + (cons "Tuple6" + (cons "Tuple7" + (cons "Tuple8" + (cons "Tuple9" + (cons "Tuple10" nil)))))))); + +make-sexp-from-names : List String -> List Sexp -> Sexp; +make-sexp-from-names name-list args = + let nb-args = List_length args; + tuple-name = List_nth (Int_- nb-args 2) name-list "" + in if Int_<= nb-args 10 + then Sexp_node (Sexp_symbol tuple-name) args + else Sexp_symbol "<ERROR: limit 10 items per tuple>"; + +make-tuple-impl = make-sexp-from-names tuple-cstr-names; +tuple-type-impl = make-sexp-from-names tuple-type-names; + +make-tuple = macro (lambda args -> IO_return (make-tuple-impl args)); + +tuple-type = macro (lambda args -> IO_return (tuple-type-impl args)); View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9da7553594a3908e07aa8234d5adaf790… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9da7553594a3908e07aa8234d5adaf790… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Keep track of residues during elaboration, in case unification becomes
by Stefan (＠monnier) 26 Aug '24

26 Aug '24

Stefan pushed to branch main at Stefan / Typer Commits: b07d2ac3 by Maxim Bernard at 2024-07-16T15:33:20-04:00 Keep track of residues during elaboration, in case unification becomes possible later. * src/elab.ml: Check for remaining residues after elaboration of definitions, but before generalization. * src/instargs.ml: Don't unify when searching for matches, simply check and discard side-effects (unless a match is found). * src/unification.ml: Keep track of residues in a global list, add them each time `unify'` is to return a `CKresidual`. Change the behavior of `unify` to only return impossible contraints, since otherwise it causes errors to be raised on residues. Provide a `check_unifiable` function to perform unification without side-effects. * tests/unify_test.ml: Adapt tests to account for new `unify` behavior. - - - - - 4 changed files: - src/elab.ml - src/instargs.ml - src/unification.ml - tests/unify_test.ml Changes: ===================================== src/elab.ml ===================================== @@ -1428,6 +1428,8 @@ and infer_and_generalize_type (ctx : elab_context) se name = and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in + Unif.check_no_residues (location e); + Unif.clean_residues (); let g = resolve_instances_and_generalize nctx e in let e' = g wrapLambda e in let t' = g (fun ne name t _l e ===================================== src/instargs.ml ===================================== @@ -106,7 +106,7 @@ let try_match t1 t2 lctx sl = List.exists (function | (Unif.CKimpossible,_,_,_) -> true | _ -> false) constraints in - match Unif.unify ~matching:sl t1 t2 lctx with + match Unif.check_unifiable ~matching:sl t1 t2 lctx with | [] -> Match | constraints when has_impossible constraints -> Impossible | _ -> Possible ===================================== src/unification.ml ===================================== @@ -44,6 +44,32 @@ let create_metavar (ctx : lexp_context) (sl : scope_level) (t : ltype) let dloc = DB.dloc let dsinfo = DB.dsinfo +(* For every definition, keep track of all residues during elaboration. There + is a chance they can be unified later (when some metavariable becomes + instanciated, for example). *) +let current_residues = ref ([] : (lexp_context * lexp * lexp) list) + +let add_residue (ctx : lexp_context) (e1 : lexp) (e2 : lexp) = + current_residues := (ctx, e1, e2) :: !current_residues + +let check_no_residues (first_def_loc : Source.Location.t) : unit = + (* Raises an error for every remaining residue. *) + List.iter + (fun (_ctx, lxp1, lxp2) -> + Log.log_error + ~section:"UNIF" + ~loc:first_def_loc + ("@[<v>Remaining residue. Can't unify:" + ^^ "@, @[<hov 2>%a@]" + ^^ "@,with:" + ^^ "@, @[<hov 2>%a@]@]") + Fmt.pp_print_lexp (clean lxp1) + Fmt.pp_print_lexp (clean lxp2)) + !current_residues + +let clean_residues () : unit = + current_residues := [] + (* For convenience *) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) @@ -55,14 +81,6 @@ type constraints = (constraint_kind * lexp_context * lexp * lexp) list type return_type = constraints -(* The association of a metavariable must change the scope levels of - the metavariables that are introduced to a wider scope. Here we - assume that this has already been done. This happens in `occurs_in` - during unification. *) -let associate (id: meta_id) (lxp: lexp) : unit = - (* FIXME: Check that the types are convertible? *) - metavar_table := U.IMap.add id (MVal lxp) (!metavar_table) - let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | MVal _ -> Log.internal_error "Checking occurrence of an instantiated metavar!!" @@ -75,7 +93,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | SortLevel (SLlub (e1, e2)) -> oi e1 || oi e2 | Sort (_, Stype e) -> oi e | Sort (_, (StypeOmega | StypeLevel)) -> false - | Builtin _ -> false + | Builtin (_, t) -> oi t | Var (_, _i) -> false | Proj (_,lxp, _) -> oi lxp | Susp (_e, _s) -> Log.internal_error "`e` should be \"clean\" here!?" @@ -115,11 +133,14 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with metavar_table := U.IMap.add id' (MVar (sl, t, cl)) (!metavar_table); false) in - let old_mvt = (!metavar_table) in + let old_mvt = !metavar_table in + let old_residue_list = !current_residues in if oi e then (* Undo the side-effects since we're not going to instantiate the var after all! *) - (metavar_table := old_mvt; true) + (metavar_table := old_mvt; + current_residues := old_residue_list; + true) else false (* When unifying a metavar with itself, if the two metavars don't @@ -218,7 +239,39 @@ let rec unify ?(matching : scope_level option) (e1: lexp) (e2: lexp) (ctx : lexp_context) : return_type = - unify' e1 e2 ctx OL.set_empty matching + let constraints = unify' e1 e2 ctx OL.set_empty matching in + List.filter (fun (kind, _, _, _) -> kind <> CKresidual) constraints + +(* The association of a metavariable must change the scope levels of + the metavariables that are introduced to a wider scope. Here we + assume that this has already been done. This happens in `occurs_in` + during unification. *) +and associate (id: meta_id) (lxp: lexp) : unit = + (* FIXME: Check that the types are convertible? *) + metavar_table := U.IMap.add id (MVal lxp) (!metavar_table); + (* Go through residues, see if, having instanciated this metavar, + we can unify any residue. *) + let old_residue_list = !current_residues in + (* Reason for purging the list: any lexp pair that is still non-unifiable + will be re-added to the list by `unify`. *) + clean_residues (); + let new_constraints = List.concat_map + (fun (ctx, lxp1, lxp2) -> unify lxp1 lxp2 ctx) + old_residue_list in + (* In case we find out some expressions are impossible to unify, + raise an error. *) + List.iter + (fun (_, _, lxp1, lxp2) -> + Log.log_error + ~section:"UNIF" + ~loc:(location lxp1) + ("@[<v>Unresolvable constraint. Expression:" + ^^ "@, @[<hov 2>%a@]" + ^^ "@,cannot be unified with:" + ^^ "@, @[<hov 2>%a@]@]") + Fmt.pp_print_lexp (clean lxp1) + Fmt.pp_print_lexp (clean lxp2)) + new_constraints and unify' (e1: lexp) (e2: lexp) (ctx : lexp_context) (vs : OL.set_plexp) @@ -279,8 +332,7 @@ and unify' (e1: lexp) (e2: lexp) | (Cons _, _) -> unify_cons msl e1' e2' ctx vs' | _ -> (if OL.conv_p ctx e1' e2' then [] - else ((* print_string "Unification failure on default\n"; *) - [(CKresidual, ctx, e1, e2)])) + else (add_residue ctx e1' e2'; [(CKresidual, ctx, e1, e2)])) (************************* Type specific unify *******************************) @@ -341,7 +393,7 @@ and unify_metavar (matching : scope_level option) "`lexp_whnf` returned an instantiated metavar!!" | MVar (sl, t, _) -> push_susp t s, sl in if not (matching_instantiation_check matching sl) - then [(CKresidual, ctx, lxp1, lxp2)] else + then (add_residue ctx lxp1 lxp2; [(CKresidual, ctx, lxp1, lxp2)]) else match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible -> log_info @@ -351,7 +403,7 @@ and unify_metavar (matching : scope_level option) ^^ "@, @[<hov 2>%a@]@]") Fmt.pp_print_subst s pp_print_clean_lexp lxp; - [(CKresidual, ctx, lxp1, lxp2)] + (add_residue ctx lxp1 lxp2; [(CKresidual, ctx, lxp1, lxp2)]) | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' -> associate idx lxp'; @@ -370,7 +422,7 @@ and unify_metavar (matching : scope_level option) pp_print_clean_lexp t pp_print_clean_lexp (OL.get_type ctx lxp) pp_print_clean_lexp lxp; - [(CKresidual, ctx, lxp1, lxp2)] in + (add_residue ctx lxp1 lxp2; [(CKresidual, ctx, lxp1, lxp2)]) in (* FIXME Here, we unify lxp1 with lxp2 again, because that the metavariables occuring in the associated term might have different substitutions from the corresponding @@ -462,7 +514,7 @@ 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 -> [] - | (_, _) -> [(CKresidual, ctx, var, lxp)] + | (_, _) -> (add_residue ctx var lxp; [(CKresidual, ctx, var, lxp)]) (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY @@ -480,7 +532,7 @@ and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs [] (List.combine lxp_list1 lxp_list2) with Invalid_argument _ (* Lists of diff. length in combine. *) - -> [(CKresidual, ctx, call, lxp)]) + -> (add_residue ctx call lxp; [(CKresidual, ctx, call, lxp)])) | (call', lxp') -> let head_left = match call' with | Call (_, head_left, _) -> head_left @@ -501,7 +553,7 @@ and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs inconvertible heads will remain. *) [(CKimpossible, ctx, head_left, head_right)] else - [(CKresidual, ctx, call, lxp)] + (add_residue ctx call lxp; [(CKresidual, ctx, call, lxp)]) (** Unify a Case with a lexp - Case, Case -> try to unify @@ -697,3 +749,19 @@ and unify_cons (matching : scope_level option) lxp1 lxp2 ctx vs = | (Cons (it1, (_, l1)), Cons (it2, (_, l2))) when l1 = l2 -> unify' it1 it2 ctx vs matching | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)] + +(* This function attempts to unify `e1` with `e2`, but discards all + side-effects, except if no impossible constraints nor any residues have + been found. + In the latter case, any instanciated metavariables are kept instanciated. *) +let check_unifiable ?(matching : scope_level option) + (e1: lexp) (e2: lexp) + (ctx : lexp_context) = + let old_residue_list = !current_residues in + let old_metavars = !metavar_table in + let unify_result = unify' e1 e2 ctx OL.set_empty matching in + current_residues := old_residue_list; + match unify_result with + | [] -> [] + | _ -> (metavar_table := old_metavars; + unify_result) ===================================== tests/unify_test.ml ===================================== @@ -55,16 +55,19 @@ let unif_output ?matching (lxp1: lexp) (lxp2: lexp) ctx = let orig_subst = !metavar_table in let constraints = unify ?matching lxp1 lxp2 ctx in match constraints with - | [] - -> let new_subst = !metavar_table in - if orig_subst == new_subst - then (Equivalent, constraints) - else (Unification, constraints) - | (CKresidual, _, _, _)::_ -> (Constraint, constraints) - | (CKimpossible, _, _, _)::_ -> (Nothing, constraints) + | [] -> + if !current_residues == [] then + let new_subst = !metavar_table in + if orig_subst == new_subst + then (Equivalent, constraints) + else (Unification, constraints) + else + (Constraint, constraints) + | _ -> (Nothing, constraints) let add_unif_test name ?matching ?(ectx=ectx) lxp_a lxp_b expected = add_test "UNIFICATION" name (fun () -> + clean_residues (); let (r, _) = unif_output ?matching lxp_a lxp_b (DB.ectx_to_lctx ectx) in if r = expected then View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b07d2ac397b7ca5b8e78917b0887eb01c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b07d2ac397b7ca5b8e78917b0887eb01c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] 4 commits: Move internal representations to a separate module, named Ir.
by Stefan (＠monnier) 28 May '24

28 May '24

Stefan pushed to branch main at Stefan / Typer Commits: 4919a2ab by Maxim Bernard at 2024-05-18T16:48:18-04:00 Move internal representations to a separate module, named Ir. Import Ir in all relevant modules, and remove unneeded imports. Move all datatypes representing context (lexp_context, elab_context, typeclass_context, runtime_env) and code (sexp, lexp, elexp, value) and their related types to the same mutually-recursive block. Rename `set` to `db_set` for clarity. Rename `value_type` to simply `value` for consistency with the naming convention used in the rest of the project. Rename all `elexp` constructors by prefixing them with an "E", to avoid clashes with `lexp`. Change `Imm` constructor so it contains a `sinfo * value` pair instead of an `sexp`. Similar change to `Eimm`. * src/sexp.ml : Replace `Sym.t` with `symbol` for clarity, and remove `t` for the same reason. Replace certain `sexp`s in function types to `token` when appropriate. Replace certain `sexp`s in function types to `token` when appropriate. * src/lexp.ml : `lexp_head` can't return the exact Imm name for now; can be fixed later (needs further refactoring). Remove unsued `pred_imm`. * src/inverse_subst.ml: Improve code clarity. * src/elab.ml (elab_macro_call) : Replace `token` with `sexp` in argument type for clarity. - - - - - 7fc20e58 by Maxim Bernard at 2024-05-21T01:57:01-04:00 Move all pretty-printing functions to the same module. * src/fmt.ml: Move printing functions from all over the project to here. Define them all in the same mutually recursive block (required to print `Imm` values). Polymorphic functions in that block require explicit type variables, otherwise OCaml attempts to assign them a non polymorphic type. Fix bug in `pp_print_lexp` (formerly `Lexp.pp_print`) in `Inductive` branch where a formatting block was opened without being closed. * src/ir.ml: Move `pretoken` from Prelexer to here. Re-arrange type definitions to minimise recursive definitions. Replace uses of `Source.Location.t` with `location` for clarity. * src/pexp.ml: Remove obsolete ArgKind module, since functions have been moved to Fmt. * src/util.ml: Move `maybename` from Lexp to here (required by Fmt). - - - - - 7b0ff399 by Maxim Bernard at 2024-05-22T01:54:10-04:00 Improve message formatting thoughout the project. Print log messages using pretty-printing functions when available and the Format module instead of string conversions, which allow for appropriate indentation to be generated. Perform a `clean` on all lexps prior to printing them, for performance reasons (otherwise, all memory would be consumed). * src/fmt.ml: Reactivate printing lexps in substitutions (since they can now be printed safely, see above). * src/lexp.ml: Define functions to be used elsewhere in the project when printing lexps. * src/log.ml: Change type of `log_msg` to allow for `%a` conversion specifications in format strings. * src/opslexp.ml: Cleanup dead code and re-organize module imports for cleanness. - - - - - 2e478c82 by Maxim Bernard at 2024-05-22T17:24:07-04:00 Rearrange definitions in Ir. * src/ir.ml: Reduce size of mutually recursive `type` block to a minimum, by extracting types that don't need to be there. Transfer a couple of definitions from Util for consistency. * src/util.ml: Transfer several definitions from here to Ir. - - - - - 30 changed files: - src/REPL.ml - src/backend.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/instargs.ml - src/inverse_subst.ml - + src/ir.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/env_test.ml - tests/eval_test.ml - tests/instargs_test.ml - tests/lexer_test.ml - tests/macro_test.ml - tests/positivity_test.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/476b8241874c55883ab2ee370813646c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/476b8241874c55883ab2ee370813646c… You're receiving this email because of your account on gitlab.com.

1 0

Types quotient et égalité définitionnelle
by Stefan Monnier 02 May '24

02 May '24

Salut James, T'avais raison de rester avec une égalité propositionnelle pour tes types quotient: renforcer l'égalité définitionnelle pour les types quotients pose des problèmes. Soit le type quotient A/F où A est le type de base et F est une fonction qui prend un argument de type A et renvoie la classe d'équivalence à laquel il appartient. Soit une élimination comme: Qrec: ?A/?F → (f : ?A → ?t) → (P : ∀ x,y . ?F x = ?F y → f x = f y) → ?t; qui dit que tu peux appliquer `f` au "contenu" d'un quotient ?A/?F pour autant que tu prouves avec `P` que `f` traite tous les éléments d'une même classe de la même manière. Le problème est que l'élimination ne garanti que l'égalité propositionnelle du résultat. Donc si tu permets à deux valeurs différentes de type A/F d'être définitionnellement égales, t'as un problème, parce que tu casses le principe que e₁ ≃ e₂ => E[e₁] ≃ E[e₂] Plus concrètement, disons que le constructeur des quotients est Qin, si tu as e₁ ≄ e₂ ∧ Qin e₁ ≃ Qin e₂ tu peux montrer que E[Qin e₁] = E[Qin e₂] parce que ton `Qrec` te donne cette `=` (i.e. égalité propositionnelle), mais tu ne peux pas montrer que cette égalité est vraie définitionnellement (`≃`), et en effet elle n'est pas vraie définitionnellement si le `f` de l'éliminateur est la fonction identité (qui est un cas possible si le contexte nous fournit la preuve `P`). Donc à moins de faire attention que `Qrec` renvoie toujours une valeur "normalisée", on perd la propriété de "subject reduction". 🙁 Étonnement, je n'ai encore pas vu une telle explication dans mes lectures. Toi? Stefan

2 1

Propositional truncation
by Stefan Monnier 25 Apr '24

25 Apr '24

Pour transformer une proposition en une "mere proposition", et que tu ne veux/peux pas utiliser `conv_erase`, au lieu de |P| = Erased P tu peux utiliser la double négation |P| = (P → ?A) → ?A maintenant qu'on a la "functional extensionality". Stefan

1 0