Stefan pushed to branch master at Stefan / Typer

Commits: 4647f3a4 by Stefan Monnier at 2016-08-28T01:04:54-04:00 Try and break some dependencies. Remove unnecessary "Type" builtin

* src/opslexp.ml: Rename from typecheck.ml. Add erasure code. * src/lparse.ml (get_type0): Remove. (empty_lctx): Remove. (default_lctx, default_rctx): Merge. Add "Type" and "Type1". * src/lexp.ml (vdef, vref): Move to util.ml. * src/util.ml (vdef, vref): Move from lexp.ml. * src/env.ml: Don't open Myers. Remove false dependency on Debruijn. * src/elexp.ml: Don't depend on Lexp. Move erasure code to opslexp.ml. * src/debruijn.ml (env_extend): Inline the functions it uses. (senv_add_var, env_add_var_info): Remove. * src/builtin.ml (type2): New var. (sexp_eq): Use sexp_equal. * btl/types.typer (Type): Remove.

- - - - -

12 changed files:

- btl/types.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml → src/opslexp.ml - src/util.ml

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -35,7 +35,6 @@ % Base Types % -----------------------------------------------------

-Type = Built-in "Type"; Int = Built-in "Int"; Float = Built-in "Float"; String = Built-in "String";

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -54,7 +54,7 @@ open Builtin

open Env open Debruijn -module TC = Typecheck +module OL = Opslexp module EL = Elexp

(* how to handle arrow keys ? *) @@ -124,7 +124,8 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) =

let ierase_type (lexps: (ldecl list list * lexpr list)) = let (ldecls, lexprs) = lexps in - (EL.clean_toplevel ldecls), (List.map EL.erase_type lexprs) + (List.map OL.clean_decls ldecls), + (List.map OL.erase_type lexprs)

let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * lexp_context) = let pdecls, pexprs = pexps in @@ -158,7 +159,7 @@ let _raw_eval f str lctx rctx = let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in let pxps = pexp_decls_all nods in let lxps, lctx = lexp_p_decls pxps lctx in - let elxps = EL.clean_toplevel lxps in + let elxps = List.map OL.clean_decls lxps in let rctx = eval_decls_toplevel elxps rctx in (* This is for consistency with ieval *) [], lctx, rctx

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -81,13 +81,11 @@ let set_predef name lexp =

(* Builtin types *) 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 (SortLevel (SLn 0))) +let type1 = Sort (dloc, Stype (SortLevel (SLn 1))) +let type2 = Sort (dloc, Stype (SortLevel (SLn 2))) let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel) -let type_level = Builtin ((dloc, "TypeLevel"), type_level)

let op_binary t = Arrow (Aexplicit, None, t, dloc, Arrow (Aexplicit, None, t, dloc, t)) @@ -236,15 +234,8 @@ let int_eq loc depth args_val ctx =

let sexp_eq loc depth 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" - + | [Vsexp (s1); Vsexp (s2)] -> btyper (sexp_equal s1 s2) + | _ -> builtin_error loc "sexp_eq expects 2 sexp"

let open_impl loc depth args_val ctx =

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -100,23 +100,15 @@ let rec senv_lookup (name: string) (ctx: lexp_context): int = else *) raw_idx

-(* 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 (loc, name) ctx = - let ((n, map), e, f) = ctx in - (try let _ = senv_lookup name ctx in - debruijn_warning loc ("Variable Shadowing " ^ name); - with Not_found -> ()); - let nmap = StringMap.add name n map in - ((n + 1, nmap), e, f) - -let env_add_var_info var (ctx: lexp_context) = - let (a, env, f) = ctx in - (a, cons (var) env, f) - let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = - env_add_var_info (1, Some def, v, t) (senv_add_var def ctx) + let (loc, name) = def in + let ((n, map), env, f) = ctx in + (try let _ = senv_lookup name ctx in + debruijn_warning loc ("Variable Shadowing " ^ name); + with Not_found -> ()); + let nmap = StringMap.add name n map in + (* FIXME: Why a db_offset of 1? *) + ((n + 1, nmap), cons (1, Some def, v, t) env, f)

let _name_error loc estr str =

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -46,7 +46,7 @@ open Lexer open Lparse open Eval module EL = Elexp -module TC = Typecheck +module OL = Opslexp

(* definitions *) open Grammar @@ -335,7 +335,7 @@ let main () = let cctx = lctx_to_cctx ctx in (* run type check *) List.iter (fun (_, lxp, _) -> - let _ = TC.check cctx lxp in ()) flexps; + let _ = OL.check cctx lxp in ()) flexps;

print_string (" " ^ (make_line '-' 76)); print_string "\n";)); @@ -347,7 +347,7 @@ let main () = (if (get_p_option "lctx") then( print_lexp_ctx nctx; print_string "\n"));

- let clean_lxp = EL.clean_toplevel lexps in + let clean_lxp = List.map OL.clean_decls lexps in

(* Eval declaration *) let rctx = default_rctx in

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -34,11 +34,10 @@ open Sexp (* Sexp type *) open Pexp (* Aexplicit *)

-module L = Lexp module U = Util

-type vdef = L.vdef -type vref = L.vref +type vdef = U.vdef +type vref = U.vref type label = symbol

module SMap = U.SMap @@ -62,75 +61,6 @@ type elexp = (* Inductive takes a slot in the env that is why it need to be here *) | Inductive of U.location * label

-let rec erase_type (lxp: L.lexp): elexp = - - match lxp with - | L.Imm(s) -> Imm(s) - | L.Builtin(v, _) -> Builtin(v) - | L.Var(v) -> Var(v) - | L.Cons(_, s) -> Cons(s) - - | L.Lambda(kind, vdef, _, body) -> - if kind != Aerasable then - Lambda(vdef, erase_type body) - else - erase_type body - - | L.Let(l, decls, body) -> - Let(l, (clean_decls decls), (erase_type body)) - - | L.Call(fct, args) -> - Call((erase_type fct), (filter_arg_list args)) - - | L.Case(l, target, _, _, cases, default) -> - Case(l, (erase_type target), (clean_map cases), - (clean_maybe default)) - - | L.Susp(l, s) -> erase_type (L.push_susp l s) - - (* To be thrown out *) - | L.Arrow _ -> Type - | L.SortLevel _ -> Type - | L.Sort _ -> Type - (* Still useful to some extend *) - | L.Inductive(l, label, _, _) -> Inductive(l, label) - -and filter_arg_list lst = - let rec filter_arg_list lst acc = - match lst with - | (kind, lxp)::tl -> - let acc = if kind != Aerasable then - (erase_type lxp)::acc else acc in - filter_arg_list tl acc - | [] -> List.rev acc in - filter_arg_list lst [] - -and clean_decls decls = - List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls - -(* toplevel is a list of value *) -and clean_toplevel decls = - List.map (fun v -> clean_decls v) decls - -and clean_maybe lxp = - match lxp with - | Some lxp -> Some (erase_type lxp) - | None -> None - -and clean_map cases = - let clean_arg_list lst = - let rec clean_arg_list lst acc = - match lst with - | (kind, var)::tl -> - let acc = if kind != Aerasable then - var::acc else acc in - clean_arg_list tl acc - | [] -> List.rev acc in - clean_arg_list lst [] in - - SMap.mapi (fun key (l, args, expr) -> - (l, (clean_arg_list args), (erase_type expr))) cases - let rec elexp_location e = match e with | Imm s -> sexp_location s

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -34,12 +34,9 @@ open Util (* msg_error *) open Fmt (* make_title, table util *)

open Sexp -(* open Lexp ( * lexp_print *)

open Elexp -open Myers -open Debruijn - +module M = Myers

let dloc = dummy_location

@@ -56,7 +53,7 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of string | Vfloat of float - | Closure of string * elexp * (((string option * value_type) ref myers) * (int * int)) + | Closure of string * elexp * (((string option * value_type) ref M.myers) * (int * int)) | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy @@ -110,11 +107,11 @@ let value_name v =

(* Runtime Environ *) type env_cell = (string option * value_type) ref -type runtime_env = (env_cell myers) * (int * int) +type runtime_env = (env_cell M.myers) * (int * int)

-let make_runtime_ctx = (nil, (0, 0)) +let make_runtime_ctx = (M.nil, (0, 0))

-let get_rte_size (ctx: runtime_env): int = let (l, _) = ctx in length l +let get_rte_size (ctx: runtime_env): int = let (l, _) = ctx in M.length l

let is_free_var idx ctx = let (l, (osize, _)) = ctx in @@ -125,7 +122,7 @@ let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): value_type = let (l, _) = ctx in try ( - let ref_cell = (nth idx l) in + let ref_cell = (M.nth idx l) in let (tn, x) = !ref_cell in match (tn, name) with | (Some n1, Some n2) -> ( @@ -154,12 +151,12 @@ let rte_shift vref ctx =

let add_rte_variable name (x: value_type) (ctx: runtime_env): runtime_env = let (l, b) = ctx in - let lst = (cons (ref (name, x)) l) in + let lst = (M.cons (ref (name, x)) l) in (lst, b)

let set_rte_variable idx name (lxp: value_type) ctx = let (l, _) = ctx in - let ref_cell = (nth idx l) in + let ref_cell = (M.nth idx l) in let (n, _) = !ref_cell in

match (n, name) with @@ -177,16 +174,16 @@ let set_rte_variable idx name (lxp: value_type) ctx = (* it allow us to remove temporary variables when we enter a new scope * ) let local_ctx ctx = let (l, (_, _)) = ctx in - let osize = length l in + let osize = M.length l in (l, (osize, 0))

let select_n (ctx: runtime_env) n: runtime_env = let (l, a) = ctx in let r = ref nil in - let s = (length l) - 1 in + let s = (M.length l) - 1 in

for i = 0 to n - 1 do - r := (cons (nth (s - i) l) (!r)); + r := (M.cons (M.nth (s - i) l) (!r)); done;

((!r), a) @@ -195,7 +192,7 @@ let select_n (ctx: runtime_env) n: runtime_env = (* and create a clean context free of function arguments *) let temp_ctx (ctx: runtime_env): runtime_env = let (l, (osize, _)) = ctx in - let tsize = length l in + let tsize = M.length l in (* Check if temporary variables are present *) if tsize != osize then( (* remove them @@ -214,7 +211,7 @@ let nfirst_rte_var n ctx = loop 0 []

let print_myers_list l print_fun = - let n = (length l) - 1 in + let n = (M.length l) - 1 in

print_string (make_title " ENVIRONMENT "); make_rheader [(None, "INDEX"); @@ -225,7 +222,7 @@ let print_myers_list l print_fun = print_string " | "; ralign_print_int (n - i) 5; print_string " | "; - print_fun (nth (n - i) l); + print_fun (M.nth (n - i) l); done; print_string (make_sep '=')

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -40,9 +40,9 @@ open Lexp (* Varbind *) open Elexp open Builtin open Grammar - open Debruijn open Env +module OL = Opslexp

(* eval error are always fatal *) @@ -107,7 +107,7 @@ let rec _eval lxp ctx i: (value_type) = and get_predef_eval name ctx = let r = (get_rte_size ctx) - !builtin_size in let v = mkSusp (get_predef_raw name) (S.shift r) in - _eval (erase_type v) ctx 0 + _eval (OL.erase_type v) ctx 0

and eval_var ctx lxp v = let ((loc, name), idx) = v in @@ -388,7 +388,7 @@ let from_lctx (ctx: lexp_context) rm: runtime_env = let vxp = match exp with | Some lxp -> let octx = add_rte_variable name Vdummy (!rctx) in - let lxp = (erase_type lxp) in + let lxp = (OL.erase_type lxp) in (try (eval lxp octx) with e -> elexp_print lxp; print_string "\n"; raise e)

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -34,17 +34,8 @@ open Grammar (* open Unify *) module S = Subst

-(*************** DeBruijn indices for variables *********************) - -(* Occurrence of a variable's symbol: we use DeBruijn index, and for - * debugging purposes, we remember the name that was used in the source - * code. *) -type vdef = U.location * string -type db_index = int (* DeBruijn index. *) -type db_offset = int (* DeBruijn index offset. *) -type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vdef * db_index - +type vdef = U.vdef +type vref = U.vref

type label = symbol

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -48,7 +48,7 @@ open Eval open Grammar open Builtin

-module TC = Typecheck +module OL = Opslexp module EL = Elexp module SU = Subst

@@ -125,7 +125,6 @@ let build_var name ctx = Var((dloc, name), type0_idx)

(* build type0 from ctx *) -let get_type0 ctx = build_var "Type" ctx let get_int ctx = build_var "Int" ctx

(* shift all variables by an offset *) @@ -184,11 +183,10 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let lxp = _type_shift lxp sh in

let v = Arrow(kind, ovar, ltp, tloc, lxp) in - v, (get_type0 ctx) + v, type0

(* Pinductive *) | Pinductive (label, formal_args, ctors) -> - let type0 = get_type0 ctx in let nctx = ref ctx in (* (arg_kind * pvar * pexp option) list *) let formal = List.map (fun (kind, var, opxp) -> @@ -318,7 +316,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = * Built-in *) | Builtin _ -> e | _ -> - (if TC.conv_p inferred_t t then () else debug_msg ( + (if OL.conv_p inferred_t t then () else debug_msg ( print_string "1 exp "; lexp_print e; print_string "\n"; print_string "2 inf "; lexp_print inferred_t; print_string "\n"; print_string "3 Ann "; lexp_print t; print_string "\n"; @@ -413,7 +411,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | [] -> largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs (* Explicit-implicit argument. *) - -> (match TC.lexp_whnf ltp ctx with + -> (match OL.lexp_whnf ltp ctx with | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) when aname = aname' -> let parg = pexp_parse sarg in @@ -424,7 +422,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = "Explicit arg to non-function") | sarg :: sargs (* Process Argument *) - -> (match TC.lexp_whnf ltp ctx with + -> (match OL.lexp_whnf ltp ctx with | Arrow (Aexplicit, _, arg_type, _, ret_type) -> let parg = pexp_parse sarg in let larg = _lexp_p_check parg arg_type ctx i in @@ -439,7 +437,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =

let handle_funcall () =

- match TC.lexp_whnf body ctx with + match OL.lexp_whnf body ctx with | Builtin((_, "Built-in"), _) -> ( (* ------ SPECIAL ------ *) @@ -476,7 +474,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* user defined macro *) | false ->( (* Get the macro *) - let lxp = match TC.lexp_whnf body ctx with + let lxp = match OL.lexp_whnf body ctx with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | lxp -> print_string "\n"; @@ -488,7 +486,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let arg = olist2tlist_lexp sargs ctx in

let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = EL.erase_type lxp in + let elexp = OL.erase_type lxp in let rctx = (from_lctx ctx 0) in

_global_eval_trace := []; @@ -644,7 +642,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = (* build new function *) let arg = olist2tlist_lexp sargs ctx in let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = EL.erase_type lxp in + let elexp = OL.erase_type lxp in let rctx = (from_lctx ctx 0) in

(* get a list of declaration *) @@ -931,15 +929,13 @@ let lexp_parse_all p ctx = _lexp_parse_all p ctx 1 * --------------------------------------------------------- *)

(* Make lxp context with built-in types *) -let empty_lctx = - let lctx = make_lexp_context in - let lxp = Builtin((dloc, "Built-in"), type0) in - env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 - -let default_lctx = +let default_lctx, default_rctx =

(* Empty context *) let lctx = make_lexp_context in + let lctx = env_extend lctx (dloc, "Type1") (LetDef type1) type2 in + let lctx = env_extend lctx (dloc, "Type") (LetDef type0) type1 in + (* FIXME: Add builtins directly here. *) let lxp = Builtin((dloc, "Built-in"), type0) in let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in

@@ -962,7 +958,7 @@ let default_lctx = builtin_size := get_size lctx;

(* Once default builtin are set we can populate the predef table *) - try + let lctx = try List.iter (fun name -> let idx = senv_lookup name lctx in let v = Var((dloc, name), idx) in @@ -970,30 +966,11 @@ let default_lctx = (* -- DONE -- *) lctx with e -> - lctx - - -(* Make runtime context with built-in types *) -let default_rctx = - (* Empty context *) - let lctx = make_lexp_context in - let lxp = Builtin((dloc, "Built-in"), type0) in - let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in - - (* Read BTL files *) - let pres = prelex_file (!btl_folder ^ "types.typer") in - let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let pxps = pexp_decls_all nods in - - _parsing_internals := true; - let d, lctx = lexp_p_decls pxps lctx in - _parsing_internals := false; - + lctx in let rctx = make_runtime_ctx in - let rctx = eval_decls_toplevel (EL.clean_toplevel d) rctx in - _global_eval_trace := []; - rctx + let rctx = eval_decls_toplevel (List.map OL.clean_decls d) rctx in + _global_eval_trace := []; + lctx, rctx

(* String Parsing * --------------------------------------------------------- *) @@ -1023,13 +1000,13 @@ let lexp_decl_str str lctx =

let _eval_expr_str str lctx rctx silent = let lxps = lexp_expr_str str lctx in - let elxps = List.map EL.erase_type lxps in + let elxps = List.map OL.erase_type lxps in (eval_all elxps rctx silent)

let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false

let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in - let elxps = (EL.clean_toplevel lxps) in + let elxps = (List.map OL.clean_decls lxps) in (eval_decls_toplevel elxps rctx), lctx

===================================== src/typecheck.ml → src/opslexp.ml ===================================== --- a/src/typecheck.ml +++ b/src/opslexp.ml @@ -1,4 +1,4 @@ -(* typecheck.ml --- Check a Lexp expression's type +(* opslexp.ml --- Operations on Lexps

Copyright (C) 2011-2016 Free Software Foundation, Inc.

@@ -28,10 +28,12 @@ module P = Pexp (* open Myers *) (* open Grammar *) open Lexp +module E = Elexp +module L = Lexp

(* open Unify *) module S = Subst -module L = List +(* module L = List *) module B = Builtin module DB = Debruijn

@@ -177,7 +179,7 @@ let rec check ctx e = | Susp (e, s) -> check ctx (push_susp e s) | Let (_, defs, e) -> let tmp_ctx = - L.fold_left (fun ctx (v, e, t) + List.fold_left (fun ctx (v, e, t) -> (match check ctx t with | Sort (_, Stype _) -> () | _ -> (U.msg_error "TC" (lexp_location t) @@ -185,12 +187,12 @@ let rec check ctx e = Myers.cons (0, Some v, ForwardRef, t) ctx) ctx defs in let (new_ctx, _) = - L.fold_left (fun (ctx,recursion_offset) (v, e, t) + List.fold_left (fun (ctx,recursion_offset) (v, e, t) -> let t' = check tmp_ctx e in assert_type e t t'; (Myers.cons (recursion_offset, Some v, LetDef e, t) ctx, recursion_offset - 1)) - (ctx, L.length defs) + (ctx, List.length defs) defs in check new_ctx e | Arrow (ak, v, t1, l, t2) @@ -216,7 +218,7 @@ let rec check ctx e = check (Myers.cons (0, Some v, Variable, t) ctx) e)) | Call (f, args) -> let ft = check ctx f in - L.fold_left (fun ft (ak,arg) + List.fold_left (fun ft (ak,arg) -> let at = check ctx arg in match ft with | Arrow (ak', v, t1, l, t2) @@ -299,8 +301,8 @@ let rec check ctx e = :: indtype fargs (start_index - 1) in let rec fieldargs fieldtypes = match fieldtypes with - | [] -> Call (it, indtype fargs (L.length fieldtypes - + L.length fargs - 1)) + | [] -> Call (it, indtype fargs (List.length fieldtypes + + List.length fargs - 1)) | (ak, vd, ftype) :: fieldtypes -> Arrow (ak, vd, ftype, lexp_location ftype, fieldargs fieldtypes) in @@ -315,3 +317,71 @@ let rec check ctx e = "Cons of a non-inductive type!"; B.type_int))

+(*********** Type erasure, before evaluation. *****************) + +let rec erase_type (lxp: L.lexp): E.elexp = + + match lxp with + | L.Imm(s) -> E.Imm(s) + | L.Builtin(v, _) -> E.Builtin(v) + | L.Var(v) -> E.Var(v) + | L.Cons(_, s) -> E.Cons(s) + + | L.Lambda(kind, vdef, _, body) -> + if kind != P.Aerasable then + E.Lambda(vdef, erase_type body) + else + erase_type body + + | L.Let(l, decls, body) -> + E.Let(l, (clean_decls decls), (erase_type body)) + + | L.Call(fct, args) -> + E.Call((erase_type fct), (filter_arg_list args)) + + | L.Case(l, target, _, _, cases, default) -> + E.Case(l, (erase_type target), (clean_map cases), + (clean_maybe default)) + + | L.Susp(l, s) -> erase_type (L.push_susp l s) + + (* To be thrown out *) + | L.Arrow _ -> E.Type + | L.SortLevel _ -> E.Type + | L.Sort _ -> E.Type + (* Still useful to some extend *) + | L.Inductive(l, label, _, _) -> E.Inductive(l, label) + +and filter_arg_list lst = + let rec filter_arg_list lst acc = + match lst with + | (kind, lxp)::tl -> + let acc = if kind != P.Aerasable then + (erase_type lxp)::acc else acc in + filter_arg_list tl acc + | [] -> List.rev acc in + filter_arg_list lst [] + +and clean_decls decls = + List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls + +and clean_maybe lxp = + match lxp with + | Some lxp -> Some (erase_type lxp) + | None -> None + +and clean_map cases = + let clean_arg_list lst = + let rec clean_arg_list lst acc = + match lst with + | (kind, var)::tl -> + let acc = if kind != P.Aerasable then + var::acc else acc in + clean_arg_list tl acc + | [] -> List.rev acc in + clean_arg_list lst [] in + + SMap.mapi (fun key (l, args, expr) -> + (l, (clean_arg_list args), (erase_type expr))) cases + +

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -23,12 +23,22 @@ this program. If not, see http://www.gnu.org/licenses/. *) module SMap = Map.Make (struct type t = string let compare = String.compare end)

- type charpos = int type bytepos = int type location = { file : string; line : int; column : charpos } let dummy_location = {file=""; line=0; column=0}

+(*************** DeBruijn indices for variables *********************) + +(* Occurrence of a variable's symbol: we use DeBruijn index, and for + * debugging purposes, we remember the name that was used in the source + * code. *) +type vdef = location * string +type db_index = int (* DeBruijn index. *) +type db_offset = int (* DeBruijn index offset. *) +type db_revindex = int (* DeBruijn index counting from the root. *) +type vref = vdef * db_index + type bottom = | B_o_t_t_o_m_ of bottom

(* print debug info *)

View it on GitLab: https://gitlab.com/monnier/typer/commit/4647f3a454f9f422364a308b21f9df9d92e0...