BONNEVALLE Vincent pushed to branch unification 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.
- - - - - 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.
- - - - - 43003f8d by Stefan Monnier at 2016-08-27T18:04:58+02: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.
- - - - - 4b31963e by Stefan Monnier at 2016-08-27T18:08:13+02: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.
- - - - - 6637588f by n3f4s at 2016-08-27T18:08:13+02:00 merge
- - - - - ac470790 by n3f4s at 2016-08-27T18:08:13+02:00 merge
- - - - - 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.
- - - - - 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.
- - - - - 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.
- - - - - 89b8df07 by Stefan Monnier at 2016-08-28T22:58:52-04:00 * btl/types.typer (sexp_dispatch_): Generalize type
- - - - - 531da09a by n3f4s at 2016-08-31T17:03:56+02:00 remove code in comment
- - - - - 133522c1 by n3f4s at 2016-08-31T17:04:38+02:00 fix infinite recursion in push_susp
add check for Identity in Metavar/Var case in push_susp
- - - - - 465e8df3 by n3f4s at 2016-08-31T17:05:43+02:00 remove trailing space
- - - - - bd6f086b by Pierre Delaunay at 2016-09-01T16:05:48-04:00 updated macro handling. implemented type_ macro. attributes are not working
Changes to be committed: * modified: btl/types.typer * modified: src/builtin.ml * modified: src/lparse.ml - updated macro handling * new file: samples/inductive.typer - type_ macro implementation
- - - - - 36b6254a by n3f4s at 2016-09-06T21:51:02+02:00 change type of metavar type in Pmetavar (infer)
- - - - - 63b652c6 by n3f4s at 2016-09-06T21:53:45+02:00 change debug output
- - - - - 915ca70f by Stefan Monnier at 2016-09-07T12:37:50-04:00 * src/opslexp.ml (lexp_whnf): Add various missing cases.
- - - - - c34bcc0a by n3f4s at 2016-09-07T19:39:45+02:00 add metavar management in lexp_whnf
- - - - - 913d45e4 by n3f4s at 2016-09-07T21:06:44+02:00 Merge branch 'master' into unification
- - - - - 1009a3c7 by n3f4s at 2016-09-07T22:29:34+02:00 add metavar handlind in lexp_whnf
- - - - - cd269106 by n3f4s at 2016-09-08T16:54:30+02:00 better lexp formatting
- - - - -
22 changed files:
- DESIGN - btl/types.typer - doc/manual.texi - + samples/inductive.typer - samples/quote.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt_lexp.ml - src/grammar.ml - src/lexp.ml - src/lparse.ml - src/typecheck.ml → src/opslexp.ml - src/util.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
@@ -1610,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 @@ -1698,23 +1797,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 @@ -35,7 +35,6 @@ % Base Types % -----------------------------------------------------
-Type = Built-in "Type"; Int = Built-in "Int"; Float = Built-in "Float"; String = Built-in "String"; @@ -72,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 tl)); + | 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 @@ -97,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 @@ -137,10 +139,22 @@ bind = Built-in "bind" ( FileHandle = Built-in "FileHandle";
% define operation on file handle +%% 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! 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); + IO a -> b -> b);
open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); @@ -163,6 +177,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.
===================================== samples/inductive.typer ===================================== --- /dev/null +++ b/samples/inductive.typer @@ -0,0 +1,46 @@ +type-impl = lambda (x : List Sexp) -> + % x follow the mask -> (_|_ Nat zero (succ Nat)) + % Type name --^ ^------^ constructors + + % Get expression + let expr = head (a := Sexp) x in + let sexp_nil = nil (a := Sexp) in + + % Expression is node_ (symbol_ "|") (list) + % we only care about the list bit + + let get-list = (lambda (node : Sexp) -> + sexp_dispatch_ (a := List Sexp) node + (lambda (op : Sexp) -> (lambda (lst : List Sexp) -> lst)) % Nodes + (lambda (str : String) -> sexp_nil) % Symbol + (lambda (str : String) -> sexp_nil) % String + (lambda (int : Int) -> sexp_nil) % Integer + (lambda (float : Float) -> sexp_nil) % Float + (lambda (lst : List Sexp) -> sexp_nil)) in % List of Sexp + + let lst = get-list expr in + + let name = head (a := Sexp) lst in + let ctor = tail (a := Sexp) lst in + + % Create a forward declaration in case the declaration is recursive + let fdecl = node_ (symbol_ "_:_") + (cons (a := Sexp) name + (cons (a := Sexp) (symbol_ "Type") sexp_nil)) in + + % Create the inductive type definition + let inductive = node_ (symbol_ "inductive_") + (cons (a := Sexp) (symbol_ "dlabel") ctor) in + + let decl = node_ (symbol_ "_=_") + (cons (a := Sexp) name + (cons (a := Sexp) inductive sexp_nil)) in + + cons (a := Sexp) fdecl + (cons (a := Sexp) decl sexp_nil); + +type_ = Macro_ type-impl; + +type Nat + | zero + | succ Nat;
===================================== 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
===================================== 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 @@ -56,38 +56,52 @@ let predef_name = [ "True"; "False"; "Bool"; + "Macro"; ]
let builtin_size = ref 0
-let predef_map : predef_table = +let default_predef_map : predef_table = (* add predef name, expr will be populated when parsing *) List.fold_left (fun m name -> SMap.add name (ref None) m) SMap.empty predef_name
+let predef_map = ref default_predef_map + let get_predef_raw (name: string) : lexp = - match !(SMap.find name predef_map) with + match !(SMap.find name (!predef_map)) with | Some exp -> exp | None -> builtin_error dloc "Try to access an empty predefined"
-let get_predef name ctx = - let r = (get_size ctx) - !builtin_size in - let v = mkSusp (get_predef_raw name) (S.shift r) in - v +let get_predef_option (name: string) ctx = + let r = (get_size ctx) - !builtin_size - 1 in + match !(SMap.find name (!predef_map)) with + | Some exp -> Some (mkSusp exp (S.shift r)) + | None -> None
+let get_predef (name: string) ctx = + let r = (get_size ctx) - !builtin_size - 1 in + let p = get_predef_raw name in + (mkSusp p (S.shift r))
let set_predef name lexp = - SMap.find name predef_map := lexp + SMap.find name (!predef_map) := lexp + +let dump_predef () = + let _ = SMap.iter (fun key item -> + print_string key; print_string " "; + let _ = match !item with + | Some lxp -> lexp_print lxp + | None -> print_string "None"; in + print_string "\n") !predef_map in ()
(* 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)) @@ -166,13 +180,11 @@ let olist2tlist_rte lst = (* Typer list to Ocaml list *) let rec tlist2olist acc expr = match expr with - | Vcons((_, "cons"), [hd; tl]) -> - tlist2olist (hd::acc) tl + | Vcons((_, "cons"), [hd; tl]) -> tlist2olist (hd::acc) tl | Vcons((_, "nil"), []) -> List.rev acc | _ -> print_string (value_name expr); print_string "\n"; - value_print expr; print_newline (); - + value_print expr; builtin_error dloc "List conversion failure'"
let make_node loc depth args_val ctx = @@ -236,15 +248,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 =
@@ -303,7 +308,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 = @@ -322,6 +327,8 @@ let has_attribute_impl loc largs ctx ftype =
let b = has_property ctx (vi, vn) (ai, an) in
+ + let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in rvar, (get_predef "Bool" ctx)
@@ -331,7 +338,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
@@ -347,8 +354,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 +376,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/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 *) @@ -99,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 = @@ -146,15 +139,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/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/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -37,23 +37,24 @@ and pp_ocaml_string_of_subst s =
and string_of_lxp lxp = match lxp with - | Imm (Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")" - | Imm (String (_, value)) -> "String(" ^ value ^ ")" - | Imm (Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")" - | Cons (((_,name),_),_) -> "Cons(" ^ name ^ ")" - | Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")" - | Let (_) -> "Let(..)" - | Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")" - | 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(...)" - | Inductive _ -> ("Inductive") ^ "(...)" - | Sort (_, s) -> ("Sort") ^ "(" ^ string_of_sort s ^ ")" - | SortLevel l -> ("SortLevel") ^ "(" ^ string_of_sort_level l ^ ")" - | Case _ -> ("Case") ^ "(...)" - | Susp (v, s) -> "Susp(" ^ (string_of_lxp v) ^ ", " ^ (string_of_subst s) ^ ")" - | _ -> "Unidentified Lexp" + | Imm (Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")" + | Imm (String (_, value)) -> "String(" ^ value ^ ")" + | Imm (Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")" + | Cons (((_,name),_),_) -> "Cons(" ^ name ^ ")" + | Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")" + | Let (_) -> "Let(..)" + | Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")" + | Arrow (kind, Some(_, name), a, _, b) -> name ^ ":Arrow(" ^ (string_of_lxp a) ^ ":" ^ string_of_kind kind ^ " => " ^ (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(...)" + | Inductive _ -> ("Inductive") ^ "(...)" + | Sort (_, s) -> ("Sort") ^ "(" ^ string_of_sort s ^ ")" + | SortLevel l -> ("SortLevel") ^ "(" ^ string_of_sort_level l ^ ")" + | Case _ -> ("Case") ^ "(...)" + | Susp (v, s) -> "Susp(" ^ (string_of_lxp v) ^ ", " ^ (string_of_subst s) ^ ")" + | _ -> "Unidentified Lexp"
and string_of_kind = function | Aexplicit -> "Aexplicit" @@ -125,3 +126,15 @@ let rec string_of_pexp pxp = | Pcons ( (_, s), (_, s2) ) -> "Pcons (" ^ s ^ ", " ^ s2 ^ ")" | Pcase _ -> "Pcase (...)" | _ -> "Pexp not handled" + + +(* let rec string_of_lexp_ctx (senv, env, prop) = *) + (* "(" ^ (string_of_senv senv) ^ "\n" ^ (string_of_env env) ^ "\n" ^ (string_of_prop prop) ^ ")" *) +(* and string_of_senv (len, sc) = *) + (* "(" ^ string_of_int len ^ ",\n " ^ (string_of_scope sc) ^ ")" *) +(* and string_of_scope sc = *) + (* "(" ^ *) + (* Debruijn.StringMap.fold (fun key value acc -> acc ^ ", (" ^ key ^ string_of_int value ^ ")") sc "" *) + (* ^ ")" *) +(* and string_of_env env = *) +
===================================== 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) ]
===================================== 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
@@ -332,7 +323,9 @@ let rec push_susp e s = (* Push a suspension one level down. *) push_susp e (scompose s' s) | (Var _ | Metavar _) -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *) - push_susp (mkSusp e s) S.identity + if S.identity_p s + then e + else push_susp (mkSusp e s) S.identity
let nosusp e = (* Return `e` without `Susp`. *) match e with @@ -353,105 +346,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 @@ -50,7 +50,7 @@ open Builtin
module Unif = Unification
-module TC = Typecheck +module OL = Opslexp module EL = Elexp module SU = Subst
@@ -156,7 +156,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"; @@ -193,11 +193,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) -> @@ -228,7 +227,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 @@ -241,7 +240,11 @@ 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"; [], [] + | _ -> lexp_error loc "Not an Inductive Type"; + Debug_fun.do_debug (fun () -> + print_string ("idt : " ^ Fmt_lexp.string_of_lxp (nosusp idt) ^ ", p : " ^ (Fmt_lexp.string_of_pexp p)); + print_newline (); ()); + [], [] in
(* build Arrow type *) @@ -264,8 +267,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = lexp_case None (loc, target, patterns) ctx i
| Pmetavar _ -> (let meta = mkMetavar () (*TODO *) + and type_ = mkMetavar () 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*)) + (meta, type_) (* FIXME return the right type *))
| Phastype (_, pxp, ptp) -> let ltp, _ = lexp_infer ptp ctx in @@ -304,7 +308,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = in let infer_lambda_body kind var body subst = (* Read var type from the provided type *) - let ltp, lbtp = match nosusp t with + let ltp, lbtp = match nosusp t (* t is captured *) with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | lxp -> (unify_with_arrow lxp kind subst) in @@ -340,11 +344,14 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = * Built-in *) | Builtin _ -> e | _ -> - (match Unif.unify inferred_t t Unif.empty_subst with (* cause eval test to fail : too many arguments *) + (match Unif.unify inferred_t t subst with | Some subst -> global_substitution := subst; inferred_t | None -> debug_msg ( let print_lxp str = print_string (Fmt_lexp.colored_string_of_lxp str Fmt_lexp.str_yellow Fmt_lexp.str_magenta) in + Debug_fun.do_debug (fun () -> + prerr_endline ("0 pxp " ^ Fmt_lexp.string_of_pexp p); + ()); 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"; @@ -416,8 +423,9 @@ 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 meta_ctx, _ = !global_substitution in
let from_lctx ctx = try (from_lctx ctx) with e ->( @@ -425,199 +433,144 @@ 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 subst ctx = - match (nosusp ltp), args with - | _, [] -> ltp - | 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) ^ " 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 = - match nosusp ltp with - (* Error case *) - | Arrow (Aexplicit, _, _, _, _) when (List.length largs <= 0) -> [] - - (* 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 []) - - (* 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"*) - | _ -> 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 body, ltp = _lexp_p_infer func ctx (i + 1) in let ltp = nosusp ltp in - - let handle_named_call (loc, name) = + Debug_fun.do_debug (fun () -> + prerr_endline ">>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"; + prerr_endline ("ltp : " ^ Fmt_lexp.string_of_lxp ltp); + prerr_endline ("body : " ^ Fmt_lexp.string_of_lxp body); + prerr_endline (string_of_int (List.length sargs) ^ " args"); + prerr_endline "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<"; + prerr_newline ();();); + + let rec handle_fun_args largs sargs ltp = match sargs with + | [] -> largs, ltp + | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs + (* Explicit-implicit argument. *) + -> (match OL.lexp_whnf ltp ctx meta_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 OL.lexp_whnf ltp ctx meta_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" + | e -> Debug_fun.do_debug (fun () -> + print_endline ("<>explicit arg : " ^ Fmt_lexp.string_of_lxp ltp); + print_endline ("<>explicit res : " ^ Fmt_lexp.string_of_lxp e); + ()); + lexp_fatal (sexp_location sarg) + "Explicit arg to non-function") in + + let handle_funcall () = + (* Here we use lexp_whnf on actual code, but it's OK + * because we only use the result when it's a "predefined constant". *) + match OL.lexp_whnf body ctx meta_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 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 - 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 + let largs, ret_type = handle_fun_args [] sargs ltp in + Call (body, List.rev largs), ret_type in + + let handle_macro_call () = + (* FIXME: We shouldn't look at `body` here at all: + * Instead, we should pass `body` (along with `arg`) to + * a `typer__expand_macro` function predefined in types.typer. *) + let lxp = match OL.lexp_whnf body ctx meta_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"; + lexp_fatal loc "Macro is ill formed" in + + (* Build function to be called *) + let arg = olist2tlist_lexp sargs ctx in
- | false, _ -> - lexp_error loc "Use of "Built-in" in user code"; - dlxp, dltype) + let lxp = Call(lxp, [(Aexplicit, arg)]) in + let elexp = OL.erase_type lxp in + let rctx = (from_lctx ctx 0) in
- | e -> - 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 call, ret_type + _global_eval_trace := [];
- 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 - - let handle_macro_call (loc, name) = - (* check for builtin *) - match is_builtin_macro name with - | true -> - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - (get_macro_impl loc name) loc largs ctx ltp - - (* 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 - | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | _ -> - 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 - - (* Build function to be called *) - let arg = olist2tlist_lexp sargs ctx in - - let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = EL.erase_type lxp in - let rctx = (from_lctx ctx 0) in - - _global_eval_trace := []; - - let vxp = try eval elexp rctx - with e -> - print_eval_trace (); - raise e in - - let sxp = match vxp with - | Vsexp(sxp) -> sxp - (* Those are sexp converted by the eval function *) - | Vint(i) -> Integer(dloc, i) - | Vstring(s) -> String(dloc, s) - | Vfloat(f) -> Float(dloc, f) - (* I have vdum here WHY *) - | v -> debug_msg (value_print v); - lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in - - let pxp = pexp_parse sxp in - _lexp_p_infer pxp ctx (i + 1)) in + let vxp = try eval elexp rctx + with e -> + print_eval_trace (); + raise e in + + let sxp = match vxp with + | Vsexp(sxp) -> sxp + (* Those are sexp converted by the eval function *) + | Vint(i) -> Integer(dloc, i) + | Vstring(s) -> String(dloc, s) + | Vfloat(f) -> Float(dloc, f) + (* I have vdum here WHY *) + | v -> debug_msg (value_print v); + lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in + + let pxp = pexp_parse sxp in + _lexp_p_infer pxp ctx (i + 1) in + + (* This is the builtin Macro type *) + let macro_type = match get_predef_option "Macro" ctx with + | Some lxp -> lxp + (* When type.typer is being parsed and the predef is not yet + * available *) + | None -> dltype in
(* determine function type *) - match fun_name, ltp with - (* Anonymous *) - | ((Plambda _), _) -> - (* Process Arguments *) + match func, ltp with + | macro, _ when OL.conv_p ltp macro_type -> ( + match macro with + (* Special form *) + | Pvar(l, name) when is_builtin_macro name -> 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 + (get_macro_impl loc name) loc largs ctx ltp
- | (Pvar (l, n), Var((_, "Macro"), _)) -> - (* FIXME: check db_idx points to a Macro type *) - handle_macro_call (l, n) + (* true macro *) + | _ -> handle_macro_call ())
- (* 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" + (* FIXME: Handle special-forms here as well! *) + | _ -> handle_funcall ()
(* Read a pattern and create the equivalent representation *) @@ -631,15 +584,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 -> @@ -717,9 +670,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 @@ -744,12 +697,14 @@ 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 *) let decls = eval elexp rctx in
+ value_print decls; print_string "\n"; + (* convert typer list to ocaml *) let decls = tlist2olist [] decls in
@@ -757,7 +712,10 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = let decls = List.map (fun g -> match g with | Vsexp(sxp) -> sxp - | _ -> lexp_fatal loc "Macro expects sexp list") decls in + | _ -> + print_string ((value_name g) ^ " : "); + value_print g; print_string "\n"; + lexp_fatal loc "Macro expects sexp list") decls in
(* read as pexp_declaraton *) pexp_decls_all decls, ctx) @@ -893,7 +851,7 @@ and _lexp_rec_decl decls ctx i = | Ldecl ((l, s), Some pxp, None) -> let lxp, ltp = lexp_p_infer pxp vctx in lst := ((l, s), lxp, ltp)::!lst; - (* replace forward ref by its true value *) + (* replace forward ref by its true value *) replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp)
(* lexp check *) @@ -922,8 +880,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 [])
@@ -1031,15 +989,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
@@ -1062,7 +1018,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 @@ -1070,30 +1026,12 @@ 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; - + lexp_warning dloc "Predef not found"; + 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 * --------------------------------------------------------- *) @@ -1123,13 +1061,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,11 +28,14 @@ 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
let conv_erase = true (* If true, conv ignores erased terms. *)
@@ -99,6 +102,70 @@ 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 _). + * FIXME: This should be memoized! + * + * BEWARE: As a general rule lexp_whnf should not be used on actual *code* + * but only on *types*. If you must use it on code, be sure to use its + * return value as little as possible since WHNF will inherently introduce + * call-by-name behavior. *) +let rec lexp_whnf e ctx meta_ctx = match e with + (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) + | Var v -> (match DB.env_lookup_expr ctx v with + | None -> e + (* We can do this blindly even for recursive definitions! + * IOW the risk of inf-looping should only show up when doing + * things like full normalization (e.g. lexp_conv_p). *) + | Some e' -> lexp_whnf e' ctx meta_ctx) + | Susp (e, s) -> lexp_whnf (push_susp e s) ctx meta_ctx + | Call (e, []) -> lexp_whnf e ctx meta_ctx + | Call (e, (((_, arg)::args) as xs)) -> + (match lexp_whnf e ctx meta_ctx with + | Lambda (_, _, _, body) -> + (* Here we apply whnf to the arg eagerly to kind of stay closer + * to the idea of call-by-value, although in this context + * we can't really make sure we always reduce the arg to a value. *) + lexp_whnf (Call (push_susp body (S.substitute (lexp_whnf arg ctx meta_ctx)), + args)) + ctx meta_ctx + | Call (e', xs1) -> Call (e', List.append xs1 xs) + | e' -> Call (e', xs)) + | Case (l, e, bt, rt, branches, default) -> + let reduce name aargs = + try + let (_, _, branch) = SMap.find name branches in + let (subst, _) + = List.fold_left + (fun (s,d) (_, arg) -> + (S.Cons (L.mkSusp (lexp_whnf arg ctx meta_ctx) (S.shift d), s), + d + 1)) + (S.identity, 0) + aargs in + lexp_whnf (push_susp branch subst) ctx meta_ctx + with Not_found + -> match default + with | Some default -> lexp_whnf default ctx meta_ctx + | _ -> U.msg_error "WHNF" l + ("Unhandled constructor " ^ + name ^ "in case expression"); + Case (l, e, bt, rt, branches, default) in + (match lexp_whnf e ctx meta_ctx with + | Cons (_, (_, name)) -> reduce name [] + | Call (Cons (_, (_, name)), aargs) -> reduce name aargs + | e' -> Case (l, e', bt, rt, branches, default)) + | Metavar (idx, _, _) -> lexp_whnf (Unification.VMap.find idx meta_ctx) ctx meta_ctx + | e -> e + + (********* Testing if a lexp is properly typed *********)
@@ -154,7 +221,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) @@ -162,12 +229,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) @@ -193,7 +260,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) @@ -276,8 +343,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 @@ -292,3 +359,72 @@ 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 (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)) + + | 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 extent. *) + | 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 *)
===================================== 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/compare/a964be1b7aecdb36af4acafa1986ea622f7...
Afficher les réponses par date