Stefan pushed to branch master at Stefan / Typer

Commits: f4630a76 by Stefan Monnier at 2016-12-15T09:25:53-05:00 Rename `inductive_` to `typecons` and make it a special-form

* src/lexp.ml (ptypecons): New var. (lexp_unparse): Don't use Pinductive.

* src/lparse.ml (infer): Move Pinductive case to sform_typecons. (sform_typecons): New function. (register_special_forms): Add it.

* src/pexp.ml (pexp): Remove Pinductive. (pexp_parse): Don't recognize `inductive_` any more. (pexp_unparse): Move Pinductive case to lexp_unparse.

* src/tweak.ml (Make.create): Use new name Array.make.

- - - - -

14 changed files:

- btl/builtins.typer - samples/autodiff.typer - samples/dependent.typer - samples/error.typer - samples/inductive.typer - samples/nat.typer - samples/pervasive.typer - src/elexp.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/tweak.ml - tests/eval_test.ml - tests/unify_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -36,11 +36,11 @@ % -----------------------------------------------------

% The trivial type which carries no information. -Unit = inductive_ Unit unit; +Unit = typecons Unit unit; unit = datacons Unit unit;

% The empty type, with no constructors: nothing can have this type. -Void = inductive_ Void; +Void = typecons Void;

% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l % Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l @@ -96,11 +96,11 @@ _-_ = Built-in "Int.-" (Int -> Int -> Int); _*_ = Built-in "Int.*" (Int -> Int -> Int); _/_ = Built-in "Int./" (Int -> Int -> Int);

-Bool = inductive_ (Boolean) (true) (false); +Bool = typecons (Boolean) (true) (false); true = datacons Bool true; false = datacons Bool false;

-Option = inductive_ (Option (a : Type)) (none) (some a); +Option = typecons (Option (a : Type)) (none) (some a); some = datacons Option some; none = datacons Option none;

@@ -113,7 +113,7 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); % -----------------------------------------------------

List : Type -> Type; -List = inductive_ (List (a : Type)) (nil) (cons a (List a)); +List = typecons (List (a : Type)) (nil) (cons a (List a));

nil = datacons List nil; cons = datacons List cons; @@ -156,7 +156,7 @@ node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); integer_ = Built-in "integer_" (Int -> Sexp); float_ = Built-in "float_" (Float -> Sexp);

-Macro = inductive_ (Macro) +Macro = typecons (Macro) (Macro_ (List Sexp -> Sexp)) (DMacro_ (List Sexp -> List Sexp));

@@ -231,5 +231,5 @@ Not : Type -> Type; Not prop = prop -> False;

% Like Bool, except that it additionally carries the meaning of its value. -Decidable = inductive_ (Decidable (prop : Type)) - (true (p ::: prop)) (false (p ::: Not prop)); +Decidable = typecons (Decidable (prop : Type)) + (true (p ::: prop)) (false (p ::: Not prop));

===================================== samples/autodiff.typer ===================================== --- a/samples/autodiff.typer +++ b/samples/autodiff.typer @@ -36,7 +36,7 @@ %* ---------------------------------------------------------------------------*)

Sym : Type; -Sym = inductive_ (dSym) +Sym = typecons (dSym) % leafs (constant Int) (placeholder String)

===================================== samples/dependent.typer ===================================== --- a/samples/dependent.typer +++ b/samples/dependent.typer @@ -1,5 +1,5 @@

-Reify = inductive_ (Reify (a : Type)) +Reify = typecons (Reify (a : Type)) (RInt (Eq (t := Type) Int a)) (RFloat (Eq (t := Type) Float a)) (RString (Eq (t := Type) String a));

===================================== samples/error.typer ===================================== --- a/samples/error.typer +++ b/samples/error.typer @@ -45,10 +45,10 @@ v = (a 2); m = lambda n -> n;

% [!] Error [Ln 27, cl 28] LPARSE Constructor "cons3" does not exist -% > inductive_: (inductive_ e (cons1) (cons2 Int)) +% > typecons: (typecons e (cons1) (cons2 Int)) % > Root:

-idt = inductive_ (idt) (cons1) (cons2 Int); +idt = typecons (idt) (cons1) (cons2 Int); cons1 = datacons idt cons1; cons2 = datacons idt cons2; cons3 = datacons idt cons3; @@ -94,7 +94,7 @@ fun2 n = case n % [!] Error [Ln 87, cl 1] LPARSE `fun4` defined but not declared! % [!] Error [Ln 86, cl 1] LPARSE Variable `fun4` declared but not defined!

-% idtb = inductive_ (idtb) (cons1b) (cons2b Int); +% idtb = typecons (idtb) (cons1b) (cons2b Int); % cons1b = datacons idtb cons1b; % cons2b = datacons idtb cons2b;

===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -70,7 +70,7 @@ type-impl = lambda (x : List Sexp) -> let type-name = get-name name in

% Create the inductive type definition - let inductive = node_ (symbol_ "inductive_") + let inductive = node_ (symbol_ "typecons") (cons name ctor) in

let decl = make-decl type-name inductive in @@ -118,6 +118,6 @@ type Point t

% transformed to: % Nat : Type; -% Nat = inductive_ (Nat) (succ Nat) (zero); +% Nat = typecons (Nat) (succ Nat) (zero); % zero = datacons Nat zero; % succ = datacons Nat succ;

===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -1,5 +1,5 @@ Nat : Type; -Nat = inductive_ (dNat) (zero) (succ Nat); +Nat = typecons (dNat) (zero) (succ Nat);

zero = datacons Nat zero; succ = datacons Nat succ;

===================================== samples/pervasive.typer ===================================== --- a/samples/pervasive.typer +++ b/samples/pervasive.typer @@ -1,13 +1,13 @@ %% (_=_) = (l : TypeLevel) ≡> (t : Type@ l) ≡> t -> t -> Type;

-Nat = inductive_ Type (zero : Nat) (succ : Nat -> Nat); +Nat = typecons Type (zero : Nat) (succ : Nat -> Nat);

-Macro = inductive_ Type (MacroExp : Nat -> Macro); +Macro = typecons Type (MacroExp : Nat -> Macro);

%% Use for `cast'. -Equiv = inductive_ (t -> t -> Type) (refl: Equiv a a); +Equiv = typecons (t -> t -> Type) (refl: Equiv a a);

-or = inductive_ (t -> t -> Type) +or = typecons (t -> t -> Type) (left: t1 -> or t1 t2) (right: t2 -> or t1 t2);

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -133,6 +133,6 @@ and elexp_string lxp = "case " ^ (elexp_string t) ^ (str_cases cases) ^ (maybe_str default)

| Inductive(_, (_, s)) -> - "inductive_ " ^ s + "typecons " ^ s

| Type -> "Type "

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -349,7 +349,7 @@ let lexp_name e = | Call _ -> "Call" | Cons _ -> "datacons" | Case _ -> "case" - | Inductive _ -> "inductive_" + | Inductive _ -> "typecons" | Susp _ -> "Susp" | Builtin (_, _, None) -> "Builtin" | Builtin _ -> "AttributeTable" @@ -358,6 +358,7 @@ let lexp_name e = | SortLevel _ -> "SortLevel"

let pdatacons = Pbuiltin (U.dummy_location, "datacons") +let ptypecons = Pbuiltin (U.dummy_location, "typecons")

(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = @@ -387,7 +388,7 @@ let rec lexp_unparse lxp = let sargs = List.map (fun elem -> pexp_unparse elem) pargs in Pcall(lexp_unparse lxp, sargs)

- | Inductive(loc, label, lfargs, ctor) -> + | Inductive(loc, label, lfargs, ctors) -> (* (arg_kind * vdef * ltype) list *) (* (arg_kind * pvar * pexp option) list *) let pfargs = List.map (fun (kind, vdef, ltp) -> @@ -395,14 +396,19 @@ let rec lexp_unparse lxp =

(* ((arg_kind * vdef option * ltype) list) SMap.t *) (* (symbol * (arg_kind * pvar option * pexp) list) list *) - let ctor = List.map (fun (str, largs) -> + let ctors = List.map (fun (str, largs) -> let pargs = List.map (fun (kind, var, ltp) -> match var with | Some (loc, name) -> (kind, Some (loc, name), lexp_unparse ltp) | None -> (kind, None, lexp_unparse ltp)) largs in ((loc, str), pargs) - ) (SMap.bindings ctor) - in Pinductive(label, pfargs, ctor) + ) (SMap.bindings ctors) in + Pcall (ptypecons, + Node (Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map (fun ((l,name) as s, types) + -> Node (Symbol s, + List.map pexp_u_ind_arg types)) + ctors)

| Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in @@ -638,7 +644,7 @@ and _lexp_to_str ctx exp = add_parens outer_parens str)

| Inductive (_, (_, name), [], ctors) -> - (keyword "inductive_") ^ " (" ^ name ^") " ^ + (keyword "typecons") ^ " (" ^ name ^") " ^ (lexp_str_ctor ctx ctors)

| Inductive (_, (_, name), args, ctors) @@ -649,7 +655,7 @@ and _lexp_to_str ctx exp = ^ (lexp_to_str ltype) ^ ")") "" args in

- (keyword "inductive_") ^ " (" ^ name ^ args_str ^") " + (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ (lexp_str_ctor ctx ctors)

| Case (_, target, _ret, map, dflt) ->(

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -306,30 +306,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = let v = mkArrow(kind, ovar, ltp, tloc, lxp) in v, type0

- | Pinductive (label, formal_args, ctors) - -> let nctx = ref ctx in - (* (arg_kind * pvar * pexp option) list *) - let formal = List.map (fun (kind, var, opxp) - -> let ltp = match opxp with - | Some pxp -> let (l,_) = infer pxp !nctx in l - | None -> let (l,_) = var in newMetatype l in - - nctx := env_extend !nctx var Variable ltp; - (kind, var, ltp)) - formal_args in - - let nctx = !nctx in - let ltp = List.fold_left (fun tp (kind, v, ltp) - -> (mkArrow (kind, Some v, ltp, tloc, tp))) - (* FIXME: See OL.check for how to - * compute the real target sort - * (not always type0). *) - type0 (List.rev formal) in - - let map_ctor = lexp_parse_inductive ctors nctx in - let v = mkInductive(tloc, label, formal, map_ctor) in - v, ltp - (* This case can be inferred. *) | Plambda (kind, var, Some ptype, body) -> let ltp = infer_type ptype ctx (Some var) in @@ -1156,6 +1132,50 @@ let sform_datacons ctx loc sargs ot = | _ -> sexp_error loc "##constr requires two arguments"; sform_dummy_ret loc

+let sform_typecons ctx loc sargs ot = + match sargs with + | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type loc, Lazy) + | formals :: constrs + -> let (label, formals) = match formals with + | Node (label, formals) -> (label, formals) + | _ -> (formals, []) in + let label = match label with + | Symbol label -> label + | _ -> let loc = sexp_location label in + sexp_error loc "Unrecognized inductive type name"; + (loc, "<error>") in + + let rec parse_formals sformals rformals ctx = match sformals with + | [] -> (List.rev rformals, ctx) + | sformal :: sformals + -> let (kind, var, opxp) = pexp_p_formal_arg sformal in + let ltp = match opxp with + | Some pxp -> let (l,_) = infer pxp ctx in l + | None -> let (l,_) = var in newMetatype l in + + parse_formals sformals ((kind, var, ltp) :: rformals) + (env_extend ctx var Variable ltp) in + + let (formals, nctx) = parse_formals formals [] ctx in + + let ctors + = List.fold_right + (fun case pcases + -> match case with + (* read Constructor name + args => Type ((Symbol * args) list) *) + | Node (Symbol s, cases) + -> (s, List.map pexp_p_ind_arg cases)::pcases + (* This is a constructor with no args *) + | Symbol s -> (s, [])::pcases + + | _ -> sexp_error (sexp_location case) + "Unrecognized constructor declaration"; + pcases) + constrs [] in + + let map_ctor = lexp_parse_inductive ctors nctx in + (mkInductive (loc, label, formals, map_ctor), Lazy) + (* 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 @@ -1195,6 +1215,7 @@ let register_special_forms () = [ ("Built-in", sform_built_in); ("datacons", sform_datacons); + ("typecons", sform_typecons); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute);

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -49,8 +49,6 @@ type pexp = | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two * otherwise isomorphic types. *) - | Pinductive of symbol * (arg_kind * pvar * pexp option) list - * (symbol * (arg_kind * pvar option * pexp) list) list | Pcase of location * pexp * (ppat * pexp) list

and ppat = @@ -78,7 +76,6 @@ let rec pexp_location e = | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f - | Pinductive ((l,_), _, _) -> l | Pcase (l, _, _) -> l

let rec pexp_pat_location e = match e with @@ -146,29 +143,6 @@ let rec pexp_parse (s : sexp) : pexp = (pexp_parse body) | Node (Symbol (start, "lambda_"), _) -> pexp_error start "Unrecognized lambda expression"; Pmetavar (start, "_") - (* inductive type *) - | Node (Symbol (start, "inductive_"), t :: cases) - -> let (name, args) = match t with - | Node (Symbol s, args) -> (s, args) (* This a constructor *) - | Symbol s -> (s, []) (* This is a Label *) - | _ -> pexp_error start "Unrecognized inductive type name"; - ((dummy_location, ""), []) in - let pcases = - List.fold_right - (fun case pcases - -> match case with - (* read Constructor name + args => Type ((Symbol * args) list) *) - | Node (Symbol s, cases) - -> (s, List.map pexp_p_ind_arg cases)::pcases - (* This is a constructor with no args *) - | Symbol s -> (s, [])::pcases - - | _ -> pexp_error (sexp_location case) - "Unrecognized constructor declaration"; pcases) - cases [] in - Pinductive (name, List.map pexp_p_formal_arg args, pcases) - | Node (Symbol (start, "inductive_"), _) - -> pexp_error start "Unrecognized inductive type"; Pmetavar (start, "_") (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -331,14 +305,6 @@ and pexp_unparse (e : pexp) : sexp = [Symbol v; pexp_unparse t])); pexp_unparse body]) | Pcall (f, args) -> Node (pexp_unparse f, args) - (* Pinductive *) - | Pinductive (s, t, branches) -> - Node (Symbol (dummy_location, "inductive_"), - sexp_u_list (List.map pexp_u_formal_arg t) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - branches) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"), pexp_unparse e @@ -420,5 +386,4 @@ let pexp_name e = | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" - | Pinductive ((_,_), _, _) -> "Pinductive" | Pcase (_, _, _) -> "Pcase"

===================================== src/tweak.ml ===================================== --- a/src/tweak.ml +++ b/src/tweak.ml @@ -53,8 +53,8 @@ module Make (H : Hashtbl.HashedType) : (S with type data = H.t) = struct let sz = if sz < 7 then 7 else sz in let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in { - table = Array.create sz emptybucket; - hashes = Array.create sz [| |]; + table = Array.make sz emptybucket; + hashes = Array.make sz [| |]; limit = limit; oversize = 0; rover = 0;

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -87,7 +87,7 @@ let _ = test_eval_eqv_named

"c = 3; e = 1; f = 2; d = 4;"

- "let TrueProp = inductive_ TrueProp I; + "let TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3" @@ -99,7 +99,7 @@ let _ = test_eval_eqv_named

"let TrueProp : Type; I : TrueProp; - TrueProp = inductive_ TrueProp I; + TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3" @@ -135,7 +135,7 @@ let _ = test_eval_eqv_named

"i = 90; idt : Type; - idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); + idt = typecons (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); d = 10; ctr0 = datacons idt ctr0; e = 20; ctr1 = datacons idt ctr1; f = 30; @@ -159,7 +159,7 @@ let _ = test_eval_eqv_named (* Those wil be used multiple times *) let nat_decl = " Nat : Type; - Nat = inductive_ (dNat) (zero) (succ Nat); + Nat = typecons (dNat) (zero) (succ Nat);

zero = datacons Nat zero; succ = datacons Nat succ; @@ -248,7 +248,7 @@ let _ = test_eval_eqv_named (cons 3 (cons 4 nil))); List' = let L : Type -> Type; - L = inductive_ (L (a : Type)) (nil) (cons a (L a)) + L = typecons (L (a : Type)) (nil) (cons a (L a)) in L; cons' = datacons List' cons; nil' = datacons List' nil; @@ -325,7 +325,7 @@ let _ = test_eval_eqv_named "Metavars"

let _ = test_eval_eqv_named "Explicit field patterns" - "Triplet = inductive_ Triplet + "Triplet = typecons Triplet (triplet (a ::: Int) (b :: Float) (c : String) (d :: Int)); triplet = datacons Triplet triplet; t = triplet (b := 5.0) (a := 3) (d := 7) (c := "hello");"

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -78,7 +78,7 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = ) str_lst

(* Inputs for the test *) -let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" +let str_induct = "Nat : Type; Nat = typecons (dNat) (zero) (succ Nat)" let str_int_3 = "i = 3" let str_int_4 = "i = 4" let str_case = "i = case true

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