Simon Génier pushed to branch arity-of-cons at Stefan / Typer
Commits: d453b186 by Simon Génier at 2021-03-09T20:41:06-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.
- - - - -
7 changed files:
- src/REPL.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - + src/listx.ml - src/opslexp.ml
Changes:
===================================== src/REPL.ml ===================================== @@ -105,7 +105,6 @@ let rec read_input i =
(* Interactive mode is not usual typer It makes things easier to test out code *) -type ldecl = vname * lexp * ltype type lexpr = lexp
(* Grouping declaration together will enable us to support mutually recursive @@ -128,10 +127,14 @@ 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 lctx', eldecls = Listx.fold_left_map OL.clean_decls 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 @@ -158,25 +161,25 @@ 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 lxps, ectx' = ilexp_parse pxps ectx in + let elxps = ierase_type (ectx_to_lctx ectx) lxps in let v, rctx = ieval' elxps rctx in - v, ectx, rctx + v, ectx', rctx
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 - (* 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 - * refer to each other (i.e. they can be mutually recursive). - * - hence the overall "list of lists" is a sequence of such - * blocs of mutually-recursive definitions. *) - let rctx = eval_decls_toplevel elxps rctx in - (* This is for consistency with ieval *) - [], 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 = Listx.fold_left_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 + * refer to each other (i.e. they can be mutually recursive). + * - hence the overall "list of lists" is a sequence of such + * blocs of mutually-recursive definitions. *) + let rctx = eval_decls_toplevel elxps rctx in + (* This is for consistency with ieval *) + [], ectx', rctx
let ieval_string = ieval prelex_string let ieval_file = ieval prelex_file
===================================== 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 = Listx.fold_left_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/lexp.ml ===================================== @@ -118,6 +118,8 @@ type ltype = lexp | SLsucc of lexp | SLlub of lexp * lexp
+type ldecl = vname * lexp * ltype + type varbind = | Variable | ForwardRef
===================================== 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,112 @@ 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 = + + let count_unless_erasable i = function + | (Aerasable, _, _) -> i + | _ -> i + 1 + in + + match lexp'_whnf ty lctx with + | Inductive (_, _, _, constructors) + -> (match SMap.find_opt name constructors with + | Some params -> List.fold_left count_unless_erasable 0 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', edecls = clean_decls lctx decls in + E.Let (l, edecls, 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 : DB.lexp_context) + (decls : ldecl list) + : DB.lexp_context * (vname * E.elexp) list = + let lctx' = DB.lctx_extend_rec lctx decls in + (lctx', 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 = +and clean_branch_map lctx cases = let clean_branch (l, args, expr) = - let rec clean_arg_list args acc subst = + 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 + | (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.map 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,13 +1231,17 @@ 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 : DB.lexp_context) + (decls : ldecl list) + : DB.lexp_context * (vname * E.elexp) list =
+ let lctx' = DB.lctx_extend_rec lctx decls in + (lctx', List.map (fun (v, lexp, _) -> (v, erase_type lctx' lexp)) decls)
(** Turning a set of declarations into an object. **)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d453b18629e5371e086697625cc0cc4f6f...
Afficher les réponses par date