Stefan pushed to branch master at Stefan / Typer

Commits: fac6cb52 by Stefan Monnier at 2016-09-26T09:30:40-04:00 Allow expressions as constructor names and inductive type refs

* src/lexp.ml (lexp): Allow an lexp for the inductive type arg of Cons. (lexp_unparse): Adjust accordingly. (push_susp): Adjust accordingly. Also merge fix from unification branch.

* src/lparse.ml (_lexp_p_infer): Adjust to new Pcons and Cons (lexp_get_inductive_type): Remove. (lexp_read_pattern): Adjust to new Ppatcons.

* src/opslexp.ml (conv_p', check): Adjust to new Cons.

* src/pexp.ml (ppat): Allow any exp as constructor. (pexp): Allow an exp for the inductive type arg of Cons.

- - - - -

4 changed files:

- src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/pexp.ml

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -60,7 +60,7 @@ type ltype = lexp | Inductive of U.location * label * ((arg_kind * vdef * ltype) list) (* formal Args *) * ((arg_kind * vdef option * ltype) list) SMap.t - | Cons of vref * symbol (* = Type info * ctor_name *) + | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp * ltype (* The base inductive type over which we switch. *) * ltype (* The type of the return value of all branches *) @@ -300,7 +300,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) ncase) cases in Inductive (l, label, nargs, ncases) - | Cons _ -> e + | Cons (it, name) -> Cons (mkSusp it s, name) | Case (l, e, it, ret, cases, default) -> Case (l, mkSusp e s, mkSusp it s, mkSusp ret s, SMap.map (fun (l, cargs, e) @@ -317,14 +317,13 @@ let rec push_susp e s = (* Push a suspension one level down. *) (* 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 - * rather than Susp. *) - | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *) - push_susp e (scompose s' s) - | (Var _) - -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *) - push_susp (mkSusp e s) S.identity - -let nosusp e = (* Return `e` without `Susp`. *) + * rather than Susp. + * But we still have to handle them here, since push_susp is called + * in many other cases than just when we bump into a Susp. *) + | Susp (e,s') -> push_susp e (scompose s' s) + | (Var _) -> nosusp (mkSusp e s) + +and nosusp e = (* Return `e` without `Susp`. *) match e with | Susp(e, s) -> push_susp e s | _ -> e @@ -497,7 +496,7 @@ let rec lexp_unparse lxp = | Imm (sexp) -> Pimm (sexp) | Builtin ((loc, name), _) -> Pvar((loc, name)) | Var ((loc, name), _) -> Pvar((loc, name)) - | Cons (((iloc, iname), idx), ctor) -> Pcons((iloc, iname), ctor) + | Cons (t, ctor) -> Pcons (lexp_unparse t, ctor) | Lambda (kind, vdef, ltp, body) -> Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body) | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> @@ -532,6 +531,7 @@ let rec lexp_unparse lxp = in Pinductive(label, pfargs, ctor)

| Case (loc, target, tltp, bltp, branches, default) -> + let bt = lexp_unparse bltp in let pbranch = List.map (fun (str, (loc, args, bch)) -> match args with | [] -> Ppatvar (loc, str), lexp_unparse bch @@ -540,7 +540,9 @@ let rec lexp_unparse lxp = match vdef with | Some vdef -> Some (kind, vdef), Ppatvar(vdef) | None -> None, Ppatany(loc)) args - in Ppatcons ((loc, str), pat_args), lexp_unparse bch + (* 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 @@ -689,8 +691,8 @@ and _lexp_to_str ctx exp = (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ (make_indent 1) ^ (lexp_to_stri 1 lbody)

- | Cons(((_, idt_name), idx), (_, ctor_name)) -> - (keyword "inductive-cons ") ^ idt_name ^ (index idx) ^ " " ^ ctor_name + | Cons(t, (_, ctor_name)) -> + (keyword "inductive-cons ") ^ (lexp_to_str t) ^ " " ^ ctor_name

| Call(fname, args) -> ( (* get function name *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -234,45 +234,30 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = lexp_call fname _args ctx i

(* Pcons *) - | Pcons(vr, sym) -> ( - let (loc, type_name) = vr in - let (_, cname) = sym in + | Pcons(t, sym) -> + let idt, _ = lexp_infer t ctx in + let (loc, cname) = sym in

- (* 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 = match env_lookup_expr ctx (vr, idx) with - | Some idt -> idt - | None -> lexp_fatal loc ("expression " ^ type_name ^ " not found") in + (* Get constructor args *) + let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) with + | Inductive(_, _, formal, ctor_def) -> ( + try formal, (SMap.find cname ctor_def) + with Not_found -> + lexp_error loc + ("Constructor "" ^ cname ^ "" does not exist"); + [], [])

- (* make Base type *) - let inductive_type = Var((loc, type_name), idx) in + | _ -> lexp_error loc "Not an Inductive Type"; [], [] in

- (* Get constructor args *) - let formal, args = match nosusp idt with - | Inductive(_, _, formal, ctor_def) -> ( - try formal, (SMap.find cname ctor_def) - with Not_found -> - lexp_error loc - ("Constructor "" ^ cname ^ "" does not exist"); - [], []) + (* build Arrow type *) + let cons_type = List.fold_left (fun ltp (kind, v, tp) -> + Arrow(kind, v, tp, loc, ltp)) idt (List.rev args) in

- | _ -> lexp_error loc "Not an Inductive Type"; [], [] in + (* Add Aerasable argument *) + let cons_type = List.fold_left (fun ltp (kind, v, tp) -> + Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in

- (* build Arrow type *) - let cons_type = List.fold_left (fun ltp (kind, v, tp) -> - Arrow(kind, v, tp, loc, ltp)) inductive_type (List.rev args) in - - (* Add Aerasable argument *) - let cons_type = List.fold_left (fun ltp (kind, v, tp) -> - Arrow(Aerasable, Some v, tp, loc, ltp)) cons_type (List.rev formal) in - - Cons((vr, idx), sym), cons_type - - with Not_found -> - lexp_error loc - ("The inductive type: " ^ type_name ^ " was not declared"); - Cons((vr, -1), sym), dltype) + Cons(idt, sym), cons_type

(* Pcase: we can infer iff `patterns` is not empty *) | Pcase (loc, target, patterns) -> @@ -538,35 +523,19 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall ()

-(* return the inductive type declaration from the constructor *) -and lexp_get_inductive_type loc ctor_name ctx : (string * lexp option) = - let cons_idx = senv_lookup ctor_name ctx in - let cons = match env_lookup_expr ctx ((loc, ctor_name), cons_idx) with - | Some lxp -> lxp - | None -> lexp_warning loc ("constructor "" ^ ctor_name ^ "" not found"); dltype in - - (* get inductive type index *) - match cons with - | Cons(((_, name), idx), _) -> - (* get inductive type declaration *) - name, env_lookup_expr ctx ((loc, name), idx + cons_idx) - - | _ -> lexp_warning loc (ctor_name ^ " is not a constructor"); - "", None - (* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx: ((string * location * (arg_kind * vdef option) list) * elab_context) =

match pattern with - | Ppatany (loc) -> (* Catch all expression nothing to do *) + | 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 *) + (* We are matching a constructor. *) | Some (Cons _) -> (name, loc, []), ctx

(* name is defined but is not a constructor *) @@ -575,28 +544,30 @@ and lexp_read_pattern pattern exp target ctx: | _ -> let nctx = ctx_define ctx var target dltype in (name, loc, []), nctx)

- (* would it not make a default match too? *) + (* Would it not make a default match too? *) with Not_found -> - (* Create a variable containing target *) + (* Create a variable containing target. *) let nctx = ctx_define ctx var target dltype in (name, loc, []), nctx)

- | Ppatcons (ctor_name, args) -> - let (loc, cons_name) = ctor_name in - - (* We need the constructor type info *) - let inductive_name, inductive_ref = match lexp_get_inductive_type loc cons_name ctx with - | name, Some lxp -> name, lxp - | _ -> "", dltype in - - (*get cons argument types *) - let cons_args = match inductive_ref with - | Inductive(_, _, _, map) -> (try SMap.find cons_name map - with Not_found -> lexp_warning loc - (inductive_name ^ " does not hold a " ^ cons_name ^ " constructor"); []) - | _ -> [] in - - (* remove non explicit argument *) + | Ppatcons (ctor, args) -> + (* Get cons argument types. *) + let lctor, _ = lexp_p_infer ctor ctx 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(_, _, _, map) + -> (try SMap.find cons_name map + with Not_found + -> lexp_warning loc + ("`" ^ lexp_to_str (it) + ^ "` does not hold a `" + ^ cons_name ^ "` constructor"); []) + | it -> lexp_fatal loc + ("`" ^ lexp_to_str (it) + ^ "` is not an inductive type!") in + + (* Remove non explicit argument. *) let rec remove_nexplicit args acc = match args with | [] -> List.rev acc

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -108,7 +108,7 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = | _,_ -> false in l1 == l2 && conv_args s1 s2 args1 args2 && SMap.equal (conv_fields s1 s2) cases1 cases2 - | (Cons (v1, l1), Cons (v2, l2)) -> l1 == l2 && conv_p (Var v1) (Var v2) + | (Cons (t1, l1), Cons (t2, l2)) -> l1 == l2 && conv_p t1 t2 (* FIXME: Various missing cases, such as Let, Case, and beta-reduction. *) | (_, _) -> false

@@ -329,9 +329,9 @@ let rec check ctx e = | _ -> ()) | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret - | Cons (vr, (_, name)) - -> (match lookup_value ctx vr with - | Some (Inductive (l, _, fargs, constructors) as it) + | Cons (t, (_, name)) + -> (match lexp_whnf t ctx with + | Inductive (l, _, fargs, constructors) as it -> let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = match fargs with

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -36,15 +36,6 @@ type pvar = symbol (* type sort = Type | Ext *) (* type tag = string *)

-type 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 - (* FIXME: For modules and such, we'll want to generalize this - * `pvar' to a pexp. *) - | Ppatcons of pvar * ((arg_kind * symbol) option * ppat) list - type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) @@ -59,9 +50,16 @@ type pexp = * otherwise isomorphic types. *) | Pinductive of symbol * (arg_kind * pvar * pexp option) list * (symbol * (arg_kind * pvar option * pexp) list) list - | Pcons of pvar * symbol + | Pcons of pexp * symbol | Pcase of location * pexp * (ppat * pexp) list

+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 + and pdecl = | Ptype of symbol * pexp (* identifier : expr *) | Pexpr of symbol * pexp (* identifier = expr *) @@ -80,13 +78,13 @@ let rec pexp_location e = | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f | Pinductive ((l,_), _, _) -> l - | Pcons ((l,_),_) -> l + | Pcons (e,_) -> pexp_location e | Pcase (l, _, _) -> l

let rec pexp_pat_location e = match e with | Ppatany l -> l | Ppatvar (l,_) -> l - | Ppatcons ((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". *) @@ -159,8 +157,8 @@ let rec pexp_parse (s : sexp) : pexp = | Node (Symbol (start, "inductive_"), _) -> pexp_error start "Unrecognized inductive type"; Pmetavar (start, "_") (* constructor *) - | Node (Symbol (start, "inductive-cons"), [Symbol tname; Symbol tag]) - -> Pcons (tname, tag) + | Node (Symbol (start, "inductive-cons"), [e; Symbol tag]) + -> Pcons (pexp_parse e, tag) | Node (Symbol (start, "cons_"), _) -> pexp_error start "Unrecognized constructor call"; Pmetavar (start, "_") (* cases analysis *) @@ -266,15 +264,15 @@ and pexp_u_pat_arg (arg : (arg_kind * symbol) option * ppat) : sexp = and pexp_p_pat (s : sexp) : ppat = match s with | Symbol (l, "_") -> Ppatany l | Symbol s -> Ppatvar s - | Node (Symbol c, args) - -> Ppatcons (c, List.map pexp_p_pat_arg args) + | Node (c, args) + -> Ppatcons (pexp_parse 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, "_") | Ppatvar s -> Symbol s - | Ppatcons (c, args) -> Node (Symbol c, List.map pexp_u_pat_arg args) + | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args)

and pexp_p_decls e: pdecl list = match e with @@ -337,9 +335,9 @@ and pexp_unparse (e : pexp) : sexp = -> Node (Symbol s, List.map pexp_u_ind_arg types)) branches) - | Pcons (tname, ((l,_) as tag)) -> + | Pcons (t, ((l,_) as tag)) -> Node (Symbol (l, "cons_"), - [Symbol tname; Symbol tag]) + [pexp_unparse t; Symbol tag]) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"), pexp_unparse e @@ -417,5 +415,5 @@ let pexp_to_string e = | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" | Pinductive ((_,_), _, _) -> "Pinductive" - | Pcons ((_,_),_) -> "Pcons" + | Pcons (_,_) -> "Pcons" | Pcase (_, _, _) -> "Pcase"

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