Stefan pushed to branch master at Stefan / Typer

Commits: bc4698bc by Stefan Monnier at 2016-03-24T22:22:01-04:00 Fix lexp's Induction to name fields. Fix lexp_context for real vars.

* src/debruijn.ml (db_idx, db_ridx): Re-introduce those type aliases. (senv_add_var): Remove redundancy. Change calling convention. (lexp_context): Make var's "value" optional. (env_extend): New function.

* src/eval.ml (nfirst_rte_var._eval.ctor_name): Fix confusion in constructor args.

* src/lexp.ml (lexp): Add optional name to constructor fields.

* src/lparse.ml (default_lctx): Adjust to new senv_add_var. (lexp_parse): Consolidate the two Plambda cases. Don't mess with local_scope here. (lexp_parse_inductive): Rename from lexp_parse_constructors. Adapt to lexp changes. Use List.fold_left. (lexp_decls): Adjust to new senv_add_var. (lexp_context_print): Handle vars without value.

- - - - -

5 changed files:

- src/debruijn.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - tests/debug.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -44,45 +44,49 @@ let debruijn_warning = msg_warning "DEBRUIJN" * ---------------------------------- *)

(* Index -> Variable Info *) -type env_elem = (int * (location * string) * lexp * ltype) +type env_elem = (int * (location * string) * lexp option * ltype) type env_type = env_elem myers

(* This exist because I don't want that file to depend on anything *) module StringMap = Map.Make (struct type t = string let compare = String.compare end) -;; + +type db_idx = int (* DeBruijn index. *) +type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *)

(* Map matching variable name and its distance in the current scope *) -type scope = (int) StringMap.t (* Map<String, int>*) +type scope = db_ridx StringMap.t (* Map<String, db_ridx>*)

type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope

- (* name -> index * index -> info * (outer_size, r_offset) *) +(* FIXME: What is this "outer_size" and "r_offset"? *) +(* name -> index * index -> info * (outer_size, r_offset) *) type lexp_context = senv_type * env_type * (int * int)

(* internal definitions * ---------------------------------- *)

-let _make_scope = StringMap.empty;; -let _make_senv_type = (0, _make_scope);; +let _make_scope = StringMap.empty +let _make_senv_type = (0, _make_scope) let _make_myers = nil -let _get_env(ctx: lexp_context): env_type = let (_, ev, _) = ctx in ev ;; +let _get_env(ctx: lexp_context): env_type = let (_, ev, _) = ctx in ev

(* Public methods: DO USE * ---------------------------------- *)

-let make_lexp_context = (_make_senv_type, _make_myers, (0, 0));; +let make_lexp_context = (_make_senv_type, _make_myers, (0, 0)) + +let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof

-let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof;; +(* FIXME: I have no idea what is a "scope" here! *)

(* Enter a local scope such as let *) let local_scope ctx pos = let ((l, map), b, c) = ctx in (* Check size *) - let n = (length b) in - ((l, map), b, (l, pos)) -;; + (* let n = (length b) in *) + ((l, map), b, (l, pos))

(* Enter a temporary scope such as Calls *) let temp_scope ctx bound = let (a, b, c) = ctx in (a, b, bound) @@ -95,29 +99,24 @@ let rec senv_lookup (name: string) (ctx: lexp_context): int = raw_idx - rof (* Shift if the variable is not bound *) else *) raw_idx -;;

(* We first add variable into our map. Later on, we will add them into * the environment. The reason for this is that the type info is * known after lexp parsing which need the index fist *) -let senv_add_var name loc ctx = +let senv_add_var (loc, name) ctx = let ((n, map), e, f) = ctx in - try - let _ = senv_lookup name ctx in - debruijn_warning loc ("Variable Shadowing " ^ name); - let nmap = StringMap.add name n map in - ((n + 1, nmap), e, f) - with - Not_found -> - let nmap = StringMap.add name n map in - ((n + 1, nmap), e, f) -;; + (try let _ = senv_lookup name ctx in + debruijn_warning loc ("Variable Shadowing " ^ name) + with Not_found -> ()); + let nmap = StringMap.add name n map in + ((n + 1, nmap), e, f)

-(* *) let env_add_var_info var (ctx: lexp_context) = let (a, env, f) = ctx in (a, cons var env, f) -;; + +let env_extend (ctx:lexp_context) (def:vdef) (v: lexp option) (t:lexp) = + env_add_var_info (0, def, v, t) (senv_add_var def ctx)

let env_lookup_type_by_index index ctx = try @@ -125,7 +124,6 @@ let env_lookup_type_by_index index ctx = Shift (index - roffset, t) with Not_found -> internal_error "DeBruijn index out of bounds!" -;;

let env_lookup_type ctx (v : vref) = let ((_, rname), dbi) = v in @@ -138,5 +136,3 @@ let env_lookup_type ctx (v : vref) =

let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index (_get_env ctx) -;; -

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -252,7 +252,7 @@ let rec _eval lxp ctx i: (value_type) = (* I am thinking about building a 'get_free_variable' to be able to *) (* handle partial application i.e build a new lambda if Partial App *) | Lambda(_, vr, _, body) -> begin - let (loc, name) = vr in + (* let (loc, name) = vr in *)

(* This was redundant since we already pushed args * when processing the call expression *) @@ -304,8 +304,9 @@ let rec _eval lxp ctx i: (value_type) = | Inductive(_, _, _, c) -> c | _ -> eval_error loc "Not an Inductive Type" in

- try let args = SMap.find cname ctor_def in - cname, args + try match SMap.find cname ctor_def with + | [] -> cname, [] + | _ -> eval_error loc "Constructor not applied" with Not_found -> eval_error loc "Constructor does not exist" end

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -71,7 +71,7 @@ type ltype = lexp | Lambda of arg_kind * vdef * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of location * label * ((arg_kind * vdef * ltype) list) - * ((arg_kind * ltype) list) SMap.t + * ((arg_kind * vdef option * ltype) list) SMap.t | Cons of vref * symbol (* = Type info * ctor_name*) | Case of location * lexp * ltype (* The base inductive type over which we switch. *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -84,11 +84,13 @@ let default_lctx = let lctx = make_lexp_context in

(* populate ctx *) - List.fold_left (fun ctx (name, lxp) -> - let ctx = senv_add_var name dloc ctx in - env_add_var_info (0, (dloc, name), lxp, lxp) ctx) - lctx - lexp_builtins + List.fold_left + (fun ctx (name, lxp) -> + let var = (dloc, name) in + let ctx = senv_add_var var ctx in + env_add_var_info (0, var, None, lxp) ctx) + lctx + lexp_builtins ;;

@@ -144,43 +146,26 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = let lxp = lexp_parse expr ctx in Arrow(kind, None, ltyp, tloc, lxp)

- (* *) - | Plambda (kind, var, Some ptype, body) -> - (* Add argument to context *) - let (loc, vname) = var in - let ltp = lexp_parse ptype ctx in (* Get Type *) - - let nctx = senv_add_var vname loc ctx in - let nctx = env_add_var_info (0, (loc, vname), dlxp, ltp) nctx in - - let ltyp = lexp_parse ptype nctx in - - let nctx = (local_scope nctx (get_roffset nctx)) in - let lbody = lexp_parse body nctx in - Lambda(kind, var, ltyp, lbody) - - | Plambda (kind, var, None, body) -> - let (loc, vname) = var in - - let nctx = senv_add_var vname loc ctx in - let nctx = env_add_var_info (0, (loc, vname), dlxp, dltype) nctx in - - let nctx = (local_scope nctx (get_roffset nctx)) in - let lbody = lexp_parse body nctx in - Lambda(kind, var, UnknownType(tloc), lbody) + | Plambda (kind, var, pt, body) -> + let nctx = senv_add_var var ctx in + let ltp = match pt with + | None -> dltype + | Some pt -> lexp_parse pt ctx in + let nctx = env_add_var_info (0, var, None, ltp) nctx in + let lbody = lexp_parse body nctx in + Lambda(kind, var, ltp, lbody)

| Pcall (fname, _args) -> lexp_call fname _args ctx

(* Pinductive *) | Pinductive (label, [], ctors) -> - let map_ctor, nctx = lexp_parse_constructors ctors ctx in - Inductive(tloc, label, [], map_ctor) + let map_ctor = lexp_parse_inductive ctors ctx in + Inductive(tloc, label, [], map_ctor)

(* Pcons *) | Pcons(vr, sym) -> ( let (loc, type_name) = vr in - let (_, ctor_name) = 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 *) @@ -269,18 +254,18 @@ and lexp_read_pattern pattern exp target ctx: | Ppatany (loc) -> (* Catch all expression nothing to do *) ("_", loc, []), ctx

- | Ppatvar (loc, name) ->( + | Ppatvar ((loc, name) as var) ->( (* FIXME better check *) try - let idx = senv_lookup name ctx in + let _ = senv_lookup name ctx in (* constructor with no args *) (name, loc, []), ctx

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

| Ppatcons (ctor_name, args) -> @@ -302,46 +287,41 @@ and lexp_read_pattern_args args ctx: match pat with (* Nothing to do *) | Ppatany (loc) -> loop tl (None::acc) ctx - | Ppatvar (loc, name) -> + | Ppatvar ((loc, name) as var) -> (* Add var *) - let nctx = senv_add_var name loc ctx in - let nctx = env_add_var_info (0, (loc, name), dlxp, dltype) nctx in - let nacc = (Some (Aexplicit, (loc, name)))::acc in + let nctx = senv_add_var var ctx in + let nctx = env_add_var_info (0, var, None, dltype) nctx in + let nacc = (Some (Aexplicit, var))::acc in loop tl nacc nctx | _ -> lexp_error dloc "Constructor inside a Constructor"; loop tl (None::acc) ctx)

in loop args [] ctx

-(* Parse inductive constructor *) -and lexp_parse_constructors ctors ctx = +(* Parse inductive type definition. *) +and lexp_parse_inductive ctors ctx =

- let make_args (args:(arg_kind * pvar option * pexp) list): - (arg_kind * ltype) list * lexp_context = + let make_args (args:(arg_kind * pvar option * pexp) list) ctx + : (arg_kind * vdef option * ltype) list = let rec loop args acc ctx = match args with - | [] -> (List.rev acc), ctx + | [] -> (List.rev acc) | hd::tl -> begin match hd with - (* What does the optional Pvar do ? - that expression does not exist in LEXP*) - | (kind, _, exp) -> - let lxp = lexp_parse exp ctx in - loop tl ((kind, lxp)::acc) ctx end in + | (kind, var, exp) -> + let lxp = lexp_parse exp ctx in + match var with + | None -> loop tl ((kind, None, lxp)::acc) ctx + | Some (var) -> + let nctx = env_extend ctx var None dltype in + loop tl ((kind, Some var, lxp)::acc) nctx + end in loop args [] ctx in

- let rec loop ctors merged ctx = - match ctors with - | [] -> merged, ctx - | hd::tl -> begin - match hd with - | ((loc, name), args) -> - let largs, nctx = make_args args in - let nmerged = SMap.add name largs merged in - loop tl nmerged ctx - end in - - loop ctors SMap.empty ctx + List.fold_left + (fun lctors ((_, name), args) -> + SMap.add name (make_args args ctx) lctors) + SMap.empty ctors

(* Parse let declaration *) and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = @@ -396,7 +376,7 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let nctx = List.fold_left (fun ctx hd -> match hd with | (_, None, _) -> ctx (* Unused variable: No Instruction *) - | ((loc, name), _, _) -> senv_add_var name loc ctx) + | (var, _, _) -> senv_add_var var ctx) ctx decls in

let n = (List.length decls) - 1 in @@ -411,7 +391,8 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let nctx = local_scope _ctx m in let lxp, ltp = lexp_p_infer pinst nctx in let nacc = ((loc, name), lxp, ltp)::acc in - let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) nctx in + let ctx2 = env_add_var_info (0, (loc, name), + Some lxp, ltp) nctx in process_var_info tl ctx2 nacc (m - 1))

| ((loc, name), Some pinst, Some ptype) ->( @@ -419,7 +400,8 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let linst = lexp_parse pinst nctx in let ltyp = lexp_parse ptype nctx in let nacc = ((loc, name), linst, ltyp)::acc in - let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) nctx in + let ctx3 = env_add_var_info (0, (loc, name), + Some linst, ltyp) nctx in process_var_info tl ctx3 nacc (m - 1))

(* Skip the variable *) @@ -660,7 +642,7 @@ and lexp_print_adv opt exp = and lexp_print_ctors opt ctors = SMap.iter (fun key value -> print_string ("(" ^ key ^ ": "); - List.iter (fun (kind, arg) -> + List.iter (fun (kind, _, arg) -> lexp_print_adv opt arg; print_string " ") value; print_string ")") ctors @@ -706,7 +688,9 @@ and lexp_context_print ctx = try let (_, (_, name), exp, tp) = env_lookup_by_index (n - idx - 1) ctx in ralign_print_string name 10; (* name must match *) print_string " | "; - lexp_print_adv (false, 0, true) exp; + (match exp with + | None -> print_string "<var>" + | Some exp -> lexp_print_adv (false, 0, true) exp); print_string ": "; lexp_print_adv (false, 0, true) tp; print_string "\n" @@ -738,8 +722,9 @@ let lexp_print e = lexp_print_adv (false, 0, true) e;;

(* add dummy definition helper *) let add_def name ctx = - let ctx = senv_add_var name dloc ctx in - env_add_var_info (0, (dloc, name), dlxp, dlxp) ctx + let var = (dloc, name) in + let ctx = senv_add_var var ctx in + env_add_var_info (0, var, None, dlxp) ctx ;;

===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -159,7 +159,6 @@ let debug_pexp_print_all pexps = (* Print lexp with debug info *) let debug_lexp_print tlxp = print_string " "; - let dloc = dummy_location in let print_info msg loc lex = print_string msg; print_string "["; print_loc loc;

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