Stefan pushed to branch master at Stefan / Typer
Commits: afa9309b by Stefan Monnier at 2016-12-02T09:11:41-05:00 Rewrite inductive-cons as a special-form; rename to datacons
* src/lparse.ml (infer): Remove Pcons case. (sform_datacons, sform_type): New functions. (register_special_forms): Name the initialization code. Use the two new sform_* functions. (dynamic_bind): New function. (default_lctx): Use them.
* src/pexp.ml (pexp): Remove Pcons.
* src/lexp.ml (pdatacons): New var. (lexp_unparse, lexp_unparse): Use it.
- - - - -
11 changed files:
- btl/builtins.typer - samples/autodiff.typer - samples/dependent.typer - samples/error.typer - samples/inductive.typer - samples/nat.typer - samples/test.typer - src/lexp.ml - src/lparse.ml - src/pexp.ml - tests/eval_test.ml
Changes:
===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -36,7 +36,7 @@ % -----------------------------------------------------
Unit = inductive_ Unit unit; -unit = inductive-cons Unit unit; +unit = datacons Unit unit;
% Basic operators _+_ = Built-in "Int.+" (Int -> Int -> Int); @@ -45,13 +45,13 @@ _*_ = Built-in "Int.*" (Int -> Int -> Int); _/_ = Built-in "Int./" (Int -> Int -> Int);
Bool = inductive_ (Boolean) (True) (False); -True = inductive-cons Bool True; -False = inductive-cons Bool False; +True = datacons Bool True; +False = datacons Bool False;
%Option : Type -> Type; Option = inductive_ (Option (a : Type)) (None) (Some a); -Some = inductive-cons Option Some; -None = inductive-cons Option None; +Some = datacons Option Some; +None = datacons Option None;
string_eq = Built-in "string_eq" (String -> String -> Bool); int_eq = Built-in "int_eq" (Int -> Int -> Bool); @@ -64,8 +64,8 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); List : Type -> Type; List = inductive_ (List (a : Type)) (nil) (cons a (List a));
-nil = inductive-cons List nil; -cons = inductive-cons List cons; +nil = datacons List nil; +cons = datacons List cons;
length : (a : Type) ≡> List a -> Int; length = lambda a ≡> @@ -109,8 +109,8 @@ Macro = inductive_ (Macro) (Macro_ (List Sexp -> Sexp)) (DMacro_ (List Sexp -> List Sexp));
-Macro_ = inductive-cons Macro Macro_ ; -DMacro_ = inductive-cons Macro DMacro_ ; +Macro_ = datacons Macro Macro_ ; +DMacro_ = datacons Macro DMacro_ ;
expand_macro_ : Macro -> List Sexp -> Sexp; expand_macro_ m args = case m
===================================== samples/autodiff.typer ===================================== --- a/samples/autodiff.typer +++ b/samples/autodiff.typer @@ -47,12 +47,12 @@ Sym = inductive_ (dSym) (inv Sym) (neg Sym);
-constant = inductive-cons Sym constant; -placeholder = inductive-cons Sym placeholder; -add = inductive-cons Sym add; -mult = inductive-cons Sym mult; -inv = inductive-cons Sym inv; -neg = inductive-cons Sym neg; +constant = datacons Sym constant; +placeholder = datacons Sym placeholder; +add = datacons Sym add; +mult = datacons Sym mult; +inv = datacons Sym inv; +neg = datacons Sym neg;
div : Sym -> Sym -> Sym; div = lambda (up : Sym) ->
===================================== samples/dependent.typer ===================================== --- a/samples/dependent.typer +++ b/samples/dependent.typer @@ -4,9 +4,9 @@ Reify = inductive_ (Reify (a : Type)) (RFloat (a = Float)) (RString (a = String));
-RInt = inductive-cons Reify RInt; -RFloat = inductive-cons Reify RFloat; -RString = inductive-cons Reify RString; +RInt = datacons Reify RInt; +RFloat = datacons Reify RFloat; +RString = datacons Reify RString;
float-to-int : Float -> Int; float-to-int x = 1;
===================================== samples/error.typer ===================================== --- a/samples/error.typer +++ b/samples/error.typer @@ -49,15 +49,15 @@ m = lambda n -> n; % > Root:
idt = inductive_ (idt) (cons1) (cons2 Int); -cons1 = inductive-cons idt cons1; -cons2 = inductive-cons idt cons2; -cons3 = inductive-cons idt cons3; +cons1 = datacons idt cons1; +cons2 = datacons idt cons2; +cons3 = datacons idt cons3;
% [!] Error [Ln 32, cl 28] LPARSE Not an Inductive Type % > Builtin: Int % > Root:
-cons4 = inductive-cons Int cons3; +cons4 = datacons Int cons3;
% /!\ Warning [Ln 70, cl 17] LPARSE Pattern cons2 is a duplicate. It will override previous pattern.
@@ -95,8 +95,8 @@ fun2 n = case n % [!] Error [Ln 86, cl 1] LPARSE Variable `fun4` declared but not defined!
% idtb = inductive_ (idtb) (cons1b) (cons2b Int); -% cons1b = inductive-cons idtb cons1b; -% cons2b = inductive-cons idtb cons2b; +% cons1b = datacons idtb cons1b; +% cons2b = datacons idtb cons2b;
% fun4 : idt -> Int; % fun4 n = case n @@ -109,4 +109,4 @@ fun2 n = case n % fun3 : idt -> Int; % fun3 n = case n % | cons1 => 1 -% | cons2 i => "AB"; \ No newline at end of file +% | cons2 i => "AB";
===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -6,12 +6,12 @@ make-decl var-name value-expr = (cons (a := Sexp) var-name (cons (a := Sexp) value-expr (nil (a := Sexp))));
-% build inductive-cons -% ctor-name = inductive-cons type-name ctor-name; +% build datacons +% ctor-name = datacons type-name ctor-name; make-cons : Sexp -> Sexp -> Sexp; make-cons ctor-name type-name = make-decl ctor-name - (node_ (symbol_ "inductive-cons") + (node_ (symbol_ "datacons") (cons (a := Sexp) type-name (cons (a := Sexp) ctor-name (nil (a := Sexp)))));
@@ -117,5 +117,5 @@ get-y p = case p | point x y => y; % transformed to: % Nat : Type; % Nat = inductive_ (Nat) (succ Nat) (zero); -% zero = inductive-cons Nat zero; -% succ = inductive-cons Nat succ; +% zero = datacons Nat zero; +% succ = datacons Nat succ;
===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -1,8 +1,8 @@ Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat);
-zero = inductive-cons Nat zero; -succ = inductive-cons Nat succ; +zero = datacons Nat zero; +succ = datacons Nat succ;
to-num : Nat -> Int; to-num = lambda (x : Nat) -> case x
===================================== samples/test.typer ===================================== --- a/samples/test.typer +++ b/samples/test.typer @@ -28,8 +28,8 @@ a = 3;
Nat : Type Nat = inductive_ (dummy_Nat) (zero) (succ Nat); -zero = inductive-cons Nat zero; -succ = inductive-cons Nat succ; +zero = datacons Nat zero; +succ = datacons Nat succ; toZero = lambda z -> case z | zero => zero @@ -53,8 +53,8 @@ plus = lambda x y -> List = inductive (dummy_List (α : Type)) (nil) (cons α (List α)); -nil = inductive-cons List nil; -cons = inductive-cons List cons; +nil = datacons List nil; +cons = datacons List cons; length : (α : Type) ≡> List α -> Nat; length = lambda α ≡> lambda (xs : List α) -> case xs @@ -70,7 +70,7 @@ length = lambda α ≡> lambda (xs : List α) ->
False = inductive (dummy_False); Unit = inductive (dummy_Unit) (unit); -unit = inductive-cons Unit unit; +unit = datacons Unit unit; Bool = inductive (dummy_Bool) (true) (false); -false = inductive-cons Bool false; -true = inductive-cons Bool true; +false = datacons Bool false; +true = datacons Bool true;
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -339,7 +339,7 @@ let lexp_name e = | Arrow _ -> "Arrow" | Lambda _ -> "lambda" | Call _ -> "Call" - | Cons _ -> "inductive-cons" + | Cons _ -> "datacons" | Case _ -> "case" | Inductive _ -> "inductive_" | Susp _ -> "Susp" @@ -349,6 +349,8 @@ let lexp_name e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel"
+let pdatacons = Pbuiltin (U.dummy_location, "datacons") + (* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = match lxp with @@ -356,7 +358,8 @@ let rec lexp_unparse lxp = | Imm (sexp) -> Pimm (sexp) | Builtin (s, _, _) -> Pbuiltin s | Var ((loc, name), _) -> Pvar((loc, name)) - | Cons (t, ctor) -> Pcons (lexp_unparse t, ctor) + | Cons (t, (l, name)) + -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body) | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> @@ -407,7 +410,10 @@ let rec lexp_unparse lxp = args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) - in Ppatcons (Pcons (bt, (loc, str)), pat_args), lexp_unparse bch + in (Ppatcons (Pcall (pdatacons, + [pexp_unparse bt; Symbol (loc, str)]), + pat_args), + lexp_unparse bch) ) (SMap.bindings branches) in
let pbranch = match default with @@ -583,7 +589,7 @@ and _lexp_to_str ctx exp = (make_indent 1) ^ (lexp_to_stri 1 lbody)
| Cons(t, (_, ctor_name)) -> - (keyword "inductive-cons ") ^ (lexp_to_str t) ^ " " ^ ctor_name + (keyword "datacons ") ^ (lexp_to_str t) ^ " " ^ ctor_name
| Call(fname, args) -> ( (* get function name *)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -335,50 +335,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype =
| Pcall (fname, args) -> infer_call fname args ctx
- | Pcons(t, sym) - -> let idt, _ = infer t ctx in - let (loc, cname) = sym in - let meta_ctx, _ = !global_substitution in - - (* Get constructor args. *) - let formal, args = match OL.lexp_whnf idt - (ectx_to_lctx ctx) meta_ctx with - | Inductive(_, _, formal, ctor_def) as lxp - -> (try formal, (SMap.find cname ctor_def) - with Not_found -> - lexp_error loc lxp - ("Constructor "" ^ cname ^ "" does not exist"); - [], []) - - | lxp -> lexp_error loc lxp ("`" ^ lexp_string idt - ^ "` is not an inductive type"); - [], [] in - - (* Build Arrow type. *) - let target = let targs, _ - = List.fold_right - (fun (ak, v, _) (targs, i) - -> ((ak, Var (v, i)) :: targs, - i - 1)) - formal - ([], List.length formal + List.length args - 1) in - mkCall (push_susp idt (S.shift (List.length formal - + List.length args)), - targs) in - let cons_type - = List.fold_left (fun ltp (kind, v, tp) - -> mkArrow (kind, v, tp, loc, ltp)) - target - (List.rev args) in - - (* Add Aerasable arguments. *) - let cons_type = List.fold_left - (fun ltp (kind, v, tp) - -> mkArrow (Aerasable, Some v, tp, loc, ltp)) - cons_type (List.rev formal) in - - mkCons(idt, sym), cons_type - | Phastype (_, pxp, ptp) -> let ltp = infer_type ptp ctx None in (check pxp ltp ctx, ltp) @@ -1102,6 +1058,30 @@ let sform_built_in ctx loc sargs = | false, _ -> error loc "Use of `Built-in` in user code"; dlxp
+let sform_datacons ctx loc sargs = + match sargs with + | [t; Symbol ((sloc, cname) as sym)] + -> let pt = pexp_parse t in + let idt, _ = infer pt ctx in + mkCons(idt, sym) + + | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; + dlxp + | _ -> sexp_error loc "##constr requires two arguments"; + dlxp + +(* Actually `Type_` could also be defined as a plain constant + * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) + * But it would be less efficient (such a lambda can't be passed as argument + * so it really can only be used applied to something, so it always generates + * β-redexes. Furthermore, I'm not sure if my PTS definition is correct to + * allow such a lambda. *) +let sform_type ctx loc sargs = + match sargs with + | [l] -> let l = pexp_parse l in + let l, _ = infer l ctx in + mkSort (loc, Stype l) + | _ -> sexp_error loc "##Type_ expects one argument"; dlxp
(* Only print var info *) and lexp_print_var_info ctx = @@ -1122,62 +1102,72 @@ and lexp_print_var_info ctx = done
(* Register special forms. *) -let _ = List.iter add_special_form - [ - ("Built-in", sform_built_in); - (* FIXME: We should add here `let_in_`, `case_`, etc... *) - ("get-attribute", sform_get_attribute); - ("new-attribute", sform_new_attribute); - ("has-attribute", sform_has_attribute); - ("add-attribute", sform_add_attribute); - (* FIXME: These should be functions! *) - ("decltype", sform_decltype); - ("declexpr", sform_declexpr); - ] +let register_special_forms () = + List.iter add_special_form + [ + ("Built-in", sform_built_in); + ("datacons", sform_datacons); + ("Type_", sform_type); + (* FIXME: We should add here `let_in_`, `case_`, etc... *) + ("get-attribute", sform_get_attribute); + ("new-attribute", sform_new_attribute); + ("has-attribute", sform_has_attribute); + ("add-attribute", sform_add_attribute); + (* FIXME: These should be functions! *) + ("decltype", sform_decltype); + ("declexpr", sform_declexpr); + ]
(* Default context with builtin types * --------------------------------------------------------- *)
+let dynamic_bind r v body = + let old = !r in + try r := v; + let res = body () in + r := old; + res + with e -> r := old; raise e + (* Make lxp context with built-in types *) -let default_lctx = - - (* Empty context *) - let lctx = make_elab_context in - let lctx = SMap.fold (fun key (e, t) ctx - -> if String.get key 0 = '-' then ctx - else ctx_define ctx (dloc, key) e t) - (!BI.lmap) lctx in - - (* Read BTL files *) - let pres = prelex_file (!btl_folder ^ "builtins.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; - - (* dump grouped decls * ) - List.iter (fun decls -> - print_string "["; - List.iter (fun ((_, s), _, _) -> - print_string (s ^ ", ")) decls; print_string "] \n") d; *) - - builtin_size := get_size lctx; - - (* Once default builtin are set we can populate the predef table *) - let lctx = try - List.iter (fun name -> - let idx = senv_lookup name lctx in - let v = Var((dloc, name), idx) in - BI.set_predef name v) BI.predef_name; - (* -- DONE -- *) - lctx +let default_lctx + = let _ = register_special_forms () in + (* Empty context *) + let lctx = make_elab_context in + let lctx = SMap.fold (fun key (e, t) ctx + -> if String.get key 0 = '-' then ctx + else ctx_define ctx (dloc, key) e t) + (!BI.lmap) lctx in + + (* Read BTL files *) + let pres = prelex_file (!btl_folder ^ "builtins.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 + + let d, lctx = dynamic_bind _parsing_internals true + (fun () -> lexp_p_decls pxps lctx) in + + (* dump grouped decls * ) + List.iter (fun decls -> + print_string "["; + List.iter (fun ((_, s), _, _) -> + print_string (s ^ ", ")) decls; print_string "] \n") d; *) + + builtin_size := get_size lctx; + + (* Once default builtin are set we can populate the predef table *) + let lctx = try + List.iter (fun name -> + let idx = senv_lookup name lctx in + let v = Var((dloc, name), idx) in + BI.set_predef name v) BI.predef_name; + (* -- DONE -- *) + lctx with e -> warning dloc "Predef not found"; lctx in - lctx + lctx
let default_rctx = EV.from_lctx default_lctx
===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -51,7 +51,6 @@ type pexp = * otherwise isomorphic types. *) | Pinductive of symbol * (arg_kind * pvar * pexp option) list * (symbol * (arg_kind * pvar option * pexp) list) list - | Pcons of pexp * symbol | Pcase of location * pexp * (ppat * pexp) list
and ppat = @@ -80,7 +79,6 @@ let rec pexp_location e = | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f | Pinductive ((l,_), _, _) -> l - | Pcons (e,_) -> pexp_location e | Pcase (l, _, _) -> l
let rec pexp_pat_location e = match e with @@ -171,11 +169,6 @@ let rec pexp_parse (s : sexp) : pexp = Pinductive (name, List.map pexp_p_formal_arg args, pcases) | Node (Symbol (start, "inductive_"), _) -> pexp_error start "Unrecognized inductive type"; Pmetavar (start, "_") - (* constructor *) - | Node (Symbol (start, "inductive-cons"), [e; Symbol tag]) - -> Pcons (pexp_parse e, tag) - | Node (Symbol (start, "cons_"), _) - -> pexp_error start "Unrecognized constructor call"; Pmetavar (start, "_") (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -346,9 +339,6 @@ and pexp_unparse (e : pexp) : sexp = -> Node (Symbol s, List.map pexp_u_ind_arg types)) branches) - | Pcons (t, ((l,_) as tag)) -> - Node (Symbol (l, "cons_"), - [pexp_unparse t; Symbol tag]) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"), pexp_unparse e @@ -431,5 +421,4 @@ let pexp_name e = | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" | Pinductive ((_,_), _, _) -> "Pinductive" - | Pcons (_,_) -> "Pcons" | Pcase (_, _, _) -> "Pcase"
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -88,7 +88,7 @@ let _ = test_eval_eqv_named "c = 3; e = 1; f = 2; d = 4;"
"let TrueProp = inductive_ TrueProp I; - I = inductive-cons TrueProp I; + I = datacons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3"
@@ -100,7 +100,7 @@ let _ = test_eval_eqv_named "let TrueProp : Type; I : TrueProp; TrueProp = inductive_ TrueProp I; - I = inductive-cons TrueProp I; + I = datacons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3"
@@ -137,10 +137,10 @@ let _ = test_eval_eqv_named idt : Type; idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); d = 10; - ctr0 = inductive-cons idt ctr0; e = 20; - ctr1 = inductive-cons idt ctr1; f = 30; - ctr2 = inductive-cons idt ctr2; g = 40; - ctr3 = inductive-cons idt ctr3; h = 50; + ctr0 = datacons idt ctr0; e = 20; + ctr1 = datacons idt ctr1; f = 30; + ctr2 = datacons idt ctr2; g = 40; + ctr3 = datacons idt ctr3; h = 50;
a = (ctr1 (ctr2 ctr0)); y = 2; b = (ctr2 (ctr2 ctr0)); z = 3; @@ -161,8 +161,8 @@ let nat_decl = " Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat);
- zero = inductive-cons Nat zero; - succ = inductive-cons Nat succ; + zero = datacons Nat zero; + succ = datacons Nat succ;
to-num : Nat -> Int; to-num = lambda (x : Nat) -> case x @@ -250,8 +250,8 @@ let _ = test_eval_eqv_named List' = let L : Type -> Type; L = inductive_ (L (a : Type)) (nil) (cons a (L a)) in L; - cons' = inductive-cons List' cons; - nil' = inductive-cons List' nil; + cons' = datacons List' cons; + nil' = datacons List' nil; my_list' = (cons' 1 nil');"
"length my_list; @@ -327,7 +327,7 @@ let _ = test_eval_eqv_named "Explicit field patterns" "Triplet = inductive_ Triplet (triplet (a ::: Int) (b :: Float) (c : String) (d :: Int)); - triplet = inductive-cons Triplet triplet; + triplet = datacons Triplet triplet; t = triplet (b := 5.0) (a := 3) (d := 7) (c := "hello");"
"case t | triplet (b := bf) cf => cf;
View it on GitLab: https://gitlab.com/monnier/typer/commit/afa9309b35337ee80df319e60f86a625b34d...