Setepenre pushed to branch master at Stefan / Typer
Commits: 72dee3e0 by Pierre Delaunay at 2016-05-07T17:28:16-04:00 Fix lexp_parse.cons arrow
Constructor arrow type with multiple args were built in reverse
Changes to be committed: * .travis.yml: tell travis to install opam * README.md: add build status * src/builtin.ml: added sexp_dispatch * src/lparse.ml: - fix lexp.parse.cons - new function (lexp_case) (lexp_case can check and infer) - Added lexp.case in `lexp_p_check` * tests/eval_test.ml: - remove failure message when failure is expected * src/lexp.ml: - made huge let expression printing more readable * src/typecheck.ml: - adaptation to new Builtin
- - - - - d4cfc3a4 by Pierre Delaunay at 2016-05-07T20:05:20-04:00 fix macro handling
Changes to be committed: * btl/types.typer: * src/builtin.ml: - make_node use typer list. typer list are converted to ocaml list - added `string_eq`, `int_eq` and `sexp_eq` those should help for `uquote` * src/lparse.ml: - Macro_ takes a function (List Sexp) -> Sexp to build a Macro. ocaml sexp list are converted to typer List Sexp during macro expansion.
- - - - -
12 changed files:
- .travis.yml - README.md - btl/types.typer - src/builtin.ml - src/debug.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml - src/util.ml - tests/eval_test.ml - tests/macro_test.ml
Changes:
===================================== .travis.yml ===================================== --- a/.travis.yml +++ b/.travis.yml @@ -1,4 +1,9 @@ language: ocaml
+addons: + apt: + packages: + - opam + script: make tests
===================================== README.md ===================================== --- a/README.md +++ b/README.md @@ -4,6 +4,8 @@ Typer
# How to build Typer
+Status [%5D(https://travis-ci...) + ## Requirement
* Ocaml 4.01
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -1,3 +1,36 @@ +%* +%* Typer Compiler +%* +%* --------------------------------------------------------------------------- +%* +%* Copyright (C) 2011-2016 Free Software Foundation, Inc. +%* +%* Author: Pierre Delaunay pierre.delaunay@hec.ca +%* Keywords: languages, lisp, dependent types. +%* +%* This file is part of Typer. +%* +%* Typer is free software; you can redistribute it and/or modify it under the +%* terms of the GNU General Public License as published by the Free Software +%* Foundation, either version 3 of the License, or (at your option) any +%* later version. +%* +%* Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%* FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%* more details. +%* +%* You should have received a copy of the GNU General Public License along +%* with this program. If not, see http://www.gnu.org/licenses/. +%* +%* --------------------------------------------------------------------------- +%* +%* Description: +%* Define builtin types and functions +%* +%* --------------------------------------------------------------------------- + +% ----------------------------------------------------- % Base Types % -----------------------------------------------------
@@ -14,6 +47,20 @@ _+_ = Built-in "_+_"; _*_ : Int -> Int -> Int; _*_ = Built-in "_*_";
+Bool = inductive_ (Boolean) (True) (False); +True = inductive-cons Bool True; +False = inductive-cons Bool False; + +string_eq : String -> String -> Bool; +string_eq = Built-in "string_eq"; + +int_eq : Int -> Int -> Bool; +int_eq = Built-in "int_eq"; + +sexp_eq : Sexp -> Sexp -> Bool; +sexp_eq = Built-in "sexp_eq"; + +% ----------------------------------------------------- % List % -----------------------------------------------------
@@ -44,6 +91,7 @@ tail = lambda a => | nil => nil | cons hd tl => tl;
+% ----------------------------------------------------- % Macro % -----------------------------------------------------
@@ -62,7 +110,31 @@ node_ = Built-in "node_"; integer_ : Int -> Sexp; integer_ = Built-in "integer_";
-Macro : Type; -Macro = inductive_ (dMacro) (Macro_ Type); +float_ : Float -> Sexp; +float_ = Built-in "float_"; + +Macro : Type; +Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp)); Macro_ = inductive-cons Macro Macro_ ;
+% Type is not accurate yet +sexp_dispatch_ : Sexp -> (Sexp -> Sexp) -> (Sexp -> Sexp) -> (Sexp -> Sexp) + -> (Sexp -> Sexp) -> (Sexp -> Sexp) -> (Sexp -> Sexp) -> (Sexp -> Sexp); +sexp_dispatch_ = Built-in "sexp_dispatch_"; + + + + + + + + + + + + + + + + +
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -47,11 +47,11 @@ let builtin_error loc msg =
(* Builtin types *) -let dloc = dummy_location +let dloc = dummy_location let slevel0 = SortLevel (SLn 0) let slevel1 = SortLevel (SLn 1) -let type0 = Sort (dloc, Stype slevel0) -let type1 = Sort (dloc, Stype slevel1) +let type0 = Sort (dloc, Stype slevel0) +let type1 = Sort (dloc, Stype slevel1) let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel) let type_level = Builtin ((dloc, "TypeLevel"), type_level) @@ -110,14 +110,33 @@ let make_symbol loc args_val ctx =
let make_node loc args_val ctx =
+ let tlist = match args_val with + | [lst] -> lst + | _ -> builtin_error loc "node_ expects one 'List Sexp'" in + + (* Typer list to Ocaml list *) + let rec tlist2olist acc expr = + match expr with + | Vcons((_, "cons"), [hd; tl]) -> + tlist2olist (hd::acc) tl + | Vcons((_, "nil"), []) -> List.rev acc + | _ -> builtin_error loc "node_ expects one 'List Sexp'" in + + + let args_val = tlist2olist [] tlist in + let op, args = match args_val with | Vsexp(s)::tl -> s, tl | _::tl -> builtin_error loc ("node_ expects sexp as operator") | _ -> builtin_error loc ("node_ expects at least 2 arguments") in
let s = List.map (fun g -> match g with - | Vsexp(sxp) -> sxp - | _ -> builtin_error loc ("node_ expects sexp as arguments")) args in + | Vsexp(sxp) -> sxp + (* eval transform sexp into those... *) + | Vint (i) -> Integer(dloc, i) + | Vstring (s) -> String(dloc, s) + | _ -> value_print g; + builtin_error loc ("node_ expects sexp as arguments")) args in
Vsexp(Node(op, s))
@@ -128,7 +147,7 @@ let make_node loc args_val ctx = let sexp_dispatch loc args ctx =
let sxp, nd, sym, str, it, flt, blk = match args with - | [Vsexp(sxp), nd, sym, str, it, flt, blk] -> + | [Vsexp(sxp); nd; sym; str; it; flt; blk] -> sxp, nd, sym, str, it, flt, blk | _ -> builtin_error loc "sexp_dispatch expects 5 arguments" in
@@ -148,6 +167,30 @@ let make_string loc args_val ctx = Vdummy let make_integer loc args_val ctx = Vdummy let make_float loc args_val ctx = Vdummy
+let ttrue = Vcons((dloc, "True"), []) +let tfalse = Vcons((dloc, "False"), []) +let btyper b = if b then ttrue else tfalse + +let string_eq loc args_val ctx = + match args_val with + | [Vstring(s1); Vstring(s2)] -> btyper (s1 = s2) + | _ -> builtin_error loc "string_eq expects 2 strings" + +let int_eq loc args_val ctx = + match args_val with + | [Vint(s1); Vint(s2)] -> btyper (s1 = s2) + | _ -> builtin_error loc "int_eq expects 2 integer" + +let sexp_eq loc args_val ctx = + match args_val with + | [Vsexp(s1); Vsexp(s2)] -> ( + match s1, s2 with + | Symbol(_, s1), Symbol(_, s2) -> btyper (s1 = s2) + | String(_, s1), String(_, s2) -> btyper (s1 = s2) + | Integer(_, s1), Integer(_, s2) -> btyper (s1 = s2) + | Float(_, s1), Float(_, s2) -> btyper (s1 = s2) + | _ -> tfalse) + | _ -> builtin_error loc "int_eq expects 2 sexp"
(* * Should we have a function that @@ -161,13 +204,18 @@ let make_float loc args_val ctx = Vdummy
(* Built-in list of types/functions *) let typer_builtins_impl = [ - ("_+_" , iadd_impl); - ("_*_" , imult_impl); - ("block_" , make_block); - ("symbol_" , make_symbol); - ("string_" , make_string); - ("integer_", make_integer); - ("node_" , make_node); + ("_+_" , iadd_impl); + ("_*_" , imult_impl); + ("block_" , make_block); + ("symbol_" , make_symbol); + ("string_" , make_string); + ("integer_" , make_integer); + ("float_" , make_float); + ("node_" , make_node); + ("sexp_dispatch_", sexp_dispatch); + ("string_eq" , string_eq); + ("int_eq" , int_eq); + ("sexp_eq" , sexp_eq); ]
(* Make built-in lookup table *)
===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -164,30 +164,6 @@ let debug_pexp_print_all pexps = pexps ;;
- -let str_split str sep = - let str = String.trim str in - let n = String.length str in - - if n = 0 then [] - else ( - - let ret = ref [] in - let buffer = Buffer.create 10 in - Buffer.add_char buffer (str.[0]); - - for i = 1 to n - 1 do - if str.[i] = sep then ( - ret := (Buffer.contents buffer)::(!ret); - Buffer.reset buffer) - else - Buffer.add_char buffer (str.[i]); - done; - (if (Buffer.length buffer) > 0 then - ret := (Buffer.contents buffer)::(!ret)); - - List.rev (!ret));; - let debug_lexp_decls decls = let sep = " : " in List.iter (fun e ->
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -140,9 +140,7 @@ and eval_case ctx i loc target pat dflt =
(* extract constructor name and arguments *) let ctor_name, args = match v with - (* | Call(Var((_, cname), tp), args) -> cname, args *) | Vcons((_, cname), args) -> cname, args - | _ -> (* -- Debug print -- *) lexp_print target; print_string "\n"; @@ -150,32 +148,8 @@ and eval_case ctx i loc target pat dflt = (* -- Crash -- *) eval_error loc "Target is not a Constructor" in
- (* let ctor_n = List.length args in *) - - (* Check if a default is present *) - let run_default df = - match df with - | Some lxp -> _eval lxp ctx (i + 1) - | None -> - (* -- Debug print -- *) - lexp_print target; print_string "\n"; - value_print v; print_string "\n"; - (* -- Crash -- *) - eval_error loc "Match Failure" in - - (* Build a filter option *) - let is_true key (_, pat_args, _) = - (*let pat_n = List.length pat_args in (pat_n = ctor_n) && *) - (ctor_name = key) in - - (* Search for the working pattern *) - let sol = SMap.filter is_true pat in - if SMap.is_empty sol then - run_default dflt - else( - (* Get working pattern *) - let key, (_, pat_args, exp) = SMap.min_binding sol in - + (* Get working pattern *) + try let (_, pat_args, exp) = SMap.find ctor_name pat in (* build context (List.fold2 has problem with some cases) *) (* This is more robust *) let rec fold2 nctx pats args = @@ -184,14 +158,20 @@ and eval_case ctx i loc target pat dflt = let nctx = add_rte_variable (Some name) arg nctx in fold2 nctx pats args | (_, None)::pats, arg::args -> fold2 nctx pats args - (* Errors *) + (* Errors: those should not happen but they might *) + (* List.fold2 would complain. we print more info *) | _::_, [] -> eval_warning loc "a) Eval::Case Pattern Error"; nctx | [], _::_ -> eval_warning loc "b) Eval::Case Pattern Error"; nctx (* Normal case *) | [], [] -> nctx in
let nctx = fold2 ctx pat_args args in - _eval exp nctx (i + 1)) + _eval exp nctx (i + 1) + + (* Run default *) + with Not_found -> (match dflt with + | Some lxp -> _eval lxp ctx (i + 1) + | _ -> eval_error loc "Match Failure")
and build_arg_list args ctx i = (* _eval every args *)
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -593,9 +593,9 @@ let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e))
type print_context = (bool * int * bool * bool * bool * bool* int)
-let pretty_ppctx = ref (true , 0, true, false, true, 2, true) -let compact_ppctx = ref (false, 0, true, false, true, 2, false) -let debug_ppctx = ref (false, 0, true, true , false, 2, true) +let pretty_ppctx = ref (true , 0, true, false, true, 4, true) +let compact_ppctx = ref (false, 0, true, false, true, 4, false) +let debug_ppctx = ref (false, 0, true, true , false, 4, true)
let rec lexp_print e = _lexp_print (!debug_ppctx) e and _lexp_print ctx e = print_string (_lexp_to_str ctx e) @@ -617,7 +617,7 @@ and _lexp_to_str ctx exp = let lexp_to_str = _lexp_to_str ctx in
(* internal context, when parsing let *) - let inter_ctx = (false, indent + 1, ptype, pindex, false, isize, color) in + let inter_ctx = (pretty, indent + 1, ptype, pindex, false, isize, color) in
let lexp_to_stri idt e = _lexp_to_str (pretty, indent + idt, ptype, pindex, false, isize, color) e in @@ -636,10 +636,10 @@ and _lexp_to_str ctx exp = let newline = (if pretty then "\n" else " ") in let nl = newline in
- let keyword str = magenta ^ str ^ reset in - let error str = red ^ str ^ reset in - let tval str = yellow ^ str ^ reset in - let fun_call str= cyan ^ str ^ reset in + let keyword str = magenta ^ str ^ reset in + let error str = red ^ str ^ reset in + let tval str = yellow ^ str ^ reset in + let fun_call str = cyan ^ str ^ reset in
let index idx = let str = _index idx in if idx < 0 then (error str) else (green ^ str ^ reset) in @@ -662,11 +662,22 @@ and _lexp_to_str ctx exp = | Var ((loc, name), idx) -> name ^ (index idx) ;
| Let (_, decls, body) -> + (* Print first decls without indent *) + let h1, decls, idt_lvl = + match _lexp_str_decls inter_ctx decls with + | h1::decls -> h1, decls, 2 + | _ -> "", [], 1 in + let decls = List.fold_left (fun str elem -> - str ^ elem ^ " ") "" (_lexp_str_decls inter_ctx decls) in + str ^ (make_indent 1) ^ elem ^ nl) + (h1 ^ nl) decls in + + let n = String.length decls - 2 in + (* remove last newline *) + let decls = (String.sub decls 0 n) in
- (keyword "let ") ^ decls ^ (keyword "in ") ^ newline ^ - (make_indent 1) ^ (lexp_to_stri 1 body) + (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ + (make_indent idt_lvl) ^ (lexp_to_stri 1 body)
| Arrow(k, Some (_, name), tp, loc, expr) -> "(" ^ name ^ " : " ^ (lexp_to_str tp) ^ ") " ^ @@ -780,16 +791,17 @@ and _lexp_str_decls ctx decls = let (pretty, indent, ptype, pindex, sepdecl, isize, _) = ctx in let lexp_to_str = _lexp_to_str ctx in
- let make_indent idt = if pretty then (make_line ' ' ((idt + indent) * isize)) else "" in + (* let make_indent idt = + if pretty then (make_line ' ' ((idt + indent) * isize)) else "" in *) + let sepdecl = (if sepdecl then "\n" else "") in
let type_str name lxp = (if ptype then ( - (make_indent 0) ^ name ^ " : " ^ (lexp_to_str lxp) ^ ";") else "") in + name ^ " : " ^ (lexp_to_str lxp) ^ ";") else "") in
let ret = List.fold_left (fun str ((_, name), lxp, ltp) -> let str = if ptype then (type_str name ltp)::str else str in - ((make_indent 0) ^ name ^ " = " ^ (lexp_to_str lxp) ^ ";" ^ - sepdecl)::str) + (name ^ " = " ^ (lexp_to_str lxp) ^ ";" ^ sepdecl)::str)
[] decls in List.rev ret
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -224,7 +224,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
(* build Arrow type *) let cons_type = List.fold_left (fun ltp (kind, v, tp) -> - Arrow(kind, v, ltp, loc, tp)) inductive_type args in + Arrow(kind, v, tp, loc, ltp)) inductive_type (List.rev args) in
Cons((vr, idx), sym), cons_type
@@ -233,56 +233,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = ("The inductive type: " ^ type_name ^ " was not declared"); Cons((vr, -1), sym), dltype)
- (* Pcase *) - (* FIXME: This should be in lexp_p_check! *) + (* Pcase: we can infer iff `patterns` is not empty *) | Pcase (loc, target, patterns) -> - - let tlxp, tltp = lexp_infer target ctx in - - let uniqueness_warn name = - lexp_warning loc ("Pattern " ^ name ^ " is a duplicate." ^ - " It will override previous pattern.") in - - let check_uniqueness loc name map = ( - try let _ = SMap.find name map in uniqueness_warn name - with e -> ()) in - - (* FIXME: check if case is exhaustive *) - - (* make a list of all branches return type *) - let texp = ref [] in - - (* Read patterns one by one *) - let rec loop ptrns merged dflt = - match ptrns with - | [] -> merged, dflt - | hd::tl -> - let (pat, exp) = hd in - (* Create pattern context *) - let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx in - (* parse using pattern context *) - let exp, ltp = lexp_infer exp nctx in - texp := ltp::!texp; - - if name = "_" then ( - (if dflt != None then uniqueness_warn name); - loop tl merged (Some exp)) - else ( - check_uniqueness iloc name merged; - let merged = SMap.add name (iloc, arg, exp) merged in - loop tl merged dflt) in - - let (lpattern, dflt) = loop patterns SMap.empty None in - - (* FIXME: check return types are equivalent *) - let return_type = match (!texp), dflt with - | hd::tl, Some _ -> hd - | hd::tl, None -> hd - | _, Some v -> v - (* This will change *) - | _, None -> lexp_error loc "case with no branch ?"; dltype - in Case (loc, tlxp, tltp, return_type, lpattern, dflt), - (return_type) + lexp_case None (loc, target, patterns) ctx i
| Phastype (_, pxp, ptp) -> let ltp, _ = lexp_infer ptp ctx in @@ -299,7 +252,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp =
match p with (* This case cannot be inferred *) - | Plambda (kind, var, None, body) -> + | Plambda (kind, var, None, body) ->( (* Read var type from the provided type *) let ltp, lbtp = match t with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp @@ -308,29 +261,78 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let nctx = env_extend ctx var None ltp in let lbody = _lexp_p_check body lbtp nctx (i + 1) in
- Lambda(kind, var, ltp, lbody) + Lambda(kind, var, ltp, lbody)) + + (* This is mostly for the case where no branches are provided *) + | Pcase (loc, target, patterns) -> + let lxp, _ = lexp_case (Some t) (loc, target, patterns) ctx i in + lxp + + | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in + (* FIXME: check that inferred_t = t! *) + e + +(* Lexp.case cam be checked and inferred *) +and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = + (* FIXME: check if case is exhaustive *) + (* Helpers *) + let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) in + + let rtype = ref rtype in + + let type_check ltp = + match !rtype with + (* FIXME: check if branch returns correct type *) + | Some rltp -> true + (* if rtype was not provided then we use the first branch as reference *) + | None -> rtype := (Some ltp); true in + + let uniqueness_warn name = + lexp_warning loc ("Pattern " ^ name ^ " is a duplicate." ^ + " It will override previous pattern.") in + + let check_uniqueness loc name map = + try let _ = SMap.find name map in uniqueness_warn name + with e -> () in + + (* get target and its type *) + let tlxp, tltp = lexp_infer target ctx in + + (* make a list of all branches return type *) + let texp = ref [] in
- (* - | Pcall (Pvar(_, "expand_"), _args) ->( - let pargs = List.map pexp_parse _args in - let largs = _lexp_parse_all pargs ctx i in + (* Read patterns one by one *) + let fold_fun (merged, dflt) (pat, exp) = + (* Create pattern context *) + let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx in
- let lxp = match largs with - | [lxp] -> lxp - | hd::tl -> lexp_error tloc "expand_ expects one lexp"; hd - | _ -> lexp_fatal tloc "expand_ expects one lexp" in + (* parse using pattern context *) + let exp, ltp = lexp_infer exp nctx in + texp := ltp::!texp;
- (* eval argument *) - let sxp = match eval lxp (from_lctx ctx) with - | Vsexp(sxp) -> sxp - | _ -> lexp_fatal tloc "expand_ expects sexp" in + (* Check ltp type. Must be similar to rtype *) + (if type_check ltp then () + else lexp_error iloc "Branch return type mismatch");
- let pxp = pexp_parse sxp in - _lexp_p_check pxp t ctx (i + 1)) *) + if name = "_" then ( + (if dflt != None then uniqueness_warn name); + merged, (Some exp)) + else ( + check_uniqueness iloc name merged; + let merged = SMap.add name (iloc, arg, exp) merged in + merged, dflt) in
- | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in - (* FIXME: check that inferred_t = t! *) - e + let (lpattern, dflt) = + List.fold_left fold_fun (SMap.empty, None) patterns in + + let return_type = match (!texp), (!rtype) with + | hd::_, _ -> hd + | _ , Some v -> v + + (* This is impossible *) + | _, None -> typer_unreachable "The case has no return type info" in + + Case (loc, tlxp, tltp, return_type, lpattern, dflt), return_type
(* Identify Call Type and return processed call *) and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = @@ -412,16 +414,35 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ " is not a correct index.") in
- let sxp = match eval lxp (from_lctx ctx) with - (* (Macro_ sexp) is returned *) - | Vcons(_, [Vsexp(sxp)]) -> sxp + let rctx = (from_lctx ctx) in + let sxp = match eval lxp rctx with + (* This give me a closure to be evaluated with sargs *) + | Vcons(_, [Closure(body, rctx)]) ->( + (* Build typer list from ocaml list *) + let rsargs = List.rev sargs in + + (* Get Constructor *) + let considx = senv_lookup "cons" ctx in + let nilidx = senv_lookup "nil" ctx in + + let tcons = Var((dloc, "cons"), considx) in + let tnil = Var((dloc, "nil"), nilidx) in + + let arg = List.fold_left (fun tail elem -> + Call(tcons, [(Aexplicit, (Imm(elem))); + (Aexplicit, tail)])) tnil rsargs in + + let rctx = add_rte_variable None (eval arg rctx) rctx in + let r = eval body rctx in + match r with + | Vsexp(s) -> s + | _ -> Epsilon) + | v -> value_print v; print_string "\n"; lexp_fatal loc "Macro_ expects sexp" in
let pxp = pexp_parse sxp in - (* Generated Code *) - let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in - Call(lxp, new_args), ltp in + _lexp_p_infer pxp ctx (i + 1) in
(* let handle_qq loc = @@ -456,17 +477,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* Anonymous *) | ((Plambda _), _) -> Call(body, new_args), ltp
- (* Call to a macro *) - | (Pvar (l, n), Builtin((_, "Macro"), _)) -> - handle_macro_call (l, n) - - (* - | (Pvar (l, "qquote"), _) -> handle_qq l *) - - (* Call to quote * ) - | (Pvar (l, "'"), _) -> (match (handle_named_call (l, "'")), sargs with - | (Call (n, _), ltp), [sxp] -> Call(n, [(Aexplicit, Imm(sxp))]), ltp - | e, _ -> lexp_warning loc "quote operator expects one argument"; e) *) + | (Pvar (l, n), Var((_, "Macro"), _)) -> + (* FIXME: check db_idx points too a Macro type *) + handle_macro_call (l, n)
(* Call to Vanilla or constructor *) | (Pvar v, _) -> handle_named_call v @@ -623,6 +636,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = (* 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; @@ -693,6 +707,8 @@ and print_lexp_ctx ctx = print_string " | "; lalign_print_int (n - idx - 1) 7; print_string " | ";
+ let ptr_str = "" in (*" | | | | " in *) + try let (_, (_, name), exp, tp) = env_lookup_by_index (n - idx - 1) ctx in
(* Print env Info *) @@ -701,9 +717,16 @@ and print_lexp_ctx ctx =
let _ = (match exp with | None -> print_string "<var>" - | Some exp -> lexp_print exp) in + | Some exp -> lexp_print exp) + (* let str = _lexp_to_str (!debug_ppctx) exp in + let str = (match str_split str '\n' with + | hd::tl -> print_string (hd ^ "\n"); tl + | _ -> []) in + + List.iter (fun elem -> + print_string (ptr_str ^ elem ^ "\n")) str) *)in
- print_string ": "; lexp_print tp; print_string "\n"; + print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n";
_print (idx + 1) tl
===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -54,7 +54,7 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 | (SortLevel (sl1), SortLevel (sl2)) -> sl1 == sl2 | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 - | (Builtin (b1, s1, _), Builtin (b2, s2, _)) -> b1 == b2 && s1 == s2 + | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 == s2 (* BEWARE: When we'll make expand let-defined vars here, we'll have to * be careful not to introduce infinite-recursion. *) | (Var (l1, v1), e2) when not (S.identity_p s1) -> @@ -152,7 +152,7 @@ let rec check ctx e = | Sort (_, (Stype _)) -> (U.msg_error "TC" (lexp_location e) "Non-level arg to Type!"; B.type_omega) - | Builtin (_, _, t) -> t + | Builtin (_, t) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v | Susp (e, s) -> check ctx (unsusp e s)
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -96,3 +96,26 @@ let print_trace name max elem_to_string print_elem trace =
let opt_map f x = match x with None -> None | Some x -> Some (f x) + +let str_split str sep = + let str = String.trim str in + let n = String.length str in + + if n = 0 then [] + else ( + + let ret = ref [] in + let buffer = Buffer.create 10 in + Buffer.add_char buffer (str.[0]); + + for i = 1 to n - 1 do + if str.[i] = sep then ( + ret := (Buffer.contents buffer)::(!ret); + Buffer.reset buffer) + else + Buffer.add_char buffer (str.[i]); + done; + (if (Buffer.length buffer) > 0 then + ret := (Buffer.contents buffer)::(!ret)); + + List.rev (!ret));; \ No newline at end of file
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -133,6 +133,7 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> * i.e the context should not grow *) let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> reset_eval_trace (); + _typer_verbose := (-1);
let code = " infinity : Int -> Int; @@ -143,9 +144,11 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> (* Expect throwing *) try (* use the silent version as an error will be thrown *) let _ = _eval_expr_str "(infinity 0);" lctx rctx true in + _typer_verbose := 20; failure () with Internal_error m -> ( + _typer_verbose := 20; if m = "Recursion Depth exceeded" then success () else
===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -48,16 +48,10 @@ let _ = (add_test "MACROS" "macros base" (fun () ->
(* define 'lambda x -> x * x' using macros *) let dcode = " - sqr_fun = node_ (symbol_ "lambda_->_") (symbol_ "x") - (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x")); - - sqr_type = node_ (symbol_ "_->_") (symbol_ "Int") (symbol_ "Int"); - - has_type = lambda (expr : Sexp) -> - lambda (tp : Sexp) -> - node_ (symbol_ "_:_") expr tp; - - sqr = Macro_ (has_type sqr_fun sqr_type);" in + sqr = Macro_ (lambda (x : List Sexp) -> + let hd = head Sexp x in + (node_ (cons (symbol_ "_*_") (cons hd (cons hd nil))))); + " in
let rctx, lctx = eval_decl_str dcode lctx rctx in
View it on GitLab: https://gitlab.com/monnier/typer/compare/2f6cc8310cb495935efa265edbfba2dbdda...
Afficher les réponses par date