Skip to content
Commits on Source (2)
......@@ -53,4 +53,10 @@ Read tests/full_debug.ml for ocaml usage
Function:
sexp_parse sexp
* Sexp -> Lexp
\ No newline at end of file
* Sexp -> Lexp
Replace variable name by their (reverse) index in the environment.
......@@ -8,7 +8,7 @@ let c = 1; a = 5; b = 10; d = 3; in
% -------------------------------------------
% define sqrt
sqrt x = lambda (x : Nat) -> x * x;
sqrt = lambda (x : Nat) -> x * x;
% define cube
cube = lambda (x : Nat) -> x * (sqrt x);
......
......@@ -35,6 +35,7 @@
open Util
open Lexp
open Myers
open Fmt
let debruijn_error = msg_error "DEBRUIJN"
let debruijn_warning = msg_warning "DEBRUIJN"
......@@ -54,172 +55,93 @@ module StringMap
(* Map matching variable name and its distance in the current scope *)
type scope = (int) StringMap.t (* Map<String, int>*)
(* Offset is the number to take us out of the inner scope
* Scope is the Mapping between Variable's names and its current index loc
* Offset + Scope *)
type senv_type = int * scope
(* The recursive type that does everything
* inner Scope * Outer Scope *)
type lexp_context = senv_type * lexp_context option * env_type
type senv_length = int (* it is not the map true length *)
type senv_type = senv_length * scope
(* name -> index * index -> info *)
type lexp_context = senv_type * env_type
(* internal definitions: DO NOT USE
* ---------------------------------- *)
let _make_scope = StringMap.empty;;
let _make_context_impl = (0, _make_scope);;
let _make_senv_type = (0, _make_scope);;
let _make_myers = nil
let _get_inner_ctx (ctx: lexp_context) =
let (ct, _, _) = ctx in ct
;;
let _get_inner_scope (ctx: lexp_context): scope =
let ((_, scope), _, _) = ctx in scope
;;
let _get_environ (ctx: lexp_context) =
let (_, _, env) = ctx in env
;;
(* get current offset *)
let _get_offset (ctx: lexp_context): int =
let ((offset, _), _, _) = ctx in offset
let _get_senv (ctx: lexp_context) =
let (ct, _) = ctx in ct
;;
(* increase the offset *)
let _inc_offset (ctx: lexp_context): lexp_context =
(* Because using ref is hell, we make a copy *)
match ctx with
| ((offset, scope), None, e) -> ((offset + 1, scope), None, e)
| ((offset, scope), Some outter, e) ->
((offset + 1, scope), Some outter, e)
let _get_scope(ctx: lexp_context): scope =
let ((_, ev), _) = ctx in ev
;;
(* Increase the indexes of all inner variables *)
let _inc_index (ctx: lexp_context): lexp_context =
let ((offset, scope), otr, env) = ctx in
let scope = StringMap.map (fun value -> value + 1) scope in
((offset, scope), otr, env)
let _get_env(ctx: lexp_context): env_type =
let (_, ev) = ctx in ev
;;
let _add_var_environ variable ctx =
let (a, b, env) = ctx in cons variable env
let _add_var_env variable ctx =
let (a, env) = ctx in cons variable env
;;
(* Public methods: DO USE
* ---------------------------------- *)
(* return its current DeBruijn index
* return -1 if the variable does not exist
* return closest variable *)
let make_lexp_context = (_make_senv_type, _make_myers);;
(* return its current DeBruijn index *)
let rec senv_lookup (name: string) (ctx: lexp_context) =
(* Search *)
let local_index = find_local name ctx in
if local_index >= 0 then
local_index
else
begin
let outter_index = _find_outer name ctx in
if outter_index >= 0 then
outter_index + (_get_offset ctx)
else
-1
end
and find_local (name: string) (ctx: lexp_context): int =
try
let inner = _get_inner_scope ctx in
StringMap.find name inner
with
Not_found -> -1
(* You should not use this function 'find_var' is the way
* the reason is _find_outer does not send back a correct index *)
and _find_outer (name: string) (ctx: lexp_context): int =
match ctx with
| (_, Some ct, _) -> (senv_lookup name ct)
| _ -> -1
let ((n, map), _) = ctx in
n - (StringMap.find name map) - 1
;;
(* We first add variable into our map later on we will add them into
(* 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 (name, loc, exp, type_info) = var in *)
(* I think this should be illegal *)
let local_index = find_local name ctx in
if local_index >= 0 then (* This is the index not the number of element *)
debruijn_warning loc ("Variable Redefinition: " ^ name);
let outer_index = _find_outer name ctx in
if outer_index >= 0 then
debruijn_warning loc ("Variable Shadowing: " ^ name);
(* Increase distance *)
let scope = StringMap.map (fun value -> value + 1) (_get_inner_scope ctx) in
(* Add new Value to the map *)
let new_scope = StringMap.add name 0 scope in
(* build new context *)
match ctx with
| ((offset, _), None, e)
-> ((offset + 1, new_scope), None, e)
| ((offset, _), Some outter, e)
-> ((offset + 1, new_scope), Some outter, e)
let ((n, map), e) = ctx in
try
let idx = senv_lookup name ctx in
debruijn_warning loc ("Variable Shadowing " ^ name);
let nmap = StringMap.add name n map in
((n + 1, nmap), e)
with
Not_found ->
let nmap = StringMap.add name n map in
((n + 1, nmap), e)
;;
(* *)
let env_add_var_info var ctx =
let (rof, (loc, name), value, ltyp) = var in
let nenv = _add_var_environ (rof, (loc, name), value, ltyp) ctx in
let (a, b, env) = ctx in
(a, b, nenv)
let env_add_var_info var (ctx: lexp_context) =
let (a, _) = ctx in
(* let (rof, (loc, name), value, ltyp) = var in *)
let nenv = _add_var_env var ctx in
(a, nenv)
;;
let env_lookup_type_by_index index ctx =
try
let (roffset, (_, name), _, t) = Myers.nth index (_get_environ ctx) in
let (roffset, (_, name), _, t) = Myers.nth index (_get_env ctx) in
Shift (index - roffset, t)
with
Not_found -> internal_error "DeBruijn index out of bounds!"
;;
let env_lookup_type (env : env_type) (v : vref) =
let env_lookup_type ctx (v : vref) =
let ((_, rname), dbi) = v in
try let (recursion_offset, (_, dname), _, t) = Myers.nth dbi env in
try let (recursion_offset, (_, dname), _, t) = Myers.nth dbi (_get_env ctx) in
if dname = rname then
Shift (dbi - recursion_offset, t)
else
internal_error "DeBruijn index refers to wrong name!"
with Not_found -> internal_error "DeBruijn index out of bounds!"
(* Make a Global context *)
let make_context = (_make_context_impl, None, _make_myers);;
(* Make a new Scope inside the outer context 'ctx' *)
let add_scope ctx = (_make_context_impl, Some ctx, _make_myers);;
(* Print Functions for testing *)
let print_scope (scp: scope) (offset: int): unit =
StringMap.iter
(fun key value
-> print_string (key ^ "\t");
print_int (value + offset);
print_string "\n")
scp
;;
let print_lexp_context (ctx: lexp_context): unit =
print_string " Context Print\n";
let rec impl (ctx2: lexp_context) (offset: int) =
let inner = _get_inner_scope ctx2 in
match ctx2 with
| (_, Some ct, _)
-> impl ct ((_get_offset ctx2) + offset);
(print_scope inner offset);
| _ -> (print_scope inner offset) in
(impl ctx 0)
;;
\ No newline at end of file
let env_lookup_by_index index ctx = Myers.nth index (_get_env ctx);;
\ No newline at end of file
......@@ -37,6 +37,13 @@ open Myers
open Sexp
open Fmt
let eval_error loc msg =
msg_error "EVAL" loc msg;
raise (internal_error msg)
;;
let dloc = dummy_location
let eval_warning = msg_warning "EVAL"
let print_myers_list l print_fun =
......@@ -102,9 +109,23 @@ let rec eval lxp ctx: (lexp * runtime_env) =
value, ctx end
(* Function call *)
| Call (fname, args) ->
| Call (lname, args) ->
(* Try to extract name *)(*
let tname = match lname with
|Var((loc, name), _) -> name
| _ -> lexp_print lname; eval_error "Incorrect Function Name" in
(* Save declaration in environment *)
let n = List.length args in
if tname = "_=_" && n == 2 then
let (((_, name), _), expr) = args in
let nctx = add_rte_variable *)
(* Add args in the scope *)
print_rte_ctx ctx;
let nctx = build_arg_list args ctx in
print_rte_ctx nctx;
(* We need to seek out the function declaration and eval the body *)
(* but currently we cannot declare functions so I hardcoded + *)
......@@ -112,14 +133,17 @@ let rec eval lxp ctx: (lexp * runtime_env) =
eval bdy nctx *)
(* fname is currently a var *)
let name = get_function_name fname in
let name = get_function_name lname in
(* Hardcoded function for now *)
if name = "_+_" then begin
(* Get the two args *)
let l = get_int (get_rte_variable 0 nctx) in
let r = get_int (get_rte_variable 1 nctx) in
(*print_int l; print_string " ";
print_int r; print_string "\n"; *)
Imm(Integer(dummy_location, l + r)), ctx end
else
Imm(String(dummy_location, "Funct Not Implemented")), ctx
......@@ -127,10 +151,8 @@ let rec eval lxp ctx: (lexp * runtime_env) =
| _ -> Imm(String(dummy_location, "Eval Not Implemented")), ctx
and build_arg_list args ctx =
(* Eval every args *)
let arg_val = List.map (fun (k, e) -> let (v, c) = eval e ctx in v) args in
(* Add args inside context *)
List.fold_left (fun c v -> add_rte_variable v c) ctx arg_val
......
......@@ -36,55 +36,43 @@ let str_size_int value =
;;
(* print n char 'c' *)
let rec make_line c n =
print_string c;
if n >= 1 then (make_line c (n - 1));
;;
(* print an integer right-aligned *)
let ralign_print_int value nb =
make_line " " (nb - (str_size_int value));
print_int value;
;;
let rec make_line c n = String.make n c;;
let lalign_print_int value nb =
print_int value;
make_line " " (nb - (str_size_int value));
;;
let ralign_print_string str nb =
make_line " " (nb - String.length str);
print_string str;
(* Big numbers are replaced by #### *)
let cut_int (v:int) (start:int) (len:int): int = 0;;
(* LALIGN
* ----------------------- *)
let ralign_generic get_size print_str print_elem cut_elem elem col =
let n = get_size elem in
if n > col then
print_elem (cut_elem elem 0 col)
else begin
print_str (make_line ' ' (col - n));
print_elem elem; end
;;
let lalign_print_string str nb =
print_string str;
make_line " " (nb - String.length str);
;;
let ralign_print_string =
ralign_generic String.length print_string print_string String.sub;;
(* print n char 'c' *)
let rec prerr_make_line c n =
prerr_string c;
if n >= 1 then (make_line c (n - 1));
;;
(* print an integer right-aligned *)
let ralign_prerr_int value nb =
prerr_make_line " " (nb - (str_size_int value));
prerr_int value;
;;
let ralign_print_int =
ralign_generic str_size_int print_string print_int cut_int;;
let lalign_prerr_int value nb =
prerr_int value;
prerr_make_line " " (nb - (str_size_int value));
;;
(* LALIGN
* ----------------------- *)
let lalign_generic get_size print_str print_elem cut_elem elem col =
let n = get_size elem in
if n > col then
print_elem (cut_elem elem 0 col)
else begin
print_elem elem;
print_str (make_line ' ' (col - n)); end
;;
let lalign_print_string =
lalign_generic String.length print_string print_string String.sub;;
let ralign_prerr_string str nb =
prerr_make_line " " (nb - String.length str);
prerr_string str;
;;
let lalign_print_int =
lalign_generic str_size_int print_string print_int cut_int;;
let lalign_prerr_string str nb =
prerr_string str;
prerr_make_line " " (nb - String.length str);
;;
......@@ -47,14 +47,15 @@ let not_implemented_error () =
internal_error "not implemented"
;;
let lexp_error loc msg =
let dloc = dummy_location
let lexp_warning = msg_warning "LEXP"
let lexp_error = msg_error "LEXP"
let lexp_fatal loc msg =
msg_error "LEXP" loc msg;
raise (internal_error msg)
;;
let dloc = dummy_location
let lexp_warning = msg_warning "LEXP"
(* Print back in CET (Close Enough Typer) easier to read *)
(* pretty ? * indent level * print_type? *)
type print_context = (bool * int * bool)
......@@ -77,17 +78,22 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =
(* Block/String/Integer/Float *)
| Pimm value -> Imm(value), ctx
(* Symbol i.e identifier /!\ A lot of Pvar are not variables /!\ *)
| Pvar (loc, name) ->
let idx = senv_lookup name ctx in
(* This should be an error but we accept it for debugging *)
if idx < 0 then
lexp_warning tloc ("Variable: '" ^ name ^ "' does not exist");
(make_var name (idx) loc), ctx;
(* Symbol i.e identifier *)
| Pvar (loc, name) -> begin
try
(* Send Variable loc *)
let idx = senv_lookup name ctx in
(make_var name idx loc), ctx;
with Not_found ->
(* Add Variable *)
let ctx = senv_add_var name loc ctx in
(make_var name 0 loc), ctx; end
(* Let, Variable declaration + local scope *)
| Plet(loc, decls, body) -> (* /!\ HERE *)
let decl, nctx = lexp_parse_let decls (add_scope ctx) in
| Plet(loc, decls, body) ->
let decl, nctx = lexp_parse_let decls ctx in
lexp_context_print nctx;
let bdy, nctx = lexp_parse body nctx in
(* Send back old context as we exit the inner scope *)
Let(tloc, decl, bdy), ctx
......@@ -115,19 +121,42 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =
let nvar = pvar_to_vdef var in (* /!\ HERE *)(* /!\ Missing Type *)
let lbody, ctx = lexp_parse body ctx in
Lambda(kind, nvar, UnknownType(tloc), lbody), ctx
(* Function Call *)
| Pcall (fname, _args) ->
(* Why function names are pexp ? *)
let fname, ctx = lexp_parse fname ctx in
(* Process Arguments *)
let pargs = pexp_parse_all _args in
let largs, fctx = lexp_parse_all pargs ctx in
(* Make everything explicit for now *)
let new_args = List.map (fun g -> (Aexplicit, g)) largs in
Call(fname, new_args), ctx
(* Call to named function which must have been defined earlier *
* i.e they must be in the context *)
begin try begin
(* Get function name *)
let name, loc = match fname with
| Pvar(loc, nm) -> nm, loc
| Pcons (_, (loc, nm)) -> nm, loc
| _ -> raise Not_found in
try
(* Check if the function was defined *)
let idx = senv_lookup name ctx in
let vf = (make_var name idx loc) in
Call(vf, new_args), ctx
with Not_found ->
(* Don't stop even if an error was found *)
lexp_error loc ("The function \"" ^ name ^
"\" was not defined");
let vf = (make_var name (-1) loc) in
Call(vf, new_args), ctx end
(* Call to a nameless function *)
with Not_found ->
(* I think this should not modify context.
* if so, funny things might happen when evaluating *)
let fname, ctx = lexp_parse fname ctx in
Call(fname, new_args), ctx end
(* Pinductive *)
| Pinductive (label, _, ctors) ->
......@@ -172,6 +201,9 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =
and lexp_read_pattern pattern exp target:
(string * location * (arg_kind * vdef) option list) =
(* lookup target val if its a var and extract its args *)
(* TODO *)
match pattern with
| Ppatany (loc) -> (* Catch all expression nothing to do *)
("_", loc, [])
......@@ -202,10 +234,9 @@ and lexp_read_pattern_args args:((arg_kind * vdef) option list) =
(* Nothing to do *)
| Ppatany (loc) -> loop tl (None::acc)
| Ppatvar (loc, name) ->
(* get kind from the call *)
let nacc = (Some (Aexplicit, (loc, name)))::acc in
loop tl nacc
| _ -> lexp_error dloc "Constructor inside a Constructor";
| _ -> lexp_fatal dloc "Constructor inside a Constructor";
in loop args []
......@@ -281,19 +312,11 @@ and lexp_parse_let decls ctx =
let decls = loop decls [] in
(* Add Each Variable to the environment *)
let rec add_var_env decls ctx =
match decls with
| [] -> ctx
| hd::tl -> begin
match hd with
(* Unused variable: No Instruction *)
(* Warning will be printed later *)
| ((loc, name), None, _) -> add_var_env tl ctx
| ((loc, name), _, _) ->
let ctx = senv_add_var name loc ctx in
add_var_env tl ctx end in
let nctx = add_var_env decls ctx in
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)
ctx decls in
(* lexp_parse instruction and types *)
let rec parse_decls decls ctx acc =
......@@ -309,19 +332,16 @@ and lexp_parse_let decls ctx =
env_add_var_info (0, (loc, name), linst, ltyp) nctx in
(parse_decls tl nctx nacc)
| ((loc, name), Some pinst, None) ->
let linst, nctx = lexp_parse pinst ctx in
(* This is where UnknownType are introduced *)
(* need Inference HERE *)
let nacc = ((loc, name), linst, UnknownType(loc))::acc in
let nctx =
env_add_var_info (0, (loc, name), linst, UnknownType(loc)) nctx in
let lxp, ltp = lexp_p_infer pinst ctx in
let nacc = ((loc, name), lxp, ltp)::acc in
let nctx =
env_add_var_info (0, (loc, name), lxp, ltp) nctx in
(parse_decls tl nctx nacc)
(* Skip the variable *)
| ((loc, name), None, _) ->
lexp_warning loc "Unused Variable";
(parse_decls tl ctx acc)
end in
lexp_warning loc "Unused Variable";
(parse_decls tl ctx acc) end in
parse_decls decls nctx []
and lexp_parse_all (p: pexp list) (ctx: lexp_context):
......@@ -379,7 +399,7 @@ and lexp_print_adv opt exp =
| Let (_, decls, body) ->
print_string "let"; lexp_print_decls (pty, indent + 1, prtp) decls;
if pty then make_line " " (indent * 4 + 4);
if pty then print_string (make_line ' ' (indent * 4 + 4));
print_string " in "; lexp_print_adv (pty, indent + 2, prtp) body
| Arrow(kind, Some (_, name), tp, loc, expr) ->
......@@ -440,7 +460,7 @@ and lexp_print_adv opt exp =
| Some (kind, (l, n)) -> print_string (" " ^ n)) arg in
SMap.iter (fun key (loc, arg, exp) ->
make_line " " (indent * 4);
print_string (make_line ' ' (indent * 4));
print_string ("| " ^ key); print_arg arg;
print_string " -> ";
slexp_print exp; print_string "; ";
......@@ -450,7 +470,7 @@ and lexp_print_adv opt exp =
match dflt with
| None -> ()
| Some df ->
make_line " " (indent * 4);
print_string (make_line ' ' (indent * 4));
print_string "| _ -> "; slexp_print df;
print_string ";"; if pty then print_string "\n"; end
......@@ -475,14 +495,37 @@ and lexp_print_decls opt decls =
List.iteri (fun idx g -> match g with
| ((loc, name), expr, ltyp) ->
if pty && idx > 0 then make_line " " (indent * 4);
if pty && idx > 0 then print_string (make_line ' ' (indent * 4));
if prtp then print_type name ltyp; print_string " ";
print_string (name ^ " = ");
lexp_print_adv opt expr; print_string ";";
if pty then print_string "\n")
decls
;;
(* Print context *)
and lexp_context_print ctx =
let ((n, map), env) = ctx in
StringMap.iter (fun key idx ->
(* Print senv info *)
print_string " ";
ralign_print_string key 20;
print_string " => ";
ralign_print_int idx 4;
print_string " => ";
(* Print env Info *)
try let (_, (_, name), exp, tp) = env_lookup_by_index (n - idx) ctx in
print_string name; (* name must match *)
print_string " = ";
lexp_print_adv (false, 0, true) exp;
print_string ": ";
lexp_print_adv (false, 0, true) tp;
print_string "\n"
with
Not_found -> print_string "Not_found \n")
map
;;
let lexp_print = lexp_print_adv (false, 0, true)
......@@ -36,15 +36,6 @@ let print_loc (loc: location) =
Fmt.ralign_print_int loc.column 3;
;;
(* print debug info *)
let prerr_loc (loc: location) =
(*print_string loc.file; *) (* Printing the file is too much*)
prerr_string "ln ";
Fmt.ralign_prerr_int loc.line 3;
prerr_string ", cl ";
Fmt.ralign_prerr_int loc.column 3;
;;
(* File is not printed because currently we parse only one file... *)
(* Section is the name of the compilation step [for debugging] *)
(* 'prerr' output is ugly *)
......
......@@ -40,6 +40,8 @@ open Sexp
open Pexp
open Lexp
open Lparse
open Debruijn
open Fmt
(* Print aPretokens *)
let rec debug_pretokens_print pretoken =
......@@ -178,3 +180,4 @@ let debug_lexp_print_all lexps =
;;
......@@ -40,6 +40,7 @@ open Debruijn
open Lparse
open Myers
open Eval
open Util
(* pexp and lexp can be done together, one by one *)
let pexp_lexp_one node ctx =
......@@ -94,7 +95,7 @@ let main () =
let pexps = pexp_parse_all nodes in
(* get lexp *)
let ctx = make_context in
let ctx = make_lexp_context in
let lexps, new_ctx = lexp_parse_all pexps ctx in
(* Printing *)(*
......