Setepenre pushed to branch master at Stefan / Typer

Commits: 573e2b5b by Pierre Delaunay at 2016-03-01T23:12:57-05:00 PCase

- - - - - 496106a8 by Pierre Delaunay at 2016-03-02T00:11:28-05:00 simple eval

- - - - - 81fa9435 by Pierre Delaunay at 2016-03-02T09:26:56-05:00 merged equivalent definition + moved inference routine to lparse

- - - - -

7 changed files:

- samples/lexp_test.typer - src/debruijn.ml - + src/eval.ml - src/lexp.ml - src/lparse.ml - tests/debug.ml - tests/full_debug.ml

Changes:

===================================== samples/lexp_test.typer ===================================== --- a/samples/lexp_test.typer +++ b/samples/lexp_test.typer @@ -1,62 +1,52 @@ -ab; - -% Type is read as a Pvar ????? -add = lambda (a : Type) -> lambda (b : Type) -> (add a b); - -% How typer is supposed to read this -p:int -> int; - -% this is a call to _=_ -odd n = case n | 0 => false | S n' => even (n'); - -% -% Here we test that two declaration with different -% name are EXACLTY equivalent in the eyes -% of the compiler -% -% Declaration order STILL MATTERS -% - -% let -let a:Nat; d:Nat; c:Nat; b:Nat; - a = b; - d = a; - c = d; - b = c; - in a + b + c + d -; - -% let: Different naming -let e:Nat; f:Nat; g:Nat; h:Nat; - e = h; - f = e; - g = f; - h = g; - in e + h + g + f -; - -% let: Different Ordering -let b:Nat; c:Nat; d:Nat; a:Nat; - c = d; - d = a; - b = c; - a = b; - in a + b + c + d -; - -% -% Recursivity detection -% - -let odd: (int -> int); - even: (int -> int); - odd n = case n | 0 => false | S n' => even (n'); - even n = case n | 0 => true | S n' => odd (n'); - in a + b; - - -% Do I consider functions as variable ?? Yes - - - - +% Eval test + +let c = 1; a = 5; b = 10; d = 3; in + a + b; + +% ------------------------------------------- +% Function Calls +% ------------------------------------------- + +% define sqrt +sqrt x = lambda (x : Nat) -> x * x; + +% define cube +cube = lambda (x : Nat) -> x * (sqrt x); + +% explicit +mult = lambda (x : Nat) -> lambda (y : Nat) -> (y * x); + +% implicit (Type annotation introduce a bug) +cube = lambda x y -> (x * y); + + +% ------------------------------------------- +% Inductive type +% ------------------------------------------- + +inductive_ (dummy_Nat) (zero) (succ Nat); + +% Usage +Nat : Type % This line is not parsed +Nat = inductive_ (dummy_Nat) (zero) (succ Nat); % zero is not parsed + +% Constructor +% ------------------------------------------- + +% only inductive-cons is available + +inductive-cons Nat succ; + +% Usage +zero = inductive-cons Nat zero; % those are aliases +succ = inductive-cons Nat succ; + +one = (succ (zero)); + +% ------------------------------------------- +% Cases +% ------------------------------------------- + +case x + | zero => y + | succ x => succ (plus x y);

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -30,18 +30,11 @@ * methods starting with '_' are considered private and should not * elsewhere in the project * - * Methods: - * make_context : make an empty context - * add_scope ctx : add new scope to the current context - * find_var name ctx: return the index of the variable 'name' - * add_variable name loc ctx : add a variable to the current context - * - * TODO: - * ADD meyers list <index -> (type, name?)> - * * ---------------------------------------------------------------------------*)

open Util +open Lexp +open Myers

let debruijn_error = msg_error "DEBRUIJN" let debruijn_warning = msg_warning "DEBRUIJN" @@ -49,6 +42,10 @@ let debruijn_warning = msg_warning "DEBRUIJN" (* Type definitions * ---------------------------------- *)

+(* Index -> Variable Info *) +type env_elem = (int * (location * string) * lexp * ltype) +type env_type = env_elem myers + (* This exist because I don't want that file to depend on anything *) module StringMap = Map.Make (struct type t = string let compare = String.compare end) @@ -60,50 +57,55 @@ type scope = (int) StringMap.t (* Map<String, int>*) (* Offset is the number to take us out of the inner scope * Scope is the Mapping between Variable's names and its current index loc * Offset + Scope *) -type context_impl = int * scope +type senv_type = int * scope

(* The recursive type that does everything * inner Scope * Outer Scope *) -type lexp_context = context_impl * lexp_context option +type lexp_context = senv_type * lexp_context option * env_type

(* internal definitions: DO NOT USE * ---------------------------------- *) - + let _make_scope = StringMap.empty;; let _make_context_impl = (0, _make_scope);; +let _make_myers = nil

let _get_inner_ctx (ctx: lexp_context) = - match ctx with - | (ct, _) -> ct + let (ct, _, _) = ctx in ct ;;

let _get_inner_scope (ctx: lexp_context): scope = - let ictx = _get_inner_ctx ctx in - match ictx with - | (_, scope) -> scope + let ((_, scope), _, _) = ctx in scope +;; + +let _get_environ (ctx: lexp_context) = + let (_, _, env) = ctx in env ;;

(* get current offset *) let _get_offset (ctx: lexp_context): int = - let inner = _get_inner_ctx ctx in - match inner with - | offset, _ -> offset + let ((offset, _), _, _) = ctx in offset ;;

(* increase the offset *) let _inc_offset (ctx: lexp_context): lexp_context = (* Because using ref is hell, we make a copy *) match ctx with - | ((offset, scope), None) -> ((offset + 1, scope), None) - | ((offset, scope), Some outter) -> ((offset + 1, scope), Some outter) + | ((offset, scope), None, e) -> ((offset + 1, scope), None, e) + | ((offset, scope), Some outter, e) -> + ((offset + 1, scope), Some outter, e) ;;

(* Increase the indexes of all inner variables *) let _inc_index (ctx: lexp_context): lexp_context = - let ((offset, scope), otr) = ctx in + let ((offset, scope), otr, env) = ctx in let scope = StringMap.map (fun value -> value + 1) scope in - ((offset, scope), otr) + ((offset, scope), otr, env) +;; + +let _add_var_environ variable ctx = + let (a, b, env) = ctx in cons variable env ;;

(* Public methods: DO USE @@ -112,7 +114,7 @@ let _inc_index (ctx: lexp_context): lexp_context = (* return its current DeBruijn index * return -1 if the variable does not exist * return closest variable *) -let rec find_var (name: string) (ctx: lexp_context) = +let rec senv_lookup (name: string) (ctx: lexp_context) = (* Search *) let local_index = find_local name ctx in if local_index >= 0 then @@ -137,14 +139,16 @@ and find_local (name: string) (ctx: lexp_context): int = * the reason is _find_outer does not send back a correct index *) and _find_outer (name: string) (ctx: lexp_context): int = match ctx with - | (_, Some ct) -> (find_var name ct) + | (_, Some ct, _) -> (senv_lookup name ct) | _ -> -1 ;; - -(* Alias *) -let get_var_index name ctx = find_var name ctx;;

-let add_variable name loc ctx = +(* We first add variable into our map later on we will add them into + * the environment. The reason for this is that the type info is + * known after lexp parsing which need the index fist *) +let senv_add_var name loc ctx = + (*let (name, loc, exp, type_info) = var in *) + (* I think this should be illegal *) let local_index = find_local name ctx in if local_index >= 0 then (* This is the index not the number of element *) @@ -156,21 +160,46 @@ let add_variable name loc ctx =

(* Increase distance *) let scope = StringMap.map (fun value -> value + 1) (_get_inner_scope ctx) in - (* Add new Value *) + (* Add new Value to the map *) let new_scope = StringMap.add name 0 scope in (* build new context *) match ctx with - | ((offset, _), None) - -> ((offset + 1, new_scope), None) - | ((offset, _), Some outter) - -> ((offset + 1, new_scope), Some outter) + | ((offset, _), None, e) + -> ((offset + 1, new_scope), None, e) + | ((offset, _), Some outter, e) + -> ((offset + 1, new_scope), Some outter, e) ;;

+(* *) +let env_add_var_info var ctx = + let (rof, (loc, name), value, ltyp) = var in + let nenv = _add_var_environ (rof, (loc, name), value, ltyp) ctx in + let (a, b, env) = ctx in + (a, b, nenv) +;; + +let env_lookup_type_by_index index ctx = + try + let (roffset, (_, name), _, t) = Myers.nth index (_get_environ ctx) in + Shift (index - roffset, t) + with + Not_found -> internal_error "DeBruijn index out of bounds!" +;; + +let env_lookup_type (env : env_type) (v : vref) = + let ((_, rname), dbi) = v in + try let (recursion_offset, (_, dname), _, t) = Myers.nth dbi env in + if dname = rname then + Shift (dbi - recursion_offset, t) + else + internal_error "DeBruijn index refers to wrong name!" + with Not_found -> internal_error "DeBruijn index out of bounds!" + (* Make a Global context *) -let make_context = (_make_context_impl, None);; +let make_context = (_make_context_impl, None, _make_myers);;

(* Make a new Scope inside the outer context 'ctx' *) -let add_scope ctx = (_make_context_impl, Some ctx);; +let add_scope ctx = (_make_context_impl, Some ctx, _make_myers);;

(* Print Functions for testing *) let print_scope (scp: scope) (offset: int): unit = @@ -188,7 +217,7 @@ let print_lexp_context (ctx: lexp_context): unit = let rec impl (ctx2: lexp_context) (offset: int) = let inner = _get_inner_scope ctx2 in match ctx2 with - | (_, Some ct) + | (_, Some ct, _) -> impl ct ((_get_offset ctx2) + offset); (print_scope inner offset); | _ -> (print_scope inner offset) in

===================================== src/eval.ml ===================================== --- /dev/null +++ b/src/eval.ml @@ -0,0 +1,159 @@ +(* + * 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: + * Simple interpreter + * + * --------------------------------------------------------------------------- *) + +open Util +open Lexp +open Lparse +open Myers +open Sexp +open Fmt + + + +let print_myers_list l print_fun = + let n = (length l) in + + print_string "-------------------\n"; + print_string " Environement: \n"; + print_string "-------------------\n"; + + for i = 0 to n - 1 do + ralign_print_int (i + 1) 4; + print_string ") "; + print_fun (nth i l); + done; + print_string "-------------------\n"; +;; + +let get_function_name fname = + match fname with + | Var(v) -> let ((loc, name), idx) = v in name + | _ -> "Name Lookup failure" +;; + +let get_int lxp = + match lxp with + | Imm(Integer(_, l)) -> l + | _ -> lexp_print lxp; -1 +;; + +(* Runtime Environ *) +type runtime_env = lexp myers +let make_runtime_ctx = nil;; +let add_rte_variable x l = (cons x l);; +let get_rte_variable idx l = (nth (idx) l);; + +let print_rte_ctx l = print_myers_list l + (fun g -> lexp_print g; print_string "\n") +;; + +(* Evaluation reduce an expression x to an Lexp.Imm *) +let rec eval lxp ctx: (lexp * runtime_env) = + + match lxp with + (* This is already a leaf *) + | Imm(v) -> lxp, ctx + + (* Return a value stored in the environ *) + | Var((loc, name), idx) -> begin + try + (get_rte_variable idx ctx), ctx + with + Not_found -> + print_string ("Variable: " ^ name ^ " was not found | "); + print_int idx; print_string "\n"; + raise Not_found end + + (* this works for non recursive let *) + | Let(_, decls, inst) -> begin + (* First we evaluate all declaration then we evaluate the instruction *) + let nctx = build_ctx decls ctx in + let value, nctx = eval inst nctx in + (* return old context as we exit let's scope*) + value, ctx end + + (* Function call *) + | Call (fname, args) -> + (* Add args in the scope *) + let nctx = build_arg_list args ctx in + + (* We need to seek out the function declaration and eval the body *) + (* but currently we cannot declare functions so I hardcoded + *) + (* let bdy = get_body fname in + eval bdy nctx *) + + (* fname is currently a var *) + let name = get_function_name fname in + (* Hardcoded function for now *) + if name = "_+_" then begin + + (* Get the two args *) + let l = get_int (get_rte_variable 0 nctx) in + let r = get_int (get_rte_variable 1 nctx) in + + Imm(Integer(dummy_location, l + r)), ctx end + else + Imm(String(dummy_location, "Funct Not Implemented")), ctx + + | _ -> Imm(String(dummy_location, "Eval Not Implemented")), ctx + +and build_arg_list args ctx = + + (* Eval every args *) + let arg_val = List.map (fun (k, e) -> let (v, c) = eval e ctx in v) args in + + (* Add args inside context *) + List.fold_left (fun c v -> add_rte_variable v c) ctx arg_val + +and build_ctx decls ctx = + match decls with + | [] -> ctx + | hd::tl -> + let (v, exp, tp) = hd in + let (value, nctx) = eval exp ctx in + let nctx = add_rte_variable value nctx in + build_ctx tl nctx +;; + +let print_eval_result lxp = + print_string " >> "; + match lxp with + | Imm(v) -> sexp_print v; print_string "\n" + | _ -> print_string "Evaluation Failed\n" +;; + +let evalprint lxp ctx = + let v, ctx = (eval lxp ctx) in + print_eval_result v; + ctx +;; +

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -192,17 +192,6 @@ let builtins = *)

-type env_elem = (db_offset * vdef * lexp option * ltype) -type env_type = env_elem myers -let env_lookup_type (env : env_type) (v : vref) = - let ((_, rname), dbi) = v in - try let (recursion_offset, (_, dname), _, t) = Myers.nth dbi env in - if dname = rname then - Shift (dbi - recursion_offset, t) - else - internal_error "DeBruijn index refers to wrong name!" - with Not_found -> internal_error "DeBruijn index out of bounds!" - (***** SMap fold2 helper *****)

let smap_fold2 c f m1 m2 init @@ -659,39 +648,4 @@ let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) * | _ -> msg_error l "Uninstantiated metavar of unknown type"; * mk_meta_dummy env l *)

-(* -let rec lexp_parse (p : pexp) (env : (vdef * lexp option * ltype) myers) = *) *) - -(* FIXME -type senv_type = (db_revindex SMap.t * db_index) -let senv_lookup senv s : db_index = - let (m, i) = senv in - i - SMap.find s senv *) - -(* Parsing a Pexp into an Lexp is really "elaboration", i.e. it needs to - * infer the types and perform macro-expansion. For won't really - * do any of that, but we can already start structuring it accordingly. - * - * More specifically, we do it with 2 mutually recursive functions: - * one takes a Pexp along with its expected type and return an Lexp - * of that type (hopefully), whereas the other takes a Pexp and - * infers its type (which it returns along with the Lexp). - * This is the idea of "bidirectional type checking", which minimizes - * the amount of "guessing" and/or annotations. Basically guessing/annotations - * is only needed at those few places where the code is not fully-normalized, - * which in normal programs is only in "let" definitions. - * So the rule of thumbs are: - * - use lexp_p_infer for destructors, and use lexp_p_check for constructors. - * - use lexp_p_check whenever you can. - *) - -let rec lexp_p_infer (env : env_type) (p : pexp) : lexp * ltype = - (UnknownType(dummy_location), UnknownType(dummy_location)) - -and lexp_p_check (env : env_type) (p : pexp) (t : ltype) : lexp = - match p with - | _ - -> let (e, inferred_t) = lexp_p_infer env p in - (* FIXME: check that inferred_t = t! *) - e

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -47,9 +47,18 @@ let not_implemented_error () = internal_error "not implemented" ;;

-let lexp_error = msg_error "LEXP" +let lexp_error loc msg = + msg_error "LEXP" loc msg; + raise (internal_error msg) +;; + +let dloc = dummy_location let lexp_warning = msg_warning "LEXP"

+(* Print back in CET (Close Enough Typer) easier to read *) + (* pretty ? * indent level * print_type? *) +type print_context = (bool * int * bool) + (* Vdef is exactly similar to Pvar but need to modify our ctx *) let pvar_to_vdef p = p @@ -70,17 +79,16 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =

(* Symbol i.e identifier /!\ A lot of Pvar are not variables /!\ *) | Pvar (loc, name) -> - let idx = get_var_index name ctx in + let idx = senv_lookup name ctx in (* This should be an error but we accept it for debugging *) if idx < 0 then lexp_warning tloc ("Variable: '" ^ name ^ "' does not exist"); - (make_var name (idx + 1) loc), ctx; + (make_var name (idx) loc), ctx;

(* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> (* /!\ HERE *) let decl, nctx = lexp_parse_let decls (add_scope ctx) in let bdy, nctx = lexp_parse body nctx in - (* print_lexp_context nctx; *) (* Send back old context as we exit the inner scope *) Let(tloc, decl, bdy), ctx

@@ -110,7 +118,9 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =

(* Function Call *) | Pcall (fname, _args) -> + (* Why function names are pexp ? *) let fname, ctx = lexp_parse fname ctx in + let pargs = pexp_parse_all _args in let largs, fctx = lexp_parse_all pargs ctx in

@@ -118,15 +128,118 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = let new_args = List.map (fun g -> (Aexplicit, g)) largs in

Call(fname, new_args), ctx - + + (* Pinductive *) + | Pinductive (label, _, ctors) -> + let dummy = (Aexplicit, (dummy_location, "a"), UnknownType(tloc))::[] in + let map_ctor, nctx = lexp_parse_constructors ctors ctx in + (* We exit current context, return old context *) + Inductive(tloc, label, dummy, map_ctor), ctx + (* Pcons *) + | Pcons(var, sym) -> (* vref, symbol*) + let (loc, name) = var in + let idx = 0 in + Cons(((pvar_to_vdef var), idx), sym), ctx + (* Pcase *) - (* Pinductive *) (* Pinductive Pexp implementation is not ready *) - + | Pcase (loc, target, patterns) -> + + let lxp, ltp = lexp_p_infer target ctx in + + (* Read patterns one by one *) + let rec loop ptrns merged dflt = + match ptrns with + | [] -> merged, dflt + | hd::tl -> + let (pat, exp) = hd in + (* Parse the pattern first then parse the expr *) + let (name, iloc, arg) = lexp_read_pattern pat exp lxp in + let exp, nctx = lexp_parse exp ctx in + if name = "_" then + loop tl merged (Some exp) + else + let merged = SMap.add name (iloc, arg, exp) merged in + loop tl merged dflt in + + let (lpattern, dflt) = loop patterns SMap.empty None in + Case(loc, lxp, ltp, lpattern, dflt), ctx + | _ -> UnknownType(tloc), ctx + +(* Read a pattern and create the equivalent representation *) +and lexp_read_pattern pattern exp target: + (string * location * (arg_kind * vdef) option list) = + + match pattern with + | Ppatany (loc) -> (* Catch all expression nothing to do *) + ("_", loc, [])

+ | Ppatvar (loc, name) -> (* Create a variable containing target *) + (*let nctx = add_variable name loc ctx in + let idx = get_var_index name nctx in + let info = (idx, (loc, name), target, UnknownType(loc)) in + let nctx = add_variable_info info nctx in *) + (name, loc, []) + + | Ppatcons (ctor_name, args) -> + let (loc, name) = ctor_name in

+ (* read pattern args *) + let args = lexp_read_pattern_args args in + (name, loc, args) + +(* Read patterns inside a constructor *) +and lexp_read_pattern_args args:((arg_kind * vdef) option list) = + + let rec loop args acc = + match args with + | [] -> (List.rev acc) + | hd::tl -> + let (_, pat) = hd in + match pat with + (* Nothing to do *) + | Ppatany (loc) -> loop tl (None::acc) + | Ppatvar (loc, name) -> + (* get kind from the call *) + let nacc = (Some (Aexplicit, (loc, name)))::acc in + loop tl nacc + | _ -> lexp_error dloc "Constructor inside a Constructor"; + + in loop args [] + +(* Parse inductive constructor *) +and lexp_parse_constructors ctors ctx = + + let make_args (args:(arg_kind * pvar option * pexp) list): + (arg_kind * ltype) list * lexp_context = + let rec loop args acc ctx = + match args with + | [] -> (List.rev acc), ctx + | hd::tl -> begin + match hd with + (* What does the optional Pvar do ? + that expression does not exist in LEXP*) + | (kind, _, exp) -> + let lxp, nctx = lexp_parse exp ctx in + loop tl ((kind, lxp)::acc) nctx end in + loop args [] ctx in + + let rec loop ctors merged ctx = + match ctors with + | [] -> merged, ctx + | hd::tl -> begin + match hd with + | ((loc, name), args) -> + let largs, nctx = make_args args in + let nmerged = SMap.add name largs merged in + (loop tl nmerged ctx) + end in + + loop ctors SMap.empty ctx + +(* Parse let declaration *) and lexp_parse_let decls ctx =

(* Merge Type info and declaration together *) @@ -177,7 +290,7 @@ and lexp_parse_let decls ctx = (* Warning will be printed later *) | ((loc, name), None, _) -> add_var_env tl ctx | ((loc, name), _, _) -> - let ctx = add_variable name loc ctx in + let ctx = senv_add_var name loc ctx in add_var_env tl ctx end in

let nctx = add_var_env decls ctx in @@ -192,12 +305,16 @@ and lexp_parse_let decls ctx = let linst, nctx = lexp_parse pinst ctx in let ltyp, nctx = lexp_parse ptype nctx in let nacc = ((loc, name), linst, ltyp)::acc in + let nctx = + env_add_var_info (0, (loc, name), linst, ltyp) nctx in (parse_decls tl nctx nacc) | ((loc, name), Some pinst, None) -> let linst, nctx = lexp_parse pinst ctx in (* This is where UnknownType are introduced *) (* need Inference HERE *) let nacc = ((loc, name), linst, UnknownType(loc))::acc in + let nctx = + env_add_var_info (0, (loc, name), linst, UnknownType(loc)) nctx in (parse_decls tl nctx nacc) (* Skip the variable *) | ((loc, name), None, _) -> @@ -215,13 +332,42 @@ and lexp_parse_all (p: pexp list) (ctx: lexp_context): | _ -> let lxp, new_ctx = lexp_parse (List.hd plst) ctx in (loop (List.tl plst) new_ctx (lxp::acc)) in (loop p ctx []) -;;

-(* Print back in CET (Close Enough Typer) easier to read *) - (* pretty ? * indent level * print_type? *) -type print_context = (bool * int * bool) +(* + * Type Inference + * --------------------- *) +(* Parsing a Pexp into an Lexp is really "elaboration", i.e. it needs to + * infer the types and perform macro-expansion. For won't really + * do any of that, but we can already start structuring it accordingly. + * + * More specifically, we do it with 2 mutually recursive functions: + * one takes a Pexp along with its expected type and return an Lexp + * of that type (hopefully), whereas the other takes a Pexp and + * infers its type (which it returns along with the Lexp). + * This is the idea of "bidirectional type checking", which minimizes + * the amount of "guessing" and/or annotations. Basically guessing/annotations + * is only needed at those few places where the code is not fully-normalized, + * which in normal programs is only in "let" definitions. + * So the rule of thumbs are: + * - use lexp_p_infer for destructors, and use lexp_p_check for constructors. + * - use lexp_p_check whenever you can. + *)

-let rec lexp_print_adv opt exp = +and lexp_p_infer (p : pexp) (env : lexp_context) : lexp * ltype = + let lxp, nctx = lexp_parse p env in + lxp, UnknownType(dummy_location) + +and lexp_p_check (env : lexp_context) (p : pexp) (t : ltype) : lexp = + match p with + | _ + -> let (e, inferred_t) = lexp_p_infer p env in + (* FIXME: check that inferred_t = t! *) + e +(* + * Printing + * --------------------- *) +(* So print can be called while parsing *) +and lexp_print_adv opt exp = let slexp_print = lexp_print_adv opt in (* short_lexp_print *) let (pty, indent, prtp) = opt in match exp with @@ -247,6 +393,11 @@ let rec lexp_print_adv opt exp = print_string "lambda ("; print_string (name ^ ": "); slexp_print ltype; print_string ") -> "; slexp_print lbody;

+ | Cons(vf, symbol) -> + let (loc, name) = symbol in + let ((loc, vname), idx) = vf in + print_string (name ^ "("); print_string (vname ^ ")"); + | Call(fname, args) -> begin (* /!\ Partial Print *) (* get function name *) let str = match fname with @@ -272,10 +423,50 @@ let rec lexp_print_adv opt exp = List.iter (fun arg -> print_string " "; print_arg arg) args; print_string ")" end

+ | Inductive (_, (_, name), _, ctors) -> + print_string ("inductive_ " ^ name ^ " "); + lexp_print_ctors opt ctors; + + | Case (_, target, tpe, map, dflt) -> begin + print_string "case "; slexp_print target; + print_string ": "; slexp_print tpe; + + if pty then print_string "\n"; + + let print_arg arg = + List.iter (fun v -> + match v with + | None -> print_string " _" + | Some (kind, (l, n)) -> print_string (" " ^ n)) arg in + + SMap.iter (fun key (loc, arg, exp) -> + make_line " " (indent * 4); + print_string ("| " ^ key); print_arg arg; + print_string " -> "; + slexp_print exp; print_string "; "; + if pty then print_string "\n";) + map; + + match dflt with + | None -> () + | Some df -> + make_line " " (indent * 4); + print_string "| _ -> "; slexp_print df; + print_string ";"; if pty then print_string "\n"; end + (* debug catch all *) | UnknownType (loc) -> print_string "unkwn"; - | _ -> print_string "expr" - + | _ -> print_string "Printint Not Implemented" + + +and lexp_print_ctors opt ctors = + SMap.iter (fun key value -> + print_string ("(" ^ key ^ ": "); + List.iter (fun (kind, arg) -> + lexp_print_adv opt arg; print_string " ") value; + print_string ")") + ctors + and lexp_print_decls opt decls = let (pty, indent, prtp) = opt in let print_type nm tp =

===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -147,20 +147,25 @@ let debug_pexp_print_all pexps = (* Print lexp with debug info *) let debug_lexp_print lxp = print_string " "; - let print_info msg loc expr= + let dloc = dummy_location in + let print_info msg loc lex = print_string msg; print_string "["; print_loc loc; print_string "]\t"; - lexp_print lxp in + lexp_print lex in + let tloc = lexp_location lxp in match lxp with - | Var((loc, _), _) -> print_info "Var " loc lxp - | Imm(s) -> print_info "Imm " dummy_location lxp - | Let(loc, _, _) -> print_info "Let " loc lxp - | Arrow(_, _, _, loc, _) -> print_info "Arrow " loc lxp - | Lambda(_, (loc, _), _, _) -> print_info "Lambda " loc lxp - | Call(_, _) -> print_info "Call " dummy_location lxp - | UnknownType(loc) -> print_info "UnknownType " loc lxp - | _ -> print_string "Nothing"; + | Var((loc, _), _) -> print_info "Var " tloc lxp + | Imm(s) -> print_info "Imm " tloc lxp + | Let(loc, _, _) -> print_info "Let " tloc lxp + | Arrow(_, _, _, loc, _) -> print_info "Arrow " tloc lxp + | Lambda(_, (loc, _), _, _) -> print_info "Lambda " tloc lxp + | Call(_, _) -> print_info "Call " tloc lxp + | Inductive(loc, _, _, _) -> print_info "Inductive " tloc lxp + | UnknownType(loc) -> print_info "UnknownType " tloc lxp + | Case(loc, _, _, _, _) -> print_info "Case " tloc lxp + | Cons (rf, sym) -> print_info "Cons " tloc lxp + | _ -> print_string "Debug Printing Not Implemented"; ;;

(* Print a list of lexp *)

===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -38,8 +38,26 @@ open Grammar open Pexp open Debruijn open Lparse +open Myers +open Eval

+(* pexp and lexp can be done together, one by one *) +let pexp_lexp_one node ctx = + let pxp = pexp_parse node in + lexp_parse pxp ctx +;; + +let pexp_lexp_all nodes ctx =

+ let rec loop nodes ctx acc = + match nodes with + | [] -> ((List.rev acc), ctx) + | hd::tl -> + let lxp, new_ctx = pexp_lexp_one hd ctx in + (loop tl new_ctx (lxp::acc)) in + (loop nodes ctx []) +;; + let main () =

let arg_n = Array.length Sys.argv in @@ -71,7 +89,7 @@ let main () =

(* get node sexp *) let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in - + (* get pexp *) let pexps = pexp_parse_all nodes in

@@ -87,7 +105,12 @@ let main () = print_title "Lexp"; debug_lexp_print_all lexps;

(* Eval Each Expression *) + print_title "Eval Print";

+ (* Eval One *) + let rctx = make_runtime_ctx in + let c, rctx = eval (List.hd lexps) rctx in + print_eval_result c

end ;;

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