Setepenre pushed to branch master at Stefan / Typer

Commits: 18d7aa8d by Pierre Delaunay at 2016-05-20T12:58:17-04:00 lexp_p_decls qui ne marche pas

- - - - -

4 changed files:

- samples/quote.typer - src/debruijn.ml - src/eval.ml - src/lparse.ml

Changes:

===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -5,19 +5,41 @@ integer = lambda (y : Int) -> (integer_ y) ; float = lambda (y : Float) -> (float_ y) ; block = lambda (y : List Sexp) -> (block_ y) ;

+quote' : List Sexp -> List Sexp; + + +% +% f = (qquote (uquote x) * x) (node _*_ [(node_ unquote "x") "x"]) +% +% f = node_ "*" cons (x, cons (symbol_ "x") nil)) +% +% +% => x + +% the expression needs to be handled +has-uquote : List Sexp -> Sexp; +has-uquote = lambda y -> + head Sexp y; %node_ (symbol_ "node_") (quote' y); + +% keep quoting the expression +hasnot-uquote : Sexp -> List Sexp -> List Sexp; +hasnot-uquote = lambda op -> + lambda y -> + case y + | nil => node_ op nil + | _ => node_ (quote' (cons op nil)) (quote' y); + + % traverse nodes node : Sexp -> List Sexp -> Sexp; -node = (lambda (op : Sexp) -> - lambda (y : List Sexp) -> - case y - | nil => node_ op nil - | _ => node_ (quote' (cons op nil)) (quote' y)); +node = lambda (op : Sexp) -> + lambda (y : List Sexp) -> + case (sexp_eq op (symbol_ "uquote")) + | True => has-uquote y + | False => hasnot-uquote op y;

- | uquote => node_ (symbol_ "node_") (cons (quote' op) - (cons (reconstruire la liste en sexp) nil))

% tree traversal -quote' : List Sexp -> List Sexp; quote' = lambda (x : List Sexp) -> let target = head Sexp x; tl = tail Sexp x; @@ -36,13 +58,6 @@ quote' = lambda (x : List Sexp) -> quote = Macro_ (lambda (x : List Sexp) -> head Sexp (quote' x));

- -% Should it return -% (node_ (symbol_ "_*_") (cons (symbol_ x) (cons (symbol_ x) nil))) - -% OR -% x * x (Lexp, donc Call(_*_, [x x]) - -%main = quote (x * x); +mn = quote (x * x);

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -126,7 +126,7 @@ let env_add_var_info var (ctx: lexp_context) =

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

let _name_error loc estr str = @@ -167,8 +167,11 @@ let _env_lookup ctx (v: vref): env_elem =

let env_lookup_type ctx (v : vref) = + (* let ((csize, _), _, _) = ctx in *) (* 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 env_lookup_expr ctx (v : vref) = @@ -179,4 +182,74 @@ let env_lookup_expr ctx (v : vref) = let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx))

+(* replace an expression by another *) +(* Most of the time it should be O(1) but it can be O(n) *) +let replace_by ctx name by = + let (a, env, b) = ctx in + let idx = senv_lookup name ctx in + (* lookup and replace *) + let rec replace_by' ctx by acc = + match ctx with + | Mnil -> debruijn_error dummy_location + ("Replace error. This expression does not exist: " ^ name) + | Mcons((_, Some (b, n), _, _) as elem, tl1, i, tl2) -> + if n = name then + (cons by tl1), acc + else + (* Skip some elements if possible *) + if idx < i then replace_by' tl1 by (elem::acc) + else replace_by' tl2 by (elem::acc) + (* replace_by' tl1 by (elem::acc) *) in + + let nenv, decls = replace_by' env by [] in + (* add old declarations *) + let nenv = List.fold_left (fun ctx elem -> cons elem ctx) nenv decls in + (a, nenv, b) + +(* shift an entire expression by n *) +let rec db_shift expr n = + let db_shift lxp = db_shift lxp n in + match expr with + (* Nothing to shift *) + | Imm _ -> expr + | SortLevel _ -> expr + | Sort _ -> expr + | Builtin _ -> expr + + | Var (s, idx) -> Var(s, idx + n) + | Susp(lxp, s) -> Susp(db_shift lxp, s) + | Cons((s, idx), t) -> Cons((s, idx + n), t) + + | Let(l, decls, lxp) -> + let decls = List.map (fun (var, lxp, ltp) -> + var, db_shift lxp, db_shift ltp) decls in + Let(l, decls, db_shift lxp) + + | Arrow(kind, var, ltp, l, lxp) -> + Arrow(kind, var, db_shift ltp, l, db_shift lxp) + + | Lambda(kind, var, ltp, lxp) -> + Lambda(kind, var, db_shift ltp, db_shift lxp) + + | Call(lxp, args) -> + let args = List.map (fun (kind, lxp) -> (kind, db_shift lxp)) args in + Call(db_shift lxp, args) + + | Inductive(l, nm, fargs, ctors) -> + let fargs = List.map (fun (kind, var, ltp) -> (kind, var, db_shift ltp)) + fargs in + let ctors = SMap.map (fun args -> + List.map (fun (kind, var, ltp) -> (kind, var, db_shift ltp)) args) + ctors in + Inductive(l, nm, fargs, ctors) + + | Case(l, tlxp, tltp, retltp, branch, dflt) -> + let dflt = match dflt with + | Some lxp -> Some (db_shift lxp) + | None -> None in + + let branch = SMap.map (fun (l, args, lxp) -> + (l, args, db_shift lxp)) branch in + Case(l, db_shift tlxp, db_shift tltp, db_shift retltp, branch, dflt) +

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -317,7 +317,7 @@ let from_lctx (ctx: lexp_context): runtime_env = let ((n, _), env, _) = ctx in let rctx = ref make_runtime_ctx in

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

(* add all variables *) @@ -336,17 +336,18 @@ let from_lctx (ctx: lexp_context): runtime_env = try let j = diff - i (* - 1 *) in let name, exp = match Myers.nth (csize - i) env with - | (_, Some (_, name), LetDef exp, _) -> name, Some exp - | _ -> "", None in + | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp + | _ -> None, None in

let vxp = match exp with | Some lxp -> let lxp = (erase_type lxp) in (try (eval lxp !rctx) - with e -> elexp_print lxp; raise e) + with e -> elexp_print lxp; + print_string "\n"; raise e)

| None -> Vdummy in - rctx := set_rte_variable j (Some name) vxp (!rctx) + rctx := set_rte_variable j name vxp (!rctx)

with Not_found -> print_int n; print_string " ";

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -66,10 +66,12 @@ let lexp_fatal = msg_fatal "LPARSE" let _global_lexp_ctx = ref make_lexp_context let _global_lexp_trace = ref [] let _parsing_internals = ref false +let _shift_glob = ref 0 let btl_folder = ref "./btl/"

(* This is used to make Type annotation and inferred type having the same index *) (* since inferred type might need to parse a lambda var to infer the type *) + let _type_shift tp i = match tp with | Var(v, idx) -> Var(v, idx) @@ -119,6 +121,9 @@ let build_var name ctx = let get_type0 ctx = build_var "Type" ctx let get_int ctx = build_var "Int" ctx

+(* shift all variables by an offset *) +let senv_lookup name ctx = + senv_lookup name ctx + !_shift_glob

let rec lexp_p_infer (p : pexp) (ctx : lexp_context): lexp * ltype = _lexp_p_infer p ctx 1 @@ -143,7 +148,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =

(* Symbol i.e identifier *) | Pvar (loc, name) ->( - try let idx = senv_lookup name ctx in + try let idx = (senv_lookup name ctx) in let lxp = (make_var name idx loc) in

(* search type *) @@ -376,8 +381,10 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let loc = pexp_location fun_name in

let from_lctx ctx = try (from_lctx ctx) - with e -> - lexp_fatal loc "Could not convert lexp context into rte context" in + with e ->( + lexp_error loc "Could not convert lexp context into rte context"; + print_eval_trace (); + raise e) in

(* consume Arrows and args together *) let rec get_return_type name i ltp args = @@ -624,92 +631,46 @@ and lexp_decls_macro (loc, mname) sargs ctx: pdecl list = (* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 0 and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = - let tctx = ctx in - let forw = SMap.empty in + let names = ref [] in + let offset = ref 0 in let merged = ref SMap.empty in - let acc = ref [] in - let idx = ref 0 in - - let rec process_decl tctx decl1 decl2 = - match decl1, decl2 with - (* identifier : type; - * 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) 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) (LetDef lxp) ltp in - tctx, 2 - - (* Foward declaration *) - | Ptype((l, s), ptp), _ -> - 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) ForwardRef ltp in - tctx, 1 - - (* infer *) - | Pexpr((l, s), pxp), _ ->( - try let value = SMap.find s !merged in - let _ = (match !value with - | (s, l, None, Some ptp) -> - let ltp, _ = lexp_p_infer ptp tctx in - let lxp = lexp_p_check pxp ltp tctx in - value := (s, l, Some pxp, Some ptp); - | (s, l, Some _, _) -> - lexp_warning l "Declaration override are not allowed" - | _ -> typer_unreachable "Empty declaration") in - tctx, 1 - 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) (LetDef lxp) ltp in - tctx, 1) - - | Pmcall(s, sargs), _ -> - let decls = lexp_decls_macro s sargs tctx in - let tctx = foldvar tctx decls in - tctx, 1 - - and foldvar tctx decls = - match decls, decls with - | p1::p2::tl2, _::tl1 -> - let tctx, v = process_decl tctx p1 (Some p2) in - idx := !idx + 1; - if v = 2 then foldvar tctx tl2 else foldvar tctx tl1 - - | p1::[], _ -> - let tctx, v = process_decl tctx p1 None in - idx := !idx + 2; - tctx - | [], _ -> tctx in - - let tctx = foldvar tctx decls in - let merged_decls = List.rev !acc in - let acc, ctx = - List.fold_left (fun (acc, ctx) rf -> - let (s, l, opxp, optp) = ! rf in - match opxp, optp with - | Some pxp, Some ptp -> - 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) (LetDef lxp) ltp) - - | Some pxp, _ -> - let lxp, ltp = lexp_p_infer pxp tctx in - ((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) ForwardRef ltp) - - | _ -> typer_unreachable "No type no expression") ([], ctx) merged_decls in - List.rev acc, ctx

+ let ctx = List.fold_left (fun vctx expr -> + match expr with + | Pexpr ((l, s), pxp) ->( + try let idx = senv_lookup s vctx in + let ltp = env_lookup_type vctx ((l, s), idx) in + let lxp = lexp_p_check pxp ltp vctx in + let (_, _, _, ltp) = SMap.find s !merged in + merged := SMap.add s (l, s, Some lxp, ltp) !merged; + let r = !offset in + offset := 0; + replace_by vctx s (r, Some (l, s), (LetDef lxp), ltp); + + with Not_found -> + let lxp, ltp = lexp_p_infer pxp vctx in + names := s::!names; + merged := SMap.add s (l, s, Some lxp, ltp) !merged; + env_extend vctx (l, s) (LetDef lxp) ltp) + + | Ptype ((l, s), ptp) -> + offset := !offset + 1; + let ltp, _ = lexp_p_infer ptp vctx in + names := s::!names; + merged := SMap.add s (l, s, None, ltp) !merged; + env_extend vctx (l, s) ForwardRef ltp + + | _ -> vctx) ctx decls in + + (* merge type and expr *) + let decls = List.fold_left (fun acc key -> + let (l, s, expr, ltp) = SMap.find key !merged in + let expr = match expr with + | Some expr -> expr + | None -> dltype in + ((l, s), expr, ltp)::acc) [] !names in + + decls, ctx

and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list =

@@ -731,7 +692,8 @@ and print_lexp_ctx (ctx : lexp_context) = (Some ('l', 10), "NAME"); (Some ('l', 7), "INDEX"); (Some ('l', 10), "NAME"); - (Some ('l', 36), "VALUE:TYPE")]; + (Some ('l', 4), "OFF"); + (Some ('l', 32), "VALUE:TYPE")];

print_string (make_sep '-');

@@ -762,14 +724,16 @@ and print_lexp_ctx (ctx : lexp_context) =

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

- try let name, exp, tp = + try let r, 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 + | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp + | _ -> 0, "", None, dltype in

(* Print env Info *) lalign_print_string name 10; (* name must match *) print_string " | "; + lalign_print_int r 4; + print_string " | ";

let _ = (match exp with | None -> print_string "<var>" @@ -851,6 +815,7 @@ let default_lctx = let default_rctx = try (from_lctx (default_lctx)) with e ->( + print_eval_trace (); lexp_error dloc "Could not convert lexp context into rte context"; raise e)

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