Stefan pushed to branch master at Stefan / Typer

Commits: 27dd27dc by Stefan Monnier at 2017-08-03T14:25:36-04:00 * src/elab.ml: Make symbols into shorthands for `typer-identifier SYM`

(newMetalevel, newMetatype): Take a lexp_context i.s.o elab_context. (infer_varref): New function, extracted from `infer`. (infer): Make symbols into shorthands for `typer-identifier SYM` and blocks into shorthands for `typer-block BLOCK`. (check): Same rewrite for symbols. (sform_identifier): New functions, using code extracted from `infer` and `check`. (register_special_forms): Use it to implement `typer-identifier`.

- - - - -

2 changed files:

- src/elab.ml - src/unification.ml

Changes:

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -236,51 +236,35 @@ let newMetavar (ctx : lexp_context) sl l name t= let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.Identity, (l, name))

-let newMetalevel (ctx : elab_context) sl = - newMetavar (ectx_to_lctx ctx) sl Util.dummy_location "l" type_level +let newMetalevel (ctx : lexp_context) sl = + newMetavar ctx sl Util.dummy_location "l" type_level

-let newMetatype (ctx : elab_context) sl loc - = newMetavar (ectx_to_lctx ctx) sl loc - "t" (mkSort (loc, Stype (newMetalevel ctx sl))) +let newMetatype (ctx : lexp_context) sl loc + = newMetavar ctx sl loc "t" (mkSort (loc, Stype (newMetalevel ctx sl)))

(* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) -let mkDummy_type ctx loc = newMetatype ctx dummy_scope_level loc +let mkDummy_type ctx loc = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc let mkDummy_check ctx loc t = newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "dummy" t let mkDummy_infer ctx loc = - let t = newMetatype ctx dummy_scope_level loc in (mkDummy_check ctx loc t, t) + let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in + (mkDummy_check ctx loc t, t)

-let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = +let infer_varref ctx ((loc, name) as id) + = let idx = senv_lookup name ctx in + let lxp = make_var name idx loc in + let ltp = env_lookup_type ctx (id, idx) in + (lxp, ltp)

- let tloc = sexp_location p in +let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

match p with - | 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 - -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); - mkDummy_infer ctx l - else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); - mkDummy_infer ctx l) - - (* Symbol i.e identifier. *) - | 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 - - (* Search type. *) - let ltp = env_lookup_type ctx ((loc, name), idx) in - lxp, ltp - - with Not_found -> - (sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); - mkDummy_infer ctx loc)) + | Symbol ((loc, name) as id) + -> if not (name = "typer-identifier") then + infer (Node (Symbol (loc, "typer-identifier"), [p])) ctx + (* Break the inf-recursion! *) + else infer_varref ctx id

| Node (se, []) -> infer se ctx

@@ -290,29 +274,19 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = parse_special_form ctx f args None else if (OL.conv_p (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then - let t = newMetatype ctx (ectx_to_scope_level ctx) + let t = newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) (sexp_location func) in let lxp = handle_macro_call ctx f args t in (lxp, t) else infer_call ctx ft args

- | Symbol (_, name) - -> assert (String.length name >= 1 || String.get name 0 = '?'); - let t = newMetatype ctx (ectx_to_scope_level ctx) (sexp_location p) in - let lxp = check p t ctx in - (lxp, t) - (* Block/String/Integer/Float. *) - | v - -> (mkImm (v), - match v with - | Integer _ -> DB.type_int - | Float _ -> DB.type_float - | String _ -> DB.type_string; - | _ -> sexp_error tloc "Could not find type"; - mkDummy_type ctx tloc) - + | Integer _ -> (mkImm (p), DB.type_int) + | Float _ -> (mkImm (p), DB.type_float) + | String _ -> (mkImm (p), DB.type_string) + | Block _ -> infer (Node (Symbol (sexp_location p, "typer-block"), [p])) + ctx

and parse_special_form ctx f args ot = let loc = lexp_location f in @@ -395,7 +369,8 @@ and infer_type pexp ectx var = match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel - ectx (ectx_to_scope_level ectx)))) + (ectx_to_lctx ectx) + (ectx_to_scope_level ectx)))) s (ectx_to_lctx ectx) with | (None | Some (_::_)) @@ -417,10 +392,10 @@ and lexp_let_decls declss (body: lexp) ctx =

and unify_with_arrow ctx tloc lxp kind var aty = let arg = match aty with - | None -> newMetatype ctx (ectx_to_scope_level ctx) tloc + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) tloc | Some laty -> laty in let nctx = ectx_extend ctx (Some var) Variable arg in - let body = newMetatype nctx (ectx_to_scope_level ctx) tloc in + let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in let arrow = mkArrow (kind, Some var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with @@ -440,6 +415,9 @@ and unify_with_arrow ctx tloc lxp kind var aty and check (p : sexp) (t : ltype) (ctx : elab_context): lexp =

match p with + | Symbol (l,name) + -> check (Node (Symbol (l, "typer-identifier"), [p])) t ctx + | Node (se, []) -> check se t ctx

| Node (func, args) @@ -453,24 +431,6 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = let (e, inferred_t) = infer_call ctx (f, ft) args in check_inferred ctx e inferred_t t

- | Symbol (l, name) when String.length name >= 1 - && String.get name 0 = '?' - -> let name = if name = "?" then "v" else - (sexp_error l "Named metavars not supported (yet)"; - String.sub name 1 (String.length name)) in - (* Shift the var so it can't refer to the local vars. - * This is used so that in cases like "lambda t (y : ?) ... " - * type inference can guess ? without having to wonder whether it - * can refer to `t` or not. If the user wants ? to be able to refer - * to `t`, then she should explicitly write (y : ? t). *) - let ctx_shift = ectx_local_scope_size ctx in - let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in - (* FIXME: `t` is defined in ctx instead of octx. - * We need something like: - * let t = push_inv_subst t (S.shift ctx_shift) in *) - mkSusp (newMetavar octx (ectx_to_scope_level ctx) l name t) - (S.shift ctx_shift) - | _ -> infer_and_check p ctx t

and infer_and_check pexp ctx t = @@ -1024,7 +984,7 @@ and get_attribute ctx loc largs = with Not_found -> None

and sform_dummy_ret ctx loc = - let t = newMetatype ctx dummy_scope_level loc in + let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "special-form-error" t, Inferred t)

@@ -1114,7 +1074,8 @@ let sform_typecons ctx loc sargs ot = let ltp = match opxp with | Some pxp -> let (l,_) = infer pxp ctx in l | None -> let (l,_) = var in - newMetatype ctx (ectx_to_scope_level ctx) l in + newMetatype (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) l in

parse_formals sformals ((kind, var, ltp) :: rformals) (env_extend ctx var Variable ltp) in @@ -1160,6 +1121,62 @@ let sform_arrow kind ctx loc sargs ot = | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret ctx loc

+let sform_identifier ctx loc sargs ot = + match sargs with + | [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 let (e,t) = SMap.find name (! BI.lmap) in + (e, Inferred t) + with Not_found + -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); + sform_dummy_ret ctx loc + else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); + sform_dummy_ret ctx loc) + + | [Symbol (loc, name)] + when String.length name >= 1 && String.get name 0 = '?' + -> assert (String.length name >= 1 && String.get name 0 = '?'); + let name = if name = "?" then "" else + (sexp_error loc "Named metavars not supported (yet)"; + String.sub name 1 (String.length name)) in + (* Shift the var so it can't refer to the local vars. + * This is used so that in cases like "lambda t (y : ?) ... " + * type inference can guess ? without having to wonder whether it + * can refer to `t` or not. If the user wants ? to be able to refer + * to `t`, then she should explicitly write (y : ? t). *) + let ctx_shift = ectx_local_scope_size ctx in + let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in + let sl = ectx_to_scope_level ctx in + let subst = S.shift ctx_shift in + let t = match ot with + | None -> newMetatype octx sl loc + (* FIXME: `t` is defined in ctx instead of octx. + * We need something like: + * let t = push_inv_subst t (S.shift ctx_shift) in *) + | Some t -> t in + (mkSusp (newMetavar octx sl loc name t) subst, + match ot with Some _ -> Checked | None -> Lazy) + + (* Normal identifier. *) + | [Symbol id] + -> (try let (e, t) = infer_varref ctx id in + (e, Inferred t) + + with Not_found -> + (let (loc, name) = id in + sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); + sform_dummy_ret ctx loc)) + + | [se] + -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); + sform_dummy_ret ctx loc) + + | _ + -> (sexp_error loc ("Too many args to ##typer-identifier"); + sform_dummy_ret ctx loc) + (* Infer or check, as the case may be. *) let elaborate ctx pe ot = match ot with @@ -1198,7 +1215,8 @@ let rec sform_lambda kind ctx loc sargs ot = (match ot with | None -> mklam (match olt1 with | Some lt1 -> lt1 - | None -> newMetatype ctx (ectx_to_scope_level ctx) loc) + | None -> newMetatype (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) loc) None (* Read var type from the provided type *) | Some t @@ -1249,7 +1267,7 @@ let rec sform_case ctx loc sargs ot = match sargs with let pcases = List.map parse_case scases in let t = match ot with | Some t -> t - | None -> newMetatype ctx (ectx_to_scope_level ctx) loc in + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc in let le = check_case t (loc, se, pcases) ctx in (le, match ot with Some _ -> Checked | None -> Inferred t)

@@ -1306,6 +1324,7 @@ let register_special_forms () = List.iter add_special_form [ ("Built-in", sform_built_in); + ("typer-identifier", sform_identifier); ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype);

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -67,11 +67,11 @@ let unify_and res op = match res with

(****************************** Top level unify *************************************)

-(** Dispatch to the right unifyer. +(** 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>)

- The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) + The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) *) let rec unify (e1: lexp) (e2: lexp) (ctx : DB.lexp_context)

View it on GitLab: https://gitlab.com/monnier/typer/commit/27dd27dc9e57f84a56a06c830a470201127b...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/27dd27dc9e57f84a56a06c830a470201127b... You're receiving this email because of your account on gitlab.com.