[Typer] [Git][monnier/typer][master] Fix various typing and inference problems with `Case`

Stefan pushed to branch master at Stefan / Typer

Commits: a459a1ea by Stefan Monnier at 2016-10-20T15:28:17-04:00 Fix various typing and inference problems with `Case`

* GNUmakefile (OBFLAGS): Add debug info.

* src/elexp.ml (elexp): Add binding of scrutinee in the default branch. (elexp_string.maybe_str): Adjust print code accordingly.

* src/eval.ml (eval_case): Bind scrutinee in the default branch.

* src/lexp.ml (lexp): Add binding of scrutinee in the default branch. (push_susp, _lexp_to_str): Adjust accordingly. (lexp_unparse): Adjust to pexp changes.

* src/lparse.ml (elab_check_proper_type): Use lexp_print to get db indexes. (ctx_extend): New function. (_lexp_p_infer): Check that arrow's args are types. (lexp_case): Rewrite; fix problems with scoping. (lexp_read_pattern, lexp_read_pattern_args): Remove.

* src/opslexp.ml (lexp_whnf): Adjust to new `Case`. Preserve the non-whnf in the sub-parts we return. (check): Check that erasable inductive type fields have a proper type. Don't assume call_split returns whnf elements. Adjust to new `Case`. (clean_maybe): Adjust to new `Case`.

* src/pexp.ml (ppat): Rename Ppatvar to Ppatsym since it can be either a var or a constructor. Drop arg_kind from Ppatcons. (pexp_p_pat_arg): Only recognize := as explicit-implicit. (pexp_u_pat_arg): Only use := for explicit-implicit.

- - - - -

8 changed files:

- DESIGN - GNUmakefile - src/elexp.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/pexp.ml

Changes:

===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1710,9 +1710,20 @@ So we'd define numbers = numbers' 0

* Papers -** BigBang: Designing a statically typed scripting language -** Dependently typed Racket -** Dependently typed Haskell +** Macros and tactics +*** Rtac +[1] Dissertation: +https://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineeri... +[2] ESOP'16: +https://gmalecha.github.io/publication/2016/01/01/extensible-and-efficient-a... +[3] ITP'14: +https://gmalecha.github.io/publication/2014/07/14/compositional-computationa... +*** ssreflect +*** Mtac +** Other +*** BigBang: Designing a statically typed scripting language +*** Dependently typed Racket +*** Dependently typed Haskell "My dissertation (github.com/goldfirere/thesis) is about adding dependent types to GHC. I believe I've solved the first problem, basically by copying Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/). Still working @@ -1720,36 +1731,36 @@ on that practical problem, though. Expect some changes in time for 7.12 though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for some discussion here.)"

-** On Irrelevance and Algorithmic Equality in Predicative Type Theory, +*** On Irrelevance and Algorithmic Equality in Predicative Type Theory, Andreas Abel & Gabriel Scherer, FOSSACS 2011. -** "A few constructions on constructors" -** How to Make Ad Hoc Proof Automation Less Ad Hoc, Beta Ziliani -** http://homotopytypetheory.org/book/ -** CMU's 2013 Fall: 15-819 Advanced Topics in Programming Languages +*** "A few constructions on constructors" +*** How to Make Ad Hoc Proof Automation Less Ad Hoc, Beta Ziliani +*** http://homotopytypetheory.org/book/ +*** CMU's 2013 Fall: 15-819 Advanced Topics in Programming Languages http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%220... -** Propositions as Sessions, Philip Wadler -** A few constructions on constructors, by Conor et al. -** Constructive selection principle (Markov's principle) +*** Propositions as Sessions, Philip Wadler +*** A few constructions on constructors, by Conor et al. +*** Constructive selection principle (Markov's principle) http://www.encyclopediaofmath.org/index.php/Constructive_selection_principle https://en.wikipedia.org/wiki/Markov%27s_principle -** size-change termination, Lee, Jones and Ben-Amram, doi:10.1145/360204.360210 -** A Predicative Analysis of Structural Recursion, Andreas Abel and Thorsten Altenkirch, http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf -** A New Look at Generalized Rewriting in Type Theory, Matthieu Sozeau -** http://moca.inria.fr/ On the implementation of construction functions for non-free concrete +*** size-change termination, Lee, Jones and Ben-Amram, doi:10.1145/360204.360210 +*** A Predicative Analysis of Structural Recursion, Andreas Abel and Thorsten Altenkirch, http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf +*** A New Look at Generalized Rewriting in Type Theory, Matthieu Sozeau +*** http://moca.inria.fr/ On the implementation of construction functions for non-free concrete data types. F. Blanqui, T. Hardin and P. Weis. ESOP'07. -** The Nemerle language -** "A Theory of Typed Hygienic Macros" de David Herman +*** The Nemerle language +*** "A Theory of Typed Hygienic Macros" de David Herman http://www.ccs.neu.edu/home/dherman/research/papers/dissertation.pdf -** http://www.mpi-sws.org/~beta/mtac/ -** Non-strictly positive and elimination +*** http://www.mpi-sws.org/~beta/mtac/ +*** Non-strictly positive and elimination "Inductively defined types", by Thierry Coquand and Christine Paulin, COLOG'88, LNCS 417 -** Dependently Typed Programming based on Automated Theorem Proving, Alasdair Armstrong, Simon Foster, and Georg Struth. +*** Dependently Typed Programming based on Automated Theorem Proving, Alasdair Armstrong, Simon Foster, and Georg Struth. http://arxiv.org/pdf/1112.3833v1

-** Strong Normalization for Coq (CiC). +*** Strong Normalization for Coq (CiC). http://www.cs.rice.edu/~emw4/uniform-lr.pdf -** Irrelevant/erasable args +*** Irrelevant/erasable args

*** The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Bruno Barras and Bruno Bernardo, fossacs08.

@@ -1779,7 +1790,7 @@ Finally we show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic.

-** Parametricity and variants of Girard's J operator, Robert Harper and John C. Mitchell, Journal Information Processing Letters archive, Volume 70 Issue 1, April 01, 1999 +*** Parametricity and variants of Girard's J operator, Robert Harper and John C. Mitchell, Journal Information Processing Letters archive, Volume 70 Issue 1, April 01, 1999 The Girard-Reynolds polymorphic λ-calculus is generally regarded as a calculus of parametric polymorphism in which all well-formed terms are strongly normalizing with respect to β-reductions. Girard demonstrated that @@ -1793,10 +1804,10 @@ impredicativity is essential to the argument; predicative variants of the polymorphic λ-calculus admit non-parametric operations without sacrificing normalization.

-** Idris (Edwin Brady) -** http://albatross-lang.sourceforge.net -** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf -** Read +*** Idris (Edwin Brady) +*** http://albatross-lang.sourceforge.net +*** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf +*** Read *** (Co)Iteration for higher-order nested datatypes, Andreas Abel and Ralph Matthes, [Abel03] *** Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna. http://www.cs.st-andrews.ac.uk/~eb/writings/types2003.pdf

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -4,7 +4,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./_build/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml)

-OBFLAGS = -build-dir _build +OBFLAGS = -lflags -g -cflags -g -build-dir _build # COMPILE_MODE = native

all: typer debug tests-build

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -52,8 +52,9 @@ type elexp = | Lambda of vdef * elexp | Call of elexp * elexp list | Cons of symbol - | Case of U.location * elexp * - (U.location * (vdef option) list * elexp) SMap.t * elexp option + | Case of U.location * elexp + * (U.location * (vdef option) list * elexp) SMap.t + * (vdef option * elexp) option (* Type place-holder just in case *) | Type (* Inductive takes a slot in the env that is why it need to be here *) @@ -90,8 +91,10 @@ let rec elexp_print lxp = print_string (elexp_string lxp) and elexp_string lxp = let maybe_str lxp = match lxp with - | Some lxp -> " | _ => " ^ (elexp_string lxp) - | None -> "" in + | Some (v, lxp) + -> " | " ^ (match v with None -> "_" | Some (_,name) -> name) + ^ " => " ^ elexp_string lxp + | None -> "" in

let str_decls d = List.fold_left (fun str ((_, s), lxp) ->

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -363,7 +363,9 @@ and eval_case ctx i loc target pat dflt =

(* Run default *) with Not_found -> (match dflt with - | Some lxp -> _eval lxp ctx i + | Some (var, lxp) + -> let var' = match var with None -> None | Some (_, n) -> Some n in + _eval lxp (add_rte_variable var' v ctx) i | _ -> error loc "Match Failure")

and build_arg_list args ctx i =

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -41,8 +41,19 @@ type label = symbol

(*************** Elaboration to Lexp *********************)

-(* Pour la propagation des types bidirectionnelle, tout va dans `infer`, - * sauf Lambda et Case qui vont dans `check`. Je crois. *) +(* The scoping of `Let` is tricky: + * + * Since it's a recursive let, the definition part of each binding is + * valid in the "final" scope which includes all the new bindings. + * + * But the type of each binding is not defined in that same scope. Instead + * it's defined in the scope of all the previous bindings. + * + * For exemple the type of the second binding of such a Let is defined in + * the scope of the surrounded context extended with the first binding. + * And the type of the 3rd binding is defined in the scope of the + * surrounded context extended with the first and the second bindings. *) + type ltype = lexp and subst = lexp S.subst and lexp = @@ -64,7 +75,7 @@ type ltype = lexp | Case of U.location * lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t - * lexp option (* Default. *) + * (vdef option * lexp) option (* Default. *) (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -276,7 +287,7 @@ let rec lexp_location e =

(********* Normalizing a term *********)

-let vdummy = (U.dummy_location, "dummy") +let vdummy = (U.dummy_location, "<anon>") let maybev mv = match mv with None -> vdummy | Some v -> v

let rec push_susp e s = (* Push a suspension one level down. *) @@ -325,7 +336,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) cases, match default with | None -> default - | Some e -> Some (mkSusp e s)) + | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -546,19 +557,24 @@ let rec lexp_unparse lxp = let bt = lexp_unparse bltp in let pbranch = List.map (fun (str, (loc, args, bch)) -> match args with - | [] -> Ppatvar (loc, str), lexp_unparse bch + | [] -> Ppatsym (loc, str), lexp_unparse bch | _ -> - let pat_args = List.map (fun (kind, vdef) -> - match vdef with - | Some vdef -> Some (kind, vdef), Ppatvar(vdef) - | None -> None, Ppatany(loc)) args + let pat_args + = List.map (fun (kind, vdef) + -> match vdef with + | Some vdef -> Some vdef, Ppatsym vdef + | None -> None, Ppatany loc) + args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in Ppatcons (Pcons (bt, (loc, str)), pat_args), lexp_unparse bch ) (SMap.bindings branches) in

let pbranch = match default with - | Some dft -> (Ppatany(loc), lexp_unparse dft)::pbranch + | Some (v,dft) -> ((match v with + | None -> Ppatany loc + | Some vdef -> Ppatsym vdef), + lexp_unparse dft)::pbranch | None -> pbranch in Pcase (loc, lexp_unparse target, pbranch)

@@ -776,8 +792,10 @@ and _lexp_to_str ctx exp =

match dflt with | None -> str - | Some df -> - str ^ nl ^ (make_indent 1) ^ "| _ => " ^ (lexp_to_stri 1 df)) + | Some (v, df) -> + str ^ nl ^ (make_indent 1) + ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name) + ^ " => " ^ (lexp_to_stri 1 df))

| Builtin ((_, name), _) -> name

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -94,14 +94,15 @@ let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *) | _ -> lexp_error l ltp - ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) + ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_string ltp)

let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp - with e -> print_string ("Exception while checking type `" - ^ lexp_string ltp ^ "` of var `" ^ - (let (_, name) = v in name) ^"`\n"); + with e -> print_string "Exception while checking type `"; + lexp_print ltp; + print_string ("` of var `" + ^ (let (_, name) = v in name) ^"`\n"); print_lexp_ctx (ectx_to_lctx ctx); raise e

@@ -124,6 +125,10 @@ let elab_check_def (ctx : elab_context) var lxp ltype = " because"; (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);])

+let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = + elab_check_proper_type ctx ltype (maybev var); + ectx_extend ctx var def ltype + let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; env_extend ctx var (LetDef lxp) ltype @@ -229,9 +234,11 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> let ltp, _ = lexp_infer tp ctx in + let _ = elab_check_proper_type ctx ltp (maybev ovar) in let nctx = ectx_extend ctx ovar Variable ltp in

let lxp, _ = lexp_infer expr nctx in + let _ = elab_check_proper_type nctx lxp (maybev ovar) in

let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, type0 @@ -294,7 +301,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =

| lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in

- (* build Arrow type *) + (* Build Arrow type. *) let target = if formal = [] then push_susp idt (S.shift (List.length args)) else @@ -382,47 +389,113 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = (* FIXME: check if case is exhaustive *) (* Helpers *)

- let lexp_infer p ctx = _lexp_p_infer p ctx i in + let lexp_infer p ctx = _lexp_p_infer p ctx i in

- let uniqueness_warn name = - warning loc ("Pattern " ^ name ^ " is a duplicate." ^ - " It will override previous pattern.") in + let pat_string p = sexp_string (pexp_u_pat p) in

- let check_uniqueness loc name map = - try let _ = SMap.find name map in uniqueness_warn name + let uniqueness_warn pat = + warning (pexp_pat_location pat) + ("Pattern " ^ pat_string pat + ^ " is a duplicate. It will override previous pattern.") in + + let check_uniqueness pat name map = + try let _ = SMap.find name map in uniqueness_warn pat with e -> () in

(* get target and its type *) let tlxp, tltp = lexp_infer target ctx in - let rec call_split e = - match e with - | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) + (* FIXME: We need to be careful with whnf: while the output is equivalent + * to the input, it's not necessarily as readable. So try to reuse the + * "non-whnf" form whenever possible. *) + let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx)) with + | Call (f, args) -> (f, args) | _ -> (e,[]) in - let it, targs = call_split (OL.lexp_whnf tltp (ectx_to_lctx ctx)) in - let _ = match it with - | Inductive (_, _, fargs, _) - -> assert (List.length fargs = List.length targs); () + let it, targs = call_split tltp in + let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with + | Inductive (_, _, fargs, constructors) + -> assert (List.length fargs = List.length targs); + constructors | _ -> lexp_error (pexp_location target) tlxp ("Can't `case` on objects of this type: " - ^ lexp_string tltp) in + ^ lexp_string tltp); + SMap.empty in

(* Read patterns one by one *) - let fold_fun (lbranches, dflt) (pat, exp) = - (* Create pattern context *) - let (name, iloc, arg), nctx = lexp_read_pattern pat tlxp ctx i in + let fold_fun (lbranches, dflt) (pat, pexp) =

- (* parse using pattern context *) + let add_default v = + (if dflt != None then uniqueness_warn pat); + let nctx = ctx_extend ctx v Variable tltp in let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in - let exp = _lexp_p_check exp rtype' nctx i in - - if name = "_" then ( - (if dflt != None then uniqueness_warn name); - lbranches, (Some exp) - ) else ( - check_uniqueness iloc name lbranches; - let lbranches = SMap.add name (iloc, arg, exp) lbranches in - lbranches, dflt) in + let lexp = _lexp_p_check pexp rtype' nctx i in + lbranches, Some (v, lexp) in + + let add_branch pctor pargs = + let loc = pexp_location pctor in + let lctor, _ = _lexp_p_infer pctor ctx i in + match OL.lexp_whnf lctor (ectx_to_lctx ctx) with + | Cons (it', (_, cons_name)) + -> let _ = if OL.conv_p it' it then () + else lexp_error loc lctor + ("Expected pattern of type `" + ^ lexp_string it ^ "` but got `" + ^ lexp_string it' ^ "`") in + let _ = check_uniqueness pat cons_name lbranches in + let cons_args + = try SMap.find cons_name constructors + with Not_found + -> lexp_error loc lctor + ("`" ^ (lexp_string it) + ^ "` does not have a `" + ^ cons_name ^ "` constructor"); + [] in + + let subst = List.fold_right (fun (_, t) s -> S.cons t s) + targs S.identity in + let rec make_nctx ctx fargs s pargs cargs = match pargs, cargs with + | [], [] -> ctx, List.rev fargs + | (_, pat)::_, [] + -> lexp_error loc lctor + "Too many arguments to the constructor"; + make_nctx ctx fargs s [] [] + | (None, Ppatany _)::pargs, (Aexplicit, _, fty)::cargs + -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + make_nctx nctx ((Aexplicit, None)::fargs) + (ssink vdummy s) pargs cargs + | (None, Ppatsym v)::pargs, (Aexplicit, _, fty)::cargs + -> let nctx = ctx_extend ctx (Some v) Variable (mkSusp fty s) in + make_nctx nctx ((Aexplicit, Some v)::fargs) + (ssink v s) pargs cargs + | (_, Ppatcons (p, _))::pargs, cargs + -> lexp_error (pexp_location p) lctor + "Nested patterns not supported!"; + make_nctx ctx fargs s pargs cargs + | pargs, (ak, _, fty)::cargs + -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + make_nctx nctx ((ak, None)::fargs) + (ssink vdummy s) pargs cargs in + let nctx, fargs = make_nctx ctx [] subst pargs cons_args in + let rtype' = mkSusp rtype + (S.shift (M.length (ectx_to_lctx nctx) + - M.length (ectx_to_lctx ctx))) in + let lexp = _lexp_p_check pexp rtype' nctx i in + SMap.add cons_name (loc, fargs, lexp) lbranches, + dflt + | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt + in + + match pat with + | Ppatany _ -> add_default None + | Ppatsym ((_, name) as var) + -> (try let idx = senv_lookup name ctx in + match OL.lexp_whnf (Var (var, idx)) (ectx_to_lctx ctx) with + | Cons _ (* It's indeed a constructor! *) + -> add_branch (Pvar var) [] + | _ -> add_default (Some var) (* A named default branch. *) + with Not_found -> add_default (Some var)) + + | Ppatcons (pctor, pargs) -> add_branch pctor pargs in

let (lpattern, dflt) = List.fold_left fold_fun (SMap.empty, None) ppatterns in @@ -543,102 +616,6 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall ()

-(* Read a pattern and create the equivalent representation *) -and lexp_read_pattern pattern target ctx trace - : ((string * location * (arg_kind * vdef option) list) - * elab_context) = - match pattern with - | Ppatany (loc) (* Catch all expression, nothing to do. *) - -> ("_", loc, []), ctx - - | Ppatvar ((loc, name) as var) ->( - try( - let idx = senv_lookup name ctx in - 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 = ctx_define ctx var target dltype in - (name, loc, []), nctx) - - (* Would it not make a default match too? *) - with Not_found -> - (* Create a variable containing target. *) - let nctx = ctx_define ctx var target dltype in - (name, loc, []), nctx) - - | Ppatcons (ctor, args) - -> (* Get cons argument types. *) - let lctor, _ = _lexp_p_infer ctor ctx trace in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) with - | Cons (it, (loc, cons_name)) - -> let cons_args = match OL.lexp_whnf it (ectx_to_lctx ctx) with - | Inductive(_, (_, label), _, map) - -> (try SMap.find cons_name map - with Not_found - -> warning loc ("`" ^ (lexp_string it) ^ "` does not hold a `" - ^ cons_name ^ "` constructor"); []) - | it -> fatal loc - ("`" ^ (lexp_string it) ^ "` is not an inductive type!") in - - (* FIXME: Don't remove them, add them without names! *) - (* FIXME: Add support for explicit-implicit fields! *) - (* Remove non explicit argument. *) - let rec remove_nexplicit args acc = - match args with - | [] -> List.rev acc - | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc) - | hd::tl -> remove_nexplicit tl acc in - - let cons_args = remove_nexplicit cons_args [] in - - (* read pattern args *) - let args, nctx = lexp_read_pattern_args args cons_args ctx in - (cons_name, loc, args), nctx - | _ -> warning (pexp_location ctor) - ("Invalid constructor `" ^ (pexp_string ctor) ^ "`"); - - ("_", pexp_location ctor, []), ctx - -(* Read patterns inside a constructor *) -and lexp_read_pattern_args args (args_type : lexp list) ctx: - (((arg_kind * vdef option) list) * elab_context)= - - let length_type = List.length args_type in - let length_pat = List.length args in - - let make_list elem size = - let rec loop i acc = - if i < size then loop (i + 1) (elem::acc) else acc - in loop 0 [] in - - let args_type = if length_type != length_pat then - make_list dltype length_pat else args_type in - - (if length_type != length_pat then warning dloc "Size Mismatch"); - - let rec loop args args_type acc ctx = - match args, args_type with - | [], _ -> (List.rev acc), ctx - | hd::tl, ltp::type_tl -> ( - let (_, pat) = hd in - match pat with - (* Nothing to do *) - | Ppatany (loc) -> loop tl type_tl ((Aexplicit, None)::acc) ctx - | Ppatvar ((loc, name) as var) -> - (* Add var *) - let nctx = env_extend ctx var Variable ltp in - let nacc = (Aexplicit, Some var)::acc in - loop tl type_tl nacc nctx - | _ -> error dloc "Constructor inside a Constructor"; - loop tl type_tl ((Aexplicit, None)::acc) ctx) - | _ -> typer_unreachable "unreachable branch" - - in loop args args_type [] ctx - (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx i = let lexp_parse p ctx = _lexp_p_infer p ctx i in

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -150,8 +150,9 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with args)) ctx | Call (e', xs1) -> Call (e', List.append xs1 xs) - | e' -> Call (e', xs)) + | e' -> Call (e, xs)) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> + let e' = lexp_whnf e ctx in let reduce name aargs = try let (_, _, branch) = SMap.find name branches in @@ -165,15 +166,16 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with lexp_whnf (push_susp branch subst) ctx with Not_found -> match default - with | Some default -> lexp_whnf default ctx + with | Some (v,default) + -> lexp_whnf (push_susp default (S.substitute e')) ctx | _ -> U.msg_error "WHNF" l ("Unhandled constructor " ^ name ^ "in case expression"); Case (l, e, rt, branches, default) in - (match lexp_whnf e ctx with + (match e' with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs - | e' -> Case (l, e', rt, branches, default)) + | _ -> Case (l, e', rt, branches, default)) | e -> e

@@ -297,19 +299,20 @@ let rec check ctx e = let level, _ = List.fold_left (fun (level, ctx) (ak, v, t) -> - (if ak == P.Aerasable && impredicative_erase - then level - else match lexp_whnf (check ctx t) ctx with - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> sort_level_max level level' - | tt -> U.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string tt ^")"); - DB.print_lexp_ctx ctx; - SortLevel SLz), + (match lexp_whnf (check ctx t) ctx with + | Sort _ when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max level level' + | tt -> U.msg_error "TC" (lexp_location t) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string tt ^")"); + (* DB.print_lexp_ctx ctx; + * U.internal_error "Oops"; *) + level), DB.lctx_extend ctx v Variable t) (level, ctx) case in @@ -322,11 +325,12 @@ let rec check ctx e = let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) - -> let rec call_split e = - match e with - | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) + -> let rec call_split e = match e with + | Call (f, args) -> (f, args) | _ -> (e,[]) in - (match call_split (lexp_whnf (check ctx e) ctx) with + let etype = lexp_whnf (check ctx e) ctx in + let it, aargs = call_split etype in + (match lexp_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -360,7 +364,9 @@ let rec check ctx e = assert_type branch ret (check nctx branch)) branches; (match default with - | Some d -> assert_type d ret (check ctx d) + | Some (v, d) + -> assert_type d (mkSusp ret (S.shift 1)) + (check (DB.lctx_extend ctx v (LetDef e) etype) d) | _ -> ()) | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret @@ -442,7 +448,7 @@ and clean_decls decls =

and clean_maybe lxp = match lxp with - | Some lxp -> Some (erase_type lxp) + | Some (v, lxp) -> Some (v, erase_type lxp) | None -> None

and clean_map cases =

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -57,8 +57,8 @@ 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 - | Ppatvar of pvar - | Ppatcons of pexp * ((arg_kind * symbol) option * ppat) list + | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *) + | Ppatcons of pexp * (symbol option * ppat) list

and pdecl = | Ptype of symbol * pexp (* identifier : expr *) @@ -83,7 +83,7 @@ let rec pexp_location e =

let rec pexp_pat_location e = match e with | Ppatany l -> l - | Ppatvar (l,_) -> l + | Ppatsym (l,_) -> l | Ppatcons (e, _) -> pexp_location e

(* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp" @@ -241,29 +241,23 @@ and pexp_u_ind_arg arg = match arg with

and pexp_p_pat_arg (s : sexp) = match s with | Symbol _ -> (None, pexp_p_pat s) - | Node (Symbol (_, "_:-_"), [Symbol f; Symbol s]) - -> (Some (Aexplicit, f), Ppatvar s) | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s]) - -> (Some (Aimplicit, f), Ppatvar s) - | Node (Symbol (_, "_:≡_"), [Symbol f; Symbol s]) - -> (Some (Aerasable, f), Ppatvar s) + -> (Some f, Ppatsym s) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; (None, Ppatany loc)

-and pexp_u_pat_arg (arg : (arg_kind * symbol) option * ppat) : sexp = +and pexp_u_pat_arg (arg : symbol option * ppat) : sexp = match arg with | (None, p) -> pexp_u_pat p - | (Some (k, ((l,_) as n)), p) -> - Node (Symbol (l, match k with Aexplicit -> "_:-_" - | Aimplicit -> "_:=_" - | Aerasable -> "_:≡_"), + | (Some ((l,_) as n), p) -> + Node (Symbol (l, "_:=_"), (* FIXME: the label is wrong! *) [Symbol (pexp_u_id (Some n)); pexp_u_pat p])

and pexp_p_pat (s : sexp) : ppat = match s with | Symbol (l, "_") -> Ppatany l - | Symbol s -> Ppatvar s + | Symbol s -> Ppatsym s | Node (c, args) -> Ppatcons (pexp_parse c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in @@ -271,7 +265,7 @@ and pexp_p_pat (s : sexp) : ppat = match s with

and pexp_u_pat (p : ppat) : sexp = match p with | Ppatany l -> Symbol (l, "_") - | Ppatvar s -> Symbol s + | Ppatsym s -> Symbol s | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args)

and pexp_p_decls e: pdecl list =

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