Septembre 2018 - Typer - mailman.iro.umontreal.ca

Datatypes and tuples
by Stefan Monnier 02 Oct '18

02 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

[Git][monnier/typer] Deleted branch graveline
by Stefan 24 Sep '18

24 Sep '18

Stefan deleted branch graveline at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch bosn
by Stefan 24 Sep '18

24 Sep '18

Stefan deleted branch bosn at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Rename Aexplicit to Anormal
by Stefan 20 Sep '18

20 Sep '18

Stefan pushed to branch master at Stefan / Typer Commits: 2f9ed1b0 by Stefan Monnier at 2018-09-21T02:30:43Z Rename Aexplicit to Anormal - - - - - 8 changed files: - src/builtin.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - tests/unify_test.ml Changes: ===================================== src/builtin.ml ===================================== @@ -95,8 +95,8 @@ let set_predef name lexp (* Builtin types *) let dloc = DB.dloc -let op_binary t = mkArrow (Aexplicit, (dloc, None), t, dloc, - mkArrow (Aexplicit, (dloc, None), t, dloc, t)) +let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, + mkArrow (Anormal, (dloc, None), t, dloc, t)) let type_eq = let lv = (dloc, Some "l") in @@ -105,9 +105,9 @@ let type_eq = DB.type_level, dloc, mkArrow (Aerasable, tv, mkSort (dloc, Stype (Var (lv, 0))), dloc, - mkArrow (Aexplicit, (dloc, None), + mkArrow (Anormal, (dloc, None), Var (tv, 0), dloc, - mkArrow (Aexplicit, (dloc, None), + mkArrow (Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (Var (lv, 3))))))) @@ -164,13 +164,13 @@ let register_builtin_csts () = let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in let _ = new_builtin_type - "IO" (mkArrow (Aexplicit, (dloc, None), + "IO" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type - "Ref" (mkArrow (Aexplicit, (dloc, None), + "Ref" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type - "Array" (mkArrow (Aexplicit, (dloc, None), + "Array" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type "FileHandle" DB.type0 in let _ = new_builtin_type "Eq" type_eq in ===================================== src/elab.ml ===================================== @@ -700,7 +700,7 @@ and check_case rtype (loc, target, ppatterns) ctx = ((ak, var)::acc) | ((ef, var)::pargs, (ak, _, fty)::cargs) when (match (ef, ak) with - | (Some (_, "_"), _) | (None, Aexplicit) -> true + | (Some (_, "_"), _) | (None, Anormal) -> true | _ -> false) -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in make_nctx nctx (ssink var s) pargs cargs pe @@ -712,7 +712,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | pargs, (ak, fname, fty)::cargs -> let var = (loc, None) in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in - if ak = Aexplicit then + if ak = Anormal then sexp_error loc ("Missing pattern for normal field" ^ (match fname with (_, Some n) -> " `" ^ n ^ "`" @@ -825,11 +825,11 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | sarg :: sargs, _ -> let (arg_type, ret_type) = match ltp' with | Arrow (ak, _, arg_type, _, ret_type) - -> assert (ak = Aexplicit); (arg_type, ret_type) + -> assert (ak = Anormal); (arg_type, ret_type) | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Aexplicit (dloc, None) None in + ltp' Anormal (dloc, None) None in let larg = check sarg arg_type ctx in - handle_fun_args ((Aexplicit, larg) :: largs) sargs pending + handle_fun_args ((Anormal, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) in let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in @@ -1260,22 +1260,22 @@ let sform_datacons ctx loc sargs ot = let elab_colon_to_ak k = match k with | "_:::_" -> Aerasable | "_::_" -> Aimplicit - | _ -> Aexplicit + | _ -> Anormal let elab_datacons_arg s = match s with | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t]) -> (elab_colon_to_ak k, elab_p_id s, t) - | _ -> (Aexplicit, (sexp_location s, None), s) + | _ -> (Anormal, (sexp_location s, None), s) let elab_typecons_arg arg : (arg_kind * vname * sexp option) = match arg with | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e]) -> (elab_colon_to_ak k, (l, Some name), Some e) - | Symbol (l, name) -> (Aexplicit, (l, Some name), None) + | Symbol (l, name) -> (Anormal, (l, Some name), None) | _ -> sexp_print arg; (sexp_error (sexp_location arg) "Unrecognized formal arg"); - (Aexplicit, (sexp_location arg, None), None) + (Anormal, (sexp_location arg, None), None) let sform_typecons ctx loc sargs ot = match sargs with @@ -1459,8 +1459,8 @@ let rec sform_lambda kind ctx loc sargs ot = ^ lexp_string lt1 ^ "`")); mklam lt1 (Some lt2) - | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit - (* `t` is an implicit arrow and `kind` is Aexplicit, + | Arrow (ak2, v, lt1, _, lt2) when kind = Anormal + (* `t` is an implicit arrow and `kind` is Anormal, * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) -> (* FIXME: Here we end up adding a local variable `v` whose @@ -1479,7 +1479,7 @@ let rec sform_lambda kind ctx loc sargs ot = -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 in mklam lt1 (Some lt2)) - | _ -> sexp_error loc ("##lambda_"^(match kind with Aexplicit -> "->" + | _ -> sexp_error loc ("##lambda_"^(match kind with Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>") ^"_ takes two arguments"); @@ -1620,10 +1620,10 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); - ("lambda_->_", sform_lambda Aexplicit); + ("lambda_->_", sform_lambda Anormal); ("lambda_=>_", sform_lambda Aimplicit); ("lambda_≡>_", sform_lambda Aerasable); - ("_->_", sform_arrow Aexplicit); + ("_->_", sform_arrow Anormal); ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable); ("case_", sform_case); ===================================== src/elexp.ml ===================================== @@ -32,7 +32,7 @@ open Sexp (* Sexp type *) -open Pexp (* Aexplicit *) +open Pexp (* Anormal *) module U = Util module L = Lexp ===================================== src/eval.ml ===================================== @@ -491,7 +491,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Aexplicit, Var (vdummy, -1))])) + -> Vtype (L.mkCall (e, [(Anormal, Var (vdummy, -1))])) | _ -> value_fatal loc f "Trying to call a non-function!" and eval_case ctx i loc target pat dflt = ===================================== src/lexp.ml ===================================== @@ -429,14 +429,14 @@ let rec lexp_unparse lxp = -> let l = lexp_location lxp in let st = lexp_unparse ltp in Node (Symbol (l, match kind with - | Aexplicit -> "lambda_->_" + | Anormal -> "lambda_->_" | Aimplicit -> "lambda_=>_" | Aerasable -> "lambda_≡>_"), [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body]) | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" + Node (Symbol (loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 @@ -476,11 +476,11 @@ let rec lexp_unparse lxp = List.map (fun arg -> match arg with - | (Aexplicit, (_,None), t) -> lexp_unparse t + | (Anormal, (_,None), t) -> lexp_unparse t | (ak, s, t) -> let (l,_) as id = sname s in Node (Symbol (l, match ak with - | Aexplicit -> "_:_" + | Anormal -> "_:_" | Aimplicit -> "_::_" | Aerasable -> "_:::_"), [Symbol id; lexp_unparse t])) @@ -652,7 +652,7 @@ let rec get_precedence expr ctx = | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" - | Arrow (Aexplicit, _, _, _, _) -> lkp "->" + | Arrow (Anormal, _, _, _, _) -> lkp "->" | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" | Call (exp, _) -> get_precedence exp ctx @@ -712,10 +712,10 @@ and lexp_str ctx (exp : lexp) : string = else green ^ str ^ reset in let kind_str k = match k with - | Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in + | Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in let kindp_str k = match k with - | Aexplicit -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in + | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in let get_name fname = match fname with | Builtin ((_, name), _, _) -> name, 0 @@ -792,7 +792,7 @@ and lexp_str ctx (exp : lexp) : string = match arg_type with | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) - | Aexplicit -> str ^ " " ^ (lexp_str' lxp) + | Anormal -> str ^ " " ^ (lexp_str' lxp) | _ -> str in ( match args with ===================================== src/opslexp.ml ===================================== @@ -391,7 +391,7 @@ let nerased_let defs erased = if not (List.mem true es) then nerased else List.fold_left (fun erased e - -> dbset_push (if e then P.Aerasable else P.Aexplicit) erased) + -> dbset_push (if e then P.Aerasable else P.Anormal) erased) erased es (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) ===================================== src/pexp.ml ===================================== @@ -29,7 +29,7 @@ let pexp_error = msg_error "PEXP" (*************** The Pexp Parser *********************) -type arg_kind = Aexplicit | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) (* This is Dangerously misleading since pvar is NOT pexp but Pvar is *) type pvar = symbol @@ -46,11 +46,11 @@ let pexp_pat_location e = match e with let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with - | (Aexplicit, s, None) -> Symbol s + | (Anormal, s, None) -> Symbol s | (ak, ((l,_) as s), t) -> Node (Symbol (l, match ak with Aerasable -> ":::" | Aimplicit -> "::" - | Aexplicit -> ":"), + | Anormal -> ":"), [Symbol s; match t with Some e -> e | None -> Symbol (l, "_")]) ===================================== tests/unify_test.ml ===================================== @@ -125,11 +125,11 @@ let input_type_t = generate_ltype_from_str str_type2 let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = - ( Lambda ((Aexplicit), + ( Lambda ((Anormal), (Util.dummy_location, Some "L1"), Var((Util.dummy_location, Some "z"), 3), Imm (Integer (Util.dummy_location, 3))), - Lambda ((Aexplicit), + Lambda ((Anormal), (Util.dummy_location, Some "L2"), Var((Util.dummy_location, Some "z"), 4), Imm (Integer (Util.dummy_location, 3))), Nothing ) View it on GitLab: https://gitlab.com/monnier/typer/commit/2f9ed1b09add160cbf9ea70bda4a4c30ee5… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/2f9ed1b09add160cbf9ea70bda4a4c30ee5… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Get rid of identifiers starting with underscore in *.ml
by Stefan 20 Sep '18

20 Sep '18

Stefan pushed to branch master at Stefan / Typer Commits: 76a477f1 by Stefan Monnier at 2018-09-21T02:27:11Z Get rid of identifiers starting with underscore in *.ml - - - - - 8 changed files: - src/REPL.ml - src/debruijn.ml - src/debug.ml - src/debug_util.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/unification.ml Changes: ===================================== src/REPL.ml ===================================== @@ -103,21 +103,21 @@ type lexpr = lexp (* Grouping declaration together will enable us to support mutually recursive * declarations while bringing us closer to normal typer *) let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = - let rec _pxp_parse sxps dacc pacc = + let rec pxp_parse sxps dacc pacc = match sxps with | [] -> (List.rev dacc), (List.rev pacc) | sxp::tl -> match sxp with (* Declaration *) | Node (Symbol (_, ("_=_" | "_:_")), [Symbol s; t]) -> - _pxp_parse tl (sxp :: dacc) pacc + pxp_parse tl (sxp :: dacc) pacc (* f arg1 arg2 = function body; *) | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> - _pxp_parse tl (sxp :: dacc) pacc + pxp_parse tl (sxp :: dacc) pacc (* Expression *) - | _ -> _pxp_parse tl dacc (sxp::pacc) in - _pxp_parse sxps [] [] + | _ -> pxp_parse tl dacc (sxp::pacc) in + pxp_parse sxps [] [] let ierase_type (lexps: (ldecl list list * lexpr list)) = ===================================== src/debruijn.ml ===================================== @@ -257,7 +257,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start = let ord = extract_names ctx [] in - let rec _print idx ord = + let rec print idx ord = match ord with | [] -> () | hd::tl ->( @@ -281,7 +281,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start = let _ = match exp with | None -> print_string "<var>" | Some exp -> ( - let str = _lexp_str (!debug_ppctx) exp in + let str = lexp_str (!debug_ppctx) exp in let str = (match str_split str '\n' with | hd::tl -> print_string hd; tl | _ -> []) in @@ -291,12 +291,12 @@ let print_lexp_ctx_n (ctx : lexp_context) start = print_string (": "); lexp_print tp; print_string "\n"; - _print (idx + 1) tl + print (idx + 1) tl with Not_found -> - (print_string "Not_found |\n"; _print (idx + 1) tl)) in + (print_string "Not_found |\n"; print (idx + 1) tl)) in - _print (start - 1) ord; print_string (make_sep '=') + print (start - 1) ord; print_string (make_sep '=') (* Only print user defined variables *) ===================================== src/debug.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -131,7 +131,7 @@ let debug_lexp_decls decls = lalign_print_string (lexp_name lxp) 15; print_string "["; loc_print loc; print_string "]"; - let str = _lexp_str_decls (!debug_ppctx) [e] in + let str = lexp_str_decls (!debug_ppctx) [e] in (* First col size = 15 + 1 + 2 + 3 + 5 + 6 * = 32 *) ===================================== src/debug_util.ml ===================================== @@ -183,7 +183,7 @@ let format_source () = print_string (make_sep '-'); print_string "\n"; - let result = _lexp_str_decls (!ppctx) (List.flatten lexps) in + let result = lexp_str_decls (!ppctx) (List.flatten lexps) in if (!write_file) then ( print_string (" " ^ " Writing output file: " ^ (!format_dest) ^ "\n"); ===================================== src/elab.ml ===================================== @@ -1012,7 +1012,7 @@ and lexp_decls_1 (pending_defs : (symbol * sexp) list) (* Pending definitions. *) : (vname * lexp * ltype) list * sexp list * elab_context = - let rec _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = + let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then let (s, l) = SMap.choose pending_decls in @@ -1022,10 +1022,10 @@ and lexp_decls_1 [], [], nctx | Symbol (_, "") :: sdecls - -> _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs | Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls - -> _lexp_decls_1 (List.append sdecls' sdecls) + -> lexp_decls_1 (List.append sdecls' sdecls) ectx nctx pending_decls pending_defs | Node (Symbol (l, "_:_"), args) :: sdecls @@ -1048,17 +1048,17 @@ and lexp_decls_1 ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") | Some [] -> () in - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else _lexp_decls_1 sdecls ectx + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + else lexp_decls_1 sdecls ectx (ectx_extend nctx (l, Some vname) ForwardRef ltp) (SMap.add vname l pending_decls) pending_defs | _ -> error l "Invalid type declaration syntax"; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "_=_") as head, args) :: sdecls (* FIXME: Move this to a "special form"! *) @@ -1090,15 +1090,15 @@ and lexp_decls_1 let decls, nctx = lexp_check_decls ectx nctx pending_defs in decls, sdecls, nctx else - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else (error l ("`" ^ vname ^ "` defined but not declared!"); - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | [Node (Symbol s, args) as d; body] -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - _lexp_decls_1 ((Node (head, + lexp_decls_1 ((Node (head, [Symbol s; Node (Symbol (sexp_location d, "lambda_->_"), [sexp_u_list args; body])])) @@ -1106,25 +1106,25 @@ and lexp_decls_1 ectx nctx pending_decls pending_defs | _ -> error l "Invalid definition syntax"; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "define-operator"), args) :: sdecls (* FIXME: Move this to a "special form"! *) - -> _lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) + -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) pending_decls pending_defs | Node (Symbol ((l, _) as v), sargs) :: sdecls -> (* expand macro and get the generated declarations *) let sdecl' = lexp_decls_macro v sargs nctx in - _lexp_decls_1 (sdecl' :: sdecls) ectx nctx + lexp_decls_1 (sdecl' :: sdecls) ectx nctx pending_decls pending_defs | sexp :: sdecls -> error (sexp_location sexp) "Invalid declaration syntax"; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in (EV.set_getenv nctx; - let res = _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in + let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in (stop_on_error (); res)) and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) ===================================== src/eval.ml ===================================== @@ -365,10 +365,10 @@ let file_write loc depth args_val = match args_val with | _ -> List.iter (fun v -> value_print v) args_val; error loc "File.write expects an out_channel and a string" -let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = +let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = let trace = append_eval_trace trace lxp in - let eval lxp ctx = _eval lxp ctx trace in + let eval' lxp ctx = eval lxp ctx trace in (* This creates an O(N^2) cost for deep recursion because rec_depth * uses `length` on the stack trace. *) @@ -398,14 +398,14 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type (* Nodes *) (* ---------------- *) | Let(_, decls, inst) - -> let nctx = _eval_decls decls ctx trace in - eval inst nctx + -> let nctx = eval_decls decls ctx trace in + eval' inst nctx (* Function call *) | Call (f, args) -> eval_call (elexp_location f) f trace - (_eval f ctx trace) - (List.map (fun e -> _eval e ctx trace) args) + (eval f ctx trace) + (List.map (fun e -> eval e ctx trace) args) (* Case *) | Case (loc, target, pat, dflt) @@ -451,8 +451,8 @@ and eval_call loc unef i f args = -> bindargs e vs (add_rte_variable x v ctx) | ([], _) -> let trace = append_typer_trace i unef in - _eval e ctx trace - | _ -> eval_call loc unef i (_eval e ctx i) vs in + eval e ctx trace + | _ -> eval_call loc unef i (eval e ctx i) vs in bindargs e vs (add_rte_variable x v ctx) | Vbuiltin (name), args @@ -496,7 +496,7 @@ and eval_call loc unef i f args = and eval_case ctx i loc target pat dflt = (* Eval target *) - let v = _eval target ctx i in + let v = eval target ctx i in (* extract constructor name and arguments *) let ctor_name, args = match v with @@ -521,23 +521,23 @@ and eval_case ctx i loc target pat dflt = | [], [] -> nctx in let nctx = fold2 ctx pat_args args in - _eval exp nctx i + eval exp nctx i (* Run default *) with Not_found -> (match dflt with | Some (var, lxp) - -> _eval lxp (add_rte_variable var v ctx) i + -> eval lxp (add_rte_variable var v ctx) i | _ -> error loc "Match Failure") and build_arg_list args ctx i = - (* _eval every args *) - let arg_val = List.map (fun (k, e) -> _eval e ctx i) args in + (* eval every args *) + let arg_val = List.map (fun (k, e) -> eval e ctx i) args in (* Add args inside context *) List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val -and _eval_decls (decls: (vname * elexp) list) - (ctx: runtime_env) i: runtime_env = +and eval_decls (decls: (vname * elexp) list) + (ctx: runtime_env) i: runtime_env = let n = (List.length decls) - 1 in @@ -546,7 +546,7 @@ and _eval_decls (decls: (vname * elexp) list) add_rte_variable name Vundefined ctx) ctx decls in List.iteri (fun idx (name, lxp) -> - let v = _eval lxp nctx i in + let v = eval lxp nctx i in let offset = n - idx in ignore (set_rte_variable offset name v nctx)) decls; @@ -559,7 +559,7 @@ and _eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let eval a b = _eval a b depth in + let eval a b = eval a b depth in let sxp, nd, ctx_nd, sym, ctx_sym, str, ctx_str, @@ -1048,7 +1048,7 @@ let register_builtin_constants () = ] let _ = register_builtin_constants () -let eval lxp ctx = _eval lxp ctx ([], []) +let eval lxp ctx = eval lxp ctx ([], []) let debug_eval lxp ctx = try eval lxp ctx @@ -1058,7 +1058,7 @@ let debug_eval lxp ctx = raise e) -let eval_decls decls ctx = _eval_decls decls ctx ([], []) +let eval_decls decls ctx = eval_decls decls ctx ([], []) let eval_decls_toplevel (decls: (vname * elexp) list list) ctx = (* Add toplevel decls function *) ===================================== src/lexp.ml ===================================== @@ -670,15 +670,15 @@ and lexp_string e = lexp_cstring (!debug_ppctx) e (* Context Print *) and lexp_cprint ctx e = print_string (lexp_cstring ctx e) -and lexp_cstring ctx e = _lexp_str ctx e +and lexp_cstring ctx e = lexp_str ctx e (* Implementation *) -and _lexp_str ctx (exp : lexp) : string = +and lexp_str ctx (exp : lexp) : string = let ctx = set_parent exp ctx in let inter_ctx = add_indent ctx 1 in - let lexp_str = _lexp_str ctx in - let lexp_stri idt e = _lexp_str (add_indent ctx idt) e in + let lexp_str' = lexp_str ctx in + let lexp_stri idt e = lexp_str (add_indent ctx idt) e in let pretty = pp_pretty ctx in let color = pp_color ctx in @@ -731,7 +731,7 @@ and _lexp_str ctx (exp : lexp) : string = | Float (_, s) -> tval (string_of_float s) | e -> sexp_string e) - | Susp (e, s) -> _lexp_str ctx (push_susp e s) + | Susp (e, s) -> lexp_str ctx (push_susp e s) | Var ((loc, name), idx) -> maybename name ^ (index idx) ; @@ -739,7 +739,7 @@ and _lexp_str ctx (exp : lexp) : string = (* print metavar result if any *) -> (let print_meta exp = let ctx = set_meta exp ctx in - _lexp_str ctx (clean exp) in + lexp_str ctx (clean exp) in match pp_meta ctx with | None -> print_meta exp @@ -750,7 +750,7 @@ and _lexp_str ctx (exp : lexp) : string = | Let (_, decls, body) -> (* Print first decls without indent *) let h1, decls, idt_lvl = - match _lexp_str_decls inter_ctx decls with + match lexp_str_decls inter_ctx decls with | h1::decls -> h1, decls, 2 | _ -> "", [], 1 in @@ -767,32 +767,32 @@ and _lexp_str ctx (exp : lexp) : string = (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) | Arrow(k, (_, Some name), tp, loc, expr) -> - "(" ^ name ^ " : " ^ (lexp_str tp) ^ ") " ^ - (kind_str k) ^ " " ^ (lexp_str expr) + "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ + (kind_str k) ^ " " ^ (lexp_str' expr) | Arrow(k, (_, None), tp, loc, expr) -> - "(" ^ (lexp_str tp) ^ " " - ^ (kind_str k) ^ " " ^ (lexp_str expr) ^ ")" + "(" ^ (lexp_str' tp) ^ " " + ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" | Lambda(k, (loc, name), ltype, lbody) -> - let arg = "(" ^ maybename name ^ " : " ^ (lexp_str ltype) ^ ")" in + let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ (make_indent 1) ^ (lexp_stri 1 lbody) | Cons(t, (_, ctor_name)) -> - (keyword "datacons ") ^ (lexp_str t) ^ " " ^ ctor_name + (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name | Call(fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = - "(" ^ (lexp_str lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str rhs) ^ ")" in + "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in let print_arg str (arg_type, lxp) = match arg_type with - | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str lxp) - | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str lxp) - | Aexplicit -> str ^ " " ^ (lexp_str lxp) + | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) + | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) + | Aexplicit -> str ^ " " ^ (lexp_str' lxp) | _ -> str in ( match args with @@ -800,7 +800,7 @@ and _lexp_str ctx (exp : lexp) : string = binop_str (" " ^ (get_binary_op_name name)) lhs rhs | _ -> let args = List.fold_left print_arg "" args in - "(" ^ (lexp_str fname) ^ args ^ ")") + "(" ^ (lexp_str' fname) ^ args ^ ")") | Inductive (_, (_, name), [], ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ @@ -811,14 +811,14 @@ and _lexp_str ctx (exp : lexp) : string = = List.fold_left (fun str (arg_kind, (_, name), ltype) -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str ltype) ^ ")") + ^ (lexp_str' ltype) ^ ")") "" args in (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ (lexp_str_ctor ctx ctors) | Case (_, target, _ret, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_str target) in + let str = (keyword "case ") ^ (lexp_str' target) in let arg_str arg = List.fold_left (fun str v -> match v with @@ -861,24 +861,24 @@ and lexp_str_ctor ctx ctors = SMap.fold (fun key value str -> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in let str = List.fold_left (fun str (k, _, arg) - -> str ^ " " ^ (_lexp_str ctx arg)) + -> str ^ " " ^ (lexp_str ctx arg)) str value in str ^ ")") ctors "" -and _lexp_str_decls ctx decls = +and lexp_str_decls ctx decls = - let lexp_str = _lexp_str ctx in + let lexp_str' = lexp_str ctx in let sepdecl = (if pp_decl ctx then "\n" else "") in let type_str name lxp = (if pp_type ctx then ( - name ^ " : " ^ (lexp_str lxp) ^ ";") else "") in + name ^ " : " ^ (lexp_str' lxp) ^ ";") else "") in let ret = List.fold_left (fun str ((_, name), lxp, ltp) -> let name = maybename name in let str = if pp_type ctx then (type_str name ltp)::str else str in - (name ^ " = " ^ (lexp_str lxp) ^ ";" ^ sepdecl)::str) + (name ^ " = " ^ (lexp_str' lxp) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret ===================================== src/unification.ml ===================================== @@ -120,7 +120,7 @@ let unify_and res op = match res with (** Dispatch to the right unifier. - If (<code>_unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) + If (<code>unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) *) @@ -141,17 +141,17 @@ and unify' (e1: lexp) (e2: lexp) | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) -> if OL.conv_p ctx e1' e2' then Some [] else None - | (l, (Metavar (idx, s, _) as r)) -> _unify_metavar ctx idx s r l - | ((Metavar (idx, s, _) as l), r) -> _unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> _unify_call r l ctx vs' - (* | (l, (Case _ as r)) -> _unify_case r l subst *) - | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' - | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' - | (Call _ as l, r) -> _unify_call l r ctx vs' - (* | (Case _ as l, r) -> _unify_case l r subst *) - (* | (Inductive _ as l, r) -> _unify_induct l r subst *) - | (Sort _ as l, r) -> _unify_sort l r ctx vs' - | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs' + | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l + | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r + | (l, (Call _ as r)) -> unify_call r l ctx vs' + (* | (l, (Case _ as r)) -> unify_case r l subst *) + | (Arrow _ as l, r) -> unify_arrow l r ctx vs' + | (Lambda _ as l, r) -> unify_lambda l r ctx vs' + | (Call _ as l, r) -> unify_call l r ctx vs' + (* | (Case _ as l, r) -> unify_case l r subst *) + (* | (Inductive _ as l, r) -> unify_induct l r subst *) + | (Sort _ as l, r) -> unify_sort l r ctx vs' + | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' | _ -> Some (if OL.conv_p ctx e1' e2' then [] else [(e1, e2)]) (********************************* Type specific unify *******************************) @@ -163,7 +163,7 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Var) -> Constraint - (_, _) -> None *) -and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs +and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), @@ -187,7 +187,7 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs - Lambda , Let -> Constraint - Lambda , lexp -> unify lexp lambda subst *) -and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = +and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) @@ -211,7 +211,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) +and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with @@ -258,7 +258,7 @@ and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and _unify_call (call: lexp) (lxp: lexp) ctx vs +and unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) @@ -276,15 +276,15 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs - Case, Case -> try to unify - Case, _ -> Constraint *) -(* and _unify_case (case: lexp) (lxp: lexp) (subst: meta_subst) : return_type = +(* and unify_case (case: lexp) (lxp: lexp) (subst: meta_subst) : return_type = * let merge (_, const) subst_res = match subst_res with * | None -> None * | Some (s', c') -> Some (s', const@c') * in * let match_unify_inner lst smap1 smap2 subst = - * match _unify_inner lst subst with + * match unify_inner lst subst with * | None -> None - * | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) + * | Some (s, c) -> merge (s, c) (unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) * in * let match_lxp_opt lxp_opt1 lxp_opt2 tail smap1 smap2 subst = * match lxp_opt1, lxp_opt2 with @@ -304,15 +304,15 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs - Inductive, Call/Metavar/Case/Let -> constraint - Inductive, _ -> None *) -(* and _unify_induct (induct: lexp) (lxp: lexp) (subst: meta_subst) : return_type = +(* and unify_induct (induct: lexp) (lxp: lexp) (subst: meta_subst) : return_type = * let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f)) * and merge map1 map2 (subst, const) : return_type = - * match (_unify_induct_sub_list (SMap.bindings map1) (SMap.bindings map2) subst) with + * match (unify_induct_sub_list (SMap.bindings map1) (SMap.bindings map2) subst) with * | Some (s', c') -> Some (s', const@c') * | None -> None * in * let zip_unify lst subst map1 map2 : return_type = - * match _unify_inner_induct lst subst with + * match unify_inner_induct lst subst with * | None -> None * | Some (s, c) -> merge map1 map2 (s, c) * in @@ -329,7 +329,7 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some [] @@ -343,7 +343,7 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - Sort, Var -> Constraint - Sort, lexp -> ERROR *) -and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs @@ -364,18 +364,18 @@ and is_same arglist arglist2 = | _, _ -> false (** try to unify the SMap part of the case *) -(* and _unify_inner_case lst subst = +(* and unify_inner_case lst subst = * let merge (_, c) res = * match res with * | Some (s', c') -> Some (s', c@c') * | None -> None * in - * let rec _unify_inner_case list_ subst = + * let rec unify_inner_case list_ subst = * match list_ with * | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 -> * (if is_same arglist arglist2 * then ( match unify lxp lxp2 subst with - * | Some (s', c) -> merge (s', c) (_unify_inner_case tail s') + * | Some (s', c) -> merge (s', c) (unify_inner_case tail s') * | None -> None) * else None) * | [] -> Some (subst, []) @@ -383,11 +383,11 @@ and is_same arglist arglist2 = * in (match lst with * | Some [] -> Some (subst, []) * | None -> None - * | Some l -> _unify_inner_case l subst) *) + * | Some l -> unify_inner_case l subst) *) (***** for Inductive *****) -(** for _unify_induct : unify the formal arg*) -(* and _unify_inner_induct lst subst : return_type = +(** for unify_induct : unify the formal arg*) +(* and unify_inner_induct lst subst : return_type = * let test ((a1, _, l1), (a2, _, l2)) subst : return_type = * if a1 = a2 then unify l1 l2 subst * else None @@ -402,16 +402,16 @@ and is_same arglist arglist2 = * ) None lst *) (** unify the SMap of list in Inductive *) -(* and _unify_induct_sub_list l1 l2 subst = +(* and unify_induct_sub_list l1 l2 subst = * let test l1 l2 subst = * let merge l1 l2 subst (s, c) = - * match (_unify_induct_sub_list l1 l2 subst) with + * match (unify_induct_sub_list l1 l2 subst) with * | Some (s1, c1) -> Some (s1, c1@c) * | None -> Some (s, c) * in - * let unify_zip lst t1 t2 = match _unify_inner_induct lst subst with + * let unify_zip lst t1 t2 = match unify_inner_induct lst subst with * | Some (s, c) -> merge l1 l2 subst (s, c) - * | None -> (_unify_induct_sub_list t1 t2 subst) + * | None -> (unify_induct_sub_list t1 t2 subst) * in * match l1, l2 with * | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> View it on GitLab: https://gitlab.com/monnier/typer/commit/76a477f15316f73fdf45ebe6b552b04299f… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/76a477f15316f73fdf45ebe6b552b04299f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Get rid of identifiers starting with underscore in *.ml
by Stefan 20 Sep '18

20 Sep '18

Stefan pushed to branch master at Stefan / Typer Commits: 32ef5ef1 by Stefan Monnier at 2018-09-21T02:10:39Z Get rid of identifiers starting with underscore in *.ml - - - - - 9 changed files: - src/REPL.ml - src/debruijn.ml - src/debug_util.ml - src/elab.ml - src/eval.ml - src/fmt.ml - src/lexer.ml - src/lexp.ml - tests/sexp_test.ml Changes: ===================================== src/REPL.ml ===================================== @@ -56,9 +56,6 @@ open Debruijn module OL = Opslexp module EL = Elexp -(* how to handle arrow keys ? *) -let _history = ref [] - let arg_batch = ref false let print_input_line i = @@ -136,27 +133,27 @@ let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = lexprs; (ldecls, lexprs), lctx -let ieval lexps rctx = +let ieval f str ectx rctx = + let ieval' lexps rctx = let (ldecls, lexprs) = lexps in let rctx = eval_decls_toplevel ldecls rctx in let vals = eval_all lexprs rctx false in - vals, rctx - -let _ieval f str ectx rctx = - let pres = (f str) in - let sxps = lex default_stt pres in - (* FIXME: This is too eager: it prevents one declaration from changing - * the grammar used in subsequent declarations. *) - let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in - - (* Different from usual typer *) - let pxps = ipexp_parse nods in - let lxps, ectx = ilexp_parse pxps ectx in - let elxps = ierase_type lxps in - let v, rctx = ieval elxps rctx in - v, ectx, rctx - -let _raw_eval f str ectx rctx = + vals, rctx in + + let pres = (f str) in + let sxps = lex default_stt pres in + (* FIXME: This is too eager: it prevents one declaration from changing + * the grammar used in subsequent declarations. *) + let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in + + (* Different from usual typer *) + let pxps = ipexp_parse nods in + let lxps, ectx = ilexp_parse pxps ectx in + let elxps = ierase_type lxps in + let v, rctx = ieval' elxps rctx in + v, ectx, rctx + +let raw_eval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in @@ -172,21 +169,21 @@ let _raw_eval f str ectx rctx = (* This is for consistency with ieval *) [], ectx, rctx -let ieval_string = _ieval prelex_string -let ieval_file = _ieval prelex_file +let ieval_string = ieval prelex_string +let ieval_file = ieval prelex_file -let eval_string = _raw_eval prelex_string -let eval_file = _raw_eval prelex_file +let eval_string = raw_eval prelex_string +let eval_file = raw_eval prelex_file -let _welcome_msg = +let welcome_msg = " Typer 0.0.0 - Interpreter - (c) 2016 %quit (%q) : leave REPL %help (%h) : print help " -let _help_msg = +let help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment %info (%i) : print elaboration environment @@ -220,11 +217,10 @@ let readfiles files (i, lctx, rctx) prt = let rec repl i clxp rctx = let repl = repl (i + 1) in let ipt = try read_input i with End_of_file -> "%quit" in - _history := ipt::!_history; match ipt with (* Check special keywords *) | "%quit" | "%q" -> () - | "%help" | "%h" -> (print_string _help_msg; repl clxp rctx) + | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) @@ -287,7 +283,7 @@ let main () = if not !arg_batch then (print_string (make_title " TYPER REPL "); - print_string _welcome_msg; + print_string welcome_msg; print_string (make_sep '-'); flush stdout); ===================================== src/debruijn.ml ===================================== @@ -135,47 +135,40 @@ let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int = get_size ectx - slen -(* internal definitions - * ---------------------------------- *) - -let _make_scope = SMap.empty -let _make_senv_type = (0, _make_scope) -let _make_myers = M.nil - -let _get_related_name (n : db_ridx) name map = - let r = Str.regexp (".*"^name^".*") in - let search r = SMap.fold (fun name idx ps -> - if (Str.string_match r name 0) then - (n - idx - 1)::ps - else - ps - ) map [] in - if ((String.sub name 0 1) = "_" || - (String.sub name ((String.length name) - 1) 1) = "_") && - ((String.length name) > 1) then - search r - else [] - (* Public methods: DO USE * ---------------------------------- *) +let empty_senv = (0, SMap.empty) +let empty_lctx = M.nil + let empty_elab_context : elab_context - = (Grammar.default_grammar, _make_senv_type, _make_myers, + = (Grammar.default_grammar, empty_senv, empty_lctx, (0, 0, ref SMap.empty)) (* senv_lookup caller were using Not_found exception *) -exception Senv_Lookup_Fail of (db_ridx list) +exception Senv_Lookup_Fail of (string list) let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds) -let get_related_name (name: string) (ctx: elab_context) = - let (_, (n, map), _, _) = ctx in - _get_related_name n name map - -(* return its current DeBruijn index *) +(* Return its current DeBruijn index. *) let senv_lookup (name: string) (ctx: elab_context): int = let (_, (n, map), _, _) = ctx in try n - (SMap.find name map) - 1 - with Not_found -> senv_lookup_fail (_get_related_name n name map) + with Not_found + -> let get_related_names (n : db_ridx) name map = + let r = Str.regexp (".*"^name^".*") in + let search r = SMap.fold (fun name _ names + -> if (Str.string_match r name 0) then + name::names + else + names) + map [] in + if ((String.sub name 0 1) = "_" || + (String.sub name ((String.length name) - 1) 1) = "_") && + ((String.length name) > 1) then + search r + else [] in + + senv_lookup_fail (get_related_names n name map) let lexp_ctx_cons (ctx : lexp_context) d v t = assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in @@ -237,16 +230,6 @@ let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx -(* Print related name raised by senv_lookup_fail *) -let print_related (xs : db_ridx list) (ctx: lexp_context) = - let tab = List.fold_left (fun str idx -> - let ((_, name), _, _) = env_lookup_by_index idx ctx in - match name with - | Some name -> (str ^ "\n\t" ^ name ^ "[" ^ (string_of_int idx) ^ "]") - | _ -> (str ^ "\n\t" ^ "[" ^ (string_of_int idx) ^ "]") - ) "" xs in - tab ^ "\n" - (* Print context *) let print_lexp_ctx_n (ctx : lexp_context) start = let n = (M.length ctx) - 1 in ===================================== src/debug_util.ml ===================================== @@ -85,47 +85,30 @@ let get_p_option name = highlight (use console color to display hints) *) -let _format_mode = ref false -let _ppctx = ref pretty_ppctx -let _format_dest = ref "" -let _write_file = ref false -let _typecheck = ref false +let format_mode = ref false +let ppctx = ref pretty_ppctx +let format_dest = ref "" +let write_file = ref false +let mod_ctx name v = let f ctx = ctx := SMap.add name v !ctx in + f ppctx; f debug_ppctx -let _set_print_pretty ctx v = - ctx := SMap.add "pretty" (Bool (v)) !ctx - -let _set_print_type ctx v = - ctx := SMap.add "print_type" (Bool (v)) !ctx - -let _set_print_index ctx v = - ctx := SMap.add "print_dbi" (Bool (v)) !ctx - -let _set_print_indent_size ctx v = - ctx := SMap.add "indent_size" (Int (v)) !ctx - -let _set_highlight ctx v = - ctx := SMap.add "color" (Bool (v))!ctx - -let mod_ctx f v = f _ppctx v; f debug_ppctx v - -let set_print_type v () = mod_ctx _set_print_type v -let set_print_index v () = mod_ctx _set_print_index v -let set_print_indent_size v = mod_ctx _set_print_indent_size v -let set_highlight v () = mod_ctx _set_highlight v -let set_print_pretty v () = mod_ctx _set_print_pretty v -let set_typecheck v () = _typecheck := v +let set_print_type v () = mod_ctx "print_type" (Bool v) +let set_print_index v () = mod_ctx "print_dbi" (Bool v) +let set_print_indent_size v = mod_ctx "indent_size" (Int v) +let set_highlight v () = mod_ctx "color" (Bool v) +let set_print_pretty v () = mod_ctx "pretty" (Bool v) let output_to_file str = - _write_file := true; - _format_dest := str; + write_file := true; + format_dest := str; set_highlight false () let arg_defs = [ (* format *) ("--format", - Arg.Unit (fun () -> _format_mode := true), " format a typer source code"); + Arg.Unit (fun () -> format_mode := true), " format a typer source code"); ("-fmt-type=on", Arg.Unit (set_print_type true), " Print type info"); ("-fmt-pretty=on", @@ -200,11 +183,11 @@ let format_source () = print_string (make_sep '-'); print_string "\n"; - let result = _lexp_str_decls (!_ppctx) (List.flatten lexps) in + let result = _lexp_str_decls (!ppctx) (List.flatten lexps) in - if (!_write_file) then ( - print_string (" " ^ " Writing output file: " ^ (!_format_dest) ^ "\n"); - let file = open_out (!_format_dest) in + if (!write_file) then ( + print_string (" " ^ " Writing output file: " ^ (!format_dest) ^ "\n"); + let file = open_out (!format_dest) in List.iter (fun str -> output_string file str) result; @@ -226,7 +209,7 @@ let main () = if arg_n == 1 then (Arg.usage (Arg.align arg_defs) usage) - else if (!_format_mode) then ( + else if (!format_mode) then ( format_source () ) else( @@ -320,7 +303,7 @@ let main () = let rctx = (try eval_decls_toplevel clean_lxp rctx; with e -> print_string reset; - print_rte_ctx (!_global_eval_ctx); + print_rte_ctx (!global_eval_ctx); print_eval_trace None; raise e) in print_string reset; ===================================== src/elab.ml ===================================== @@ -64,7 +64,7 @@ module EL = Elexp (* dummies *) let dloc = dummy_location -let _parsing_internals = ref false +let parsing_internals = ref false let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" @@ -107,9 +107,7 @@ let get_special_form name = (* Used for sform_load because sform are * added before default context's function. *) -let _sform_default_ectx = ref empty_elab_context -let _set_default_ectx ectx = - _sform_default_ectx := ectx +let sform_default_ectx = ref empty_elab_context (* The prefix `elab_check_` is used for functions which do internal checking * (i.e. errors signalled here correspond to internal errors rather than @@ -272,6 +270,12 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | _ -> sexp_error 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 + (newMetavar (ectx_to_lctx ctx) dummy_scope_level + (loc, Some "special-form-error") t, + Inferred t) + let elab_varref ctx (loc, name) = try let idx = senv_lookup name ctx in @@ -279,7 +283,14 @@ let elab_varref ctx (loc, name) let lxp = mkVar (id, idx) in let ltp = env_lookup_type ctx (id, idx) in (lxp, Inferred ltp) - with Senv_Lookup_Fail xs -> senv_lookup_fail xs + with Senv_Lookup_Fail xs -> + (let relateds = + if ((List.length xs) > 0) then + ". Did you mean: " ^ (String.concat " or " xs) ^" ?" + else "" in + sexp_error loc ("The variable: `" ^ name ^ + "` was not declared" ^ relateds); + sform_dummy_ret ctx loc) (* Turn metavar into plain vars after generalization. *) let rec meta_to_var ids o (e : lexp) = @@ -1177,12 +1188,6 @@ and get_attribute ctx loc largs = try Some (AttributeMap.find var map) with Not_found -> None -and sform_dummy_ret ctx loc = - let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in - (newMetavar (ectx_to_lctx ctx) dummy_scope_level - (loc, Some "special-form-error") t, - Inferred t) - and sform_get_attribute ctx loc (sargs : sexp list) ot = match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with | Some e -> (e, Lazy) @@ -1222,7 +1227,7 @@ let sform_decltype ctx loc sargs ot = let builtin_value_types : ltype option SMap.t ref = ref SMap.empty let sform_built_in ctx loc sargs ot = - match !_parsing_internals, sargs with + match !parsing_internals, sargs with | true, [String (_, name)] -> (match ot with | Some ltp @@ -1403,17 +1408,7 @@ let sform_identifier ctx loc sargs ot = match ot with Some _ -> Checked | None -> Lazy) (* Normal identifier. *) - | [Symbol id] - -> (try elab_varref ctx id - with Senv_Lookup_Fail xs -> - (let (loc, name) = id in - let relateds = - if ((List.length xs) > 0) then - ". Did you mean: " ^ (print_related xs (ectx_to_lctx ctx)) - else "" in - sexp_error loc ("The variable: `" ^ name ^ - "` was not declared" ^ relateds); - sform_dummy_ret ctx loc)) + | [Symbol id] -> elab_varref ctx id | [se] -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); @@ -1564,7 +1559,7 @@ let lexp_print_var_info ctx = print_string "\n") done -let _in_pervasive = ref true +let in_pervasive = ref true (* arguments : elab_context from where load is called, @@ -1584,16 +1579,16 @@ let sform_load usr_elctx loc sargs ot = (* read file as elab_context *) let ld_elctx = match sargs with - | [String (_,file_name)] -> if !_in_pervasive then + | [String (_,file_name)] -> if !in_pervasive then read_file file_name usr_elctx else - read_file file_name !_sform_default_ectx - | _ -> (error loc "argument to load should be one file name (String)"; !_sform_default_ectx) in + read_file file_name !sform_default_ectx + | _ -> (error loc "argument to load should be one file name (String)"; !sform_default_ectx) in (* get lexp_context *) let usr_lctx = ectx_to_lctx usr_elctx in let ld_lctx = ectx_to_lctx ld_elctx in - let dflt_lctx = ectx_to_lctx !_sform_default_ectx in + let dflt_lctx = ectx_to_lctx !sform_default_ectx in (* length of some lexp_context *) let usr_len = M.length usr_lctx in @@ -1602,12 +1597,12 @@ let sform_load usr_elctx loc sargs ot = (* create a tuple from context and shift it to user context * * also check if we are in pervasive in which case * * we want to load in the current context rather than the default *) - let tuple = if !_in_pervasive then + let tuple = if !in_pervasive then OL.ctx2tup usr_lctx ld_lctx else OL.ctx2tup dflt_lctx ld_lctx in - let tuple' = if !_in_pervasive then + let tuple' = if !in_pervasive then tuple else (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in @@ -1686,7 +1681,7 @@ let default_ectx (!BI.lmap) lctx in (* read base file *) - let lctx = dynamic_bind _parsing_internals true + let lctx = dynamic_bind parsing_internals true (fun () -> read_file (btl_folder ^ "/builtins.typer") lctx) in @@ -1699,10 +1694,10 @@ let default_ectx builtin_size := get_size lctx; - let lctx = dynamic_bind _in_pervasive true + let ectx = dynamic_bind in_pervasive true (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in - let _ = _set_default_ectx lctx in - lctx + let _ = sform_default_ectx := ectx in + ectx with (Stop_Compilation _) -> fatal dloc "compilation stopped in default context" let default_rctx = EV.from_ectx default_ectx @@ -1710,28 +1705,23 @@ let default_rctx = EV.from_ectx default_ectx (* String Parsing * --------------------------------------------------------- *) -(* Lexp helper *) -let _lexp_expr_str (str: string) (tenv: token_env) - (grm: grammar) (limit: string option) (ctx: elab_context) = - let pxps = _sexp_parse_str str tenv grm limit in - let lexps = lexp_parse_all pxps ctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) - lexps; - lexps - - -(* specialized version *) let lexp_expr_str str ctx = - try _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx - with Stop_Compilation s -> (print_string s; []) - -let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) = - let sdecls = _sexp_parse_str str tenv grm limit in - lexp_p_decls sdecls ctx + try let tenv = default_stt in + let grm = ectx_get_grammar ctx in + let limit = Some ";" in + let pxps = sexp_parse_str str tenv grm limit in + let lexps = lexp_parse_all pxps ctx in + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) + lexps; + lexps + with Stop_Compilation s -> (print_string s; []) -(* specialized version *) let lexp_decl_str str ctx = - try _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + try let tenv = default_stt in + let grm = ectx_get_grammar ctx in + let limit = Some ";" in + let sdecls = sexp_parse_str str tenv grm limit in + lexp_p_decls sdecls ctx with Stop_Compilation s -> (print_string s; ([],ctx)) @@ -1739,12 +1729,10 @@ let lexp_decl_str str ctx = * --------------------------------------------------------- *) (* Because we cant include Elab in eval.ml *) -let _eval_expr_str str lctx rctx silent = - let lxps = lexp_expr_str str lctx in - let elxps = List.map OL.erase_type lxps in - (EV.eval_all elxps rctx silent) - -let eval_expr_str str lctx rctx = try _eval_expr_str str lctx rctx false +let eval_expr_str str lctx rctx = + try let lxps = lexp_expr_str str lctx in + let elxps = List.map OL.erase_type lxps in + EV.eval_all elxps rctx false with Stop_Compilation s -> (print_string s; []) let eval_decl_str str lctx rctx = ===================================== src/eval.ml ===================================== @@ -52,9 +52,9 @@ module Prelexer = Prelexer (* prelex_string *) type eval_debug_info = elexp list * elexp list let dloc = dummy_location -let _global_eval_trace = ref ([], []) -let _global_eval_ctx = ref make_runtime_ctx -let _eval_max_recursion_depth = ref 23000 +let global_eval_trace = ref ([], []) +let global_eval_ctx = ref make_runtime_ctx +(* let eval_max_recursion_depth = ref 23000 *) let builtin_functions = ref (SMap.empty : ((location -> eval_debug_info @@ -68,14 +68,14 @@ let add_builtin_function name f arity = let append_eval_trace trace (expr : elexp) = let (a, b) = trace in let r = expr::a, b in - _global_eval_trace := r; r + global_eval_trace := r; r let append_typer_trace trace (expr : elexp) = let (a, b) = trace in let r = (a, expr::b) in - _global_eval_trace := r; r + global_eval_trace := r; r -let get_trace () = !_global_eval_trace +let get_trace () = !global_eval_trace let rec_depth trace = let (a, b) = trace in @@ -105,7 +105,7 @@ let debug_messages error_type loc message messages = error_type loc (msg ^ "\n") let root_string () = - let a, _ = !_global_eval_trace in + let a, _ = !global_eval_trace in match List.rev a with | [] -> "" | e::_ -> elexp_string e @@ -136,9 +136,9 @@ let tunit = Vcons ((dloc, "unit"), []) Another solution could be to define a function in elaboration step and then undefine it. The thing is elab_context may not exist at runtime so I must save it somewhere if the Elab.* function persist. *) -let _last_elab_context = ref empty_elab_context +let macro_monad_elab_context = ref empty_elab_context -let set_getenv (ectx : elab_context) = _last_elab_context := ectx +let set_getenv (ectx : elab_context) = macro_monad_elab_context := ectx (* * Builtins @@ -311,7 +311,7 @@ let parser_custom loc depth args_val = match args_val with let parser_newest loc depth args_val = match args_val with | [Vsexp (Block (_,toks,_))] -> - let grm = ectx_get_grammar (!_last_elab_context) in + let grm = ectx_get_grammar (!macro_monad_elab_context) in o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) | [s] -> (warning loc "Parser.newest do nothing without a Block"; s) | _ -> error loc "Parser.newest expects a Block as argument" @@ -372,13 +372,13 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type (* This creates an O(N^2) cost for deep recursion because rec_depth * uses `length` on the stack trace. *) - (* (if (rec_depth trace) > (!_eval_max_recursion_depth) then + (* (if (rec_depth trace) > (!eval_max_recursion_depth) then * fatal (elexp_location lxp) "Recursion Depth exceeded"); *) (* Save current trace in a global variable. If an error occur, we will be able to retrieve the most recent trace and context *) - _global_eval_ctx := ctx; - _global_eval_trace := trace; + global_eval_ctx := ctx; + global_eval_trace := trace; match lxp with (* Leafs *) @@ -625,7 +625,7 @@ and print_typer_trace' trace = let _ = List.iteri (fun i expr -> print_string " "; - Fmt._print_ct_tree i; print_string "+- "; + Fmt.print_ct_tree i; print_string "+- "; print_string ((elexp_string expr) ^ "\n")) trace in print_string (Fmt.make_sep '=') @@ -633,7 +633,7 @@ and print_typer_trace' trace = and print_typer_trace trace = match trace with | Some t -> print_typer_trace' t - | None -> let (a, b) = !_global_eval_trace in + | None -> let (a, b) = !global_eval_trace in print_typer_trace' b and print_trace title trace default = @@ -651,7 +651,7 @@ and print_trace title trace default = print_string (" [" ^ (loc_string (type_loc expr)) ^ "] "); (* Print call trace visualization *) - Fmt._print_ct_tree i; print_string "+- "; + Fmt.print_ct_tree i; print_string "+- "; (* Print element *) print_string ((type_name expr) ^ ": " ^ (type_string expr) ^ "\n") @@ -666,7 +666,7 @@ and print_trace title trace default = print_string (Fmt.make_sep '=') and print_eval_trace trace = - let (a, b) = !_global_eval_trace in + let (a, b) = !global_eval_trace in print_trace " EVAL TRACE " trace a let io_bind loc depth args_val = @@ -747,7 +747,7 @@ let gensym = let count = ref 0 in | _ -> error loc "gensym takes a Unit as argument") let getenv loc depth args_val = match args_val with - | [v] -> Vcommand (fun () -> Velabctx !_last_elab_context) + | [v] -> Vcommand (fun () -> Velabctx !macro_monad_elab_context) | _ -> error loc "getenv takes a single Unit as argument" let debug_doc loc depth args_val = match args_val with @@ -1053,7 +1053,7 @@ let eval lxp ctx = _eval lxp ctx ([], []) let debug_eval lxp ctx = try eval lxp ctx with e -> ( - print_rte_ctx (!_global_eval_ctx); + print_rte_ctx (!global_eval_ctx); print_eval_trace None; raise e) ===================================== src/fmt.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -117,7 +117,7 @@ let make_sep c = " " ^ (make_line c 76) ^ "\n" (* used to help visualize the call trace *) -let _print_ct_tree i = +let print_ct_tree i = let rec loop j = if j = i then () else match j with ===================================== src/lexer.ml ===================================== @@ -1,6 +1,6 @@ (* lexer.ml --- Second half of lexical analysis of Typer. -Copyright (C) 2011-2017 Free Software Foundation, Inc. +Copyright (C) 2011-2018 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -144,16 +144,11 @@ let lex tenv (pts : pretoken list) : sexp list = in gettokens pts bpos cpos (tok :: acc) in gettokens pts 0 0 [] -let _lex_str (str: string) tenv = +let lex_str (str: string) tenv = let pretoks = prelex_string str in lex tenv pretoks -let lex_str str = _lex_str str default_stt - -let _sexp_parse_str (str: string) tenv grm limit = - let toks = _lex_str str tenv in +let sexp_parse_str (str: string) tenv grm limit = + let toks = lex_str str tenv in sexp_parse_all_to_list grm toks limit -let sexp_parse_str str = - _sexp_parse_str str default_stt default_grammar (Some ";") - ===================================== src/lexp.ml ===================================== @@ -705,9 +705,11 @@ and _lexp_str ctx (exp : lexp) : string = let fun_call str = cyan ^ str ^ reset in let index idx = - let _index idx = if pp_dbi ctx then ("[" ^ (string_of_int idx) ^ "]") else "" in - let str = _index idx in if idx < 0 then (error str) else - (green ^ str ^ reset) in + let str = if pp_dbi ctx + then ("[" ^ (string_of_int idx) ^ "]") + else "" in + if idx < 0 then error str + else green ^ str ^ reset in let kind_str k = match k with | Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in ===================================== tests/sexp_test.ml ===================================== @@ -2,8 +2,12 @@ open Sexp open Lexer open Utest_lib +let sexp_parse_str dcode + = sexp_parse_str dcode Grammar.default_stt Grammar.default_grammar (Some ";") + let test_sexp_add dcode testfun = - add_test "SEXP" dcode (fun () -> testfun (sexp_parse_str dcode)) + add_test "SEXP" dcode + (fun () -> testfun (sexp_parse_str dcode)) let _ = test_sexp_add "lambda x -> x + x" (fun ret -> match ret with View it on GitLab: https://gitlab.com/monnier/typer/commit/32ef5ef1be1bb09c350aab9df82b49d3771… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/32ef5ef1be1bb09c350aab9df82b49d3771… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Avoid the <foo>_opt functions not available in older OCaml
by Stefan 18 Sep '18

18 Sep '18

Stefan pushed to branch master at Stefan / Typer Commits: a7bdf1e6 by Stefan Monnier at 2018-09-18T23:04:14Z Avoid the <foo>_opt functions not available in older OCaml * src/util.ml (smap_find_opt): New function to replace SMap.find_opt. * src/eval.ml (nth_ctor_arg.find_nth): Avoid List.nth_opt. (erasable_p2.is_erasable): Use List.exists. - - - - - 2 changed files: - src/eval.ml - src/util.ml Changes: ===================================== src/eval.ml ===================================== @@ -778,7 +778,7 @@ let constructor_p name ectx = with Senv_Lookup_Fail _ -> false let erasable_p name nth ectx = - let is_erasable ctors = match (SMap.find_opt name ctors) with + let is_erasable ctors = match (smap_find_opt name ctors) with | (Some args) -> if (nth < (List.length args) && nth >= 0) then ( match (List.nth args nth) with @@ -796,14 +796,14 @@ let erasable_p name nth ectx = with Senv_Lookup_Fail _ -> false let erasable_p2 t name ectx = - let is_erasable ctors = match (SMap.find_opt t ctors) with - | (Some args) -> - ( match (List.find_opt (fun (k, oname, _) -> - match oname with - | (_, Some n) -> (n = name && k = Aerasable) - | _ -> false) args) with - | Some _ -> true - | _ -> false ) + let is_erasable ctors = match (smap_find_opt t ctors) with + | Some args -> + (List.exists + (fun (k, oname, _) + -> match oname with + | (_, Some n) -> (n = name && k = Aerasable) + | _ -> false) + args) | _ -> false in try let idx = senv_lookup t ectx in match OL.lexp_whnf (mkVar ((dummy_location, Some t), idx)) @@ -816,12 +816,13 @@ let erasable_p2 t name ectx = with Senv_Lookup_Fail _ -> false let nth_ctor_arg name nth ectx = - let find_nth ctors = match (SMap.find_opt name ctors) with - | (Some args) -> - ( match (List.nth_opt args nth) with - | Some (_, (_, Some n), _) -> n - | _ -> "_" ) - | _ -> "_" in + let find_nth ctors = match (smap_find_opt name ctors) with + | Some args -> + (match (List.nth args nth) with + | (_, (_, Some n), _) -> n + | _ -> "_" + | exception (Failure _) -> "_" ) + | _ -> "_" in try let idx = senv_lookup name ectx in match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with @@ -837,7 +838,7 @@ let ctor_arg_pos name arg ectx = | [] -> None | (_, (_, Some x), _)::xs -> if x = arg then Some n else find_opt xs (n + 1) | _::xs -> find_opt xs (n + 1) in - let find_arg ctors = match (SMap.find_opt name ctors) with + let find_arg ctors = match (smap_find_opt name ctors) with | (Some args) -> ( match (find_opt args 0) with | None -> (-1) ===================================== src/util.ml ===================================== @@ -21,6 +21,10 @@ You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) module SMap = Map.Make (String) +(* Apparently OCaml-4.02 doesn't have find_opt and Debian stable still + * uses 4.02. *) +let smap_find_opt s m = try Some (SMap.find s m) with Not_found -> None + module IMap = Map.Make (struct type t = int let compare = compare end) type charpos = int View it on GitLab: https://gitlab.com/monnier/typer/commit/a7bdf1e671ce956a9780f7f3ca0b01678ce… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/a7bdf1e671ce956a9780f7f3ca0b01678ce… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 115 commits: New sform_load. Work in progress.
by Stefan 17 Sep '18

17 Sep '18

Stefan pushed to branch master at Stefan / Typer Commits: 2432cce1 by Jonathan Graveline at 2018-05-07T22:21:30Z New sform_load. Work in progress. - - - - - 4a0ed5b5 by Jonathan Graveline at 2018-05-07T22:37:20Z -lib nums to -pkg num - - - - - 905fc6f0 by Jonathan Graveline at 2018-05-10T01:08:36Z Modification and use of susp within sform_load - - - - - 5aa903a9 by Jonathan Graveline at 2018-05-10T01:12:36Z Modification of mktup and new function used in mktup - - - - - fc0bf4fa by Jonathan Graveline at 2018-05-10T15:15:35Z Removed 'reset_intra_ref' - - - - - 34d24f66 by Jonathan Graveline at 2018-05-10T15:20:01Z Correction in 'sform_load' and removed unused '_sform_default_rctx' - - - - - 83f93ecc by Jonathan Graveline at 2018-05-14T22:13:28Z First draft - - - - - f0d1072f by Jonathan Graveline at 2018-05-14T22:15:06Z First draft - - - - - a7dfcc1b by Jonathan Graveline at 2018-05-14T22:17:48Z Added some built-in function for Int, Float, String - - - - - 3b80038f by Jonathan Graveline at 2018-05-14T22:19:39Z Added some function for Int, Float, String - - - - - 00e86f25 by Jonathan Graveline at 2018-05-17T00:31:38Z Use of predefined function `shift` - - - - - 3d4d9623 by Jonathan Graveline at 2018-05-17T00:33:20Z Unfinished work on ctx2tup and mktup - - - - - d84820f3 by Jonathan Graveline at 2018-05-17T22:07:55Z >From master - - - - - bd6a3933 by Jonathan Graveline at 2018-05-17T22:09:07Z Replace elab.ml - - - - - cdc94f8b by Jonathan Graveline at 2018-05-17T22:10:37Z Change from master - - - - - 3da1ce59 by Jonathan Graveline at 2018-05-17T22:15:49Z push_susp reverse let definition (not sure if it was an error) - - - - - bfa8bdcf by Jonathan Graveline at 2018-05-17T22:16:53Z Change from master - - - - - 69659f54 by Jonathan Graveline at 2018-05-17T22:19:36Z ctx2tup from master and different shift for tuple values - - - - - a7ed6fa2 by Stefan Monnier at 2018-05-18T19:43:20Z Merge branch 'trunk' into graveline Also adds bool.typer and empty.typer for testing purposes, mostly. - - - - - aaa4c5dc by Stefan Monnier at 2018-05-18T21:10:47Z Add missing parts of last commit - - - - - 891026a4 by Jonathan Graveline at 2018-05-25T03:30:19Z Corrected String.sub String.concat - - - - - ae09719f by Jonathan Graveline at 2018-05-25T03:32:17Z Better name, more function - - - - - 26df3634 by Jonathan Graveline at 2018-05-25T03:33:03Z Better name - - - - - 7e8cd430 by Jonathan Graveline at 2018-05-25T03:34:45Z do macro, first draft - - - - - 00a41105 by Jonathan Graveline at 2018-05-26T15:17:41Z Syntax now using ";" and better use of IO_bind - - - - - eaca195c by Jonathan Graveline at 2018-05-26T15:23:04Z Sexp_print for debugging - - - - - 588c02a6 by Jonathan Graveline at 2018-05-26T15:23:50Z Sexp_print for debugging - - - - - df88126a by Jonathan Graveline at 2018-05-26T21:05:59Z Renamed Sexp_print to Sexp_debug_print - - - - - 34da1bba by Jonathan Graveline at 2018-05-26T21:08:02Z Renamed Sexp_print to Sexp_debug_print - - - - - 0259aaff by Jonathan Graveline at 2018-05-26T21:10:19Z cleanup - - - - - 6045d6aa by Jonathan Graveline at 2018-05-30T20:22:24Z Added make_block and Sexp_dispatch for Block - - - - - c096b10e by Jonathan Graveline at 2018-05-30T20:24:01Z New Sexp_block - - - - - 338fd242 by Jonathan Graveline at 2018-05-30T20:25:26Z New Sexp_block - - - - - 66f64c95 by Jonathan Graveline at 2018-05-30T20:27:21Z action now use block - - - - - fe78c2da by Jonathan Graveline at 2018-05-31T18:55:38Z Change to sexp_dispatch and added parse_default - - - - - a8779758 by Jonathan Graveline at 2018-05-31T18:56:37Z Added Parser_default - - - - - bd3aa605 by Jonathan Graveline at 2018-05-31T18:57:59Z Added Parser_default - - - - - 7884d73f by Jonathan Graveline at 2018-06-13T19:49:52Z Renamed Parse_default to Parser_default, Corrected String.sub argument count - - - - - b46c9421 by Jonathan Graveline at 2018-06-13T19:55:28Z Upload case.typer - - - - - 17fce738 by Jonathan Graveline at 2018-06-13T20:02:46Z Added Int->String - - - - - d3100d5e by Jonathan Graveline at 2018-06-14T02:25:03Z Added Ref as a built in type. - - - - - 1c406196 by Jonathan Graveline at 2018-06-14T02:26:12Z Added Vref as a value_type - - - - - 6fbec92e by Jonathan Graveline at 2018-06-14T02:27:39Z Added built in function Ref_make, Ref_read, Ref_write - - - - - ee004b1c by Jonathan Graveline at 2018-06-14T02:28:53Z Added Ref_make, Ref_read, Ref_write - - - - - 2669433a by Jonathan Graveline at 2018-06-14T03:23:09Z Ref_write affect when command is run - - - - - 56e7649d by Jonathan Graveline at 2018-06-15T22:47:16Z New built-in gensym, changed macro signature to return IO Sexp - - - - - 203222b1 by Stefan Monnier at 2018-06-21T15:06:32Z Merge branch 'trunk' into graveline - - - - - abda0e39 by Jonathan Graveline at 2018-06-21T16:28:58Z macro do in pervasive; test for macro do; some change on macro case - - - - - eb8acb50 by Jonathan Graveline at 2018-06-21T16:30:52Z Merge branch 'graveline' of https://gitlab.com/monnier/typer into graveline - - - - - cec64f4a by Jonathan Graveline at 2018-06-21T16:57:44Z After last merge symbol "_" in macro do need to be declared - - - - - a8a77d78 by Jonathan Graveline at 2018-06-22T20:45:23Z New type Elab_Context and functions Elab_getenv, Elab_isbound, Elab_isconstructor - - - - - 46381fd8 by Jonathan Graveline at 2018-06-25T18:11:36Z samples/list_n.typer, there must be some mistakes - - - - - 246ba428 by Jonathan Graveline at 2018-06-25T21:22:00Z macro "case" now use "do" and "Elab_isconstructor"; added tests/case_test.ml - - - - - 9e9a8e89 by Jonathan Graveline at 2018-06-27T17:57:09Z Correction of macro "do", dflt-sym need a symbol and not just "_" - - - - - 4c682c42 by Jonathan Graveline at 2018-06-28T21:57:57Z New type and value for Array with some functions - - - - - af4ba9f6 by Jonathan Graveline at 2018-06-29T20:41:33Z Correction of Array functions and simplification - - - - - 9156b075 by Jonathan Graveline at 2018-07-02T21:08:22Z New data structure "Table" (some kind of tree) (work in progress) - - - - - 124601a5 by Jonathan Graveline at 2018-07-03T22:19:55Z Corrected indentation in case.typer; table.typer rewriten with unit tests/table_test.ml - - - - - e98cf539 by Jonathan Graveline at 2018-07-05T19:03:15Z Using rlwrap to add auto-completion and history - - - - - a0f050f7 by Jonathan Graveline at 2018-07-05T19:40:51Z Stop compiler on first error - - - - - ece77ad2 by Jonathan Graveline at 2018-07-05T19:43:43Z Don't try to print value if there's none - - - - - 72bfc552 by Jonathan Graveline at 2018-07-05T19:49:54Z Added .directory to .gitignore - - - - - f3667866 by Jonathan Graveline at 2018-07-06T03:03:52Z Print similar name with error message when a variable isn't found - - - - - a89aa4f4 by Jonathan Graveline at 2018-07-11T19:39:36Z Compile samples/* only once in some unit tests; New balanced bst (bbst.typer) - - - - - 81821861 by Jonathan Graveline at 2018-07-11T19:57:31Z Corrected macro type in default attribute and eval_test.ml - - - - - c7d2bbfe by Stefan Monnier at 2018-07-18T21:01:03Z Merge branch 'trunk' into graveline - - - - - 33a23595 by Stefan Monnier at 2018-07-21T21:29:49Z Make isconstructor pure and boolean; and ignore names in lctx * btl/builtins.typer (Elab_isbound, Elab_isconstructor): Make pure and Bool. * samples/case.typer (is_ctor): Adjust accordingly. * src/debruijn.ml (lctx_olookup, lctx_olookup_type) (lctx_olookup_value): Delete. * src/elab.ml (elab_p_id): Not recursive. (check_case): Use Eval.constructor_p. * src/eval.ml (sexp_dispatch): Remove dead code. (is_bound): Use senv_lookup. (constructor_p): New function, extracted from Elab.check_case. (is_constructor): Use it. * tests/elabctx_test.ml (v2o_bool): New function. ("Elab_isbound", "Elab_isconstructor"): Adjust to new types of isbound and isconstructor. Add test case for alias to a constructor. - - - - - c08685e0 by Stefan Monnier at 2018-07-24T00:57:53Z Merge branch 'trunk' into graveline - - - - - ff69f5cf by Jonathan Graveline at 2018-07-24T01:55:12Z more List functions - - - - - 61fc705d by Jonathan Graveline at 2018-07-24T02:18:36Z progression on the `case` macro - - - - - 9f8cd189 by Stefan Monnier at 2018-07-24T02:19:28Z Merge branch 'trunk' into graveline - - - - - e3e9599b by Jonathan Graveline at 2018-07-24T02:22:13Z Merge branch 'graveline' of https://gitlab.com/monnier/typer into graveline - - - - - c8fad518 by Jonathan Graveline at 2018-07-25T00:08:43Z update on macro `case` - - - - - 450e86fa by Jonathan Graveline at 2018-07-25T20:28:33Z *samples/list.typer, more consistent function's type declaration - - - - - 5d4e2008 by Jonathan Graveline at 2018-07-25T20:35:26Z Stop compilation on error in `check` and elab functions Also store all errors and warnings for future use - - - - - 2b2bac1b by Jonathan Graveline at 2018-07-25T20:40:47Z Print related name only when the name has underscore - - - - - 26e9e4c2 by Jonathan Graveline at 2018-07-25T21:25:59Z Add an exception for sform_load's context when in pervasive.typer - - - - - a188451f by Jonathan Graveline at 2018-07-26T02:52:06Z Merge branch 'master' of https://gitlab.com/monnier/typer into graveline - - - - - be29169e by Jonathan Graveline at 2018-07-26T04:45:56Z Change lost somewhere in previous commit *samples/case2.typer *samples/do.typer *samples/list.typer - - - - - b0b911ec by Jonathan Graveline at 2018-07-26T04:55:06Z Many change to use `load` in pervasive.typer and move some definition Temporary workaround for tuple access in macro `.` renamed: samples/case2.typer -> btl/case.typer renamed: samples/do.typer -> btl/do.typer renamed: samples/list.typer -> btl/list.typer modified: btl/pervasive.typer deleted: samples/case.typer modified: src/opslexp.ml modified: tests/array_test.ml modified: tests/case_test.ml - - - - - 572470f8 by Jonathan Graveline at 2018-07-27T05:30:17Z `plain-let` (not recursive nor sequential) without grammar yet - - - - - 84261c57 by Jonathan Graveline at 2018-07-27T06:20:33Z keep count of `insert`/`remove` for faster `length` calculation - - - - - 4d149272 by Jonathan Graveline at 2018-07-27T06:22:26Z use `if ... then ... else ...` syntax where appropriate - - - - - 0ab2e43c by Jonathan Graveline at 2018-07-27T12:39:23Z Minimal built-in functions for unit tests in Typer - - - - - 14f1aafb by Jonathan Graveline at 2018-07-30T20:57:35Z Correction of some unit test primitive (put action in `Vcommand` and set to correct type) New primitive Integer->String (useful with Sexp_dispatch) - - - - - e1917e8b by Jonathan Graveline at 2018-07-30T21:05:01Z Don't print related name with the single character symbol "_" Added boolean operation from samples/bool.typer to pervasive.typer - - - - - 35f6bc54 by Jonathan Graveline at 2018-07-30T21:09:57Z *polyfun.typer: Implicit `case` at function definition level (macro not working if at top-level, but working in `let`) - - - - - a9f1a0dd by Jonathan Graveline at 2018-07-30T21:13:49Z macro for tuple creation and access (more to come) (`_,_` not working yet, temporarily using `_:_`) - - - - - b27dd3ea by Jonathan Graveline at 2018-07-31T17:28:32Z `plain-let` with grammar setup - - - - - 5c4ba829 by Jonathan Graveline at 2018-07-31T22:47:13Z Add function syntax support in `plain-let` - - - - - 4191f41f by Jonathan Graveline at 2018-08-01T02:22:54Z new built-in function `Parser_*` and use it in do.typer - - - - - 38b621d2 by Jonathan Graveline at 2018-08-01T16:12:25Z use `if...then...else...` syntax where appropriate udict and odict (from table and bbst) for convenience - - - - - 28006ea4 by Jonathan Graveline at 2018-08-01T17:33:28Z define operator `<-`, use it in do.typer and tuple.typer tuple now working with `,` (needed escape: `_\,_`) - - - - - b3519661 by Jonathan Graveline at 2018-08-02T19:38:52Z macro `case` should now work on tuple use `sexp_name` in `Sexp_debug_print` change in `is_binary_op` (I think it was a bug) tuple constructor now has a `gensym` name - - - - - d63644ec by Jonathan Graveline at 2018-08-03T19:12:23Z samples/tuple_test.typer: Test written in Typer for tuple Changed warning, info and fatal output in unit test primitive - - - - - bedf45c5 by Jonathan Graveline at 2018-08-03T20:45:49Z Correction in polyfun.typer; unit test in Typer for macro `_|_` - - - - - afe315b8 by Jonathan Graveline at 2018-08-06T15:52:15Z `Env.value_equal`: using structural equality when comparing constructor name - - - - - ffe322a7 by Jonathan Graveline at 2018-08-06T16:26:56Z Rewrote unit test for `Bbst` and `Table` in Typer code - - - - - e9a91eba by Jonathan Graveline at 2018-08-06T23:14:53Z An attempt to fix a problem with `load_` - - - - - f4c0cfb7 by Jonathan Graveline at 2018-08-07T16:42:57Z `tunit` in eval.ml is now `unit` rather than `()` - - - - - 3d4035ac by Jonathan Graveline at 2018-08-07T18:25:12Z Correction of bounds check in `array_get` samples/array_test.typer: Unit test for `Array` rewritten in Typer - - - - - f9d7cefc by Jonathan Graveline at 2018-08-09T17:30:04Z New primitive for inductive type info Temporary fix of macro `case` to pass unit tests Commented incorrect `Metavar` case in `conv_p` - - - - - ab2c6d9b by Jonathan Graveline at 2018-08-10T16:59:38Z New macro `Test_file` not working on multiple call Unit test rewritten in Typer for `case`, `do`, `Elab_Context` Correction of primitive `Elab.is-arg-erasable` - - - - - a8b733a6 by Jonathan Graveline at 2018-08-13T17:05:25Z Macro `Test_file` now return a command: `exec-test` from loaded file File samples/batch_test.typer now working Most unit test in Typer adapted for `Test_file` and batch_test.typer - - - - - c11bb8a4 by Jonathan Graveline at 2018-08-13T20:52:32Z New complementary primitive: `Elab_arg-pos` Improved macro `case` on explicit field pattern - - - - - cf4448de by Jonathan Graveline at 2018-08-20T21:58:13Z Macro `Tuple` returning a type Comment for `Test_file` in pervasive.typer - - - - - 3981eea1 by Jonathan Graveline at 2018-08-22T23:29:34Z New character '@' introducing docstring New primitive `Elab.debug-doc` mostly for testing docstring Replaced `load_` by `load` - - - - - 451ead23 by Jonathan Graveline at 2018-08-23T20:56:11Z Documentation, work in progress Some more tests in samples/case_test.typer - - - - - caa73195 by Jonathan Graveline at 2018-08-24T18:33:07Z Revised comments, trying to be more clear - - - - - cd2381bc by Jonathan Graveline at 2018-08-24T19:46:34Z New unit test for `plain-let` Revision of bbst.typer and table.typer - - - - - 6ef13572 by Jonathan Graveline at 2018-08-27T19:01:33Z More comments in samples/myers.typer Basic unit tests on Myers list in samples/myers_test.typer - - - - - 13cf5ad0 by Jonathan Graveline at 2018-08-29T20:49:39Z Revised comments; commented more function in btl/builtins.typer Rewrite tuple body; commented tuple unit tests (but they should work) - - - - - a1747386 by Jonathan Graveline at 2018-08-30T20:16:35Z Removed "debug output" in `Ref_make` from src/eval.ml samples/decltype.typer: another version of `decltype` implemented in Typer samples/math.typer: a toy math library - - - - - 9fd7015b by Jonathan Graveline at 2018-08-31T21:25:07Z Revised comments and documentation from btl/ and samples/ - - - - - 2269559a by Stefan Monnier at 2018-09-17T21:21:16Z Merge remote-tracking branch 'remotes/gitlab/graveline' into trunk - - - - - 24 changed files: - .gitignore - GNUmakefile - btl/builtins.typer - + btl/case.typer - + btl/do.typer - + btl/list.typer - btl/pervasive.typer - + btl/plain-let.typer - + btl/polyfun.typer - + btl/tuple.typer - + samples/array_test.typer - + samples/batch_test.typer - + samples/bbst.typer - + samples/bbst_test.typer - + samples/bool.typer - − samples/bugs.typer - + samples/case_test.typer - + samples/decltype.typer - + samples/do_test.typer - + samples/elabctx_test.typer - samples/empty.typer - samples/error.typer - + samples/list_n.typer - + samples/math.typer The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/compare/90f98f1062c2db34c6815fbb8885ec364b… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/90f98f1062c2db34c6815fbb8885ec364b… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/eval.ml: Add trivial comment
by Stefan 17 Sep '18

17 Sep '18

Stefan pushed to branch master at Stefan / Typer Commits: 90f98f10 by Stefan Monnier at 2018-09-17T19:29:27Z * src/eval.ml: Add trivial comment - - - - - 1 changed file: - src/eval.ml Changes: ===================================== src/eval.ml ===================================== @@ -310,13 +310,13 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type (* Nodes *) (* ---------------- *) - | Let(_, decls, inst) -> - let nctx = _eval_decls decls ctx trace in + | Let(_, decls, inst) + -> let nctx = _eval_decls decls ctx trace in eval inst nctx (* Function call *) - | Call (f, args) -> - eval_call (elexp_location f) f trace + | Call (f, args) + -> eval_call (elexp_location f) f trace (_eval f ctx trace) (List.map (fun e -> _eval e ctx trace) args) @@ -332,6 +332,10 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type * or somehow recover a lexp-ctx from the runtime-ctx (maybe * with extra info that `Type` could carry), * or find another trick. + * + * We could replace erasable arguments (like t above) with a Metavar, + * but the other issue of converting Values back to Lexps remains! + * * Hence, the `e` carried by `Vtype` is just indicative and not * something we can use. *) | Type e -> Vtype e View it on GitLab: https://gitlab.com/monnier/typer/commit/90f98f1062c2db34c6815fbb8885ec364be… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/90f98f1062c2db34c6815fbb8885ec364be… You're receiving this email because of your account on gitlab.com.

1 0

***SPAM*** [Git][monnier/typer][master] 48 commits: Added draft file presenting the theory behind Typer plus the file's dependencies
by Stefan 17 Sep '18

17 Sep '18

Stefan pushed to branch master at Stefan / Typer Commits: 27f86f61 by nbos at 2018-07-07T04:41:05Z Added draft file presenting the theory behind Typer plus the file's dependencies - - - - - 1e7b80b3 by nbos at 2018-07-09T20:19:32Z Prettified boxes; fixed PTS definition; added impredicative R; gave explanations on E- vs R- rules - - - - - 0881ba77 by nbos at 2018-07-09T21:45:50Z New macro - - - - - a05b2179 by nbos at 2018-07-09T21:46:50Z Started CCw to Typer translation - - - - - 9887dcff by nbos at 2018-07-10T18:53:09Z Corrected typos; moved some rules and renamed rule groups; fixed boxes around figures - - - - - 2110c130 by nbos at 2018-07-12T01:09:45Z Changed some notation - - - - - 488c0fde by nbos at 2018-07-12T03:01:36Z Removed pmb style - - - - - 9cbcda53 by nbos at 2018-07-17T15:56:58Z Modified TypeLevel definition and notation; described CCw; finished skeleton of proof - - - - - 6125b349 by nbos at 2018-07-17T17:42:40Z Separated Case 1 of proof into two; introducing Erasable constructor - - - - - 16b5fb2e by nbos at 2018-07-24T07:13:51Z Changed notation for CCw; added abbrevs for keyworkds (sans serif) - - - - - 5a751a66 by nbos at 2018-07-24T07:18:02Z Finished translation from CCw; changed presentation of CCw to be based on CC rather than ECC - - - - - 7d665323 by nbos at 2018-07-24T08:18:21Z Contextualized notation for Typer's compound terms and CCw - - - - - 26b5c9c8 by nbos at 2018-07-27T02:27:37Z Cleaned text; fixed translation to account for new rules of CCw - - - - - 25024193 by nbos at 2018-07-30T08:11:16Z New commands; removed unecesary math layer in sans keywords - - - - - 618d6ae9 by nbos at 2018-07-30T08:15:13Z Restructured whole proof of extention of CCω - - - - - b2fdff75 by nbos at 2018-07-30T09:59:21Z Added room for special case E-Lam - - - - - da1e981a by nbos at 2018-07-31T12:36:38Z Add a few theorem-style environments; clean some unused commands - - - - - 42ee60bb by nbos at 2018-07-31T12:39:09Z Begin Lemma 3.1; clean translation format; add theorem-style environments where appropriate - - - - - 2eb3b210 by nbos at 2018-07-31T15:55:21Z Introduce translation operator; reduce number of assumptions in sec.3 and prove new lemmas instead - - - - - ce6c1ca9 by nbos at 2018-08-03T19:45:52Z Define translation operator; stage the proof to be bidirectional; replace correspondance between PTS's with lemmas of injective maps between sorts and axioms of CCw and Typer - - - - - 69c04c10 by nbos at 2018-08-03T20:12:04Z Prove lemma 3.3 + 3.4 - - - - - 1599bd1c by nbos at 2018-08-03T20:25:50Z Prove lemma 3.5 - - - - - 54fcd9b8 by nbos at 2018-08-06T23:33:22Z Add labels and refs to figures in text - - - - - cd8d5f59 by nbos at 2018-08-07T09:09:37Z Add labels and refs to equations; add (Prop, Prop, Prop) axiom to Rcc; define translation on applications; prove (most of) lemma 3.6 - - - - - 7f3a4233 by nbos at 2018-08-08T07:49:41Z Finish proof of lemma 3.6; make it a case analysis on [M]* rather than [M]; make M -> M* definition a figure - - - - - 58024bcd by nbos at 2018-08-08T10:40:51Z Enhance layout of translation section; define soundness/completeness of translation; label lemmas; clean A-equiv lemma; add R-equiv lemma; complete completeness (=>) proof - - - - - ab7b5700 by nbos at 2018-08-09T13:54:04Z Clarified lem:S-equiv; boxed definition of translation in fig:[] - - - - - af784c9b by nbos at 2018-08-09T14:45:56Z Fix lemma lem:A-equiv - - - - - d5a33c33 by nbos at 2018-08-09T15:27:31Z Add feedback FIXME's - - - - - 769d8856 by nbos at 2018-08-10T02:28:06Z Fix and streamline lem:S-equiv and lem:A-equiv; split first part of lem:R-equiv into lem:Re-equiv - - - - - e9edd7ec by nbos at 2018-08-10T03:40:34Z Put theorems and lemmas on the same counter - - - - - 9b526a75 by nbos at 2018-08-14T04:21:58Z Reduce margin; avoid undefined use of ∪ with CCω sorts; make eq:corresctness-translation a theorem; finish proof of lem:R-equiv; start proof of lem:Re-equiv - - - - - 37d2e51b by nbos at 2018-08-14T06:02:11Z Fix references to lemmas lem:S- lem:A- lem:R- and lem:Re-equiv in proof - - - - - 998d77aa by nbos at 2018-08-14T06:22:00Z Complete proof of lem:Re-equiv - - - - - c42b26d7 by nbos at 2018-08-14T12:19:21Z Move lem:E-Lam-FV to before completeness proof; generalize lem:E-Lam-FV out of only translations - - - - - e7c3aa6b by nbos at 2018-08-14T15:28:52Z Remove custom font - - - - - 74dcbd9d by nbos at 2018-08-14T15:40:30Z Add title and authors; setup cases for soundness of translation proof - - - - - 1ee31754 by nbos at 2018-08-16T18:02:55Z Populate soundness proof with typing rules; rephrase some sentences to be impersonal; add substitution in definition of translation - - - - - 5bfe76e4 by nbos at 2018-08-17T21:55:44Z Add 'pack' as an example - - - - - 70fac346 by nbos at 2018-08-22T09:14:43Z Fix part of lem:FV-E-Lam; expand on example Pack - - - - - c52700fd by nbos at 2018-08-22T21:29:36Z Finish fix lem:FV-E-Lam - - - - - 57ed864b by nbos at 2018-08-22T22:36:04Z Restructure sections and figures; correct some awkward phrasing - - - - - 89aecbb1 by nbos at 2018-08-30T09:05:45Z Rewrite a valid proof of lem:E-Lam-FV; start proof of soundness of translation; expand on guarded by destructors predicate D - - - - - e25ebfb7 by nbos at 2018-08-30T19:00:52Z Review of completeness of translation proof - - - - - d374fc40 by nbos at 2018-09-01T09:22:40Z Rephrase parts of completeness of translation proof; finish soundness of translation proof; finish example - - - - - 576bfd64 by nbos at 2018-09-02T04:26:20Z Add of sans-serif keyword command - - - - - b15652de by nbos at 2018-09-02T04:29:15Z Restructure some sentences; add recursive definition of free variables; define beta- and iota-reductions; add transitivity to congruence relation - - - - - 306196bf by Stefan Monnier at 2018-09-17T17:26:03Z Merge remote-tracking branch 'remotes/gitlab/bosn' into trunk - - - - - 3 changed files: - + doc/formal/commands.tex - + doc/formal/typer_theory.bib - + doc/formal/typer_theory.tex Changes: ===================================== doc/formal/commands.tex ===================================== @@ -0,0 +1,88 @@ +%% Theorems +\newtheorem{theorem}{Theorem}[section] +\newtheorem{lemma}[theorem]{Lemma} + +\theoremstyle{definition} +\newtheorem{definition}{Definition}[section] + +\theoremstyle{definition} +\newtheorem{remark}{Remark}[section] + + +%% Defined/Free variables +\newcommand{\Dom}[1]{\textsf{Dom}(#1)} +\newcommand{\dv}[1]{\textsf{DV}(#1)} +\newcommand{\fv}[1]{\textsf{FV}(#1)} + +%% Sans +\newcommand{\Ind}{\textsf{Ind}} +\newcommand{\Constr}{\textsf{Constr}} +\newcommand{\Case}{\textsf{Case}} +\newcommand{\of}{\textsf{of}} +\newcommand{\Elim}{\textsf{Elim}} +\newcommand{\Fix}{\textsf{Fix}} +\newcommand{\Letrec}{\textsf{Letrec}} +\newcommand{\Let}{\textsf{Let}} +\newcommand{\In}{\textsf{in}} + +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\TypeLevel}{\textsf{TypeLevel}} +\newcommand{\SortL}{\textsf{SortL}} +\newcommand{\Sort}{\textsf{Sort}} +\newcommand{\z}{\textsf{z}} +\newcommand{\s}{\textsf{s}} + +\newcommand{\Sortw}{\ensuremath{\mathsf{Sort}_\omega}} + +% Bolds +\newcommand{\todo}{\textbf{ TODO }} + +% Caligraphics +\renewcommand{\S}{\mathcal{S}} +\newcommand{\A}{\mathcal{A}} +\newcommand{\R}{\mathcal{R}} +\newcommand{\U}{\mathcal{U}} +\newcommand{\D}{\mathcal{D}} +\newcommand{\V}{\mathcal{V}} + +%% Abbrevs +\let\~\vdash +\let\Ga\Gamma +\let\La\Lambda +\let\la\lambda +\let\<\langle +\let\>\rangle +\let\l\ell + +% Abstractions +\newlength{\ProdSpace} +\setlength{\ProdSpace}{-2.5pt} +\newcommand{\explicit}{\hspace{\ProdSpace}\rightarrow\hspace{\ProdSpace}} +\newcommand{\implicit}{\hspace{\ProdSpace}\Rightarrow\hspace{\ProdSpace}} +\newcommand{\erasable}{\hspace{\ProdSpace}\Rrightarrow\hspace{\ProdSpace}} + +% Misc +\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center} + \bf \underline{#1} + \end{center}} + +\renewcommand{\tag}[1]{\textsc{(#1)}} +\newcommand{\rew}[1]{\ensuremath{\llbracket #1 \rrbracket}} + +\newcommand{\emptyctx}{% + \mathchoice{\raisebox{1pt}{$\displaystyle\cdot$}} + {\raisebox{1pt}{$\cdot$}} + {\raisebox{0.5pt}{$\scriptstyle\cdot$}} + {\raisebox{0.2pt}{$\scriptscriptstyle\cdot$}}} + +\newcommand{\ap}{\raisebox{1.7pt}{\scalebox{0.8}{$|$}}} +\newcommand{\app}{\raisebox{1.7pt}{\scalebox{0.8}{$||$}}} +\newcommand{\appp}{\raisebox{1.7pt}{\scalebox{0.8}{$|||$}}} + +\renewcommand{\:}{\hspace{-3pt}:\hspace{-3pt}} +\newcommand{\nottype}{/\hspace{-7pt}:} + +\newcommand{\CC}{\text{CC$\omega$}} +\newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}} +\newcommand{\Tdash}{\vdash_{\hspace{-2pt}_{T}}} \ No newline at end of file ===================================== doc/formal/typer_theory.bib ===================================== @@ -0,0 +1,59 @@ +@inproceedings{gimenez, + title={Codifying guarded definitions with recursive schemes}, + author={Gim{\'e}nez, Eduarde}, + booktitle={International Workshop on Types for Proofs and Programs}, + pages={39--59}, + year={1994}, + organization={Springer} +} +@inproceedings{bruno, + title={The implicit calculus of constructions as a programming language with dependent types}, + author={Barras, Bruno and Bernardo, Bruno}, + booktitle={International Conference on Foundations of Software Science and Computational Structures}, + pages={365--379}, + year={2008}, + organization={Springer} +} +@article{barendregt, + title={Introduction to generalized type systems}, + author={Barendregt, Henk}, + journal={Journal of functional programming}, + volume={1}, + number={2}, + pages={125--154}, + year={1991}, + publisher={Cambridge University Press} +} +@article{miquel, + title={Le Calcul des Constructions implicite: syntaxe et s{\'e}mantique}, + author={Miquel, Alexandre}, + journal={These de doctorat, Universit{\'e} Paris}, + volume={7}, + year={2001} +} +@article{CC, + author = {Coquand, Thierry and Huet, Gerard}, + title = {The Calculus of Constructions}, + journal = {Inf. Comput.}, + issue_date = {February/March 1988}, + volume = {76}, + number = {2-3}, + month = feb, + year = {1988}, + issn = {0890-5401}, + pages = {95--120}, + numpages = {26}, + url = {http://dx.doi.org/10.1016/0890-5401(88)90005-3}, + doi = {10.1016/0890-5401(88)90005-3}, + acmid = {47725}, + publisher = {Academic Press, Inc.}, + address = {Duluth, MN, USA}, +} +@inproceedings{luo, + title={ECC, an extended calculus of constructions}, + author={Luo, Zhaohui}, + booktitle={Logic in Computer Science, 1989. LICS'89, Proceedings., Fourth Annual Symposium on}, + pages={386--395}, + year={1989}, + organization={IEEE} +} ===================================== doc/formal/typer_theory.tex ===================================== @@ -0,0 +1,1110 @@ +\documentclass[10pt]{article} +\usepackage[a4paper,margin=35mm,footskip=10mm]{geometry} + +\usepackage{amsmath,amsthm,amssymb,mathtools,stmaryrd} +\usepackage{mathpartir,mdframed,empheq} +\usepackage{parskip} + +\title{\textbf{Exposition of Typer's Type Theory}} +\author{ + \begin{tabular}{c} Nathaniel Bos \\ McGill University \\ \texttt{nathaniel.bos(a)mail.mcgill.ca} \end{tabular} + ~~~~~~ + \begin{tabular}{c} Stefan Monnier \\ DIRO - Universit\'e de Montr\'eal \\ \texttt{monnier(a)iro.umontreal.ca} \end{tabular} +} +\date{} +\input{commands} +\begin{document} + +\maketitle + +We here formalize the Typer language and prove some of its properties. + +\section{Typer's Type Theory} +The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructions (CC) \cite{CC} enriched with the following features: + +\begin{itemize} + \renewcommand{\labelitemi}{$-$} + \setlength\itemsep{-3pt} +\item An infinite hierarchy of type universes inspired by Luo's Extended Calculus of Constructions (ECC) \cite{luo} without cumulativity; +\item Product rules that allow for both predicative and impredicative arguments and abstractions in every universe; +\item Universe polymorphism allowing the parametrization of type universes; +\item Erasure of propositional arguments with decidable type checking from Barras and Bernardo's variant of Miquel's Implicit Calculus of Constructions (ICC) \cite{bruno}\cite{miquel}; +\item Inductive definitions as presented by Gim\'enez in \cite{gimenez}. +\end{itemize} + +\subsection{Universes and Universe Polymorphism} +\begin{figure} + \label{fig:PTS} + \begin{empheq}[box=\fbox]{align*} + \hspace{15mm} & \ & \ & \hspace{7mm} \\ + \S = \{ & \SortL;\ \Sortw;\ \Type\ \l\} &\forall\l \in \mathbb{L} \\[9pt] + \A = \{ &(\TypeLevel : \SortL); \\ + &(\Type\ \l : \Type\ (\mathsf{s}\ \l))\} &\forall\l \in \mathbb{L} \\[9pt] + \R = \{ &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \\ + &(\SortL,\ \Sortw,\ \Sortw); \\ + &(\Type\ \l_1,\ \Type\ \l_2,\ \Type\ (\l_1 \cup \l_2))\} &\forall\l_1,\l_2 \in \mathbb{L}\\[-4pt] + \end{empheq} + \vspace{-5mm} + \caption{Typer's Pure Type System} +\end{figure} + +\begin{figure} + \label{fig:Re} + \begin{empheq}[box=\fbox]{align*} + \hspace{15mm} & \ & \ & \hspace{7mm} \\ + \R_e = \{ &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \\ + &(\SortL,\ \Sortw,\ \Sortw); \\ + &(\Type\ \l_1,\ \Type\ \l_2,\ \Type\ \l_2) \} &\forall\l_1,\l_2 \in \mathbb{L}\\[-4pt] + \end{empheq} + \vspace{-5mm} + \caption{Typer's Impredicative Rules} +\end{figure} + +Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \z ~~|~~ \s\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ +%% FIXME: We'll need somewhere to clarify that those `l`s have to be present +%% in the Γ environment with type TypeLevel. +The two first constructs correspond to the constant zero and to the successor function, respectively. We define a set $\mathbb{L}$ closed under those two constructs. We write $\s^i$ to abbreviate the application of the successor $i$ times. When applied on type levels, the operator $\cup$ returns the greater of the two. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. All type levels $\l$ inhabit the type \TypeLevel\ which belongs to the sort \SortL. + +\Sortw\ is the unique sort of all the universe polymorphic function types. We describe the explicit part of Typer as a Pure Type System \cite{barendregt} in figure \ref{fig:PTS}. % FIXME: PDF prints 1.1 instead of 1 +Because erasable definitions can be impredicative in Typer, we define a separate set of rules $\R_e$ (figure \ref{fig:Re}). % FIXME: PDF prints 1.1 instead of 2 + +\subsection{Erasure in Typer} +Typer manipulates three separate kinds of terms to simplify the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and executed. \emph{Implicit} terms are also used during execution, but Typer can infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are inferred during elaboration, provide type information during checking and are erased before execution. + +\textbf{Notation:} The notation we adopt in this document is meant to allow for the distinction between the three kinds of terms and also to evoke actual Typer code. The traditional explicit lambda term $\la(x\:A).b$ are here be written $\la(x\:A)\explicit b$ and similarly the product type $\Pi(x\:A).B$ are written $(x\:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Compound terms of our calculus therefore all take one of the following forms: +\begin{center} + \begin{tabular}[h]{rclll} + & & $\la$-abstraction & Product type & Application \\[3mm] + Explicit: & & $\la(T:T)\explicit T$ & $(T:T)\explicit T$ & $T{\ap}T$ \\ + Implicit: & & $\la(T:T)\implicit T$ & $(T:T)\implicit T$ & $T{\app}T$ \\ + Erasable: & & $\la(T:T)\erasable T$ & $(T:T)\erasable T$ & $T{\appp}T$ \\[10pt] + \end{tabular} +\end{center} + +After elaboration, implicit terms behave exactly like explicit terms so we will not explicitly include them in our calculus; they will be assumed to be a subset of the explicit terms. + +\textbf{Notation:} We define a context $\Ga$ as a list of typing declarations $(x_i:T_i)$ and write $\Ga \~$ to express that $\Ga$ is well formed. Contexts are concatenated with the semicolon or enriched with an additional declarations with a comma. We write the empty context as a dot ($\cdot$). The set of declared variables in a context $\Ga$ is written $\dv{\Ga}$ and the set of free (i.e. unbound) variables in a term $T$ is written $\fv{T}$ (defined in figure \ref{fig:fv}). The expression $M\{N/x\}$ denotes the substitution of free occurrences of variable $x$ for a term $N$ in term $M$. +\begin{figure}[h] + \label{fig:fv} + \centering + \fbox{\begin{minipage}{0.9\linewidth} + Where $s \in \S$ + \begin{align*} + \fv{s} &= \emptyset & \fv{x} &= x \\[5pt] + \fv{\la(x:T)\explicit M} &= \fv{T}\cup(\fv{M}\backslash\{x\}) & \fv{(x:T)\explicit U} &= \fv{T}\cup(\fv{U}\backslash\{x\}) \\ + \fv{\la(x:T)\erasable M} &= \fv{T}\cup(\fv{M}\backslash\{x\}) & \fv{(x:T)\erasable U} &= \fv{T}\cup(\fv{U}\backslash\{x\}) \\[5pt] + \fv{M \ap N} &= \fv{M}\cup\fv{N} & \fv{M \appp N} &= \fv{M}\cup\fv{N}\\ + \end{align*} + \end{minipage}} + \caption{Definition of the set of free variables} +\end{figure} + +\begin{figure}[h] + \label{fig:*} + \centering + \fbox{\begin{minipage}{0.9\linewidth} + Where $s \in \S$ + \begin{align*} + s^* &= s & x^* &= x \\[5pt] + (\la(x:T)\explicit M)^* &= \la(x)\explicit M^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \\ + (\la(x:T)\erasable M)^* &= M^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \\[5pt] + (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^*\\ + \end{align*} + \end{minipage}} + \caption{Extraction function $M \mapsto M^*$} +\end{figure} + +We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules shown in figure \ref{fig:Typing-rules} are taken directly from Barras and Bernardo's ICC \cite{bruno}, but written in Typer's syntax. + +\begin{figure}[h] + \ \\ \ \\ \fbox{ + \begin{mathpar} + \\ + \infer + {\ } + {\emptyctx \~} + \textsc{ (Wf-E)} + \and %-------------------- + \infer + {\Ga \~ T:s \\ s \in \S \\ x \notin \dv{\Ga}} + {\Ga , x:T \~} + \textsc{ (Wf-S)} + \and %-------------------- + \infer + {\Ga \~ \\ (s_1:s_2) \in \A} + {\Ga \~ s_1:s_2} + \textsc{ (Sort)} + \and %-------------------- + \infer + {\Ga \~ \\ (x:T) \in \Ga} + {\Ga \~ x:T} + \textsc{ (Var)} + \and %-------------------- + \\\\ + \infer + {\Ga \~ T:s_1 \\ \Ga, x:T \~ U:s_2 \\ (s_1,s_2,s_3) \in \R} + {\Ga \~ (x:T) \explicit U : s_3} + \textsc{ (X-Prod)} + \and %-------------------- + \infer + {\Ga, x:T \~ M:U \\ \Ga \~ (x:T) \explicit U : s} + {\Ga \~ \la(x:T) \explicit M : (x:T) \explicit U} + \textsc{ (X-Lam)} + \and %-------------------- + \infer + {\Ga \~ M : (x:T) \explicit U \\ \Ga \~ N:T} + {\Ga \~ M|N : U\{N/x\}} + \textsc{ (X-App)} + \\\\ + \infer + {\Ga \~ T:s_1 \\ \Ga, x:T \~ U:s_2 \\ (s_1,s_2,s_3) \in \R_e} + {\Ga \~ (x:T) \erasable U : s_3} + \textsc{ (E-Prod)} + \and %-------------------- + \infer + {\Ga, x:T \~ M:U \\ \Ga \~ (x:T) \erasable U : s \\ x \notin \fv{M^*}} + {\Ga \~ \la(x:T) \erasable M : (x:T) \erasable U} + \textsc{ (E-Lam)} + \and %-------------------- + \infer + {\Ga \~ M : (x:T) \erasable U \\ \Ga \~ N:T} + {\Ga \~ M|||N : U\{N/x\}} + \textsc{ (E-App)} + \\ + \end{mathpar} + } + \caption{Typer's Typing Rules from ICC} + \label{fig:Typing-rules} +\end{figure} + +There are two notable differences between explicit and erasable typing rules: +\begin{enumerate} +\item In the erasable product rule \textsc{E-Prod}, the set of rules is the impredicative $\R_e$ instead of $\R$ +\item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with new free terms after erasure. +\end{enumerate} + +\subsection{Inductive Definitions} +\textbf{Notation:} We abbreviate a list of terms $N_i$ as $\vec{N}$. For example, $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the list of terms $N_i$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to a member $i$ of the set $\{1,2,3,...,n\}$ for $n = |\vec{N}|$. +\\ +\begin{definition} + We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. +\end{definition} +\begin{definition} + \label{def:foc} + We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax: + + $$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~ (\vec{x}:\vec{M})C$$ + + Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. +\end{definition} +We extend our abstract syntax with three terms from Gim\'enez's inductive definitions \cite{gimenez}: +\begin{itemize} + \renewcommand{\labelitemi}{$-$} + \setlength\itemsep{-3pt} +\item $\Ind(X:A) \<\vec{C}\>$ is an inductively defined type recursively bound to $X$. $\vec{C}$ is the list of constructor signatures which must be a \emph{form of constructor} w.r.t. $X$. +\item $\Constr(i:I)$ stands for the $i$th constructor of an inductive type $I$. +\item $\Case\ M\: S \text{ of } \<\vec{G}\>$ is the function by case analysis on the expression $M$ of type $S$ and where $\<\vec{G}\>$ is the list of cases, represented as abstractions of the respective patterns of constructions. +\end{itemize} + +The typing rules for inductive definitions and case analysis are presented in figure \ref{fig:IND-rules}. + +\begin{figure}[h] + \ \\ \ \\ \fbox{ + \begin{mathpar} + \infer + {\text{Where } I = \Ind(X:\text{Type }\l_A) \<\vec{C}\> \text{ and } i \in |\vec{C}|.\hspace{100mm}} + {} + \and + \infer + {\Ga \~ \text{Type } \l_{A}: \bigcup_{i\in|\vec{C}|} \text{Type } \l_i \\ + \Ga, X:\text{Type } \l_A \stackrel{\forall i \in |\vec{C}|}{\~} C_i:\text{Type } \l_i} + {\Ga \~ I : \text{Type } \l_A} + \textsc{ (Ind)} + \and %-------------------- + \infer + {\Ga \~ I:A} + {\Ga \~ \Constr(i,I) : C_i \{I / X\}} + \textsc{ (Constr)} + \and %-------------------- + \infer + { \Ga \~ Q : (\vec{z}:\vec{Z})(I\ \vec{z}) \to \text{Type } \l_A \\ + \Ga \~ M:(I\ \vec{P}) \\ + %% FIXME: Actually, each Gi returns the constant type Q + %% (it does take some parameters corresponding to the elements + %% carried by the constructor, of course), along with an + %% additional argument (P : Eq M (Ci \vec{x})) witnessing that + %% the case has found M to be of the form "Ci \vec{x}". + %% + %% FIXME: Before introducing inductive types (and hence `case`) + %% we thus need to introduce the built-in `Eq` type, defined in + %% .../typer/btl/builtins.typer as follow: + %% + %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l + %% Eq_refl : ((x : ?t) ≡> Eq x x); + %% Eq_cast : (x : ?t) ≡> (y : ?t) + %% . ≡> (p : Eq x y) + %% . ≡> (f : ?t -> ?t') + %% . ≡> f x -> f y; + %% + %% At run-time `Eq_cast` will be a no-op (i.e. `Eq_cast x` will reduce + %% to `x`), but there is no corresponding normalization rule applied + %% during type-checking (it would be unsound because it would be reduced + %% even in contexts where the `p : Eq x y` argument doesn't actually + %% exist, such as + %% + %% λ (P : Eq Int String) → concat "bug" (cast (p := P) 5) + %% + %% We'll probably want to add an additional builtin of the form: + %% + %% Eq_cast_eval : Eq (Eq_cast ?x) ?x; + %% + %% to axiomatize the runtime behavior of `Eq_cast`, but I haven't + %% bothered to do that yet. + %% + %% FIXME: Typer's `case` construct can have a "default" + %% branch; not sure how to provide that in this setting where + %% the branches implicitly specify their constructor by the position + %% of the branch. Maybe we should use a formalism closer to Typer's + %% real representation where we don't use natural numbers "i" but + %% labels (strings) to name each constructor. Let's keep using "i" + %% and forget about the default branch for now, tho. + \Ga \stackrel{\forall i \in |\vec{G}|}{\~} G_i:Q} + %% FIXME: Similarly, here, the return type is just Q with no `\vec{P}` + %% nor `M` argument. + {\Ga \~ \Case\ M:(I\ \vec{P}) \of \<\vec{G}\> : Q} + \textsc{ (Case)} + \end{mathpar} + } + \caption{Typer's Inductive and Case Typing Rules} + \label{fig:IND-rules} +\end{figure} + +\subsection{Fixpoint Operator} + +Recursion is specified through the use of a recursive operator \Letrec \todo + +\begin{mathpar} + \infer + { \Ga \~ M:T \\ + \Ga, x:=M:T \~ N : U} + {\Ga \~ \Let (x:T) = M\ \In\ N : U \{T / x\}} + \textsc{ (Let)} +\end{mathpar} + +\begin{definition} + A \emph{recursive position} in the form of constructor $(\vec{x}:\vec{M}) (X \vec{N})$ is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. Note that this is not in contradiction to definition \ref{def:foc} because some abstraction $(x_i:M_i)$ could be non-dependent (i.e. of form $P \explicit C$ in definition \ref{def:foc}), in which $X$ is free to appear. We abbreviate this property as $RP\{i,C\}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. +\end{definition} +\begin{definition} + The \emph{guarded by destructors} condition is written as the predicate $\D_\V\{f,k,x,M\}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which collects the recursive components of $x$ in $M$. Below, we write $\D_\V\{M\}$ for brevity instead of the full $\D_\V\{f,k,x,M\}$. We also write $\D_\V\{\vec{M}\}$ instead of $\D_\V\{M_1\} \land\D_\V\{M_2\}\land ...$. By structural induction on term $M$, we describe when $\D_\V\{M\}$ is true by assigning conjunctions of necessary conditions to each form of $M$: + \begin{align*} + \D_\V\{M\} & = \text{True} & \text{if } f \notin \fv{M}\\ + \D_\V\{\la (z:P)\to Q\} & = \D_\V\{P\} \land \D_\V\{Q\} \\ + \D_\V\{(z:P)\to Q\} & = \D_\V\{P\} \land \D_\V\{Q\} \\ + \D_\V\{\Letrec ?\} & = \ ? \\ + \D_\V\{\Ind(X\:A)\<\vec{C}\>\} & = \D_\V\{A\} \land \D_\V\{\vec{C}\} \\ + \D_\V\{f \vec{P}\} & = (|\vec{P}| > k) \land (P_{k+1} \equiv (z\ \vec{Q})) \land \D_\V\{\vec{P}\} & \text{with $z \in \V$}\\ + \D_\V\{N \vec{P}\} & = \D_\V\{N\} \land \D_\V\{\vec{P}\} &\text{if $N \neq f$}\\ + \D_\V\{\Case\ (z\ \vec{P})\:S\ \of\ \<\vec{G}\>\} & = + % \D_\V\{Q\} \land \D_\V\{S\} \land \D_\V\{\vec{P}\} &\text{with $z \in \V \cup \{x\}$}\\ + % & \quad \land S \equiv I\vec{R} & \text{with }I =\Ind (X:A)\<\vec{C}\> \\ + % & \quad \land \text{if } + \end{align*} +\end{definition} + +\subsection{Conversion Rules} +Typer admits $\beta$- and $\iota$-conversions. The congruence relation between converted terms is written $\cong$. $\beta$-reduction is defined as +$$(\la (x:T)\explicit e_1)|e_2 ~ \cong_\beta ~ e_1\{e_2/x\}$$ +$$(\la (x:T)\erasable e_1)|||e_2 ~ \cong_\beta ~ e_1\{e_2/x\}$$ + +$\iota$-reduction concerns case analyses: +$$\Case\ (\Constr (i,I)\vec{P}):S\ \of\ \<\vec{G}\> \cong_{\iota} (G_i\vec{P})$$ +Conversion rules are exposed in figure \ref{fig:conv}. + +\begin{figure}[h] + \label{fig:conv} + \ \\ \ \\ \fbox{ + \begin{mathpar} + \infer + {M \cong N \\ N \cong P} + {M \cong P} + \and %-------------------- + %% FIXME: Add conversion rules for other terms? (lambda, product type, application) + \infer + {A \cong A' \\ |\vec{C}| = |\vec{C'}| \\ C_i \stackrel{\forall i \in |\vec{C}|}{\cong} C_i'} + {\Ind (X:A)\<\vec{C}\> \cong \Ind (X:A')\<\vec{C'}\>} + \and %-------------------- + \infer + {I \cong I'} + {\Constr(i,I) \cong \Constr(i,I')} + \and %-------------------- + \infer + {M \cong M' \\ S \cong S' \\ |\vec{G}| = |\vec{G'}| \\ + G_i \stackrel{\forall i \in |\vec{C}|}{\cong} G_i'} + {\Case\ M :S \text{ of } \<\vec{G}\> \cong \Case\ M' :S' \text{ of } \<\vec{G'}\>} + \and %-------------------- + \infer + {B \cong B' \\ N \cong N'} + {\Letrec\ ? \todo} + \\ + \end{mathpar} + } + \caption{Typer's Conversion Rules} +\end{figure} + +\section{Typer as an Extension of a Calculus of Constructions} +In this section we show that the erasable terms of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an impredicative $\mathsf{Prop}$ and an infinite hierarchy of predicative universes (\CC). This will be demonstrated through a translation and a proof of its correctness. + +\subsection{Definition of \CC} + +\begin{figure}[h] + \begin{empheq}[box=\fbox]{align*} + \hspace{20mm} & \ & \ & \hspace{7mm} \\ + \S_{CC} = \{ & \Prop; \Type_i\} &\forall i > 0 \\[9pt] + \A_{CC} = \{ &(\Prop : \Type_1); \\ + &(\Type_i : \Type_{i+1})\} &\forall i > 0 \\[9pt] + \R_{CC} = \{ &(\Prop, \Prop, \Prop) \\ + &(\Prop, \Type_i, \Type_i) &\forall i > 0 \\ + &(\Type_i, \Prop, \Prop); &\forall i > 0 \\ + &(\Type_i,\Type_j,\Type_{\max (i,j)}); &\forall i > 0 \\ + \end{empheq} + \vspace{-5mm} + \caption{\CC's Pure Type System} + \label{fig:CC-pts} +\end{figure} + +\begin{figure}[h] + \ \\ \ \\ \fbox{ + \begin{mathpar} + \\ + \infer + {\ } + {\emptyctx \CCdash} + \textsc{ (CC-Wf-E)} + \and %-------------------- + \infer + {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} + {\Ga , x:T \CCdash} + \textsc{ (CC-Wf-S)} + \and %-------------------- + \infer + {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} + \textsc{ (CC-Sort)} + \and %-------------------- + \infer + {\Ga \CCdash \\ (x:T) \in \Ga} + {\Ga \CCdash x:T} + \textsc{ (CC-Var)} + \and %-------------------- + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : s_3} + \textsc{ (CC-Prod)} + \and %-------------------- + \infer + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \textsc{ (CC-Lam)} + \and %-------------------- + \infer + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U\{N/x\}} + \textsc{ (CC-App)} + \\ + \end{mathpar} + } + \caption{\CC's Typing Rules} + \label{fig:CC-rules} +\end{figure} + +Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, to which we add an infinite hierarchy of predicative universes above an impredicative \Prop. Thus we have: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$ + +\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, where the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,j)})$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (e.g. dependent types or polymorphic functions). Our definition of \CC\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}). + +\subsection{Translation} +\begin{figure}[h] + \centering + \fbox{ + \begin{minipage}{0.85\linewidth} + \begin{align*} + \rew{\cdot} &= \cdot & \rew{\Prop} &= \Type\ \z \\ + \rew{\Ga,x:T} &= \rew{\Ga},x:\rew{T} & \rew{\Type_{i}} &= \Type\ (\s^{i}\ \z) \\[-20pt] + \end{align*} + \begin{align*} + \rew{\la(x:T)\explicit U} &= + \begin{cases} + \la(x : \rew{T}) \erasable \rew{U} &\text{if $(U:\tau)$, $(\tau : \Prop)$ and $(T:\Type_i)$}\\ + \la(x : \rew{T}) \explicit \rew{U} &\text{otherwise} + \end{cases}\\ + \rew{(x:T)\explicit U} &= + \begin{cases} + (x : \rew{T})\erasable \rew{U} &\text{if $(U: \Prop)$ and $(T:\Type_i)$}\\ + (x : \rew{T})\explicit \rew{U} &\text{otherwise} + \end{cases}\\ + \rew{M \ap N} &= + \begin{cases} + \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(N:\tau':\Type_i)$} \\ + \rew{M}|\rew{N} &\text{otherwise} + \end{cases}\\ + \rew{U\{N/x\}} &= \rew{U}\{\rew{N}/x\}\\ + % FIXME: Is substitution relevent here? Is it part of the syntax or + % meta-syntax? + \end{align*} + \end{minipage} + } + \caption{Definition of the translation} + \label{fig:[]} +\end{figure} + +The translator operator \rew{\_} is defined on contexts and terms of \CC. We expose the translation on figure \ref{fig:[]}. We will consider this translation correct if it is both complete and sound as per the following definitions. \emph{Completeness} of the translation ($\Rightarrow$) is established if every translated expression of \CC\ inhabits its translated type in the Typer system. \emph{Soundness} of the translation ($\Leftarrow$) is established if every valid typing derivation of translated terms in the Typer system implies a valid typing derivation in \CC: +\begin{theorem} + \label{thm:correctness-translation} + \begin{align*} + \Ga \CCdash & ~~ \iff ~~ \rew{\Ga} \~ \\ + \Ga \CCdash e:\tau & ~~ \iff ~~ \rew{\Ga} \~ \rew{e}:\rew{\tau} + \end{align*} +\end{theorem} + +Before proving the correctness of the equality, we show the following lemmas: +\begin{lemma} + \label{lem:S-equiv} + $s \in \S_{CC} \iff \rew{s} \in \S$ + \begin{proof} + In the forward direction, for $\Prop \in S_{CC}$, we know that $$\rew{\Prop} = \Type\ \z\ \in \S$$ + And for $\Type_i \in \S_{CC}$, we know that $$\rew{\Type_i} = \Type\ (\s^i\ \z) \in \S \quad \forall i > 0$$ + Conversely, because the translation on sorts is defined on elements of $S_{CC}$, it follows that if $\rew{s} \in S$, then by necessity $s \in S_{CC}$. + \end{proof} +\end{lemma} + +% FIXME: For the following lemmas, I'm not sure whether to stop at the +% '(\s^i\ \z) \forall i' form or to show the switch to the '\Type\ \ell +% \forall \ell' form. The first is sufficient, but looks less like our +% presentation of the PTS but the second has the typelevel variable 'l' in +% the syntax for '\ell' and may lead to confusion even if we bind \ell to +% elements of \mathbb{L} + +\begin{lemma} + \label{lem:A-equiv} + $(s_1:s_2) \in \A_{CC} \iff (\rew{s_1}:\rew{s_2}) \in \A$ + \begin{proof} + In the forward direction, for $(\Prop\:\Type_1) \in \A_{CC}$, we know that + \begin{align*} + (\rew{\Prop}:\rew{\Type_1}) &= (\Type\ \z:\Type\ (\s\ \z)) \in \A + \end{align*} + + And for $(\Type_i\:\Type_{i+1}) \in \A_{CC}$, we know that + \begin{align*} + (\rew{\Type_i}:\rew{\Type_{i+1}}) &= (\Type\ (\s^i\ \z):\Type\ (\s^{i+1}\ \z)) &&\forall\ i>0\\ + &= (\Type\ (\s^i\ \z):\Type\ (\s\ (\s^i\ \z)) &&\forall\ i>0\\ + &= (\Type\ (\s\ \l):\Type\ (\s\ (\s\ \l))) &\in \A \quad &\forall\ \l \in \mathbb{L} + \end{align*} + Conversely, since the translation on sorts is defined on elements of $S_{CC}$, sorts $\rew{s}$ match with sorts of the form $\Type\ (\s^i\ \z)\in \S\ \forall i \ge 0$ (lemma \ref{lem:S-equiv}). It follows that axioms $(\rew{s_1}:\rew{s_2}) \in \A$ match with axioms of the form $(\Type\ \l:\Type\ (\s\ \l)) \in \A ~~ \forall \l \in \mathbb{L}$, for each of which there exists an axiom $(s_1:s_2) \in A_{CC}$ by the equality just established in the forward direction. + \end{proof} +\end{lemma} + +\begin{lemma} + \label{lem:R-equiv} $(s_1,s_2,s_3) \in \R_{CC} \iff (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R \text{ if } s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$ + \begin{proof} + In the forward direction, first there is $(\Prop,\Prop,\Prop) \in \R_{CC}$ for which we have + $$(\rew{\Prop},\rew{\Prop},\rew{\Prop}) = (\Type\ \z,\Type\ \z,\Type\ \z) \in \R$$ + Second, there is $(\Prop, \Type_i, \Type_i) \in \R_{CC}\ \forall i > 0$ for which we have + $$(\rew{\Prop}, \rew{\Type_i}, \rew{\Type_i}) = (\Type\ \z, \Type\ (\s^i\ \z), \Type\ (\s^i\ \z)) \in \R \quad \forall i > 0$$ + And finally there is $(\Type_i, \Type_j, \Type_{\max (i,j)})$ for which we have + \begin{align*} + & (\rew{\Type_i}, \rew{\Type_j}, \rew{\Type_{\max (i,j)}}) \\ + &= + \begin{cases} + (\Type\ (\s^i\ \z),\Type\ (\s^j\ \z),\Type\ (\s^i\ \z)) & \text{if } i>j \\ + (\Type\ (\s^i\ \z),\Type\ (\s^j\ \z),\Type\ (\s^j\ \z)) & \text{if } j>i + \end{cases} \quad \forall i,j > 0 \\ + &= + \begin{cases} + (\Type\ (\s\ \l_1), \Type\ (\s\ \l_2), \Type\ (\s\ \l_1)) & \text{if } (\s\ \l_1) \cup (\s\ \l_2) = (\s\ \l_1) \\ + (\Type\ (\s\ \l_1), \Type\ (\s\ \l_2), \Type\ (\s\ \l_2)) & \text{if } (\s\ \l_1) \cup (\s\ \l_2) = (\s\ \l_2) + \end{cases} \quad \forall \l_1,\l_2 \in \mathbb{L} \\ + &= (\Type\ (\s\ \l_1), \Type\ (\s\ \l_2), \Type\ ((\s\ \l_1) \cup (\s\ \l_2))) \quad \in \R \quad \forall \l_1,\l_2 \in \mathbb{L} + \end{align*} + Conversely, since the translation on sorts is defined on elements of $S_{CC}$, sorts $\rew{s}$ match with sorts of the form $\Type\ (\s^i\ \z)\in \S\ \forall i \ge 0$ (lemma \ref{lem:S-equiv}). It follows that rules $(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$ match with rules of the form $$(\Type\ \l_1, \Type\ \l_2, \Type\ (\l_1 \cup \l_2)) \in \R ~~ \forall \l_1,\l_2 \in \mathbb{L}$$ By the equalities established in the forward direction, each such rule has a single corresponding rule in $(s_1,s_2,s_3) \in \R_{CC}$, as long as $s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$. + + \end{proof} +\end{lemma} +\begin{lemma} + \label{lem:Re-equiv} + $(\Type_i,\Prop,\Prop) \in \R_{CC} \iff (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e \quad \forall i > 0$ + \begin{proof} + In the forward direction, for $(\Type_i,\Prop,\Prop) \in \R_{CC}$, we have + \begin{align*} + (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) &= (\Type\ (\s^i\ \z),\Type\ \z, \Type\ \z) &&\forall\ i > 0\\ + &= (\Type\ (\s\ \l),\Type\ \z, \Type\ \z) & \in \R_e \quad &\forall\ \l \in \mathbb{L} + \end{align*} + Conversely, $(\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e\ \forall i > 0$ matches with rules of the form $$(\Type\ (\s\ \l),\Type\ \z, \Type\ \z) \in \R_e \quad \forall\ \l \in \mathbb{L}$$ For each of which there is a rule $(\Type_i,\Prop,\Prop) \in \R_{CC}$ by the equality established in the forward direction. + \end{proof} +\end{lemma} + +\begin{lemma} + \label{lem:E-Lam-FV} + If we have + \begin{mathpar} + % Induction on derivations in CCω is used because induction on + % derivations of translated terms in Typer can lead to a case + % (e.g. X-App) where it is possible to insert a term absent in CCω + % (e.g. an explicit abstraction of a higher sort over a body of sort + % Type z) in the derivation tree, thus allowing variable 'y' to appear + % free in the term + + % So instead of using this lemma (in completeness, case:E-Lam) with the + % translated premises, we can use it with the initial (CCω) ones + {\Ga, y:V \CCdash P:W \\ \Ga, y:V \CCdash W : \Prop \\ \Ga \CCdash V : \Type_i} + \end{mathpar} + then the following always holds + $$y \notin \fv{\rew{P}^*}$$ + + \begin{proof} + By induction on the typing derivation $\Ga, y:V \CCdash P:W$, either a typing rule is not applicable to this derivation or we show that it satisfies $y \notin \fv{\rew{P}^*}$. + + \textbf{CC-Sort:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} + \tag{CC-Sort} + \end{mathpar} + All axioms of $\A_{CC}$ are constructed with sorts $s_1, s_2 \in \S_{CC}$. There are no sorts in $\S_{CC}$ smaller than $\Prop$. Since here $s_2$ is $W$ and by assuption $W : \Prop$, then no axiom $(s_1:s_2) \in \A_{CC}$ will match $(P:W)$ and this typing rule cannot apply. + + \textbf{CC-Var:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash \\ (x:T) \in \Ga} + {\Ga \CCdash x:T} + \tag{CC-Var} + \end{mathpar} + Considering that typing judgments are introduced in contexts exclusively by means of rule \textsc{CC-Wf-S}, we can assume + \begin{mathpar} + {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} + \end{mathpar} + which all holds by the assignment $s = \Prop$. Thus, $P$ (here $x$) is a variable. The translation and extraction for the variable leaves it untouched + $$\rew{P}^* = P^* = P$$ + Because $y : V : \Type_i$ and $P : W : \Prop$, we have that $y \neq P$ because they are variables that inhabit different universes so it follows that $y \notin \fv{P}$. + + \textbf{CC-Prod:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : \s_3} + \tag{CC-Prod} + \end{mathpar} + Similarly to case \textsc{CC-Sort}, we cannot apply this rule because here $s_3 = W$ and by assumption $W : \Prop$ and \Prop\ is the smallest universe in $\S_{CC}$. So no rule $(s_1,s_2,s_3) \in \R_{CC}$ can match in this case. + + \textbf{CC-Lam:}\\ + \begin{mathpar} + \infer + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \tag{CC-Lam} + \end{mathpar} + Sort $s$ here is $\Prop$ because $(x:T) \explicit U$ is $W$ and by assumption $W : \Prop$. The construction of $(x:T) \explicit U$ reveals that $U : \Prop$ because every rule $(s_1,s_2,s_3) \in \R_{CC}$ that has $s_3 = \Prop$ also has $s_2 = \Prop$: + \begin{mathpar} + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:\Prop \\ (s_1,\Prop,\Prop) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : \Prop} + \tag{CC-Prod} + \end{mathpar} + The translation for the lambda abstraction $\la(x:T) \explicit M$ has a predicative and impredicative case. In both cases, however, the extraction erases the type annotation $\rew{T}$. Therefore $\fv{\rew{P}^*} = \fv{\rew{M}^*}$ and $y \notin \fv{\rew{M}^*}$ holds by the induction hypothesis because $M : U : \Prop$. + + \textbf{CC-App:}\\ + \begin{mathpar} + \infer + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U\{N/x\}} + \tag{CC-App} + \end{mathpar} + Here $P = M|N$ and $W = U\{N/x\}$. $y \notin \fv{\rew{P}^*}$ will hold if we can show that $y \notin \fv{\rew{M}^*}$ and---unless $N$ is an impredicative argument---$y \notin \fv{\rew{N}^*}$. By assumption $U\{N/x\} : \Prop$ + %% Does this step really hold? + and therefore also $U : \Prop$. It follows that $(x:T)\explicit U : \Prop$ by the typing rule \textsc{CC-Prod}. Thus, by induction hypothesis, we have $y \notin \fv{\rew{M}^*}$ because $M : (x:T)\explicit U : \Prop$. If $N : T : \Prop$, then we can also apply the induction hypothesis. Otherwise, the extraction on the translation erases the impredicative argument completely. + \end{proof} +\end{lemma} + +\subsection{Completeness of translation} +By structural induction on typing derivation of \CC, as per theorem \ref{thm:correctness-translation} ($\Rightarrow$), each valid derivation translates to a valid derivation in the Typer system. For most typing rules, by assuming the rule in \CC, we derive the necessary premises in Typer to show that the corresponding Typer rule also applies. + +\underline{\textbf{CC-Wf-E:}} +\begin{mathpar} + \infer + {\ } + {\emptyctx \CCdash} + \tag{CC-Wf-E} +\end{mathpar} +The translation is immediately true under Typer by rule \textsc{Wf-E}. +\begin{mathpar} + \infer + {\ } + {\rew{\cdot} \~} + \tag{Wf-E} +\end{mathpar} + +\underline{\textbf{CC-Wf-S:}} +\begin{mathpar} + \infer + {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} + {\Ga , x:T \CCdash} + \tag{CC-Wf-S} +\end{mathpar} +By the induction hypothesis we assume +$$\rew{\Ga} \~ \rew{T}:\rew{s}$$ + +From lemma \ref{lem:S-equiv} we infer +$$\rew{s} \in \S$$ + +To apply the Typer rule \textsc{Wf-S}, we have to show that +$$x \notin \dv{\rew{\Ga}}$$ + +\begin{lemma} + \label{lem:DV-equiv} + We have the following equality: + $$\dv{\Ga} = \dv{\rew{\Ga}}$$ + \begin{proof} + By structural induction on $\Ga$. The equality holds on the base case $\rew{\cdot} = \cdot$ since both the empty context and its translation have no declared variables. The equality holds on the recursive case $\rew{\Ga, x \: T} = \rew{\Ga}, x \: \rew{T}$ since the name of the declared variable is left unchanged. + \end{proof} +\end{lemma} +\begin{lemma} + \label{lem:not-DV-equiv} + The following holds: + $$x \notin \dv{\Ga} \iff x \notin \dv{\rew{\Ga}}$$ + \begin{proof} + Follows directly from lemma \ref{lem:DV-equiv}. + \end{proof} +\end{lemma} +We reach the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s} \\ \rew{s} \in \S \\ x \notin \dv{\rew{\Ga}}} + {\rew{\Ga} , x:\rew{T} \~} + \tag{WF-S} +\end{mathpar} + +\underline{\textbf{CC-Sort:}}\\ +\begin{mathpar} + \infer + {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} + \tag{CC-Sort} +\end{mathpar} +By the induction hypothesis we assume +$$\rew{\Ga} \~$$ + +From lemma \ref{lem:A-equiv} we infer +$$(\rew{s_1}:\rew{s_2}) \in \A$$ + +We reach the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} + {\rew{\Ga} \~ \rew{s_1}:\rew{s_2}} + \tag{Sort} +\end{mathpar} + +\underline{\textbf{CC-Var:}}\\ +\begin{mathpar} + \infer + {\Ga \CCdash \\ (x:T) \in \Ga} + {\Ga \CCdash x:T} + \tag{CC-Var} +\end{mathpar} +By the induction hypothesis we assume +$$\rew{\Ga} \~$$ + +\begin{lemma} + \label{lem:in-ctx-equiv} + The following holds: + $$(x:T) \in \Ga \iff (x:\rew{T}) \in \rew{\Ga}$$ + \begin{proof} + By structural induction on $\Ga$. The base case makes the proposition false on both sides. By lemma \ref{lem:DV-equiv}, the set of declared variables in a \CC\ context and in its translation are the same, so we must only show that they both have the appropriate types. It follows from the recursive definition of translation on contexts $\rew{\Ga, x \: T} = \rew{\Ga}, x \: \rew{T}$ that they do. + \end{proof} +\end{lemma} + +With lemma \ref{lem:in-ctx-equiv}, we reach the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (x:\rew{T}) \in \rew{\Ga}} + {\rew{\Ga} \~ x:\rew{T}} + \tag{Var} +\end{mathpar} + +\underline{\textbf{CC-Prod:}}\\ +\begin{mathpar} + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : s_3} + \tag{CC-Prod} +\end{mathpar} +By the induction hypothesis, there are two subcases to consider---a predicative and an impredicative one: + +\textbf{Predicative subcase:}\\ +The predicative subcase will concern applications of \textsc{CC-Prod} for which the rule is $(s_1,s_2,s_3) \in \R_{CC}$ where $s_1 \neq \Type_i$ or $s_2 \neq \Prop$. We can assume +\begin{mathpar} + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2}} +\end{mathpar} +From lemma \ref{lem:R-equiv} we infer +$$(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ +with which we produce the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2} \\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} + {\rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}} + \tag{X-Prod} +\end{mathpar} + +\textbf{Impredicative subcase:}\\ +The impredicative subcase will concern applications of \textsc{CC-Prod} for which the rule is $(\Type_i,\Prop,\Prop) \in \R_{CC}$. We can assume +\begin{mathpar} + {\rew{\Ga} \~ \rew{T}:\rew{\Type_i} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop}} +\end{mathpar} +From lemma \ref{lem:Re-equiv} we infer +$$(\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ +with which we produce the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{\Type_i} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}} + \tag{E-Prod} +\end{mathpar} + +\underline{\textbf{CC-Lam:}}\\ +\begin{mathpar} + \infer + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \tag{CC-Lam} +\end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ \rew{(x:T) \explicit U} : \rew{s}} +\end{mathpar} +To apply a lambda rule of Typer, we have to consider the two cases for the translation \rew{(x:T) \explicit U}: + +\textbf{Predicative subcase:}\\ +The predicative product type translates to an explicit product type $(x:\rew{T}) \explicit \rew{U}$ and we apply the explicit \textsc{X-Lam} typing rule to derive the typing of the explicit lambda abstraction. +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s}} + {\rew{\Ga} \~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} + \tag{X-Lam} +\end{mathpar} + +\textbf{Impredicative subcase:}\\ +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort $\rew{\Prop}$ with $T : \Type_i$ and $U : \Prop$ by the definition of translation. We call upon lemma \ref{lem:E-Lam-FV} to infer that $x \notin \fv{\rew{M}^*}$ and we have the sufficient premises to apply rule \textsc{E-Lam}. We obtain the translation of the conclusion +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \\ x \notin \fv{\rew{M}^*}} + {\rew{\Ga} \~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} + \tag{E-Lam} +\end{mathpar} + +\underline{\textbf{CC-App:}}\\ +\begin{mathpar} + \infer + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U\{N/x\}} + \tag{CC-App} +\end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\rew{\Ga} \~ \rew{M} : \rew{(x:T) \explicit U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} +\end{mathpar} +Again, there are two subcases to consider for the translation $\rew{(x:T) \explicit U}$: + +\textbf{Predicative subcase:}\\ +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \explicit \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} + {\rew{\Ga} \~ \rew{M}|\rew{N} : \rew{U}\{\rew{N}/x\}} + \tag{X-App} +\end{mathpar} +\textbf{Impredicative subcase:}\\ +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} + {\rew{\Ga} \~ \rew{M}|||\rew{N} : \rew{U}\{\rew{N}/x\}} + \tag{E-App} +\end{mathpar} +\qed + +\subsection{Soundness of translation} +By structural induction on typing derivations of Typer, as per theorem \ref{thm:correctness-translation} ($\Leftarrow$), each valid derivation of translated terms has a corresponding valid derivation in \CC. We consider each of Typer's typing rules, the terms of which are limited to be translated terms of \CC. We implicitly distribute translation in contexts. + +\underline{\textbf{Wf-E:}}\\ +\begin{mathpar} + \infer + {\ } + {\rew{\cdot} \~} + \tag{Wf-E} +\end{mathpar} + +The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E} + +\begin{mathpar} + \infer + {\ } + {\emptyctx \CCdash} + \tag{CC-Wf-E} +\end{mathpar} + +\underline{\textbf{Wf-S:}}\\ +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:s' \\ s' \in \S \\ x \notin \dv{\rew{\Ga}}} + {\rew{\Ga} , x:\rew{T} \~} + \tag{WF-S} +\end{mathpar} +It is not immediately obvious that sort $s'$ is a translated sort. Sorts in $\S$ that are not translations of sorts in $\S_{CC}$ include \SortL\ and \Sortw. However, because we assume the construction of translated term $\rew{T}$, it cannot correspond to \TypeLevel\ (inhabitant of \SortL) or universe-polymorphic types (inhabitants of \Sortw) so $s'$ can only really be of form $\Type\ \l$. Because each sort of the latter form has a corresponding sort in $\S_{CC}$ (lemma \ref{lem:S-equiv}), we can set $s' = \rew{s}$ with $s \in \S_{CC}$. + +Thus, by the induction hypothesis we have +\begin{mathpar} + {\Ga \CCdash T:s \\ s \in \S_{CC}} +\end{mathpar} +By lemma \ref{lem:not-DV-equiv} we infer +\begin{mathpar} + x \notin \dv{\Ga} +\end{mathpar} +We therefore have the corresponding rule +\begin{mathpar} + \infer + {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} + {\Ga , x:T \CCdash} + \tag{CC-Wf-S} +\end{mathpar} + +\underline{\textbf{Sort:}}\\ +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} + {\rew{\Ga} \~ \rew{s_1}:\rew{s_2}} + \tag{Sort} +\end{mathpar} +By lemma \ref{lem:A-equiv}, we infer from $(\rew{s_1}:\rew{s_2}) \in \A$ that $(s_1:s_2) \in \A_{CC}$. We can assume +\begin{mathpar} + {\Ga \CCdash} +\end{mathpar} +by the induction hypothesis. Therefore we have the rule +\begin{mathpar} + \infer + {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} + \tag{CC-Sort} +\end{mathpar} + +\underline{\textbf{Var:}}\\ +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (x:\rew{T}) \in \rew{\Ga}} + {\rew{\Ga} \~ x:\rew{T}} + \tag{Var} +\end{mathpar} +By lemma \ref{lem:in-ctx-equiv}, we infer from $(x:\rew{T}) \in \rew{\Ga}$ that $(x:T) \in \Ga$. By the induction hypothesis we have +\begin{mathpar} + \Ga \CCdash +\end{mathpar} +We therefore have the corresponding rule +\begin{mathpar} + \infer + {\Ga \CCdash \\ (x:T) \in \Ga} + {\Ga \CCdash x:T} + \tag{CC-Var} +\end{mathpar} + +\underline{\textbf{X-Prod:}}\\ +This case considers the typing derivation of term $\rew{(x:T)\explicit U}$. If \textsc{X-Prod} constructed it, then $\rew{(x:T)\explicit U} = (x:\rew{T})\explicit \rew{U}$. +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:s_1' \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:s_2' \\ (s_1',s_2',\rew{s_3}) \in \R} + {\rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}} + \tag{X-Prod} +\end{mathpar} +\SortL\ is not part of the co-domain of the translation function $\rew{\_}$, so $\rew{s_3}$ only matches with sorts of form $\Type\ \l\ $(where $\l \in \mathbb{L}$). The only rule scheme matching this condition is $(\Type\ \l_1, \Type\ \l_2, \Type\ (\l_1 \cup \l_2)) \in R$. Because every sort of form $\Type\ \l$ occupies the co-domain of the translation function, we can set $s_1' = \rew{s_1}$ and $s_2' = \rew{s_2}$. Thus, we have +\begin{mathpar} + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2} \\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in R_{CC}} +\end{mathpar} + +By induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2} +\end{mathpar} +By lemma \ref{lem:R-equiv} we infer +$$(s_1,s_2,s_3) \in \R_{CC}$$ +We can therefore apply the rule +\begin{mathpar} + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : s_3} + \tag{CC-Prod} +\end{mathpar} + +\underline{\textbf{E-Prod:}}\\ +This case considers the typing derivation of term $\rew{(x:T)\explicit U}$. If \textsc{E-Prod} constructed it, then $\rew{(x:T)\explicit U} = (x:\rew{T})\erasable \rew{U}$ so by the definition of translation, $U : \Prop$ and $T : \Type_i$. +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{\Type_i} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}} + \tag{E-Prod} +\end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash T:\Type_i \\ \Ga, x:T \CCdash U:\Prop} +\end{mathpar} +By lemma \ref{lem:Re-equiv} we have +\begin{mathpar} + {(\Type_i,\Prop,\Prop) \in \R_e} +\end{mathpar} +We can therefore apply the rule +\begin{mathpar} + \infer + {\Ga \CCdash T:\Type_i \\ \Ga, x:T \CCdash U:\Prop \\ (\Type_i,\Prop,\Prop) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : \Prop} + \tag{CC-Prod} +\end{mathpar} + +\underline{\textbf{X-Lam:}}\\ +This case considers the typing derivation of term $\rew{\la(x:T)\explicit M}$. If \textsc{X-Lam} constructed it, then $\rew{\la(x:T)\explicit M} = \la(x:\rew{T})\explicit \rew{M}$ and accordingly has the product type $\rew{(x:T)\explicit U} = (x:\rew{T})\explicit \rew{U}$. +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s}} + {\rew{\Ga} \~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} + \tag{X-Lam} +\end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} +\end{mathpar} +We can therefore apply the rule +\begin{mathpar} + \infer + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \tag{CC-Lam} +\end{mathpar} + +\underline{\textbf{E-Lam:}}\\ +This case considers the typing derivation of term $\rew{\la(x:T)\explicit M}$. If \textsc{E-Lam} constructed it, then $\rew{\la(x:T)\explicit M} = \la(x:\rew{T})\erasable \rew{M}$ and accordingly has the product type $\rew{(x:T)\explicit U} = (x:\rew{T})\erasable \rew{U}$. In this case, by the definition of translation, we necessarily have $U:\Prop$ and $T:\Type_i$. +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \\ x \notin \fv{\rew{M}^*}} + {\rew{\Ga} \~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} + \tag{E-Lam} +\end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} +\end{mathpar} +We can therefore apply the rule +\begin{mathpar} + \infer + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : \Prop} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \tag{CC-Lam} +\end{mathpar} + +\underline{\textbf{X-App:}}\\ +This case considers the typing derivation of term $\rew{M|N}$. If \textsc{X-App} constructed it, then $\rew{M|N} = \rew{M}|\rew{N}$ and $\rew{M}$ has type $\rew{(x:T)\explicit U} = (x:\rew{T})\explicit \rew{U}$. +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \explicit \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} + {\rew{\Ga} \~ \rew{M}|\rew{N} : \rew{U}\{\rew{N}/x\}} + \tag{X-App} +\end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} +\end{mathpar} +We can therefore apply the rule +\begin{mathpar} + \infer + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U\{N/x\}} + \tag{CC-App} +\end{mathpar} + +\underline{\textbf{E-App:}}\\ +This case considers the typing derivation of term $\rew{M|N}$. If \textsc{E-App} constructed it, then $\rew{M|N} = \rew{M}|||\rew{N}$ and $\rew{M}$ has type $\rew{(x:T)\explicit U} = (x:\rew{T})\erasable \rew{U}$. +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} + {\rew{\Ga} \~ \rew{M}|||\rew{N} : \rew{U}\{\rew{N}/x\}} + \tag{E-App} +\end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} +\end{mathpar} +We can therefore apply the rule +\begin{mathpar} + \infer + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U\{N/x\}} + \tag{CC-App} +\end{mathpar} + +Rules \textsc{Ind}, \textsc{Constr}, and \textsc{Case} cannot construct the judgment $\rew{\Ga} \~ \rew{e} : \rew{\tau}$ because inductive types are not part of the domain of the translation operator. \qed + +\subsection{Example} +Consider the impredicative encoding of the \texttt{pack} existential type constructor in \CC: + +\begin{align*} + \mathtt{pack}\ : \quad + &(\tau : \Type_1) \explicit (f : (x : \tau) \explicit \Prop) \explicit (w : \tau) \explicit (p : f| w) \explicit\\ + &(t : \Prop) \explicit (b : (y : \tau) \explicit (z : f|y) \explicit t) \explicit t \{w/y\} \{p/z\}\\[10pt] + :=\ &\la (\tau : \Type_1) \explicit \la (f : (x : \tau) \explicit \Prop) \explicit \la (w : \tau) \explicit \la (p : f|w) \explicit\\ + &\la (t : \Prop) \explicit \la (b : (y : \tau) \explicit (z : f|y) \explicit t) \explicit b|w|p +\end{align*} + +The translation of \texttt{pack} to Typer will assign abstractions to be either explicit or erasable depending on them being predicative of impredicative, respectively. The translation of the product type of $f$ in \texttt{pack} for example will be explicit by its predicativity: +\begin{align*} + \Ga &\CCdash \tau : \Type_1\\ + \Ga &\CCdash \Prop : \Type_1\\ + \Ga &\CCdash (x : \tau)\explicit\Prop : \Type_1 &\quad\quad\text{by \texttt{CC-Prod} and rule $(\Type_1,\Type_1,\Type_1)$} +\end{align*} +\begin{align*} + \rew{\Ga} \CCdash \rew{(x : \tau)\explicit\Prop} : \rew{\Type_1} + &\quad\leadsto\quad \rew{\Ga} \~ (x : \rew{\tau}) \explicit \rew{\Prop} : \Type\ (\s\ \z)\\ + &\quad\leadsto\quad \rew{\Ga} \~ (x : \tau) \explicit \Type\ \z : \Type\ (\s\ \z) +\end{align*} + +On the other hand, $b$ has both an erasable and an explicit component: + +\begin{align*} + \Ga &\CCdash t : \Prop \\ + \Ga &\CCdash f|y : \Prop \\ + \Ga &\CCdash (z : f|y)\explicit t : \Prop &\quad\quad\text{by \texttt{CC-Prod} and rule $(\Prop,\Prop,\Prop)$}\\[10pt] + \Ga &\CCdash \tau : \Type_1 \\ + \Ga &\CCdash (z : f|y)\explicit t : \Prop\\ + \Ga &\CCdash (y : \tau)\explicit (z : f|y)\explicit t : \Prop &\quad\quad\text{by \texttt{CC-Prod} and rule $(\Type_1,\Prop,\Prop)$}\\ +\end{align*} +\begin{align*} + \rew{\Ga} \CCdash \rew{(y : \tau)\explicit (z : f|y)\explicit t} : \rew{\Prop} + &\quad\leadsto\quad \rew{\Ga} \~ (y : \tau)\erasable \rew{(z : f|y)\explicit t} : \Type\ \z\\ + &\quad\leadsto\quad \rew{\Ga} \~ (y : \tau)\erasable (z : f|y)\explicit \rew{t} : \Type\ \z\\ + &\quad\leadsto\quad \rew{\Ga} \~ (y : \tau)\erasable (z : f|y)\explicit t : \Type\ \z\\ +\end{align*} + +If we proceed acordingly on the rest of the term, we get +\begin{align*} + \mathtt{pack}\ : \quad + &(\tau : \Type\ (\s\ \z)) \erasable (f : (x : \tau) \explicit \Type\ \z) \erasable (w : \tau) \erasable (p : f| w) \explicit\\ + &(t : \Type\ \z) \erasable (b : (y : \tau) \erasable (z : f|y) \explicit t) \explicit t \{w/y\} \{p/z\}\\[10pt] + :=\ &\la (\tau : \Type\ (\s\ \z)) \erasable \la (f : (x : \tau) \explicit \Type\ \z) \erasable \la (w : \tau) \erasable \la (p : f|w) \explicit\\ + &\la (t : \Type\ \z) \erasable \la (b : (y : \tau) \erasable (z : f|y) \explicit t) \explicit b|||w|p +\end{align*} + +Finally, we can apply the extraction function and erase all but the explicit program +\begin{align*} + \mathtt{pack}\ : \quad + &\forall (\tau : \Type\ (\s\ \z)).\forall(f : (x : \tau) \explicit \Type\ \z).\forall(w : \tau).(p : f| w) \explicit\\ + &\forall(t : \Type\ \z).(b : \forall(y : \tau).(z : f|y) \explicit t) \explicit t \{w/y\} \{p/z\}\\[10pt] + :=\ &\la (p) \explicit \la (b) \explicit b|p +\end{align*} + + + +\newpage +\bibliographystyle{alpha} +\bibliography{typer_theory} +\end{document} View it on GitLab: https://gitlab.com/monnier/typer/compare/0e695aca54e25cd721768069be9b64ca8e… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/0e695aca54e25cd721768069be9b64ca8e… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Septembre 2018