[Typer] [Git][monnier/typer][master] 8 commits: misc

Setepenre pushed to branch master 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

- - - - -

9 changed files:

- btl/types.typer - samples/inductive.typer - − samples/int_index_inconsistency.typer - src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/eval.ml - src/lparse.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 @@ -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_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 @@ -137,4 +138,9 @@ and elexp_str lxp =

| Type -> "Type "

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

===================================== 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 *) @@ -153,13 +158,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

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -69,13 +69,19 @@ 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_to_str 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) with | Sort (_, _) -> () (* All clear! *) @@ -198,7 +204,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"); @@ -513,32 +519,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 @@ -546,17 +537,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)) @@ -698,69 +680,57 @@ 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 = match lxp with + | Some lxp -> lxp + | None -> lexp_fatal loc "expression does not exist" in + + (* Special Form *) + match body with + | Var((_, "add-attribute"), _) -> + print_string "Not Implemented"; [], 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 @@ -787,6 +757,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 @@ -829,23 +800,32 @@ 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 + print_string "lexp_decls_macro \n"; flush stdout; + + if nctx = nctx' then( + print_string "nctx = nctx'\n"; flush stdout; (* Plain macro expansion! *) lexp_decls_1 (List.append pdecls' pdecls) ectx nctx - pending_decls pending_defs + pending_decls pending_defs) + else if ectx = nctx then (assert (SMap.is_empty pending_decls); assert (pending_defs = []); + + print_string "ectx = nctx\n"; flush stdout; lexp_decls_1 (List.append pdecls' pdecls) ectx nctx' pending_decls pending_defs) - else lexp_fatal l "Context changed in already changed context" + + else ( + print_string "error\n"; flush stdout; lexp_fatal l "Context changed in already changed context"))

and _lexp_decls pdecls ctx i: ((vdef * lexp * ltype) list list * elab_context) =

===================================== 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/cee2f8e4fa0673a7752a1ead05befbbb45f...