Stefan pushed to branch unification 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.

- - - - - a761156c by Stefan Monnier at 2016-09-26T09:50:04-04:00 Merge branch 'trunk' into unification

- - - - -

6 changed files:

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

Changes:

===================================== src/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -40,7 +40,7 @@ and string_of_lxp lxp = | L.Imm (Sexp.Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")" | L.Imm (Sexp.String (_, value)) -> "String(" ^ value ^ ")" | L.Imm (Sexp.Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")" - | L.Cons (((_,tname),_),(_, cname)) -> "Cons(" ^ tname ^ ", " ^ cname ^")" + | L.Cons (it, (_, cname)) -> "Cons(" ^ string_of_lxp it ^ ", " ^ cname ^")" | L.Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")" | L.Let (_) -> "Let(..)" | L.Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")" @@ -77,7 +77,7 @@ let rec colored_string_of_lxp lxp lcol vcol = | L.Imm (Sexp.Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")" | L.Imm (Sexp.String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")" | L.Imm (Sexp.Float (_, value)) -> (lcol "Float" ) ^ "(" ^ (vcol (string_of_float value)) ^ ")" - | L.Cons (((_,name),_),_) -> (lcol "Cons" ) ^ "(" ^ (vcol name) ^ ")" + | L.Cons (it, _) -> (lcol "Cons" ) ^ "(" ^ (colored_string_of_lxp it lcol vcol) ^ ")" | L.Builtin ((_, name), _) -> (lcol "Builtin") ^ "(" ^ (vcol name) ^ ")" | L.Let (_) -> (lcol "Let(..)") | L.Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")" @@ -121,7 +121,8 @@ let rec string_of_pexp pxp = | Pexp.Plambda _ -> "Plambda (...)" | Pexp.Pcall _ -> "Pcall (...)" | Pexp.Pinductive _ -> "Pinductive (...)" - | Pexp.Pcons ( (_, s), (_, s2) ) -> "Pcons (" ^ s ^ ", " ^ s2 ^ ")" + | Pexp.Pcons (it, (_, s2)) -> "Pcons (" ^ string_of_pexp it + ^ ", " ^ s2 ^ ")" | Pexp.Pcase _ -> "Pcase (...)" | _ -> "Pexp not handled"

===================================== 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 *) @@ -307,7 +307,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) @@ -503,7 +503,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) -> @@ -538,6 +538,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 @@ -546,7 +547,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 @@ -697,8 +700,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 @@ -232,49 +232,36 @@ 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 - - (* 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 - - (* make Base type *) - let inductive_type = Var((loc, type_name), idx) 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"); - [], []) - | _ -> lexp_error loc "Not an Inductive Type"; - Debug_fun.do_debug (fun () -> - print_string ("idt : " ^ Fmt_lexp.string_of_lxp (nosusp idt) ^ ", p : " ^ (Fmt_lexp.string_of_pexp p)); - print_newline (); ()); - [], [] - 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) + | Pcons(t, sym) -> + let idt, _ = lexp_infer t ctx in + let (loc, cname) = sym in + let meta_ctx, _ = !global_substitution in + + (* Get constructor args *) + let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) + meta_ctx with + | Inductive(_, _, formal, ctor_def) -> ( + try formal, (SMap.find cname ctor_def) + with Not_found -> + lexp_error loc + ("Constructor "" ^ cname ^ "" does not exist"); + [], []) + + | _ -> lexp_error loc "Not an Inductive Type"; + Debug_fun.do_debug (fun () -> + print_string ("idt : " ^ Fmt_lexp.string_of_lxp (nosusp idt) ^ ", p : " ^ (Fmt_lexp.string_of_pexp p)); + print_newline (); ()); + [], [] in + + (* 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 + + (* 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(idt, sym), cons_type

(* Pcase: we can infer iff `patterns` is not empty *) | Pcase (loc, target, patterns) -> @@ -594,35 +581,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 *) @@ -631,28 +602,32 @@ 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 + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with + | Cons (it, (loc, cons_name)) + -> let cons_args = match OL.lexp_whnf it (ectx_to_lctx ctx) + meta_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

@@ -131,7 +131,7 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx = +let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx"); @@ -339,9 +339,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 VMap.empty 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"

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -115,10 +115,8 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = *) and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = match (cons, lxp) with - | (Cons ((_, idx), (_, name)), - Cons ((_, idx2), (_, name2))) when name = name2 -> - if idx = idx2 then Some (subst, []) - else None + | (Cons (it1, (_, name)), + Cons (it2, (_, name2))) when name = name2 -> unify it1 it2 subst | (_, _) -> None

(** Unify a builtin (bltin) and a lexp (lxp) if it is possible

View it on GitLab: https://gitlab.com/monnier/typer/compare/df72decc0f773ba25bf13abbf2f87f57603...