Setepenre pushed to branch master at Stefan / Typer

Commits: 9b332512 by Pierre Delaunay at 2016-05-21T09:11:50-04:00 Use Susp to shift when required.

I don't understand why:

sqr = lambda (x : Int) -> x * x; main = sqr 2; % sqr[0] 2; % failed to find sqr[0] found main

is not processed correctly sqr is not shifted by one as it should have been.

Changes to be committed: * src/lparse.ml * src/lexp.ml * src/debruijn.ml

- - - - -

9 changed files:

- .gitignore - GNUmakefile - btl/types.typer - src/debruijn.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml

Changes:

===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -15,7 +15,7 @@ manual.?? *_build/ *~ #*# -test__.ml +test.ml _temp_hack test__.typer *.orig

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -47,6 +47,10 @@ tests-build: tests-run: @./_build/tests/utests --verbose= 3

+test-file: + ocamlbuild src/test.$(COMPILE_MODE) -I src $(OBFLAGS) + @mv _build/src/test.$(COMPILE_MODE) _build/test + # There is nothing here. I use this to test if opam integration works install: tests

@@ -80,3 +84,6 @@ run/tests:

run/typer-file: @./_build/typer ./samples/test__.typer + +run/test-file: + @./_build/test

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -44,78 +44,6 @@ Sexp = Built-in "Sexp"; _+_ = Built-in "_+_" (Int -> Int -> Int); _*_ = Built-in "_*_" (Int -> Int -> Int);

-Bool = inductive_ (Boolean) (True) (False); -True = inductive-cons Bool True; -False = inductive-cons Bool False; - -%Option : Type -> Type; -Option = inductive_ (Option (a : Type)) (None) (Some a); -Some = inductive-cons Option Some; -None = inductive-cons Option None; - -string_eq = Built-in "string_eq" (String -> String -> Bool); -int_eq = Built-in "int_eq" (Int -> Int -> Bool); -sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); - -% ----------------------------------------------------- -% List -% ----------------------------------------------------- - -List : Type -> Type; -List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); - -nil = inductive-cons List nil; -cons = inductive-cons List cons; - -length : (a : Type) => List a -> Int; -length = lambda a => - lambda xs -> - case xs - | nil => 0 - | cons hd tl => (1 + (length a tl)); - -head : (a : Type) => List a -> a; -head = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => hd; - -tail : (a : Type) => List a -> List a; -tail = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => tl; - -% ----------------------------------------------------- -% Macro -% ----------------------------------------------------- - -block_ = Built-in "block_" ((List Sexp) -> Sexp); -symbol_ = Built-in "symbol_" (String -> Sexp); -string_ = Built-in "string_" (String -> Sexp); -node_ = Built-in "node_" (Sexp -> (List Sexp) -> Sexp); -integer_ = Built-in "integer_" (Int -> Sexp); -float_ = Built-in "float_" (Float -> Sexp); - -% Macro : Type; -Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp)); -Macro_ = inductive-cons Macro Macro_ ; - -sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp - -> (Sexp -> List Sexp -> Sexp) - -> (String -> Sexp) - -> (String -> Sexp) - -> (Int -> Sexp) - -> (Float -> Sexp) - -> (List Sexp -> Sexp) - -> Sexp); - - - - -

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -166,18 +166,19 @@ let _env_lookup ctx (v: vref): env_elem = Not_found -> debruijn_error loc "DeBruijn index out of bounds!"

-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 env_lookup_type ctx (v : vref): lexp = + let (_, idx) = v in + let (_, _, _, ltp) = _env_lookup ctx v in + (* unsusp_all *) (Susp (ltp, (S.shift (idx + 1))))

+let env_lookup_expr ctx (v : vref): lexp = + let (_, idx) = v in + let (r, _, lxp, _) = _env_lookup ctx v in

- let (_, _, _, t) = _env_lookup ctx v in t + let lxp = match lxp with + | LetDef lxp -> lxp in

-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 + (* unsusp_all *) (Susp (lxp, (S.shift (idx - r + 1))))

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

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -140,6 +140,20 @@ let rec elexp_location e = | Inductive(l, _) -> l | Type -> U.dummy_location

+ +let elexp_name e = + match e with + | Imm _ -> "Imm" + | Builtin _ -> "Builtin" + | Var _ -> "Var" + | Let _ -> "Let" + | Lambda _ -> "Lambda" + | Call _ -> "Call" + | Cons _ -> "Cons" + | Case _ -> "Case" + | Type -> "Type" + | Inductive _ -> "Inductive" + let rec elexp_print lxp = print_string (elexp_str lxp) and elexp_to_string lxp = elexp_str lxp and elexp_str lxp =

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -84,6 +84,18 @@ let value_location (vtp: value_type) = (* location info was lost or never existed *) | _ -> dloc

+ +let value_name v = + match v with + | Vint _ -> "Vint" + | Vstring _ -> "Vstring" + | Vcons _ -> "Vcons" + | Vbuiltin _ -> "Sbuiltin" + | Vfloat _ -> "Vfloat" + | Closure _ -> "Closure" + | Vsexp _ -> "Vsexp" + | Vdummy -> "Vdummy" + (* Runtime Environ *) type env_cell = (string option * value_type) ref type runtime_env = (env_cell myers) * (int * int)

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -291,10 +291,9 @@ and print_eval_result i lxp =

and print_eval_trace () = - print_trace " EVAL TRACE " 50 elexp_to_string elexp_print !_global_eval_trace + print_trace " EVAL TRACE " 50 elexp_name elexp_print !_global_eval_trace

let eval lxp ctx = - _global_eval_trace := []; _eval lxp ctx 1

let debug_eval lxp ctx =

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -322,7 +322,10 @@ let rec unsusp e s = (* Push a suspension one level down. *) | None -> default | Some e -> Some (mkSusp e s))

- +let unsusp_all e = + match e with + | Susp(e, s) -> unsusp e s + | _ -> e

let lexp_to_string e = match e with @@ -665,6 +668,8 @@ and _lexp_to_str ctx exp = | Float (_, s) -> tval (string_of_float s) | e -> sexp_to_str e)

+ | Susp _ -> _lexp_to_str ctx (unsusp_all exp) + | Var ((loc, name), idx) -> name ^ (index idx) ;

| Let (_, decls, body) -> @@ -711,7 +716,7 @@ and _lexp_to_str ctx exp = | _ -> "__", -1, true, true in

let binop_str op (_, lhs) (_, rhs) = - (lexp_to_str lhs) ^ op ^ (lexp_to_str rhs) in + (lexp_to_str lhs) ^ op ^ (index idx) ^ " " ^ (lexp_to_str rhs) in

let add_parens bl str = if bl then "(" ^ str ^ ")" else str in @@ -722,11 +727,11 @@ and _lexp_to_str ctx exp = * Either use the boring (_+_ e1 e2) notation, or check the * grammar to decide when we can use the infix notation and * when to add parenthese. *) - | ("_=_", [lhs; rhs]) -> binop_str " = " lhs rhs - | ("_+_", [lhs; rhs]) -> binop_str " + " lhs rhs - | ("_-_", [lhs; rhs]) -> binop_str " - " lhs rhs - | ("_/_", [lhs; rhs]) -> binop_str " / " lhs rhs - | ("_*_", [lhs; rhs]) -> binop_str " * " lhs rhs + | ("_=_", [lhs; rhs]) -> binop_str " =" lhs rhs + | ("_+_", [lhs; rhs]) -> binop_str " +" lhs rhs + | ("_-_", [lhs; rhs]) -> binop_str " -" lhs rhs + | ("_/_", [lhs; rhs]) -> binop_str " /" lhs rhs + | ("_*_", [lhs; rhs]) -> binop_str " *" lhs rhs (* not an operator *) | _ -> let args = List.fold_left

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -235,7 +235,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =

(* Get constructor args *) let formal, args = match idt with - | LetDef Inductive(_, _, formal, ctor_def) -> ( + | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> lexp_error loc @@ -388,7 +388,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* consume Arrows and args together *) let rec get_return_type name i ltp args = - match ltp, args with + match (unsusp_all ltp), args with | _, [] -> ltp | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) | _, _ -> lexp_warning loc @@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in - (* let ret_type = get_return_type 0 ltp new_args in *) + let ltp = unsusp_all ltp in

let handle_named_call (loc, name) = (* Process Arguments *) @@ -414,8 +414,8 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in

- match env_lookup_expr ctx ((loc, name), idx) with - | LetDef Builtin((_, "Built-in"), _) ->( + match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + | Builtin((_, "Built-in"), _) ->( (* ------ SPECIAL ------ *) match !_parsing_internals, largs with | true, [Imm(String (_, str))] -> @@ -432,7 +432,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_error loc "Use of "Built-in" in user code"; dlxp, dltype)

- | _ -> + | e -> let ret_type = get_return_type name 0 ltp new_args in Call(vf, new_args), ret_type

@@ -448,9 +448,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc ("Could not find Variable: " ^ name) in

(* Get the macro *) - let lxp = try match env_lookup_expr ctx ((loc, name), idx) with - | LetDef e -> e - | _ -> lexp_fatal loc "The macro cannot be expanded"; + let lxp = try env_lookup_expr ctx ((loc, name), idx) (* with + | 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 @@ -544,8 +544,7 @@ 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 *) - | LetDef Cons _ -> - (name, loc, []), ctx + | Cons _ -> (name, loc, []), ctx

(* name is defined but is not a constructor *) (* it technically could be ... (expr option) *) @@ -664,11 +663,13 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) =

(* 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 + let (l, s, lxp, ltp) = SMap.find key !merged in + let lxp = match lxp with + | Some lxp -> lxp | None -> dltype in - ((l, s), expr, ltp)::acc) [] !names in + let ltp = unsusp_all ltp in + let lxp = unsusp_all lxp in + ((l, s), lxp, ltp)::acc) [] !names in

decls, ctx

@@ -786,31 +787,41 @@ let lexp_parse_all p ctx = _lexp_parse_all p ctx 1 * --------------------------------------------------------- *)

(* Make lxp context with built-in types *) -let default_lctx = - (* Empty context *) +let empty_lctx = let lctx = make_lexp_context in let lxp = Builtin((dloc, "Built-in"), 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 - let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let pxps = pexp_decls_all nods in - - _parsing_internals := true; - let _, lctx = lexp_p_decls pxps lctx in - _parsing_internals := false; - - (* Once default builtin are set we can populate the predef table *) - List.iter (fun name -> - let idx = senv_lookup name lctx in - let v = Var((dloc, name), idx) in (* - let value = (env_lookup_expr lctx v) in *) - set_predef name (Some v)) predef_name; - (* -- DONE -- *) + env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 + +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") (LetDef lxp) type0 in + + (* Read BTL files *) + let pres = prelex_file (!btl_folder ^ "types.typer") in + let sxps = lex default_stt pres in + let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in + let pxps = pexp_decls_all nods in + + _parsing_internals := true; + let _, lctx = lexp_p_decls pxps lctx in + _parsing_internals := false; + + (* Once default builtin are set we can populate the predef table *) + try + List.iter (fun name -> + let idx = senv_lookup name lctx in + let v = Var((dloc, name), idx) in (* + let value = (env_lookup_expr lctx v) in *) + set_predef name (Some v)) predef_name; + (* -- DONE -- *) + lctx + with e -> lctx

+ (* Make runtime context with built-in types *) let default_rctx = try (from_lctx (default_lctx))

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