Février 2017 - 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][master] * src/pexp.ml (pexp): Remove type
by Stefan 28 Fév '17

28 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: 79cd9b86 by Stefan Monnier at 2017-02-28T02:08:42-05:00 * src/pexp.ml (pexp): Remove type (pexp_location, pexp_name, pexp_parse, pexp_unparse, pexp_string) (pexp_print): Remove functions. * src/lparse.ml (pexp_fatal, pexp_error): Remove functions. - - - - - 6 changed files: - src/REPL.ml - src/debug.ml - src/debug_util.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml Changes: ===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -106,7 +106,7 @@ 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): (pdecl list * pexp list) = +let ipexp_parse (sxps: sexp list): (pdecl list * sexp list) = let rec _pxp_parse sxps dacc pacc = match sxps with | [] -> (List.rev dacc), (List.rev pacc) @@ -120,7 +120,7 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) = _pxp_parse tl (List.append (pexp_p_decls sxp) dacc) pacc (* Expression *) - | _ -> _pxp_parse tl dacc ((pexp_parse sxp)::pacc) in + | _ -> _pxp_parse tl dacc (sxp::pacc) in _pxp_parse sxps [] [] ===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -114,13 +114,13 @@ let debug_sexp_print_all tokens = (* Print a Pexp with debug info *) let debug_pexp_print ptop = print_string " "; - let l = pexp_location ptop in + let l = sexp_location ptop in let print_info msg loc pex = print_string msg; print_string "["; loc_print loc; print_string "]\t"; - pexp_print pex in - print_info (pexp_name ptop) l ptop + sexp_print pex in + print_info (sexp_name ptop) l ptop let debug_pexp_decls decls = let loc_print l = print_string "["; loc_print l; print_string "] " in @@ -130,12 +130,12 @@ let debug_pexp_decls decls = let _ = match e with | Pexpr ((l, name), pxp) -> - lalign_print_string (pexp_name pxp) 15; - loc_print l; print_string " = "; pexp_print pxp + lalign_print_string (sexp_name pxp) 15; + loc_print l; print_string " = "; sexp_print pxp | Ptype ((l, name), ptp) -> - lalign_print_string (pexp_name ptp) 15; - loc_print l; print_string " : "; pexp_print ptp + lalign_print_string (sexp_name ptp) 15; + loc_print l; print_string " : "; sexp_print ptp | Pmcall((l, op), args) -> lalign_print_string "Macro Decls" 15; ===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -218,7 +218,7 @@ let format_source () = (* merged declaration, allow us to process declaration in multiple pass *) (* first detect recursive decls then lexp decls*) type mdecl = - | Ldecl of symbol * pexp option * pexp option + | Ldecl of symbol * sexp option * sexp option | Lmcall of symbol * sexp list let lexp_detect_recursive pdecls = @@ -370,14 +370,14 @@ let main () = lalign_print_string s 20; let _ = match ptp with - | Some pxp -> pexp_print pxp; + | Some pxp -> sexp_print pxp; | None -> print_string " " in print_string "\n"; lalign_print_string s 20; let _ = match pxp with - | Some pxp -> pexp_print pxp; + | Some pxp -> sexp_print pxp; | None -> print_string " " in print_string "\n") ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -371,30 +371,30 @@ let stypecons = Symbol (U.dummy_location, "##typecons") let rec lexp_unparse lxp = match lxp with | Susp _ as e -> lexp_unparse (nosusp e) - | Imm (sexp) -> Pimm (sexp) - | Builtin ((l,name), _, _) -> Pimm (Symbol (l, "##" ^ name)) - | Var ((loc, name), _) -> Pimm (Symbol (loc, name)) + | Imm (sexp) -> sexp + | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) + | Var ((loc, name), _) -> Symbol (loc, name) | Cons (t, (l, name)) - -> Pimm (Node (sdatacons, - [pexp_unparse (lexp_unparse t); Symbol (l, name)])) + -> Node (sdatacons, + [lexp_unparse t; Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in - let st = pexp_unparse (lexp_unparse ltp) in - Pimm (Node (Symbol (l, match kind with - | Aexplicit -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol vdef; st]); - pexp_unparse (lexp_unparse body)])) + let st = lexp_unparse ltp in + Node (Symbol (l, match kind with + | Aexplicit -> "lambda_->_" + | Aimplicit -> "lambda_=>_" + | Aerasable -> "lambda_≡>_"), + [Node (Symbol (l, "_:_"), [Symbol vdef; st]); + lexp_unparse body]) | Arrow (arg_kind, vdef, ltp1, loc, ltp2) - -> let ut1 = pexp_unparse (lexp_unparse ltp1) in - Pimm (Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), - [(match vdef with None -> ut1 - | Some v -> Node (Symbol (loc, "_:_"), - [Symbol v; ut1])); - pexp_unparse (lexp_unparse ltp2)])) + -> let ut1 = lexp_unparse ltp1 in + Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" + | Aimplicit -> "_=>_" + | Aerasable -> "_≡>_"), + [(match vdef with None -> ut1 + | Some v -> Node (Symbol (loc, "_:_"), + [Symbol v; ut1])); + lexp_unparse ltp2]) | Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) @@ -403,14 +403,13 @@ let rec lexp_unparse lxp = -> Ptype (vdef, lexp_unparse ltp) :: Pexpr(vdef, lexp_unparse lxp)::acc) [] ldecls in - Pimm (Node (Symbol (loc, "let_in_"), - [pexp_u_decls pdecls; - pexp_unparse (lexp_unparse body)])) + Node (Symbol (loc, "let_in_"), + [pexp_u_decls pdecls; + lexp_unparse body]) | Call(lxp, largs) -> (* (arg_kind * lexp) list *) - let pargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in - let sargs = List.map (fun elem -> pexp_unparse elem) pargs in - Pimm (Node (pexp_unparse (lexp_unparse lxp), sargs)) + let sargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in + Node (lexp_unparse lxp, sargs) | Inductive(loc, label, lfargs, ctors) -> (* (arg_kind * vdef * ltype) list *) @@ -427,12 +426,12 @@ let rec lexp_unparse lxp = | None -> (kind, None, lexp_unparse ltp)) largs in ((loc, str), pargs) ) (SMap.bindings ctors) in - Pimm (Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - ctors)) + Node (stypecons, + Node (Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map (fun ((l,name) as s, types) + -> Node (Symbol s, + List.map pexp_u_ind_arg types)) + ctors) | Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in @@ -448,8 +447,8 @@ let rec lexp_unparse lxp = args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) - in (Ppatcons (Pimm (Node (sdatacons, - [pexp_unparse bt; Symbol (loc, str)])), + in (Ppatcons (Node (sdatacons, + [bt; Symbol (loc, str)]), pat_args), lexp_unparse bch) ) (SMap.bindings branches) in @@ -461,36 +460,33 @@ let rec lexp_unparse lxp = lexp_unparse dft)::pbranch | None -> pbranch in let e = lexp_unparse target in - Pimm (Node (Symbol (loc, "case_"), - pexp_unparse e - :: List.map - (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), - [pexp_u_pat pat; - pexp_unparse branch])) - pbranch)) + Node (Symbol (loc, "case_"), + e :: List.map + (fun (pat, branch) -> + Node (Symbol (pexp_pat_location pat, "_=>_"), + [pexp_u_pat pat; branch])) + pbranch) (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _) - -> Pimm (Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx - ^ "[" ^ subst_string subst ^ "]")) + -> Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx + ^ "[" ^ subst_string subst ^ "]") - | SortLevel (SLz) -> Pimm (Symbol (U.dummy_location, "##TypeLevel.z")) + | SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l) - -> Pimm (Node (Symbol (lexp_location l, "##TypeLevel.succ"), - [pexp_unparse (lexp_unparse l)])) + -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), + [lexp_unparse l]) | SortLevel (SLlub (l1, l2)) - -> Pimm (Node (Symbol (lexp_location l1, "##TypeLevel.∪"), - [pexp_unparse (lexp_unparse l1); - pexp_unparse (lexp_unparse l2)])) - | Sort (l, StypeOmega) -> Pimm (Symbol (l, "##Type_ω")) - | Sort (l, StypeLevel) -> Pimm (Symbol (l, "##Type_ℓ")) + -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + [lexp_unparse l1; lexp_unparse l2]) + | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (l, "##Type_ℓ") | Sort (l, Stype sl) - -> Pimm (Node (Symbol (lexp_location sl, "##Type_"), - [pexp_unparse (lexp_unparse sl)])) + -> Node (Symbol (lexp_location sl, "##Type_"), + [lexp_unparse sl]) (* FIXME: ¡Unify lexp_print and lexp_string! *) -and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) +and lexp_string lxp = sexp_string (lexp_unparse lxp) and subst_string s = match s with | S.Identity -> "Id" ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -78,8 +78,6 @@ let debug_message error_type type_name type_string loc expr message = let lexp_fatal = debug_message fatal lexp_name lexp_string let lexp_warning = debug_message warning lexp_name lexp_string let lexp_error = debug_message error lexp_name lexp_string -let pexp_fatal = debug_message fatal pexp_name pexp_string -let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string (** Builtin Macros i.e, special forms. *) @@ -246,28 +244,28 @@ let mkDummy_check loc t = newMetavar loc "dummy" t let mkDummy_infer loc = let t = newMetatype loc in (mkDummy_check loc t, t) -let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = +let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = - let tloc = pexp_location p in + let tloc = sexp_location p in (* Save current trace in a global variable. If an error occur, we will be able to retrieve the most recent trace and context. *) _global_lexp_ctx := ctx; match p with - | Pimm (Symbol (l,name)) + | Symbol (l,name) when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then let name = string_sub name 2 (String.length name) in try SMap.find name (! BI.lmap) with Not_found - -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); + -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); mkDummy_infer l - else (pexp_error l p ("Invalid special identifier `" ^ name ^ "`"); + else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); mkDummy_infer l) (* Symbol i.e identifier. *) - | Pimm (Symbol (loc, name)) + | Symbol (loc, name) when String.length name < 1 || String.get name 0 != '?' -> (try let idx = senv_lookup name ctx in @@ -278,11 +276,13 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = lxp, ltp with Not_found -> - (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); + (sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); mkDummy_infer loc)) - | Pimm (Node (func, args)) - -> let (f, t) as ft = infer (pexp_parse func) ctx in + | Node (se, []) -> infer se ctx + + | Node (func, args) + -> let (f, t) as ft = infer func ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t type_special_form) then parse_special_form ctx f args None @@ -294,20 +294,20 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args - | Pimm (Symbol (_, name)) + | Symbol (_, name) -> assert (String.length name >= 1 || String.get name 0 = '?'); - let t = newMetatype (pexp_location p) in + let t = newMetatype (sexp_location p) in let lxp = check p t ctx in (lxp, t) (* Block/String/Integer/Float. *) - | Pimm v + | v -> (mkImm (v), match v with | Integer _ -> DB.type_int | Float _ -> DB.type_float | String _ -> DB.type_string; - | _ -> pexp_error tloc p "Could not find type"; + | _ -> sexp_error tloc "Could not find type"; mkDummy_type tloc) @@ -361,8 +361,7 @@ and get_implicit_arg ctx loc name t = | _ -> value_fatal loc v "default attribute should return a sexp" in (* lparse the argument *) - let parg = pexp_parse lsarg in - check parg t ctx + check lsarg t ctx | None -> newMetavar loc name t (* Build the list of implicit arguments to instantiate. *) @@ -430,11 +429,13 @@ and unify_with_arrow ctx tloc lxp kind var aty = (mkDummy_type l, mkDummy_type l) | Some subst -> global_substitution := subst; arg, body -and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = +and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = match p with - | Pimm (Node (func, args)) - -> let (f, ft) = infer (pexp_parse func) ctx in + | Node (se, []) -> check se t ctx + + | Node (func, args) + -> let (f, ft) = infer func ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft type_special_form) then let (e, _) = parse_special_form ctx f args (Some t) in e @@ -445,10 +446,10 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = let (e, inferred_t) = infer_call ctx (f, ft) args in check_inferred ctx e inferred_t t - | Pimm (Symbol (l,"?")) -> newMetavar l "v" t - | Pimm (Symbol (l, name)) when String.length name > 1 - && String.get name 0 = '?' - -> pexp_error l p "Named metavars not supported (yet)"; + | Symbol (l,"?") -> newMetavar l "v" t + | Symbol (l, name) when String.length name > 1 + && String.get name 0 = '?' + -> sexp_error l "Named metavars not supported (yet)"; newMetavar l name t | _ -> infer_and_check p ctx t @@ -513,7 +514,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors - | _ -> lexp_error (pexp_location target) tlxp + | _ -> lexp_error (sexp_location target) tlxp ("Can't `case` on objects of this type: " ^ lexp_string tltp); SMap.empty in @@ -530,7 +531,7 @@ and check_case rtype (loc, target, ppatterns) ctx = lbranches, Some (v, lexp) in let add_branch pctor pargs = - let loc = pexp_location pctor in + let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in let meta_ctx, _ = !global_substitution in match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with @@ -563,7 +564,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match (pargs, cargs) with | (_, []) when not (SMap.is_empty pe) -> let pending = SMap.bindings pe in - pexp_error loc pctor + sexp_error loc ("Explicit pattern args `" ^ String.concat ", " (List.map (fun (l, _) -> l) pending) @@ -575,7 +576,7 @@ and check_case rtype (loc, target, ppatterns) ctx = "Too many pattern args to the constructor"; make_nctx ctx s [] [] pe acc | (_, Ppatcons (p, _))::pargs, cargs - -> lexp_error (pexp_location p) lctor + -> lexp_error (sexp_location p) lctor "Nested patterns not supported!"; make_nctx ctx s pargs cargs pe acc | (_, (ak, Some (_, fname), fty)::cargs) @@ -596,13 +597,12 @@ and check_case rtype (loc, target, ppatterns) ctx = | ((Some (l, fname), fpat)::pargs, cargs) -> let var = match fpat with Ppatsym v -> Some v | _ -> None in if SMap.mem fname pe then - pexp_error l pctor - ("Duplicate explicit field `" ^ fname ^ "`"); + sexp_error l ("Duplicate explicit field `" ^ fname ^ "`"); make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in if ak = Aexplicit then - pexp_error loc pctor + sexp_error loc ("Missing pattern for normal field" ^ (match fname with Some (_,n) -> " `" ^ n ^ "`" | _ -> "")); @@ -628,7 +628,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match OL.lexp_whnf (mkVar (var, idx)) (ectx_to_lctx ctx) meta_ctx with | Cons _ (* It's indeed a constructor! *) - -> add_branch (Pimm (Symbol var)) [] + -> add_branch (Symbol var) [] | _ -> add_default (Some var) (* A named default branch. *) with Not_found -> add_default (Some var)) @@ -646,13 +646,7 @@ and handle_macro_call ctx func args t = | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in - let pxp = try pexp_parse sxp - with e -> - error dloc "An error occurred while expanding a macro"; - sexp_print sxp; - raise e in - - check pxp t ctx + check sxp t ctx (* Identify Call Type and return processed call. *) and infer_call ctx (func, ltp) (sargs: sexp list) = @@ -670,8 +664,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in - let parg = pexp_parse sarg in - let larg = check parg arg_type ctx in + let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (SMap.remove aname pending) (L.mkSusp ret_type (S.substitute larg)) @@ -680,8 +673,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = Arrow (ak, _, arg_type, _, ret_type) when (aname = "_") (* Explicit-implicit argument. *) - -> let parg = pexp_parse sarg in - let larg = check parg arg_type ctx in + -> let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) @@ -724,8 +716,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = largs, ltp | sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) - -> let parg = pexp_parse sarg in - let larg = check parg arg_type ctx in + -> let larg = check sarg arg_type ctx in handle_fun_args ((Aexplicit, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) @@ -741,7 +732,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = - let make_args (args:(arg_kind * pvar option * pexp) list) ctx + let make_args (args:(arg_kind * pvar option * sexp) list) ctx : (arg_kind * vname option * ltype) list = let rec loop args acc ctx = match args with @@ -826,7 +817,7 @@ and sexp_decls_macro_print sxp_decls = | e -> sexp_print e; print_string "\n" and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = - try let lxp, ltp = infer (Pimm (Symbol (loc, mname))) ctx in + try let lxp, ltp = infer (Symbol (loc, mname)) ctx in (* FIXME: Check that (conv_p ltp Macro)! *) let ret = lexp_expand_macro loc lxp sargs ctx None in @@ -847,7 +838,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) - (defs : (vname * pexp * ltype) list) + (defs : (vname * sexp * ltype) list) : (vname * lexp * ltype) list * elab_context = let (declmap, nctx) = List.fold_right @@ -873,7 +864,7 @@ and lexp_decls_1 (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) - (pending_defs : (vname * pexp * ltype) list) (* Pending definitions. *) + (pending_defs : (vname * sexp * ltype) list) (* Pending definitions. *) : (vname * lexp * ltype) list * pdecl list * elab_context = match pdecls with @@ -947,11 +938,11 @@ and lexp_p_decls pdecls ctx: ((vname * lexp * ltype) list list * elab_context) = let declss, nnctx = lexp_p_decls pdecls nctx in decls :: declss, nnctx -and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list = +and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = List.map (fun pe -> let e, _ = infer pe ctx in e) p and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = - let e, _ = infer (pexp_parse e) ctx in e + let e, _ = infer e ctx in e (* -------------------------------------------------------------------------- * Special forms implementation @@ -959,8 +950,7 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = and sform_new_attribute ctx loc sargs ot = match sargs with - | [t] -> let ptp = pexp_parse t in - let ltp = infer_type ptp ctx None in + | [t] -> let ltp = infer_type t ctx None in let meta_ctx, _ = !global_substitution in (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` * is False, for example): Should be a type like `AttributeMap t` @@ -1048,8 +1038,7 @@ 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 | true, [String (_, name); stp] - -> let ptp = pexp_parse stp in - let ltp = infer_type ptp ctx None in + -> let ltp = infer_type stp ctx None in let meta_ctx, _ = !global_substitution in let ltp' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp in let bi = mkBuiltin ((loc, name), ltp', None) in @@ -1067,8 +1056,7 @@ let sform_built_in ctx loc sargs ot = let sform_datacons ctx loc sargs ot = match sargs with | [t; Symbol ((sloc, cname) as sym)] - -> let pt = pexp_parse t in - let idt, _ = infer pt ctx in + -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy) | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; @@ -1122,10 +1110,8 @@ let sform_typecons ctx loc sargs ot = let sform_hastype ctx loc sargs ot = match sargs with - | [se; st] -> let pe = pexp_parse se in - let pt = pexp_parse st in - let lt = infer_type pt ctx None in - let le = check pe lt ctx in + | [se; st] -> let lt = infer_type st ctx None in + let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; sform_dummy_ret loc @@ -1136,11 +1122,9 @@ let sform_arrow kind ctx loc sargs ot = -> let (v, st1) = match st1 with | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (Some v, st1) | _ -> (None, st1) in - let pt1 = pexp_parse st1 in - let pt2 = pexp_parse st2 in - let lt1 = infer_type pt1 ctx v in + let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type pt2 nctx None in + let lt2 = infer_type st2 nctx None in (mkArrow (kind, v, lt1, loc, lt2), Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret loc @@ -1156,10 +1140,9 @@ let sform_lambda kind ctx loc sargs ot' = match sargs with | [sargs; sbody] -> let sargs = sexp_p_list sargs ["_:_"] in - let pbody = pexp_parse sbody in let rec do_all_args sargs ctx ot = match sargs with - | [] -> elaborate ctx pbody ot + | [] -> elaborate ctx sbody ot | sarg :: sargs -> let (arg, ost1) = match sarg with | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st) @@ -1169,7 +1152,7 @@ let sform_lambda kind ctx loc sargs ot' = ((dummy_location, "_"), None) in let olt1 = match ost1 with - | Some st -> Some (infer_type (pexp_parse st) ctx (Some arg)) + | Some st -> Some (infer_type st ctx (Some arg)) | _ -> None in let lt1, olt2 = @@ -1214,14 +1197,13 @@ let rec sform_case ctx loc sargs ot = match sargs with | [Node (Symbol (_, "_|_"), se :: scases)] -> let parse_case branch = match branch with | Node (Symbol (_, "_=>_"), [pat; code]) - -> (pexp_p_pat pat, pexp_parse code) + -> (pexp_p_pat pat, code) | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; - (Ppatany l, Pimm (Symbol (l, "?"))) in - let pe = pexp_parse se in + (Ppatany l, Symbol (l, "?")) in let pcases = List.map parse_case scases in let t = match ot with Some t -> t | None -> newMetatype loc in - let le = check_case t (loc, pe, pcases) ctx in + let le = check_case t (loc, se, pcases) ctx in (le, match ot with Some _ -> Checked | None -> Inferred t) (* In case there are no branches, pretend there was a | anyway. *) @@ -1232,10 +1214,9 @@ let rec sform_case ctx loc sargs ot = match sargs with let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] -> let pdecls = pexp_p_decls sdecls in - let pbody = pexp_parse sbody in let declss, nctx = lexp_p_decls pdecls ctx in (* FIXME: Use `elaborate`. *) - let bdy, ltp = infer pbody nctx in + let bdy, ltp = infer sbody nctx in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in (lexp_let_decls declss bdy nctx, Inferred (mkSusp ltp s)) @@ -1250,8 +1231,7 @@ let sform_letin ctx loc sargs ot = match sargs with * allow such a lambda. *) let sform_type ctx loc sargs ot = match sargs with - | [l] -> let l = pexp_parse l in - let l, _ = infer l ctx in + | [l] -> let l, _ = infer l ctx in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) | _ -> sexp_error loc "##Type_ expects one argument"; ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -36,78 +36,55 @@ type pvar = symbol (* type sort = Type | Ext *) (* type tag = string *) -type pexp = - (* | Psort of location * sort *) - | Pimm of sexp (* Used for strings, ... *) - and ppat = (* This data type allows nested patterns, but in reality we don't * support them. I.e. we don't want Ppatcons within Ppatcons. *) | Ppatany of location | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *) - | Ppatcons of pexp * (symbol option * ppat) list + | Ppatcons of sexp * (symbol option * ppat) list and pdecl = - | Ptype of symbol * pexp (* identifier : expr *) - | Pexpr of symbol * pexp (* identifier = expr *) + | Ptype of symbol * sexp (* identifier : expr *) + | Pexpr of symbol * sexp (* identifier = expr *) | Pmcall of symbol * sexp list (* identifier [sexp] *) -let rec pexp_location e = - match e with - (* | Psort (l,_) -> l *) - | Pimm s -> sexp_location s - -let pexp_name e = - match e with - | Pimm _ -> "Pimm" - let rec pexp_pat_location e = match e with | Ppatany l -> l | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> pexp_location e - -(* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp" - * and "pexp_u" is the prefix for "unparse a pexp, returning a sexp". *) -let rec pexp_parse (s : sexp) : pexp = - match s with - (* This is an internal error because Epsilon does not have any location - * information so it needs to be caught elsewhere. *) - | (Block _ | Integer _ | Float _ | String _ | Symbol _) -> Pimm s - | Node (f, []) -> pexp_parse f - | Node _ -> Pimm s - -and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = + | Ppatcons (e, _) -> sexp_location e + +and pexp_p_actual_arg arg : (arg_kind * pvar option * sexp) = match arg with | Node (Symbol (_, ":≡"), [Symbol s; e]) - -> (Aerasable, Some s, pexp_parse e) + -> (Aerasable, Some s, e) | Node (Symbol (_, ":="), [Symbol s; e]) - -> (Aimplicit, Some s, pexp_parse e) + -> (Aimplicit, Some s, e) | Node (Symbol (_, ":-"), [Symbol s; e]) - -> (Aexplicit, Some s, pexp_parse e) - | e -> (Aexplicit, None, pexp_parse e) + -> (Aexplicit, Some s, e) + | e -> (Aexplicit, None, e) -and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = +and pexp_p_formal_arg arg : (arg_kind * pvar * sexp option) = match arg with | Node (Symbol (_, "_:::_"), [Symbol s; e]) - -> (Aerasable, s, Some (pexp_parse e)) + -> (Aerasable, s, Some e) | Node (Symbol (_, "_::_"), [Symbol s; e]) - -> (Aimplicit, s, Some (pexp_parse e)) + -> (Aimplicit, s, Some e) | Node (Symbol (_, "_:_"), [Symbol s; e]) - -> (Aexplicit, s, Some (pexp_parse e)) + -> (Aexplicit, s, Some e) | Symbol s -> (Aexplicit, s, None) | _ -> sexp_print arg; (pexp_error (sexp_location arg) "Unrecognized formal arg"); (Aexplicit, (sexp_location arg, "{arg}"), None) -and pexp_u_formal_arg (arg : arg_kind * pvar * pexp option) = +and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with | (Aexplicit, s, None) -> Symbol s | (ak, ((l,_) as s), t) -> Node (Symbol (l, match ak with Aerasable -> ":::" | Aimplicit -> "::" | Aexplicit -> ":"), - [Symbol s; match t with Some e -> pexp_unparse e + [Symbol s; match t with Some e -> e | None -> Symbol (l, "_")]) and pexp_p_id (x : location * string) : (location * string) option = @@ -122,21 +99,21 @@ and pexp_u_id (x : (location * string) option) : (location * string) = and pexp_p_ind_arg s = match s with | Node (Symbol (_,"_:_"), [Symbol s; t]) - -> (Aexplicit, pexp_p_id s, pexp_parse t) + -> (Aexplicit, pexp_p_id s, t) | Node (Symbol (_,"_::_"), [Symbol s; t]) - -> (Aimplicit, pexp_p_id s, pexp_parse t) + -> (Aimplicit, pexp_p_id s, t) | Node (Symbol (_,"_:::_"), [Symbol s; t]) - -> (Aerasable, pexp_p_id s, pexp_parse t) - | _ -> (Aexplicit, None, pexp_parse s) + -> (Aerasable, pexp_p_id s, t) + | _ -> (Aexplicit, None, s) and pexp_u_ind_arg arg = match arg with - | (Aexplicit, None, t) -> pexp_unparse t + | (Aexplicit, None, t) -> t | (k, s, t) -> let (l,_) as id = pexp_u_id s in Node (Symbol (l, match k with Aexplicit -> "_:_" | Aimplicit -> "_::_" | Aerasable -> "_:::_"), - [Symbol id; pexp_unparse t]) + [Symbol id; t]) and pexp_p_pat_arg (s : sexp) = match s with | Symbol _ -> (None, pexp_p_pat s) @@ -158,28 +135,28 @@ and pexp_p_pat (s : sexp) : ppat = match s with | Symbol (l, "_") -> Ppatany l | Symbol s -> Ppatsym s | Node (c, args) - -> Ppatcons (pexp_parse c, List.map pexp_p_pat_arg args) + -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in pexp_error l "Unknown pattern"; Ppatany l and pexp_u_pat (p : ppat) : sexp = match p with | Ppatany l -> Symbol (l, "_") | Ppatsym s -> Symbol s - | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args) + | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args) and pexp_p_decls e: pdecl list = match e with | Symbol (_, "") -> [] | Node (Symbol (_, ("_;_" | "_;" | ";_")), decls) -> List.concat (List.map pexp_p_decls decls) - | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] - | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, pexp_parse t)] + | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, t)] + | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, t)] | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> - [Pexpr(s, Pimm (Node (Symbol (sexp_location d, "lambda_->_"), - [(match args with - | [] -> Sexp.dummy_epsilon - | arg::args -> Node (arg, args)); - t])))] + [Pexpr (s, Node (Symbol (sexp_location d, "lambda_->_"), + [(match args with + | [] -> Sexp.dummy_epsilon + | arg::args -> Node (arg, args)); + t]))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) @@ -188,19 +165,13 @@ and pexp_p_decls e: pdecl list = print_string ((sexp_name e) ^ ": \""); sexp_print e; print_string "\"\n"; pexp_error (sexp_location e) ("Unknown declaration"); [] -and pexp_unparse (e : pexp) : sexp = - match e with - (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) - (* | Psort (l,Type) -> Symbol (l, "%Type%") *) - | Pimm s -> s - and pexp_u_decl decl = match decl with | Pexpr (s, v) -> - Node (Symbol (dummy_location, "_=_"), [Symbol s; pexp_unparse v]) + Node (Symbol (dummy_location, "_=_"), [Symbol s; v]) | Ptype (s, v) -> - Node (Symbol (dummy_location, "_:_"), [Symbol s; pexp_unparse v]) + Node (Symbol (dummy_location, "_:_"), [Symbol s; v]) | Pmcall(s, args) -> Node (Symbol s, args) @@ -212,13 +183,6 @@ and pexp_u_decls (ds: pdecl list) = | _ -> Node (Symbol (dummy_location, "_;_"), List.map pexp_u_decl ds) -and pexp_string e = sexp_string (pexp_unparse e) -and pexp_print e = print_string (pexp_string e) - -(* Parse All Pexp as a list *) -let pexp_parse_all (nodes: sexp list) = - List.map pexp_parse nodes - let pexp_decls_all (nodes: sexp list): pdecl list = let rec loop nodes acc = match nodes with @@ -235,8 +199,7 @@ let pexp_decls_all (nodes: sexp list): pdecl list = (* Lexp helper *) let _pexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) = - let sxps = _sexp_parse_str str tenv grm limit in - pexp_parse_all sxps + _sexp_parse_str str tenv grm limit (* specialized version *) let pexp_expr_str str = View it on GitLab: https://gitlab.com/monnier/typer/commit/79cd9b8661fb7d5b4a83e698d1b45f1b52d…

1 0

[Git][monnier/typer][master] * src/lparse.ml (sform_letin): New function
by Stefan 28 Fév '17

28 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: 69727028 by Stefan Monnier at 2017-02-28T01:45:03-05:00 * src/lparse.ml (sform_letin): New function (register_special_forms): Register it. * src/pexp.ml (pexp): Remove Plet. - - - - - 4 changed files: - src/lexp.ml - src/lparse.ml - src/pexp.ml - − tests/pexp_test.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -403,7 +403,9 @@ let rec lexp_unparse lxp = -> Ptype (vdef, lexp_unparse ltp) :: Pexpr(vdef, lexp_unparse lxp)::acc) [] ldecls in - Plet (loc, pdecls, lexp_unparse body) + Pimm (Node (Symbol (loc, "let_in_"), + [pexp_u_decls pdecls; + pexp_unparse (lexp_unparse body)])) | Call(lxp, largs) -> (* (arg_kind * lexp) list *) let pargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -281,14 +281,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); mkDummy_infer loc)) - (* Let, Variable declaration + local scope. *) - | Plet (loc, decls, body) - -> let declss, nctx = lexp_p_decls decls ctx in - let bdy, ltp = infer body nctx in - let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in - (lexp_let_decls declss bdy nctx), - mkSusp ltp s - | Pimm (Node (func, args)) -> let (f, t) as ft = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in @@ -1237,6 +1229,18 @@ let rec sform_case ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized case expression"; sform_dummy_ret loc +let sform_letin ctx loc sargs ot = match sargs with + | [sdecls; sbody] + -> let pdecls = pexp_p_decls sdecls in + let pbody = pexp_parse sbody in + let declss, nctx = lexp_p_decls pdecls ctx in + (* FIXME: Use `elaborate`. *) + let bdy, ltp = infer pbody nctx in + let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in + (lexp_let_decls declss bdy nctx, + Inferred (mkSusp ltp s)) + | _ -> sexp_error loc "Unrecognized let_in_ expression"; + sform_dummy_ret loc (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1286,6 +1290,7 @@ let register_special_forms () = ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable); ("case_", sform_case); + ("let_in_", sform_letin); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -39,7 +39,6 @@ type pvar = symbol type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) - | Plet of location * pdecl list * pexp and ppat = (* This data type allows nested patterns, but in reality we don't @@ -58,12 +57,10 @@ let rec pexp_location e = match e with (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s - | Plet (l, _, _) -> l let pexp_name e = match e with | Pimm _ -> "Pimm" - | Plet (_, _, _) -> "Plet" let rec pexp_pat_location e = match e with | Ppatany l -> l @@ -77,11 +74,6 @@ let rec pexp_parse (s : sexp) : pexp = (* This is an internal error because Epsilon does not have any location * information so it needs to be caught elsewhere. *) | (Block _ | Integer _ | Float _ | String _ | Symbol _) -> Pimm s - (* let *) - | Node (Symbol (start, "let_in_"), [decls; body]) - -> Plet (start, pexp_p_decls decls, pexp_parse body) - | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) - -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) | Node (f, []) -> pexp_parse f | Node _ -> Pimm s @@ -201,9 +193,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s - | Plet (start, decls, body) -> - Node (Symbol (start, "let_in_"), - [pexp_u_decls decls; pexp_unparse body]) and pexp_u_decl decl = match decl with ===================================== tests/pexp_test.ml deleted ===================================== --- a/tests/pexp_test.ml +++ /dev/null @@ -1,22 +0,0 @@ -open Pexp -open Utest_lib - - -let _ = (add_test "PEXP" "Type Parsing" (fun () -> - - let dcode = " - let a : Nat; a = 1; b : Nat; b = 3; in a + b;" in - - let ret = pexp_expr_str dcode in - match ret with - | [expr] ->( - match expr with - | Plet(_, arg, _) -> (match arg with - | Ptype(_, tp)::_ ->success () - | _ -> failure ()) - | _ -> failure ()) - | _ -> failure ()) -) - - -let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/commit/6972702846972e9a2ca16c311f3abdf503f…

1 0

[Git][monnier/typer][master] * src/lparse.ml (sform_case): New function
by Stefan 28 Fév '17

28 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: 61d04393 by Stefan Monnier at 2017-02-28T01:34:25-05:00 * src/lparse.ml (sform_case): New function (register_special_forms): Register it. * src/pexp.ml (pexp): Remove Pcase. - - - - - 3 changed files: - src/lexp.ml - src/lparse.ml - src/pexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -458,7 +458,15 @@ let rec lexp_unparse lxp = | Some vdef -> Ppatsym vdef), lexp_unparse dft)::pbranch | None -> pbranch - in Pcase (loc, lexp_unparse target, pbranch) + in let e = lexp_unparse target in + Pimm (Node (Symbol (loc, "case_"), + pexp_unparse e + :: List.map + (fun (pat, branch) -> + Node (Symbol (pexp_pat_location pat, "_=>_"), + [pexp_u_pat pat; + pexp_unparse branch])) + pbranch)) (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -302,8 +302,9 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args - | (Pcase _ | Pimm (Symbol _)) - -> let t = newMetatype (pexp_location p) in + | Pimm (Symbol (_, name)) + -> assert (String.length name >= 1 || String.get name 0 = '?'); + let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t) @@ -440,9 +441,6 @@ and unify_with_arrow ctx tloc lxp kind var aty = and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = match p with - | Pcase (loc, target, branches) - -> check_case t (loc, target, branches) ctx - | Pimm (Node (func, args)) -> let (f, ft) = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in @@ -1220,6 +1218,26 @@ let sform_lambda kind ctx loc sargs ot' = | _ -> sexp_error loc "##lambda_->_ takes two arguments"; sform_dummy_ret loc +let rec sform_case ctx loc sargs ot = match sargs with + | [Node (Symbol (_, "_|_"), se :: scases)] + -> let parse_case branch = match branch with + | Node (Symbol (_, "_=>_"), [pat; code]) + -> (pexp_p_pat pat, pexp_parse code) + | _ -> let l = (sexp_location branch) in + sexp_error l "Unrecognized simple case branch"; + (Ppatany l, Pimm (Symbol (l, "?"))) in + let pe = pexp_parse se in + let pcases = List.map parse_case scases in + let t = match ot with Some t -> t | None -> newMetatype loc in + let le = check_case t (loc, pe, pcases) ctx in + (le, match ot with Some _ -> Checked | None -> Inferred t) + + (* In case there are no branches, pretend there was a | anyway. *) + | [e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot + | _ -> sexp_error loc "Unrecognized case expression"; + sform_dummy_ret loc + + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1267,6 +1285,7 @@ let register_special_forms () = ("_->_", sform_arrow Aexplicit); ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable); + ("case_", sform_case); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,9 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Plet of location * pdecl list * pexp - (* The symbols are only used so that we can distinguish two - * otherwise isomorphic types. *) - | Pcase of location * pexp * (ppat * pexp) list and ppat = (* This data type allows nested patterns, but in reality we don't @@ -62,13 +59,11 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Pcase (l, _, _) -> l let pexp_name e = match e with | Pimm _ -> "Pimm" | Plet (_, _, _) -> "Plet" - | Pcase (_, _, _) -> "Pcase" let rec pexp_pat_location e = match e with | Ppatany l -> l @@ -87,21 +82,6 @@ let rec pexp_parse (s : sexp) : pexp = -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) - (* cases analysis *) - | Node (Symbol (start, "case_"), - [Node (Symbol (_, "_|_"), e :: cases)]) - -> let parse_case branch = match branch with - | Node (Symbol (_, "_=>_"), [pat; code]) - -> (pexp_p_pat pat, pexp_parse code) - | _ -> let l = (sexp_location branch) in - pexp_error l "Unrecognized simple case branch"; - (Ppatany l, Pimm (Symbol (l, "?"))) - in Pcase (start, pexp_parse e, List.map parse_case cases) - | Node (Symbol (start, "case_"), [e]) -> Pcase (start, pexp_parse e, []) - | Node (Symbol (start, "case_"), _) - -> pexp_error start "Unrecognized case expression"; - Pimm (Symbol (start, "?")) - (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f | Node _ -> Pimm s @@ -224,15 +204,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Pcase (start, e, branches) -> - Node (Symbol (start, "case_"), - pexp_unparse e - :: List.map - (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), - [pexp_u_pat pat; - pexp_unparse branch])) - branches) and pexp_u_decl decl = match decl with View it on GitLab: https://gitlab.com/monnier/typer/commit/61d04393f190f3b7f9fce40a0819621e3d9…

1 0

[Git][monnier/typer][master] * src/pexp.ml (pexp): Remove Pcall
by Stefan 28 Fév '17

28 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: 5aff0bb4 by Stefan Monnier at 2017-02-28T01:11:29-05:00 * src/pexp.ml (pexp): Remove Pcall Use `Pimm (Node ..)` instead. - - - - - 3 changed files: - src/lexp.ml - src/lparse.ml - src/pexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -364,8 +364,8 @@ let lexp_name e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel" -let pdatacons = Pimm (Symbol (U.dummy_location, "##datacons")) -let ptypecons = Pimm (Symbol (U.dummy_location, "##typecons")) +let sdatacons = Symbol (U.dummy_location, "##datacons") +let stypecons = Symbol (U.dummy_location, "##typecons") (* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = @@ -375,7 +375,8 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _, _) -> Pimm (Symbol (l, "##" ^ name)) | Var ((loc, name), _) -> Pimm (Symbol (loc, name)) | Cons (t, (l, name)) - -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) + -> Pimm (Node (sdatacons, + [pexp_unparse (lexp_unparse t); Symbol (l, name)])) | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in let st = pexp_unparse (lexp_unparse ltp) in @@ -407,7 +408,7 @@ let rec lexp_unparse lxp = | Call(lxp, largs) -> (* (arg_kind * lexp) list *) let pargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in let sargs = List.map (fun elem -> pexp_unparse elem) pargs in - Pcall(lexp_unparse lxp, sargs) + Pimm (Node (pexp_unparse (lexp_unparse lxp), sargs)) | Inductive(loc, label, lfargs, ctors) -> (* (arg_kind * vdef * ltype) list *) @@ -424,12 +425,12 @@ let rec lexp_unparse lxp = | None -> (kind, None, lexp_unparse ltp)) largs in ((loc, str), pargs) ) (SMap.bindings ctors) in - Pcall (ptypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - ctors) + Pimm (Node (stypecons, + Node (Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map (fun ((l,name) as s, types) + -> Node (Symbol s, + List.map pexp_u_ind_arg types)) + ctors)) | Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in @@ -445,8 +446,8 @@ let rec lexp_unparse lxp = args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) - in (Ppatcons (Pcall (pdatacons, - [pexp_unparse bt; Symbol (loc, str)]), + in (Ppatcons (Pimm (Node (sdatacons, + [pexp_unparse bt; Symbol (loc, str)])), pat_args), lexp_unparse bch) ) (SMap.bindings branches) in @@ -466,16 +467,17 @@ let rec lexp_unparse lxp = | SortLevel (SLz) -> Pimm (Symbol (U.dummy_location, "##TypeLevel.z")) | SortLevel (SLsucc l) - -> Pcall (Pimm (Symbol (lexp_location l, "##TypeLevel.succ")), - [pexp_unparse (lexp_unparse l)]) + -> Pimm (Node (Symbol (lexp_location l, "##TypeLevel.succ"), + [pexp_unparse (lexp_unparse l)])) | SortLevel (SLlub (l1, l2)) - -> Pcall (Pimm (Symbol (lexp_location l1, "##TypeLevel.∪")), - [pexp_unparse (lexp_unparse l1); pexp_unparse (lexp_unparse l2)]) + -> Pimm (Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + [pexp_unparse (lexp_unparse l1); + pexp_unparse (lexp_unparse l2)])) | Sort (l, StypeOmega) -> Pimm (Symbol (l, "##Type_ω")) | Sort (l, StypeLevel) -> Pimm (Symbol (l, "##Type_ℓ")) | Sort (l, Stype sl) - -> Pcall (Pimm (Symbol (lexp_location sl, "##Type_")), - [pexp_unparse (lexp_unparse sl)]) + -> Pimm (Node (Symbol (lexp_location sl, "##Type_"), + [pexp_unparse (lexp_unparse sl)])) (* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -289,14 +289,14 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = (lexp_let_decls declss bdy nctx), mkSusp ltp s - | Pcall (func, args) - -> let (f, t) as ft = infer func ctx in + | Pimm (Node (func, args)) + -> let (f, t) as ft = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t type_special_form) then parse_special_form ctx f args None else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then - let t = newMetatype (pexp_location func) in + let t = newMetatype (sexp_location func) in let lxp = handle_macro_call ctx f args t in (lxp, t) else @@ -443,8 +443,8 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = | Pcase (loc, target, branches) -> check_case t (loc, target, branches) ctx - | Pcall (func, args) - -> let (f, ft) = infer func ctx in + | Pimm (Node (func, args)) + -> let (f, ft) = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft type_special_form) then let (e, _) = parse_special_form ctx f args (Some t) in e ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,7 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Plet of location * pdecl list * pexp - | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two * otherwise isomorphic types. *) | Pcase of location * pexp * (ppat * pexp) list @@ -63,14 +62,12 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l let pexp_name e = match e with | Pimm _ -> "Pimm" | Plet (_, _, _) -> "Plet" - | Pcall (_, _) -> "Pcall" | Pcase (_, _, _) -> "Pcase" let rec pexp_pat_location e = match e with @@ -106,7 +103,7 @@ let rec pexp_parse (s : sexp) : pexp = Pimm (Symbol (start, "?")) (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f - | Node (f, args) -> Pcall (pexp_parse f, args) + | Node _ -> Pimm s and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = match arg with @@ -206,11 +203,11 @@ and pexp_p_decls e: pdecl list = | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, pexp_parse t)] | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> - [Pexpr(s, Pcall (Pimm (Symbol (sexp_location d, "lambda_->_")), - [(match args with - | [] -> Sexp.dummy_epsilon - | arg::args -> Node (arg, args)); - t]))] + [Pexpr(s, Pimm (Node (Symbol (sexp_location d, "lambda_->_"), + [(match args with + | [] -> Sexp.dummy_epsilon + | arg::args -> Node (arg, args)); + t])))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) @@ -227,7 +224,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Pcall (f, args) -> Node (pexp_unparse f, args) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"), pexp_unparse e View it on GitLab: https://gitlab.com/monnier/typer/commit/5aff0bb40c62d4c7e80762cad3e0bf324a9…

1 0

[Git][monnier/typer][master] * src/lparse.ml (sform_lambda): New function
by Stefan 28 Fév '17

28 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: b3b5b11f by Stefan Monnier at 2017-02-28T00:59:56-05:00 * src/lparse.ml (sform_lambda): New function (parse_special_form): Pass `ot` to the special form. (elaborate): New function. (register_special_forms): Register it under all three names. * src/pexp.ml (pexp): Remove Plambda. - - - - - 3 changed files: - src/lexp.ml - src/lparse.ml - src/pexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -376,8 +376,15 @@ let rec lexp_unparse lxp = | Var ((loc, name), _) -> Pimm (Symbol (loc, name)) | Cons (t, (l, name)) -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) - | Lambda (kind, vdef, ltp, body) -> - Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body) + | Lambda (kind, vdef, ltp, body) + -> let l = lexp_location lxp in + let st = pexp_unparse (lexp_unparse ltp) in + Pimm (Node (Symbol (l, match kind with + | Aexplicit -> "lambda_->_" + | Aimplicit -> "lambda_=>_" + | Aerasable -> "lambda_≡>_"), + [Node (Symbol (l, "_:_"), [Symbol vdef; st]); + pexp_unparse (lexp_unparse body)])) | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> let ut1 = pexp_unparse (lexp_unparse ltp1) in Pimm (Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -289,16 +289,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = (lexp_let_decls declss bdy nctx), mkSusp ltp s - (* This case can be inferred. *) - | Plambda (kind, var, Some ptype, body) - -> let ltp = infer_type ptype ctx (Some var) in - - let nctx = env_extend ctx var Variable ltp in - let lbody, lbtp = infer body nctx in - - let lambda_type = mkArrow (kind, Some var, ltp, tloc, lbtp) in - mkLambda(kind, var, ltp, lbody), lambda_type - | Pcall (func, args) -> let (f, t) as ft = infer func ctx in let meta_ctx, _ = !global_substitution in @@ -312,7 +302,7 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args - | (Plambda _ | Pcase _ | Pimm (Symbol _)) + | (Pcase _ | Pimm (Symbol _)) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t) @@ -334,7 +324,7 @@ and parse_special_form ctx f args ot = match OL.lexp_whnf f (ectx_to_lctx ctx) meta_ctx with | Builtin ((_, name), _, _) -> (* Special form. *) - let (e, ot') = (get_special_form name) ctx loc args None in + let (e, ot') = (get_special_form name) ctx loc args ot in (* `ot` is None if we're inferring and `Some t` if we're checking. *) (match (ot, ot') with | (Some t, Checked) -> (e, t) @@ -425,22 +415,15 @@ and lexp_let_decls declss (body: lexp) ctx = List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body -and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = - - let tloc = pexp_location p in - - (* Safe current trace in a global variable. If an error occur, - we will be able to retrieve the most recent trace and context *) - _global_lexp_ctx := ctx; - - let unify_with_arrow lxp kind var aty subst = +and unify_with_arrow ctx tloc lxp kind var aty = let body = newMetatype tloc in let arg = match aty with | None -> newMetatype tloc | Some laty -> laty in let l, _ = var in let arrow = mkArrow (kind, Some var, arg, l, body) in - match Unif.unify arrow lxp (ectx_to_lctx ctx) subst with + let meta_ctx, _ = !global_substitution in + match Unif.unify arrow lxp (ectx_to_lctx ctx) meta_ctx with | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " ^ lexp_string arrow @@ -454,39 +437,9 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = (mkDummy_type l, mkDummy_type l) | Some subst -> global_substitution := subst; arg, body - in - let infer_lambda_body kind var def_arg_type body subst = - (* Check argument type annotation, if any. *) - let def_arg_type = match def_arg_type with - | Some def_arg_type - -> Some (infer_type def_arg_type ctx (Some var)) - | _ -> None in +and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = - (* Read var type from the provided type *) - let meta_ctx, _ = !global_substitution in - let given_arg_type, given_body_type = - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with - | Arrow(kind, _, ltp, _, lbtp) - -> (match def_arg_type with - | None -> () - | Some def_arg_type - -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) def_arg_type ltp) then - lexp_error (lexp_location def_arg_type) def_arg_type - ("Type mismatch! Context expected `" - ^ lexp_string ltp ^ "`")); - ltp, lbtp - | lxp -> unify_with_arrow lxp kind var def_arg_type subst in - - let nctx = env_extend ctx var Variable given_arg_type in - let lbody = check body given_body_type nctx in - mkLambda (kind, var, given_arg_type, lbody) - - in - let subst, _ = !global_substitution in match p with - | Plambda (kind, var, def_arg_type, body) - -> infer_lambda_body kind var def_arg_type body subst - | Pcase (loc, target, branches) -> check_case t (loc, target, branches) ctx @@ -1202,6 +1155,71 @@ let sform_arrow kind ctx loc sargs ot = | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret loc +(* Infer or check, as the case may be. *) +let elaborate ctx pe ot = + match ot with + | Some t -> (check pe t ctx, Checked) + | None -> let (le, lt) = infer pe ctx in + (le, Inferred lt) + +let sform_lambda kind ctx loc sargs ot' = + match sargs with + | [sargs; sbody] + -> let sargs = sexp_p_list sargs ["_:_"] in + let pbody = pexp_parse sbody in + + let rec do_all_args sargs ctx ot = match sargs with + | [] -> elaborate ctx pbody ot + | sarg :: sargs + -> let (arg, ost1) = match sarg with + | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st) + | Symbol arg -> (arg, None) + | _ -> sexp_error (sexp_location sarg) + "Unrecognized lambda argument"; + ((dummy_location, "_"), None) in + + let olt1 = match ost1 with + | Some st -> Some (infer_type (pexp_parse st) ctx (Some arg)) + | _ -> None in + + let lt1, olt2 = + match ot with + | None -> ((match olt1 with + | Some lt1 -> lt1 + | None -> newMetatype loc), + None) + (* Read var type from the provided type *) + | Some t + -> let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind + -> (match olt1 with + | None -> () + | Some lt1' + -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) lt1 lt1') + then lexp_error (lexp_location lt1') lt1' + ("Type mismatch! Context expected `" + ^ lexp_string lt1 ^ "`")); + (lt1, Some lt2) + (* FIXME: If `t` is an implicit arrow and `kind` is Aexplicit, + * then auto-add a corresponding Lambda wrapper! *) + | lt + -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 + in (lt1, Some lt2) in + + let nctx = env_extend ctx arg Variable lt1 in + let (lbody, alt) = do_all_args sargs nctx olt2 in + (mkLambda (kind, arg, lt1, lbody), + match alt with + | Lazy -> Lazy + | Checked -> Checked + | Inferred lt2 + -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))) in + + do_all_args sargs ctx ot' + | _ -> sexp_error loc "##lambda_->_ takes two arguments"; + sform_dummy_ret loc + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1243,6 +1261,9 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("lambda_->_", sform_lambda Aexplicit); + ("lambda_=>_", sform_lambda Aimplicit); + ("lambda_≡>_", sform_lambda Aerasable); ("_->_", sform_arrow Aexplicit); ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable); ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,7 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Plet of location * pdecl list * pexp - | Plambda of arg_kind * pvar * pexp option * pexp | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two * otherwise isomorphic types. *) @@ -64,7 +63,6 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l @@ -72,7 +70,6 @@ let pexp_name e = match e with | Pimm _ -> "Pimm" | Plet (_, _, _) -> "Plet" - | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" | Pcase (_, _, _) -> "Pcase" @@ -93,26 +90,6 @@ let rec pexp_parse (s : sexp) : pexp = -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) - (* lambda *) - | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), - [arg; body]) - -> let kind = match arw with - | "lambda_->_" -> Aexplicit | "lambda_=>_" -> Aimplicit - | _ -> Aerasable in - List.fold_right - (fun arg pbody - -> let (v, t) = match arg with - | Symbol v -> (v, None) - | Node (Symbol (_, "_:_"), [Symbol v; t]) - -> (v, Some (pexp_parse t)) - | _ -> pexp_error start "Unrecognized lambda argument"; - ((dummy_location, "unrecognized_arg"), None) - in Plambda (kind, v, t, pbody)) - (sexp_p_list arg ["_:_"]) - (pexp_parse body) - | Node (Symbol (start, "lambda_"), _) - -> pexp_error start "Unrecognized lambda expression"; - Pimm (Symbol (start, "?")) (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -228,15 +205,12 @@ and pexp_p_decls e: pdecl list = -> List.concat (List.map pexp_p_decls decls) | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, pexp_parse t)] - | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> - let rec mkfun args = - match args with - | [] -> pexp_parse t (* Plambda of arg_kind * pvar * pexp option * pexp *) - | (Symbol s :: args) -> Plambda(Aexplicit, s, None, mkfun args) - | (arg :: args) -> pexp_error (sexp_location arg) - "Unknown argument format"; - mkfun args - in [Pexpr(s, mkfun args)] + | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> + [Pexpr(s, Pcall (Pimm (Symbol (sexp_location d, "lambda_->_")), + [(match args with + | [] -> Sexp.dummy_epsilon + | arg::args -> Node (arg, args)); + t]))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) @@ -253,15 +227,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Plambda (ak, v, t, body) -> - Node (Symbol (dummy_location, match ak with - | Aexplicit -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [(match t with None -> Symbol v - | Some t -> Node (Symbol (dummy_location, "_:_"), - [Symbol v; pexp_unparse t])); - pexp_unparse body]) | Pcall (f, args) -> Node (pexp_unparse f, args) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"), View it on GitLab: https://gitlab.com/monnier/typer/commit/b3b5b11f774cf385698dcd66fdf4a95edb3…

1 0

[Git][monnier/typer][master] * src/lparse.ml (sform_arrow): New special form
by Stefan 27 Fév '17

27 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: b035fe3e by Stefan Monnier at 2017-02-27T21:33:29-05:00 * src/lparse.ml (sform_arrow): New special form (register_special_forms): Register it under all three names. * src/pexp.ml (pexp): Remove Parrow. - - - - - 3 changed files: - src/lexp.ml - src/lparse.ml - src/pexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -378,8 +378,15 @@ let rec lexp_unparse lxp = -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body) - | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> - Parrow(arg_kind, vdef, lexp_unparse ltp1, loc, lexp_unparse ltp2) + | Arrow (arg_kind, vdef, ltp1, loc, ltp2) + -> let ut1 = pexp_unparse (lexp_unparse ltp1) in + Pimm (Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" + | Aimplicit -> "_=>_" + | Aerasable -> "_≡>_"), + [(match vdef with None -> ut1 + | Some v -> Node (Symbol (loc, "_:_"), + [Symbol v; ut1])); + pexp_unparse (lexp_unparse ltp2)])) | Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -289,16 +289,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = (lexp_let_decls declss bdy nctx), mkSusp ltp s - (* ------------------------------------------------------------------ *) - | Parrow (kind, ovar, tp, loc, expr) - -> let ltp = infer_type tp ctx ovar in - let nctx = ectx_extend ctx ovar Variable ltp in - - let lxp = infer_type expr nctx None in - - let v = mkArrow(kind, ovar, ltp, tloc, lxp) in - v, type0 - (* This case can be inferred. *) | Plambda (kind, var, Some ptype, body) -> let ltp = infer_type ptype ctx (Some var) in @@ -1197,6 +1187,21 @@ let sform_hastype ctx loc sargs ot = | _ -> sexp_error loc "##_:_ takes two arguments"; sform_dummy_ret loc +let sform_arrow kind ctx loc sargs ot = + match sargs with + | [st1; st2] + -> let (v, st1) = match st1 with + | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (Some v, st1) + | _ -> (None, st1) in + let pt1 = pexp_parse st1 in + let pt2 = pexp_parse st2 in + let lt1 = infer_type pt1 ctx v in + let nctx = ectx_extend ctx v Variable lt1 in + let lt2 = infer_type pt2 nctx None in + (mkArrow (kind, v, lt1, loc, lt2), Lazy) + | _ -> sexp_error loc "##_->_ takes two arguments"; + sform_dummy_ret loc + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1238,6 +1243,9 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("_->_", sform_arrow Aexplicit); + ("_=>_", sform_arrow Aimplicit); + ("_≡>_", sform_arrow Aerasable); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,7 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Plet of location * pdecl list * pexp - | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two @@ -65,7 +64,6 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l @@ -74,7 +72,6 @@ let pexp_name e = match e with | Pimm _ -> "Pimm" | Plet (_, _, _) -> "Plet" - | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" | Pcase (_, _, _) -> "Pcase" @@ -96,17 +93,6 @@ let rec pexp_parse (s : sexp) : pexp = -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) - (* arrow *) - | Node (Symbol (start, (("_->_" | "_=>_" | "_≡>_") as arw)), [t1; t2]) - -> let kind = (match arw with - | "_->_" -> Aexplicit | "_=>_" -> Aimplicit | _ -> Aerasable) in - (match t1 with - | Node (Symbol (_, "_:_"), [Symbol v; t1]) - -> Parrow (kind, Some v, pexp_parse t1, start, pexp_parse t2) - | _ -> Parrow (kind, None, pexp_parse t1, start, pexp_parse t2)) - | Node (Symbol (start, ("_->_" | "_=>_" | "_≡>_")), _) - -> pexp_error start "Unrecognized arrow expression"; - Pimm (Symbol (start, "?")) (* lambda *) | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), [arg; body]) @@ -267,14 +253,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Parrow (kind, arg, t1, l, t2) -> - let ut1 = pexp_unparse t1 in - Node (Symbol (l, match kind with Aexplicit -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), - [(match arg with None -> ut1 - | Some v -> Node (Symbol (l, "_:_"), [Symbol v; ut1])); - pexp_unparse t2]) | Plambda (ak, v, t, body) -> Node (Symbol (dummy_location, match ak with | Aexplicit -> "lambda_->_" View it on GitLab: https://gitlab.com/monnier/typer/commit/b035fe3ed50db7a9238baa92aec59d4273b…

1 0

[Git][monnier/typer][master] * src/pexp.ml (pexp): Remove Pvar
by Stefan 27 Fév '17

27 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: baf904f3 by Stefan Monnier at 2017-02-27T21:16:37-05:00 * src/pexp.ml (pexp): Remove Pvar Use `Pimm (Symbol ..)` instead. - - - - - 3 changed files: - src/lexp.ml - src/lparse.ml - src/pexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -364,16 +364,16 @@ let lexp_name e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel" -let pdatacons = Pvar (U.dummy_location, "##datacons") -let ptypecons = Pvar (U.dummy_location, "##typecons") +let pdatacons = Pimm (Symbol (U.dummy_location, "##datacons")) +let ptypecons = Pimm (Symbol (U.dummy_location, "##typecons")) (* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = match lxp with | Susp _ as e -> lexp_unparse (nosusp e) | Imm (sexp) -> Pimm (sexp) - | Builtin ((l,name), _, _) -> Pvar (l, "##" ^ name) - | Var ((loc, name), _) -> Pvar (loc, name) + | Builtin ((l,name), _, _) -> Pimm (Symbol (l, "##" ^ name)) + | Var ((loc, name), _) -> Pimm (Symbol (loc, name)) | Cons (t, (l, name)) -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> @@ -450,17 +450,17 @@ let rec lexp_unparse lxp = -> Pimm (Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]")) - | SortLevel (SLz) -> Pvar (U.dummy_location, "##TypeLevel.z") + | SortLevel (SLz) -> Pimm (Symbol (U.dummy_location, "##TypeLevel.z")) | SortLevel (SLsucc l) - -> Pcall (Pvar (lexp_location l, "##TypeLevel.succ"), + -> Pcall (Pimm (Symbol (lexp_location l, "##TypeLevel.succ")), [pexp_unparse (lexp_unparse l)]) | SortLevel (SLlub (l1, l2)) - -> Pcall (Pvar (lexp_location l1, "##TypeLevel.∪"), + -> Pcall (Pimm (Symbol (lexp_location l1, "##TypeLevel.∪")), [pexp_unparse (lexp_unparse l1); pexp_unparse (lexp_unparse l2)]) - | Sort (l, StypeOmega) -> Pvar (l, "##Type_ω") - | Sort (l, StypeLevel) -> Pvar (l, "##Type_ℓ") + | Sort (l, StypeOmega) -> Pimm (Symbol (l, "##Type_ω")) + | Sort (l, StypeLevel) -> Pimm (Symbol (l, "##Type_ℓ")) | Sort (l, Stype sl) - -> Pcall (Pvar (lexp_location sl, "##Type_"), + -> Pcall (Pimm (Symbol (lexp_location sl, "##Type_")), [pexp_unparse (lexp_unparse sl)]) (* FIXME: ¡Unify lexp_print and lexp_string! *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -255,18 +255,8 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = _global_lexp_ctx := ctx; match p with - (* Block/String/Integer/Float. *) - | Pimm v - -> (mkImm (v), - match v with - | Integer _ -> DB.type_int - | Float _ -> DB.type_float - | String _ -> DB.type_string; - | _ -> pexp_error tloc p "Could not find type"; - mkDummy_type tloc) - - | Pvar (l,name) when String.length name >= 1 - && String.get name 0 == '#' + | Pimm (Symbol (l,name)) + when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then let name = string_sub name 2 (String.length name) in try SMap.find name (! BI.lmap) @@ -277,7 +267,8 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = mkDummy_infer l) (* Symbol i.e identifier. *) - | Pvar (loc, name) when String.length name < 1 || String.get name 0 != '?' + | Pimm (Symbol (loc, name)) + when String.length name < 1 || String.get name 0 != '?' -> (try let idx = senv_lookup name ctx in let lxp = make_var name idx loc in @@ -331,11 +322,22 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args - | (Plambda _ | Pcase _ | Pvar _) + | (Plambda _ | Pcase _ | Pimm (Symbol _)) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t) + (* Block/String/Integer/Float. *) + | Pimm v + -> (mkImm (v), + match v with + | Integer _ -> DB.type_int + | Float _ -> DB.type_float + | String _ -> DB.type_string; + | _ -> pexp_error tloc p "Could not find type"; + mkDummy_type tloc) + + and parse_special_form ctx f args ot = let loc = lexp_location f in let meta_ctx, _ = !global_substitution in @@ -510,9 +512,9 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = let (e, inferred_t) = infer_call ctx (f, ft) args in check_inferred ctx e inferred_t t - | Pvar (l,"?") -> newMetavar l "v" t - | Pvar (l, name) when String.length name > 1 - && String.get name 0 = '?' + | Pimm (Symbol (l,"?")) -> newMetavar l "v" t + | Pimm (Symbol (l, name)) when String.length name > 1 + && String.get name 0 = '?' -> pexp_error l p "Named metavars not supported (yet)"; newMetavar l name t @@ -693,7 +695,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match OL.lexp_whnf (mkVar (var, idx)) (ectx_to_lctx ctx) meta_ctx with | Cons _ (* It's indeed a constructor! *) - -> add_branch (Pvar var) [] + -> add_branch (Pimm (Symbol var)) [] | _ -> add_default (Some var) (* A named default branch. *) with Not_found -> add_default (Some var)) @@ -891,7 +893,7 @@ and sexp_decls_macro_print sxp_decls = | e -> sexp_print e; print_string "\n" and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = - try let lxp, ltp = infer (Pvar (loc, mname)) ctx in + try let lxp, ltp = infer (Pimm (Symbol (loc, mname))) ctx in (* FIXME: Check that (conv_p ltp Macro)! *) let ret = lexp_expand_macro loc lxp sargs ctx None in ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -39,7 +39,6 @@ type pvar = symbol type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) - | Pvar of pvar | Plet of location * pdecl list * pexp | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp @@ -65,7 +64,6 @@ let rec pexp_location e = match e with (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s - | Pvar (l,_) -> l | Plet (l, _, _) -> l | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l @@ -75,7 +73,6 @@ let rec pexp_location e = let pexp_name e = match e with | Pimm _ -> "Pimm" - | Pvar (_,_) -> "Pvar" | Plet (_, _, _) -> "Plet" | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" @@ -93,14 +90,12 @@ let rec pexp_parse (s : sexp) : pexp = match s with (* This is an internal error because Epsilon does not have any location * information so it needs to be caught elsewhere. *) - | (Block _ | Integer _ | Float _ | String _) -> Pimm s - (* | Symbol (l, "Type") -> Psort (l, Type) *) - | Symbol s -> Pvar s + | (Block _ | Integer _ | Float _ | String _ | Symbol _) -> Pimm s (* let *) | Node (Symbol (start, "let_in_"), [decls; body]) -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) - -> pexp_error start "Unrecognized let expression"; Pvar (start, "?") + -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) (* arrow *) | Node (Symbol (start, (("_->_" | "_=>_" | "_≡>_") as arw)), [t1; t2]) -> let kind = (match arw with @@ -110,7 +105,8 @@ let rec pexp_parse (s : sexp) : pexp = -> Parrow (kind, Some v, pexp_parse t1, start, pexp_parse t2) | _ -> Parrow (kind, None, pexp_parse t1, start, pexp_parse t2)) | Node (Symbol (start, ("_->_" | "_=>_" | "_≡>_")), _) - -> pexp_error start "Unrecognized arrow expression"; Pvar (start, "?") + -> pexp_error start "Unrecognized arrow expression"; + Pimm (Symbol (start, "?")) (* lambda *) | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), [arg; body]) @@ -129,7 +125,8 @@ let rec pexp_parse (s : sexp) : pexp = (sexp_p_list arg ["_:_"]) (pexp_parse body) | Node (Symbol (start, "lambda_"), _) - -> pexp_error start "Unrecognized lambda expression"; Pvar (start, "?") + -> pexp_error start "Unrecognized lambda expression"; + Pimm (Symbol (start, "?")) (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -138,11 +135,12 @@ let rec pexp_parse (s : sexp) : pexp = -> (pexp_p_pat pat, pexp_parse code) | _ -> let l = (sexp_location branch) in pexp_error l "Unrecognized simple case branch"; - (Ppatany l, Pvar (l, "?")) + (Ppatany l, Pimm (Symbol (l, "?"))) in Pcase (start, pexp_parse e, List.map parse_case cases) | Node (Symbol (start, "case_"), [e]) -> Pcase (start, pexp_parse e, []) | Node (Symbol (start, "case_"), _) - -> pexp_error start "Unrecognized case expression"; Pvar (start, "?") + -> pexp_error start "Unrecognized case expression"; + Pimm (Symbol (start, "?")) (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f | Node (f, args) -> Pcall (pexp_parse f, args) @@ -266,7 +264,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s - | Pvar v -> Symbol v | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) View it on GitLab: https://gitlab.com/monnier/typer/commit/baf904f35aacace8b5c6a1032be7aa1c4ff…

1 0

[Git][monnier/typer][master] * src/lparse.ml (sform_hastype): New function
by Stefan 27 Fév '17

27 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: fa5e92ad by Stefan Monnier at 2017-02-27T21:08:16-05:00 * src/lparse.ml (sform_hastype): New function (register_special_forms): Record it. * src/pexp.ml (pexp): Remove Phastype. - - - - - 2 changed files: - src/lparse.ml - src/pexp.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -331,10 +331,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args - | Phastype (_, pxp, ptp) - -> let ltp = infer_type ptp ctx None in - (check pxp ltp ctx, ltp) - | (Plambda _ | Pcase _ | Pvar _) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in @@ -1189,6 +1185,16 @@ let sform_typecons ctx loc sargs ot = let map_ctor = lexp_parse_inductive ctors nctx in (mkInductive (loc, label, formals, map_ctor), Lazy) +let sform_hastype ctx loc sargs ot = + match sargs with + | [se; st] -> let pe = pexp_parse se in + let pt = pexp_parse st in + let lt = infer_type pt ctx None in + let le = check pe lt ctx in + (le, Inferred lt) + | _ -> sexp_error loc "##_:_ takes two arguments"; + sform_dummy_ret loc + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1229,6 +1235,7 @@ let register_special_forms () = ("Built-in", sform_built_in); ("datacons", sform_datacons); ("typecons", sform_typecons); + ("_:_", sform_hastype); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,7 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Pvar of pvar - | Phastype of location * pexp * pexp | Plet of location * pdecl list * pexp | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp @@ -67,7 +66,6 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Pvar (l,_) -> l - | Phastype (l,_,_) -> l | Plet (l, _, _) -> l | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l @@ -78,7 +76,6 @@ let pexp_name e = match e with | Pimm _ -> "Pimm" | Pvar (_,_) -> "Pvar" - | Phastype (_,_,_) -> "Phastype" | Plet (_, _, _) -> "Plet" | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" @@ -99,8 +96,6 @@ let rec pexp_parse (s : sexp) : pexp = | (Block _ | Integer _ | Float _ | String _) -> Pimm s (* | Symbol (l, "Type") -> Psort (l, Type) *) | Symbol s -> Pvar s - | Node (Symbol (start, "_:_"), [e; t]) - -> Phastype (start, pexp_parse e, pexp_parse t) (* let *) | Node (Symbol (start, "let_in_"), [decls; body]) -> Plet (start, pexp_p_decls decls, pexp_parse body) @@ -272,8 +267,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s | Pvar v -> Symbol v - | Phastype (l,e,t) - -> Node (Symbol (l, "_:_"), [pexp_unparse e; pexp_unparse t]) | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) View it on GitLab: https://gitlab.com/monnier/typer/commit/fa5e92ad80caedeba73191b0a892ab538d4…

1 0

[Git][monnier/typer][master] * src/pexp.ml (pexp): Remove Pmetavar
by Stefan 27 Fév '17

27 Fév '17

Stefan pushed to branch master at Stefan / Typer Commits: 3a54a263 by Stefan Monnier at 2017-02-27T20:56:07-05:00 * src/pexp.ml (pexp): Remove Pmetavar Use Pvar with a leading ? instead. Reserve identifiers starting with # for future use. - - - - - 3 changed files: - src/lexp.ml - src/lparse.ml - src/pexp.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -447,8 +447,8 @@ let rec lexp_unparse lxp = (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _) - -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx - ^ "[" ^ subst_string subst ^ "]>")) + -> Pimm (Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx + ^ "[" ^ subst_string subst ^ "]")) | SortLevel (SLz) -> Pvar (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -265,17 +265,19 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = | _ -> pexp_error tloc p "Could not find type"; mkDummy_type tloc) - | Pvar (l,name) when String.length name > 2 + | Pvar (l,name) when String.length name >= 1 && String.get name 0 == '#' - && String.get name 1 == '#' - -> let name = string_sub name 2 (String.length name) in - (try SMap.find name (! BI.lmap) - with Not_found - -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); - mkDummy_infer l) + -> if String.length name > 2 && String.get name 1 == '#' then + let name = string_sub name 2 (String.length name) in + try SMap.find name (! BI.lmap) + with Not_found + -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); + mkDummy_infer l + else (pexp_error l p ("Invalid special identifier `" ^ name ^ "`"); + mkDummy_infer l) (* Symbol i.e identifier. *) - | Pvar (loc, name) + | Pvar (loc, name) when String.length name < 1 || String.get name 0 != '?' -> (try let idx = senv_lookup name ctx in let lxp = make_var name idx loc in @@ -333,7 +335,7 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = -> let ltp = infer_type ptp ctx None in (check pxp ltp ctx, ltp) - | (Plambda _ | Pcase _ | Pmetavar _) + | (Plambda _ | Pcase _ | Pvar _) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t) @@ -512,8 +514,9 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = let (e, inferred_t) = infer_call ctx (f, ft) args in check_inferred ctx e inferred_t t - | Pmetavar (l,"") -> newMetavar l "v" t - | Pmetavar (l, name) + | Pvar (l,"?") -> newMetavar l "v" t + | Pvar (l, name) when String.length name > 1 + && String.get name 0 = '?' -> pexp_error l p "Named metavars not supported (yet)"; newMetavar l name t ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -41,7 +41,6 @@ type pexp = | Pimm of sexp (* Used for strings, ... *) | Pvar of pvar | Phastype of location * pexp * pexp - | Pmetavar of pvar | Plet of location * pdecl list * pexp | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp @@ -69,7 +68,6 @@ let rec pexp_location e = | Pimm s -> sexp_location s | Pvar (l,_) -> l | Phastype (l,_,_) -> l - | Pmetavar (l, _) -> l | Plet (l, _, _) -> l | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l @@ -81,7 +79,6 @@ let pexp_name e = | Pimm _ -> "Pimm" | Pvar (_,_) -> "Pvar" | Phastype (_,_,_) -> "Phastype" - | Pmetavar (_, _) -> "Pmetavar" | Plet (_, _, _) -> "Plet" | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" @@ -101,8 +98,6 @@ let rec pexp_parse (s : sexp) : pexp = * information so it needs to be caught elsewhere. *) | (Block _ | Integer _ | Float _ | String _) -> Pimm s (* | Symbol (l, "Type") -> Psort (l, Type) *) - | Symbol (l, name) when String.length name > 0 && String.get name 0 == '?' - -> Pmetavar (l, String.sub name 1 (String.length name - 1)) | Symbol s -> Pvar s | Node (Symbol (start, "_:_"), [e; t]) -> Phastype (start, pexp_parse e, pexp_parse t) @@ -110,7 +105,7 @@ let rec pexp_parse (s : sexp) : pexp = | Node (Symbol (start, "let_in_"), [decls; body]) -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) - -> pexp_error start "Unrecognized let expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized let expression"; Pvar (start, "?") (* arrow *) | Node (Symbol (start, (("_->_" | "_=>_" | "_≡>_") as arw)), [t1; t2]) -> let kind = (match arw with @@ -120,7 +115,7 @@ let rec pexp_parse (s : sexp) : pexp = -> Parrow (kind, Some v, pexp_parse t1, start, pexp_parse t2) | _ -> Parrow (kind, None, pexp_parse t1, start, pexp_parse t2)) | Node (Symbol (start, ("_->_" | "_=>_" | "_≡>_")), _) - -> pexp_error start "Unrecognized arrow expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized arrow expression"; Pvar (start, "?") (* lambda *) | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), [arg; body]) @@ -139,7 +134,7 @@ let rec pexp_parse (s : sexp) : pexp = (sexp_p_list arg ["_:_"]) (pexp_parse body) | Node (Symbol (start, "lambda_"), _) - -> pexp_error start "Unrecognized lambda expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized lambda expression"; Pvar (start, "?") (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -148,11 +143,11 @@ let rec pexp_parse (s : sexp) : pexp = -> (pexp_p_pat pat, pexp_parse code) | _ -> let l = (sexp_location branch) in pexp_error l "Unrecognized simple case branch"; - (Ppatany l, Pmetavar (l, "_")) + (Ppatany l, Pvar (l, "?")) in Pcase (start, pexp_parse e, List.map parse_case cases) | Node (Symbol (start, "case_"), [e]) -> Pcase (start, pexp_parse e, []) | Node (Symbol (start, "case_"), _) - -> pexp_error start "Unrecognized case expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized case expression"; Pvar (start, "?") (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f | Node (f, args) -> Pcall (pexp_parse f, args) @@ -277,7 +272,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s | Pvar v -> Symbol v - | Pmetavar (l,name) -> Symbol (l, "?" ^ name) | Phastype (l,e,t) -> Node (Symbol (l, "_:_"), [pexp_unparse e; pexp_unparse t]) | Plet (start, decls, body) -> View it on GitLab: https://gitlab.com/monnier/typer/commit/3a54a26388826075d9b183e39d40abb1a25…

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Février 2017