Setepenre pushed to branch master at Stefan / Typer

Commits: d951e229 by Pierre Delaunay at 2016-05-11T10:01:39-04:00 Fix security issue with builtin

Changes to be committed: * src/lparse.ml: "Built-in" is only usable during lexp_parse of internal typer files * .travis.yml: try to make travis compile * opam: added opam package definition (travis might need it) * GNUmakefile: add a dummy (make install) for opam

- - - - - 73a0c47f by Pierre Delaunay at 2016-05-11T11:41:35-04:00 merge

- - - - - de9aad3d by Pierre Delaunay at 2016-05-12T10:53:14-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer

- - - - - 2f9f95fa by Pierre Delaunay at 2016-05-13T10:56:42-04:00 Use TC.conv_p to check that inferred_t = t in lexp_p_check

Changes to be committed: * src/debug_util.ml * src/lparse.ml: - default_lctx is not a function anymore (avoid reading builtin files more than once) - builtin types are now built from the context * tests/* - adapted to changes * src/eval.ml - eval now uses elexp instead of lexp * src/util.ml - added `debug_msg` which eval whatever it has been given as argument if `_typer_verbose` is >= 4

- - - - -

18 changed files:

- .travis.yml - GNUmakefile - btl/types.typer - + opam - samples/qquote_temp.typer - + samples/quote.typer - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/util.ml - tests/debruijn_test.ml - tests/env_test.ml - tests/eval_test.ml - tests/lexp_test.ml - tests/macro_test.ml

Changes:

===================================== .travis.yml ===================================== --- a/.travis.yml +++ b/.travis.yml @@ -1,9 +1,16 @@ language: ocaml

+env: + - OCAML_VERSION=4.02 + addons: apt: packages: - ocaml

+before_script: + - opam config setup -a + - opam config env + script: make tests

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

+# There is nothing here. I use this to test if opam integration works +install: tests + tests: tests-build tests-run

# Make language doc

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -51,7 +51,7 @@ Bool = inductive_ (Boolean) (True) (False); True = inductive-cons Bool True; False = inductive-cons Bool False;

-Option : Type -> Type; +%Option : Type -> Type; Option = inductive_ (Option (a : Type)) (None) (Some a); Some = inductive-cons Option Some; None = inductive-cons Option None; @@ -118,7 +118,7 @@ integer_ = Built-in "integer_"; float_ : Float -> Sexp; float_ = Built-in "float_";

-Macro : Type; +% Macro : Type; Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp)); Macro_ = inductive-cons Macro Macro_ ;

===================================== opam ===================================== --- /dev/null +++ b/opam @@ -0,0 +1 @@ +opam-version: "1.2" name: "typer" version: "0.0.0" maintainer: "Stefan Monnier monnier@iro.umontreal.ca" authors: "Stefan Monnier monnier@iro.umontreal.ca, Pierre Delaunay pierre.delaunay@hec.ca" homepage: "https://gitlab.com/monnier/typer" build: [ [make] ] build-test: [make "tests"] install: [make "install"] remove: ["ocamlfind" "remove" "typer"] depends: [ "ocamlfind" {build} ] \ No newline at end of file

===================================== samples/qquote_temp.typer ===================================== --- a/samples/qquote_temp.typer +++ b/samples/qquote_temp.typer @@ -5,41 +5,10 @@ sqr = Macro_ (lambda (x : List Sexp) -> (node_ (symbol_ "_*_") (cons hd (cons hd nil))));

-symbol = lambda (y : String) -> (symbol_ y) ; -string = lambda (y : String) -> (string_ y) ; -integer = lambda (y : Int) -> (integer_ y) ; -float = lambda (y : Float) -> (float_ y) ; -block = lambda (y : List Sexp) -> (block_ y) ;

-qquote : List Sexp -> List Sexp;

-node = (lambda (op : Sexp) -> - lambda (y : List Sexp) -> - case y - | nil => node_ op nil - | _ => node_ op (qquote y)); - - -qquote = lambda (x : List Sexp) -> - let target = head Sexp x; - tl = tail Sexp x; - - rhd = sexp_dispatch_ target - node symbol string integer float block; - - rtl = case tl - | nil => nil - | _ => qquote tl; - - in - cons rhd rtl; - - -nd = node_ (symbol_ "_+_") (cons (symbol_ "x") (cons (symbol_ "x") nil)); -tst = cons nd nil; - -% tst = (cons (symbol_ "x") (cons (symbol_ "x") nil)); - -main = qquote tst; - -main = Macro_ lamda \ No newline at end of file +%nd = node_ (symbol_ "_+_") (cons (symbol_ "x") (cons (symbol_ "x") nil)); +%tst = cons nd nil; +%tst = (cons (symbol_ "x") (cons (symbol_ "x") nil)); +%main = qquote tst; +%main = Macro_ lamda \ No newline at end of file

===================================== samples/quote.typer ===================================== --- /dev/null +++ b/samples/quote.typer @@ -0,0 +1,41 @@ +% those are name aliases +symbol = lambda (y : String) -> (symbol_ y) ; +string = lambda (y : String) -> (string_ y) ; +integer = lambda (y : Int) -> (integer_ y) ; +float = lambda (y : Float) -> (float_ y) ; +block = lambda (y : List Sexp) -> (block_ y) ; + +% traverse nodes +node : Sexp -> List Sexp -> Sexp; +node = (lambda (op : Sexp) -> + lambda (y : List Sexp) -> + case y + | nil => node_ op nil + | _ => node_ op (quote' y)); + +% tree traversal +quote' : List Sexp -> List Sexp; +quote' = lambda (x : List Sexp) -> + let target = head Sexp x; + tl = tail Sexp x; + + rhd = sexp_dispatch_ target + node symbol string integer float block; + + rtl = case tl + | nil => nil + | _ => quote' tl; + + in (cons rhd rtl); + + +% quote definition +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); \ No newline at end of file

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -45,6 +45,7 @@ open Prelexer open Lexer open Lparse open Eval +module EL = Elexp

(* definitions *) open Grammar @@ -54,8 +55,6 @@ open Builtin open Debruijn open Env

- - let dloc = dummy_location let dummy_decl = Imm(String(dloc, "Dummy"))

@@ -192,7 +191,7 @@ let format_source () = let toks = lex default_stt pretoks in let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in let pexps = pexp_decls_all nodes in - let ctx = default_lctx () in + let ctx = default_lctx in let lexps, _ = lexp_p_decls pexps ctx in

print_string (make_sep '-'); print_string "\n"; @@ -268,7 +267,7 @@ let main () = debug_pexp_decls pexps; print_string "\n"));

(* get lexp *) - let ctx = default_lctx () in + let ctx = default_lctx in

print_string yellow; let lexps, nctx = @@ -288,10 +287,12 @@ let main () = (if (get_p_option "lctx") then( print_lexp_ctx nctx; print_string "\n"));

+ let clean_lxp = EL.clean_decls lexps in + (* Eval declaration *) - let rctx = default_rctx () in + let rctx = default_rctx in print_string yellow; - let rctx = (try eval_decls lexps rctx; + let rctx = (try eval_decls clean_lxp rctx; with e -> print_string reset; print_rte_ctx (!_global_eval_ctx);

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -74,7 +74,7 @@ let rec erase_type (lxp: L.lexp): elexp = | L.Cons(_, s) -> Cons(s)

| L.Lambda(kind, vdef, _, body) -> - if kind == Aexplicit then + if kind != Aerasable then Lambda(vdef, erase_type body) else erase_type body @@ -98,12 +98,11 @@ let rec erase_type (lxp: L.lexp): elexp = (* Still useful to some extend *) | L.Inductive(l, label, _, _) -> Inductive(l, label)

- and filter_arg_list lst = let rec filter_arg_list lst acc = match lst with | (kind, lxp)::tl -> - let acc = if kind == Aexplicit then + let acc = if kind != Aerasable then (erase_type lxp)::acc else acc in filter_arg_list tl acc | [] -> List.rev acc in @@ -122,7 +121,7 @@ and clean_map cases = let rec clean_arg_list lst acc = match lst with | (kind, var)::tl -> - let acc = if kind == Aexplicit then + let acc = if kind != Aerasable then var::acc else acc in clean_arg_list tl acc | [] -> List.rev acc in @@ -131,7 +130,6 @@ and clean_map cases = SMap.mapi (fun key (l, args, expr) -> (l, (clean_arg_list args), (erase_type expr))) cases

- let rec elexp_location e = match e with | Imm s -> sexp_location s @@ -148,8 +146,8 @@ let rec elexp_location e = | Sort _ -> U.dummy_location | SortLevel _ -> 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 = let maybe_str lxp = match lxp with

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -34,8 +34,9 @@ open Util (* msg_error *) open Fmt (* make_title, table util *)

open Sexp -open Lexp (* lexp_print *) +(* open Lexp ( * lexp_print *)

+open Elexp open Myers open Debruijn

@@ -54,7 +55,7 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of string | Vfloat of float - | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) + | Closure of elexp * (((string option * value_type) ref myers) * (int * int)) | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy @@ -62,7 +63,7 @@ type value_type = let rec value_print (vtp: value_type) = match vtp with | Closure (lxp, _) -> - print_string ("Closure(" ^ (_lexp_to_str (!debug_ppctx) lxp) ^ ")") + print_string ("Closure(" ^ (elexp_str lxp) ^ ")") | Vsexp sxp -> sexp_print sxp | Vint(i) -> print_int i | Vfloat(f) -> print_float f @@ -79,7 +80,7 @@ let rec value_print (vtp: value_type) = let value_location (vtp: value_type) = match vtp with | Vcons ((loc, _), _) -> loc - | Closure (lxp, _) -> lexp_location lxp + | Closure (lxp, _) -> elexp_location lxp (* location info was lost or never existed *) | _ -> dloc

@@ -96,7 +97,8 @@ let is_free_var idx ctx = let tsize = (get_rte_size ctx) - osize in if idx > tsize then true else false

-let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): value_type = +let get_rte_variable (name: string option) (idx: int) + (ctx: runtime_env): value_type = let (l, _) = ctx in try ( let ref_cell = (nth idx l) in

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

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

+open Elexp open Builtin open Grammar

open Debruijn open Env

-module ET = Elexp

(* eval error are always fatal *) let eval_error loc msg = @@ -64,7 +64,7 @@ let _builtin_lookup = ref SMap.empty (* This is an internal definition * 'i' is the recursion depth used to print the call trace *) let rec _eval lxp ctx i: (value_type) = - let tloc = lexp_location lxp in + let tloc = elexp_location lxp in

(if i > (!_eval_max_recursion_depth) then eval_fatal tloc "Recursion Depth exceeded"); @@ -78,10 +78,10 @@ let rec _eval lxp ctx i: (value_type) = | Imm(Integer (_, i)) -> Vint(i) | Imm(String (_, s)) -> Vstring(s) | Imm(sxp) -> Vsexp(sxp) - | Inductive (_, _, _, _) -> Vdummy - | Cons (_, label) -> Vcons (label, []) - | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) - | Builtin ((_, str), _) -> Vbuiltin(str) + | Inductive (_, _) -> Vdummy + | Cons (label) -> Vcons (label, []) + | Lambda (_, lxp) -> Closure(lxp, ctx) + | Builtin ((_, str)) -> Vbuiltin(str)

(* Return a value stored in env *) | Var((loc, name), idx) as e -> eval_var ctx e ((loc, name), idx) @@ -96,11 +96,11 @@ let rec _eval lxp ctx i: (value_type) = | Call (lname, args) -> eval_call ctx i lname args

(* Case *) - | Case (loc, target, _, _, pat, dflt) + | Case (loc, target, pat, dflt) -> (eval_case ctx i loc target pat dflt)

| _ -> print_string "debug catch-all eval: "; - lexp_print lxp; Vstring("eval Not Implemented") + elexp_print lxp; print_string "\n"; Vstring("eval Not Implemented")

and eval_var ctx lxp v = let ((loc, name), idx) = v in @@ -109,8 +109,8 @@ and eval_var ctx lxp v = eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")

and eval_call ctx i lname args = - let loc = lexp_location lname in - let args = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in + let loc = elexp_location lname in + let args = List.map (fun e -> _eval e ctx (i + 1)) args in let f = _eval lname ctx (i + 1) in

let rec eval_call f args ctx = @@ -130,7 +130,7 @@ and eval_call ctx i lname args = (* return result of eval *) | _, [] -> f

- | _ -> value_print f; + | _ -> debug_msg (value_print f); eval_error loc "Cannot eval function" in

eval_call f args ctx @@ -144,8 +144,9 @@ and eval_case ctx i loc target pat dflt = | Vcons((_, cname), args) -> cname, args | _ -> (* -- Debug print -- *) - lexp_print target; print_string "\n"; - value_print v; print_string "\n"; + debug_msg ( + elexp_print target; print_string "\n"; + value_print v; print_string "\n"); (* -- Crash -- *) eval_error loc "Target is not a Constructor" in

@@ -155,10 +156,10 @@ and eval_case ctx i loc target pat dflt = (* This is more robust *) let rec fold2 nctx pats args = match pats, args with - | (_, Some (_, name))::pats, arg::args -> + | (Some (_, name))::pats, arg::args -> let nctx = add_rte_variable (Some name) arg nctx in fold2 nctx pats args - | (_, None)::pats, arg::args -> fold2 nctx pats args + | (None)::pats, arg::args -> fold2 nctx pats args (* Errors: those should not happen but they might *) (* List.fold2 would complain. we print more info *) | _::_, [] -> eval_warning loc "a) Eval::Case Pattern Error"; nctx @@ -182,18 +183,18 @@ and build_arg_list args ctx i = List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val

and eval_decls decls ctx = _eval_decls decls ctx 0 -and _eval_decls (decls: ((vdef * lexp * ltype) list)) - (ctx: runtime_env) i: runtime_env = +and _eval_decls (decls: ((vdef * elexp) list)) + (ctx: runtime_env) i: runtime_env =

(* Read declarations once and push them *) - let ctx = List.fold_left (fun ctx ((_, name), lxp, ltp) -> + let ctx = List.fold_left (fun ctx ((_, name), lxp) -> add_rte_variable (Some name) Vdummy ctx) ctx decls in

let n = (List.length decls) - 1 in

(* Read declarations once and push them *) - let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp, ltp) -> + let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp) -> _global_eval_trace := []; let lxp = _eval lxp ctx (i + 1) in let ctx = set_rte_variable idx (Some name) lxp ctx in @@ -257,7 +258,7 @@ and sexp_dispatch loc args ctx =

let sxp = match sxp with | Vsexp(sxp) -> sxp - | _ -> value_print sxp; + | _ -> debug_msg (value_print sxp); eval_error loc "sexp_dispatch expects a Sexp as 1st arg" in

match sxp with @@ -289,7 +290,7 @@ and print_eval_result i lxp =

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

let eval lxp ctx = _global_eval_trace := []; @@ -315,8 +316,7 @@ let from_lctx (ctx: lexp_context): runtime_env = let ((_, _), env, _) = ctx in let rctx = ref make_runtime_ctx in

- (* Skip builtins: They are already in default_rctx() *) - let bsize = 1 in + let bsize = 1 in (*skip the first Built-in function (useless) *) let csize = get_size ctx in

(* add all variables *) @@ -333,8 +333,10 @@ let from_lctx (ctx: lexp_context): runtime_env = let (_, (_, name), exp, _) = !(Myers.nth j env) in

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

| None -> Vdummy in

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -65,7 +65,8 @@ type ltype = lexp | Arrow of arg_kind * vdef option * ltype * U.location * lexp | Lambda of arg_kind * vdef * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label * ((arg_kind * vdef * ltype) list) + | Inductive of U.location * label + * ((arg_kind * vdef * ltype) list) (* formal Args *) * ((arg_kind * vdef option * ltype) list) SMap.t | Cons of vref * symbol (* = Type info * ctor_name *) | Case of U.location * lexp

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -48,6 +48,9 @@ open Eval open Grammar open Builtin

+module TC = Typecheck +module EL = Elexp + (* Shortcut => Create a Var *) let make_var name index loc = Var(((loc, name), index)) @@ -62,6 +65,7 @@ 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 btl_folder = ref "./btl/"

(* The main job of lexp (currently) is to determine variable name (index) @@ -99,11 +103,16 @@ let btl_folder = ref "./btl/" * - use lexp_p_check whenever you can. *)

-(* - * Infer: Imm, bultin, var, let, arrow, call, inductive, cons, case - * - * check: lambda - *) + +let build_var name ctx = + let type0_idx = senv_lookup name ctx in + Var((dloc, name), type0_idx) + +(* build type0 from ctx *) +let get_type0 ctx = build_var "Type" ctx +let get_int ctx = build_var "Int" ctx + + let rec lexp_p_infer (p : pexp) (ctx : lexp_context): lexp * ltype = _lexp_p_infer p ctx 1

@@ -119,7 +128,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* Block/String/Integer/Float *) | Pimm value -> (Imm(value), match value with - | Integer _ -> type_int + | Integer _ -> get_int ctx | Float _ -> type_float | String _ -> type_string; | _ -> lexp_error tloc "Could not find type"; @@ -154,33 +163,29 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =

let lxp, _ = lexp_infer expr ctx in let v = Arrow(kind, ovar, ltp, tloc, lxp) in - v, type0 + v, (get_type0 ctx)

(* Pinductive *) | Pinductive (label, formal_args, ctors) -> - let ctx = ref ctx in + let type0 = get_type0 ctx in + let nctx = ref ctx in (* (arg_kind * pvar * pexp option) list *) let formal = List.map (fun (kind, var, opxp) -> let ltp, _ = match opxp with - | Some pxp -> _lexp_p_infer pxp !ctx (i + 1) + | Some pxp -> _lexp_p_infer pxp !nctx (i + 1) | None -> dltype, dltype in

- ctx := env_extend !ctx var None dltype; + nctx := env_extend !nctx var None ltp; (kind, var, ltp) ) formal_args in - (* (arg_kind * vdef * ltype) list *)

- (* -- Should I do that ?? --* ) - let rec make_type args tp = - match args with - | (kind, (loc, n), ltp)::tl -> - make_type tl (Arrow(kind, Some (loc, n), ltp, loc, tp)) - | [] -> tp in *) + let nctx = !nctx in + let ltp = List.fold_left (fun tp (kind, _, _) -> + (Arrow(kind, None, type0, tloc, tp))) type0 formal in

- let ctx = !ctx in - let map_ctor = lexp_parse_inductive ctors ctx i in + let map_ctor = lexp_parse_inductive ctors nctx i in let v = Inductive(tloc, label, formal, map_ctor) in - v, type0 + v, ltp

(* This case can be inferred *) | Plambda (kind, var, optype, body) -> @@ -269,9 +274,18 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let lxp, _ = lexp_case (Some t) (loc, target, patterns) ctx i in lxp

- | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in - (* FIXME: check that inferred_t = t! *) - e + | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in ( + match e with + (* Built-in is a dummy function with no type. We cannot check + * Built-in *) + | Builtin _ -> e + | _ -> + (if TC.conv_p inferred_t t then () else debug_msg ( + print_string "1 exp "; lexp_print e; print_string "\n"; + print_string "2 inf "; lexp_print inferred_t; print_string "\n"; + print_string "3 Ann "; lexp_print t; print_string "\n"; + lexp_warning tloc "Type Mismatch inferred != Annotation")); + e)

(* Lexp.case cam be checked and inferred *) and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = @@ -380,10 +394,14 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = Call(vf, new_args), ret_type

| Some Builtin((_, "Built-in"), ltp) ->( + match !_parsing_internals with + | false -> lexp_error loc "Use of Built-in in user code"; + dlxp, dlxp + | _ ->( match largs with | [Imm (String (_, str)) ] -> Builtin((loc, str), ltp), ltp - | _ -> typer_unreachable "cannot be reached") + | _ -> typer_unreachable "cannot be reached"))

(* a builtin functions *) | Some Builtin((_, name), ltp) -> @@ -423,14 +441,18 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let arg = olist2tlist_lexp sargs ctx in let lxp = Call(lxp, [(Aexplicit, arg)]) in

+ (* + print_string "\n\n"; + lexp_print lxp; print_string "\n\n"; *) + let rctx = (from_lctx ctx) in - let sxp = match eval lxp rctx with + let sxp = match eval (EL.erase_type lxp) rctx with | Vsexp(sxp) -> sxp (* Those are sexp converted by the eval function *) | Vint(i) -> Integer(dloc, i) | Vstring(s) -> String(dloc, s) | Vfloat(f) -> Float(dloc, f) - | v -> value_print v; print_string "\n"; + | v -> debug_msg (value_print v); lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in

let pxp = pexp_parse sxp in @@ -769,7 +791,7 @@ let add_def name ctx = * --------------------------------------------------------- *)

(* Make lxp context with built-in types *) -let default_lctx () = +let default_lctx = (* Empty context *) let lctx = make_lexp_context in let lxp = Builtin((dloc, "Built-in"), type0) in @@ -781,12 +803,14 @@ let default_lctx () = 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 - lctx + _parsing_internals := false; + lctx

(* Make runtime context with built-in types *) -let default_rctx () = - try (from_lctx (default_lctx ())) +let default_rctx = + try (from_lctx (default_lctx)) with e -> lexp_fatal dloc "Could not convert lexp context into rte context"

@@ -820,10 +844,12 @@ let lexp_decl_str str lctx =

let _eval_expr_str str lctx rctx silent = let lxps = lexp_expr_str str lctx in - (eval_all lxps rctx silent) + let elxps = List.map EL.erase_type lxps in + (eval_all elxps rctx silent)

let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false

let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in - (eval_decls lxps rctx), lctx + let elxps = (EL.clean_decls lxps) in + (eval_decls elxps rctx), lctx

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -66,12 +66,17 @@ let msg_message lvl kind section (loc: location) msg = print_string msg; print_newline ()) else ()

-let msg_error = msg_message 1 "[!] Error " -let msg_info = msg_message 3 "[?] Info " -let msg_warning = msg_message 2 "/!\ Warning " + let msg_fatal s l m = msg_message 0 "[X] Fatal " s l m; internal_error m +let msg_error = msg_message 1 "[!] Error " +let msg_warning = msg_message 2 "/!\ Warning " +let msg_info = msg_message 3 "[?] Info " + +(* Compiler Internal Debug print *) +let debug_msg expr = + if 4 <= !_typer_verbose then expr else ()

let not_implemented_error () = internal_error "not implemented"

===================================== tests/debruijn_test.ml ===================================== --- a/tests/debruijn_test.ml +++ b/tests/debruijn_test.ml @@ -36,7 +36,7 @@ open Builtin open Debruijn

-let lctx = default_lctx () +let lctx = default_lctx

let make_val value = Imm(String(dloc, value))

===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -36,7 +36,7 @@ open Builtin open Env

-let rctx = default_rctx () +let rctx = default_rctx

let make_val value = Vstring(value)

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -38,8 +38,8 @@ open Builtin open Env

(* default environment *) -let lctx = default_lctx () -let rctx = default_rctx () +let lctx = default_lctx +let rctx = default_rctx

let _ = (add_test "EVAL" "Variable Cascade" (fun () -> reset_eval_trace (); @@ -156,8 +156,6 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> * ------------------------ *)

let _ = (add_test "EVAL" "Inductive::Case" (fun () -> - let lctx = default_lctx () in - let rctx = default_rctx () in reset_eval_trace ();

(* Inductive type declaration + Noisy declarations *)

===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -34,24 +34,9 @@ open Lparse (* add_def *) open Builtin

(* default environment *) -let lctx = default_lctx () +let lctx = default_lctx

-let _ = (add_test "LEXP" "Built-in type Inference" (fun () -> - - let dcode = "a = 10; b = 1.12;" in - - let ret, _ = lexp_decl_str dcode lctx in - - match ret with - (* (vdef * lexp * ltype) *) - | [(_, _, Builtin((_, "Int"), _)); - (_, _, Builtin((_, "Float"), _))] -> - success() - - | _ -> failure () -)) - let _ = (add_test "LEXP" "lexp_print" (fun () ->

let dcode = "

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -39,8 +39,8 @@ open Env

(* default environment *) -let lctx = default_lctx () -let rctx = default_rctx () +let lctx = default_lctx +let rctx = default_rctx

let _ = (add_test "MACROS" "macros base" (fun () ->

View it on GitLab: https://gitlab.com/monnier/typer/compare/a93ade4b22f00b07114f4865a3555181d4f...