Stefan pushed to branch unification at Stefan / Typer

Commits: 1d2bbfca by Stefan Monnier at 2016-09-19T17:46:29-04:00 * src/debruijn.ml (elab_context): Rename from lexp_context.

- - - - - b0866ba1 by Stefan Monnier at 2016-09-19T17:52:08-04:00 * src/debruijn.ml (lexp_context): Rename from env_type.

- - - - - 222406c2 by Stefan Monnier at 2016-09-19T18:38:35-04:00 * src/debruijn.ml (lexp_ctx_cons): New fun. Test sanity of `offset`

(M): Alias for Myers, which we don't open any more. (lctx_extend, lctx_extend_rec): New functions. (env_extend): Use them. * src/opslexp.ml (check): Use lctx_extend(_rec).

- - - - - a6e1dc19 by Pierre Delaunay at 2016-09-20T13:07:36-04:00 Added a new way to make tests for eval using a similar mechanism that what is used for sexp

* src/env.ml - new functions (value_equal) and (value_eq_list) * tests/eval_test.ml - new function (test_eval_eqv) - modified tests to use the new mechanism - added 3 new tests on special forms (decltype) (declexpr) and (has-attribute)

- - - - - 2eb9aeee by Pierre Delaunay at 2016-09-20T16:53:19-04:00 Special forms are macros but conv_p does not recognize them as such (db index problem). I have implemented a temporary work around. - src/lparse.ml

- - - - - 66020e6c by Pierre Delaunay at 2016-09-20T16:53:37-04:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - df72decc by Stefan Monnier at 2016-09-25T21:55:39-04:00 Merge branch 'trunk' into unification

- - - - -

10 changed files:

- src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - tests/eval_test.ml

Changes:

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -127,7 +127,7 @@ let ierase_type (lexps: (ldecl list list * lexpr list)) = (List.map OL.clean_decls ldecls), (List.map OL.erase_type lexprs)

-let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * lexp_context) = +let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in let ldecls, lctx = lexp_p_decls pdecls lctx in let lexprs = lexp_parse_all pexprs lctx in

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -190,7 +190,8 @@ let make_node loc depth args_val ctx = | [Vsexp(op); lst] -> op, lst | op::_ -> builtin_error loc - ("node_ expects one 'Sexp' got " ^ (value_name op)) in + ("node_ expects one 'Sexp' got " ^ (value_name op)) + | _ -> typer_unreachable "-" in

(* value_print tlist; print_string "\n"; *)

@@ -306,7 +307,10 @@ let get_attribute_impl loc largs ctx ftype = | _ -> builtin_error loc "get-attribute expects two arguments" in

let lxp = get_property ctx (vi, vn) (ai, an) in - let Some ltype = env_lookup_expr ctx ((loc, an), ai) in + let ltype = match env_lookup_expr ctx ((loc, an), ai) with + | Some ltp -> ltp + | None -> builtin_error loc "not expression available" in + lxp, ltype

let new_attribute_impl loc largs ctx ftype = @@ -336,7 +340,9 @@ let declexpr_impl loc largs ctx ftype = | [Var((_, vn), vi)] -> (vi, vn) | _ -> builtin_error loc "declexpr expects one argument" in

- let Some lxp = env_lookup_expr ctx ((loc, vn), vi) in + let lxp = match env_lookup_expr ctx ((loc, vn), vi) with + | Some lxp -> lxp + | None -> builtin_error loc "no expr available" in let ltp = env_lookup_type ctx ((loc, vn), vi) in lxp, ftype

@@ -363,7 +369,7 @@ let builtin_macro = [ ]

type macromap = - (location -> lexp list -> lexp_context -> lexp -> (lexp * lexp)) SMap.t + (location -> lexp list -> elab_context -> lexp -> (lexp * lexp)) SMap.t

let macro_impl_map : macromap = List.fold_left (fun map (name, funct) ->

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -35,9 +35,8 @@ open Util open Lexp module L = Lexp -open Myers +module M = Myers open Fmt -(*open Typecheck env_elem and env_type *)

module S = Subst

@@ -62,7 +61,7 @@ type property_env = property_elem PropertyMap.t (* easier to debug with type annotations *) type env_elem = (int * vdef option * varbind * ltype) (* FIXME: This is the *lexp context*. *) -type env_type = env_elem myers +type lexp_context = env_elem M.myers

type db_idx = int (* DeBruijn index. *) type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) @@ -73,13 +72,12 @@ type scope = db_ridx StringMap.t (* Map<String, db_ridx>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope

-(* FIXME: This is the *elaboration context* (i.e. a context that holds +(* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) -type lexp_context = senv_type * env_type * property_env -type elab_context = lexp_context +type elab_context = senv_type * lexp_context * property_env

(* Extract the lexp context from the context used during elaboration. *) -let ectx_to_lctx (ectx : elab_context) : env_type = +let ectx_to_lctx (ectx : elab_context) : lexp_context = let (_, lctx, _) = ectx in lctx

(* internal definitions @@ -87,20 +85,20 @@ let ectx_to_lctx (ectx : elab_context) : env_type =

let _make_scope = StringMap.empty let _make_senv_type = (0, _make_scope) -let _make_myers = nil -let _get_env(ctx: lexp_context): env_type = let (_, ev, _) = ctx in ev +let _make_myers = M.nil +let _get_env(ctx: elab_context): lexp_context = let (_, ev, _) = ctx in ev

(* Public methods: DO USE * ---------------------------------- *)

-let make_lexp_context = (_make_senv_type, _make_myers, PropertyMap.empty) +let make_elab_context = (_make_senv_type, _make_myers, PropertyMap.empty)

let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof

let get_size ctx = let ((n, _), _, _) = ctx in n

(* return its current DeBruijn index *) -let rec senv_lookup (name: string) (ctx: lexp_context): int = +let rec senv_lookup (name: string) (ctx: elab_context): int = let ((n, map), _, _) = ctx in let raw_idx = n - (StringMap.find name map) - 1 in (* if raw_idx > (n - csize) then @@ -108,16 +106,38 @@ let rec senv_lookup (name: string) (ctx: lexp_context): int = else *) raw_idx

-let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = +let lexp_ctx_cons (ctx : lexp_context) offset d v t = + assert (offset >= 0 && + (ctx = M.nil || + let (previous_offset, _, _, _) = M.car ctx in + previous_offset >= 0 && previous_offset <= 1 + offset)); + M.cons (offset, d, v, t) ctx + +let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) = + lexp_ctx_cons ctx 0 (Some def) v t + +let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env, f) = ctx in (try let _ = senv_lookup name ctx in debruijn_warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = StringMap.add name n map in - ((n + 1, nmap), cons (0, Some def, v, t) env, f) + ((n + 1, nmap), + lexp_ctx_cons env 0 (Some def) v t, + f) + +let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = + let (ctx, _) = + List.fold_left + (fun (ctx, recursion_offset) (def, e, t) -> + lexp_ctx_cons ctx recursion_offset (Some def) (LetDef e) t, + recursion_offset - 1) + (ctx, List.length defs) defs in + ctx

let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = + (* FIXME: Use lctx_extend_rec! *) List.fold_left (fun (ctx, recursion_offset) (def, e, t) -> let (loc, name) = def in @@ -126,7 +146,9 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = debruijn_warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = StringMap.add name n map in - ((n + 1, nmap), cons (recursion_offset, Some def, LetDef e, t) env, f), + ((n + 1, nmap), + lexp_ctx_cons env recursion_offset (Some def) (LetDef e) t, + f), recursion_offset - 1) (ctx, List.length defs) defs

@@ -165,7 +187,7 @@ let env_lookup_expr ctx (v : vref): lexp option = | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) | _ -> None

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

(* replace an expression by another *) @@ -176,17 +198,17 @@ let replace_by ctx name by = (* lookup and replace *) let rec replace_by' ctx by acc = match ctx with - | Mnil -> debruijn_error dummy_location + | M.Mnil -> debruijn_error dummy_location ("Replace error. This expression does not exist: " ^ name) - | Mcons((_, None, _, _) as elem, tl1, i, tl2) -> + | M.Mcons((_, None, _, _) as elem, tl1, i, tl2) -> (* 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) *)

- | Mcons((_, Some (b, n), _, _) as elem, tl1, i, tl2) -> + | M.Mcons((_, Some (b, n), _, _) as elem, tl1, i, tl2) -> if n = name then - (cons by tl1), acc + (M.cons by tl1), acc else (* Skip some elements if possible *) if idx <= i then replace_by' tl1 by (elem::acc) @@ -195,7 +217,7 @@ let replace_by ctx name by =

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 + let nenv = List.fold_left (fun ctx elem -> M.cons elem ctx) nenv decls in (a, nenv, b)

(* -------------------------------------------------------------------------- *) @@ -204,7 +226,7 @@ let replace_by ctx name by =

let add_property ctx (var_i, var_n) (att_i, att_n) (prop: lexp) - : lexp_context = + : elab_context =

let (a, b, property_map) = ctx in let n = get_size ctx in

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -326,7 +326,7 @@ let main () = print_string "\n"));

(* get typecheck context *) - let lctx_to_cctx (lctx: lexp_context) = + let lctx_to_cctx (lctx: elab_context) = let (_, env, _) = ctx in env in

(if (get_p_option "typecheck") then(

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -44,6 +44,8 @@ let env_error loc msg = msg_error "ENV" loc msg; raise (internal_error msg)

+let env_warning loc msg = msg_warning "ENV" loc msg + let str_idx idx = "[" ^ (string_of_int idx) ^ "]"

@@ -62,6 +64,37 @@ type value_type = | Vcommand of (unit -> value_type)

+let rec value_equal a b = + match a, b with + | Vint(i1), Vint(i2) -> i1 = i2 + | Vstring(s1), Vstring(s2) -> s1 = s2 + | Vbuiltin(s1), Vbuiltin(s2) -> s1 = s2 + | Vfloat(f1), Vfloat(f2) -> f1 = f2 + | Vsexp(a), Vsexp(b) -> sexp_equal a b + | Vin (c1), Vin(c2) -> c1 = c2 + | Vout (c1), Vout(c2) -> c2 = c2 + | Vcommand (f1), Vcommand(f2)-> f1 = f2 + | Vdummy, Vdummy -> + env_warning dloc "Vdummy"; true + + | Closure(s1, b1, ctx1), Closure(s2, b2, ctx2) -> + env_warning dloc "Closure"; + if (s1 != s2) then false else true + + | Vcons((_, ct1), a1), Vcons((_, ct2), a2) -> + if (ct1 != ct2) then false else + not (List.exists2 + (fun a b -> not (value_equal a b)) a1 a2) + + | _ -> false + +let rec value_eq_list a b = + match a, b with + | [], [] -> true + | v1::vv1, v2::vv2 -> + value_equal v1 v2 && value_eq_list vv1 vv2 + | _ -> false + let rec value_print (vtp: value_type) = match vtp with | Closure (_, lxp, _) ->

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -411,11 +411,12 @@ let eval_all lxps rctx silent = let maybe s = match s with Some v -> v | _ -> ""

(* build a rctx from a lctx, rm is used to ignore the last 'rm' elements *) -let from_lctx (ctx: lexp_context) rm: runtime_env = +let from_lctx (ctx: elab_context) rm: runtime_env = let ((n, _), env, _) = ctx in let n = n - 1 in let rctx = ref make_runtime_ctx in

+ (* FIXME: Why not use Myers.map (Myers.nthcdr) ? *) for i = 0 to (n - rm) do let name, exp = match (Myers.nth (n - i) env) with | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -496,43 +496,43 @@ let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) *)

-(* ugly printing (sexp_print (pexp_unparse (lexp_to_pexp e))) *) -let rec lexp_to_pexp lxp = +(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) +let rec lexp_unparse lxp = match lxp with - | Susp _ as e -> lexp_to_pexp (nosusp e) + | Susp _ as e -> lexp_unparse (nosusp e) | Imm (sexp) -> Pimm (sexp) | Builtin ((loc, name), _) -> Pvar((loc, name)) | Var ((loc, name), _) -> Pvar((loc, name)) | Cons (((iloc, iname), idx), ctor) -> Pcons((iloc, iname), ctor) | Lambda (kind, vdef, ltp, body) -> - Plambda(kind, vdef, Some (lexp_to_pexp ltp), lexp_to_pexp body) + Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body) | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> - Parrow(arg_kind, vdef, lexp_to_pexp ltp1, loc, lexp_to_pexp ltp2) + Parrow(arg_kind, vdef, lexp_unparse ltp1, loc, lexp_unparse ltp2)

| Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) let pdecls = List.fold_left (fun acc (vdef, lxp, ltp) -> - Ptype(vdef, lexp_to_pexp ltp)::Pexpr(vdef, lexp_to_pexp lxp)::acc) [] ldecls in - Plet (loc, pdecls, lexp_to_pexp body) + Ptype(vdef, lexp_unparse ltp)::Pexpr(vdef, lexp_unparse lxp)::acc) [] ldecls in + Plet (loc, pdecls, lexp_unparse body)

| Call(lxp, largs) -> (* (arg_kind * lexp) list *) - let pargs = List.map (fun (kind, elem) -> lexp_to_pexp elem) largs in + let pargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in let sargs = List.map (fun elem -> pexp_unparse elem) pargs in - Pcall(lexp_to_pexp lxp, sargs) + Pcall(lexp_unparse lxp, sargs)

| Inductive(loc, label, lfargs, ctor) -> (* (arg_kind * vdef * ltype) list *) (* (arg_kind * pvar * pexp option) list *) let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, vdef, Some (lexp_to_pexp ltp))) lfargs in + (kind, vdef, Some (lexp_unparse ltp))) lfargs in

(* ((arg_kind * vdef option * ltype) list) SMap.t *) (* (symbol * (arg_kind * pvar option * pexp) list) list *) let ctor = List.map (fun (str, largs) -> let pargs = List.map (fun (kind, var, ltp) -> match var with - | Some (loc, name) -> (kind, Some (loc, name), lexp_to_pexp ltp) - | None -> (kind, None, lexp_to_pexp ltp)) largs + | Some (loc, name) -> (kind, Some (loc, name), lexp_unparse ltp) + | None -> (kind, None, lexp_unparse ltp)) largs in ((loc, str), pargs) ) (SMap.bindings ctor) in Pinductive(label, pfargs, ctor) @@ -540,25 +540,25 @@ let rec lexp_to_pexp lxp = | Case (loc, target, tltp, bltp, branches, default) -> let pbranch = List.map (fun (str, (loc, args, bch)) -> match args with - | [] -> Ppatvar (loc, str), lexp_to_pexp bch + | [] -> Ppatvar (loc, str), lexp_unparse bch | _ -> let pat_args = List.map (fun (kind, vdef) -> match vdef with | Some vdef -> Some (kind, vdef), Ppatvar(vdef) | None -> None, Ppatany(loc)) args - in Ppatcons ((loc, str), pat_args), lexp_to_pexp bch + in Ppatcons ((loc, str), pat_args), lexp_unparse bch ) (SMap.bindings branches) in

let pbranch = match default with - | Some dft -> (Ppatany(loc), lexp_to_pexp dft)::pbranch + | Some dft -> (Ppatany(loc), lexp_unparse dft)::pbranch | None -> pbranch - in Pcase (loc, lexp_to_pexp target, pbranch) + in Pcase (loc, lexp_unparse target, pbranch)

(* | SortLevel of sort_level | Sort of U.location * sort *)

- | _ as e -> Pimm (String(lexp_location e, "Type")) + | _ as e -> Pimm (Symbol(lexp_location e, "Type"))

(* @@ -775,9 +775,8 @@ and _lexp_to_str ctx exp = | Builtin ((_, name), _) -> name

| Sort (_, Stype lvl) -> (match lvl with - | SortLevel (SLn 0) -> "Type" - | SortLevel (SLn v) -> "Type" ^ (string_of_int v) - | _ -> "Type") + | SortLevel (SLn v) -> "Type_" ^ (string_of_int v) + | _ -> "Type_?")

| _ -> print_string "Printing Not Implemented\n"; "-- --"

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -66,7 +66,7 @@ let lexp_warning = msg_warning "LPARSE" let lexp_error = msg_error "LPARSE" let lexp_fatal = msg_fatal "LPARSE"

-let _global_lexp_ctx = ref make_lexp_context +let _global_lexp_ctx = ref make_elab_context let _global_lexp_trace = ref [] let _parsing_internals = ref false let btl_folder = ref "./btl/" @@ -85,7 +85,7 @@ let _type_shift tp i = | Var(v, idx) -> Var(v, idx) | expr -> expr

-let ctx_define (ctx: lexp_context) var lxp ltype = +let ctx_define (ctx: elab_context) var lxp ltype = let (_, cctx, _) = ctx in if OL.conv_p ltype (OL.check cctx lxp) then env_extend ctx var (LetDef lxp) ltype @@ -104,7 +104,7 @@ let ctx_define (ctx: lexp_context) var lxp ltype = (* The main job of lexp (currently) is to determine variable name (index) * and to regroup type specification with their variable * - * lexp_context is composed of two environment: senv and env. + * elab_context is composed of two environment: senv and env. * the senv environment is used to find the correct debruijn index * while the env environment is used to save variable information. * the env environment look a lot like the runtime environment that will be @@ -153,10 +153,10 @@ let mkMetavar () = let meta = Unif.create_metavar () in let name = "__Metavar_" ^ (string_of_int meta) in Metavar (meta, S.Identity, (Util.dummy_location, name))

-let rec lexp_p_infer (p : pexp) (ctx : lexp_context): lexp * ltype = +let rec lexp_p_infer (p : pexp) (ctx : elab_context): lexp * ltype = _lexp_p_infer p ctx 1

-and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = +and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =

let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) in let tloc = pexp_location p in @@ -299,10 +299,10 @@ and lexp_let_decls decls (body: lexp) ctx i = List.fold_left (fun lxp decls -> Let(dloc, decls, lxp)) body decls

-and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp = +and lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context): lexp = _lexp_p_check p t ctx 1

-and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = +and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) i: lexp = let tloc = pexp_location p in

@@ -572,8 +572,14 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =

(* determine function type *) match func, ltp with - (* FIXME: this branch is never used because of missing shift somewhere *) - (* while special form have a type macro this does not recognize them as such *) + (* This is a work around for the bug described below *) + | Pvar(l, name), _ when is_builtin_macro name -> + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx i in + (get_macro_impl loc name) loc largs ctx ltp + + (* FIXME: the branch 'builtin macro' is never used because of missing shift somewhere *) + (* while special forms have a type macro this does not recognize them as such *) | macro, _ when OL.conv_p ltp macro_type -> ( match macro with | Pvar(l, name) when is_builtin_macro name -> @@ -606,7 +612,7 @@ and lexp_get_inductive_type loc ctor_name ctx : (string * lexp option) =

(* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx: - ((string * location * (arg_kind * vdef option) list) * lexp_context) = + ((string * location * (arg_kind * vdef option) list) * elab_context) =

match pattern with | Ppatany (loc) -> (* Catch all expression nothing to do *) @@ -661,7 +667,7 @@ and lexp_read_pattern pattern exp target ctx:

(* Read patterns inside a constructor *) and lexp_read_pattern_args args (args_type : lexp list) ctx: - (((arg_kind * vdef option) list) * lexp_context)= + (((arg_kind * vdef option) list) * elab_context)=

let length_type = List.length args_type in let length_pat = List.length args in @@ -723,7 +729,7 @@ and lexp_parse_inductive ctors ctx i =

(* Macro declaration handling, return a list of declarations * to be processed *) -and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = +and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = (* lookup for mname_ *) let idx = try senv_lookup mname ctx with Not_found -> @@ -865,7 +871,7 @@ and lexp_detect_recursive pdecls = (List.rev !decls)

-and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) = +and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * elab_context) = (* detect mutually recursive def and merge definition *) let decls = lexp_detect_recursive decls in let all = ref [] in @@ -940,7 +946,7 @@ and _lexp_rec_decl decls ctx i = and lexp_decls_toplevel decls ctx = _lexp_decls decls ctx 1

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

let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with @@ -951,7 +957,7 @@ and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = (loop p ctx [])

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

print_string (make_title " LEXP CONTEXT "); @@ -967,7 +973,7 @@ and print_lexp_ctx (ctx : lexp_context) =

(* it is annoying to print according to StringMap order *) (* let's use myers list order *) - let rec extract_names (lst: env_type) acc = + let rec extract_names (lst: lexp_context) acc = match lst with | Mnil-> acc | Mcons (hd, tl, _, _) -> @@ -1057,7 +1063,7 @@ let lexp_parse_all p ctx = _lexp_parse_all p ctx 1 let default_lctx, default_rctx =

(* Empty context *) - let lctx = make_lexp_context in + let lctx = make_elab_context in let lctx = ctx_define lctx (dloc, "Type1") type1 type2 in let lctx = ctx_define lctx (dloc, "Type") type0 type1 in (* FIXME: Add builtins directly here. *) @@ -1103,7 +1109,7 @@ let default_lctx, default_rctx =

(* Lexp helper *) let _lexp_expr_str (str: string) (tenv: token_env) - (grm: grammar) (limit: string option) (ctx: lexp_context) = + (grm: grammar) (limit: string option) (ctx: elab_context) = let pxps = _pexp_expr_str str tenv grm limit in lexp_parse_all pxps ctx

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -41,14 +41,12 @@ let conv_erase = true (* If true, conv ignores erased terms. *)

(* Lexp context *)

-type lexp_context = DB.env_type - -let lookup_type (ctx : lexp_context) vref = +let lookup_type (ctx : DB.lexp_context) vref = let (_, i) = vref in let (_, _, _, t) = Myers.nth i ctx in mkSusp t (S.shift (i + 1))

-let lookup_value (ctx : lexp_context) vref = +let lookup_value (ctx : DB.lexp_context) vref = let (_, i) = vref in match Myers.nth i ctx with | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) @@ -133,7 +131,7 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let rec lexp_whnf e (ctx : lexp_context) meta_ctx = +let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx"); @@ -235,24 +233,19 @@ let rec check ctx e = | Let (_, defs, e) -> let tmp_ctx = List.fold_left (fun ctx (v, e, t) - -> (match check ctx t with - | Sort (_, Stype _) -> () - | _ -> (U.msg_error "TC" (lexp_location t) - "Def type is not a type!"; ())); - Myers.cons (0, Some v, ForwardRef, t) ctx) - ctx defs in - let (new_ctx, _) = - List.fold_left (fun (ctx,recursion_offset) (v, e, t) - -> let t' = check tmp_ctx e in - assert_type e t t'; - (Myers.cons (recursion_offset, Some v, LetDef e, t) ctx, - recursion_offset - 1)) - (ctx, List.length defs) - defs in + -> (match check ctx t with + | Sort (_, Stype _) -> () + | _ -> (U.msg_error "TC" (lexp_location t) + "Def type is not a type!"; ())); + DB.lctx_extend ctx v ForwardRef t) + ctx defs in + let _ = List.iter (fun (v, e, t) -> assert_type e t (check tmp_ctx e)) + defs in + let new_ctx = DB.lctx_extend_rec ctx defs in check new_ctx e | Arrow (ak, v, t1, l, t2) -> (let k1 = check ctx t1 in - let k2 = check (Myers.cons (0, v, Variable, t1) ctx) t2 in + let k2 = check (DB.lexp_ctx_cons ctx 0 v Variable t1) t2 in match k1, k2 with | (Sort (_, s1), Sort (_, s2)) -> Sort (l, sort_compose l s1 s2) @@ -270,7 +263,7 @@ let rec check ctx e = Arrow (ak, Some v, t, l, (* FIXME: If ak is Aerasable, make sure the var only appears * in type annotations. *) - check (Myers.cons (0, Some v, Variable, t) ctx) e)) + check (DB.lctx_extend ctx v Variable t) e)) | Call (f, args) -> let ft = check ctx f in List.fold_left (fun ft (ak,arg) @@ -299,7 +292,7 @@ let rec check ctx e = Arrow (ak, Some v, t, lexp_location t, (* FIXME: `sort_compose` doesn't do what we want! *) arg_loop args (sort_compose l s s') - (Myers.cons (0, Some v, Variable, t) ctx)) in + (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args (Stype (SortLevel (SLn 0))) ctx in (* FIXME: Check cases! *) tct @@ -329,7 +322,8 @@ let rec check ctx e = (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes - -> mkctx (Myers.cons (0, vdef, Variable, mkSusp ftype s) ctx) + -> mkctx (DB.lexp_ctx_cons ctx 0 + vdef Variable (mkSusp ftype s)) (S.cons (Var ((match vdef with Some vd -> vd | None -> (l, "_")), 0)) s)

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -41,161 +41,98 @@ open Env let lctx = default_lctx let rctx = default_rctx

-let _ = (add_test "EVAL" "Variable Cascade" (fun () -> +(* Params: + * decl: declarations to be processed before evaluating + * run : expr to be evaluated + * res : expected result + *) +let test_eval_eqv_named name decl run res = + add_test "EVAL" name (fun () -> reset_eval_trace (); + let rctx, lctx = eval_decl_str decl lctx rctx in

- let dcode = " - a = 10; - b = a; - c = b; - d = c;" in + let erun = eval_expr_str run lctx rctx in (* evaluated run expr *) + let eres = eval_expr_str res lctx rctx in (* evaluated res expr *)

- let rctx, lctx = eval_decl_str dcode lctx rctx in + if value_eq_list erun eres + then success () + else ( + value_print (List.hd erun); + value_print (List.hd eres); + failure ()))

- let ecode = "d;" in +let test_eval_eqv decl run res = test_eval_eqv_named run decl run res

- let ret = eval_expr_str ecode lctx rctx in +let _ = test_eval_eqv "" "2 + 2" "4"

- match ret with - | [Vint(r)] -> expect_equal_int r 10 - | _ -> failure ()) -) +let _ = test_eval_eqv_named + "Variable Cascade"

+ "a = 10; b = a; c = b; d = c;" + + "d" (* == *) "10"

(* Let * ------------------------ *)

-let _ = (add_test "EVAL" "Let" (fun () -> - reset_eval_trace (); +let _ = test_eval_eqv_named + "Let"

- (* Noise. Makes sure the correct variables are selected *) - let dcode = " - c = 3; e = 1; f = 2; d = 4;" in - let rctx, lctx = eval_decl_str dcode lctx rctx in - - let ecode = " - let a = 10; x = 50; y = 60; b = 20; in a + b;" in - - let ret = eval_expr_str ecode lctx rctx in - (* Expect a single result *) - match ret with - | [Vint(r)] -> expect_equal_int r 30 - | _ -> failure ()) -) + "c = 3; e = 1; f = 2; d = 4;"

+ "let a = 10; x = 50; y = 60; b = 20; + in a + b;" (* == *) "30"

(* Lambda * ------------------------ *) -let _ = (add_test "EVAL" "Lambda" (fun () -> - reset_eval_trace ();

- let dcode = " - sqr : Int -> Int; - sqr = lambda x -> x * x; - " in +let _ = test_eval_eqv_named + "Lambda"

- (* Declare lambda *) - let rctx, lctx = eval_decl_str dcode lctx rctx in - - (* Eval defined lambda *) - let ret = eval_expr_str "(sqr 4);" lctx rctx in - (* Expect a single result *) - match ret with - | [Vint(r)] -> expect_equal_int r (4 * 4) - | _ -> failure ()) -) - -let _ = (add_test "EVAL" "Nested Lambda" (fun () -> - reset_eval_trace (); - - let code = " - sqr : Int -> Int; - sqr = lambda x -> x * x; + "sqr : Int -> Int; + sqr = lambda x -> x * x;"

- cube : Int -> Int; - cube = lambda x -> x * (sqr x);" in + "(sqr 4);" (* == *) "16"

- (* Declare lambda *) - let rctx, lctx = eval_decl_str code lctx rctx in - - (* Eval defined lambda *) - let ret = eval_expr_str "(cube 4);" lctx rctx in - (* Expect a single result *) - match ret with - | [Vint(r)] -> expect_equal_int r (4 * 4 * 4) - | _ -> failure ()) -) +let _ = test_eval_eqv_named + "Nested Lambda"

-(* This makes sure contexts are reinitialized between calls - * i.e the context should not grow *) -let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> - reset_eval_trace (); - _typer_verbose := (-1); + "sqr : Int -> Int; + sqr = lambda x -> x * x;

- let code = " - infinity : Int -> Int; - infinity = lambda (beyond : Int) -> (infinity beyond);" in + cube : Int -> Int; + cube = lambda x -> x * (sqr x);"

- let rctx, lctx = eval_decl_str code lctx rctx in + "(cube 4)" (* == *) "64"

- (* Expect throwing *) - try (* use the silent version as an error will be thrown *) - let _ = _eval_expr_str "(infinity 0);" lctx rctx true in - _typer_verbose := 20; - failure () - with - Internal_error m -> ( - _typer_verbose := 20; - if m = "Recursion Depth exceeded" then - success () - else - failure ()) -))

(* Cases + Inductive types * ------------------------ *)

-let _ = (add_test "EVAL" "Inductive::Case" (fun () -> - reset_eval_trace (); +let _ = test_eval_eqv_named + "Inductive::Case"

- (* Inductive type declaration + Noisy declarations *) - let code = " - i = 90; - idt : Type; - idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); - d = 10; - ctr0 = inductive-cons idt ctr0; e = 20; - ctr1 = inductive-cons idt ctr1; f = 30; - ctr2 = inductive-cons idt ctr2; g = 40; - ctr3 = inductive-cons idt ctr3; h = 50; - - a = (ctr1 (ctr2 ctr0)); y = 2; - b = (ctr2 (ctr2 ctr0)); z = 3; - c = (ctr3 (ctr2 ctr0)); w = 4; - - test_fun = lambda (k : idt) -> case k - | ctr1 l => 1 - | ctr2 l => 2 - | _ => 3;" in + "i = 90; + idt : Type; + idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); + d = 10; + ctr0 = inductive-cons idt ctr0; e = 20; + ctr1 = inductive-cons idt ctr1; f = 30; + ctr2 = inductive-cons idt ctr2; g = 40; + ctr3 = inductive-cons idt ctr3; h = 50;

- let rctx, lctx = eval_decl_str code lctx rctx in + a = (ctr1 (ctr2 ctr0)); y = 2; + b = (ctr2 (ctr2 ctr0)); z = 3; + c = (ctr3 (ctr2 ctr0)); w = 4;

- let rcode = "(test_fun a); (test_fun b); (test_fun c)"in + test_fun = lambda (k : idt) -> case k + | ctr1 l => 1 + | ctr2 l => 2 + | _ => 3;"

- (* Eval defined lambda *) - let ret = eval_expr_str rcode lctx rctx in - (* Expect 3 results *) - match ret with - | [Vint(a); Vint(b); Vint(c)] -> - let t1 = expect_equal_int a 1 in - let t2 = expect_equal_int b 2 in - let t3 = expect_equal_int c 3 in - if t1 = 0 && t2 = 0 && t3 = 0 then - success () - else - failure () - | _ -> failure () -)) + "(test_fun a); (test_fun b); (test_fun c)" + + "1; 2; 3"

(* Those wil be used multiple times *) let nat_decl = " @@ -215,165 +152,129 @@ let bool_decl = " false = inductive-cons Bool false; true = inductive-cons Bool true;"

-let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () -> - reset_eval_trace (); +let _ = test_eval_eqv_named + "Inductive::Recursive Call"

- let code = nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two);" in + (nat_decl ^ " + one = (succ zero); + two = (succ one); + three = (succ two);")

- let rctx, lctx = eval_decl_str code lctx rctx in + "(to-num zero); (to-num one); (to-num two);"

- let rcode = "(to-num zero); (to-num one); (to-num two);"in + "0; 1; 2"

- (* Eval defined lambda *) - let ret = eval_expr_str rcode lctx rctx in - (* Expect a 3 results *) - match ret with - | [Vint(a); Vint(b); Vint(c)] -> - let t1 = expect_equal_int a 0 in - let t2 = expect_equal_int b 1 in - let t3 = expect_equal_int c 2 in - if t1 = 0 && t2 = 0 && t3 = 0 then - success () - else - failure () - | _ -> failure ()) -) - -let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> - reset_eval_trace (); +let _ = test_eval_eqv_named + "Inductive::Nat Plus"

- let code = nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two); + (nat_decl ^ " + one = (succ zero); + two = (succ one); + three = (succ two);

- plus : Nat -> Nat -> Nat; - plus = lambda (x : Nat) -> lambda (y : Nat) -> case x - | zero => y - | succ z => succ (plus z y); - " in + plus : Nat -> Nat -> Nat; + plus = lambda (x : Nat) -> lambda (y : Nat) -> case x + | zero => y + | succ z => succ (plus z y);")

- let rctx, lctx = eval_decl_str code lctx rctx in + "to-num (plus zero two); + to-num (plus two zero); + to-num (plus two one);"

- let rcode = " - (to-num (plus zero two)); - (to-num (plus two zero)); - (to-num (plus two one));"in + "2; 2; 3"

- (* Eval defined lambda *) - let ret = eval_expr_str rcode lctx rctx in - (* Expect a 3 results *) - match ret with - | [Vint(a); Vint(b); Vint(c)] -> - let t1 = expect_equal_int a 2 in - let t2 = expect_equal_int b 2 in - let t3 = expect_equal_int c 3 in - if t1 = 0 && t2 = 0 && t3 = 0 then - success () - else - failure () - | _ -> failure () -)) +let _ = test_eval_eqv_named + "Mutually Recursive Definition"

-let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> - reset_eval_trace (); + (nat_decl ^ " + one = (succ zero); + two = (succ one); + three = (succ two);

- let dcode = nat_decl ^ " - one = (succ zero); - two = (succ one); - three = (succ two); + even : Nat -> Int; + odd = lambda (n : Nat) -> case n + | zero => 0 + | succ y => (even y);

- even : Nat -> Int; - odd = lambda (n : Nat) -> case n - | zero => 0 - | succ y => (even y); + even = lambda (n : Nat) -> case n + | zero => 1 + | succ y => (odd y);")

- even = lambda (n : Nat) -> case n - | zero => 1 - | succ y => (odd y);" in + "(odd one); (even one); (odd two); (even two);"

- let rctx, lctx = eval_decl_str dcode lctx rctx in + "1; 0; 0; 1"

- let rcode = "(odd one); (even one); (odd two); (even two);" in

- (* Eval defined lambda *) - let ret = eval_expr_str rcode lctx rctx in - (* Expect a 3 results *) - match ret with - | [Vint(a); Vint(b); Vint(c); Vint(d)] -> - let t1 = expect_equal_int a 1 in - let t2 = expect_equal_int b 0 in - let t3 = expect_equal_int c 0 in - let t4 = expect_equal_int d 1 in - if t1 = 0 && t2 = 0 && t3 = 0 && t4 = 0 then - success () - else - failure () - | _ -> failure () -)) +let _ = test_eval_eqv_named + "Partial Application"

+ "add : Int -> Int -> Int; + add = lambda x y -> (x + y);

-let _ = (add_test "EVAL" "Partial Application" (fun () -> - reset_eval_trace (); + inc : Int -> Int; + inc = (add 1);"

- let dcode = " - add : Int -> Int -> Int; - add = lambda x y -> (x + y); + "(inc 1); (inc 2); (inc 3);"

- inc : Int -> Int; - inc = (add 1);" in + "2; 3; 4"

- let rctx, lctx = eval_decl_str dcode lctx rctx in +(* + * Lists + *) +let _ = test_eval_eqv_named + "Lists"

- let rcode = "(inc 1); (inc 2); (inc 3);" in + "my_list = cons (a := Int) 1 + (cons (a := Int) 2 + (cons (a := Int) 3 + (cons (a := Int) 4 (nil (a := Int)))))"

- (* Eval defined lambda *) - let ret = eval_expr_str rcode lctx rctx in - (* Expect a 3 results *) - match ret with - | [Vint(a); Vint(b); Vint(c)] -> - let t1 = expect_equal_int a 2 in - let t2 = expect_equal_int b 3 in - let t3 = expect_equal_int c 4 in - if t1 = 0 && t2 = 0 && t3 = 0 then - success () - else - failure () - | _ -> failure () -)) + "length (a := Int) my_list; + head (a := Int) my_list; + head (a := Int) (tail (a := Int) my_list)"

+ "4; 1; 2"

-let _ = (add_test "EVAL" "List" (fun () -> - reset_eval_trace (); +(* + * Special forms + *) +let _ = test_eval_eqv "w = 2" "decltype w" "Int" +let _ = test_eval_eqv "w = 2" "declexpr w" "2"

- let dcode = " - my_list = (cons(a := Int) 1 (cons(a := Int) 2 (cons(a := Int) 3 (cons(a := Int) 4 (nil(a := Int)))))); - " in +let attr_decl = " + w = 2; + greater-than = new-attribute (Int -> Bool); + attribute w greater-than (lambda (y : Int) -> True);"

- let rctx, lctx = eval_decl_str dcode lctx rctx in +let _ = test_eval_eqv attr_decl + "has-attribute w greater-than" + "True"

- let rcode = "(length(a := Int) my_list); - (head(a := Int) my_list); - (head(a := Int) (tail(a := Int) my_list));" in +(* This makes sure contexts are reinitialized between calls + * i.e the context should not grow *) +let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> + reset_eval_trace (); + _typer_verbose := (-1);

- (* Eval defined lambda *) - let ret = eval_expr_str rcode lctx rctx in - (* Expect a 3 results *) - match ret with - | [Vint(a); Vint(b); Vint(c)] -> - let t1 = expect_equal_int a 4 in - let t2 = expect_equal_int b 1 in - let t3 = expect_equal_int c 2 in - if t1 = 0 && t2 = 0 && t3 = 0 then - success () - else - failure () - | _ -> failure () -)) + let code = " + infinity : Int -> Int; + infinity = lambda (beyond : Int) -> (infinity beyond);" in

+ let rctx, lctx = eval_decl_str code lctx rctx in + + (* Expect throwing *) + try (* use the silent version as an error will be thrown *) + let _ = _eval_expr_str "(infinity 0);" lctx rctx true in + _typer_verbose := 20; + failure () + with + Internal_error m -> ( + _typer_verbose := 20; + if m = "Recursion Depth exceeded" then + success () + else + failure ()) +))

let _ = (add_test "EVAL" "Monads" (fun () -> reset_eval_trace (); @@ -382,7 +283,6 @@ let _ = (add_test "EVAL" "Monads" (fun () -> c = bind (a := Type) (b := Type) (open "./_build/w_file.txt" "w") (lambda (f : FileHandle) -> write f "Hello2"); - " in

let rctx, lctx = eval_decl_str dcode lctx rctx in @@ -391,30 +291,11 @@ let _ = (add_test "EVAL" "Monads" (fun () ->

(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in - (* Expect a 3 results *) match ret with | [v] -> success () | _ -> failure () ))

-(* -let test_eval_eqv decl run expected_result = - add_test "EVAL" dcode1 (fun () -> - - let rctx, lctx = eval_decl_str decl lctx rctx in - - let result = eval_expr_str rcode lctx rctx - let expected_result = eval_expr_str expected_result lctx rctx - - if sexp_eq_list result expected_result - then success () - else ( - value_print (List.hd s1); - value_print (List.hd s2); - failure ())) - -*) - (* run all tests *) let _ = run_all ()

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