[Typer] [Git][monnier/typer][master] 5 commits: merge

Setepenre pushed to branch master at Stefan / Typer

Commits: f66e4e42 by Pierre Delaunay at 2016-05-11T11:41:35-04:00 merge

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

- - - - - 9ff1a46a by Pierre Delaunay at 2016-05-13T10:51:22-04:00 Use TC.conv_p to check that inferred_t = t in lexp_p_check

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

- - - - - c00870ce by Pierre Delaunay at 2016-05-15T09:45:45-04:00 merge

- - - - - 3002bbb1 by Pierre Delaunay at 2016-05-17T21:38:50-04:00 Add pdecl

Changes to be committed: * src/pexp.ml: - new type `pdecl` * adapted files to new pdecl type - src/debug.ml - src/lparse.ml * src/REPL.ml: - The case `f arg1 arg2 = body` is now correctly identified as a declaration. * new file: - samples/macro_decls.typer * src/lparse.ml: - lexp_context ref cell anymore

- - - - -

11 changed files:

- .travis.yml - + samples/macro_decls.typer - samples/quote.typer - src/REPL.ml - src/debug.ml - src/elexp.ml - src/lparse.ml - src/pexp.ml - src/util.ml - tests/eval_test.ml - tests/pexp_test.ml

Changes:

===================================== .travis.yml ===================================== --- a/.travis.yml +++ b/.travis.yml @@ -12,5 +12,9 @@ before_script: - opam config setup -a - opam config env

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

===================================== samples/macro_decls.typer ===================================== --- /dev/null +++ b/samples/macro_decls.typer @@ -0,0 +1,6 @@ +type_ = Macro_ (lambda (x : List Sexp) -> head Sexp x); + + +type Nat + | zero + | succ Nat;

===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -12,9 +12,9 @@ node = (lambda (op : Sexp) -> case y | nil => node_ op nil | _ => node_ (quote' (cons op nil)) (quote' y)); - | _ => node_ (symbol_ "node_") (cons (quote' op) - (cons (reconstruire la liste en sexp) nil)) - | uquote => y + + | uquote => node_ (symbol_ "node_") (cons (quote' op) + (cons (reconstruire la liste en sexp) nil))

% tree traversal quote' : List Sexp -> List Sexp; @@ -35,8 +35,7 @@ quote' = lambda (x : List Sexp) -> % quote definition quote = Macro_ (lambda (x : List Sexp) -> head Sexp (quote' x));

-fun n = - let x = 2 in +

% Should it return % (node_ (symbol_ "_*_") (cons (symbol_ x) (cons (symbol_ x) nil))) @@ -47,14 +46,3 @@ fun n = %main = quote (x * x);

-Quelque chose comme: - - Nat = inductive Nat - | zero - | succ Nat; - -est parsé comme: - - Call(op=_|_, args=[(inductive Nat), zero, (succ Nat)]) - -for it to work, we could define _|_ as a Macro

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -99,15 +99,12 @@ let rec read_input i =

(* Interactive mode is not usual typer It makes things easier to test out code *) -type pdecl = pvar * pexp * bool -type pexpr = pexp - type ldecl = vdef * lexp * ltype type lexpr = lexp

(* Grouping declaration together will enable us to support mutually recursive * declarations while bringing us closer to normal typer *) -let ipexp_parse (sxps: sexp list): (pdecl list * pexpr list) = +let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) = let rec _pxp_parse sxps dacc pacc = match sxps with | [] -> (List.rev dacc), (List.rev pacc) @@ -115,6 +112,11 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexpr list) = (* Declaration *) | Node (Symbol (_, ("_=_" | "_:_")), [Symbol s; t]) -> _pxp_parse tl (List.append (pexp_p_decls sxp) dacc) pacc + + (* f arg1 arg2 = function body; *) + | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> + _pxp_parse tl (List.append (pexp_p_decls sxp) dacc) pacc + (* Expression *) | _ -> _pxp_parse tl dacc ((pexp_parse sxp)::pacc) in _pxp_parse sxps [] []

===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -97,10 +97,10 @@ let rec debug_sexp_print sexp =

| Node(f, args) -> print_info "Node: " (sexp_location f); - sexp_print f; print_string " \t "; - List.iter (fun sexp -> sexp_print sexp; print_string " @ ") + sexp_print f; print_string " ["; + List.iter (fun sexp -> print_string " "; sexp_print sexp) args; - print_string " " + print_string "]"

(* Print a list of sexp *) let debug_sexp_print_all tokens = @@ -135,19 +135,27 @@ let debug_pexp_print ptop = (*| _ -> print_info "Not Impl " l ptop *)

let debug_pexp_decls decls = + let print_loc l = print_string "["; print_loc l; print_string "] " in + List.iter (fun e -> - let ((loc, name), pxp, tp) = e in + print_string " "; + + let _ = match e with + | Pexpr ((l, name), pxp) -> + lalign_print_string (pexp_to_string pxp) 15; + print_loc l; print_string " = "; pexp_print pxp + + | Ptype ((l, name), ptp) -> + lalign_print_string (pexp_to_string ptp) 15; + print_loc l; print_string " : "; pexp_print ptp

- print_string " "; - lalign_print_string (pexp_to_string pxp) 15; - print_string "["; print_loc loc; print_string "] "; + | Pmcall((l, op), args) -> + lalign_print_string "Macro Decls" 15; + print_loc l; sexp_print (Node(Symbol(l, op), args)) in

- print_string name; - if tp then print_string " : " else print_string " = "; - pexp_print pxp; print_string "\n" + print_string "\n")

- ) - decls + decls

(* Print a list of pexp *)

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -139,7 +139,6 @@ let rec elexp_location e = | Case (l,_,_,_) -> l | Inductive(l, _) -> l | Type -> U.dummy_location - let rec elexp_print lxp = print_string (elexp_str lxp) and elexp_to_string lxp = elexp_str lxp and elexp_str lxp =

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -265,6 +265,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | _ -> pexp_print p; print_string "\n"; lexp_fatal tloc "Unhandled Pexp"

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

@@ -447,7 +450,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

let lxp = match lxp with | Call(Var((_, "Macro_"), _), [(Aexplicit, fct)]) -> fct - | _ -> lexp_fatal loc "Macro ill formed" in + | _ -> lexp_fatal loc "Macro is ill formed" in

(* Build function to be called *) let arg = olist2tlist_lexp sargs ctx in @@ -604,91 +607,108 @@ and lexp_parse_inductive ctors ctx i = SMap.add name (make_args args ctx) lctors) SMap.empty ctors

+(* Macro declaration handling, return a list of declarations + * to be processed *) +and lexp_decls_macro (loc, mname) sargs ctx: pdecl list = + (* lookup for mname_ *) + let _ = try senv_lookup mname ctx + with Not_found -> + lexp_warning loc ("Macro "" ^ mname ^ "" was not found!"); 0 in + (* FIXME *) + (* (eval macro) -> Sexp *) + (* pexp_decls -> [pdecl] *) + + lexp_warning loc "Macro decls are not implemented yet!"; + [] + (* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 0 and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = - (* (pvar * pexp * bool) list *) - - let ctx = ref ctx in - let idx = ref 0 in - - (* Merge Type info and declaration together - * merge using a map to guarantee uniqueness. *) - let rec merge_decls (decls: (pvar * pexp * bool) list) merged acc: - ((location * pexp option * pexp option * int) SMap.t * string list) = - - (* we cant evaluate here because variables are not in the environment *) - match decls with - | [] -> merged, (List.rev acc) - | ((loc, name), pxp, bl)::tl -> - let (l, opxp, optp, i), acc = try (SMap.find name merged), acc - with Not_found -> - idx := !idx + 1; - ctx := env_extend (!ctx) (loc, name) None dltype; - (loc, None, None, !idx - 1), (name::acc) in - - let new_decl = match bl with - | true -> (l, opxp, Some pxp, i) - | false -> (l, Some pxp, optp, i) in - - let nmerged = SMap.add name new_decl merged in - (merge_decls tl nmerged acc) in - - let mdecls, ord = merge_decls decls SMap.empty [] in - - (* cast map to list to preserve declaration order *) - let ndecls = List.map (fun name -> - let (l, inst, tp, _) = SMap.find name mdecls in - ((l, name), inst, tp) ) ord in - - (* This is required for later *) - let ctx = !ctx in - let lst = ref [] in - - (* Doing types and expressions separately allow us to use *) - (* all typing information when lexp_parsing recursive definition *) - (* The price of this is iterating twice over declarations *) - (* + now we need to lookup type info *) - - (* Process types once *) - let n = ref ((List.length ndecls) - 1) in - (* for each declaration lexp their types *) - List.iter (fun ((loc, name), opxp, otpxp) -> - let vdef = (loc, name) in - let vref = (vdef, !n) in - n := !n - 1; - - match opxp, otpxp with - | _, Some tpxp -> let ltp, _ = _lexp_p_infer tpxp ctx (i + 1) in - (env_set_var_info ctx vref None ltp); - | _ -> ()) - ndecls; - - (* Process declaration in itself*) - let n = ref ((List.length ndecls) - 1) in - List.iter (fun ((loc, name), opxp, otpxp) -> - _global_lexp_trace := []; - let vdef = (loc, name) in - let vref = (vdef, !n) in - n := !n - 1; - - match opxp, otpxp with - | Some pxp, Some ptp -> - let ltp = env_lookup_type ctx vref in - let lxp = _lexp_p_check pxp ltp ctx (i + 1) in - (env_set_var_info ctx vref (Some lxp) ltp); - lst := (vdef, lxp, ltp)::!lst - - | Some pxp, None -> - let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in - (env_set_var_info ctx vref (Some lxp) ltp); - lst := (vdef, lxp, ltp)::!lst - - | None, _ -> lexp_warning loc "Unused Variable" - ) - ndecls; - - List.rev (!lst), ctx + let tctx = ctx in + let forw = SMap.empty in + let merged = ref SMap.empty in + let acc = ref [] in + let idx = ref 0 in + + let rec process_decl tctx decl1 decl2 = + match decl1, decl2 with + (* identifier : type; + * identifier : expr; *) + | Ptype((l, s1), ptp), Some Pexpr((_, s2), pxp) when s1 = s2 -> + let ltp, _ = lexp_p_infer ptp tctx in + let octx = env_extend tctx (l, s1) None ltp in + let lxp = lexp_p_check pxp ltp octx in + acc := (ref (s1, l, Some pxp, Some ptp))::!acc; + let tctx = env_extend tctx (l, s1) (Some lxp) ltp in + tctx, 2 + + (* Foward declaration *) + | Ptype((l, s), ptp), _ -> + let ltp, _ = lexp_p_infer ptp tctx in + acc := (ref (s, l, None, Some ptp))::!acc; + merged := SMap.add s (List.hd !acc) !merged; + let tctx = env_extend tctx (l, s) None ltp in + tctx, 1 + + (* infer *) + | Pexpr((l, s), pxp), _ ->( + try let value = SMap.find s !merged in + let _ = (match !value with + | (s, l, None, Some ptp) -> + let ltp, _ = lexp_p_infer ptp tctx in + let lxp = lexp_p_check pxp ltp tctx in + value := (s, l, Some pxp, Some ptp); + | (s, l, Some _, _) -> + lexp_warning l "Declaration override are not allowed" + | _ -> typer_unreachable "Empty declaration") in + tctx, 1 + with Not_found -> + let lxp, ltp = lexp_p_infer pxp tctx in + acc := (ref (s, l, Some pxp, None))::!acc; + let tctx = env_extend tctx (l, s) (Some lxp) ltp in + tctx, 1) + + | Pmcall(s, sargs), _ -> + let decls = lexp_decls_macro s sargs tctx in + let tctx = foldvar tctx decls in + tctx, 1 + + and foldvar tctx decls = + match decls, decls with + | p1::p2::tl2, _::tl1 -> + let tctx, v = process_decl tctx p1 (Some p2) in + idx := !idx + 1; + if v = 2 then foldvar tctx tl2 else foldvar tctx tl1 + + | p1::[], _ -> + let tctx, v = process_decl tctx p1 None in + idx := !idx + 2; + tctx + | [], _ -> tctx in + + let tctx = foldvar tctx decls in + let merged_decls = List.rev !acc in + let acc, ctx = + List.fold_left (fun (acc, ctx) rf -> + let (s, l, opxp, optp) = ! rf in + match opxp, optp with + | Some pxp, Some ptp -> + let ltp, _ = lexp_p_infer ptp tctx in + let lxp = lexp_p_check pxp ltp tctx in + let acc = ((l, s), lxp, ltp)::acc in + acc, (env_extend ctx (l, s) (Some lxp) ltp) + + | Some pxp, _ -> + let lxp, ltp = lexp_p_infer pxp tctx in + ((l, s), lxp, ltp)::acc, (env_extend ctx (l, s) (Some lxp) ltp) + + | None, Some ptp -> + lexp_warning l "Unused variable"; + let ltp, _ = lexp_p_infer ptp tctx in + ((l, s), dlxp, ltp)::acc, (env_extend ctx (l, s) None ltp) + + | _ -> typer_unreachable "No type no expression") ([], ctx) merged_decls in + List.rev acc, ctx

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

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -51,7 +51,7 @@ type pexp = | Pvar of pvar | Phastype of location * pexp * pexp | Pmetavar of pvar - | Plet of location * (pvar * pexp * bool) list * pexp + | Plet of location * pdecl list * pexp | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp | Pcall of pexp * sexp list (* Curried call. *) @@ -62,6 +62,11 @@ type pexp = | Pcons of pvar * symbol | Pcase of location * pexp * (ppat * pexp) list

+and pdecl = + | Ptype of symbol * pexp (* identifier : expr *) + | Pexpr of symbol * pexp (* identifier = expr *) + | Pmcall of symbol * sexp list (* identifier [sexp] *) +

let rec pexp_location e = match e with @@ -271,13 +276,13 @@ and pexp_u_pat (p : ppat) : sexp = match p with | Ppatvar s -> Symbol s | Ppatcons (c, args) -> Node (Symbol c, List.map pexp_u_pat_arg args)

-and pexp_p_decls e = +and pexp_p_decls e: pdecl list = match e with | Epsilon -> [] | Node (Symbol (_, ("_;_" | "_;" | ";_")), decls) -> List.concat (List.map pexp_p_decls decls) - | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [(s, pexp_parse t, true)] - | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [(s, pexp_parse t, false)] + | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] + | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, pexp_parse t)] | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> let rec mkfun args = match args with @@ -286,8 +291,13 @@ and pexp_p_decls e = | (arg :: args) -> pexp_error (sexp_location arg) "Unknown argument format"; mkfun args - in [(s, mkfun args, false)] - | _ -> pexp_error (sexp_location e) ("Unknown declaration"); [] + in [Pexpr(s, mkfun args)] + (* everything else is considered a macro + * An error will be produced during lexp_parsing if the macro does not exist + * once expanded the Pmcall macro will produce a list of pdecl *) + | Node (Symbol (l, op), args) -> [Pmcall((l, op), args)] + | _ -> + pexp_error (sexp_location e) ("Unknown declaration"); []

and pexp_unparse (e : pexp) : sexp = match e with @@ -339,10 +349,19 @@ and pexp_unparse (e : pexp) : sexp = [pexp_u_pat pat; pexp_unparse branch])) branches) -and pexp_u_decl (s, v, declp) = - Node (Symbol (dummy_location, if declp then "_:_" else "_=_"), - [Symbol s; pexp_unparse v]) -and pexp_u_decls ds = + +and pexp_u_decl decl = + match decl with + | Pexpr (s, v) -> + Node (Symbol (dummy_location, "_=_"), [Symbol s; pexp_unparse v]) + + | Ptype (s, v) -> + Node (Symbol (dummy_location, "_:_"), [Symbol s; pexp_unparse v]) + + | Pmcall(s, args) -> + Node (Symbol s, args) + +and pexp_u_decls (ds: pdecl list) = match ds with | [] -> Epsilon | [d] -> pexp_u_decl d @@ -356,7 +375,7 @@ let pexp_print e = sexp_print (pexp_unparse e) let pexp_parse_all (nodes: sexp list) = List.map pexp_parse nodes

-let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = +let pexp_decls_all (nodes: sexp list): pdecl list = let rec loop nodes acc = match nodes with | [] -> acc

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -55,6 +55,16 @@ let internal_error s = raise (Internal_error s) exception Unreachable_error of string let typer_unreachable s = raise (Unreachable_error s)

+(* Multi line error message ? + * + * | [X] Fatal SECTION [ln 12, cl 12: FILE.typer] + * | >> typer_dump = something; + * | >> + * | >> My Error message is on multiple line + * | >> multiple line + * | ------------------------------------------------ + *) + (* File is not printed because currently we parse only one file... *) (* Section is the name of the compilation step [for debugging] *) (* 'prerr' output is ugly *) @@ -62,14 +72,15 @@ let msg_message lvl kind section (loc: location) msg = if lvl <= !_typer_verbose then( print_string (" " ^ kind); print_string " ["; print_loc loc; print_string "] "; - print_string (section ^ " "); - print_string msg; + Fmt.lalign_print_string section 8; + print_string (" " ^ msg); print_newline ()) else ()

let msg_fatal s l m = msg_message 0 "[X] Fatal " s l m; internal_error m + let msg_error = msg_message 1 "[!] Error " let msg_warning = msg_message 2 "/!\ Warning " let msg_info = msg_message 3 "[?] Info "

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -161,6 +161,7 @@ let _ = (add_test "EVAL" "Inductive::Case" (fun () -> (* Inductive type declaration + Noisy declarations *) let code = " i = 90; + idt : Type; idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); d = 10; ctr0 = inductive-cons idt ctr0; e = 20; @@ -198,6 +199,7 @@ let _ = (add_test "EVAL" "Inductive::Case" (fun () ->

(* Those wil be used multiple times *) let nat_decl = " + Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat);

zero = inductive-cons Nat zero;

===================================== tests/pexp_test.ml ===================================== --- a/tests/pexp_test.ml +++ b/tests/pexp_test.ml @@ -12,9 +12,8 @@ let _ = (add_test "PEXP" "Type Parsing" (fun () -> | [expr] ->( match expr with | Plet(_, arg, _) -> (match arg with - | [] -> failure () - | (_, tp, bl)::_ ->( - if bl = true then success () else failure ())) + | Ptype(_, tp)::_ ->success () + | _ -> failure ()) | _ -> failure ()) | _ -> failure ()) )

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