Simon Génier pushed to branch arity-of-cons at Stefan / Typer Commits: f92d48f1 by Simon Génier at 2021-03-07T00:37:33-05:00 Add information about the arity of data cons in Elexps. This is not used with the AST interpreter, but pretty much any other backend would want that information. - - - - - 6 changed files: - src/REPL.ml - src/elab.ml - src/elexp.ml - src/eval.ml - + src/listx.ml - src/opslexp.ml Changes: ===================================== src/REPL.ml ===================================== @@ -128,10 +128,19 @@ let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = pxp_parse sxps [] [] -let ierase_type (lexps: (ldecl list list * lexpr list)) = - let (ldecls, lexprs) = lexps in - (List.map OL.clean_decls ldecls), - (List.map OL.erase_type lexprs) +let ierase_type + (lctx : DB.lexp_context) + (ldecls, lexprs : ldecl list list * lexpr list) + : (vname * EL.elexp) list list * EL.elexp list = + + let erase_decl lctx ldecls = + let eldecls = OL.clean_decls lctx ldecls in + let lctx' = DB.lctx_extend_rec lctx ldecls in + lctx', eldecls + in + let lctx', eldecls = Listx.fold_left_map erase_decl lctx ldecls in + let elexprs = List.map (OL.erase_type lctx') lexprs in + eldecls, elexprs let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in @@ -159,7 +168,7 @@ let ieval f str ectx rctx = (* Different from usual typer *) let pxps = ipexp_parse nods in let lxps, ectx = ilexp_parse pxps ectx in - let elxps = ierase_type lxps in + let elxps = ierase_type (ectx_to_lctx ectx) lxps in let v, rctx = ieval' elxps rctx in v, ectx, rctx @@ -167,7 +176,7 @@ let raw_eval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in let lxps, ectx = Elab.lexp_p_decls [] sxps ectx in - let elxps = List.map OL.clean_decls lxps in + let elxps = List.map (OL.clean_decls (ectx_to_lctx ectx)) lxps in (* At this point, `elxps` is a `(vname * elexp) list list`, where: * - each `(vname * elexp)` is a definition * - each `(vname * elexp) list` is a list of definitions which can ===================================== src/elab.ml ===================================== @@ -1063,7 +1063,7 @@ and track_fv rctx lctx e = in String.concat " " (List.map tfv nc) and lexp_eval ectx e = - let ee = OL.erase_type e in + let ee = OL.erase_type (ectx_to_lctx ectx) e in let rctx = EV.from_ectx ectx in if not (EV.closed_p rctx (OL.fv e)) then @@ -1929,12 +1929,14 @@ let lexp_decl_str str ctx = * --------------------------------------------------------- *) (* Because we cant include Elab in eval.ml *) -let eval_expr_str str lctx rctx = - let lxps = lexp_expr_str str lctx in - let elxps = List.map OL.erase_type lxps in +let eval_expr_str str ectx rctx = + let lxps = lexp_expr_str str ectx in + let lctx = ectx_to_lctx ectx in + let elxps = List.map (OL.erase_type lctx) lxps in EV.eval_all elxps rctx false -let eval_decl_str str lctx rctx = - let lxps, lctx = lexp_decl_str str lctx in - let elxps = List.map OL.clean_decls lxps in - (EV.eval_decls_toplevel elxps rctx), lctx +let eval_decl_str str ectx rctx = + let lxps, ectx = lexp_decl_str str ectx in + let lctx = ectx_to_lctx ectx in + let elxps = List.map (OL.clean_decls lctx) lxps in + (EV.eval_decls_toplevel elxps rctx), ectx ===================================== src/elexp.ml ===================================== @@ -64,8 +64,9 @@ type elexp = * is just a shorthand for Call (Call (f, [e1]), [e2]). *) | Call of elexp * elexp list - (* A data constructor, such as `cons` or `nil`. *) - | Cons of symbol + (* A data constructor, such as `cons` or `nil`. The int is its arity and the + * symbol, its name. *) + | Cons of int * symbol (* Case analysis on an agebraic datatype. * Case (l, e, branches, default) @@ -87,7 +88,7 @@ let rec elexp_location e = | Let (l,_,_) -> l | Lambda ((l,_),_) -> l | Call (f,_) -> elexp_location f - | Cons ((l,_)) -> l + | Cons (_, (l, _)) -> l | Case (l,_,_,_) -> l | Type e -> L.lexp_location e @@ -133,14 +134,14 @@ and elexp_string lxp = str ^ " " ^ (elexp_string lxp)) "" lst in match lxp with - | Imm(s) -> sexp_string s - | Builtin((_, s)) -> s - | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" - | Cons((_, s)) -> "datacons(" ^ s ^")" + | Imm(s) -> sexp_string s + | Builtin((_, s)) -> s + | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" + | Cons (_, (_, s)) -> "datacons(" ^ s ^")" - | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b) + | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b) - | Let(_, d, b) -> + | Let(_, d, b) -> "let" ^ (str_decls d) ^ " in " ^ (elexp_string b) | Call(fct, args) -> ===================================== src/eval.ml ===================================== @@ -438,7 +438,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) | Imm(String (_, s)) -> Vstring s | Imm(Float (_, n)) -> Vfloat n | Imm(sxp) -> Vsexp sxp - | Cons (label) -> Vcons (label, []) + | Cons (_, label) -> Vcons (label, []) | Lambda (n, lxp) -> Closure (n, lxp, ctx) | Builtin ((_, str)) -> Vbuiltin str @@ -1149,7 +1149,7 @@ let from_lctx (lctx: lexp_context): runtime_env = ref (match def with | LetDef (_, e) -> if closed_p rctx (OL.fv e) then - eval (OL.erase_type e) rctx + eval (OL.erase_type lctx e) rctx else Vundefined | _ -> Vundefined)) rctx @@ -1170,7 +1170,7 @@ let from_lctx (lctx: lexp_context): runtime_env = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type e) nrctx) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx e) nrctx) evs else () in nrctx and from_lctx lctx = ===================================== src/listx.ml ===================================== @@ -0,0 +1,46 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier@umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. *) + +(* Backport from 4.08. *) +let filter_map (f : 'a -> 'b option) (xs : 'a list) : 'b list = + let rec loop xs ys = + match xs with + | [] -> List.rev ys + | x :: xs + -> (match f x with + | Some y -> loop xs (y :: ys) + | None -> loop xs ys) + in + loop xs [] + +(* Backport from 4.11. *) +let fold_left_map + (f : 'a -> 'b -> 'a * 'c) + (i : 'a) + (bs : 'b list) + : 'a * 'c list = + + let rec loop fold_acc map_acc bs = match bs with + | [] -> (fold_acc, List.rev map_acc) + | b :: bs + -> let fold_acc, new_element = f fold_acc b in + loop fold_acc (new_element :: map_acc) bs + in + loop i [] bs ===================================== src/opslexp.ml ===================================== @@ -48,6 +48,9 @@ type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t (* Metavars that appear in non-erasable positions. *) * unit IMap.t +let error ~location message = + Log.log_fatal ~section:"OPSLEXP" ~loc:location message + module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but * I haven't found any such functionality in OCaml's libs. *) @@ -1112,82 +1115,103 @@ let _ = register_reducible_builtins () a dummy. *) let erasure_dummy = DB.type0 -let rec erase_type (lxp: lexp): E.elexp = - match lexp_lexp' lxp with - | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _) -> E.Builtin(v) - | L.Var(v) -> E.Var(v) - | L.Cons(_, s) -> E.Cons(s) - | L.Lambda (P.Aerasable, _, _, body) -> - erase_type (L.push_susp body (S.substitute erasure_dummy)) - | L.Lambda (_, vdef, _, body) -> - E.Lambda (vdef, erase_type body) - - | L.Let(l, decls, body) -> - E.Let(l, (clean_decls decls), (erase_type body)) - - | L.Call(fct, args) -> - E.Call((erase_type fct), (filter_arg_list args)) - - | L.Case(l, target, _, cases, default) -> - E.Case(l, (erase_type target), (clean_map cases), - (clean_default default)) - - | L.Susp(l, s) -> erase_type (L.push_susp l s) - - (* To be thrown out *) - | L.Arrow _ -> E.Type lxp - | L.SortLevel _ -> E.Type lxp - | L.Sort _ -> E.Type lxp - (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar (idx, s, _) - -> (match metavar_lookup idx with - | MVal e -> erase_type (push_susp e s) - | MVar (_, t, _) - -> Log.internal_error "Metavar in erase_type") - -and filter_arg_list lst = - let rec filter_arg_list lst acc = - match lst with - | (kind, lxp)::tl -> - let acc = if kind != P.Aerasable then - (erase_type lxp)::acc else acc in - filter_arg_list tl acc - | [] -> List.rev acc in - filter_arg_list lst [] - -and clean_decls decls = - List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls - -and clean_default lxp = +let arity_of_cons + (lctx : DB.lexp_context) + (ty : lexp) + (location, name : symbol) + : int = + + match lexp'_whnf ty lctx with + | Inductive (_, _, _, constructors) + -> (match SMap.find_opt name constructors with + | Some params -> List.length params + | None -> error ~location ("invalid constructor: " ^ name)) + | _ + -> (let message = + {|can't deduce arity of constructor "|} + ^ name + ^ {|", because it is not an inductive type: |} + ^ lexp_string ty + in + error ~location:(lexp_location ty) message) + +let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = + match lexp_lexp' lxp with + | L.Imm (s) -> E.Imm (s) + | L.Builtin (v, _) -> E.Builtin (v) + | L.Var (v) -> E.Var (v) + | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) + + | L.Lambda (P.Aerasable, _, _, body) + -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy)) + + | L.Lambda (_, vdef, ty, body) + -> let lctx' = DB.lctx_extend lctx vdef Variable ty in + E.Lambda (vdef, erase_type lctx' body) + + | L.Let (l, decls, body) + -> let lctx' = DB.lctx_extend_rec lctx decls in + E.Let (l, clean_decls lctx' decls, erase_type lctx' body) + + | L.Call (fct, args) + -> E.Call (erase_type lctx fct, Listx.filter_map (clean_arg lctx) args) + + | L.Case (location, target, _, branches, default) + -> let etarget = erase_type lctx target in + let ebranches = clean_branch_map lctx branches in + E.Case (location, etarget, ebranches, clean_default lctx default) + + | L.Susp (l, s) -> erase_type lctx (L.push_susp l s) + + (* To be thrown out *) + | L.Arrow _ -> E.Type lxp + | L.SortLevel _ -> E.Type lxp + | L.Sort _ -> E.Type lxp + + (* Still useful to some extent. *) + | L.Inductive (_, _, _, _) -> E.Type lxp + | L.Metavar (idx, s, _) + -> (match metavar_lookup idx with + | MVal e -> erase_type lctx (push_susp e s) + | MVar _ -> Log.internal_error "Metavar in erase_type") + +and clean_arg lctx = function + | (P.Aerasable, _) -> None + | (_, lexp) -> Some (erase_type lctx lexp) + +and clean_decls lctx decls = + List.map (fun (v, lexp, _) -> (v, erase_type lctx lexp)) decls + +and clean_default lctx lxp = match lxp with - | Some (v, lxp) -> - Some (v, - erase_type (L.push_susp lxp (S.substitute erasure_dummy))) + | Some (v, lxp) + -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) in + Some (v, erase_type lctx lxp') | None -> None -and clean_map cases = - let clean_branch (l, args, expr) = - let rec clean_arg_list args acc subst = +and clean_branch_map lctx cases = + let clean_branch name (l, args, expr) = + let rec clean_arg_list args acc subst lctx = match args with - | (P.Aerasable, _)::tl -> - (* Drop the variable and substitute it in the body. *) - clean_arg_list tl acc (S.cons erasure_dummy subst) - | (kind, var)::tl -> - (* Keep the variable and sink the substitution. *) - clean_arg_list tl (var::acc) (ssink var subst) - | [] -> - (List.rev acc, subst) in - let args, subst = clean_arg_list args [] S.identity in - let subst = (S.cons erasure_dummy subst) in (* Substitute the equality. *) - (l, args, erase_type (L.push_susp expr subst)) in - SMap.map clean_branch cases + | (P.Aerasable, _) :: tl + -> (* Drop the variable and substitute it in the body. *) + clean_arg_list tl acc (S.cons erasure_dummy subst) lctx + | (_, var) :: tl + -> (* Keep the variable and sink the substitution. *) + let lctx' = DB.lctx_extend lctx var Variable erasure_dummy in + clean_arg_list tl (var :: acc) (ssink var subst) lctx' + | [] -> (List.rev acc, subst, lctx) + in + let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in + let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) + (l, eargs, erase_type lctx' (L.push_susp expr subst)) + in + SMap.mapi clean_branch cases (* The following entry points to erasure, `erase_type` and `clean_decls`, check that no metavariables are left before performing the erasure itself. *) -let erase_type lxp = +let erase_type lctx lxp = let _, (mvs, _) = fv lxp in if not (IMap.is_empty mvs) then Log.log_fatal @@ -1198,12 +1222,12 @@ let erase_type lxp = ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) ) mvs) ("Metavariables in erase_type :"); - erase_type lxp + erase_type lctx lxp (* Textually identical to the previous definition of `clean_decls`, but calls the new `erase_type`, which checks for metavars. *) -let clean_decls decls = - List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls +let clean_decls lctx decls = + List.map (fun (v, lxp, _) -> (v, erase_type lctx lxp)) decls (** Turning a set of declarations into an object. **) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f92d48f1415242fcd6eada5bc6ab67e33b... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f92d48f1415242fcd6eada5bc6ab67e33b... You're receiving this email because of your account on gitlab.com.