Stefan pushed to branch master at Stefan / Typer

Commits: f9a5b2f2 by Stefan Monnier at 2016-11-26T11:23:49-05:00 Add new ##... syntax to refer to existing builtins

* src/builtin.ml (lmap): New var. (add_builtin_cst): New function.

* src/lexp.ml (mkSusp): Don't bother suspending immediates. (lexp_unparse): Use Pbuiltin. (_lexp_to_str): Use the ##... syntax.

* src/lparse.ml (macromap): Adjust to earlier change. (make_macro_map): Use it. (infer): Handle Pbuiltin.

* src/pexp.ml (pexp): Add Pbuiltin constructor. (pexp_parse): Recognize new ##... syntax. (pexp_location, pexp_unparse): Handle it.

* src/prelexer.ml (string_sub): Move to util.ml.

- - - - -

8 changed files:

- DESIGN - src/builtin.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/prelexer.ml - src/util.ml - tests/eval_test.ml

Changes:

===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1219,22 +1219,30 @@ For IO the macro would return "bind e1 e2", whereas for "a * b" it would use

Here's an example of a use of partial functions:

- type Exp (e : Env) := - Var i (t : lookup i e) + type Exp (e : Env) + | Var i (t : lookup i e)

where "lookup" might fail. Without partial functions, we have to use a relational style, as in:

- type Exp (e : Env) := - Var i (_: lookup i e t) t + type Exp (e : Env) + | Var i (_: lookup i e t) t

In the present case, we could make "lookup" return False, but if we change it to:

- type Exp (e : Env) (τ : EType) := - SetVar i (v : Exp Env (lookup i e)) + type Exp (e : Env) (τ : EType) + | SetVar i (v : Exp Env (lookup i e))

-Suddenly, this doesn't work any more. +Suddenly, this doesn't work any more. We would then have to do something +like, have `lookup` return an `Option` and then do: + + type Exp (e : Env) (τ : EType) + | SetVar i (v : (case lookup i e + | Some t => Exp Env t + | None -> False)) + +It would be neat to have some way to "automate" this.

* Erasable constructors

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1,9 +1,6 @@ -(* - * Typer Compiler +(* builtin.ml --- Infrastructure to define built-in primitives * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2016 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -25,8 +22,34 @@ * * --------------------------------------------------------------------------- * - * Description: - * Hold built-in types definition and built-in functions implementation + * There are several different issues with how to make the compiler's code + * interact with code defined in Typer: + * + * ** Exporting primitives + * + * I.e. how to give a name and a type to a primitive implemented in OCaml + * + * There are several conflicting desires, here: we'd generally want the name, + * the type (and the association) to be close to the primitive's definition, so + * that adding a new primitive doesn't require changes in many files. + * + * But it's also good to have the type written in some Typer file, both for + * the convenience of writing the code in Typer syntax with typer-mode support, + * and also because error messages can easily refer to that file, so it can be + * used for user-documentation. + * + * ** Importing definitions + * + * Sometimes we want some part of the core to be defined in Typer and used + * from OCaml. Examples are the type `Macro` along with the `expand-macro` + * function or the type Bool/true/false used with various primitives. + * + * ** Intertwined dependencies + * + * The various importing/exporting might need to be interlaced. Some exported + * functions's types will want to refer to imported types, while some imported + * definitions may want to refer to exported definitions. So we'd like to be + * able to do them in "any" order. * * ---------------------------------------------------------------------------*)

@@ -34,6 +57,8 @@ open Util

open Sexp (* Integer/Float *) open Pexp (* arg_kind *) +module L = Lexp +module OL = Opslexp open Lexp

module DB = Debruijn @@ -168,9 +193,11 @@ let decltype_impl loc largs ctx ftype = (* mkSusp prop (S.shift (var_i + 1)) *) ltype

+(* Map of lexp builtin elements accessible via (## <name>). *) +let lmap = ref (SMap.empty : (L.lexp * L.ltype) SMap.t)

- - - - - +let add_builtin_cst (name : string) (e : lexp) + = let map = !lmap in + assert (not (SMap.mem name map)); + let t = OL.check VMap.empty Myers.nil e in + lmap := SMap.add name (e, t) map

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -166,6 +166,8 @@ let rec mkSusp e s = * 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 + (* FIXME: `Builtin` shouuld be treated like `Imm`. *) + | Imm _ -> e | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v | Metavar (vn, s', vd, t) -> mkMetavar (vn, scompose s' s, vd, mkSusp t s) @@ -349,10 +351,7 @@ let rec lexp_unparse lxp = match lxp with | Susp _ as e -> lexp_unparse (nosusp e) | Imm (sexp) -> Pimm (sexp) - | Builtin ((loc, name), _, None) -> Pvar((loc, name)) - | Builtin ((loc, name), ltp, _ ) - -> Pcall(Pvar((loc, name)), [pexp_unparse (lexp_unparse ltp)]) - + | Builtin (s, _, _) -> Pbuiltin s | Var ((loc, name), _) -> Pvar((loc, name)) | Cons (t, ctor) -> Pcons (lexp_unparse t, ctor) | Lambda (kind, vdef, ltp, body) -> @@ -655,15 +654,16 @@ and _lexp_to_str ctx exp = ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name) ^ " => " ^ (lexp_to_stri 1 df))

- | Builtin ((_, name), _, _) -> name + | Builtin ((_, name), _, _) -> "##" ^ name

- | Sort (_, Stype (SortLevel SLz)) -> "Type_0" - | Sort (_, Stype _) -> "Type_?" - | Sort (_, StypeOmega) -> "Type_ω" - | Sort (_, StypeLevel) -> "Type_Level" + | Sort (_, Stype (SortLevel SLz)) -> "##Type" + | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" + | Sort (_, StypeLevel) -> "##TypeLevel" + | Sort (_, Stype _) -> "##Type_?" (* FIXME! *) + | Sort (_, StypeOmega) -> "##Type_ω" (* FIXME: Should never happen! *)

- | SortLevel (SLz) -> "<Level0>" - | SortLevel (SLsucc e) -> "<LevelS?>" + | SortLevel (SLz) -> "##TypeLevel.z" + | SortLevel (SLsucc e) -> "##TypeLevel.succ"

and lexp_str_ctor ctx ctors = SMap.fold (fun key value str

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -43,10 +43,11 @@ open Lexp

open Env open Debruijn +module DB = Debruijn open Eval

open Grammar -open Builtin +module BI = Builtin

module Unif = Unification

@@ -113,7 +114,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp =

(* Builtin Macro i.e, special forms *) type macromap = - (location -> lexp list -> elab_context -> lexp -> (lexp * lexp)) SMap.t + (location -> lexp list -> elab_context -> lexp -> lexp) SMap.t

let elab_check_proper_type (ctx : elab_context) ltp var = let meta_ctx, _ = !global_substitution in @@ -247,6 +248,12 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = | _ -> pexp_error tloc p "Could not find type"; dltype)

+ | Pbuiltin (l,name) + -> (try SMap.find name (! BI.lmap) + with Not_found + -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); + dlxp, dltype) + (* Symbol i.e identifier. *) | Pvar (loc, name) -> (try @@ -808,7 +815,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = infer pxp ctx in

(* This is the builtin Macro type *) - let macro_type, macro_disp = match get_predef_option "Macro" ctx with + let macro_type, macro_disp = match BI.get_predef_option "Macro" ctx with | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx, true (* When type.typer is being parsed and the predef is not yet available *) | None -> dltype, false in @@ -867,9 +874,9 @@ and lexp_expand_dmacro macro_funct sargs ctx and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type =

(* Build the function to be called *) - let macro_expand = get_predef expand_fun ctx in + let macro_expand = BI.get_predef expand_fun ctx in let args = [(Aexplicit, macro_funct); - (Aexplicit, (olist2tlist_lexp sargs ctx))] in + (Aexplicit, (BI.olist2tlist_lexp sargs ctx))] in

let macro = mkCall (macro_expand, args) in let emacro = OL.erase_type macro in @@ -901,7 +908,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = let ret = lexp_expand_dmacro body sargs ctx in

(* convert typer list to ocaml *) - let decls = tlist2olist [] ret in + let decls = BI.tlist2olist [] ret in

(* extract sexp from result *) let decls = List.map (fun g -> @@ -1023,8 +1030,8 @@ and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list = * -------------------------------------------------------------------------- *) and builtin_macro = [ (* FIXME: These should be functions! *) - ("decltype", decltype_impl); - ("declexpr", declexpr_impl); + ("decltype", BI.decltype_impl); + ("declexpr", BI.declexpr_impl); (* FIXME: These are not macros but `special-forms`. * We should add here `let_in_`, `case_`, etc... *) ("get-attribute", get_attribute_impl); @@ -1033,7 +1040,7 @@ and builtin_macro = [ ("add-attribute", add_attribute_impl); ]

-and make_macro_map unit = +and make_macro_map unit : macromap = List.fold_left (fun map (name, funct) -> SMap.add name funct map) SMap.empty builtin_macro

@@ -1095,9 +1102,9 @@ and has_attribute_impl loc largs ctx ftype = | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in

try let _ = AttributeMap.find var map in - (get_predef "True" ctx) + BI.get_predef "True" ctx with Not_found -> - (get_predef "False" ctx) + BI.get_predef "False" ctx

(* Only print var info *) and lexp_print_var_info ctx = @@ -1154,7 +1161,7 @@ let default_lctx, default_rctx = List.iter (fun name -> let idx = senv_lookup name lctx in let v = Var((dloc, name), idx) in - set_predef name (Some v)) predef_name; + BI.set_predef name (Some v)) BI.predef_name; (* -- DONE -- *) lctx with e ->

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -39,6 +39,7 @@ type pvar = symbol type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) + | Pbuiltin of symbol | Pvar of pvar | Phastype of location * pexp * pexp | Pmetavar of pvar @@ -70,6 +71,7 @@ let rec pexp_location e = match e with (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s + | Pbuiltin (l,_) -> l | Pvar (l,_) -> l | Phastype (l,_,_) -> l | Pmetavar (l, _) -> l @@ -97,6 +99,18 @@ let rec pexp_parse (s : sexp) : pexp = (* | Symbol (l, "Type") -> Psort (l, Type) *) | Symbol (l, name) when String.length name > 0 && String.get name 0 == '?' -> Pmetavar (l, String.sub name 1 (String.length name - 1)) + | Symbol (l, name) when String.length name > 2 + && String.get name 0 == '#' + && String.get name 1 == '#' + -> Pbuiltin (l, string_sub name 2 (String.length name)) + (* | Node (Symbol (start, "##"), [Symbol s]) + * -> Pbuiltin s + * | Node (Symbol (start, "##"), [e]) + * -> pexp_error (sexp_location e) "Non-symbol argument to `##`"; + * Pmetavar (start, "") + * | Node (Symbol (start, "##"), _) + * -> pexp_error start "`##` takes exactly one argument"; + * Pmetavar (start, "") *) | Symbol s -> Pvar s | Node (Symbol (start, "_:_"), [e; t]) -> Phastype (start, pexp_parse e, pexp_parse t) @@ -297,8 +311,10 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s + | Pbuiltin (l,name) -> Symbol (l, "##" ^ name) + (* | Pbuiltin ((l,_) as s) -> Node (Symbol (l, "##"), [Symbol s]) *) | Pvar v -> Symbol v - | Pmetavar (l,name) -> Symbol (l,"?"^name) + | Pmetavar (l,name) -> Symbol (l, "?" ^ name) | Phastype (l,e,t) -> Node (Symbol (l, "_:_"), [pexp_unparse e; pexp_unparse t]) | Plet (start, decls, body) -> @@ -406,6 +422,7 @@ let pexp_print e = print_string (pexp_string e) let pexp_name e = match e with | Pimm _ -> "Pimm" + | Pbuiltin _ -> "Pbuiltin" | Pvar (_,_) -> "Pvar" | Phastype (_,_,_) -> "Phastype" | Pmetavar (_, _) -> "Pmetavar"

===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -46,8 +46,6 @@ type pretoken = (* FIXME: Add syntax for char constants (maybe 'c'). *) (* FIXME: Handle multiline strings. *)

-let string_sub str b e = String.sub str b (e - b) - let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) if utf8_head_p c then cp+1 else cp

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -90,6 +90,7 @@ let debug_msg expr = let not_implemented_error () = internal_error "not implemented"

let string_implode chars = String.concat "" (List.map (String.make 1) chars) +let string_sub str b e = String.sub str b (e - b)

let opt_map f x = match x with None -> None | Some x -> Some (f x)

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -190,7 +190,7 @@ let _ = test_eval_eqv_named three = succ two;

plus : Nat -> Nat -> Nat; - plus = lambda (x : Nat) -> lambda (y : Nat) -> case x + plus x y = case x | zero => y | succ z => succ (plus z y);")

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