Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Août 2016
- 2 participants
- 11 discussions
[Git][monnier/typer][master] * btl/types.typer (sexp_dispatch_): Generalize type
by Stefan 29 Aoû '16
by Stefan 29 Aoû '16
29 Aoû '16
Stefan pushed to branch master at Stefan / Typer
Commits:
89b8df07 by Stefan Monnier at 2016-08-28T22:58:52-04:00
* btl/types.typer (sexp_dispatch_): Generalize type
- - - - -
2 changed files:
- btl/types.typer
- samples/quote.typer
Changes:
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -96,25 +96,28 @@ tail = lambda a ≡>
% Macro
% -----------------------------------------------------
-block_ = Built-in "block_" ((List Sexp) -> Sexp);
-symbol_ = Built-in "symbol_" (String -> Sexp);
-string_ = Built-in "string_" (String -> Sexp);
-node_ = Built-in "node_" (Sexp -> (List Sexp) -> Sexp);
-integer_ = Built-in "integer_" (Int -> Sexp);
-float_ = Built-in "float_" (Float -> Sexp);
+block_ = Built-in "block_" (List Sexp -> Sexp);
+symbol_ = Built-in "symbol_" (String -> Sexp);
+string_ = Built-in "string_" (String -> Sexp);
+node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp);
+integer_ = Built-in "integer_" (Int -> Sexp);
+float_ = Built-in "float_" (Float -> Sexp);
% Macro : Type;
-Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp));
+Macro = inductive_ (dMacro) (Macro_ (List Sexp -> Sexp));
Macro_ = inductive-cons Macro Macro_ ;
-sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp
- -> (Sexp -> List Sexp -> Sexp)
- -> (String -> Sexp)
- -> (String -> Sexp)
- -> (Int -> Sexp)
- -> (Float -> Sexp)
- -> (List Sexp -> Sexp)
- -> Sexp);
+sexp_dispatch_ = Built-in "sexp_dispatch_" (
+ (a : Type) ≡>
+ Sexp
+ -> (Sexp -> List Sexp -> a)
+ -> (String -> a)
+ -> (String -> a)
+ -> (Int -> a)
+ -> (Float -> a)
+ -> (List Sexp -> a)
+ -> a
+ );
% -----------------------------------------------------
% Monads
=====================================
samples/quote.typer
=====================================
--- a/samples/quote.typer
+++ b/samples/quote.typer
@@ -44,7 +44,7 @@ quote' = lambda (x : List Sexp) ->
let target = head Sexp x;
tl = tail Sexp x;
- rhd = sexp_dispatch_ target
+ rhd = sexp_dispatch_ (a := Sexp) target
node symbol string integer float block;
rtl = case tl
View it on GitLab: https://gitlab.com/monnier/typer/commit/89b8df076d92eadb9ccf9244db65a3b8ada…
1
0
[Git][monnier/typer][master] * btl/types.typer (length, head, tail): Make type erasable
by Stefan 29 Aoû '16
by Stefan 29 Aoû '16
29 Aoû '16
Stefan pushed to branch master at Stefan / Typer
Commits:
f33ba8a5 by Stefan Monnier at 2016-08-28T22:27:46-04:00
* btl/types.typer (length, head, tail): Make type erasable
* src/opslexp.ml (erase_type): Adjust indices after removing an
erasable formal argument.
- - - - -
2 changed files:
- btl/types.typer
- src/opslexp.ml
Changes:
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -71,22 +71,22 @@ List = inductive_ (dList (a : Type)) (nil) (cons a (List a));
nil = inductive-cons List nil;
cons = inductive-cons List cons;
-length : (a : Type) => List a -> Int;
-length = lambda a =>
+length : (a : Type) ≡> List a -> Int;
+length = lambda a ≡>
lambda xs ->
case xs
| nil => 0
| cons hd tl => (1 + (length(a := a) tl));
-head : (a : Type) => List a -> a;
-head = lambda a =>
+head : (a : Type) ≡> List a -> a;
+head = lambda a ≡>
lambda xs ->
case xs
| nil => nil
| cons hd tl => hd;
-tail : (a : Type) => List a -> List a;
-tail = lambda a =>
+tail : (a : Type) ≡> List a -> List a;
+tail = lambda a ≡>
lambda xs ->
case xs
| nil => nil
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -327,11 +327,12 @@ let rec erase_type (lxp: L.lexp): E.elexp =
| 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.Lambda (P.Aerasable, _, _, body) ->
+ (* The var shouldn't appear in body, basically, but we need
+ * to adjust the debruijn indices of other vars, hence the subst. *)
+ erase_type (L.push_susp body (S.substitute Builtin.type0))
+ | L.Lambda (_, vdef, _, body) ->
+ E.Lambda (vdef, erase_type body)
| L.Let(l, decls, body) ->
E.Let(l, (clean_decls decls), (erase_type body))
@@ -349,7 +350,7 @@ let rec erase_type (lxp: L.lexp): E.elexp =
| L.Arrow _ -> E.Type
| L.SortLevel _ -> E.Type
| L.Sort _ -> E.Type
- (* Still useful to some extend *)
+ (* Still useful to some extent. *)
| L.Inductive(l, label, _, _) -> E.Inductive(l, label)
and filter_arg_list lst =
View it on GitLab: https://gitlab.com/monnier/typer/commit/f33ba8a5bf9221188f9d82534981088be75…
1
0
Stefan pushed to branch master at Stefan / Typer
Commits:
277049a0 by Stefan Monnier at 2016-08-28T01:06:43-04:00
* src/lparse.ml (get_int): Remove
(_lexp_p_infer): Use type_int instead.
- - - - -
1 changed file:
- src/lparse.ml
Changes:
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -124,9 +124,6 @@ let build_var name ctx =
let type0_idx = senv_lookup name ctx in
Var((dloc, name), type0_idx)
-(* build type0 from ctx *)
-let get_int ctx = build_var "Int" ctx
-
(* shift all variables by an offset *)
let senv_lookup name ctx =
senv_lookup name ctx + !_shift_glob
@@ -146,7 +143,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
(* Block/String/Integer/Float *)
| Pimm value -> (Imm(value),
match value with
- | Integer _ -> get_int ctx
+ | Integer _ -> type_int
| Float _ -> type_float
| String _ -> type_string;
| _ -> lexp_error tloc "Could not find type";
View it on GitLab: https://gitlab.com/monnier/typer/commit/277049a0fad4331ae4b0ca8c16a4d63f447…
1
0
[Git][monnier/typer][master] Try and break some dependencies. Remove unnecessary "Type" builtin
by Stefan 28 Aoû '16
by Stefan 28 Aoû '16
28 Aoû '16
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/4647f3a454f9f422364a308b21f9df9d92e…
1
0
[Git][monnier/typer][master] * src/lparse.ml (lexp_call): Rewrite to work one-arg at a time
by Stefan 27 Aoû '16
by Stefan 27 Aoû '16
27 Aoû '16
Stefan pushed to branch master at Stefan / Typer
Commits:
d05adcab by Stefan Monnier at 2016-08-27T10:50:37-04:00
* src/lparse.ml (lexp_call): Rewrite to work one-arg at a time
Add basic support for explicit-implicit args. Use lexp_whnf.
(lexp_call.get_return_type): Remove.
(_lexp_p_infer, lexp_read_pattern, lexp_decls_macro):
Adjust to new env_lookup_expr.
(_lexp_parse_all.loop): Don't use List.hd when not needed.
* src/typecheck.ml (lexp_whnf): New function.
* src/debruijn.ml (env_lookup_expr): Return an option.
* src/builtin.ml (get_attribute_impl, declexpr_impl): Adjust accordingly.
* btl/types.typer (length): One more explicit-implicit arg.
- - - - -
7 changed files:
- DESIGN
- btl/types.typer
- src/builtin.ml
- src/debruijn.ml
- src/lexp.ml
- src/lparse.ml
- src/typecheck.ml
Changes:
=====================================
DESIGN
=====================================
--- a/DESIGN
+++ b/DESIGN
@@ -1655,6 +1655,60 @@ Look ma! No axioms!
Or almost: with these classical definitions we cannot prove the classical
axiom of choice as a theorem, so if you need it, you have to add it as an axiom.
+* Co-induction
+
+Coinductive data is basically defined by observation, so what is often
+written as something like
+
+ codata Stream α
+ | Nil
+ | Cons α (Stream α)
+
+really means something like:
+
+ type StreamAccessor
+ | Car | Cdr
+ Stream α =
+ (a : StreamAccessor)
+ -> case a
+ | Car => Maybe α
+ | Cdr => Maybe (Stream α)
+
+And with length, that could turn into:
+
+ type StreamAccessor n
+ | Empty? | Car (n > 0) | Cdr (n > 0)
+ Stream α n =
+ (a : StreamAccessor n)
+ -> case a
+ | Empty? => Maybe (n > 0)
+ | Car _ => α
+ | Cdr _ => Stream α (n - 1)
+
+In either case, the definition of `Stream` is recursive and doesn't follow
+the supported forms of recursion in CIC (i.e. inductive types and inductive
+functions) so it requires ad-hoc support.
+
+It would help to have something akin to the "impredicative encoding" of
+inductive types to get an intuitive idea of what should be safe and what
+might be dangerous.
+
+Let's try for `Stream α`:
+
+ Stream α =
+ (β : Type) -> (a : StreamAccessor)
+ -> (case a
+ | Car => Maybe α -> β
+ | Cdr => Maybe β -> β)
+ -> β
+
+So we'd define
+
+ numbers' n β a = case a
+ | Car => λ f -> f (just n)
+ | Cdr => λ f -> f (just ¿?¿) %% (numbers' (n + 1))
+ numbers = numbers' 0
+
* Papers
** BigBang: Designing a statically typed scripting language
** Dependently typed Racket
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -77,7 +77,7 @@ length = lambda a =>
lambda xs ->
case xs
| nil => 0
- | cons hd tl => (1 + (length a tl));
+ | cons hd tl => (1 + (length(a := a) tl));
head : (a : Type) => List a -> a;
head = lambda a =>
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -303,7 +303,7 @@ let get_attribute_impl loc largs ctx ftype =
| _ -> builtin_error loc "get-attribute expects two arguments" in
let lxp = get_property ctx (vi, vn) (ai, an) in
- let ltype = env_lookup_expr ctx ((loc, an), ai) in
+ let Some ltype = env_lookup_expr ctx ((loc, an), ai) in
lxp, ltype
let new_attribute_impl loc largs ctx ftype =
@@ -331,7 +331,7 @@ let declexpr_impl loc largs ctx ftype =
| [Var((_, vn), vi)] -> (vi, vn)
| _ -> builtin_error loc "declexpr expects one argument" in
- let lxp = env_lookup_expr ctx ((loc, vn), vi) in
+ let Some lxp = env_lookup_expr ctx ((loc, vn), vi) in
let ltp = env_lookup_type ctx ((loc, vn), vi) in
lxp, ftype
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -34,6 +34,7 @@
open Util
open Lexp
+module L = Lexp
open Myers
open Fmt
(*open Typecheck env_elem and env_type *)
@@ -146,15 +147,13 @@ let env_lookup_type ctx (v : vref): lexp =
let (_, _, _, ltp) = _env_lookup ctx v in
mkSusp ltp (S.shift (idx + 0))
-let env_lookup_expr ctx (v : vref): lexp =
+let env_lookup_expr ctx (v : vref): lexp option =
let (_, idx) = v in
let (r, _, lxp, _) = _env_lookup ctx v in
-
- let lxp = match lxp with
- | LetDef lxp -> lxp
- | _ -> Sort (dummy_location, Stype (SortLevel (SLn 0))) in
-
- mkSusp lxp (S.shift (idx + 1 - r))
+ match lxp with
+ | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r)))
+ (* FIXME: why Sort here? *)
+ | _ -> None
let env_lookup_by_index index (ctx: lexp_context): env_elem =
(Myers.nth index (_get_env ctx))
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -351,105 +351,6 @@ let lexp_to_string e =
| Builtin _ -> "Builtin"
| _ -> "lexp_to_string: not implemented"
-
-
-(* Apply substitution `s' and then reduce to weak head normal form.
- * WHNF implies:
- * - Not a Let.
- * - Not a let-bound variable.
- * - Not a Susp.
- * - Not an instantiated Metavar.
- * - Not a Call (Lambda _).
- * - Not a Call (Call _).
- * - Not a Call (_, []).
- * - Not a Case (Cons _).
- * - Not a Call (MetaSet, ..).
- *)
-(* let rec lexp_whnf (s : lexp VMap.t) e =
- * match e with
- * | (Imm _ | Builtin _) -> e
- * | Sort (_, (StypeLevel | StypeOmega | Stype (SortLevel (SLn _)))) -> e
- * | Sort (l, Stype e) -> Sort (l, Stype (mk_susp s e))
- * | SortLevel (SLn _) -> e
- * | SortLevel (SLsucc e) ->
- * (match lexp_whnf s e with
- * | SortLevel (SLn n) -> SortLevel (SLn (n + 1))
- * | e' -> SortLevel (SLsucc e'))
- * | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, mk_susp s t1, l, mk_susp s t2)
- * | Lambda (ak, v, t, e) -> Lambda (ak, v, mk_susp s t, mk_susp s e)
- * | Call (f, args) ->
- * List.fold_left (fun e (ak,arg) ->
- * match e with
- * | Builtin (b,_,_) ->
- * (match builtin_reduce b [] arg with
- * | Some e -> e
- * | _ -> Call (e, [(ak, mk_susp s arg)]))
- * | Call (Builtin (b,_,_), args) ->
- * (match builtin_reduce b args arg with
- * | Some e -> e
- * | _ -> Call (e, [(ak, mk_susp s arg)]))
- * | Lambda (_, (_,v), _, body)
- * -> lexp_whnf (VMap.add v (mk_susp s arg) VMap.empty) body
- * | Call (f, args) -> Call (f, (ak, mk_susp s arg) :: args)
- * | _ -> Call (e, [(ak, mk_susp s arg)]))
- * (lexp_whnf s f) args
- * | Inductive (id, t, branches)
- * -> Inductive (id, mk_susp s t, SMap.map (mk_susp s) branches)
- * | Cons (t, tag) -> Cons (mk_susp s t, tag)
- * | Case (l, e, t, branches, default)
- * -> let select name actuals
- * = try let (l,formals,body) = SMap.find name branches in
- * lexp_whnf (List.fold_left2 (fun s (_,a) (_,(_,f)) ->
- * VMap.add f a s)
- * s actuals formals)
- * body
- * with Not_found ->
- * match default with
- * | None -> msg_error l "Unmatched constructor";
- * mk_meta_dummy VMap.empty l
- * | Some body -> lexp_whnf s body
- * in
- * (match lexp_whnf s e with
- * | Cons (_, (_,name)) -> select name []
- * | Call (Cons (_, (_, name)), actuals) -> select name actuals
- * | e -> Case (l, e, t,
- * SMap.map (fun (l,args,body)
- * -> (l, args, mk_susp s body))
- * branches,
- * match default with Some e -> Some (mk_susp s e)
- * | None -> None))
- * | Susp (s', e) -> lexp_whnf (lexp_subst_subst s s') e
- * | Metavar (_,MetaFoF,r) ->
- * (match !r with | MetaSet e -> lexp_whnf s e | _ -> e)
- * | Metavar (l, MetaGraft s', r) ->
- * let s' = (lexp_subst_subst s s') in
- * (match !r with MetaSet e -> lexp_whnf s' e
- * (\* FIXME: filter s' w.r.t `venv'. *\)
- * | MetaUnset (venv,_,_) -> Metavar (l, MetaGraft s', r))
- * (\* BEWARE: we need a recursive environment, which is kinda painful
- * * to create (tho we could use ref'cells), so we use a hack instead. *\)
- * | Let (l,decls,body)
- * -> let decls' = List.map (fun (v, e, t) -> (v, mk_susp s e, mk_susp s t))
- * decls in
- * let s' = List.fold_left (fun s ((l',v),e,t) ->
- * VMap.add v (Let (l, decls', Var (l', v))) s)
- * s decls
- * in lexp_whnf s' body
- * | Var (l,v)
- * -> (try match VMap.find v s with
- * (\* Hack attack! A recursive binding, let's unroll it here. *\)
- * | Let (_,decls,Var (_, v')) when v = v'
- * -> let e = List.fold_left (fun e ((_,v'), e', _) ->
- * if v = v' then e' else e)
- * (\* This metavar is just a placeholder
- * * which should be dropped. *\)
- * (mk_meta_dummy VMap.empty l) decls
- * (\* Here we stay in `s' to keep the recursive bindings. *\)
- * in lexp_whnf s (lexp_copy e)
- * | e -> lexp_whnf VMap.empty (lexp_copy e)
- * with Not_found -> e) *)
-
-
(*
(* In non-recursion calls, `s' is always empty. *)
let lexp_conv_p env = lexp_conv_p env VMap.empty
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -235,7 +235,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
(* An inductive type named type_name must be in the environment *)
try let idx = senv_lookup type_name ctx in
(* Check if the constructor exists *)
- let idt = env_lookup_expr ctx (vr, idx) in
+ let Some idt = env_lookup_expr ctx (vr, idx) in
(* make Base type *)
let inductive_type = Var((loc, type_name), idx) in
@@ -391,8 +391,8 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =
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 =
- let loc = pexp_location fun_name in
+and lexp_call (func: pexp) (sargs: sexp list) ctx i =
+ let loc = pexp_location func in
let from_lctx ctx = try (from_lctx ctx)
with e ->(
@@ -400,60 +400,70 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
print_eval_trace ();
raise e) in
- (* consume Arrows and args together *)
- let rec get_return_type name i ltp args =
- match (nosusp ltp), args with
- | _, [] -> ltp
- | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl)
- | _, _ -> lexp_warning loc
- (name ^ " was provided with too many args. Expected: " ^
- (string_of_int i)); ltp in
-
(* Vanilla : sqr is inferred and (lambda x -> x * x) is returned
* Macro : sqr is returned
* Constructor : a constructor is returned
* Anonymous : lambda *)
(* retrieve function's body *)
- let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in
+ let body, ltp = _lexp_p_infer func ctx (i + 1) in
let ltp = nosusp ltp in
- let handle_named_call (loc, name) =
+ let rec handle_fun_args largs sargs ltp = match sargs with
+ | [] -> largs, ltp
+ | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs
+ (* Explicit-implicit argument. *)
+ -> (match TC.lexp_whnf ltp ctx with
+ | Arrow (ak, Some (_, aname'), arg_type, _, ret_type)
+ when aname = aname'
+ -> let parg = pexp_parse sarg in
+ let larg = _lexp_p_check parg arg_type ctx i in
+ handle_fun_args ((ak, larg) :: largs) sargs
+ (L.mkSusp ret_type (S.substitute larg))
+ | _ -> lexp_fatal (sexp_location sarg)
+ "Explicit arg to non-function")
+ | sarg :: sargs
+ (* Process Argument *)
+ -> (match TC.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
+ handle_fun_args ((Aexplicit, larg) :: largs) sargs
+ (L.mkSusp ret_type (S.substitute larg))
+ | Arrow _ as t -> lexp_print t; print_string "\n";
+ sexp_print sarg; print_string "\n";
+ lexp_fatal (sexp_location sarg)
+ "Expected non-explicit arg"
+ | _ -> lexp_fatal (sexp_location sarg)
+ "Explicit arg to non-function") in
+
+ let handle_funcall () =
+
+ match TC.lexp_whnf body ctx with
+ | Builtin((_, "Built-in"), _)
+ -> (
+ (* ------ SPECIAL ------ *)
+ match !_parsing_internals, sargs with
+ | true, [String (_, str)] ->
+ Builtin((loc, str), ltp), ltp
+
+ | true, [String (_, str); stp] ->
+ let ptp = pexp_parse stp in
+ let ltp, _ = _lexp_p_infer ptp ctx (i + 1) in
+ Builtin((loc, str), ltp), ltp
+
+ | true, _ ->
+ lexp_error loc "Wrong Usage of \"Built-in\"";
+ dlxp, dltype
+
+ | false, _ ->
+ lexp_error loc "Use of \"Built-in\" in user code";
+ dlxp, dltype)
+
+ | e ->
(* Process Arguments *)
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- let new_args = List.map (fun g -> (Aexplicit, g)) largs in
-
- try (* Check if the function was defined *)
- let idx = senv_lookup name ctx in
- let vf = (make_var name idx loc) in
-
- match nosusp (env_lookup_expr ctx ((loc, name), idx)) with
- | Builtin((_, "Built-in"), _) ->(
- (* ------ SPECIAL ------ *)
- match !_parsing_internals, largs with
- | true, [Imm(String (_, str))] ->
- Builtin((loc, str), ltp), ltp
-
- | true, [Imm(String (_, str)); ltp] ->
- Builtin((loc, str), ltp), ltp
-
- | true, _ ->
- lexp_error loc "Wrong Usage of \"Built-in\"";
- dlxp, dltype
-
- | false, _ ->
- lexp_error loc "Use of \"Built-in\" in user code";
- dlxp, dltype)
-
- | e ->
- let ret_type = get_return_type name 0 ltp new_args in
- Call(vf, new_args), ret_type
-
- with Not_found ->
- lexp_error loc ("The function \"" ^ name ^ "\" was not defined");
- let vf = (make_var name (-1) loc) in
- Call(vf, new_args), ltp in
+ let largs, ret_type = handle_fun_args [] sargs ltp in
+ Call (body, List.rev largs), ret_type in
let handle_macro_call (loc, name) =
(* check for builtin *)
@@ -465,20 +475,10 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
(* user defined macro *)
| false ->(
- (* look up for definition *)
- let idx = try senv_lookup name ctx
- with Not_found ->
- lexp_fatal loc ("Could not find Variable: " ^ name) in
-
(* Get the macro *)
- let lxp = try env_lookup_expr ctx ((loc, name), idx)
- with Not_found ->
- lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^
- " is not a correct index.") in
-
- let lxp = match nosusp lxp with
+ let lxp = match TC.lexp_whnf body ctx with
| Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
- | _ ->
+ | lxp ->
print_string "\n";
print_string (lexp_to_string lxp); print_string "\n";
lexp_print lxp; print_string "\n";
@@ -512,36 +512,12 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
_lexp_p_infer pxp ctx (i + 1)) in
(* determine function type *)
- match fun_name, ltp with
- (* Anonymous *)
- | ((Plambda _), _) ->
- (* Process Arguments *)
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- let new_args = List.map (fun g -> (Aexplicit, g)) largs in
- Call(body, new_args), ltp
-
- | (Pvar (l, n), Var((_, "Macro"), _)) ->
- (* FIXME: check db_idx points to a Macro type *)
- handle_macro_call (l, n)
-
- (* Call to Vanilla or constructor *)
- | (Pvar v, _) -> handle_named_call v
-
- (* Constructor. This case is rarely used *)
- | (Pcons(_, v), _) -> handle_named_call v
-
- | Pcall(fct, sargs2), ltp ->
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- let new_args = List.map (fun g -> (Aexplicit, g)) largs in
- let body, ltp = lexp_call fct sargs2 ctx (i + 1) in
- Call(body, new_args), ltp
-
- | e, _ ->
- pexp_print e; print_string "\n";
- print_string ((pexp_to_string e) ^ "\n");
- lexp_fatal (pexp_location e) "This expression cannot be called"
+ match func, ltp with
+ (* FIXME: Rather than check a var name, define a builtin for it. *)
+ (* FIXME: Don't force func to be a Pvar. *)
+ | (Pvar (l, n), Var((_, "Macro"), _)) -> handle_macro_call (l, n)
+ (* FIXME: Handle special-forms here as well! *)
+ | _ -> handle_funcall ()
(* Read a pattern and create the equivalent representation *)
@@ -555,15 +531,15 @@ and lexp_read_pattern pattern exp target ctx:
| Ppatvar ((loc, name) as var) ->(
try(
let idx = senv_lookup name ctx in
- match nosusp (env_lookup_expr ctx ((loc, name), idx)) with
- (* We are matching a constructor *)
- | Cons _ -> (name, loc, []), ctx
+ match env_lookup_expr ctx ((loc, name), idx) with
+ (* We are matching a constructor *)
+ | Some (Cons _) -> (name, loc, []), ctx
- (* name is defined but is not a constructor *)
- (* it technically could be ... (expr option) *)
- (* What about Var -> Cons ? *)
- | _ -> let nctx = env_extend ctx var (LetDef target) dltype in
- (name, loc, []), nctx)
+ (* name is defined but is not a constructor *)
+ (* it technically could be ... (expr option) *)
+ (* What about Var -> Cons ? *)
+ | _ -> let nctx = env_extend ctx var (LetDef target) dltype in
+ (name, loc, []), nctx)
(* would it not make a default match too? *)
with Not_found ->
@@ -641,9 +617,9 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) =
" is not a correct index.") in
(* get stored function *)
- let lxp = match nosusp lxp with
- | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
- | _ -> print_string "\n";
+ let lxp = match lxp with
+ | Some (Call(Var((_, "Macro_"), _), [(_, fct)])) -> fct
+ | Some lxp -> print_string "\n";
print_string (lexp_to_string lxp); print_string "\n";
lexp_print lxp; print_string "\n";
lexp_fatal loc "Macro is ill formed" in
@@ -846,8 +822,8 @@ and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list =
let rec loop (plst: pexp list) ctx (acc: lexp list) =
match plst with
| [] -> (List.rev acc)
- | _ -> let lxp, _ = _lexp_p_infer (List.hd plst) ctx (i + 1) in
- (loop (List.tl plst) ctx (lxp::acc)) in
+ | pe :: plst -> let lxp, _ = _lexp_p_infer pe ctx (i + 1) in
+ (loop plst ctx (lxp::acc)) in
(loop p ctx [])
=====================================
src/typecheck.ml
=====================================
--- a/src/typecheck.ml
+++ b/src/typecheck.ml
@@ -33,6 +33,7 @@ open Lexp
module S = Subst
module L = List
module B = Builtin
+module DB = Debruijn
let conv_erase = true (* If true, conv ignores erased terms. *)
@@ -99,6 +100,28 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool =
and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2
+(* Reduce to weak head normal form.
+ * WHNF implies:
+ * - Not a Let.
+ * - Not a let-bound variable.
+ * - Not a Susp.
+ * - Not an instantiated Metavar.
+ * - Not a Call (Lambda _).
+ * - Not a Call (Call _).
+ * - Not a Call (_, []).
+ * - Not a Case (Cons _).
+ * - Not a Call (MetaSet, ..).
+ *)
+let rec lexp_whnf e ctx = match e with
+ | Var v -> (match DB.env_lookup_expr ctx v with
+ | None -> e
+ (* FIXME: We shouldn't do this blindly for recursive definitions! *)
+ | Some e' -> lexp_whnf e' ctx)
+ | Susp (e, s) -> lexp_whnf (push_susp e s) ctx
+ (* FIXME: Obviously incomplete! *)
+ | e -> e
+
+
(********* Testing if a lexp is properly typed *********)
View it on GitLab: https://gitlab.com/monnier/typer/commit/d05adcab62ee2637006f96556c49ce30c94…
1
0
Stefan pushed to branch master at Stefan / Typer
Commits:
e5fa8b6d by Stefan Monnier at 2016-08-27T10:35:44-04:00
Fix syntax of explicit-implicit args
* typer-mode.el (typer-smie-grammar): Fix grammar for `:=`.
Add if/then/else to the grammar. Remove `:-` and `:≡`.
* tests/sexp_test.ml: Add test for `:=` and if/then/else.
* tests/eval_test.ml, tests/macro_test.ml: Use explicit implicit args.
* src/grammar.ml (default_grammar): Update from type-mode.el.
* doc/manual.texi (Core Syntax): Only keep `:=` for explicit args.
* src/builtin.ml (get_attribute_impl, declexpr_impl)
(is_builtin_macro): Silence compiler-warning.
* btl/types.typer (length): Pass explicitly implicit parameter.
- - - - -
9 changed files:
- DESIGN
- btl/types.typer
- doc/manual.texi
- src/builtin.ml
- src/grammar.ml
- tests/eval_test.ml
- tests/macro_test.ml
- tests/sexp_test.ml
- typer-mode.el
Changes:
=====================================
DESIGN
=====================================
--- a/DESIGN
+++ b/DESIGN
@@ -99,7 +99,6 @@ or "implicit". This has 2 downsides:
* Syntax
arw ::= '≡>' | '=>' | '->'
-assign::= ':≡' | ':=' | ':-'
colon ::= ':::' | '::' | ':'
exp ::= '(' id ':' exp ')' arw exp | exp arw exp #Function Types
| 'let' decls 'in' exp
@@ -115,8 +114,8 @@ decl ::= id ':' exp
simple_arg ::= id | '('id ':' exp')'
formal_arg ::= id | '(' id colon exp ')'
ind_arg ::= exp | '(' id colon exp ')'
-pat_arg ::= id | '(' id assign pattern ')'
-actual_arg ::= exp | '(' id assign exp ')'
+pat_arg ::= id | '(' id ':=' pattern ')'
+actual_arg ::= exp | '(' id ':=' exp ')'
An identifier which starts with a question mark is one meant to be
generalized as an implicit/erasable argument. E.g.
@@ -1434,7 +1433,13 @@ need to do anyway.
Does it come with a cost? That depends on the universe-level of the
equality type.
-*** E.g. if (=) is in Type 0:
+We can encode equality in CoC:
+
+ eq x y = ∀f. f x -> f y
+ eq_refl : ∀x. eq x x
+ eq_refl x f P = P
+
+*** E.g. if (x = y) is in Type 0:
type (=) (t:Type l) (a:t) : t -> Type 0
refl: a = a
@@ -1461,7 +1466,7 @@ this should not affect typing very much since
so the level of T is not affected.
-*** E.g. if (=) is in Type l:
+*** E.g. if (x = y) is in Type l:
type (=) (t:Type l) (a:t) : t -> Type l
refl: a = a
@@ -1506,6 +1511,21 @@ make sense for "erasable" terms.
Also, by marking "large" elements of inductive definitions as erasable, we'd
get something similar to preventing strong elimination for them.
+E.g. in cast-ultimate.v I had to use axioms like
+
+ EQ_ex : Exists K1 TF1 = Exists K2 TF2 -> (∀F. F K1 TF1 = F K2 TF2)
+
+whose soundness is actually not known.
+With impredicative erasable args we do not need an axiom de define:
+
+ EQ_ex : Exists(K:≡K1) TF1 = Exists(K:≡K2) TF2
+ -> (∀F. F(K:≡K1) TF1 = F(K:≡K2) TF2)
+
+Notice how F only takes an erasable version of K1 and K2, thus
+imposing a constraint on the axiom which might indeed be sufficient to make
+it sound. Hopefully it's also still sufficient for the cast-ultimate.v proof
+to go through!
+
** Universe level of equality
In current Coq, homogenous equality is:
@@ -1553,6 +1573,31 @@ Which I guess is comparable to:
type (~=) (t1:Type l) (a1:t1) (t2:Type l) (Q:t1 = t2) : t2 -> Type l
refl: a1 ~= (coerce Q a1)
+*** "Natural" level via encoding
+
+Let's check the "natural" level of the "eq" encoding:
+
+ eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) ->
+ (l':Level) ≡> (T':Type l') ≡> (f:T -> T') -> f x -> f y
+ eq x y : Typeω
+
+Ouch! But if we consider that the level of inductive definitions is
+normally unaffected by the level at which they're eliminated (contrary to
+what happens for the kind of impredicative encoding used here) we could
+treat it more like
+
+ eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) ->
+ (T':Type 0) ≡> (f:T -> T') -> f x -> f y
+ eq x y : Type l
+
+Which gives us the dreaded "Type (l+1)" if T is "Type l".
+But if x and y are types, we should be able to cut the middle man:
+
+ eq' = λ(l : Level) ≡> λ(x : Type l) (y : Type l) ->
+ (T':Type 0) ≡> (f : Type l -> T') -> f x -> f y
+ eq' x y : Type l
+
+but that doesn't seem to help.
** Inference
@@ -1698,23 +1743,11 @@ sacrificing normalization.
** http://albatross-lang.sourceforge.net
** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf
** Read
+*** (Co)Iteration for higher-order nested datatypes, Andreas Abel and Ralph Matthes, [Abel03]
*** Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna.
http://www.cs.st-andrews.ac.uk/~eb/writings/types2003.pdf
*** A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi, Andrew Gacek and Gopalan Nadathur
*** How OCaml type checker works, http://okmij.org/ftp/ML/generalization.html
-* Skip lists
-
-SkipList a
- | Empty
- | Cons (val : a) (next : SkipList a) (skip : Nat) (dest : SkipList a)
-
-At position 2^n, we want skip=2^(n-1)
-At position 2^n+2^(n-1) we want two contradictory things:
-- skip=2^(n-1) to get to the pivotal 2^n (for when we start before
- 2^n+2^(n-1) and need to go past 2^n).
-- skip=2^(n-2) to do the binary search between 2^n+2^(n-1) and 2^n (for when
- we don't want to go past 2^n, e.g. because we started from before
- 2^(n+1)).
* Related languages
** Idris
** F-star (https://www.fstar-lang.org)
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -138,6 +138,12 @@ FileHandle = Built-in "FileHandle";
% define operation on file handle
run-io = Built-in "run-io" (
+ %% FIXME: runIO should have type IO Unit -> b -> b
+ %% or IO a -> b -> b, which means "run the IO, throw away the result,
+ %% and then return the second argument unchanged". The "dummy" b argument
+ %% is actually crucial to make sure the result of runIO is used, otherwise
+ %% the whole call would look like a dead function call and could be
+ %% optimized away!
(a : Type) ≡>
(b : Type) ≡>
IO a -> (a -> IO b) -> (IO b) -> Unit);
@@ -163,6 +169,7 @@ has-attribute = Built-in "has-attribute" (Macro);
% Context Accessors
% -----------------------------------------------------
+%% FIXME: These should be functions!
decltype = Built-in "decltype" Macro;
declexpr = Built-in "declexpr" Macro;
=====================================
doc/manual.texi
=====================================
--- a/doc/manual.texi
+++ b/doc/manual.texi
@@ -119,7 +119,6 @@ The core syntax of the language is as follows:
@example
arw ::= '≡>' | '=>' | '->'
-assign::= ':≡' | ':=' | ':-'
colon ::= ':::' | '::' | ':'
exp ::= id
| '(' id ':' exp ')' arw exp
@@ -137,12 +136,12 @@ decl ::= id ':' exp
simple_arg ::= id | '(' id ':' exp ')'
formal_arg ::= id | '(' id colon exp ')'
ind_arg ::= exp | '(' id colon exp ')'
-pat_arg ::= id | '(' id assign id ' )'
-actual_arg ::= exp | '(' id assign exp ')'
+pat_arg ::= id | '(' id ':=' id ' )'
+actual_arg ::= exp | '(' id ':=' exp ')'
label ::= id
@end example
-The three different kinds of arrows, assign symbols and colons are
+The three different kinds of arrows and colons are
used respectively for @emph{erasable} arguments, @emph{implicit}
arguments, and @emph{explicit} arguments. @emph{explicit} arguments
are the normal kind of arguments we're all familiar with.
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -347,8 +347,11 @@ let decltype_impl loc largs ctx ftype =
ltype, type0
let builtin_macro = [
+ (* FIXME: These should be functions! *)
("decltype", decltype_impl);
("declexpr", declexpr_impl);
+ (* FIXME: These are not macros but `special-forms`.
+ * We should add here `let_in_`, `case_`, etc... *)
("get-attribute", get_attribute_impl);
("new-attribute", new_attribute_impl);
("has-attribute", has_attribute_impl);
@@ -366,7 +369,7 @@ let get_macro_impl loc name =
with Not_found -> builtin_error loc ("Builtin macro" ^ name ^ " not found")
let is_builtin_macro name =
- try SMap.find name macro_impl_map; true
+ try let _ = SMap.find name macro_impl_map in true
with Not_found -> false
=====================================
src/grammar.ml
=====================================
--- a/src/grammar.ml
+++ b/src/grammar.ml
@@ -66,37 +66,38 @@ let default_stt : token_env =
let default_grammar : grammar =
List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g)
SMap.empty
- [("^", Some 165, Some 152);
- ("/", Some 140, Some 153);
- ("*", Some 141, Some 154);
- ("-", Some 109, Some 128);
- ("+", Some 110, Some 129);
- ("!=", Some 111, Some 89);
- (">=", Some 112, Some 90);
- ("<=", Some 113, Some 91);
- (">", Some 114, Some 92);
- ("<", Some 115, Some 93);
- ("==", Some 116, Some 94);
- ("&&", Some 77, Some 95);
+ [("^", Some 166, Some 153);
+ ("/", Some 141, Some 154);
+ ("*", Some 142, Some 155);
+ ("-", Some 110, Some 129);
+ ("+", Some 111, Some 130);
+ ("!=", Some 112, Some 90);
+ (">=", Some 113, Some 91);
+ ("<=", Some 114, Some 92);
+ (">", Some 115, Some 93);
+ ("<", Some 116, Some 94);
+ ("==", Some 117, Some 95);
+ ("&&", Some 78, Some 96);
("||", Some 53, Some 65);
(",", Some 41, Some 41);
- (":≡", Some 166, Some 0);
- (":-", Some 167, Some 1);
- (":=", Some 168, Some 2);
- ("::", Some 169, Some 17);
- (":::", Some 170, Some 16);
- (";", Some 15, Some 15);
+ ("::", Some 167, Some 17);
+ (":::", Some 168, Some 16);
+ ("then", Some 2, Some 1);
+ (";", Some 14, Some 14);
("type", None, Some 30);
("=", Some 28, Some 29);
- ("in", Some 4, Some 66);
+ (":=", Some 170, Some 15);
+ ("in", Some 3, Some 67);
+ ("else", Some 1, Some 66);
("|", Some 54, Some 54);
- (")", Some 3, None);
- ("->", Some 117, Some 98);
- ("=>", Some 117, Some 97);
- ("≡>", Some 117, Some 96);
- ("let", None, Some 4);
- (":", Some 78, Some 78);
- ("lambda", None, Some 117);
+ (")", Some 0, None);
+ ("->", Some 118, Some 99);
+ ("=>", Some 118, Some 98);
+ ("≡>", Some 118, Some 97);
+ ("let", None, Some 3);
+ (":", Some 79, Some 79);
+ ("lambda", None, Some 118);
("case", None, Some 42);
- ("(", None, Some 3)
+ ("if", None, Some 2);
+ ("(", None, Some 0)
]
=====================================
tests/eval_test.ml
=====================================
--- a/tests/eval_test.ml
+++ b/tests/eval_test.ml
@@ -350,14 +350,14 @@ let _ = (add_test "EVAL" "List" (fun () ->
reset_eval_trace ();
let dcode = "
- my_list = (cons 1 (cons 2 (cons 3 (cons 4 nil))));
+ my_list = (cons(a := Int) 1 (cons(a := Int) 2 (cons(a := Int) 3 (cons(a := Int) 4 (nil(a := Int))))));
" in
let rctx, lctx = eval_decl_str dcode lctx rctx in
- let rcode = "(length Int my_list);
- (head Int my_list);
- (head Int (tail Int my_list));" in
+ let rcode = "(length(a := Int) my_list);
+ (head(a := Int) my_list);
+ (head(a := Int) (tail(a := Int) my_list));" in
(* Eval defined lambda *)
let ret = eval_expr_str rcode lctx rctx in
=====================================
tests/macro_test.ml
=====================================
--- a/tests/macro_test.ml
+++ b/tests/macro_test.ml
@@ -48,8 +48,8 @@ let _ = (add_test "MACROS" "macros base" (fun () ->
(* define 'lambda x -> x * x' using macros *)
let dcode = "
my_fun = lambda (x : List Sexp) ->
- let hd = head Sexp x in
- (node_ (symbol_ \"_*_\") (cons hd (cons hd nil)));
+ let hd = head(a := Sexp) x in
+ (node_ (symbol_ \"_*_\") (cons(a := Sexp) hd (cons(a := Sexp) hd (nil(a := Sexp)))));
sqr = Macro_ my_fun;
" in
@@ -71,10 +71,10 @@ let _ = (add_test "MACROS" "macros decls" (fun () ->
let dcode = "
decls-impl = lambda (x : List Sexp) ->
- cons (node_ (symbol_ \"_=_\")
- (cons (symbol_ \"a\") (cons (integer_ 1) nil)))
- (cons (node_ (symbol_ \"_=_\")
- (cons (symbol_ \"b\") (cons (integer_ 2) nil))) nil);
+ cons(a := Sexp) (node_ (symbol_ \"_=_\")
+ (cons(a := Sexp) (symbol_ \"a\") (cons(a := Sexp) (integer_ 1) (nil(a := Sexp)))))
+ (cons(a := Sexp) (node_ (symbol_ \"_=_\")
+ (cons(a := Sexp) (symbol_ \"b\") (cons(a := Sexp) (integer_ 2) (nil(a := Sexp))))) (nil(a := Sexp)));
my-decls = Macro_ decls-impl;
=====================================
tests/sexp_test.ml
=====================================
--- a/tests/sexp_test.ml
+++ b/tests/sexp_test.ml
@@ -36,6 +36,9 @@ let test_sexp_eqv dcode1 dcode2 =
let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0"
let _ = test_sexp_eqv "(x + y)" "_+_ x y"
+let _ = test_sexp_eqv "(x := y)" "_:=_ x y"
+let _ = test_sexp_eqv "if A then B else C -> D" "if A then B else (C -> D)"
+let _ = test_sexp_eqv "A : B -> C" "A : (B -> C)"
let _ = test_sexp_eqv "f __; y" "(f ( __; ) y)"
let _ = test_sexp_eqv "case e | p1 => e1 | p2 => e2"
"case_ ( _|_ e ( _=>_ p1 e1) ( _=>_ p2 e2))"
=====================================
typer-mode.el
=====================================
--- a/typer-mode.el
+++ b/typer-mode.el
@@ -86,7 +86,7 @@
(smie-merge-prec2s
(smie-bnf->prec2
'((id)
- (exp ("(" exp ")")
+ (exp ("(" exp ")") ("(" explicit-arg ")")
(exp "->" exp) (exp "=>" exp) (exp "≡>" exp)
("let" decls "in" exp)
(exp ":" exp)
@@ -96,7 +96,7 @@
("lambda" simple_arg "≡>" exp)
("case" exp-branches)
;; ("letrec" decl "in" exp)
- ;; ("if" exp "then" exp "else" exp)
+ ("if" exp "then" exp "else" exp)
)
(simple_arg (id) ("(" typed_arg ")"))
(typed_arg (id ":" exp))
@@ -106,7 +106,8 @@
(decls (decls ";" decls) (decl))
(decl (id ":" exp) (exp "=" exp) ("type" inductive_branches))
(inductive_branches (exp) (inductive_branches "|" inductive_branches))
- (explicit-arg (id ":=" exp) (id ":-" exp) (id ":≡" exp))
+ (explicit-arg (id ":=" exp) ;; (id ":-" exp) (id ":≡" exp)
+ )
(exp-branches (exp "|" branches))
(branches (branches "|" branches) (pattern "=>" exp)))
'((assoc ";")
@@ -127,6 +128,11 @@
(assoc ":") ;Should this be left or right?
(right "->" "=>" "≡>")
)
+ ;; There's also ambiguity with "else": should "...A else B => C"
+ ;; mean "(...A else B) => C" or "...A else (B => C)".
+ ;; I think it should be "...A else (B => C)".
+ '((nonassoc "else")
+ (nonassoc ":" "=>" "->" "≡>"))
)
;; Precedence of "=" is tricky as well. Cases to consider:
;; - "x : e1 = e2"
View it on GitLab: https://gitlab.com/monnier/typer/commit/e5fa8b6d9a995df0ea54f8df84c71e2f034…
1
0
[Git][monnier/typer][unification] 3 commits: Tweak use of substitutions and unsusp
by Stefan 27 Aoû '16
by Stefan 27 Aoû '16
27 Aoû '16
Stefan pushed to branch unification at Stefan / Typer
Commits:
c17b5a1f by Stefan Monnier at 2016-08-26T23:47:10-04:00
Tweak use of substitutions and unsusp
* src/lexp.ml (subst): Newtype.
(mkSusp): Also apply eagerly to Metavar.
(push_susp): Rename from unsusp.
(nosusp): Rename from ususp_all.
(_lexp_to_str): Use push_susp.
- - - - -
536bba67 by Stefan Monnier at 2016-08-26T23:51:29-04:00
* src/lexp.ml (push_susp): Don't be so picky.
- - - - -
a964be1b by Stefan Monnier at 2016-08-26T23:54:31-04:00
Merge branch 'trunk' into unification
- - - - -
0 changed files:
Changes:
View it on GitLab: https://gitlab.com/monnier/typer/compare/85c06461b075f72f81da8013daa30d0fb2…
1
0
27 Aoû '16
Stefan pushed to branch master at Stefan / Typer
Commits:
c17b5a1f by Stefan Monnier at 2016-08-26T23:47:10-04:00
Tweak use of substitutions and unsusp
* src/lexp.ml (subst): Newtype.
(mkSusp): Also apply eagerly to Metavar.
(push_susp): Rename from unsusp.
(nosusp): Rename from ususp_all.
(_lexp_to_str): Use push_susp.
- - - - -
536bba67 by Stefan Monnier at 2016-08-26T23:51:29-04:00
* src/lexp.ml (push_susp): Don't be so picky.
- - - - -
5 changed files:
- src/elexp.ml
- src/lexp.ml
- src/lparse.ml
- src/subst.ml
- src/typecheck.ml
Changes:
=====================================
src/elexp.ml
=====================================
--- a/src/elexp.ml
+++ b/src/elexp.ml
@@ -86,7 +86,7 @@ let rec erase_type (lxp: L.lexp): elexp =
Case(l, (erase_type target), (clean_map cases),
(clean_maybe default))
- | L.Susp(l, s) -> erase_type (L.unsusp l s)
+ | L.Susp(l, s) -> erase_type (L.push_susp l s)
(* To be thrown out *)
| L.Arrow _ -> Type
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -53,13 +53,14 @@ type label = symbol
(* Pour la propagation des types bidirectionnelle, tout va dans `infer`,
* sauf Lambda et Case qui vont dans `check`. Je crois. *)
type ltype = lexp
+ and subst = lexp S.subst
and lexp =
| Imm of sexp (* Used for strings, ... *)
| SortLevel of sort_level
| Sort of U.location * sort
| Builtin of vdef * ltype
| Var of vref
- | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *)
+ | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *)
(* This "Let" allows recursion. *)
| Let of U.location * (vdef * lexp * ltype) list * lexp
| Arrow of arg_kind * vdef option * ltype * U.location * lexp
@@ -109,9 +110,12 @@ type varbind =
let rec mkSusp e s =
if S.identity_p s then e else
+ (* We apply the substitution eagerly to some terms.
+ * There's no deep technical rason for that:
+ * it just seemed like a good idea to do it eagerly when it's easy. *)
match e with
| Susp (e, s') -> mkSusp e (scompose s' s)
- | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *)
+ | Var (l,v) -> slookup s l v
| _ -> Susp (e, s)
and scompose s1 s2 = S.compose mkSusp s1 s2
and slookup s l v = S.lookup (fun l i -> Var (l, i))
@@ -271,16 +275,13 @@ let rec lexp_location e =
let vdummy = (U.dummy_location, "dummy")
let maybev mv = match mv with None -> vdummy | Some v -> v
-let rec unsusp e s = (* Push a suspension one level down. *)
+let rec push_susp e s = (* Push a suspension one level down. *)
match e with
| Imm _ -> e
| SortLevel _ -> e
| Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s))
| Sort (l, _) -> e
| Builtin _ -> e
- | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v
- | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!";
- mkSusp e (scompose s' s)
| Let (l, defs, e)
-> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in
let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty)
@@ -321,10 +322,19 @@ let rec unsusp e s = (* Push a suspension one level down. *)
match default with
| None -> default
| Some e -> Some (mkSusp e s))
-
-let unsusp_all e =
+ (* Susp should never appear around Var/Susp/Metavar because mkSusp
+ * pushes the subst into them eagerly. IOW if there's a Susp(Var..)
+ * or Susp(Metavar..) it's because some chunk of code should use mkSusp
+ * rather than Susp. *)
+ | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *)
+ push_susp e (scompose s' s)
+ | (Var _)
+ -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *)
+ push_susp (mkSusp e s) S.identity
+
+let nosusp e = (* Return `e` without `Susp`. *)
match e with
- | Susp(e, s) -> unsusp e s
+ | Susp(e, s) -> push_susp e s
| _ -> e
let lexp_to_string e =
@@ -668,7 +678,7 @@ and _lexp_to_str ctx exp =
| Float (_, s) -> tval (string_of_float s)
| e -> sexp_to_str e)
- | Susp _ -> _lexp_to_str ctx (unsusp_all exp)
+ | Susp (e, s) -> _lexp_to_str ctx (push_susp e s)
| Var ((loc, name), idx) -> name ^ (index idx) ;
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -241,7 +241,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
let inductive_type = Var((loc, type_name), idx) in
(* Get constructor args *)
- let formal, args = match unsusp_all idt with
+ let formal, args = match nosusp idt with
| Inductive(_, _, formal, ctor_def) -> (
try formal, (SMap.find cname ctor_def)
with Not_found ->
@@ -297,7 +297,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp =
(* This case cannot be inferred *)
| Plambda (kind, var, None, body) ->(
(* Read var type from the provided type *)
- let ltp, lbtp = match unsusp_all t with
+ let ltp, lbtp = match nosusp t with
| Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp
| _ -> lexp_error tloc "Type does not match"; dltype, dltype in
@@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
(* consume Arrows and args together *)
let rec get_return_type name i ltp args =
- match (unsusp_all ltp), args with
+ match (nosusp ltp), args with
| _, [] -> ltp
| Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl)
| _, _ -> lexp_warning loc
@@ -416,7 +416,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
(* retrieve function's body *)
let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in
- let ltp = unsusp_all ltp in
+ let ltp = nosusp ltp in
let handle_named_call (loc, name) =
(* Process Arguments *)
@@ -428,7 +428,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
let idx = senv_lookup name ctx in
let vf = (make_var name idx loc) in
- match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with
+ match nosusp (env_lookup_expr ctx ((loc, name), idx)) with
| Builtin((_, "Built-in"), _) ->(
(* ------ SPECIAL ------ *)
match !_parsing_internals, largs with
@@ -476,7 +476,7 @@ 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 lxp = match unsusp_all lxp with
+ let lxp = match nosusp lxp with
| Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
| _ ->
print_string "\n";
@@ -555,7 +555,7 @@ and lexp_read_pattern pattern exp target ctx:
| Ppatvar ((loc, name) as var) ->(
try(
let idx = senv_lookup name ctx in
- match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with
+ match nosusp (env_lookup_expr ctx ((loc, name), idx)) with
(* We are matching a constructor *)
| Cons _ -> (name, loc, []), ctx
@@ -641,7 +641,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) =
" is not a correct index.") in
(* get stored function *)
- let lxp = match unsusp_all lxp with
+ let lxp = match nosusp lxp with
| Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
| _ -> print_string "\n";
print_string (lexp_to_string lxp); print_string "\n";
=====================================
src/subst.ml
=====================================
--- a/src/subst.ml
+++ b/src/subst.ml
@@ -21,6 +21,28 @@ this program. If not, see <http://www.gnu.org/licenses/>. *)
module U = Util
+(* Implementation of the subsitution calculus.
+ *
+ * As a general rule, try not to use the constructors of the `subst'
+ * datatype, but use the following entry points instead.
+ * Constructor functions:
+ * - S.identity
+ * - S.cons
+ * - S.mkShift
+ * - S.shift
+ * - S.compose
+ * - S.substitute
+ * - S.sink
+ * Destructor functions:
+ * - S.identity_p
+ * - S.lookup
+ *
+ * This implementation is generic (i.e. can be with various datatypes
+ * implementing the associated lambda-calculus), which is the reason for
+ * the added complexity of arguments like `mkVar` and `mkShift` to `S.lookup`.
+ * So in general, you'll want to use Lexp.scompose and Lexp.slookup
+ * for those functions.
+ *)
(* Suspensions definitions.
*
@@ -236,6 +258,7 @@ let shift (m:db_offset) = mkShift Identity m
(* The trivial substitution which doesn't do anything. *)
let identity = Identity
+(* Test if a substitution is trivial. The "_p" stands for "predicate". *)
let identity_p s = match s with | Identity -> true | _ -> false
(* Compose two substitutions. This implements the merging rules.
=====================================
src/typecheck.ml
=====================================
--- a/src/typecheck.ml
+++ b/src/typecheck.ml
@@ -110,7 +110,7 @@ let lookup_type ctx vref =
let lookup_value ctx vref =
let (_, i) = vref in
match Myers.nth i ctx with
- | (o, _, LetDef v, _) -> Some (unsusp v (S.shift (i + 1 - o)))
+ | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o)))
| _ -> None
let assert_type e t t' =
@@ -151,7 +151,7 @@ let rec check ctx e =
| Builtin (_, t) -> t
(* FIXME: Check recursive references. *)
| Var v -> lookup_type ctx v
- | Susp (e, s) -> check ctx (unsusp e s)
+ | Susp (e, s) -> check ctx (push_susp e s)
| Let (_, defs, e)
-> let tmp_ctx =
L.fold_left (fun ctx (v, e, t)
View it on GitLab: https://gitlab.com/monnier/typer/compare/e54bbd6d3f50ce539b9669e07cec546057…
1
0
[Git][monnier/typer][unification] 8 commits: fix throw exception for partial application
by BONNEVALLE Vincent 26 Aoû '16
by BONNEVALLE Vincent 26 Aoû '16
26 Aoû '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
4ef9006d by n3f4s at 2016-08-22T17:07:33+02:00
fix throw exception for partial application
- - - - -
d00bf033 by n3f4s at 2016-08-22T20:17:04+02:00
remove useless printing
- - - - -
da4bebac by n3f4s at 2016-08-23T23:15:52+02:00
remove debug printing
- - - - -
343fb9c2 by Stefan Monnier at 2016-08-23T20:26:42-04:00
* tests/sexp_test.ml (test_sexp_add): New function. Use it.
- - - - -
2331f785 by Stefan Monnier at 2016-08-23T20:28:44-04:00
* tests/sexp_test.ml (test_sexp_eqv): New fun. Add some tests
* src/sexp.ml (sexp_equal, sexp_eq_list): New funcs.
* src/prelexer.ml (pretokens_equal, pretokens_eq_list): New funs.
- - - - -
c9bd8ae0 by Stefan Monnier at 2016-08-23T20:30:22-04:00
* src/lexer.ml (nexttoken.lexsym): Fix __<something> handling
- - - - -
e54bbd6d by Stefan Monnier at 2016-08-23T20:34:24-04:00
* src/grammar.ml (char_kind): New type
(token_env): Move here; use it.
(default_stt): Adjust accordingly.
Add entry for '.' tho not currently obeyed.
* src/lexer.ml (token_env): Move to util.ml.
(nexttoken, nexttoken.lexsym): Adjust to new token_env type.
* src/lparse.ml (_lexp_expr_str):
* src/pexp.ml (_pexp_expr_str): Use `token_type'.
* src/debruijn.ml (has_property): Remove unused var.
- - - - -
85c06461 by n3f4s at 2016-08-25T17:30:34+02:00
Merge branch 'master' into unification
- - - - -
9 changed files:
- DESIGN
- src/debruijn.ml
- src/grammar.ml
- src/lexer.ml
- src/lparse.ml
- src/pexp.ml
- src/prelexer.ml
- src/sexp.ml
- tests/sexp_test.ml
Changes:
=====================================
DESIGN
=====================================
--- a/DESIGN
+++ b/DESIGN
@@ -1,5 +1,12 @@
-*- outline -*-
+New:
+- extend the stt table to give precedence for "inner op chars" to use within
+ identifiers (i.e. the "." for module naming).
+- "Confusion is power: blurring the line between Bool and Type".
+ Maybe have "if" use a "Decidable" type class, or maybe automatically
+ turn "e : t : Bool" into "e : t = true : Type"?
+
* Categories of arguments
We want different categories of arguments. I'm thinking here of the
following categories, which are not necessarily mutually-exclusive:
@@ -841,16 +848,6 @@ univalence n = ua ¹ n , ua n , ua- n , ua- n , ua- n
-* Modules and macros
-If we want to be able to call a macro from another module (via
-"Module.macro <args>"), then we have to allow macro calls to have a "name"
-that's not just a symbol but a module-ref (i.e. a potentially complex
-expression), so it's not obvious how to distinguish macro calls from
-function calls, short of normalizing Pcall's function argument.
-
-Solution: macros have a different type, so if M.x has type "macro", we know
-we should normalize it to get the actual macro.
-
* Modules
Modules should be able to hold definitions which are universe-polymorphic,
@@ -1003,32 +1000,10 @@ Tokens will be made of any sequence of letters other than blanks/comments.
special tokens: a(b are 3 tokens if ( is special, but a_(_b is a single
(magic) token.
-** To affect lexing and parsing, declarations have to take effect before the
- whole file is parsed. At first we could say that parsing stops (to allow
- evaluation) at every top-level semi-colon, or after every top-level
- closer. But what about
-
- module Toto = {
- define _::_ a b = ...
- define foo = 1 :: 2
- }
-
- This seems very reasonable, but requires evaluation in the middle of the
- parse of a top-level construct. So we have to handle some top-level
- elements (like "module = ...") specially.
-
- E.g.:
- - make it imperative: "module toto;" is a self-contained top-level
- expression which affects the interpretation of subsequent expressions
- to be considered as within `toto'.
- - if we disallow declarations of new special tokens within such a module,
- then we could re-parse the remaining expressions after finding the
- definition for _::_.
- - make it possible for the evaluation of expressions to read the rest
- of the input (and hence lex&parse it any way it wants).
- - define special "reader macros", so "module".
- - define {...} as special so it gets read and passed to `module'
- without parsing.
+** Structured identifiers
+We want to support identifiers with inner structure, such as "foo.bar.baz".
+
+This could be lexed into a Node identical to that of ( __.__ foo bar baz)
** Provide syntax for backquote&unquote
Since "," is to be used as separator, maybe (,e) and (`e) could be used?
@@ -1379,6 +1354,7 @@ when they're only used in irrelevant args might relieve the tension.
** Papers
*** occurrence checks: [Reed, LFMTP 2009; Abel & Pientka, TLCA 2011]
*** pruning: [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA 2011]
+*** http://www.cs.cmu.edu/~fp/papers/jicslp96.pdf
* Universes
** Universe polymorphism
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -233,8 +233,8 @@ let has_property ctx (var_i, var_n) (att_i, att_n): bool =
try
let pmap = PropertyMap.find (n - var_i, var_n) property_map in
- let prop = PropertyMap.find (n - att_i, att_n) pmap in
- true
+ let _ = PropertyMap.find (n - att_i, att_n) pmap in
+ true
with Not_found -> false
=====================================
src/grammar.ml
=====================================
--- a/src/grammar.ml
+++ b/src/grammar.ml
@@ -38,12 +38,20 @@ open Util
type grammar = (int option * int option) SMap.t
-let default_stt =
- let stt = Array.make 256 false
- in stt.(Char.code ';') <- true;
- stt.(Char.code ',') <- true;
- stt.(Char.code '(') <- true;
- stt.(Char.code ')') <- true;
+(* A token_end array indicates the few chars which are separate tokens,
+ * even if not surrounded by spaces, such as '(', ')', and ';'.
+ * It also indicates which chars are "inner" operators, i.e. those chars
+ * that make up the inner structure of structured identifiers such as
+ * foo.bar.baz. *)
+type char_kind = | CKnormal | CKseparate | CKinner of int
+type token_env = char_kind array
+let default_stt : token_env =
+ let stt = Array.make 256 CKnormal
+ in stt.(Char.code ';') <- CKseparate;
+ stt.(Char.code ',') <- CKseparate;
+ stt.(Char.code '(') <- CKseparate;
+ stt.(Char.code ')') <- CKseparate;
+ stt.(Char.code '.') <- CKinner 5;
stt
(* default_grammar is auto-generated from typer-smie-grammar via:
=====================================
src/lexer.ml
=====================================
--- a/src/lexer.ml
+++ b/src/lexer.ml
@@ -27,17 +27,6 @@ open Grammar
(*************** The Lexer phase *********************)
-(* FIXME: if we want to handle mixfix declarations such as "let _$_ x y =
- toto in a+1 $ b-2" we could make the "_$_" token (i.e. a simple lexical
- criteria) trigger the addition of corresponding syntax rules, but
- it seems hard to extend it so the precedence can also be specified
- because it is awkward to include the info in the lexical part, and as
- soon as we move into the syntactical part we get bitten by the fact that
- we don't know what the syntax means until we perform macroexpansion
- (i.e. much later). *)
-
-type token_env = bool array
-
let digit_p char =
let code = Char.code char
in Char.code '0' <= code && code <= Char.code '9'
@@ -84,7 +73,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos
(hSymbol ({file;line;column=column+bpos},
string_sub name bpos (String.length name)),
pts', 0, 0)
- else if stt.(Char.code name.[bpos])
+ else if stt.(Char.code name.[bpos]) = CKseparate
&& not (name.[bpos+1] == '_') then
(hSymbol ({file;line;column=column+bpos},
string_sub name bpos (bpos + 1)),
@@ -97,14 +86,17 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos
pts', 0, 0)
else
let char = name.[bp] in
- if char == '_' then
+ if char == '_'
+ && bp + 1 < String.length name
+ && name.[bp + 1] != '_' then
(* Skip next char, in case it's a special token. *)
(* For utf-8, this cp+2 is risky but actually works: _ counts
- as 1 and if the input is valid utf-8 the next byte has to
- be a leading byte, so it has to count as 1 as well ;-) *)
+ * as 1 and if the input is valid utf-8 the next byte has to
+ * be a leading byte, so it has to count as 1 as well ;-) *)
lexsym (bp+2) (cp+2)
- else if stt.(Char.code name.[bp]) && (bp + 1 >= String.length name
- || not (name.[bp+1] == '_')) then
+ else if stt.(Char.code name.[bp]) = CKseparate
+ && (bp + 1 >= String.length name
+ || not (name.[bp+1] == '_')) then
(hSymbol ({file;line;column=column+bpos},
string_sub name bpos bp),
pts, bp, cp)
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -448,19 +448,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
* Anonymous : lambda *)
let rec infer_implicit_arg ltp largs nargs depth =
- (* TODO : check arg number ?*)
- (* FIXME error management *)
match nosusp ltp with
(* Error case *)
- | Arrow (Aexplicit, _, _, _, _) when (List.length largs <= 0) ->
- Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) Not enough arguments : \n\tltp = "
- ^ Fmt_lexp.string_of_lxp ltp
- ^ " ,\n\tlargs = ["
- ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs)
- ^ "],\n\tfun_name = "
- ^ Fmt_lexp.string_of_pexp fun_name);
- Debug_fun.do_debug (fun () -> prerr_newline (); ());
- assert false
+ | Arrow (Aexplicit, _, _, _, _) when (List.length largs <= 0) -> []
(* Explicit parameter *)
| Arrow (Aexplicit, _, ltp_arg, _, ltp_ret) ->
@@ -472,32 +462,20 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
(if List.length largs >0
then let head, tail = List.hd largs, List.tl largs
in (Aexplicit, head)::(infer_implicit_arg ltp_ret tail (nargs - 1) (depth - 1))
- else assert false)
+ else [])
(* Implicit paramter not given*)
| Arrow (kind, _, ltp_arg, _, ltp_ret) -> (kind, mkMetavar ())::(infer_implicit_arg ltp_ret largs nargs (depth - 1))
(* "End" of the arrow "list"*)
- | _ -> Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) ltp = "
- ^ Fmt_lexp.string_of_lxp ltp
- ^ " ,\n\tlargs = ["
- ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs)
- ^ "],\n\tfun_name = "
- ^ Fmt_lexp.string_of_pexp fun_name
- ^ "\n");
- (* Cause the throw in builtin*)
- (* [] *)
- List.map (fun g -> Aexplicit, g) largs
- (* cause the too many args *)
+ | _ -> List.map (fun g -> Aexplicit, g) largs
in
(* retrieve function's body *)
let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in
let ltp = nosusp ltp in
let handle_named_call (loc, name) =
- Debug_fun.debug_print_no_buff ("<LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ")\n");
(* Process Arguments *)
- Debug_fun.do_debug (fun () -> prerr_newline (); ());
let pargs = List.map pexp_parse sargs in
let largs = _lexp_parse_all pargs ctx i in
let rec depth_of = function
@@ -534,14 +512,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
let subst, _ = !global_substitution in
let ret_type = get_return_type name 0 ltp new_args subst ctx in
let call = Call(vf, new_args)
- in
- Debug_fun.debug_print_no_buff "<LPARSE.lexp_call>(new_args) "; (* debug printing remove ASAP*)
- Debug_fun.do_debug (fun () ->
- List.iter (fun (_, l) -> Debug_fun.debug_print_lexp l; prerr_string ", "; ()) new_args; ()
- );
- Debug_fun.debug_print_lexp call;
- Debug_fun.debug_print_no_buff "\n";
- call, ret_type
+ in call, ret_type
with Not_found ->
Debug_fun.debug_print_no_buff ("==== <LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ") ====\n");
@@ -1128,7 +1099,7 @@ let default_rctx =
* --------------------------------------------------------- *)
(* Lexp helper *)
-let _lexp_expr_str (str: string) (tenv: bool array)
+let _lexp_expr_str (str: string) (tenv: token_env)
(grm: grammar) (limit: string option) (ctx: lexp_context) =
let pxps = _pexp_expr_str str tenv grm limit in
lexp_parse_all pxps ctx
=====================================
src/pexp.ml
=====================================
--- a/src/pexp.ml
+++ b/src/pexp.ml
@@ -389,7 +389,7 @@ let pexp_decls_all (nodes: sexp list): pdecl list =
* --------------------------------------------------------- *)
(* Lexp helper *)
-let _pexp_expr_str (str: string) (tenv: bool array)
+let _pexp_expr_str (str: string) (tenv: token_env)
(grm: grammar) (limit: string option) =
let sxps = _sexp_parse_str str tenv grm limit in
pexp_parse_all sxps
@@ -419,5 +419,3 @@ let pexp_to_string e =
| Pinductive ((_,_), _, _) -> "Pinductive"
| Pcons ((_,_),_) -> "Pcons"
| Pcase (_, _, _) -> "Pcase"
-
-
=====================================
src/prelexer.ml
=====================================
--- a/src/prelexer.ml
+++ b/src/prelexer.ml
@@ -172,3 +172,15 @@ let pretokens_to_str pretokens =
let pretokens_print p = print_string (pretokens_to_str p)
+(* Prelexer comparison, ignoring source-line-number info, used for tests. *)
+let rec pretokens_equal p1 p2 = match p1, p2 with
+ | Pretoken (_, s1), Pretoken (_, s2) -> s1 = s2
+ | Prestring (_, s1), Prestring (_, s2) -> s1 = s2
+ | Preblock (_, ps1, _), Preblock (_, ps2, _) ->
+ pretokens_eq_list ps1 ps2
+ | _ -> false
+and pretokens_eq_list ps1 ps2 = match ps1, ps2 with
+ | [], [] -> true
+ | (p1 :: ps1), (p2 :: ps2) ->
+ pretokens_equal p1 p2 && pretokens_eq_list ps1 ps2
+ | _ -> false
=====================================
src/sexp.ml
=====================================
--- a/src/sexp.ml
+++ b/src/sexp.ml
@@ -231,3 +231,21 @@ let sexp_parse_all_to_list grm tokens limit =
| _ -> let (sxp, rest) = sexp_parse_all grm tokens limit in
sexp_parse_impl grm rest limit (sxp :: acc) in
sexp_parse_impl grm tokens limit []
+
+(* Sexp comparison, ignoring source-line-number info, used for tests. *)
+let rec sexp_equal s1 s2 = match s1, s2 with
+ | Epsilon, Epsilon -> true
+ | Block (_, ps1, _), Block (_, ps2, _) -> pretokens_eq_list ps1 ps2
+ | Symbol (_, s1), Symbol (_, s2) -> s1 = s2
+ | String (_, s1), String (_, s2) -> s1 = s2
+ | Integer (_, n1), Integer (_, n2) -> n1 = n2
+ | Float (_, n1), Float (_, n2) -> n1 = n2
+ | Node (s1, ss1), Node (s2, ss2) ->
+ sexp_equal s1 s2 && sexp_eq_list ss1 ss2
+ | _ -> false
+
+and sexp_eq_list ss1 ss2 = match ss1, ss2 with
+ | [], [] -> true
+ | (s1 :: ss1), (s2 :: ss2) ->
+ sexp_equal s1 s2 && sexp_eq_list ss1 ss2
+ | _ -> false
=====================================
tests/sexp_test.ml
=====================================
--- a/tests/sexp_test.ml
+++ b/tests/sexp_test.ml
@@ -2,38 +2,43 @@ open Sexp
open Lexer
open Utest_lib
-let _ = (add_test "SEXP" "lambda x -> x + x" (fun () ->
+let test_sexp_add dcode testfun =
+ add_test "SEXP" dcode (fun () -> testfun (sexp_parse_str dcode))
- let dcode = "lambda x -> x + x;" in
-
- let ret = sexp_parse_str dcode in
+let _ = test_sexp_add "lambda x -> x + x" (fun ret ->
match ret with
- | [Node(lbd, [x; add])] -> (match lbd, x, add with
- | (Symbol(_, "lambda_->_"), Symbol(_, "x"),
- Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])) -> success ()
- | _ -> failure ())
- | _ -> failure ()
-))
-
-let _ = (add_test "SEXP" "x * x * x" (fun () ->
-
- let dcode = "x * x * x;" in
-
- let ret = sexp_parse_str dcode in
- match ret with
- | [n] ->(match n with
- | Node(Symbol(_, "_*_"),
- [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); Symbol(_, "x")])
- -> success ()
-
- | Node(Symbol(_, "_*_"),
- [Symbol(_, "x"); Node(Symbol(_, "_*_"), [Symbol(_, "x")]); Symbol(_, "x")])
- -> success ()
-
- | _ -> failure ())
- | _ -> failure ()
-
-))
+ | [Node(Symbol(_, "lambda_->_"),
+ [Symbol(_, "x");
+ Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])])]
+ -> success ()
+ | _ -> failure ()
+)
+
+let _ = test_sexp_add "x * x * x" (fun ret ->
+ match ret with
+ | [Node(Symbol(_, "_*_"),
+ [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]);
+ Symbol(_, "x")])]
+ -> success ()
+ | _ -> failure ()
+)
+
+let test_sexp_eqv dcode1 dcode2 =
+ add_test "SEXP" dcode1
+ (fun () ->
+ let s1 = sexp_parse_str dcode1 in
+ let s2 = sexp_parse_str dcode2 in
+ if sexp_eq_list s1 s2
+ then success ()
+ else (sexp_print (List.hd s1);
+ sexp_print (List.hd s2);
+ failure ()))
+
+let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0"
+let _ = test_sexp_eqv "(x + y)" "_+_ x y"
+let _ = test_sexp_eqv "f __; y" "(f ( __; ) y)"
+let _ = test_sexp_eqv "case e | p1 => e1 | p2 => e2"
+ "case_ ( _|_ e ( _=>_ p1 e1) ( _=>_ p2 e2))"
(* run all tests *)
let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/compare/80547416749c74d44c42a4b8aadfb51c90…
1
0
[Git][monnier/typer][unification] Deleted 48 commits: add global (susbtitution * constraint) variable
by BONNEVALLE Vincent 25 Aoû '16
by BONNEVALLE Vincent 25 Aoû '16
25 Aoû '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
WARNING: The push did not contain any new commits, but force pushed to delete the commits and changes below.
Deleted commits:
d0a20473 by n3f4s at 2016-08-01T21:25:00+02:00
add global (susbtitution * constraint) variable
- - - - -
68895a5c by n3f4s at 2016-08-01T21:44:36+02:00
add unification for default case of infer
- - - - -
8a15dbf9 by n3f4s at 2016-08-01T21:46:49+02:00
add unification for lambda in check
- - - - -
d0a41841 by n3f4s at 2016-08-01T21:47:27+02:00
add unification for default case in check
- - - - -
910c29ef by n3f4s at 2016-08-05T23:51:10+02:00
change debug print from stdout to stderr
- - - - -
501fd9c5 by n3f4s at 2016-08-05T23:51:36+02:00
remove lambda case from infer
- - - - -
17e17516 by n3f4s at 2016-08-05T23:53:26+02:00
add None case for Plambda in check & refactoring
- - - - -
7051ef29 by n3f4s at 2016-08-05T23:54:21+02:00
add debug and idea of implicit argument in call
- - - - -
0e53c1ea by n3f4s at 2016-08-05T23:55:00+02:00
add test for inference
- - - - -
872b0143 by n3f4s at 2016-08-08T17:47:11+02:00
better debuging
- - - - -
76ecccda by n3f4s at 2016-08-08T18:12:05+02:00
better debug printing and add mkMetavar helper
- - - - -
0cb401ef by n3f4s at 2016-08-08T18:13:04+02:00
refactoring of Plambda case in check
- - - - -
34c98ba5 by n3f4s at 2016-08-10T17:46:09+02:00
better output
- - - - -
d997582c by n3f4s at 2016-08-10T18:05:21+02:00
debug check for Plambda
- - - - -
98220426 by n3f4s at 2016-08-10T18:07:23+02:00
add a case for metavar in default case in check
avoid stack overflow caused by infinite recursion between
infer and check
- - - - -
f57a7c31 by n3f4s at 2016-08-10T18:09:00+02:00
add function that create metavar for implicit arg
- - - - -
284f6487 by n3f4s at 2016-08-10T18:09:45+02:00
use infer_implicit_arg to manage non Aexplicit
extract the part that check for non Aexplicit arg and create metavar for
implicit arg to a function
- - - - -
484b86c8 by n3f4s at 2016-08-10T18:13:41+02:00
add test for non Aexplicit arg in function
- - - - -
98488b1a by n3f4s at 2016-08-10T18:14:00+02:00
remove type anotation in test
- - - - -
06c50bba by n3f4s at 2016-08-10T21:06:03+02:00
add mkMetavar wrapper
- - - - -
7d49d849 by n3f4s at 2016-08-10T21:13:30+02:00
replace metavar construction by call to wrapper
- - - - -
93ab8238 by n3f4s at 2016-08-10T21:15:00+02:00
replace metavar construction by call to wrapper
- - - - -
912c40d4 by n3f4s at 2016-08-10T21:24:32+02:00
extract unification with "new" arrow in a function
- - - - -
8b9efc77 by n3f4s at 2016-08-10T21:32:08+02:00
extract Lambda creation into a function
- - - - -
e4b8d6d2 by n3f4s at 2016-08-10T21:34:29+02:00
better output for error in default case in check
- - - - -
257114e0 by n3f4s at 2016-08-10T21:59:07+02:00
default case of check return inferred_t
cause eval test to fail with an error : too many argument
- - - - -
d16f8174 by n3f4s at 2016-08-10T22:03:55+02:00
move lambda case from infer to check
makes infinite recursion pass (infinte recursion failed in previous
commit) but cause errors in unfication test : change result of
lexp_decls_str
- - - - -
a7e14366 by n3f4s at 2016-08-10T22:22:57+02:00
reduce lambda case in check
(do not resolve bugs)
- - - - -
8e08924e by n3f4s at 2016-08-10T23:32:06+02:00
better ouput
- - - - -
c379c3cc by n3f4s at 2016-08-10T23:33:48+02:00
add test for lparse
- - - - -
22ffd69b by n3f4s at 2016-08-10T23:34:35+02:00
add implicit arg management
- - - - -
8554fb2a by n3f4s at 2016-08-10T23:35:07+02:00
add debug output when var/fun not found
- - - - -
1cb81d1c by n3f4s at 2016-08-10T23:52:21+02:00
debug infinite (mutual) recursion for check &infer
- - - - -
eb7ee412 by n3f4s at 2016-08-11T21:19:35+02:00
add pexp formatting
- - - - -
3b603a9a by n3f4s at 2016-08-11T21:24:13+02:00
raise an error for non handled case in infer
- - - - -
a9d89581 by n3f4s at 2016-08-11T21:26:48+02:00
remove metavar case in default case in check
- - - - -
a9273fa2 by n3f4s at 2016-08-11T21:45:21+02:00
Merge branch 'tests' into unification
- - - - -
6fa48187 by n3f4s at 2016-08-12T23:12:22+02:00
add name in metavar creation
- - - - -
eabcc167 by n3f4s at 2016-08-17T00:03:00+02:00
modify the test to make them pass
- stop lparse test from always failing
- change the L-exp in unify_test according to decl_str output
- - - - -
b520dda8 by n3f4s at 2016-08-17T00:05:28+02:00
change the output of infer_implicit_arg
fix throw in conversion from typer list to ocaml list but cause error
regarding number of argument
- - - - -
77fef2c1 by n3f4s at 2016-08-17T00:07:32+02:00
add basic printing for metavar in _lexp_to_str
- - - - -
49d6e22d by n3f4s at 2016-08-17T00:20:18+02:00
add call to lambda with implicit arg, lparse test
- - - - -
5b0b03fe by n3f4s at 2016-08-17T21:45:55+02:00
remove unused code
- - - - -
f2751880 by n3f4s at 2016-08-17T21:46:48+02:00
remove commented code
- - - - -
3172b157 by n3f4s at 2016-08-17T22:32:42+02:00
add Pmetavar case in lexp_p_infer
- - - - -
d4c27327 by n3f4s at 2016-08-18T18:53:22+02:00
improve implicit/explicit argument handling
- - - - -
133f6fc1 by n3f4s at 2016-08-18T18:54:09+02:00
try to resolve not enough arg with metavar
- - - - -
80547416 by n3f4s at 2016-08-19T06:11:22+02:00
add arg_kind in lexp printing
- - - - -
8 changed files:
- src/builtin.ml
- src/debug_fun.ml
- src/fmt_lexp.ml
- src/lexp.ml
- src/lparse.ml
- tests/lparse_test.ml
- tests/unify_test.ml
- tests/utest_lib.ml
Changes:
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -171,7 +171,7 @@ let rec tlist2olist acc expr =
| Vcons((_, "nil"), []) -> List.rev acc
| _ ->
print_string (value_name expr); print_string "\n";
- value_print expr;
+ value_print expr; print_newline ();
builtin_error dloc "List conversion failure'"
=====================================
src/debug_fun.ml
=====================================
--- a/src/debug_fun.ml
+++ b/src/debug_fun.ml
@@ -1,8 +1,8 @@
open Fmt_lexp
-(* let _debug = true *)
-let _debug = false
+let _debug = true
+(* let _debug = false *)
let logs = ref []
@@ -17,18 +17,21 @@ let clear_indent () =
in
do_debug (fun () ->
List.iter (fun (s1, s2) ->
- print_string s1;
- print_string (String.make (!indent * 2) '-');
- print_string s2;
+ prerr_string s1;
+ prerr_string (String.make (!indent * 2) '-');
+ prerr_string s2;
indent := !indent + 1;
) (!logs);
logs := [];
- print_newline ();
+ prerr_newline ();
())
+let debug_print_no_buff str =
+ do_debug (fun () -> prerr_string str; ())
+
let debug_print_lexp lxp =
let str = colored_string_of_lxp lxp str_yellow str_magenta
- in do_debug (fun () -> print_string str; ())
+ in do_debug (fun () -> prerr_string str; ())
let debug_print_unify fn lhs rhs str =
let debug_print_unify fn lhs rhs str =
=====================================
src/fmt_lexp.ml
=====================================
--- a/src/fmt_lexp.ml
+++ b/src/fmt_lexp.ml
@@ -1,5 +1,6 @@
open Sexp
+open Pexp
open Lexp
open Fmt
@@ -43,7 +44,7 @@ and string_of_lxp lxp =
| Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")"
| Let (_) -> "Let(..)"
| Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")"
- | Arrow (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (string_of_lxp b) ^ ")"
+ | Arrow (kind, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ ":" ^ string_of_kind kind ^ " => " ^ (string_of_lxp b) ^ ")"
| Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ ": " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ "))"
| Metavar (value, _, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")"
| Call (_) -> "Call(...)"
@@ -54,6 +55,11 @@ and string_of_lxp lxp =
| Susp (v, s) -> "Susp(" ^ (string_of_lxp v) ^ ", " ^ (string_of_subst s) ^ ")"
| _ -> "Unidentified Lexp"
+and string_of_kind = function
+ | Aexplicit -> "Aexplicit"
+ | Aimplicit -> "Aimplicit"
+ | Aerasable -> "Aerasable"
+
and string_of_sort_level lvl =
match lvl with
| SLn i -> "SLn(" ^ string_of_int i ^ ")"
@@ -65,7 +71,7 @@ and string_of_sort sort =
| StypeOmega -> "StypeOmega"
| StypeLevel -> "StypeLevel"
-let colored_string_of_lxp lxp lcol vcol =
+let rec colored_string_of_lxp lxp lcol vcol =
match lxp with
| Imm (Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")"
| Imm (String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")"
@@ -81,9 +87,9 @@ let colored_string_of_lxp lxp lcol vcol =
| Call (_) -> (lcol "Call(...)" )
| Case _ -> (lcol "Case") ^ "(...)"
| Inductive _ -> (lcol "Inductive") ^ "(...)"
- | Sort _ -> (lcol "Sort") ^ "(...)"
- | SortLevel _ -> (lcol "SortLevel") ^ "(...)"
- | Susp _ -> (lcol "Susp") ^ "(...)"
+ | Sort (_, s) -> (lcol "Sort") ^ "(" ^ vcol (string_of_sort s)^ ")"
+ | SortLevel l -> (lcol "SortLevel") ^ "(" ^ vcol (string_of_sort_level l) ^ ")"
+ | Susp (v, s) -> (lcol "Susp") ^ "(" ^ colored_string_of_lxp v lcol vcol ^ ", " ^ vcol (string_of_subst s) ^")"
| _ -> (lcol "Unidentified Lexp")
let padding_right (str: string ) (dim: int ) (char_: char) : string =
@@ -102,3 +108,20 @@ let center (str: string ) (dim: int ) (char_: char) : string =
in (String.make lpad char_) ^ str ^ (String.make lpad char_)
+let rec string_of_pexp pxp =
+ match pxp with
+ (* | Psort of location * sort *)
+ | Pimm (Integer (_, i)) -> "Pimm( Integer (" ^ string_of_int i ^ "))"
+ | Pimm (Float (_, f)) -> "Pimm( Float (" ^ string_of_float f ^ "))"
+ | Pimm (String (_, s)) -> "Pimm (String (" ^ s ^ "))"
+ | Pvar (_, s) -> "Pvar (" ^ s ^ ")"
+ | Phastype (_, p1, p2) -> "Phastype (" ^ string_of_pexp p1 ^ ", " ^ string_of_pexp p2 ^ ")"
+ | Pmetavar (_, s) -> "Pmetavar (" ^ s ^ ")"
+ | Plet (_, _, p) -> "Plet (_, " ^ string_of_pexp p ^ ")"
+ | Parrow (_, _, _, _, _) -> "Parrow (...)"
+ | Plambda _ -> "Plambda (...)"
+ | Pcall _ -> "Pcall (...)"
+ | Pinductive _ -> "Pinductive (...)"
+ | Pcons ( (_, s), (_, s2) ) -> "Pcons (" ^ s ^ ", " ^ s2 ^ ")"
+ | Pcase _ -> "Pcase (...)"
+ | _ -> "Pexp not handled"
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -684,6 +684,8 @@ and _lexp_to_str ctx exp =
| Var ((loc, name), idx) -> name ^ (index idx) ;
+ | Metavar (idx, subst, (loc, name)) -> "?" ^ name ^ (index idx) (*TODO : print subst*)
+
| Let (_, decls, body) ->
(* Print first decls without indent *)
let h1, decls, idt_lvl =
@@ -797,7 +799,7 @@ and _lexp_to_str ctx exp =
| SortLevel (SLn v) -> "Type" ^ (string_of_int v)
| _ -> "Type")
- | _ -> print_string "Printing Not Implemented"; "-- --"
+ | _ -> print_string "Printing Not Implemented\n"; "-- --"
and lexp_str_ctor ctx ctors =
SMap.fold (fun key value str ->
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -130,6 +130,13 @@ let build_var name ctx =
let get_type0 ctx = build_var "Type" ctx
let get_int ctx = build_var "Int" ctx
+(* :-( *)
+let global_substitution = ref (Unif.empty_subst, [])
+
+let mkMetavar () = let meta = Unif.create_metavar ()
+ in let name = "__Metavar_" ^ (string_of_int meta)
+ in Metavar (meta, S.Identity, (Util.dummy_location, name))
+
(* shift all variables by an offset *)
let senv_lookup name ctx =
senv_lookup name ctx + !_shift_glob
@@ -210,22 +217,6 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
let v = Inductive(tloc, label, formal, map_ctor) in
v, ltp
- (* This case can be inferred *)
- | Plambda (kind, var, optype, body) ->
- let ltp, _ = match optype with
- | Some ptype -> lexp_infer ptype ctx
- (* This case must have been lexp_p_check *)
- | None -> lexp_error tloc "Lambda require type annotation";
- dltype, dltype in
-
- let nctx = env_extend ctx var Variable ltp in
- let lbody, lbtp = lexp_infer body nctx in
- (* We added one variable in the ctx * )
- let lbtp = _type_shift lbtp 1 in *)
-
- let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in
- Lambda(kind, var, ltp, lbody), lambda_type
-
| Pcall (fname, _args) ->
lexp_call fname _args ctx i
@@ -250,8 +241,8 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
lexp_error loc
("Constructor \"" ^ cname ^ "\" does not exist");
[], [])
-
- | _ -> lexp_error loc "Not an Inductive Type"; [], [] in
+ | _ -> lexp_error loc "Not an Inductive Type"; [], []
+ in
(* build Arrow type *)
let cons_type = List.fold_left (fun ltp (kind, v, tp) ->
@@ -272,14 +263,17 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
| Pcase (loc, target, patterns) ->
lexp_case None (loc, target, patterns) ctx i
+ | Pmetavar _ -> (let meta = mkMetavar () (*TODO *)
+ in lexp_warning dloc "<LEXP_P_INFER>(Pmetavar case) Check output : may be wrong lexp/type returned";
+ (meta, meta) (* FIXME pretty sure that's not should be returned*))
+
| Phastype (_, pxp, ptp) ->
let ltp, _ = lexp_infer ptp ctx in
(_lexp_p_check pxp ltp ctx (i + 1)), ltp
- (*FIXME right thing to do*)
- | _ -> let meta = Unif.mkMetavar S.Identity (Util.dummy_location, "") (*???*)
- in (meta, lexp_p_check p meta ctx)
-
+ | Plambda _ -> (let meta = mkMetavar ()
+ in let lxp = lexp_p_check p meta ctx
+ in (lxp, meta))
and lexp_let_decls decls (body: lexp) ctx i =
(* build the weird looking let *)
@@ -290,48 +284,71 @@ and lexp_let_decls decls (body: lexp) ctx i =
and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp =
_lexp_p_check p t ctx 1
-(*TODO : - add substitution parameter for unification
- - try to unify in default case *)
and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp =
- let tloc = pexp_location p in
+ let tloc = pexp_location p
+ in
_global_lexp_ctx := ctx;
_global_lexp_trace := (i, tloc, p)::!_global_lexp_trace;
+ let unify_with_arrow lxp kind subst =
+ let arg, body = mkMetavar (), mkMetavar ()
+ in let arrow = Arrow (kind, None, arg, Util.dummy_location, body)
+ in match Unif.unify arrow lxp subst with
+ | Some(subst) -> global_substitution := subst; arg, body
+ | None -> lexp_error tloc ("Type " ^ Fmt_lexp.string_of_lxp lxp
+ ^ " and "
+ ^ Fmt_lexp.string_of_lxp arrow
+ ^ " does not match"); dltype, dltype
+
+ in
+ let infer_lambda_body kind var body subst =
+ (* Read var type from the provided type *)
+ let ltp, lbtp = match nosusp t with
+ | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp
+ | lxp -> (unify_with_arrow lxp kind subst)
+ in
+ let nctx = env_extend ctx var Variable ltp in
+ let lbody = _lexp_p_check body lbtp nctx (i + 1) in Lambda(kind, var, ltp, lbody)
+
+ in
+ let subst, _ = !global_substitution
+ in
+ let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1)
+ in
match p with
(* This case cannot be inferred *)
- | Plambda (kind, var, None, body) ->(
- (* Read var type from the provided type *)
- let ltp, lbtp = match nosusp t with
- | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp
- | _ -> lexp_error tloc "Type does not match"; dltype, dltype in
+ | Plambda (kind, var, None, body) ->(infer_lambda_body kind var body subst)
- let nctx = env_extend ctx var Variable ltp in
- let lbody = _lexp_p_check body lbtp nctx (i + 1) in
+ (* This case can be inferred *)
+ | Plambda (kind, var, Some (ptype), body) ->
+ let ltp, _ = lexp_infer ptype ctx
+ in let nctx = env_extend ctx var Variable ltp
+ in let lbody, lbtp = lexp_infer body nctx
+ 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
+ | _ -> (let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in
(* e *)
match e with
(* Built-in is a dummy function with no type. We cannot check
* Built-in *)
| Builtin _ -> e
| _ ->
- (* (if TC.conv_p inferred_t t then () else debug_msg ( *)
- (match Unif.unify inferred_t t Unif.empty_subst with
- | Some _ -> ()
+ (match Unif.unify inferred_t t Unif.empty_subst with (* cause eval test to fail : too many arguments *)
+ | Some subst -> global_substitution := subst; inferred_t
| None -> 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";
- lexp_warning tloc "Type Mismatch inferred != Annotation"));
- e
+ let print_lxp str =
+ print_string (Fmt_lexp.colored_string_of_lxp str Fmt_lexp.str_yellow Fmt_lexp.str_magenta) in
+ print_string "1 exp "; (print_lxp e); print_string "\n";
+ print_string "2 inf "; (print_lxp inferred_t); print_string "\n";
+ print_string "3 Ann susp("; (print_lxp (nosusp t)); print_string ")\n";
+ lexp_warning tloc "Type Mismatch inferred != Annotation"); e ))
(* Lexp.case cam be checked and inferred *)
and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =
@@ -409,28 +426,87 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
raise e) in
(* consume Arrows and args together *)
- let rec get_return_type name i ltp args =
+ let rec get_return_type name i ltp args subst ctx =
match (nosusp ltp), args with
| _, [] -> ltp
- | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl)
+ | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl subst ctx)
+ (* Do a lookup to check where the var "point" to*)
+ (* | Var(vt), hd::args -> (let ltp = Debruijn.env_lookup_expr ctx vt in get_return_type name (i) ltp args subst ctx) *)
+ | Metavar _, (kind, arg)::tl -> let arr = Arrow (kind, None, mkMetavar (), Util.dummy_location, ltp)
+ (* in ltp *)
+ in (match Unif.unify ltp arr subst with
+ | None -> ltp (*?????*)
+ | Some (subst, c) -> global_substitution := (subst, c); get_return_type name (i + 1) arr tl subst ctx)
| _, _ -> lexp_warning loc
(name ^ " was provided with too many args. Expected: " ^
- (string_of_int i)); ltp in
+ (string_of_int i) ^ " got : " ^ (string_of_int (List.length args))
+ ^ " for lexp : " ^ Fmt_lexp.string_of_lxp (nosusp ltp)); ltp in
(* Vanilla : sqr is inferred and (lambda x -> x * x) is returned
* Macro : sqr is returned
* Constructor : a constructor is returned
* Anonymous : lambda *)
+ let rec infer_implicit_arg ltp largs nargs depth =
+ (* TODO : check arg number ?*)
+ (* FIXME error management *)
+ match nosusp ltp with
+ (* Error case *)
+ | Arrow (Aexplicit, _, _, _, _) when (List.length largs <= 0) ->
+ Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) Not enough arguments : \n\tltp = "
+ ^ Fmt_lexp.string_of_lxp ltp
+ ^ " ,\n\tlargs = ["
+ ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs)
+ ^ "],\n\tfun_name = "
+ ^ Fmt_lexp.string_of_pexp fun_name);
+ Debug_fun.do_debug (fun () -> prerr_newline (); ());
+ assert false
+
+ (* Explicit parameter *)
+ | Arrow (Aexplicit, _, ltp_arg, _, ltp_ret) ->
+ (let head, tail = List.hd largs, List.tl largs
+ in (Aexplicit, head)::(infer_implicit_arg ltp_ret tail (nargs - 1) (depth - 1)))
+
+ (* Implicit parameter explictly given*)
+ | Arrow (kind, _, ltp_arg, _, ltp_ret) when nargs = depth ->
+ (if List.length largs >0
+ then let head, tail = List.hd largs, List.tl largs
+ in (Aexplicit, head)::(infer_implicit_arg ltp_ret tail (nargs - 1) (depth - 1))
+ else assert false)
+
+ (* Implicit paramter not given*)
+ | Arrow (kind, _, ltp_arg, _, ltp_ret) -> (kind, mkMetavar ())::(infer_implicit_arg ltp_ret largs nargs (depth - 1))
+
+ (* "End" of the arrow "list"*)
+ | _ -> Debug_fun.debug_print_no_buff ( "<LPARSE.LEXP_CALL>(infer_implicit_arg) ltp = "
+ ^ Fmt_lexp.string_of_lxp ltp
+ ^ " ,\n\tlargs = ["
+ ^ (List.fold_left (fun a e -> a ^ ", " ^ (Fmt_lexp.string_of_lxp e)) "" largs)
+ ^ "],\n\tfun_name = "
+ ^ Fmt_lexp.string_of_pexp fun_name
+ ^ "\n");
+ (* Cause the throw in builtin*)
+ (* [] *)
+ List.map (fun g -> Aexplicit, g) largs
+ (* cause the too many args *)
+ in
(* retrieve function's body *)
let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in
let ltp = nosusp ltp in
let handle_named_call (loc, name) =
+ Debug_fun.debug_print_no_buff ("<LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ")\n");
(* Process Arguments *)
+ Debug_fun.do_debug (fun () -> prerr_newline (); ());
let pargs = List.map pexp_parse sargs in
let largs = _lexp_parse_all pargs ctx i in
- let new_args = List.map (fun g -> (Aexplicit, g)) largs in
+ let rec depth_of = function
+ Arrow (_, _, _, _, ltp) -> 1 + (depth_of ltp)
+ | _ -> 0
+ in
+ let new_args = infer_implicit_arg ltp largs ((List.length largs) - 1) (depth_of ltp)
+ (* let new_args = List.map (fun g -> (Aexplicit, g)) largs *)
+ in
try (* Check if the function was defined *)
let idx = senv_lookup name ctx in
@@ -455,10 +531,31 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
dlxp, dltype)
| e ->
- let ret_type = get_return_type name 0 ltp new_args in
- Call(vf, new_args), ret_type
+ let subst, _ = !global_substitution in
+ let ret_type = get_return_type name 0 ltp new_args subst ctx in
+ let call = Call(vf, new_args)
+ in
+ Debug_fun.debug_print_no_buff "<LPARSE.lexp_call>(new_args) "; (* debug printing remove ASAP*)
+ Debug_fun.do_debug (fun () ->
+ List.iter (fun (_, l) -> Debug_fun.debug_print_lexp l; prerr_string ", "; ()) new_args; ()
+ );
+ Debug_fun.debug_print_lexp call;
+ Debug_fun.debug_print_no_buff "\n";
+ call, ret_type
with Not_found ->
+ Debug_fun.debug_print_no_buff ("==== <LPARSE.LEXP_CALL>handle_named_call (?loc?, " ^ name ^ ") ====\n");
+ Debug_fun.do_debug (fun () -> (* Some debug printing, remove ASAP*)
+ prerr_string "==== <LPARSE.lexp_call>(largs) ";
+ List.iter (fun l -> Debug_fun.debug_print_lexp l; prerr_string ", ") largs;
+ prerr_string " ====";
+ prerr_newline (); ());
+ Debug_fun.debug_print_no_buff "==== <LPARSE.lexp_call>(body) ";
+ Debug_fun.debug_print_lexp body;
+ Debug_fun.do_debug (fun () -> prerr_string " =="; prerr_newline ();() );
+ Debug_fun.debug_print_no_buff "==== <LPARSE.lexp_call>(ltp) ";
+ Debug_fun.debug_print_lexp ltp;
+ Debug_fun.do_debug (fun () -> prerr_string " ===="; prerr_newline ();() );
lexp_error loc ("The function \"" ^ name ^ "\" was not defined");
let vf = (make_var name (-1) loc) in
Call(vf, new_args), ltp in
=====================================
tests/lparse_test.ml
=====================================
--- a/tests/lparse_test.ml
+++ b/tests/lparse_test.ml
@@ -3,6 +3,11 @@ open Lparse
open Fmt_lexp
open Utest_lib
+open Pexp
+open Lexp
+
+open Builtin
+
let test
(input_gen: (unit -> 'a list))
(fmt: 'b list -> string list)
@@ -24,7 +29,9 @@ let generate_tests (name: string)
(fun () -> if res then success () else failure ()))
(test input_gen fmt tester)
-let input = "x = lambda x -> x;"
+(* let input = "y = lambda x -> x + 1;" *)
+let input = "id = lambda (α : Type) ≡> lambda x : α -> x;
+res = id 3;"
let generate_lexp_from_str str =
List.hd ((fun (lst, _) ->
@@ -37,6 +44,76 @@ let _ = generate_tests
"TYPECHECK"
(fun () -> [generate_lexp_from_str input])
(fun x -> List.map string_of_lxp x)
- (fun x -> (x, false))
+ (fun x -> (x, true))
+
+let lctx = default_lctx
+let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () ->
+
+ let dcode = "
+ sqr = lambda (x) -> x * x;
+ cube = lambda (x) -> x * (sqr x);
+
+ mult = lambda (x) -> lambda (y) -> x * y;
+
+ twice = (mult 2);
+
+ let_fun = lambda (x) ->
+ let a = (twice x); b = (mult 2 x); in
+ a + b;" in
+
+ let ret1, _ = lexp_decl_str dcode lctx in
+
+ let to_str decls =
+ let str = _lexp_str_decls (!compact_ppctx) (List.flatten ret1) in
+ List.fold_left (fun str lxp -> str ^ lxp) "" str in
+
+ (* Cast to string *)
+ let str1 = to_str ret1 in
+
+ print_string str1;
+
+ (* read code again *)
+ let ret2, _ = lexp_decl_str str1 lctx in
+
+ (* Cast to string *)
+ let str2 = to_str ret2 in
+
+ if str1 = str2 then success () else failure ()
+))
+
+(*
+let set_to_list s =
+ StringSet.fold (fun g a -> g::a) s []
+
+let _ = (add_test "LEXP" "Free Variable" (fun () ->
+
+ let dcode = "
+ a = 2;
+ b = 3;
+ f = lambda n -> (a + n); % a is a fv
+ g = lambda x -> ((f b) + a + x); % f,a,b are fv
+ " in
+
+ let ret = pexp_decl_str dcode in
+ let g = match List.rev ret with
+ | (_, g, _)::_ -> g
+ | _ -> raise (Unexpected_result "Unexpected empty list") in
+
+ let (bound, free) = free_variable g in
+
+ let bound = set_to_list bound in
+ let (free, _) = free in
+
+ match bound with
+ | ["x"] ->(
+ match free with
+ | ["_+_"; "f"; "b"; "a"] -> success ()
+ | _ -> failure ())
+ | _ -> failure ()
+
+)) *)
+
+(* run all tests *)
+let _ = run_all ()
let _ = run_all ()
=====================================
tests/unify_test.ml
=====================================
--- a/tests/unify_test.ml
+++ b/tests/unify_test.ml
@@ -152,17 +152,17 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
::(input_lambda2 , input_lambda3 , Constraint)
::(input_lambda3 , input_lambda3 , Equivalent)
- ::(input_arrow2 , input_int_4 , Nothing)
- ::(input_arrow2 , input_induct , Nothing)
- ::(input_arrow2 , input_case , Constraint)
+ ::(input_arrow2 , input_int_4 , Unification) (* changes in lexp_p_infer & lexp_p_check *)
+ ::(input_arrow2 , input_induct , Unification) (* changed the "output" of lexp_decl_str*)
+ ::(input_arrow2 , input_case , Constraint) (* which changed the type of the Lexp*)
::(input_arrow2 , input_case2 , Constraint)
::(input_arrow2 , input_let , Constraint)
- ::(input_arrow2 , input_induct , Nothing)
- ::(input_arrow2 , input_lambda , Nothing)
- ::(input_arrow2 , input_lambda2 , Nothing)
- ::(input_arrow2 , input_arrow3 , Constraint) (* It's a constraint because we don't know yet the type *)
- ::(input_arrow3 , input_arrow , Constraint) (* of the var inside the arrow *)
- ::(input_arrow2 , input_arrow , Equivalent)
+ ::(input_arrow2 , input_induct , Unification)
+ ::(input_arrow2 , input_lambda , Unification)
+ ::(input_arrow2 , input_lambda2 , Unification)
+ ::(input_arrow2 , input_arrow3 , Unification)
+ ::(input_arrow3 , input_arrow , Unification)
+ ::(input_arrow2 , input_arrow , Unification)
::(input_arrow3 , input_arrow3 , Equivalent)
::(input_type , input_type_t , Equivalent)
=====================================
tests/utest_lib.ml
=====================================
--- a/tests/utest_lib.ml
+++ b/tests/utest_lib.ml
@@ -117,6 +117,12 @@ let ut_string2 = ut_string 2
let unexpected_throw sk tk e =
ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n");
ut_string2 "[ ] UNEXPECTED THROW:\n";
+ ut_string2 "[ ] ----------------------------- Callstack (20): -----------------------------------------\n";
+ ut_string2 ("[ ] " ^ (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20)));
+ ut_string2 "[ ] ---------------------------------------------------------------------------------------\n";
+ ut_string2 "[ ] ----------------------------- Backtrace: ----------------------------------------------\n";
+ ut_string2 ("[ ] " ^ (Printexc.get_backtrace ()) ^ "\n");
+ ut_string2 "[ ] ---------------------------------------------------------------------------------------\n";
ut_string2 "[ ] "; ut_string2 ((Printexc.to_string e) ^ "\n" ^ reset)
let _expect_equal_t to_string value expect =
View it on GitLab: https://gitlab.com/monnier/typer/compare/304245b63c5caed07861573d5be8e8ca89…
2
1