Stefan pushed to branch master at Stefan / Typer

Commits: d05adcab by Stefan Monnier at 2016-08-27T10:50:37-04:00 * src/lparse.ml (lexp_call): Rewrite to work one-arg at a time

Add basic support for explicit-implicit args. Use lexp_whnf. (lexp_call.get_return_type): Remove. (_lexp_p_infer, lexp_read_pattern, lexp_decls_macro): Adjust to new env_lookup_expr. (_lexp_parse_all.loop): Don't use List.hd when not needed. * src/typecheck.ml (lexp_whnf): New function. * src/debruijn.ml (env_lookup_expr): Return an option. * src/builtin.ml (get_attribute_impl, declexpr_impl): Adjust accordingly. * btl/types.typer (length): One more explicit-implicit arg.

- - - - -

7 changed files:

- DESIGN - btl/types.typer - src/builtin.ml - src/debruijn.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml

Changes:

===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1655,6 +1655,60 @@ Look ma! No axioms! Or almost: with these classical definitions we cannot prove the classical axiom of choice as a theorem, so if you need it, you have to add it as an axiom.

+* Co-induction + +Coinductive data is basically defined by observation, so what is often +written as something like + + codata Stream α + | Nil + | Cons α (Stream α) + +really means something like: + + type StreamAccessor + | Car | Cdr + Stream α = + (a : StreamAccessor) + -> case a + | Car => Maybe α + | Cdr => Maybe (Stream α) + +And with length, that could turn into: + + type StreamAccessor n + | Empty? | Car (n > 0) | Cdr (n > 0) + Stream α n = + (a : StreamAccessor n) + -> case a + | Empty? => Maybe (n > 0) + | Car _ => α + | Cdr _ => Stream α (n - 1) + +In either case, the definition of `Stream` is recursive and doesn't follow +the supported forms of recursion in CIC (i.e. inductive types and inductive +functions) so it requires ad-hoc support. + +It would help to have something akin to the "impredicative encoding" of +inductive types to get an intuitive idea of what should be safe and what +might be dangerous. + +Let's try for `Stream α`: + + Stream α = + (β : Type) -> (a : StreamAccessor) + -> (case a + | Car => Maybe α -> β + | Cdr => Maybe β -> β) + -> β + +So we'd define + + numbers' n β a = case a + | Car => λ f -> f (just n) + | Cdr => λ f -> f (just ¿?¿) %% (numbers' (n + 1)) + numbers = numbers' 0 + * Papers ** BigBang: Designing a statically typed scripting language ** Dependently typed Racket

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -77,7 +77,7 @@ length = lambda a => lambda xs -> case xs | nil => 0 - | cons hd tl => (1 + (length a tl)); + | cons hd tl => (1 + (length(a := a) tl));

head : (a : Type) => List a -> a; head = lambda a =>

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -303,7 +303,7 @@ let get_attribute_impl loc largs ctx ftype = | _ -> builtin_error loc "get-attribute expects two arguments" in

let lxp = get_property ctx (vi, vn) (ai, an) in - let ltype = env_lookup_expr ctx ((loc, an), ai) in + let Some ltype = env_lookup_expr ctx ((loc, an), ai) in lxp, ltype

let new_attribute_impl loc largs ctx ftype = @@ -331,7 +331,7 @@ let declexpr_impl loc largs ctx ftype = | [Var((_, vn), vi)] -> (vi, vn) | _ -> builtin_error loc "declexpr expects one argument" in

- let lxp = env_lookup_expr ctx ((loc, vn), vi) in + let Some lxp = env_lookup_expr ctx ((loc, vn), vi) in let ltp = env_lookup_type ctx ((loc, vn), vi) in lxp, ftype

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -34,6 +34,7 @@

open Util open Lexp +module L = Lexp open Myers open Fmt (*open Typecheck env_elem and env_type *) @@ -146,15 +147,13 @@ let env_lookup_type ctx (v : vref): lexp = let (_, _, _, ltp) = _env_lookup ctx v in mkSusp ltp (S.shift (idx + 0))

-let env_lookup_expr ctx (v : vref): lexp = +let env_lookup_expr ctx (v : vref): lexp option = let (_, idx) = v in let (r, _, lxp, _) = _env_lookup ctx v in - - let lxp = match lxp with - | LetDef lxp -> lxp - | _ -> Sort (dummy_location, Stype (SortLevel (SLn 0))) in - - mkSusp lxp (S.shift (idx + 1 - r)) + match lxp with + | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) + (* FIXME: why Sort here? *) + | _ -> None

let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx))

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -351,105 +351,6 @@ let lexp_to_string e = | Builtin _ -> "Builtin" | _ -> "lexp_to_string: not implemented"

- - -(* Apply substitution `s' and then reduce to weak head normal form. - * WHNF implies: - * - Not a Let. - * - Not a let-bound variable. - * - Not a Susp. - * - Not an instantiated Metavar. - * - Not a Call (Lambda _). - * - Not a Call (Call _). - * - Not a Call (_, []). - * - Not a Case (Cons _). - * - Not a Call (MetaSet, ..). - *) -(* let rec lexp_whnf (s : lexp VMap.t) e = - * match e with - * | (Imm _ | Builtin _) -> e - * | Sort (_, (StypeLevel | StypeOmega | Stype (SortLevel (SLn _)))) -> e - * | Sort (l, Stype e) -> Sort (l, Stype (mk_susp s e)) - * | SortLevel (SLn _) -> e - * | SortLevel (SLsucc e) -> - * (match lexp_whnf s e with - * | SortLevel (SLn n) -> SortLevel (SLn (n + 1)) - * | e' -> SortLevel (SLsucc e')) - * | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, mk_susp s t1, l, mk_susp s t2) - * | Lambda (ak, v, t, e) -> Lambda (ak, v, mk_susp s t, mk_susp s e) - * | Call (f, args) -> - * List.fold_left (fun e (ak,arg) -> - * match e with - * | Builtin (b,_,_) -> - * (match builtin_reduce b [] arg with - * | Some e -> e - * | _ -> Call (e, [(ak, mk_susp s arg)])) - * | Call (Builtin (b,_,_), args) -> - * (match builtin_reduce b args arg with - * | Some e -> e - * | _ -> Call (e, [(ak, mk_susp s arg)])) - * | Lambda (_, (_,v), _, body) - * -> lexp_whnf (VMap.add v (mk_susp s arg) VMap.empty) body - * | Call (f, args) -> Call (f, (ak, mk_susp s arg) :: args) - * | _ -> Call (e, [(ak, mk_susp s arg)])) - * (lexp_whnf s f) args - * | Inductive (id, t, branches) - * -> Inductive (id, mk_susp s t, SMap.map (mk_susp s) branches) - * | Cons (t, tag) -> Cons (mk_susp s t, tag) - * | Case (l, e, t, branches, default) - * -> let select name actuals - * = try let (l,formals,body) = SMap.find name branches in - * lexp_whnf (List.fold_left2 (fun s (_,a) (_,(_,f)) -> - * VMap.add f a s) - * s actuals formals) - * body - * with Not_found -> - * match default with - * | None -> msg_error l "Unmatched constructor"; - * mk_meta_dummy VMap.empty l - * | Some body -> lexp_whnf s body - * in - * (match lexp_whnf s e with - * | Cons (_, (_,name)) -> select name [] - * | Call (Cons (_, (_, name)), actuals) -> select name actuals - * | e -> Case (l, e, t, - * SMap.map (fun (l,args,body) - * -> (l, args, mk_susp s body)) - * branches, - * match default with Some e -> Some (mk_susp s e) - * | None -> None)) - * | Susp (s', e) -> lexp_whnf (lexp_subst_subst s s') e - * | Metavar (_,MetaFoF,r) -> - * (match !r with | MetaSet e -> lexp_whnf s e | _ -> e) - * | Metavar (l, MetaGraft s', r) -> - * let s' = (lexp_subst_subst s s') in - * (match !r with MetaSet e -> lexp_whnf s' e - * (* FIXME: filter s' w.r.t `venv'. *) - * | MetaUnset (venv,_,_) -> Metavar (l, MetaGraft s', r)) - * (* BEWARE: we need a recursive environment, which is kinda painful - * * to create (tho we could use ref'cells), so we use a hack instead. *) - * | Let (l,decls,body) - * -> let decls' = List.map (fun (v, e, t) -> (v, mk_susp s e, mk_susp s t)) - * decls in - * let s' = List.fold_left (fun s ((l',v),e,t) -> - * VMap.add v (Let (l, decls', Var (l', v))) s) - * s decls - * in lexp_whnf s' body - * | Var (l,v) - * -> (try match VMap.find v s with - * (* Hack attack! A recursive binding, let's unroll it here. *) - * | Let (_,decls,Var (_, v')) when v = v' - * -> let e = List.fold_left (fun e ((_,v'), e', _) -> - * if v = v' then e' else e) - * (* This metavar is just a placeholder - * * which should be dropped. *) - * (mk_meta_dummy VMap.empty l) decls - * (* Here we stay in `s' to keep the recursive bindings. *) - * in lexp_whnf s (lexp_copy e) - * | e -> lexp_whnf VMap.empty (lexp_copy e) - * with Not_found -> e) *) - - (* (* In non-recursion calls, `s' is always empty. *) let lexp_conv_p env = lexp_conv_p env VMap.empty

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -235,7 +235,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* An inductive type named type_name must be in the environment *) try let idx = senv_lookup type_name ctx in (* Check if the constructor exists *) - let idt = env_lookup_expr ctx (vr, idx) in + let Some idt = env_lookup_expr ctx (vr, idx) in

(* make Base type *) let inductive_type = Var((loc, type_name), idx) in @@ -391,8 +391,8 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = Case (loc, tlxp, tltp, return_type, lpattern, dflt), return_type

(* Identify Call Type and return processed call *) -and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = - let loc = pexp_location fun_name in +and lexp_call (func: pexp) (sargs: sexp list) ctx i = + let loc = pexp_location func in

let from_lctx ctx = try (from_lctx ctx) with e ->( @@ -400,60 +400,70 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = print_eval_trace (); raise e) in

- (* consume Arrows and args together *) - let rec get_return_type name i ltp args = - match (nosusp ltp), args with - | _, [] -> ltp - | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) - | _, _ -> lexp_warning loc - (name ^ " was provided with too many args. Expected: " ^ - (string_of_int i)); ltp in - (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned * Macro : sqr is returned * Constructor : a constructor is returned * Anonymous : lambda *)

(* retrieve function's body *) - let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in + let body, ltp = _lexp_p_infer func ctx (i + 1) in let ltp = nosusp ltp in

- let handle_named_call (loc, name) = + let rec handle_fun_args largs sargs ltp = match sargs with + | [] -> largs, ltp + | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs + (* Explicit-implicit argument. *) + -> (match TC.lexp_whnf ltp ctx with + | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) + when aname = aname' + -> let parg = pexp_parse sarg in + let larg = _lexp_p_check parg arg_type ctx i in + handle_fun_args ((ak, larg) :: largs) sargs + (L.mkSusp ret_type (S.substitute larg)) + | _ -> lexp_fatal (sexp_location sarg) + "Explicit arg to non-function") + | sarg :: sargs + (* Process Argument *) + -> (match TC.lexp_whnf ltp ctx with + | Arrow (Aexplicit, _, arg_type, _, ret_type) + -> let parg = pexp_parse sarg in + let larg = _lexp_p_check parg arg_type ctx i in + handle_fun_args ((Aexplicit, larg) :: largs) sargs + (L.mkSusp ret_type (S.substitute larg)) + | Arrow _ as t -> lexp_print t; print_string "\n"; + sexp_print sarg; print_string "\n"; + lexp_fatal (sexp_location sarg) + "Expected non-explicit arg" + | _ -> lexp_fatal (sexp_location sarg) + "Explicit arg to non-function") in + + let handle_funcall () = + + match TC.lexp_whnf body ctx with + | Builtin((_, "Built-in"), _) + -> ( + (* ------ SPECIAL ------ *) + match !_parsing_internals, sargs with + | true, [String (_, str)] -> + Builtin((loc, str), ltp), ltp + + | true, [String (_, str); stp] -> + let ptp = pexp_parse stp in + let ltp, _ = _lexp_p_infer ptp ctx (i + 1) in + Builtin((loc, str), ltp), ltp + + | true, _ -> + lexp_error loc "Wrong Usage of "Built-in""; + dlxp, dltype + + | false, _ -> + lexp_error loc "Use of "Built-in" in user code"; + dlxp, dltype) + + | e -> (* Process Arguments *) - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - - try (* Check if the function was defined *) - let idx = senv_lookup name ctx in - let vf = (make_var name idx loc) in - - match nosusp (env_lookup_expr ctx ((loc, name), idx)) with - | Builtin((_, "Built-in"), _) ->( - (* ------ SPECIAL ------ *) - match !_parsing_internals, largs with - | true, [Imm(String (_, str))] -> - Builtin((loc, str), ltp), ltp - - | true, [Imm(String (_, str)); ltp] -> - Builtin((loc, str), ltp), ltp - - | true, _ -> - lexp_error loc "Wrong Usage of "Built-in""; - dlxp, dltype - - | false, _ -> - lexp_error loc "Use of "Built-in" in user code"; - dlxp, dltype) - - | e -> - let ret_type = get_return_type name 0 ltp new_args in - Call(vf, new_args), ret_type - - with Not_found -> - lexp_error loc ("The function "" ^ name ^ "" was not defined"); - let vf = (make_var name (-1) loc) in - Call(vf, new_args), ltp in + let largs, ret_type = handle_fun_args [] sargs ltp in + Call (body, List.rev largs), ret_type in

let handle_macro_call (loc, name) = (* check for builtin *) @@ -465,20 +475,10 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* user defined macro *) | false ->( - (* look up for definition *) - let idx = try senv_lookup name ctx - with Not_found -> - lexp_fatal loc ("Could not find Variable: " ^ name) in - (* Get the macro *) - let lxp = try env_lookup_expr ctx ((loc, name), idx) - with Not_found -> - lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ - " is not a correct index.") in - - let lxp = match nosusp lxp with + let lxp = match TC.lexp_whnf body ctx with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | _ -> + | lxp -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n"; lexp_print lxp; print_string "\n"; @@ -512,36 +512,12 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = _lexp_p_infer pxp ctx (i + 1)) in

(* determine function type *) - match fun_name, ltp with - (* Anonymous *) - | ((Plambda _), _) -> - (* Process Arguments *) - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - Call(body, new_args), ltp - - | (Pvar (l, n), Var((_, "Macro"), _)) -> - (* FIXME: check db_idx points to a Macro type *) - handle_macro_call (l, n) - - (* Call to Vanilla or constructor *) - | (Pvar v, _) -> handle_named_call v - - (* Constructor. This case is rarely used *) - | (Pcons(_, v), _) -> handle_named_call v - - | Pcall(fct, sargs2), ltp -> - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - let body, ltp = lexp_call fct sargs2 ctx (i + 1) in - Call(body, new_args), ltp - - | e, _ -> - pexp_print e; print_string "\n"; - print_string ((pexp_to_string e) ^ "\n"); - lexp_fatal (pexp_location e) "This expression cannot be called" + match func, ltp with + (* FIXME: Rather than check a var name, define a builtin for it. *) + (* FIXME: Don't force func to be a Pvar. *) + | (Pvar (l, n), Var((_, "Macro"), _)) -> handle_macro_call (l, n) + (* FIXME: Handle special-forms here as well! *) + | _ -> handle_funcall ()

(* Read a pattern and create the equivalent representation *) @@ -555,15 +531,15 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match nosusp (env_lookup_expr ctx ((loc, name), idx)) with - (* We are matching a constructor *) - | Cons _ -> (name, loc, []), ctx + match env_lookup_expr ctx ((loc, name), idx) with + (* We are matching a constructor *) + | Some (Cons _) -> (name, loc, []), ctx

- (* name is defined but is not a constructor *) - (* it technically could be ... (expr option) *) - (* What about Var -> Cons ? *) - | _ -> let nctx = env_extend ctx var (LetDef target) dltype in - (name, loc, []), nctx) + (* name is defined but is not a constructor *) + (* it technically could be ... (expr option) *) + (* What about Var -> Cons ? *) + | _ -> let nctx = env_extend ctx var (LetDef target) dltype in + (name, loc, []), nctx)

(* would it not make a default match too? *) with Not_found -> @@ -641,9 +617,9 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = " is not a correct index.") in

(* get stored function *) - let lxp = match nosusp lxp with - | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | _ -> print_string "\n"; + let lxp = match lxp with + | Some (Call(Var((_, "Macro_"), _), [(_, fct)])) -> fct + | Some lxp -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n"; lexp_print lxp; print_string "\n"; lexp_fatal loc "Macro is ill formed" in @@ -846,8 +822,8 @@ and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with | [] -> (List.rev acc) - | _ -> let lxp, _ = _lexp_p_infer (List.hd plst) ctx (i + 1) in - (loop (List.tl plst) ctx (lxp::acc)) in + | pe :: plst -> let lxp, _ = _lexp_p_infer pe ctx (i + 1) in + (loop plst ctx (lxp::acc)) in

(loop p ctx [])

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -33,6 +33,7 @@ open Lexp module S = Subst module L = List module B = Builtin +module DB = Debruijn

let conv_erase = true (* If true, conv ignores erased terms. *)

@@ -99,6 +100,28 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2

+(* Reduce to weak head normal form. + * WHNF implies: + * - Not a Let. + * - Not a let-bound variable. + * - Not a Susp. + * - Not an instantiated Metavar. + * - Not a Call (Lambda _). + * - Not a Call (Call _). + * - Not a Call (_, []). + * - Not a Case (Cons _). + * - Not a Call (MetaSet, ..). + *) +let rec lexp_whnf e ctx = match e with + | Var v -> (match DB.env_lookup_expr ctx v with + | None -> e + (* FIXME: We shouldn't do this blindly for recursive definitions! *) + | Some e' -> lexp_whnf e' ctx) + | Susp (e, s) -> lexp_whnf (push_susp e s) ctx + (* FIXME: Obviously incomplete! *) + | e -> e + + (********* Testing if a lexp is properly typed *********)

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