Setepenre pushed to branch master at Stefan / Typer

Commits: 25168277 by Pierre Delaunay at 2016-05-19T17:22:01-04:00 lexp_context use varbind

Changes to be committed: * lot of modified files

- - - - -

8 changed files:

- src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml - − tests/debruijn_test.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -36,6 +36,8 @@ open Util open Lexp open Myers open Fmt +(*open Typecheck env_elem and env_type *) + module S = Subst

let debruijn_error l m = msg_error "DEBRUIJN" l m; internal_error m @@ -44,9 +46,10 @@ let debruijn_warning = msg_warning "DEBRUIJN" (* Type definitions * ---------------------------------- *)

-(* Index -> Variable Info *) -type env_elem = (int * (location * string) * lexp option * ltype) -type env_type = (env_elem ref) myers +(* easier to debug with type annotations *) +type env_elem = (int * vdef option * varbind * ltype) +type env_type = env_elem myers +

(* This exist because I don't want that file to depend on anything *) module StringMap @@ -119,11 +122,11 @@ let senv_add_var (loc, name) ctx =

let env_add_var_info var (ctx: lexp_context) = let (a, env, f) = ctx in - (a, cons (ref var) env, f) + (a, cons (var) env, f)

-let env_extend (ctx: lexp_context) (def: vdef) (v: lexp option) (t: lexp) = +let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = let ((n, map), e, f) = ctx in - env_add_var_info (n, def, v, t) (senv_add_var def ctx) + env_add_var_info (n, Some def, v, t) (senv_add_var def ctx)

let _name_error loc estr str = @@ -131,6 +134,7 @@ let _name_error loc estr str = debruijn_error loc ("DeBruijn index refers to wrong name. " ^ "Expected: "" ^ estr ^ "" got "" ^ str ^ """)

+(* let env_set_var_info ctx (def: vref) (v: lexp option) (t: lexp) = let ((dv_size, _), info_env, _) = ctx in let ((loc, ename), dbi) = def in @@ -143,18 +147,19 @@ let env_set_var_info ctx (def: vref) (v: lexp option) (t: lexp) =

rf := (0, (loc, ename), v, t)) with - Not_found -> debruijn_error loc "DeBruijn index out of bounds!" + Not_found -> debruijn_error loc "DeBruijn index out of bounds!" *)

(* generic lookup *) let _env_lookup ctx (v: vref): env_elem = let ((dv_size, _), info_env, _) = ctx in let ((loc, ename), dbi) = v in

- try(let ret = !(Myers.nth dbi info_env) in - let (_, (_, name), _, _) = ret in - - (* Check if names match *) - _name_error loc ename name; + try(let ret = (Myers.nth dbi info_env) in + let _ = match ret with + | (_, Some (_, name), _, _) -> + (* Check if names match *) + _name_error loc ename name; + | _ -> () in

ret) with @@ -164,14 +169,14 @@ let _env_lookup ctx (v: vref): env_elem = let env_lookup_type ctx (v : vref) = (* FIXME: We need to S.shift here, since `t` is valid in the context in * which `vref` appeared, rather than in `ctx`. *) - let (_, (_, _), _, t) = _env_lookup ctx v in t + let (_, _, _, t) = _env_lookup ctx v in t

let env_lookup_expr ctx (v : vref) = (* FIXME: We need S.shift here, since `lxp` is valid in the context in * which `vref` appeared (plus recursion offset), rather than in `ctx`. *) - let (_, (_, _), lxp, _) = _env_lookup ctx v in lxp + let (_, _, lxp, _) = _env_lookup ctx v in lxp

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

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -287,7 +287,9 @@ let main () =

(* convert a lctx context into a typecheck context *) (* they will be the same in the future *) - let lctx_to_cctx (lctx: lexp_context): TC.tc_ctx = + let lctx_to_cctx (lctx: lexp_context) = + let (_, env, _) = ctx in env in + (* let (_, env, _) = lctx in let n = Myers.length env in

@@ -299,7 +301,7 @@ let main () = | None -> TC.ForwardRef in let cctx = Myers.cons (i, Some v, vlxp, ltp) cctx in loop (i - 1) env cctx) in - loop n env Myers.nil in + loop n env Myers.nil in *)

(if (get_p_option "typecheck") then( let cctx = lctx_to_cctx ctx in

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -139,6 +139,7 @@ let rec elexp_location e = | Case (l,_,_,_) -> l | Inductive(l, _) -> l | Type -> U.dummy_location + let rec elexp_print lxp = print_string (elexp_str lxp) and elexp_to_string lxp = elexp_str lxp and elexp_str lxp =

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -35,7 +35,7 @@ open Fmt

open Sexp open Pexp (* Arg_kind *) -(* open Lexp *) +open Lexp (* Varbind *)

open Elexp open Builtin @@ -314,24 +314,30 @@ let eval_all lxps rctx silent =

(* build a rctx from a lctx *) let from_lctx (ctx: lexp_context): runtime_env = - let ((_, _), env, _) = ctx in + let ((n, _), env, _) = ctx in let rctx = ref make_runtime_ctx in

- let bsize = 1 in (*skip the first Built-in function (useless) *) - let csize = get_size ctx in + let bsize = 0 in (*skip the first Built-in function (useless) *) + let csize = n - 1 in

(* add all variables *) for i = bsize to csize do - let (_, (_, name), _, _) = !(Myers.nth (csize - i) env) in - rctx := add_rte_variable (Some name) Vdummy (!rctx) + let name = match (Myers.nth (csize - i) env) with + | (_, Some (_, name), _, _) -> Some name + | _ -> None in + + rctx := add_rte_variable name Vdummy (!rctx) done;

let diff = csize - bsize in

(* process all of them *) for i = 0 to diff do + try let j = diff - i (* - 1 *) in - let (_, (_, name), exp, _) = !(Myers.nth j env) in + let name, exp = match Myers.nth (csize - i) env with + | (_, Some (_, name), LetDef exp, _) -> name, Some exp + | _ -> "", None in

let vxp = match exp with | Some lxp -> @@ -340,7 +346,11 @@ let from_lctx (ctx: lexp_context): runtime_env = with e -> elexp_print lxp; raise e)

| None -> Vdummy in - rctx := set_rte_variable j (Some name) vxp (!rctx) + + with Not_found -> + print_int n; print_string " "; + print_int (csize - i); print_string "\n "; + raise Not_found done; !rctx

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -97,6 +97,11 @@ type ltype = lexp | SLsucc of lexp

+type varbind = + | Variable + | ForwardRef + | LetDef of lexp + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -166,7 +166,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let ltp, _ = lexp_infer tp ctx in let nctx, sh = match ovar with | None -> ctx, 0 - | Some var -> (env_extend ctx var None ltp), 1 in + | Some var -> (env_extend ctx var Variable ltp), 1 in

let lxp, _ = lexp_infer expr nctx in let lxp = _type_shift lxp sh in @@ -184,7 +184,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Some pxp -> _lexp_p_infer pxp !nctx (i + 1) | None -> dltype, dltype in

- nctx := env_extend !nctx var None ltp; + nctx := env_extend !nctx var Variable ltp; (kind, var, ltp) ) formal_args in

@@ -204,7 +204,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | None -> lexp_error tloc "Lambda require type annotation"; dltype, dltype in

- let nctx = env_extend ctx var None ltp in + let nctx = env_extend ctx var Variable ltp in let lbody, lbtp = lexp_infer body nctx in (* We added one variable in the ctx * ) let lbtp = _type_shift lbtp 1 in *) @@ -230,7 +230,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =

(* Get constructor args *) let formal, args = match idt with - | Some Inductive(_, _, formal, ctor_def) -> ( + | LetDef Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> lexp_error loc @@ -282,7 +282,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in

- let nctx = env_extend ctx var None ltp in + let nctx = env_extend ctx var Variable ltp in let lbody = _lexp_p_check body lbtp nctx (i + 1) in

Lambda(kind, var, ltp, lbody)) @@ -408,7 +408,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let vf = (make_var name idx loc) in

match env_lookup_expr ctx ((loc, name), idx) with - | Some Builtin((_, "Built-in"), _) ->( + | LetDef Builtin((_, "Built-in"), _) ->( (* ------ SPECIAL ------ *) match !_parsing_internals, largs with | true, [Imm(String (_, str))] -> @@ -442,11 +442,11 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* Get the macro *) let lxp = try match env_lookup_expr ctx ((loc, name), idx) with - | None -> lexp_fatal loc "The macro cannot be expanded"; - | Some e -> e - with Not_found -> - lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ - " is not a correct index.") in + | LetDef e -> e + | _ -> lexp_fatal loc "The macro cannot be expanded"; + with Not_found -> + lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ + " is not a correct index.") in

let lxp = match lxp with | Call(Var((_, "Macro_"), _), [(Aexplicit, fct)]) -> fct @@ -537,19 +537,19 @@ and lexp_read_pattern pattern exp target ctx: let idx = senv_lookup name ctx in match (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) - | Some Cons _ -> + | LetDef Cons _ -> (name, loc, []), ctx

(* name is defined but is not a constructor *) (* it technically could be ... (expr option) *) (* What about Var -> Cons ? *) - | _ -> let nctx = env_extend ctx var (Some target) dltype in + | _ -> let nctx = env_extend ctx var (LetDef target) dltype in (name, loc, []), nctx)

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

| Ppatcons (ctor_name, args) -> @@ -573,7 +573,7 @@ and lexp_read_pattern_args args ctx: | Ppatany (loc) -> loop tl ((Aexplicit, None)::acc) ctx | Ppatvar ((loc, name) as var) -> (* Add var *) - let nctx = env_extend ctx var None dltype in + let nctx = env_extend ctx var Variable dltype in let nacc = (Aexplicit, Some var)::acc in loop tl nacc nctx | _ -> lexp_error dloc "Constructor inside a Constructor"; @@ -597,7 +597,7 @@ and lexp_parse_inductive ctors ctx i = match var with | None -> loop tl ((kind, None, lxp)::acc) ctx | Some (var) -> - let nctx = env_extend ctx var None dltype in + let nctx = env_extend ctx var Variable dltype in loop tl ((kind, Some var, lxp)::acc) nctx end in loop args [] ctx in @@ -636,10 +636,10 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = * identifier : expr; *) | Ptype((l, s1), ptp), Some Pexpr((_, s2), pxp) when s1 = s2 -> let ltp, _ = lexp_p_infer ptp tctx in - let octx = env_extend tctx (l, s1) None ltp in + let octx = env_extend tctx (l, s1) ForwardRef ltp in let lxp = lexp_p_check pxp ltp octx in acc := (ref (s1, l, Some pxp, Some ptp))::!acc; - let tctx = env_extend tctx (l, s1) (Some lxp) ltp in + let tctx = env_extend tctx (l, s1) (LetDef lxp) ltp in tctx, 2

(* Foward declaration *) @@ -647,7 +647,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = let ltp, _ = lexp_p_infer ptp tctx in acc := (ref (s, l, None, Some ptp))::!acc; merged := SMap.add s (List.hd !acc) !merged; - let tctx = env_extend tctx (l, s) None ltp in + let tctx = env_extend tctx (l, s) ForwardRef ltp in tctx, 1

(* infer *) @@ -665,7 +665,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = with Not_found -> let lxp, ltp = lexp_p_infer pxp tctx in acc := (ref (s, l, Some pxp, None))::!acc; - let tctx = env_extend tctx (l, s) (Some lxp) ltp in + let tctx = env_extend tctx (l, s) (LetDef lxp) ltp in tctx, 1)

| Pmcall(s, sargs), _ -> @@ -696,16 +696,16 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = let ltp, _ = lexp_p_infer ptp tctx in let lxp = lexp_p_check pxp ltp tctx in let acc = ((l, s), lxp, ltp)::acc in - acc, (env_extend ctx (l, s) (Some lxp) ltp) + acc, (env_extend ctx (l, s) (LetDef lxp) ltp)

| Some pxp, _ -> let lxp, ltp = lexp_p_infer pxp tctx in - ((l, s), lxp, ltp)::acc, (env_extend ctx (l, s) (Some lxp) ltp) + ((l, s), lxp, ltp)::acc, (env_extend ctx (l, s) (LetDef lxp) ltp)

| None, Some ptp -> lexp_warning l "Unused variable"; let ltp, _ = lexp_p_infer ptp tctx in - ((l, s), dlxp, ltp)::acc, (env_extend ctx (l, s) None ltp) + ((l, s), dlxp, ltp)::acc, (env_extend ctx (l, s) ForwardRef ltp)

| _ -> typer_unreachable "No type no expression") ([], ctx) merged_decls in List.rev acc, ctx @@ -722,7 +722,7 @@ and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = (loop p ctx [])

(* Print context *) -and print_lexp_ctx ctx = +and print_lexp_ctx (ctx : lexp_context) = let ((n, map), env, f) = ctx in

print_string (make_title " LEXP CONTEXT "); @@ -737,11 +737,13 @@ and print_lexp_ctx ctx =

(* it is annoying to print according to StringMap order *) (* let's use myers list order *) - let rec extract_names lst acc = + let rec extract_names (lst: env_type) acc = match lst with | Mnil-> acc | Mcons (hd, tl, _, _) -> - let (_, (_, name), _, _) = !hd in + let name = match hd with + | (_, Some (_, name), _, _) -> name + | _ -> "" in extract_names tl (name::acc) in

let ord = extract_names env [] in @@ -760,7 +762,10 @@ and print_lexp_ctx ctx =

let ptr_str = "" in (*" | | | | " in *)

- try let (_, (_, name), exp, tp) = env_lookup_by_index (n - idx - 1) ctx in + try let name, exp, tp = + match env_lookup_by_index (n - idx - 1) ctx with + | (_, Some (_, name), LetDef exp, tp) -> name, Some exp, tp + | _ -> "", None, dltype in

(* Print env Info *) lalign_print_string name 10; (* name must match *) @@ -813,12 +818,6 @@ and lexp_print_var_info ctx = let lexp_parse_all p ctx = _lexp_parse_all p ctx 1

-(* add dummy definition helper *) -let add_def name ctx = - let var = (dloc, name) in - let ctx = senv_add_var var ctx in - env_add_var_info (0, var, None, dlxp) ctx - (* Default context with builtin types * --------------------------------------------------------- *)

@@ -827,7 +826,7 @@ let default_lctx = (* Empty context *) let lctx = make_lexp_context in let lxp = Builtin((dloc, "Built-in"), type0) in - let lctx = env_extend lctx (dloc, "Built-in") (Some lxp) type0 in + let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in

(* Read BTL files *) let pres = prelex_file (!btl_folder ^ "types.typer") in @@ -851,8 +850,9 @@ let default_lctx = (* Make runtime context with built-in types *) let default_rctx = try (from_lctx (default_lctx)) - with e -> - lexp_fatal dloc "Could not convert lexp context into rte context" + with e ->( + lexp_error dloc "Could not convert lexp context into rte context"; + raise e)

(* String Parsing

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -101,14 +101,6 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2

(********* Testing if a lexp is properly typed *********)

-type varbind = - | Variable - | ForwardRef - | LetDef of lexp - -(* easier to debug with type annotations *) -type tc_elem = int * vdef option * varbind * lexp -type tc_ctx = tc_elem Myers.myers

let lookup_type ctx vref = let (_, i) = vref in

===================================== tests/debruijn_test.ml deleted ===================================== --- a/tests/debruijn_test.ml +++ /dev/null @@ -1,79 +0,0 @@ -(* - * Typer Compiler - * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. - * - * Author: Pierre Delaunay pierre.delaunay@hec.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/. - * - * --------------------------------------------------------------------------- *) - -open Util -open Utest_lib - -open Sexp -open Lexp -open Lparse - -open Builtin -open Debruijn - - -let lctx = default_lctx - -let make_val value = Imm(String(dloc, value)) - - -let _ = (add_test "DEBRUIJN" "Set Variables" (fun () -> - - if 10 <= (!_global_verbose_lvl) then ( - - let var = [ - ("za", Some type_float, type_int, Some type_int, type_float); - ("zb", Some type_float, type_int, Some type_int, type_float); - ("zc", Some type_float, type_int, Some type_int, type_float); - ("zd", Some type_float, type_int, Some type_int, type_float); - ] in - - let n = (List.length var) - 1 in - - let lctx = List.fold_left (fun ctx (n, l, t, _, _) -> - env_extend ctx (dloc, n) l t) lctx var in - - print_lexp_ctx lctx; - - let _, _ = List.fold_left (fun (ctx, idx) (n, _, _, l, t) -> - let _ = (env_set_var_info ctx ((dloc, n), idx) l t) in - (ctx, idx - 1)) - (lctx, n) var in - - print_lexp_ctx lctx; - - success () - ) - else - success () - -)) - - - -(* run all tests *) -let _ = run_all ()

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