Stefan pushed to branch master at Stefan / Typer

Commits: 7fa6faac by Stefan Monnier at 2016-05-05T20:36:48-04:00 * src/lexp.ml (lexp): Add return type to `Case`

(_lexp_to_str): * src/typecheck.ml (unsusp, check): * src/lparse.ml (_lexp_p_infer): * src/eval.ml (_eval): Adjust accordingly.

- - - - -

4 changed files:

- src/eval.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml

Changes:

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -95,7 +95,8 @@ let rec _eval lxp ctx i: (value_type) = | Call (lname, args) -> eval_call ctx i lname args

(* Case *) - | Case (loc, target, _, pat, dflt) -> (eval_case ctx i loc target pat dflt) + | Case (loc, target, _, _, pat, dflt) + -> (eval_case ctx i loc target pat dflt)

| _ -> print_string "debug catch-all eval: "; lexp_print lxp; Vstring("eval Not Implemented")

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -79,6 +79,7 @@ type ltype = lexp | Cons of vref * symbol (* = Type info * ctor_name *) | Case of location * lexp * ltype (* The base inductive type over which we switch. *) + * ltype (* The type of the return value of all branches *) * (location * (arg_kind * vdef) option list * lexp) SMap.t * lexp option (* Default. *) (* (* For logical metavars, there's no substitution. *) @@ -250,7 +251,7 @@ let rec lexp_location e = | Call (f,_) -> lexp_location f | Inductive (l,_,_,_) -> l | Cons (_,(l,_)) -> l - | Case (l,_,_,_,_) -> l + | Case (l,_,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e * | Metavar ((l,_),_,_) -> l *) @@ -549,6 +550,9 @@ and _lexp_print ctx e = print_string (_lexp_to_str ctx e) (* If I remember correctly ocaml doc, concat string is actually terrible *) (* It might be better to use a Buffer. *) and lexp_to_str exp = _lexp_to_str (!debug_ppctx) exp + +(* FIXME: We don't want lexp_to_str, instead we want lexp_to_pexp (aka + * "unparse"), which we can then combine with pexp_to_sexp, etc... *) and _lexp_to_str ctx exp = (* create a string instead of printing *)

@@ -640,6 +644,10 @@ and _lexp_to_str ctx exp =

match (str, args) with (* Special Operators *) + (* FIXME: Get rid of these special cases: + * Either use the boring (_+_ e1 e2) notation, or check the + * grammar to decide when we can use the infix notation and + * when to add parenthese. *) | ("_=_", [lhs; rhs]) -> binop_str " = " lhs rhs | ("_+_", [lhs; rhs]) -> binop_str " + " lhs rhs | ("_-_", [lhs; rhs]) -> binop_str " - " lhs rhs @@ -662,15 +670,18 @@ and _lexp_to_str ctx exp =

| Inductive (_, (_, name), args, ctors) -> let args_str = List.fold_left (fun str (arg_kind, (_, name), ltype) -> - str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " ^ (lexp_to_str ltype) ^ ")") + str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " + ^ (lexp_to_str ltype) ^ ")") "" args in

(keyword "inductive_") ^ " (" ^ name ^ args_str ^") " ^ (lexp_str_ctor ctx ctors)

- | Case (_, target, tpe, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_to_str target) ^ - " : " ^ (lexp_to_str tpe) in + | Case (_, target, tpe, _ret, map, dflt) ->( + let str = (keyword "case ") ^ (lexp_to_str target) + (* FIXME: `tpe' is the *base* type of `target`. E.g. if `target` + * is a `List Int`, then `tpe` will be `List`. + ^ * " : " ^ (lexp_to_str tpe) *) in let arg_str arg = List.fold_left (fun str v -> match v with

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -232,6 +232,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = Cons((vr, -1), sym), dltype)

(* Pcase *) + (* FIXME: This should be in lexp_p_check! *) | Pcase (loc, target, patterns) ->

let tlxp, tltp = lexp_infer target ctx in @@ -277,9 +278,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | hd::tl, None -> hd | _, Some v -> v (* This will change *) - | _, None -> lexp_error loc "case with no branch ?"; dltype in - - Case(loc, tlxp, tltp, lpattern, dflt), (return_type) + | _, None -> lexp_error loc "case with no branch ?"; dltype + in Case (loc, tlxp, tltp, return_type, lpattern, dflt), + (return_type)

| Phastype (_, pxp, ptp) -> let ltp, _ = lexp_infer ptp ctx in

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -159,8 +159,8 @@ let rec unsusp e s = (* Push a suspension one level down. *) cases in Inductive (l, label, nargs, ncases) | Cons _ -> e - | Case (l, e, it, cases, default) - -> Case (l, mkSusp e s, mkSusp it s, + | Case (l, e, it, ret, cases, default) + -> Case (l, mkSusp e s, mkSusp it s, mkSusp ret s, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left (fun s carg -> match carg with @@ -251,6 +251,8 @@ let rec check ctx e = | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); Arrow (ak, Some v, t, l, + (* FIXME: If ak is Aerasable, make sure the var only appears + * in type annotations. *) check (Myers.cons (0, Some v, Variable, t) ctx) e)) | Call (f, args) -> let ft = check ctx f in @@ -281,11 +283,10 @@ let rec check ctx e = let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in (* FIXME: Check cases! *) tct - (* | Case (l, e, it, branches, default) - * -> let et = check ctx e in *) + (*| Case (l, e, it, branches, default) + -> let et = check ctx e in (* FIXME: Check that `et` is derived from `it`. - * E.g. `et` could be `List Int` while `it` is `List`. *) - (* FIXME: If there are no branches nor default, then we have no - * way to infer the type! *) - (* FIXME: Check branches and default! *) - + * E.g. if `et` is `List Int` then `it` should be `List`. *) + SMap.iter (fun name (l, vdefs, branch) + -> + *)

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