Stefan pushed to branch master at Stefan / Typer

Commits: 7896e300 by Stefan Monnier at 2018-06-21T01:28:09Z Make all variable "names" optional

* src/util.ml (vname): Make the string optional. Change all `vname option` to `vname`.

- - - - -

15 changed files:

- src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/unification.ml - src/util.ml - tests/env_test.ml - tests/unify_test.ml

Changes:

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2017 Free Software Foundation, Inc. + * Copyright (C) 2016-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -95,19 +95,19 @@ let set_predef name lexp (* Builtin types *) let dloc = DB.dloc

-let op_binary t = mkArrow (Aexplicit, None, t, dloc, - mkArrow (Aexplicit, None, t, dloc, t)) +let op_binary t = mkArrow (Aexplicit, (dloc, None), t, dloc, + mkArrow (Aexplicit, (dloc, None), t, dloc, t))

let type_eq = - let lv = (dloc, "l") in - let tv = (dloc, "t") in - mkArrow (Aerasable, Some lv, + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + mkArrow (Aerasable, lv, DB.type_level, dloc, - mkArrow (Aerasable, Some tv, + mkArrow (Aerasable, tv, mkSort (dloc, Stype (Var (lv, 0))), dloc, - mkArrow (Aexplicit, None, + mkArrow (Aexplicit, (dloc, None), Var (tv, 0), dloc, - mkArrow (Aexplicit, None, + mkArrow (Aexplicit, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (Var (lv, 3)))))))

@@ -163,7 +163,8 @@ let register_builtin_csts () = let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in let _ = new_builtin_type - "IO" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) in + "IO" (mkArrow (Aexplicit, (dloc, None), + DB.type0, dloc, DB.type0)) in let _ = new_builtin_type "FileHandle" DB.type0 in let _ = new_builtin_type "Eq" type_eq in ()

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -94,7 +94,7 @@ let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None)

(* easier to debug with type annotations *) -type env_elem = (vname option * varbind * ltype) +type env_elem = (vname * varbind * ltype) type lexp_context = env_elem M.myers

type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) @@ -166,31 +166,24 @@ let lexp_ctx_cons (ctx : lexp_context) d v t = | _ -> true)); M.cons (d, v, t) ctx

-let lctx_extend (ctx : lexp_context) (def: vname option) (v: varbind) (t: lexp) = +let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) = lexp_ctx_cons ctx def v t

let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = - let (loc, name) = def in + let (loc, oname) = def in let (grm, (n, map), env, sl) = ctx in - let nmap = SMap.add name n map in + let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), - lexp_ctx_cons env (Some def) v t, + lexp_ctx_cons env def v t, sl)

-let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t - -let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp) - : elab_context = - match def with - | None -> let (grm, (n, map), lctx, sl) = ectx in - (grm, (n + 1, map), lexp_ctx_cons lctx None v t, sl) - | Some def -> env_extend ectx def v t +let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t

let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = let (ctx, _) = List.fold_left (fun (ctx, recursion_offset) (def, e, t) -> - lexp_ctx_cons ctx (Some def) (LetDef (recursion_offset, e)) t, + lexp_ctx_cons ctx def (LetDef (recursion_offset, e)) t, recursion_offset - 1) (ctx, List.length defs) defs in ctx @@ -198,8 +191,10 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = let (grm, (n, senv), lctx, sl) = ctx in let senv', _ = List.fold_left - (fun (senv, i) ((_, vname), _, _) -> - SMap.add vname i senv, i + 1) + (fun (senv, i) ((_, oname), _, _) -> + (match oname with None -> senv + | Some name -> SMap.add name i senv), + i + 1) (senv, n) defs in (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl)

@@ -236,7 +231,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start = let names = ref [] in for i = start to n do let name = match (M.nth (n - i) lst) with - | (Some (_, name), _, _) -> name + | ((_, Some name), _, _) -> name | _ -> "" in names := name::!names done; !names in @@ -255,14 +250,13 @@ let print_lexp_ctx_n (ctx : lexp_context) start =

try let r, name, exp, tp = match env_lookup_by_index (n - idx - 1) ctx with - | (Some (_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp - | (Some (_, name), _, tp) -> 0, name, None, tp - | (_, _, tp) -> 0, "", None, tp in + | ((_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp + | ((_, name), _, tp) -> 0, name, None, tp in

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

let _ = match exp with @@ -296,11 +290,11 @@ let dump_lexp_ctx (ctx : lexp_context) =

(* generic lookup *) let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = - let ((loc, ename), dbi) = v in + let ((loc, oename), dbi) = v in

try(let ret = (Myers.nth dbi ctx) in - let _ = match ret with - | (Some (_, name), _, _) -> + let _ = match (ret, oename) with + | (((_, Some name), _, _), Some ename) -> (* Check if names match *) if not (ename = name) then (print_lexp_ctx ctx; @@ -314,7 +308,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = ret) with Not_found -> error loc ("DeBruijn index " - ^ string_of_int dbi ^ " of `" ^ ename + ^ string_of_int dbi ^ " of `" ^ maybename oename ^ "` out of bounds!")

@@ -340,8 +334,8 @@ let env_lookup_expr ctx (v : vref): lexp option =

type lct_view = | CVempty - | CVlet of vname option * varbind * ltype * lexp_context - | CVfix of (vname option * lexp * ltype) list * lexp_context + | CVlet of vname * varbind * ltype * lexp_context + | CVfix of (vname * lexp * ltype) list * lexp_context

let rec lctx_view lctx = match lctx with

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -281,10 +281,10 @@ let main () =

(if (get_p_option "lexp-merge-debug") then( List.iter (fun ((l, s), lxp, ltp) -> - lalign_print_string s 20; + lalign_print_string (maybename s) 20; lexp_print ltp; print_string "\n";

- lalign_print_string s 20; + lalign_print_string (maybename s) 20; lexp_print lxp; print_string "\n";

) flexps)); @@ -334,7 +334,7 @@ let main () = let main = (senv_lookup "main" nctx) in

(* get main body *) - let body = (get_rte_variable (Some "main") main rctx) in + let body = (get_rte_variable (dloc, Some "main") main rctx) in

(* eval main *) print_eval_result 1 body

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -60,10 +60,6 @@ module Unif = Unification module OL = Opslexp module EL = Elexp

-(* Shortcut => Create a Var *) -let make_var name index loc = - mkVar (((loc, name), index)) - (* dummies *) let dloc = dummy_location

@@ -124,9 +120,9 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = | _ -> let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with - | None -> lexp_error (lexp_location ltp) ltp - ("`" ^ typestr ^ "` is not a proper type") - | Some (l, name) + | (l, None) -> lexp_error l ltp + ("`" ^ typestr ^ "` is not a proper type") + | (l, Some name) -> lexp_error l ltp ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr) @@ -136,8 +132,8 @@ let elab_check_proper_type (ctx : elab_context) ltp var = with e -> print_string "Exception while checking type `"; lexp_print ltp; (match var with - | None -> () - | Some (_, name) + | (_, None) -> () + | (_, Some name) -> print_string ("` of var `" ^ name ^"`\n")); print_lexp_ctx (ectx_to_lctx ctx); raise e @@ -164,26 +160,26 @@ let elab_check_def (ctx : elab_context) var lxp ltype = ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); raise e) then - elab_check_proper_type ctx ltype (Some var) + elab_check_proper_type ctx ltype var else (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ lexp_string lxp ^ " !: " ^ lexp_string ltype; " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype])

-let ctx_extend (ctx: elab_context) (var : vname option) def ltype = +let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; ectx_extend ctx var def ltype

let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; - env_extend ctx var (LetDef (0, lxp)) ltype + ectx_extend ctx var (LetDef (0, lxp)) ltype

let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in let _ = List.fold_left (fun n (var, lxp, ltp) -> elab_check_proper_type - nctx (push_susp ltp (S.shift n)) (Some var); + nctx (push_susp ltp (S.shift n)) var; n - 1) (List.length decls) decls in @@ -232,21 +228,22 @@ let ctx_define_rec (ctx: elab_context) decls = * definitions. *)

-let newMetavar (ctx : lexp_context) sl l name t= +let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in - mkMetavar (meta, S.Identity, (l, name)) + mkMetavar (meta, S.Identity, name)

let newMetalevel (ctx : lexp_context) sl loc = - newMetavar ctx sl Util.dummy_location "ℓ" type_level + newMetavar ctx sl (loc, Some "ℓ") type_level

let newMetatype (ctx : lexp_context) sl loc - = newMetavar ctx sl loc "τ" (mkSort (loc, Stype (newMetalevel ctx sl loc))) + = newMetavar ctx sl (loc, Some "τ") + (mkSort (loc, Stype (newMetalevel ctx sl loc)))

(* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) let mkDummy_type ctx loc = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc let mkDummy_check ctx loc t = newMetavar (ectx_to_lctx ctx) dummy_scope_level - loc "dummy" t + (loc, None) t let mkDummy_infer ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (mkDummy_check ctx loc t, t) @@ -265,9 +262,10 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | _ -> sexp_error loc "define-operator expects 3 argument"; ctx

-let elab_varref ctx ((loc, name) as id) +let elab_varref ctx (loc, name) = let idx = senv_lookup name ctx in - let lxp = make_var name idx loc in + let id = (loc, Some name) in + let lxp = mkVar (id, idx) in let ltp = env_lookup_type ctx (id, idx) in (lxp, Inferred ltp)

@@ -390,6 +388,9 @@ let generalize (nctx : elab_context) e = wrap (IMap.mem id nes) vname mt'' l e' in loop (IMap.empty) len mfvs

+and elab_p_id ((l,name) : symbol) : vname = + (l, match name with "_" -> None | _ -> Some name) + (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = match se with @@ -440,7 +441,7 @@ and elab_special_form ctx f args ot = sform_dummy_ret ctx loc

(* Make up an argument of type `t` when none is provided. *) -and get_implicit_arg ctx loc name t = +and get_implicit_arg ctx loc oname t = (* lookup default attribute of t. *) (* FIXME: Don't lookup defaults/tactics here. Instead, just always * generate a metavar at this point. The use of defaults/tactics should be @@ -448,7 +449,7 @@ and get_implicit_arg ctx loc name t = match try (* FIXME: We shouldn't hard code as popular a name as `default`. *) let pidx, pname = (senv_lookup "default" ctx), "default" in - let default = Var ((dloc, pname), pidx) in + let default = Var ((dloc, Some pname), pidx) in get_attribute ctx loc [default; t] with Not_found -> None with | Some attr @@ -470,17 +471,15 @@ and get_implicit_arg ctx loc name t =

(* Elaborate the argument *) check lsarg t ctx - | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc name t + | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) + (loc, oname) t

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2) - -> let arg = get_implicit_arg - ctx (lexp_location e) - (Eval.varname v) - t1 in + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) + -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (e, List.rev args), t) in instantiate t [] @@ -510,9 +509,9 @@ and infer_type pexp ectx var = -> (let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with - | None -> lexp_error (lexp_location t) t - ("`" ^ typestr ^ "` is not a proper type") - | Some (l, name) + | (l, None) -> lexp_error l t + ("`" ^ typestr ^ "` is not a proper type") + | (l, Some name) -> lexp_error l t ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr)) @@ -527,10 +526,10 @@ and unify_with_arrow ctx tloc lxp kind var aty = let arg = match aty with | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) tloc | Some laty -> laty in - let nctx = ectx_extend ctx (Some var) Variable arg in + let nctx = ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in - let arrow = mkArrow (kind, Some var, arg, l, body) in + let arrow = mkArrow (kind, var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " @@ -666,39 +665,34 @@ and check_case rtype (loc, target, ppatterns) ctx = -> lexp_error loc lctor "Too many pattern args to the constructor"; make_nctx ctx s [] [] pe acc - | (_, Ppatcons (p, _))::pargs, cargs - -> lexp_error (sexp_location p) lctor - "Nested patterns not supported!"; - make_nctx ctx s pargs cargs pe acc - | (_, (ak, Some (_, fname), fty)::cargs) + | (_, (ak, (_, Some fname), fty)::cargs) when SMap.mem fname pe -> let var = SMap.find fname pe in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in - make_nctx nctx (ssink (maybev var) s) pargs cargs + make_nctx nctx (ssink var s) pargs cargs (SMap.remove fname pe) ((ak, var)::acc) - | ((ef, fpat)::pargs, (ak, _, fty)::cargs) + | ((ef, var)::pargs, (ak, _, fty)::cargs) when (match (ef, ak) with | (Some (_, "_"), _) | (None, Aexplicit) -> true | _ -> false) - -> let var = match fpat with Ppatsym v -> Some v | _ -> None in - let nctx = ctx_extend ctx var Variable (mkSusp fty s) in - make_nctx nctx (ssink (maybev var) s) pargs cargs pe + -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) - | ((Some (l, fname), fpat)::pargs, cargs) - -> let var = match fpat with Ppatsym v -> Some v | _ -> None in - if SMap.mem fname pe then + | ((Some (l, fname), var)::pargs, cargs) + -> if SMap.mem fname pe then sexp_error l ("Duplicate explicit field `" ^ fname ^ "`"); make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs - -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + -> let var = (loc, None) in + let nctx = ctx_extend ctx var Variable (mkSusp fty s) in if ak = Aexplicit then sexp_error loc ("Missing pattern for normal field" - ^ (match fname with Some (_,n) -> " `" ^ n ^ "`" + ^ (match fname with (_, Some n) -> " `" ^ n ^ "`" | _ -> "")); - make_nctx nctx (ssink vdummy s) pargs cargs pe - ((ak, None)::acc) in + make_nctx nctx (ssink var s) pargs cargs pe + ((ak, var)::acc) in let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) @@ -712,15 +706,15 @@ and check_case rtype (loc, target, ppatterns) ctx = in

match pat with - | Ppatany _ -> add_default None - | Ppatsym ((_, name) as var) + | Ppatsym ((_, None) as var) -> add_default var + | Ppatsym ((l, Some name) as var) -> (try let idx = senv_lookup name ctx in match OL.lexp_whnf (mkVar (var, idx)) (ectx_to_lctx ctx) with | Cons _ (* It's indeed a constructor! *) - -> add_branch (Symbol var) [] - | _ -> add_default (Some var) (* A named default branch. *) - with Not_found -> add_default (Some var)) + -> add_branch (Symbol (l, name)) [] + | _ -> add_default var (* A named default branch. *) + with Not_found -> add_default var)

| Ppatcons (pctor, pargs) -> add_branch pctor pargs in

@@ -749,7 +743,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, ltp' with - | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) + | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in let larg = check sarg arg_type ctx in @@ -778,7 +772,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args largs sargs pending ltp

(* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, v, arg_type, _, ret_type) + | _, Arrow ((Aerasable | Aimplicit) as ak, (l,v), arg_type, _, ret_type) (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) @@ -786,8 +780,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = ctx (match sargs with | [] -> loc | sarg::_ -> sexp_location sarg) - (match v with Some (_, name) -> name | _ -> "v") - arg_type in + v arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) | [], _ @@ -808,7 +801,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | Arrow (ak, _, arg_type, _, ret_type) -> assert (ak = Aexplicit); (arg_type, ret_type) | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Aexplicit (dloc, "<anon>") None in + ltp' Aexplicit (dloc, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Aexplicit, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) in @@ -819,8 +812,8 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx =

- let make_args (args:(arg_kind * pvar option * sexp) list) ctx - : (arg_kind * vname option * ltype) list = + let make_args (args:(arg_kind * vname * sexp) list) ctx + : (arg_kind * vname * ltype) list = let nctx = ectx_new_scope ctx in let rec loop args acc ctx = match args with @@ -835,7 +828,7 @@ and lexp_parse_inductive ctors ctx = acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> Arrow (Aerasable, Some vname, t, l, e)) + -> Arrow (Aerasable, vname, t, l, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -845,13 +838,10 @@ and lexp_parse_inductive ctors ctx = | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' - | hd::tl -> begin - match hd with - | (kind, var, exp) -> - let lxp = infer_type exp ctx var in - let nctx = ectx_extend ctx var Variable lxp in - loop tl ((kind, var, lxp)::acc) nctx - end in + | (kind, var, exp)::tl + -> let lxp = infer_type exp ctx var in + let nctx = ectx_extend ctx var Variable lxp in + loop tl ((kind, var, lxp)::acc) nctx in loop args [] nctx in

List.fold_left @@ -868,7 +858,7 @@ and track_fv rctx lctx e = "a bug" else let tfv i = let name = match Myers.nth i rctx with - | (Some n,_) -> n + | ((_, Some n),_) -> n | _ -> "<anon>" in match Myers.nth i lctx with | (_, LetDef (o, e), _) @@ -910,7 +900,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) let args = [macro; BI.o2v_list sargs] in

(* FIXME: Make a proper `Var`. *) - EV.eval_call loc (EL.Var ((DB.dloc, "expand_macro"), 0)) ([], []) + EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) ([], []) macro_expand args

(* Print each generated decls *) @@ -934,7 +924,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp =

and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) - (defs : (vname * sexp) list) + (defs : (symbol * sexp) list) : (vname * lexp * ltype) list * elab_context = (* Preserve the new operators added to nctx. *) let ectx = let (_, a, b, c) = ectx in @@ -942,7 +932,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (grm, a, b, c) in let (declmap, nctx) = List.fold_right - (fun ((_, vname) as v, pexp) (map, nctx) -> + (fun ((l, vname), pexp) (map, nctx) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with @@ -951,24 +941,24 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let e = check pexp adjusted_t nctx in let (grm, ec, lc, sl) = nctx in let d = (v', LetDef (i + 1, e), t) in - (IMap.add i (v, e, t) map, + (IMap.add i ((l, Some vname), e, t) map, (grm, ec, Myers.set_nth i d lc, sl)) | _ -> U.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls

-and infer_and_generalize_type (ctx : elab_context) se oname = +and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in - let t = infer_type se nctx oname in + let t = infer_type se nctx name in match OL.lexp_whnf t (ectx_to_lctx ctx) with (* There's no point generalizing a single metavar, and it's useful * to keep it ungeneralized so we can use `x : ?` to declare that * `x` will be defined later without specifying its type yet. *) | Metavar _ -> t | _ -> let g = generalize nctx t in - g (fun _ne vname t l e - -> mkArrow (Aerasable, Some vname, t, l, e)) + g (fun _ne name t l e + -> mkArrow (Aerasable, name, t, l, e)) t

and infer_and_generalize_def (ctx : elab_context) se = @@ -979,9 +969,9 @@ and infer_and_generalize_def (ctx : elab_context) se = -> mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e)) e in - let t' = g (fun ne vname t l e + let t' = g (fun ne name t l e -> mkArrow ((if ne then Aimplicit else Aerasable), - Some vname, t, sexp_location se, e)) + name, t, sexp_location se, e)) t in (e', t')

@@ -990,7 +980,7 @@ and lexp_decls_1 (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : location SMap.t) (* Pending type decls. *) - (pending_defs : (vname * sexp) list) (* Pending definitions. *) + (pending_defs : (symbol * sexp) list) (* Pending definitions. *) : (vname * lexp * ltype) list * sexp list * elab_context =

match sdecls with @@ -1011,8 +1001,8 @@ and lexp_decls_1 | Node (Symbol (l, "_:_"), args) :: sdecls (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((l, vname) as v); stp] - -> let ltp = infer_and_generalize_type nctx stp (Some v) in + | [Symbol (l, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (l, Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1034,7 +1024,7 @@ and lexp_decls_1 (error l ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) else lexp_decls_1 sdecls ectx - (env_extend nctx v ForwardRef ltp) + (ectx_extend nctx (l, Some vname) ForwardRef ltp) (SMap.add vname l pending_decls) pending_defs | _ -> error l "Invalid type declaration syntax"; @@ -1043,16 +1033,17 @@ and lexp_decls_1 | Node (Symbol (l, "_=_") as head, args) :: sdecls (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((l, vname) as v); sexp] + | [Symbol ((l, vname)); sexp] when SMap.is_empty pending_decls -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) let (lexp, ltp) = infer_and_generalize_def nctx sexp in + let var = (l, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) - [(v, mkSusp lexp (S.shift 1), ltp)], sdecls, - ctx_define nctx v lexp ltp + [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, + ctx_define nctx var lexp ltp

| [Symbol ((l, vname) as v); sexp] -> if SMap.mem vname pending_decls then @@ -1116,7 +1107,7 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp =

and sform_new_attribute ctx loc sargs ot = match sargs with - | [t] -> let ltp = infer_type t ctx None in + | [t] -> let ltp = infer_type t ctx (loc, None) in (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` * is False, for example): Should be a type like `AttributeMap t` * instead. *) @@ -1129,7 +1120,7 @@ and sform_new_attribute ctx loc sargs ot = and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with - | [table; Var((_, name), idx); attr] -> table, (n - idx, name), attr + | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in

let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with @@ -1145,7 +1136,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = and get_attribute ctx loc largs = let ctx_n = get_size ctx in let table, var = match largs with - | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name) + | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in

let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with @@ -1157,7 +1148,8 @@ and get_attribute ctx loc largs =

and sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in - (newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "special-form-error" t, + (newMetavar (ectx_to_lctx ctx) dummy_scope_level + (loc, Some "special-form-error") t, Inferred t)

and sform_get_attribute ctx loc (sargs : sexp list) ot = @@ -1168,7 +1160,7 @@ and sform_get_attribute ctx loc (sargs : sexp list) ot = and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with - | [table; Var((_, name), idx)] -> table, (n - idx, name) + | [table; Var((_, Some name), idx)] -> table, (n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in

let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with @@ -1229,6 +1221,26 @@ let sform_datacons ctx loc sargs ot = | _ -> sexp_error loc "##constr requires two arguments"; sform_dummy_ret ctx loc

+let elab_colon_to_ak k = match k with + | "_:::_" -> Aerasable + | "_::_" -> Aimplicit + | _ -> Aexplicit + +let elab_datacons_arg s = match s with + | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t]) + -> (elab_colon_to_ak k, elab_p_id s, t) + | _ -> (Aexplicit, (sexp_location s, None), s) + +let elab_typecons_arg arg : (arg_kind * vname * sexp option) = + match arg with + | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e]) + -> (elab_colon_to_ak k, + (l, Some name), Some e) + | Symbol (l, name) -> (Aexplicit, (l, Some name), None) + | _ -> sexp_print arg; + (sexp_error (sexp_location arg) "Unrecognized formal arg"); + (Aexplicit, (sexp_location arg, None), None) + let sform_typecons ctx loc sargs ot = match sargs with | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) @@ -1245,7 +1257,7 @@ let sform_typecons ctx loc sargs ot = let rec parse_formals sformals rformals ctx = match sformals with | [] -> (List.rev rformals, ctx) | sformal :: sformals - -> let (kind, var, opxp) = pexp_p_formal_arg sformal in + -> let (kind, var, opxp) = elab_typecons_arg sformal in let ltp = match opxp with | Some pxp -> let (l,_) = infer pxp ctx in l | None -> let (l,_) = var in @@ -1253,7 +1265,7 @@ let sform_typecons ctx loc sargs ot = (ectx_to_scope_level ctx) l in

parse_formals sformals ((kind, var, ltp) :: rformals) - (env_extend ctx var Variable ltp) in + (ectx_extend ctx var Variable ltp) in

let (formals, nctx) = parse_formals formals [] ctx in

@@ -1263,7 +1275,7 @@ let sform_typecons ctx loc sargs ot = -> match case with (* read Constructor name + args => Type ((Symbol * args) list) *) | Node (Symbol s, cases) - -> (s, List.map pexp_p_ind_arg cases)::pcases + -> (s, List.map elab_datacons_arg cases)::pcases (* This is a constructor with no args *) | Symbol s -> (s, [])::pcases

@@ -1277,7 +1289,7 @@ let sform_typecons ctx loc sargs ot =

let sform_hastype ctx loc sargs ot = match sargs with - | [se; st] -> let lt = infer_type st ctx None in + | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; @@ -1287,11 +1299,11 @@ let sform_arrow kind ctx loc sargs ot = match sargs with | [st1; st2] -> let (v, st1) = match st1 with - | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (Some v, st1) - | _ -> (None, st1) in + | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) + | _ -> ((sexp_location st1, None), st1) in let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type st2 nctx None in + let lt2 = infer_type st2 nctx (sexp_location st2, None) in (mkArrow (kind, v, lt1, loc, lt2), Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret ctx loc @@ -1343,14 +1355,14 @@ let sform_identifier ctx loc sargs ot = let subst = S.shift ctx_shift in let (_, _, rmmap) = ectx_get_scope ctx in if not (name = "") && SMap.mem name (!rmmap) then - (mkMetavar (SMap.find name (!rmmap), subst, (loc, name)), Lazy) + (mkMetavar (SMap.find name (!rmmap), subst, (loc, Some name)), Lazy) else let t = match ot with | None -> newMetatype octx sl loc | Some t (* `t` is defined in ctx instead of octx. *) -> Inverse_subst.apply_inv_subst t subst in - let mv = newMetavar octx sl loc name t in + let mv = newMetavar octx sl (loc, Some name) t in (if not (name = "") then let idx = match mv with | Metavar (idx, _, _) -> idx @@ -1379,22 +1391,22 @@ let rec sform_lambda kind ctx loc sargs ot = match sargs with | [sarg; sbody] -> let (arg, ost1) = match sarg with - | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st) - | Symbol arg -> (arg, None) + | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st) + | Symbol arg -> (elab_p_id arg, None) | _ -> sexp_error (sexp_location sarg) "Unrecognized lambda argument"; - ((dummy_location, "_"), None) in + ((dummy_location, None), None) in

let olt1 = match ost1 with - | Some st -> Some (infer_type st ctx (Some arg)) + | Some st -> Some (infer_type st ctx arg) | _ -> None in

let mklam lt1 olt2 = - let nctx = env_extend ctx arg Variable lt1 in + let nctx = ectx_extend ctx arg Variable lt1 in let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2)) + | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2)) | _ -> alt) in

(match ot with @@ -1416,21 +1428,20 @@ let rec sform_lambda kind ctx loc sargs ot = ^ lexp_string lt1 ^ "`")); mklam lt1 (Some lt2)

- | Arrow (ak2, ov, lt1, _, lt2) when kind = Aexplicit + | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit (* `t` is an implicit arrow and `kind` is Aexplicit, * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) - -> let v = var_of_ovar loc ov in - (* FIXME: Here we end up adding a local variable `v` whose + -> (* FIXME: Here we end up adding a local variable `v` whose * name is lot lexically present, so there's a risk of * name capture. We should make those vars anonymous? *) - let nctx = env_extend ctx v Variable lt1 in + let nctx = ectx_extend ctx v Variable lt1 in (* FIXME: Don't go back to sform_lambda, but use an internal * loop to avoid re-computing olt1 each time. *) let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in (mkLambda (ak2, v, lt1, lam), match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, ov, lt1, loc, lt2')) + | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) | _ -> alt)

| lt @@ -1450,7 +1461,7 @@ let rec sform_case ctx loc sargs ot = match sargs with -> (pexp_p_pat pat, code) | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; - (Ppatany l, Symbol (l, "?")) in + (Ppatsym (l, None), Symbol (l, "?")) in let pcases = List.map parse_case scases in let t = match ot with | Some t -> t @@ -1563,7 +1574,7 @@ let default_ectx let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = Var((dloc, name), idx) in + let v = mkVar ((dloc, Some name), idx) in BI.set_predef name v) BI.predef_names; with e -> warning dloc "Predef not found"; in @@ -1572,7 +1583,7 @@ let default_ectx let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx -> if String.get key 0 = '-' then ctx - else ctx_define ctx (dloc, key) e t) + else ctx_define ctx (dloc, Some key) e t) (!BI.lmap) lctx in

(* read base file *) @@ -1600,7 +1611,7 @@ let default_rctx = EV.from_ectx default_ectx (* Lexp helper *) let _lexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) (ctx: elab_context) = - let pxps = _pexp_expr_str str tenv grm limit in + let pxps = _sexp_parse_str str tenv grm limit in let lexps = lexp_parse_all pxps ctx in List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps;

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -48,7 +48,7 @@ type elexp = | Imm of sexp

(* A builtin constant, typically a function implemented in Ocaml. *) - | Builtin of vname + | Builtin of symbol

(* A variable reference, using deBruijn indexing. *) | Var of vref @@ -72,8 +72,8 @@ type elexp = * tests the value of `e`, and either selects the corresponding branch * in `branches` or branches to the `default`. *) | Case of U.location * elexp - * (U.location * (vname option) list * elexp) SMap.t - * (vname option * elexp) option + * (U.location * vname list * elexp) SMap.t + * (vname * elexp) option

(* A Type expression. There's no useful operation we can apply to it, * but they can appear in the code. *) @@ -109,19 +109,19 @@ and elexp_string lxp = let maybe_str lxp = match lxp with | Some (v, lxp) - -> " | " ^ (match v with None -> "_" | Some (_,name) -> name) + -> " | " ^ (match v with (_, None) -> "_" | (_, Some name) -> name) ^ " => " ^ elexp_string lxp | None -> "" in

let str_decls d = List.fold_left (fun str ((_, s), lxp) -> - str ^ " " ^ s ^ " = " ^ (elexp_string lxp)) "" d in + str ^ " " ^ L.maybename s ^ " = " ^ (elexp_string lxp)) "" d in

let str_pat lst = List.fold_left (fun str v -> str ^ " " ^ (match v with - | None -> "_" - | Some (_, s) -> s)) "" lst in + | (_, None) -> "_" + | (_, Some s) -> s)) "" lst in

let str_cases c = SMap.fold (fun key (_, lst, lxp) str -> @@ -135,10 +135,10 @@ and elexp_string lxp = match lxp with | Imm(s) -> sexp_string s | Builtin((_, s)) -> s - | Var((_, s), i) -> s ^ "[" ^ string_of_int i ^ "]" + | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" | Cons((_, s)) -> "datacons(" ^ s ^")"

- | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_string b) + | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)

| Let(_, d, b) -> "let" ^ (str_decls d) ^ " in " ^ (elexp_string b)

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -54,7 +54,7 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of string | Vfloat of float - | Closure of string * elexp * runtime_env + | Closure of vname * elexp * runtime_env | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vundefined @@ -64,7 +64,7 @@ type value_type = | Vcommand of (unit -> value_type)

(* Runtime Environ *) - and runtime_env = (string option * (value_type ref)) M.myers + and runtime_env = (vname * (value_type ref)) M.myers

let rec value_equal a b = match a, b with @@ -134,7 +134,7 @@ let rec value_string v = | Vfloat f -> string_of_float f | Vsexp s -> sexp_string s | Vtype e -> L.lexp_string e - | Closure (s, elexp, _) -> "(lambda " ^ s ^ " -> " ^ (elexp_string elexp) ^ ")" + | Closure ((_, s), elexp, _) -> "(lambda " ^ L.maybename s ^ " -> " ^ (elexp_string elexp) ^ ")" | Vcons ((_, s), lst) -> let args = List.fold_left (fun str v -> str ^ " " ^ value_string v) @@ -147,13 +147,13 @@ let make_runtime_ctx = M.nil

let get_rte_size (ctx: runtime_env): int = M.length ctx

-let get_rte_variable (name: string option) (idx: int) +let get_rte_variable (name: vname) (idx: int) (ctx: runtime_env): value_type = try ( let (defname, ref_cell) = (M.nth idx ctx) in let x = !ref_cell in match (defname, name) with - | (Some n1, Some n2) -> ( + | ((_, Some n1), (_, Some n2)) -> ( if n1 = n2 then x else ( @@ -163,11 +163,11 @@ let get_rte_variable (name: string option) (idx: int)

| _ -> x) with Not_found -> - let n = match name with Some n -> n | None -> "" in + let n = match name with (_, Some n) -> n | _ -> "" in error dloc ("Variable lookup failure. Var: "" ^ n ^ "" idx: " ^ (str_idx idx))

-let add_rte_variable name (x: value_type) (ctx: runtime_env) +let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) : runtime_env = let valcell = ref x in M.cons (name, valcell) ctx @@ -176,7 +176,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = let (n, ref_cell) = (M.nth idx ctx) in

(match (n, name) with - | Some n1, Some n2 + | ((_, Some n1), (_, Some n2)) -> if (n1 != n2) then error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) | _ -> ()); @@ -187,7 +187,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = let nfirst_rte_var n ctx = let rec loop i acc = if i < n then - loop (i + 1) ((get_rte_variable None i ctx)::acc) + loop (i + 1) ((get_rte_variable L.vdummy i ctx)::acc) else List.rev acc in loop 0 [] @@ -214,8 +214,8 @@ let print_rte_ctx_n (ctx: runtime_env) start = let g = !vref in let _ = match n with - | Some m -> lalign_print_string m 12; print_string " | " - | None -> print_string (make_line ' ' 12); print_string " | " in + | (_, Some m) -> lalign_print_string m 12; print_string " | " + | _ -> print_string (make_line ' ' 12); print_string " | " in

value_print g; print_string "\n") start

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -301,7 +301,7 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type | Imm(Float (_, n)) -> Vfloat n | Imm(sxp) -> Vsexp sxp | Cons (label) -> Vcons (label, []) - | Lambda ((_, n), lxp) -> Closure (n, lxp, ctx) + | Lambda (n, lxp) -> Closure (n, lxp, ctx) | Builtin ((_, str)) -> Vbuiltin str

(* Return a value stored in env *) @@ -338,11 +338,11 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type

and eval_var ctx lxp v = - let ((loc, name), idx) = v in - try get_rte_variable (Some name) (idx) ctx + let (name, idx) = v in + try get_rte_variable name idx ctx with e -> - elexp_fatal loc lxp - ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") + elexp_fatal (fst name) lxp + ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ")

(* unef: unevaluated function (to make the trace readable) *) and eval_call loc unef i f args = @@ -355,14 +355,14 @@ and eval_call loc unef i f args =

| Closure (x, e, ctx), v::vs -> let rec bindargs e vs ctx = match (vs, e) with - | (v::vs, Lambda ((_, x), e)) + | (v::vs, Lambda (x, e)) (* "Uncurry" on the fly. *) - -> bindargs e vs (add_rte_variable (Some x) v ctx) + -> bindargs e vs (add_rte_variable x v ctx) | ([], _) -> let trace = append_typer_trace i unef in _eval e ctx trace | _ -> eval_call loc unef i (_eval e ctx i) vs in - bindargs e vs (add_rte_variable (Some x) v ctx) + bindargs e vs (add_rte_variable x v ctx)

| Vbuiltin (name), args -> (try let (builtin, arity) = SMap.find name !builtin_functions in @@ -379,16 +379,16 @@ and eval_call loc unef i f args = else let rec buildctx args ctx = match args with | [] -> ctx - | arg::args -> buildctx args (add_rte_variable None arg ctx) in + | arg::args -> buildctx args (add_rte_variable vdummy arg ctx) in let rec buildargs n = if n >= 0 - then (Var ((loc, "<dummy>"), n))::buildargs (n - 1) + then (Var (vdummy, n))::buildargs (n - 1) else [] in let rec buildbody n = if n > 0 then - Lambda ((loc, "<dummy>"), buildbody (n - 1)) + Lambda (vdummy, buildbody (n - 1)) else Call (Builtin (dloc, name), buildargs (arity - 1)) in - Closure ("<dummy>", + Closure (vdummy, buildbody (arity - nargs - 1), buildctx args Myers.nil)

@@ -400,7 +400,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Aexplicit, Var ((dummy_location, "?"), -1))])) + -> Vtype (L.mkCall (e, [(Aexplicit, Var (vdummy, -1))])) | _ -> value_fatal loc f "Trying to call a non-function!"

and eval_case ctx i loc target pat dflt = @@ -420,9 +420,7 @@ and eval_case ctx i loc target pat dflt = let rec fold2 nctx pats args = match pats, args with | pat::pats, arg::args - -> let nctx = add_rte_variable (match pat with - | Some (_, name) -> Some name - | _ -> None) arg nctx in + -> let nctx = add_rte_variable pat arg nctx in fold2 nctx pats args (* Errors: those should not happen but they might *) (* List.fold2 would complain. we print more info *) @@ -437,8 +435,7 @@ and eval_case ctx i loc target pat dflt = (* Run default *) with Not_found -> (match dflt with | Some (var, lxp) - -> let var' = match var with None -> None | Some (_, n) -> Some n in - _eval lxp (add_rte_variable var' v ctx) i + -> _eval lxp (add_rte_variable var v ctx) i | _ -> error loc "Match Failure")

and build_arg_list args ctx i = @@ -446,7 +443,7 @@ and build_arg_list args ctx i = let arg_val = List.map (fun (k, e) -> _eval e ctx i) args in

(* Add args inside context *) - List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val + List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val

and _eval_decls (decls: (vname * elexp) list) (ctx: runtime_env) i: runtime_env = @@ -454,13 +451,13 @@ and _eval_decls (decls: (vname * elexp) list) let n = (List.length decls) - 1 in

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

- List.iteri (fun idx ((_, name), lxp) -> + List.iteri (fun idx (name, lxp) -> let v = _eval lxp nctx i in let offset = n - idx in - ignore (set_rte_variable offset (Some name) v nctx)) decls; + ignore (set_rte_variable offset name v nctx)) decls;

nctx

@@ -478,7 +475,8 @@ and sexp_dispatch loc depth args = it, ctx_it, flt, ctx_flt, blk, ctx_blk = match args with - + (* FIXME: Don't match against `Closure` to later use `eval`, instead + * pass the value to "funcall". *) | [sxp; Closure(_, nd, ctx_nd); Closure(_, sym, ctx_sym); Closure(_, str, ctx_str); Closure(_, it, ctx_it); Closure(_, flt, ctx_flt); Closure(_, blk, ctx_blk)] -> @@ -493,25 +491,25 @@ and sexp_dispatch loc depth args = match sxp with | Node (op, s) ->( let rctx = ctx_nd in - let rctx = add_rte_variable None (Vsexp(op)) rctx in - let rctx = add_rte_variable None (o2v_list s) rctx in + let rctx = add_rte_variable vdummy (Vsexp(op)) rctx in + let rctx = add_rte_variable vdummy (o2v_list s) rctx in match eval nd rctx with | Closure(_, nd, _) -> eval nd rctx | _ -> error loc "Node has 2 arguments")

| Symbol (_ , s) -> let rctx = ctx_sym in - eval sym (add_rte_variable None (Vstring s) rctx) + eval sym (add_rte_variable vdummy (Vstring s) rctx) | String (_ , s) -> let rctx = ctx_str in - eval str (add_rte_variable None (Vstring s) rctx) + eval str (add_rte_variable vdummy (Vstring s) rctx) | Integer (_ , i) -> let rctx = ctx_it in - eval it (add_rte_variable None (Vinteger (BI.big_int_of_int i)) + eval it (add_rte_variable vdummy (Vinteger (BI.big_int_of_int i)) rctx) | Float (_ , f) -> let rctx = ctx_flt in - eval flt (add_rte_variable None (Vfloat f) rctx) (* + eval flt (add_rte_variable vdummy (Vfloat f) rctx) (* | Block (_ , s, _) -> eval blk (add_rte_variable None (o2v_list s)) *) | _ -> @@ -579,7 +577,7 @@ and print_eval_trace trace = print_trace " EVAL TRACE " trace a

let io_bind loc depth args_val = - let trace_dum = (Var ((loc, "<dummy>"), -1)) in + let trace_dum = (Var ((loc, None), -1)) in

match args_val with | [Vcommand cmd; callback] @@ -608,14 +606,15 @@ let sys_exit loc depth args_val = match args_val with

let y_operator loc depth args = match args with - | [f] -> let aname = "<anon>" in - let yf_ref = ref Vundefined in - let yf = Closure(aname, - Call (Var ((dloc, "f"), 1), - [Var ((dloc, "yf"), 2); - Var ((dloc, aname), 0)]), - Myers.cons (Some "f", ref f) - (Myers.cons (Some "yf", yf_ref) + | [f] -> let yf_ref = ref Vundefined in + let fname = (dloc, Some "f") in + let yfname = (dloc, Some "yf") in + let yf = Closure(vdummy, + Call (Var (fname, 1), + [Var (yfname, 2); + Var (vdummy, 0)]), + Myers.cons (fname, ref f) + (Myers.cons (yfname, yf_ref) Myers.nil)) in yf_ref := yf; yf @@ -690,12 +689,6 @@ let eval_all lxps rctx silent = List.map (fun g -> evalfun g rctx) lxps

-let varname s = match s with Some (_, v) -> v | _ -> "<anon>" - -let roname loname = (match (loname : symbol option) with - | Some (_, name) -> Some name - | _ -> None) - module CMap (* Memoization table. FIXME: Ideally the keys should be "weak", but * I haven't found any such functionality in OCaml's libs. *) @@ -721,7 +714,7 @@ let from_lctx (lctx: lexp_context): runtime_env = | CVempty -> Myers.nil | CVlet (loname, def, _, lctx) -> let rctx = from_lctx lctx in - Myers.cons (roname loname, + Myers.cons (loname, ref (match def with | LetDef (_, e) -> let e = L.clean e in @@ -740,7 +733,7 @@ let from_lctx (lctx: lexp_context): runtime_env = let (nrctx, evs, alldefs) = List.fold_left (fun (rctx, evs, alldefs) (loname, e, _) -> let rc = ref Vundefined in - let nrctx = Myers.cons (roname loname, rc) rctx in + let nrctx = Myers.cons (loname, rc) rctx in (nrctx, (e, rc)::evs, alldefs)) (rctx, [], true) defs in let _ =

===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution

-Copyright (C) 2016-2017 Free Software Foundation, Inc. +Copyright (C) 2016-2018 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -92,7 +92,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - Lexp.mkVar ((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx) + Lexp.mkVar ((U.dummy_location, None), idx)

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -270,7 +270,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with mkLet (l, ndefs, apply_inv_subst e s') | Arrow (ak, v, t1, l, t2) -> mkArrow (ak, v, apply_inv_subst t1 s, l, - apply_inv_subst t2 (ssink (maybev v) s)) + apply_inv_subst t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) | Call (f, args) @@ -285,7 +285,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink (maybev v) s, + -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs)) (s, []) args in @@ -297,13 +297,13 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink (maybev ov) s) + (fun s (_,ov) -> ssink ov s) s cargs in (l, cargs, apply_inv_subst e s')) cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink (maybev v) s))) + | Some (v,e) -> Some (v, apply_inv_subst e (ssink v s))) | Metavar (id, s', name) -> match metavar_lookup id with | MVal e -> apply_inv_subst (push_susp e s') s

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -64,22 +64,22 @@ type ltype = lexp | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort - | Builtin of vname * ltype * lexp AttributeMap.t option + | Builtin of symbol * ltype * lexp AttributeMap.t option | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname option * ltype * U.location * lexp + | Arrow of arg_kind * vname * ltype * U.location * lexp | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of U.location * label * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname option * ltype) list) SMap.t + * ((arg_kind * vname * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname option) list * lexp) SMap.t - * (vname option * lexp) option (* Default. *) + * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (vname * lexp) option (* Default. *) (* The `subst` only applies to the lexp associated * with the metavar's "value", not to the ltype. *) | Metavar of meta_id * subst * vname @@ -205,10 +205,6 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es))

-let var_of_ovar l ov = match ov with - | None -> (l, "<anon>") - | Some v -> v - (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -257,8 +253,9 @@ let rec lexp_location e =

(********* Normalizing a term *********)

-let vdummy = (U.dummy_location, "<anon>") -let maybev mv = match mv with None -> vdummy | Some v -> v +let vdummy = (U.dummy_location, None) +let maybename n = match n with None -> "<anon>" | Some v -> v +let sname (l,n) = (l, maybename n)

let rec push_susp e s = (* Push a suspension one level down. *) match e with @@ -278,7 +275,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in mkLet (l, loop s defs, mkSusp e s') | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s)) + -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) | Call (f, args) -> mkCall (mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) @@ -290,7 +287,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink (maybev v) s, + -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) (s, []) args in @@ -302,13 +299,13 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> mkCase (l, mkSusp e s, mkSusp ret s, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink (maybev ov) s) + (fun s (_,ov) -> ssink ov s) s cargs in (l, cargs, mkSusp e s')) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s))) + | Some (v,e) -> Some (v, mkSusp e (ssink v s))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -342,7 +339,7 @@ let clean e = (s, []) defs in mkLet (l, ndefs, clean s' e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, clean s t1, l, clean (ssink (maybev v) s) t2) + -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) | Call (f, args) -> mkCall (clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) @@ -354,7 +351,7 @@ let clean e = let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink (maybev v) s, + -> (ssink v s, (ak, v, clean s t) :: nargs)) (s, []) args in @@ -366,13 +363,13 @@ let clean e = -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink (maybev ov) s) + (fun s (_,ov) -> ssink ov s) s cargs in (l, cargs, clean s' e)) cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink (maybev v) s) e)) + | Some (v,e) -> Some (v, clean (ssink v s) e)) | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) @@ -392,7 +389,8 @@ let rec lexp_unparse lxp = | Susp _ as e -> lexp_unparse (nosusp e) | Imm (sexp) -> sexp | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) - | Var ((loc, name), _) -> Symbol (loc, name) + (* FIXME: Add a Sexp syntax for debindex references. *) + | Var ((loc, name), _) -> Symbol (loc, maybename name) | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) @@ -403,16 +401,16 @@ let rec lexp_unparse lxp = | Aexplicit -> "lambda_->_" | Aimplicit -> "lambda_=>_" | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol vdef; st]); + [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body]) - | Arrow (arg_kind, vdef, ltp1, loc, ltp2) + | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) -> let ut1 = lexp_unparse ltp1 in Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), - [(match vdef with None -> ut1 - | Some v -> Node (Symbol (loc, "_:_"), - [Symbol v; ut1])); + [(match oname with None -> ut1 + | Some v -> Node (Symbol (l, "_:_"), + [Symbol (l,v); ut1])); lexp_unparse ltp2])

| Let (loc, ldecls, body) @@ -420,9 +418,9 @@ let rec lexp_unparse lxp = let sdecls = List.fold_left (fun acc (vdef, lxp, ltp) -> Node (Symbol (U.dummy_location, "_=_"), - [Symbol vdef; lexp_unparse ltp]) + [Symbol (sname vdef); lexp_unparse ltp]) :: Node (Symbol (U.dummy_location, "_=_"), - [Symbol vdef; lexp_unparse lxp]) + [Symbol (sname vdef); lexp_unparse lxp]) :: acc) [] ldecls in Node (Symbol (loc, "let_in_"), @@ -437,7 +435,7 @@ let rec lexp_unparse lxp = (* (arg_kind * vdef * ltype) list *) (* (arg_kind * pvar * pexp option) list *) let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, vdef, Some (lexp_unparse ltp))) lfargs in + (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in

Node (stypecons, Node (Symbol label, List.map pexp_u_formal_arg pfargs) @@ -447,9 +445,9 @@ let rec lexp_unparse lxp = List.map (fun arg -> match arg with - | (Aexplicit, None, t) -> lexp_unparse t + | (Aexplicit, (_,None), t) -> lexp_unparse t | (ak, s, t) - -> let (l,_) as id = pexp_u_id s in + -> let (l,_) as id = sname s in Node (Symbol (l, match ak with | Aexplicit -> "_:_" | Aimplicit -> "_::_" @@ -462,13 +460,13 @@ let rec lexp_unparse lxp = let bt = lexp_unparse bltp in let pbranch = List.map (fun (str, (loc, args, bch)) -> match args with - | [] -> Ppatsym (loc, str), lexp_unparse bch + | [] -> Ppatsym (loc, Some str), lexp_unparse bch | _ -> let pat_args - = List.map (fun (kind, vdef) - -> match vdef with - | Some vdef -> Some vdef, Ppatsym vdef - | None -> None, Ppatany loc) + = List.map (fun (kind, ((l,oname) as name)) + -> match oname with + | Some vdef -> (Some (l,vdef), name) + | None -> (None, name)) args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) @@ -479,9 +477,7 @@ let rec lexp_unparse lxp = ) (SMap.bindings branches) in

let pbranch = match default with - | Some (v,dft) -> ((match v with - | None -> Ppatany loc - | Some vdef -> Ppatsym vdef), + | Some (v,dft) -> (Ppatsym v, lexp_unparse dft)::pbranch | None -> pbranch in let e = lexp_unparse target in @@ -494,7 +490,7 @@ let rec lexp_unparse lxp =

(* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name)) - -> Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx + -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]")

| SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") @@ -630,7 +626,7 @@ let rec get_precedence expr ctx = | Call (exp, _) -> get_precedence exp ctx | Builtin ((_, name), _, _) when is_binary_op name -> lkp (get_binary_op_name name) - | Var ((_, name), _) when is_binary_op name -> + | Var ((_, Some name), _) when is_binary_op name -> lkp (get_binary_op_name name) | _ -> None, None

@@ -689,7 +685,7 @@ and _lexp_str ctx (exp : lexp) : string =

let get_name fname = match fname with | Builtin ((_, name), _, _) -> name, 0 - | Var((_, name), idx) -> name, idx + | Var((_, Some name), idx) -> name, idx | Lambda _ -> "__", 0 | Cons _ -> "__", 0 | _ -> "__", -1 in @@ -703,7 +699,7 @@ and _lexp_str ctx (exp : lexp) : string =

| Susp (e, s) -> _lexp_str ctx (push_susp e s)

- | Var ((loc, name), idx) -> name ^ (index idx) ; + | Var ((loc, name), idx) -> maybename name ^ (index idx) ;

| Metavar (idx, subst, (loc, name)) (* print metavar result if any *) @@ -715,7 +711,7 @@ and _lexp_str ctx (exp : lexp) : string = | None -> print_meta exp | Some e when e != exp -> print_meta exp | _ -> - "?" ^ name ^ (subst_string subst) ^ (index idx)) + "?" ^ maybename name ^ (subst_string subst) ^ (index idx))

| Let (_, decls, body) -> (* Print first decls without indent *) @@ -736,16 +732,16 @@ and _lexp_str ctx (exp : lexp) : string = (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body)

- | Arrow(k, Some (_, name), tp, loc, expr) -> + | Arrow(k, (_, Some name), tp, loc, expr) -> "(" ^ name ^ " : " ^ (lexp_str tp) ^ ") " ^ (kind_str k) ^ " " ^ (lexp_str expr)

- | Arrow(k, None, tp, loc, expr) -> + | Arrow(k, (_, None), tp, loc, expr) -> "(" ^ (lexp_str tp) ^ " " ^ (kind_str k) ^ " " ^ (lexp_str expr) ^ ")"

| Lambda(k, (loc, name), ltype, lbody) -> - let arg = "(" ^ name ^ " : " ^ (lexp_str ltype) ^ ")" in + let arg = "(" ^ maybename name ^ " : " ^ (lexp_str ltype) ^ ")" in

(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ (make_indent 1) ^ (lexp_stri 1 lbody) @@ -780,7 +776,7 @@ and _lexp_str ctx (exp : lexp) : string = -> let args_str = List.fold_left (fun str (arg_kind, (_, name), ltype) - -> str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " + -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " ^ (lexp_str ltype) ^ ")") "" args in

@@ -792,8 +788,8 @@ and _lexp_str ctx (exp : lexp) : string = let arg_str arg = List.fold_left (fun str v -> match v with - | (_ ,None) -> str ^ " _" - | (_, Some (_, n)) -> str ^ " " ^ n) + | (_, (_, None)) -> str ^ " _" + | (_, (_, Some n)) -> str ^ " " ^ n) "" arg in

let str = SMap.fold (fun k (_, arg, exp) str -> @@ -805,7 +801,8 @@ and _lexp_str ctx (exp : lexp) : string = | None -> str | Some (v, df) -> str ^ nl ^ (make_indent 1) - ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name) + ^ "| " ^ (match v with (_, None) -> "_" + | (_, Some name) -> name) ^ " => " ^ (lexp_stri 1 df))

| Builtin ((_, name), _, _) -> "##" ^ name @@ -845,7 +842,8 @@ and _lexp_str_decls ctx decls =

let ret = List.fold_left (fun str ((_, name), lxp, ltp) - -> let str = if pp_type ctx then (type_str name ltp)::str else str in + -> let name = maybename name in + let str = if pp_type ctx then (type_str name ltp)::str else str in (name ^ " = " ^ (lexp_str lxp) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -79,19 +79,17 @@ let rec lctx_to_subst lctx = | DB.CVlet (_, LetDef (_, e), _, lctx) -> let s = lctx_to_subst lctx in L.scompose (S.substitute e) s - | DB.CVlet (ov, _, _, lctx) + | DB.CVlet (v, _, _, lctx) -> let s = lctx_to_subst lctx in (* Here we decide to keep those vars in the target domain. * Another option would be to map them to `L.impossible`, * hence making the target domain be empty (i.e. making the substitution * generate closed results). *) - L.ssink (maybev ov) s + L.ssink v s | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in let s2 = lexp_defs_subst DB.dloc S.identity - (List.map (fun (oname, e, t) - -> (maybev oname, e, t)) - (List.rev defs)) in + (List.rev defs) in L.scompose s2 s1

(* Take an expression `e` that is "closed" relatively to context lctx @@ -246,7 +244,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = t12 t22 | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) - && conv_p' (DB.lexp_ctx_cons ctx (Some l1) Variable t1) + && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs') e1 e2 | (Call (f1, args1), Call (f2, args2)) @@ -275,7 +273,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = SMap.equal (conv_fields ctx vs) cases1 cases2 | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx (Some l1) Variable t1) + && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs) args1 args2 | _,_ -> false in @@ -422,10 +420,10 @@ let rec check' erased ctx e = (* FIXME: Check the attributemap as well! *) t (* FIXME: Check recursive references. *) - | Var (((_, name), idx) as v) + | Var (((l, name), idx) as v) -> if DB.set_mem idx erased then - U.msg_error "TC" (lexp_location e) - ("Var `" ^ name ^ "`" + U.msg_error "TC" l + ("Var `" ^ maybename name ^ "`" ^ " can't be used here, because it's `erasable`"); lookup_type ctx v | Susp (e, s) -> check erased ctx (push_susp e s) @@ -433,7 +431,7 @@ let rec check' erased ctx e = -> let _ = List.fold_left (fun ctx (v, e, t) -> (let _ = check_type DB.set_empty ctx t in - DB.lctx_extend ctx (Some v) ForwardRef t)) + DB.lctx_extend ctx v ForwardRef t)) ctx defs in (* FIXME: Allow erasable let-bindings! *) let nerased = DB.set_sink (List.length defs) erased in @@ -466,9 +464,9 @@ let rec check' erased ctx e = mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in - mkArrow (ak, Some v, t, l, + mkArrow (ak, v, t, l, check (dbset_push ak erased) - (DB.lctx_extend ctx (Some v) Variable t) + (DB.lctx_extend ctx v Variable t) e)) | Call (f, args) -> let ft = check erased ctx f in @@ -526,8 +524,8 @@ let rec check' erased ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in - mkArrow (ak, Some v, t, lexp_location t, - arg_loop (DB.lctx_extend ctx (Some v) Variable t) + mkArrow (ak, v, t, lexp_location t, + arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in let tct = arg_loop ctx erased args in @@ -562,9 +560,7 @@ let rec check' erased ctx e = | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (S.cons (Var ((match vdef with Some vd -> vd - | None -> (l, "_")), - 0)) + (S.cons (Var (vdef, 0)) (S.mkShift s 1)) vdefs fieldtypes | _,_ -> (U.msg_error "TC" l @@ -611,7 +607,7 @@ let rec check' erased ctx e = match fargs with | [] -> fieldargs fieldtypes | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, Some vd, atype, l, + -> mkArrow (P.Aerasable, vd, atype, l, buildtype fargs) in buildtype fargs with Not_found @@ -773,8 +769,8 @@ let rec get_type ctx e = | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) - -> (mkArrow (ak, Some v, t, l, - get_type (DB.lctx_extend ctx (Some v) Variable t) + -> (mkArrow (ak, v, t, l, + get_type (DB.lctx_extend ctx v Variable t) e)) | Call (f, args) -> let ft = get_type ctx f in @@ -814,8 +810,8 @@ let rec get_type ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (ak, Some v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in + -> mkArrow (ak, v, t, lexp_location t, + arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) -> ret @@ -841,7 +837,7 @@ let rec get_type ctx e = match fargs with | [] -> fieldargs fieldtypes | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, Some vd, atype, l, + -> mkArrow (P.Aerasable, vd, atype, l, buildtype fargs) in buildtype fargs with Not_found -> DB.type_int) @@ -958,20 +954,21 @@ let ctx2tup ctx nctx = types) SMap.empty), cons_label), - List.map (fun (oname, t) - -> (P.Aimplicit, Var (maybev oname, offset))) + List.map (fun (name, t) + -> (P.Aimplicit, Var (name, offset))) types) - | (DB.CVlet (oname, LetDef (_, e), t, _) :: blocs) - -> Let (loc, [(maybev oname, mkSusp e (S.shift 1), t)], - mk_lets_and_tup blocs ((oname, t) :: types)) + | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) + -> Let (loc, [(name, mkSusp e (S.shift 1), t)], + mk_lets_and_tup blocs ((name, t) :: types)) | (DB.CVfix (defs, _) :: blocs) - -> Let (loc, List.map (fun (oname, e, t) -> (maybev oname, e, t)) defs, + -> Let (loc, defs, mk_lets_and_tup blocs (List.append (List.rev (List.map (fun (oname, _, t) -> (oname, t)) defs)) - types)) in + types)) + | _ -> assert false in mk_lets_and_tup (get_blocs nctx []) []

(* opslexp.ml ends here. *)

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -1,6 +1,6 @@ (* pexp.ml --- Proto lambda-expressions, half-way between Sexp and Lexp.

-Copyright (C) 2011-2017 Free Software Foundation, Inc. +Copyright (C) 2011-2018 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -37,31 +37,14 @@ type pvar = symbol (* type tag = string *)

type ppat = - (* This data type allows nested patterns, but in reality we don't - * support them. I.e. we don't want Ppatcons within Ppatcons. *) - | Ppatany of location - | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *) - | Ppatcons of sexp * (symbol option * ppat) list - -let rec pexp_pat_location e = match e with - | Ppatany l -> l + | Ppatsym of vname (* A named default pattern, or a 0-ary constructor. *) + | Ppatcons of sexp * (symbol option * vname) list + +let pexp_pat_location e = match e with | Ppatsym (l,_) -> l | Ppatcons (e, _) -> sexp_location e

-and pexp_p_formal_arg arg : (arg_kind * pvar * sexp option) = - match arg with - | Node (Symbol (_, "_:::_"), [Symbol s; e]) - -> (Aerasable, s, Some e) - | Node (Symbol (_, "_::_"), [Symbol s; e]) - -> (Aimplicit, s, Some e) - | Node (Symbol (_, "_:_"), [Symbol s; e]) - -> (Aexplicit, s, Some e) - | Symbol s -> (Aexplicit, s, None) - | _ -> sexp_print arg; - (pexp_error (sexp_location arg) "Unrecognized formal arg"); - (Aexplicit, (sexp_location arg, "{arg}"), None) - -and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = +let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with | (Aexplicit, s, None) -> Symbol s | (ak, ((l,_) as s), t) @@ -71,62 +54,29 @@ and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = [Symbol s; match t with Some e -> e | None -> Symbol (l, "_")])

-and pexp_p_id (x : location * string) : (location * string) option = - match x with - | (_, "_") -> None - | _ -> Some x - -and pexp_u_id (x : (location * string) option) : (location * string) = - match x with - | None -> (dummy_location, "_") - | Some x -> x - -and pexp_p_ind_arg s = match s with - | Node (Symbol (_,"_:_"), [Symbol s; t]) - -> (Aexplicit, pexp_p_id s, t) - | Node (Symbol (_,"_::_"), [Symbol s; t]) - -> (Aimplicit, pexp_p_id s, t) - | Node (Symbol (_,"_:::_"), [Symbol s; t]) - -> (Aerasable, pexp_p_id s, t) - | _ -> (Aexplicit, None, s) - -and pexp_p_pat_arg (s : sexp) = match s with - | Symbol _ -> (None, pexp_p_pat s) - | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s]) - -> (Some f, Ppatsym s) +let pexp_p_pat_arg (s : sexp) = match s with + | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n)) + | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)]) + -> (Some f, (l, Some n)) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; - (None, Ppatany loc) + (None, (loc, None))

-and pexp_u_pat_arg (arg : symbol option * ppat) : sexp = - match arg with - | (None, p) -> pexp_u_pat p - | (Some ((l,_) as n), p) -> - Node (Symbol (l, "_:=_"), - (* FIXME: the label is wrong! *) - [Symbol (pexp_u_id (Some n)); pexp_u_pat p]) - -and pexp_p_pat (s : sexp) : ppat = match s with - | Symbol (l, "_") -> Ppatany l - | Symbol s -> Ppatsym s +let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = + let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in + match okn with + | None -> pname + | Some ((l,_) as n) -> + Node (Symbol (l, "_:=_"), [Symbol n; pname]) + +let pexp_p_pat (s : sexp) : ppat = match s with + | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n) | Node (c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in - pexp_error l "Unknown pattern"; Ppatany l + pexp_error l "Unknown pattern"; Ppatsym (l, None)

-and pexp_u_pat (p : ppat) : sexp = match p with - | Ppatany l -> Symbol (l, "_") - | Ppatsym s -> Symbol s +let pexp_u_pat (p : ppat) : sexp = match p with + | Ppatsym (l, None) -> Symbol (l, "_") + | Ppatsym (l, Some n) -> Symbol (l, n) | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args) - -(* String Parsing - * --------------------------------------------------------- *) - -(* Lexp helper *) -let _pexp_expr_str (str: string) (tenv: token_env) - (grm: grammar) (limit: string option) = - _sexp_parse_str str tenv grm limit - -(* specialized version *) -let pexp_expr_str str = - _pexp_expr_str str default_stt default_grammar (Some ";")

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -194,7 +194,7 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = -> if var_kind1 = var_kind2 then unify_and (unify' ltype1 ltype2 ctx vs) (unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx (Some v1) Variable ltype1) + (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else None | ((Lambda _, Var _)

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -1,6 +1,6 @@ (* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-

-Copyright (C) 2011-2017 Free Software Foundation, Inc. +Copyright (C) 2011-2018 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -33,7 +33,7 @@ let dummy_location = {file=""; line=0; column=0} (* Occurrence of a variable's symbol: we use DeBruijn index, and for * debugging purposes, we remember the name that was used in the source * code. *) -type vname = location * string +type vname = location * string option type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *)

===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -45,18 +45,19 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> if 10 <= (!_global_verbose_lvl) then (

let var = [ - ((Some "a"), DB.type_int, (make_val "a")); - ((Some "b"), DB.type_int, (make_val "b")); - ((Some "c"), DB.type_int, (make_val "c")); - ((Some "d"), DB.type_int, (make_val "d")); - ((Some "e"), DB.type_int, (make_val "e")); + ((dloc, Some "a"), DB.type_int, (make_val "a")); + ((dloc, Some "b"), DB.type_int, (make_val "b")); + ((dloc, Some "c"), DB.type_int, (make_val "c")); + ((dloc, Some "d"), DB.type_int, (make_val "d")); + ((dloc, Some "e"), DB.type_int, (make_val "e")); ] in

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

- let rctx = List.fold_left (fun ctx (n, t, _) -> - add_rte_variable n Vundefined ctx) - rctx var in + let rctx = List.fold_left + (fun ctx (n, t, _) -> + add_rte_variable n Vundefined ctx) + rctx var in

print_rte_ctx rctx;

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -1,6 +1,6 @@ (* unify_test.ml --- Test the unification algorithm * - * Copyright (C) 2016-2017 Free Software Foundation, Inc. + * Copyright (C) 2016-2018 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle tiv.crb@gmail.com * @@ -126,12 +126,12 @@ let input_type_t = generate_ltype_from_str str_type2 let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

( Lambda ((Aexplicit), - (Util.dummy_location, "L1"), - Var((Util.dummy_location, "z"), 3), + (Util.dummy_location, Some "L1"), + Var((Util.dummy_location, Some "z"), 3), Imm (Integer (Util.dummy_location, 3))), Lambda ((Aexplicit), - (Util.dummy_location, "L2"), - Var((Util.dummy_location, "z"), 4), + (Util.dummy_location, Some "L2"), + Var((Util.dummy_location, Some "z"), 4), Imm (Integer (Util.dummy_location, 3))), Nothing )

::(input_induct , input_induct , Equivalent) (* 2 *) @@ -183,8 +183,8 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

::(input_type , input_type_t , Equivalent) (* 44 *)

- ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), - Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *) + ::(Metavar (0, S.Identity, (Util.dummy_location, Some "M")), + Var ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *)

::[]

View it on GitLab: https://gitlab.com/monnier/typer/commit/7896e300745bccf30ff3514672b43f9a3694...