[Typer] [Git][monnier/typer][unification] 13 commits: misc

Stefan pushed to branch unification at Stefan / Typer

Commits: 6cdee9a8 by Pierre Delaunay at 2016-09-29T00:40:07-04:00 misc

- - - - - e244e3f3 by Pierre Delaunay at 2016-09-29T01:36:19-04:00 Merged

- - - - - 3a5fadd4 by Pierre Delaunay at 2016-09-29T11:49:27-04:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - ba2917e2 by Pierre Delaunay at 2016-09-29T11:50:04-04:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - a37dc44c by Pierre Delaunay at 2016-10-02T02:10:13-04:00 misc

- - - - - 145906d2 by Pierre Delaunay at 2016-10-02T02:10:21-04:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - 6ebf2b5f by Pierre Delaunay at 2016-10-02T02:23:58-04:00 misc

- - - - - 74435fef by Pierre Delaunay at 2016-10-05T19:17:45-04:00 * src/eval.ml, src/lparse.ml, src/elexp.ml Added new functions - (lexp_debug_message) - (elexp_debug_message) - (value_debug_message) which prints the type name followed by a value print and an exception. That code was runduntant in a lot of area

* src/lparse.ml New function: - (lexp_expand_macro) Expand a macro given a Lexp.Call (Macro_ fun) This can be used for standard macro as well as for macro declarations. Updated how macro and macro declarations are handled

- - - - - 894dd057 by Stefan Monnier at 2016-10-05T22:36:27-04:00 * src/lparse.ml (lexp_decls_1): Fix inf-loop on structural equality

- - - - - b09b7491 by Pierre Delaunay at 2016-10-05T22:54:29-04:00 * src/lparse.ml - added "add-attribute" implementation that was removed during debugging

- - - - - 53c41e25 by Stefan Monnier at 2016-10-05T23:16:26-04:00 Fix some context and whnf handling in `check`.

* src/debruijn.ml (lctx_extend): Change vdef arg to be an option.

* src/lparse.ml (lexp_decls_1): Fix inf-loop on structural equality. (elab_check_def): Add debug output. Don't call conv_p. (ctx_define_rec): Do check that it's properly typed.

* src/opslexp.ml (check) <Let>, <Lambda>, <Case>: Call lexp_whnf. (check) <Inductive>: Fix context computation for fields.

- - - - - e612a4c9 by Pierre Delaunay at 2016-10-06T15:38:31-04:00 Unified function name. (There were a lot of inconsistency)

* To retrieve the string representation of a tree node use: pretoken_string/sexp_string/pexp_string/lexp_string/elexp_string/value_string

* To retrieve the tree node name use: pretoken_name/sexp_name/pexp_name/lexp_name/elexp_name/value_name

- - - - - 834fd729 by Stefan Monnier at 2016-10-07T18:28:13-04:00 Merge branch 'trunk' into unification

- - - - -

16 changed files:

- btl/types.typer - samples/inductive.typer - − samples/int_index_inconsistency.typer - src/debruijn.ml - src/debug.ml - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - tests/eval_test.ml

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -104,7 +104,6 @@ node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); integer_ = Built-in "integer_" (Int -> Sexp); float_ = Built-in "float_" (Float -> Sexp);

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

===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -97,6 +97,7 @@ type Either t1 t2 | either-first t1 | either-second t2;

+ type Pair t1 t2 | pair t1 t2;

@@ -119,4 +120,4 @@ get-y p = case p | point x y => y; % Nat : Type; % Nat = inductive_ (Nat) (succ Nat) (zero); % zero = inductive-cons Nat zero; -% succ = inductive-cons Nat succ; \ No newline at end of file +% succ = inductive-cons Nat succ;

===================================== samples/int_index_inconsistency.typer deleted ===================================== --- a/samples/int_index_inconsistency.typer +++ /dev/null @@ -1,10 +0,0 @@ -% -% Int index inconsistency -% ------------------------------ -sqr = lambda (x : Int) -> x * x; -v = sqr 2; - -sqr2 : Int -> Int; -sqr2 = lambda x -> x * x; - -v2 = sqr2 2;

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -117,8 +117,8 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = || 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 lctx_extend (ctx : lexp_context) (def: vdef option) (v: varbind) (t: lexp) = + lexp_ctx_cons ctx 0 def v t

let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in @@ -268,6 +268,8 @@ let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = let env_lookup_type ctx (v : vref): lexp = lctx_lookup_type (ectx_to_lctx ctx) v

+ (* mkSusp ltp (S.shift (idx + 1)) *) + let env_lookup_expr ctx (v : vref): lexp option = lctx_lookup_value (ectx_to_lctx ctx) v

===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -142,11 +142,11 @@ let debug_pexp_decls decls =

let _ = match e with | Pexpr ((l, name), pxp) -> - lalign_print_string (pexp_to_string pxp) 15; + lalign_print_string (pexp_string pxp) 15; print_loc l; print_string " = "; pexp_print pxp

| Ptype ((l, name), ptp) -> - lalign_print_string (pexp_to_string ptp) 15; + lalign_print_string (pexp_string ptp) 15; print_loc l; print_string " : "; pexp_print ptp

| Pmcall((l, op), args) -> @@ -172,7 +172,7 @@ let debug_lexp_decls decls = let ((loc, name), lxp, ltp) = e in

print_string " "; - lalign_print_string (lexp_to_string lxp) 15; + lalign_print_string (lexp_string lxp) 15; print_string "["; print_loc loc; print_string "]";

let str = _lexp_str_decls (!debug_ppctx) [e] in

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -382,7 +382,11 @@ let main () = ) merged));

(* debug lexp parsing once merged *) - let lexps, nctx = _lexp_decls pexps octx 0 in + let lexps, nctx = try _lexp_decls pexps octx 0 + with e -> + print_lexp_trace (); + internal_error "Fail" in + (* use the new way of parsing expr *) let ctx = nctx in let flexps = List.flatten lexps in

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -43,6 +43,7 @@ type label = symbol module SMap = U.SMap

let elexp_warning = U.msg_warning "ELEXP" +let elexp_fatal = U.msg_fatal "ELEXP"

type elexp = | Imm of sexp @@ -77,28 +78,27 @@ let rec elexp_location e =

let elexp_name e = match e with - | Imm _ -> "Imm" - | Builtin _ -> "Builtin" - | Var _ -> "Var" - | Let _ -> "Let" - | Lambda _ -> "Lambda" + | Imm _ -> "Imm" + | Var _ -> "Var" + | Let _ -> "Let" | Call _ -> "Call" | Cons _ -> "Cons" | Case _ -> "Case" - | Type -> "Type" + | Type -> "Type" + | Lambda _ -> "Lambda" + | Builtin _ -> "Builtin" | Inductive _ -> "Inductive"

-let rec elexp_print lxp = print_string (elexp_str lxp) -and elexp_to_string lxp = elexp_str lxp -and elexp_str lxp = +let rec elexp_print lxp = print_string (elexp_string lxp) +and elexp_string lxp = let maybe_str lxp = match lxp with - | Some lxp -> " | _ => " ^ (elexp_str lxp) + | Some lxp -> " | _ => " ^ (elexp_string lxp) | None -> "" in

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

let str_pat lst = List.fold_left (fun str v -> @@ -108,33 +108,36 @@ and elexp_str lxp =

let str_cases c = SMap.fold (fun key (_, lst, lxp) str -> - str ^ " | " ^ key ^ " " ^ (str_pat lst) ^ " => " ^ (elexp_str lxp)) + str ^ " | " ^ key ^ " " ^ (str_pat lst) ^ " => " ^ (elexp_string lxp)) c "" in

let str_args lst = List.fold_left (fun str lxp -> - str ^ " " ^ (elexp_str lxp)) "" lst in + str ^ " " ^ (elexp_string lxp)) "" lst in

match lxp with - | Imm(s) -> sexp_to_str s + | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), _) -> s | Cons((_, s)) -> s

- | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_str b) + | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_string b)

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

| Call(fct, args) -> - "(" ^ (elexp_str fct) ^ (str_args args) ^ ")" + "(" ^ (elexp_string fct) ^ (str_args args) ^ ")"

| Case(_, t, cases, default) -> - "case " ^ (elexp_str t) ^ (str_cases cases) ^ (maybe_str default) + "case " ^ (elexp_string t) ^ (str_cases cases) ^ (maybe_str default)

| Inductive(_, (_, s)) -> "inductive_ " ^ s

| Type -> "Type "

+(* Print Lexp name followed by the lexp in itself, finally throw an exception *) +let elexp_debug_message loc lxp message = + elexp_fatal loc (message ^ "\n" ^ (elexp_name lxp) ^ ": " ^ (elexp_string lxp) ^ "\n");

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -99,27 +99,6 @@ let rec value_eq_list a b = value_equal v1 v2 && value_eq_list vv1 vv2 | _ -> false

-let rec value_print (vtp: value_type) = - match vtp with - | Closure (_, lxp, _) -> - print_string ("Closure(" ^ (elexp_str lxp) ^ ")") - | Vsexp sxp -> sexp_print sxp - | Vint(i) -> print_int i - | Vfloat(f) -> print_float f - | Vstring(s) -> print_string (""" ^ s ^ """) - | Vcons ((_, n), []) -> print_string n - | Vcons ((_, n), args) -> - print_string ("(" ^ n); - List.iter (fun arg -> print_string " "; value_print arg) args; - print_string ")"; - - | Vbuiltin(str) -> print_string str - | Vdummy -> print_string "value_print_dummy" - | Vin _ -> print_string "in_channel" - | Vout _ -> print_string "out_channel" - | Vcommand _ -> print_string "command" - (* | _ -> print_string "debug print" *) - let value_location (vtp: value_type) = match vtp with | Vcons ((loc, _), _) -> loc @@ -127,21 +106,39 @@ let value_location (vtp: value_type) = (* location info was lost or never existed *) | _ -> dloc

- let value_name v = match v with - | Vint _ -> "Vint" - | Vstring _ -> "Vstring" - | Vcons _ -> "Vcons" - | Vbuiltin _ -> "Sbuiltin" + | Vin _ -> "Vin" + | Vout _ -> "Vout" + | Vint _ -> "Vint" + | Vsexp _ -> "Vsexp" + | Vcons _ -> "Vcons" | Vfloat _ -> "Vfloat" - | Closure _ -> "Closure" - | Vsexp _ -> "Vsexp" - | Vdummy -> "Vdummy" - | Vin _ -> "Vin" - | Vout _ -> "Vout" + | Vdummy -> "Vdummy" + | Vstring _ -> "Vstring" + | Closure _ -> "Closure" + | Vbuiltin _ -> "Vbuiltin" | Vcommand _ -> "Vcommand"

+let rec value_string v = + match v with + | Vin _ -> "in_channel" + | Vout _ -> "out_channe;" + | Vdummy -> "dummy" + | Vcommand _ -> "command" + | Vstring s -> """ ^ s ^ """ + | Vbuiltin s -> s + | Vint i -> string_of_int i + | Vfloat f -> string_of_float f + | Vsexp s -> sexp_string s + | Closure (s, elexp, _) -> "(" ^ s ^ (elexp_string elexp) ^ ")" + | Vcons ((_, s), lst) -> + let args = List.fold_left (fun str v -> + (str ^ " " ^ (value_string v))) "" lst in + "(" ^ s ^ args ^ ")" + +let value_print (vtp: value_type) = print_string (value_string vtp) + let make_runtime_ctx = M.nil

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

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -61,6 +61,11 @@ let _eval_max_recursion_depth = ref 255 let reset_eval_trace () = _global_eval_trace := [] let _builtin_lookup = ref SMap.empty

+(* Print value name followed by the value in itself, finally throw an exception *) +let value_debug_message loc vxp message = + print_string "\n"; + print_string (value_name vxp); print_string ": "; value_print vxp; print_string "\n"; + eval_fatal loc message

(* This is an internal definition * 'i' is the recursion depth used to print the call trace *) @@ -68,7 +73,7 @@ let rec _eval lxp (ctx : Env.runtime_env) i: (value_type) = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let rec _eval lxp ctx i"); - prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_str lxp); + prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_string lxp); prerr_endline ("[StackTrace] ctx = ???"); prerr_endline ("[StackTrace] i = " ^ (string_of_int i)); prerr_endline ("[StackTrace] ------------------------------------------"); @@ -122,7 +127,7 @@ and eval_var ctx lxp v = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let eval_var ctx lxp v"); - prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_str lxp); + prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_string lxp); prerr_endline ("[StackTrace] ctx = ???"); prerr_endline ("[StackTrace] v = ((?loc?, " ^ name ^ "), " ^ (string_of_int idx) ^ ")"); prerr_endline ("[StackTrace] ------------------------------------------"); @@ -174,13 +179,7 @@ and eval_case ctx i loc target pat dflt = (* extract constructor name and arguments *) let ctor_name, args = match v with | Vcons((_, cname), args) -> cname, args - | _ -> - (* -- Debug print -- *) - debug_msg ( - elexp_print target; print_string "\n"; - value_print v; print_string "\n"); - (* -- Crash -- *) - eval_error loc "Target is not a Constructor" in + | _ -> elexp_debug_message loc target "Target is not a Constructor" in

(* Get working pattern *) try let (_, pat_args, exp) = SMap.find ctor_name pat in @@ -381,7 +380,7 @@ let debug_eval lxp ctx = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let debug_eval lxps rctx silent"); - prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_str lxp); + prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_string lxp); prerr_endline ("[StackTrace] ctx = ???"); prerr_endline ("[StackTrace] ------------------------------------------"); ());

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -346,18 +346,18 @@ and nosusp e = (* Return `e` without `Susp`. *) | Susp(e, s) -> push_susp e s | _ -> e

-let lexp_to_string e = +let lexp_name e = match e with - | Imm _ -> "Imm" - | Var _ -> "Var" - | Let _ -> "let" - | Arrow _ -> "Arrow" + | Imm _ -> "Imm" + | Var _ -> "Var" + | Let _ -> "let" + | Arrow _ -> "Arrow" | Lambda _ -> "lambda" - | Call _ -> "Call" + | Call _ -> "Call" + | Cons _ -> "inductive-cons" + | Case _ -> "case" | Inductive _ -> "inductive_" - | Cons _ -> "inductive-cons" - | Case _ -> "case" - | Builtin _ -> "Builtin" + | Builtin _ -> "Builtin" | _ -> "lexp_to_string: not implemented"

(* @@ -574,7 +574,7 @@ let rec lexp_unparse lxp =

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

- +let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) (* * Printing * --------------------- *) @@ -623,7 +623,7 @@ let default_print_context =

(* If I remember correctly ocaml doc, concat string is actually terrible *) (* It might be better to use a Buffer. *) -and lexp_to_str exp = _lexp_to_str (!debug_ppctx) exp +and lexp_pretty_string exp = _lexp_to_str (!debug_ppctx) exp

and _lexp_to_str ctx exp = (* create a string instead of printing *) @@ -672,7 +672,7 @@ and _lexp_to_str ctx exp = | String (_, s) -> tval (""" ^ s ^ """) | Integer(_, s) -> tval (string_of_int s) | Float (_, s) -> tval (string_of_float s) - | e -> sexp_to_str e) + | e -> sexp_string e)

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

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -71,30 +71,45 @@ let _global_lexp_trace = ref [] let _parsing_internals = ref false let btl_folder = ref "./btl/"

+(* Print Lexp name followed by the lexp in itself, finally throw an exception *) +let lexp_debug_message loc lxp message = + print_string "\n"; + print_string (lexp_string lxp); print_string ": "; lexp_print lxp; print_string "\n"; + lexp_fatal loc message + + (* merged declaration, allow us to process declaration in multiple pass *) (* first detect recursive decls then lexp decls*) type mdecl = | Ldecl of symbol * pexp option * pexp option | Lmcall of symbol * sexp list

- let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with | Sort (_, _) -> () (* All clear! *) | _ -> lexp_error l ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_to_str ltp) + ^ lexp_string ltp)

let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp with e -> print_string ("Exception while checking type `" - ^ lexp_to_str ltp ^ "` of var `" ^ + ^ lexp_string ltp ^ "` of var `" ^ (let (_, name) = v in name) ^"`\n"); print_lexp_ctx (ectx_to_lctx ctx); raise e

let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in - if OL.conv_p ltype (OL.check lctx lxp) then + let ltype' = try OL.check lctx lxp + with e -> + print_string "Error while type-checking:\n"; + lexp_print lxp; + print_string "\nIn context:\n"; + print_lexp_ctx (ectx_to_lctx ctx); + raise e in + (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is + * convertible to `Type_0`, because it doesn't have access to lctx. *) + if true (* OL.conv_p ltype ltype' *) then elab_check_proper_type ctx ltype var else (print_string "¡¡ctx_define error!!\n"; @@ -120,15 +135,12 @@ let ctx_define_rec (ctx: elab_context) decls = n - 1) (List.length decls) decls in - (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is - * convertible to `Type_0`, because it doesn't have access to lctx. - * - * let _ = List.fold_left (fun n (var, lxp, ltp) - * -> elab_check_def nctx var lxp - * (push_susp ltp (S.shift n)); - * n - 1) - * (List.length decls) - * decls in *) + let _ = List.fold_left (fun n (var, lxp, ltp) + -> elab_check_def nctx var lxp + (push_susp ltp (S.shift n)); + n - 1) + (List.length decls) + decls in nctx

(* The main job of lexp (currently) is to determine variable name (index) @@ -221,7 +233,7 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =

(* search type *) let ltp = env_lookup_type ctx ((loc, name), idx) in - lxp, ltp + lxp, ltp (* Return Macro[22] *)

with Not_found -> (lexp_error loc ("The variable: "" ^ name ^ "" was not declared"); @@ -538,16 +550,8 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let larg = _lexp_p_check parg arg_type ctx i in handle_fun_args ((ak, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) - | e -> Debug_fun.do_debug - (fun () -> - print_endline ("<>explicit arg : " - ^ Fmt_lexp.string_of_lxp ltp); - print_endline ("<>explicit res : " - ^ Fmt_lexp.string_of_lxp e); - ()); - lexp_fatal (sexp_location sarg) - ("Explicit-implicit arg `" ^ aname - ^ "` to non-function (type = " ^ lexp_to_str ltp ^ ")")) + | _ -> lexp_fatal (sexp_location sarg) + ("Explicit-implicit arg `" ^ aname ^ "` to non-function (type = " ^ lexp_string ltp ^ ")")) | sarg :: sargs (* Process Argument *) -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx with @@ -564,9 +568,8 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = lexp_print t; print_string "\n"; print_lexp_ctx (ectx_to_lctx ctx); lexp_fatal (sexp_location sarg) - ("Explicit arg `" ^ sexp_to_str sarg - ^ "` to non-function (type = " - ^ lexp_to_str ltp ^ ")")) in + ("Explicit arg `" ^ sexp_string sarg + ^ "` to non-function (type = " ^ lexp_string ltp ^ ")")) in

let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK @@ -603,32 +606,17 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = Call (body, List.rev largs), ret_type in

let handle_macro_call () = - (* Build function to be called *) - let macro_expand = get_predef "expand_macro_" ctx in - let args = [(Aexplicit, body); (Aexplicit, (olist2tlist_lexp sargs ctx))] in - let macro = Call(macro_expand, args) in - let emacro = OL.erase_type macro in - let rctx = from_lctx ctx in - - _global_eval_trace := []; - - let vxp = try eval emacro rctx - with e -> - print_eval_trace (); - raise e in - - let sxp = match vxp with - | Vsexp(sxp) -> sxp - (* Those are sexp converted by the eval function *) - | Vint(i) -> Integer(dloc, i) - | Vstring(s) -> String(dloc, s) - | Vfloat(f) -> Float(dloc, f) - (* I have vdum here WHY *) - | v -> debug_msg (value_print v); print_string "\n"; - lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in - - let pxp = pexp_parse sxp in - _lexp_p_infer pxp ctx (i + 1) in + let sxp = match lexp_expand_macro body sargs ctx with + | Vsexp(sxp) -> sxp + (* Those are sexp converted by the eval function *) + | Vint(i) -> Integer(dloc, i) + | Vstring(s) -> String(dloc, s) + | Vfloat(f) -> Float(dloc, f) + | v -> + value_debug_message loc v "Macro_ expects '(List Sexp) -> Sexp'" in + + let pxp = pexp_parse sxp in + _lexp_p_infer pxp ctx (i + 1) in

(* This is the builtin Macro type *) let macro_type, macro_disp = match get_predef_option "Macro" ctx with @@ -636,17 +624,8 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* When type.typer is being parsed and the predef is not yet available *) | None -> dltype, false in

- (*print_string "\nmacro_type="; lexp_print macro_type; - print_string "\nltp="; lexp_print ltp; - print_string " (= "; lexp_print (OL.lexp_whnf ltp (ectx_to_lctx ctx)); print_string ")\n"; *) - (* determine function type *) match func, ltp with - | 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 - | macro, _ when (macro_disp (* FIXME: This call to lexp_whnf shouldn't be needed! *) && OL.conv_p (OL.lexp_whnf ltp (ectx_to_lctx ctx) @@ -704,11 +683,11 @@ and lexp_read_pattern pattern exp target ctx: -> (try SMap.find cons_name map with Not_found -> lexp_warning loc - ("`" ^ lexp_to_str (it) + ("`" ^ lexp_string (it) ^ "` does not hold a `" ^ cons_name ^ "` constructor"); []) | it -> lexp_fatal loc - ("`" ^ lexp_to_str (it) + ("`" ^ lexp_string (it) ^ "` is not an inductive type!") in

(* FIXME: Don't remove them, add them without names! *) @@ -727,7 +706,7 @@ and lexp_read_pattern pattern exp target ctx: (cons_name, loc, args), nctx | _ -> lexp_warning (pexp_location ctor) ("Invalid constructor `" - ^ (pexp_to_string ctor) ^ "`"); + ^ (pexp_string ctor) ^ "`"); ("_", pexp_location ctor, []), ctx

(* Read patterns inside a constructor *) @@ -799,69 +778,71 @@ and lexp_parse_inductive ctors ctx i =

(* Macro declaration handling, return a list of declarations * to be processed *) +and lexp_expand_macro macro_funct sargs ctx = + + (* Build the function to be called *) + let macro_expand = get_predef "expand_macro_" ctx in + let args = [(Aexplicit, macro_funct); (Aexplicit, (olist2tlist_lexp sargs ctx))] in + + let macro = Call(macro_expand, args) in + let emacro = OL.erase_type macro in + let rctx = from_lctx ctx in + + (* eval macro *) + _global_eval_trace := []; + let vxp = try eval emacro rctx + with e -> print_eval_trace (); raise e in + (* Return results *) + (* Vint/Vstring/Vfloat might need to be converted to sexp *) + vxp + 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 -> - lexp_warning loc ("Macro "" ^ mname ^ "" was not found!"); 0 in - - (* get Macro declaration *) - let lxp = try env_lookup_expr ctx ((loc, mname), idx) - with Not_found -> - lexp_fatal loc (mname ^ " was found but " ^ (string_of_int idx) ^ - " is not a correct index.") in - - (* get stored function *) - let lxp = match lxp with - | Some (Call(Var((_, "Macro_"), _), [(_, fct)])) -> fct - | None -> lexp_fatal loc "expression does not exist" - | Some lxp -> print_string "\n"; - print_string (lexp_to_str lxp); print_string "\n"; - lexp_print lxp; print_string "\n"; - lexp_fatal loc "Macro is ill formed" in - - match lxp with - | Var((_, "add-attribute"), _) ->( - (* Builtin macro *) - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx 0 in - - (* extract info *) - let var, att, fn = match largs with - | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vi, vn), (ai, an), fn - | _ -> lexp_fatal loc "add-attribute expects 3 args" in - - let ctx = add_property ctx var att fn in - - (* FIXME: We need to have something in lexp to represent this - * add-attribute operation! *) - [], ctx - ) - (* Standard Macro *) - | _ -> ( - (* build new function *) - let arg = olist2tlist_lexp sargs ctx in - let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = OL.erase_type lxp in - let rctx = from_lctx ctx in - - (* get a list of declaration *) - let decls = eval elexp rctx in - - (* convert typer list to ocaml *) - let decls = tlist2olist [] decls in - - (* extract sexp from result *) - let decls = List.map (fun g -> - match g with - | Vsexp(sxp) -> sxp - | _ -> - print_string ((value_name g) ^ " : "); - value_print g; print_string "\n"; - lexp_fatal loc "Macro expects sexp list") decls in - - (* read as pexp_declaraton *) - pexp_decls_all decls, ctx) + try (* Lookup macro declaration *) + let idx = senv_lookup mname ctx in + let ltp = env_lookup_type ctx ((loc, mname), idx) in + let lxp = env_lookup_expr ctx ((loc, mname), idx) in + + (* lxp has the form (Call (Var(_, "Macro_"), [(_, function)])) + * We need the function so we can call it later *) + let body, mfun = match lxp with + | Some (Call(_, [(_, lxp)]) as e) -> e, lxp + | Some lxp -> lxp, lxp + | None -> lexp_fatal loc "expression does not exist" in + + (* Special Form *) + match mfun with + | Var((_, "add-attribute"), _) ->( + (* Builtin macro *) + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx 0 in + + (* extract info *) + let var, att, fn = match largs with + | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vi, vn), (ai, an), fn + | _ -> lexp_fatal loc "add-attribute expects 3 args" in + + let ctx = add_property ctx var att fn in + + (* FIXME: We need to have something in lexp to represent this + * add-attribute operation! *) + [], ctx) + + | _ ->( + let ret = lexp_expand_macro body sargs ctx in + + (* convert typer list to ocaml *) + let decls = tlist2olist [] ret in + + (* extract sexp from result *) + let decls = List.map (fun g -> + match g with + | Vsexp(sxp) -> sxp + | _ -> value_debug_message loc g "Macro expects sexp list") decls in + + (* read as pexp_declaraton *) + pexp_decls_all decls, ctx) + with _ -> + lexp_fatal loc "Macro not found"

(* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 0 @@ -888,6 +869,7 @@ and lexp_decls_1 (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) (pending_defs : (vdef * pexp * ltype) list) (* Pending definitions. *) : (vdef * lexp * ltype) list * pdecl list * elab_context = + match pdecls with | [] -> (if not (SMap.is_empty pending_decls) then let (s, (l, _)) = SMap.choose pending_decls in @@ -930,23 +912,28 @@ and lexp_decls_1 decls, pdecls, nctx else lexp_decls_1 pdecls ectx nctx pending_decls pending_defs - + with Not_found -> lexp_error l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs)

| Pmcall ((l, _) as v, sargs) :: pdecls - -> let pdecls', nctx' = lexp_decls_macro v sargs nctx in - if nctx = nctx' then + -> ((* expand macro and get the generated declarations *) + let pdecls', nctx' = lexp_decls_macro v sargs nctx in + + if nctx == nctx' then (* Plain macro expansion! *) lexp_decls_1 (List.append pdecls' pdecls) ectx nctx pending_decls pending_defs - else if ectx = nctx then + + else if ectx == nctx then (assert (SMap.is_empty pending_decls); assert (pending_defs = []); + lexp_decls_1 (List.append pdecls' pdecls) ectx nctx' pending_decls pending_defs) - else lexp_fatal l "Context changed in already changed context" + + else lexp_fatal l "Context changed in already changed context")

and _lexp_decls pdecls ctx i: ((vdef * lexp * ltype) list list * elab_context) = @@ -970,7 +957,7 @@ and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =

and print_lexp_trace () = - print_trace " LEXP TRACE " 50 pexp_to_string pexp_print !_global_lexp_trace + print_trace " LEXP TRACE " 50 pexp_string pexp_print !_global_lexp_trace

(* Only print var info *) and lexp_print_var_info ctx =

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -191,7 +191,9 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp =

let assert_type e t t' = - if conv_p t t' then () + (* FIXME: conv_p is not up to the task yet: it needs to take the ctx + * into account! *) + if true (* conv_p t t' *) then () else U.msg_error "TC" (lexp_location e) "Type mismatch"; ()

let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with @@ -202,8 +204,8 @@ let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *) -> U.msg_error "TC" (lexp_location l1) ("Can't compute the max of levels `" - ^ lexp_to_str l1 ^ "` and `" - ^ lexp_to_str l2 ^ "`"); + ^ lexp_string l1 ^ "` and `" + ^ lexp_string l2 ^ "`"); SortLevel SLz

let sort_compose l s1 s2 = @@ -242,11 +244,11 @@ let rec check ctx e = | Let (_, defs, e) -> let tmp_ctx = List.fold_left (fun ctx (v, e, t) - -> (match check ctx t with + -> (match lexp_whnf (check ctx t) ctx VMap.empty with | Sort (_, Stype _) -> () | _ -> (U.msg_error "TC" (lexp_location t) "Def type is not a type!"; ())); - DB.lctx_extend ctx v ForwardRef t) + DB.lctx_extend ctx (Some v) ForwardRef t) ctx defs in let _ = List.fold_left (fun n (v, e, t) -> assert_type e (push_susp t (S.shift n)) @@ -270,14 +272,14 @@ let rec check ctx e = "Not a proper type"; Sort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) - -> ((match check ctx t with + -> ((match lexp_whnf (check ctx t) ctx VMap.empty with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); Arrow (ak, Some v, t, l, (* FIXME: If ak is Aerasable, make sure the var only appears * in type annotations. *) - check (DB.lctx_extend ctx v Variable t) e)) + check (DB.lctx_extend ctx (Some v) Variable t) e)) | Call (f, args) -> let ft = check ctx f in List.fold_left (fun ft (ak,arg) @@ -292,7 +294,7 @@ let rec check ctx e = mkSusp t2 (S.substitute arg) | _ -> (U.msg_error "TC" (lexp_location arg) ("Calling a non function (type = " - ^ lexp_to_str ft ^ ")!"); + ^ lexp_string ft ^ ")!"); ft)) ft args | Inductive (l, label, args, cases) @@ -302,28 +304,31 @@ let rec check ctx e = -> let level = SMap.fold (fun _ case level -> - List.fold_left - (fun level (ak, _, t) -> - if ak == P.Aerasable && impredicative_erase - then level - else match lexp_whnf (check ctx t) ctx VMap.empty with - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> sort_level_max level level' - | tt -> U.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_to_str t - ^ " is not a Type! (" - ^ lexp_to_str tt ^")"); - DB.print_lexp_ctx ctx; - SortLevel SLz) - level - case) + let level, _ = + List.fold_left + (fun (level, ctx) (ak, v, t) -> + (if ak == P.Aerasable && impredicative_erase + then level + else match lexp_whnf (check ctx t) ctx VMap.empty with + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max level level' + | tt -> U.msg_error "TC" (lexp_location t) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string tt ^")"); + DB.print_lexp_ctx ctx; + SortLevel SLz), + DB.lctx_extend ctx v Variable t) + (level, ctx) + case in + level) cases (SortLevel SLz) in Sort (l, Stype level) | (ak, v, t)::args -> Arrow (ak, Some v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in + arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in let tct = arg_loop args ctx in tct | Case (l, e, it, ret, branches, default) @@ -331,7 +336,7 @@ let rec check ctx e = match e with | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) | _ -> (e,[]) in - (match call_split (check ctx e) with + (match call_split (lexp_whnf (check ctx e) ctx VMap.empty) with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -464,4 +469,4 @@ and clean_map cases = SMap.mapi (fun key (l, args, expr) -> (l, (clean_arg_list args), (erase_type expr))) cases

- +

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -404,16 +404,20 @@ let _pexp_decl_str (str: string) tenv grm limit = let pexp_decl_str str = _pexp_decl_str str default_stt default_grammar (Some ";")

-let pexp_to_string e = + +let pexp_string e = sexp_string (pexp_unparse e) +let pexp_print e = print_string (pexp_string e) + +let pexp_name e = match e with - | Pimm _ -> "Pimm" - | Pvar (_,_) -> "Pvar" + | Pimm _ -> "Pimm" + | Pvar (_,_) -> "Pvar" | Phastype (_,_,_) -> "Phastype" - | Pmetavar (_, _) -> "Pmetavar" - | Plet (_, _, _) -> "Plet" - | Parrow (_, _, _, _, _) -> "Parrow" - | Plambda (_,(_,_), _, _) -> "Plambda" - | Pcall (_, _) -> "Pcall" + | Pmetavar (_, _) -> "Pmetavar" + | Plet (_, _, _) -> "Plet" + | Parrow (_, _, _, _, _) -> "Parrow" + | Plambda (_,(_,_), _, _) -> "Plambda" + | Pcall (_, _) -> "Pcall" | Pinductive ((_,_), _, _) -> "Pinductive" - | Pcons (_,_) -> "Pcons" + | Pcons (_,_) -> "Pcons" | Pcase (_, _, _) -> "Pcase"

===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -142,10 +142,6 @@ let prelex_file file = (* Traditionally, line numbers start at 1 :-( *) 1 [] []

-(* Since current implementation is not compatible with stream * - * we write a temporary file and use this file as input. * - * This is a terrible solution but for the things we do it does not * - * really matters. Plus it will make testing easier. *) let prelex_string str = let pos = ref 0 in let getline () = @@ -160,19 +156,25 @@ let prelex_string str = line in prelex "<string>" getline 1 [] []

-let rec _pretokens_to_str pretok = +let pretoken_name pretok = + match pretok with + | Pretoken _ -> "Pretoken" + | Prestring _ -> "Prestring" + | Preblock _ -> "Preblock" + +let rec pretoken_string pretok = match pretok with | Preblock(_,pts,_) -> "{" ^ ( - List.fold_left (fun str pts -> str ^ " " ^ (_pretokens_to_str pts)) + List.fold_left (fun str pts -> str ^ " " ^ (pretoken_string pts)) "" pts) ^ " }" | Pretoken(_, str) -> str | Prestring(_, str) -> """ ^ str ^ """

-let pretokens_to_str pretokens = - List.fold_left (fun str pt -> str ^ (_pretokens_to_str pt)) "" pretokens +let pretokens_string pretokens = + List.fold_left (fun str pt -> str ^ (pretoken_string pt)) "" pretokens

-let pretokens_print p = print_string (pretokens_to_str p) +let pretokens_print p = print_string (pretokens_string p)

(* Prelexer comparison, ignoring source-line-number info, used for tests. *)

===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -63,20 +63,20 @@ let emptyString = hString ""

(*************** The Sexp Printer *********************)

-let rec sexp_to_str sexp = +let rec sexp_string sexp = match sexp with | Epsilon -> "ε" (* "ε" *) - | Block(_,pts,_) -> "{" ^ (pretokens_to_str pts) ^ " }" + | Block(_,pts,_) -> "{" ^ (pretokens_string pts) ^ " }" | Symbol(_, name) -> name | String(_, str) -> """ ^ str ^ """ | Integer(_, n) -> string_of_int n | Float(_, x) -> string_of_float x | Node(f, args) -> - let str = "(" ^ (sexp_to_str f) in + let str = "(" ^ (sexp_string f) in (List.fold_left (fun str sxp -> - str ^ " " ^ (sexp_to_str sxp)) str args) ^ ")" + str ^ " " ^ (sexp_string sxp)) str args) ^ ")"

-let sexp_print sexp = print_string (sexp_to_str sexp) +let sexp_print sexp = print_string (sexp_string sexp)

let rec sexp_location s = match s with @@ -88,6 +88,16 @@ let rec sexp_location s = | Node (s, _) -> sexp_location s | Epsilon -> (internal_error "Looking for the location of Epsilon")

+let rec sexp_name s = + match s with + | Block _ -> "Block" + | Symbol _ -> "Symbol" + | String _ -> "String" + | Integer _ -> "Integer" + | Float _ -> "Float" + | Node _ -> "Node" + | Epsilon -> "Epsilon" + (*************** The Sexp Parser *********************)

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -253,7 +253,7 @@ let _ = test_eval_eqv attr_decl "True"

(* This makes sure contexts are reinitialized between calls - * i.e the context should not grow *) + * i.e the context should not grow * ) let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> reset_eval_trace (); _typer_verbose := (-1); @@ -276,7 +276,7 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> success () else failure ()) -)) +)) *)

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

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