Simon Génier pushed to branch there-can-be-only-one-inductive at Stefan / Typer
Commits: 71f83760 by Simon Génier at 2020-12-09T18:26:34-05:00 Remove arguments to inductive types.
There used to be two ways to express indexed types: one could either add parameters directly on the type or put the type behind a lambda. These two are semantically equivalent, so we unify them into the latter in this patch.
- - - - -
10 changed files:
- btl/builtins.typer - btl/pervasive.typer - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/unification.ml - + tests/opslexp_test.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -191,14 +191,14 @@ Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp; %% List %% -----------------------------------------------------
-%% FIXME: "List : ?" should be sufficient but triggers -List : Type_ ?ℓ -> Type_ ?ℓ; -%% List a = typecons List (nil) (cons a (List a)); -%% nil = lambda a ≡> datacons (List a) nil; -%% cons = lambda a ≡> datacons (List a) cons; -List = typecons (List (ℓ ::: TypeLevel) (a : Type_ ℓ)) (nil) (cons a (List a)); -nil = datacons List nil; -cons = datacons List cons; +List : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; +List = lambda ℓ ≡> lambda α -> typecons List (nil) (cons α (List (ℓ := ℓ) α)); + +nil : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> List (ℓ := ℓ) α; +nil = lambda ℓ ≡> lambda α ≡> datacons (List (ℓ := ℓ) α) nil; + +cons : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> α -> List (ℓ := ℓ) α -> List (ℓ := ℓ) α; +cons = lambda ℓ ≡> lambda α ≡> datacons (List (ℓ := ℓ) α) cons;
%%%% Macro-related definitions
===================================== btl/pervasive.typer ===================================== @@ -32,659 +32,664 @@
%%%% `Option` type
-Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a); -some = datacons Option some; -none = datacons Option none; +Option : Type_ ?ℓ -> Type_ ?ℓ; +Option = lambda α -> typecons Option (none) (some α);
-%%%% List functions - -List_length : List ?a -> Int; % Recursive defs aren't generalized :-( -List_length xs = case xs - | nil => 0 - | cons hd tl => - (1 + (List_length tl)); - -%% ML's typical `head` function is not total, so can't be defined -%% as-is in Typer. There are several workarounds: -%% - Provide a default value : `a -> List a -> a`; -%% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; -%% - Return an Option/Error -List_head1 xs = case xs - | nil => none - | cons hd tl => some hd; - -List_head x = lambda xs -> case xs - | cons x _ => x - | nil => x; - -List_tail xs = case xs - | nil => nil - | cons hd tl => tl; - -List_map : (?a -> ?b) -> List ?a -> List ?b; -List_map f = lambda xs -> case xs - | nil => nil - | cons x xs => cons (f x) (List_map f xs); - -List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a; -List_foldr f = lambda xs -> lambda i -> case xs - | nil => i - | cons x xs => f x (List_foldr f xs i); - -List_find : (?a -> Bool) -> List ?a -> Option ?a; -List_find f = lambda xs -> case xs - | nil => none - | cons x xs => case f x | true => some x | false => List_find f xs; - -List_nth : Int -> List ?a -> ?a -> ?a; -List_nth = lambda n -> lambda xs -> lambda d -> case xs - | nil => d - | cons x xs - => case Int_<= n 0 - | true => x - | false => List_nth (n - 1) xs d; - -%%%% A more flexible `lambda` - -%% An `Sexp` which we use to represents an *error*. -Sexp_error = Sexp_symbol "<error>"; - -%% Sexp_to_list : Sexp -> List Sexp -> List Sexp; -Sexp_to_list s = lambda exceptions -> - let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"! - Sexp_dispatch - s - (node := lambda head -> lambda tail - -> case List_find (Sexp_eq head) exceptions - | some _ => singleton () - | none => cons head tail) - (symbol := lambda s - -> case String_eq "" s - | true => nil - | false => singleton ()) - singleton singleton singleton singleton; - -multiarg_lambda = - %% This macro lets `lambda_->_` (and siblings) accept multiple arguments. - %% TODO: We could additionally turn - %% lambda (x :: t) y -> e - %% into - %% lambda (x : t) => lambda y -> e` - %% thus providing an alternate syntax for lambdas which don't use - %% => and ≡>. - let exceptions = List_map Sexp_symbol - (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in - lambda name -> - let sym = (Sexp_symbol name); - mklambda = lambda arg -> lambda body -> - Sexp_node sym (cons arg (cons body nil)) in - lambda (margs : List Sexp) - -> IO_return - case margs - | nil => Sexp_error - | cons fargs margstail - => case margstail - | nil => Sexp_error - | cons body bodytail - => case bodytail - | cons _ _ => Sexp_error - | nil => List_foldr mklambda - (Sexp_to_list fargs exceptions) - body; - -lambda_->_ = macro (multiarg_lambda "##lambda_->_"); -lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); -lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_"); - -%%%% More list functions - -List_reverse : List ?a -> List ?a -> List ?a; -List_reverse l t = case l - | nil => t - | cons hd tl => List_reverse tl (cons hd t); - -List_concat l t = List_reverse (List_reverse l nil) t; - -List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a; -List_foldl f i xs = case xs - | nil => i - | cons x xs => List_foldl f (f i x) xs; - -List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; -List_mapi f xs = let - helper : (a -> Int -> b) -> Int -> List a -> List b; - helper f i xs = case xs - | nil => nil - | cons x xs => cons (f x i) (helper f (i + 1) xs); -in helper f 0 xs; - -List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c; -List_map2 f xs ys = case xs - | nil => nil - | cons x xs => case ys - | nil => nil % error - | cons y ys => cons (f x y) (List_map2 f xs ys); - -%% Fold 2 List as long as both List are non-empty -List_fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> List ?b -> List ?c -> ?a; -List_fold2 f o xs ys = case xs - | cons x xs => ( case ys - | cons y ys => List_fold2 f (f o x y) xs ys - | nil => o ) % may be an error - | nil => o; % may or may not be an error - -%% Is argument List empty? -List_empty : List ?a -> Bool; -List_empty xs = Int_eq (List_length xs) 0; - -%%% Good 'ol combinators - -I x = x; - -%% Use explicit erasable annotations since with an annotation like -%% K : ?a -> ?b -> ?a; -%% Typer generalizes to -%% K : (a : Type) ≡> (b : Type) ≡> a -> b -> a; -%% Which is less general. -%% FIXME: Change the generalizer to insert the `(b : Type) ≡>` -%% more lazily (i.e. after the `a` argument). -K : ?a -> (b : Type) ≡> b -> ?a; -K x y = x; - -%%%% Quasi-Quote macro - -%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) -%% -%% f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil)) -%% -%% => x - -%% Takes an Sexp `x` as argument and return an Sexp which represents code -%% which will construct an Sexp equivalent to `x` at run-time. -%% This is basically *cross stage persistence* for Sexp. -quote1 : Sexp -> Sexp; -quote1 x = let - qlist : List Sexp -> Sexp; - qlist xs = case xs - | nil => Sexp_symbol "nil" - | cons x xs => Sexp_node (Sexp_symbol "cons") - (cons (quote1 x) - (cons (qlist xs) nil)); - make_app str sexp = - Sexp_node (Sexp_symbol str) (cons sexp nil); - - node op y = case (Sexp_eq op (Sexp_symbol "uquote")) - | true => List_head Sexp_error y - | false => Sexp_node (Sexp_symbol "##Sexp.node") - (cons (quote1 op) - (cons (qlist y) nil)); - symbol s = make_app "##Sexp.symbol" (Sexp_string s); - string s = make_app "##Sexp.string" (Sexp_string s); - integer i = make_app "##Sexp.integer" - (make_app "##Int->Integer" (Sexp_integer i)); - float f = make_app "##Sexp.float" (Sexp_float f); - block sxp = - %% FIXME ##Sexp.block takes a string (and prelexes - %% it) but we have a sexp, what should we do? - Sexp_symbol "<error FIXME block quoting>"; - in Sexp_dispatch x node symbol string integer float block; - -%% quote definition -quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); - -%%%% The `type` declaration macro - -%% Build a declaration: -%% var-name = value-expr; -make-decl : Sexp -> Sexp -> Sexp; -make-decl var-name value-expr = - Sexp_node (Sexp_symbol "_=_") - (cons var-name - (cons value-expr nil)); - -chain-decl : Sexp -> Sexp -> Sexp; -chain-decl a b = - Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil)); - -chain-decl3 : Sexp -> Sexp -> Sexp -> Sexp; -chain-decl3 a b c = - Sexp_node (Sexp_symbol "_;_") (cons a (cons b (cons c nil))); - -%% Build datacons: -%% ctor-name = datacons type-name ctor-name; -make-cons : Sexp -> Sexp -> Sexp; -make-cons ctor-name type-name = - make-decl ctor-name - (Sexp_node (Sexp_symbol "datacons") - (cons type-name - (cons ctor-name nil))); - -%% Build type annotation: -%% var-name : type-expr; -make-ann : Sexp -> Sexp -> Sexp; -make-ann var-name type-expr = - Sexp_node (Sexp_symbol "_:_") - (cons var-name - (cons type-expr nil)); - -type-impl = lambda (x : List Sexp) -> - %% `x` follow the mask -> - %% (_|_ Nat zero (succ Nat)) - %% Type name --^ ^------^ constructors - - %% Return a list contained inside a node sexp. - let knil = K nil; - kerr = K Sexp_error; - - get-list : Sexp -> List Sexp; - get-list node = Sexp_dispatch node - (lambda op lst -> lst) % Nodes - knil % Symbol - knil % String - knil % Integer - knil % Float - knil; % List of Sexp - - %% Get a name (symbol) from a sexp - %% - (name t) -> name - %% - name -> name - get-name : Sexp -> Sexp; - get-name sxp = - Sexp_dispatch sxp - (lambda op _ -> get-name op) % Nodes - (lambda _ -> sxp) % Symbol - kerr % String - kerr % Integer - kerr % Float - kerr; % List of Sexp - - get-args : Sexp -> List Sexp; - get-args sxp = - Sexp_dispatch sxp - (lambda _ args -> args) % Nodes - (lambda _ -> (nil : List Sexp)) % Symbol - (lambda _ -> (nil : List Sexp)) % String - (lambda _ -> (nil : List Sexp)) % Integer - (lambda _ -> (nil : List Sexp)) % Float - (lambda _ -> (nil : List Sexp)); % List of Sexp - - get-type : Sexp -> Sexp; - get-type sxp = - Sexp_dispatch sxp - (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) - | true => List_nth 1 ss Sexp_error - | false => sxp) - (lambda _ -> sxp) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error); - - get-head = List_head Sexp_error; - - %% Get expression. - expr = get-head x; - - %% Expression is Sexp_node (Sexp_symbol "|") (list) - %% we only care about the list bit - lst = get-list expr; - - %% head is (Sexp_node type-name (arg list)) - name = get-head lst; - ctor = List_tail lst; - - type-name = get-name name; - - %% Create the inductive type definition. - inductive = Sexp_node (Sexp_symbol "typecons") - (cons name ctor); - - %% Declare the inductive type as a function - %% Useful for recursive type - type-decl = quote ((uquote (get-name name)) : (uquote ( - (List_foldl (lambda args arg -> - Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil))) - %% FIXME: Don't hardcode TypeLevel.z! - (Sexp_symbol "Type") (List_reverse (get-args name) nil)) - ))); - - decl = make-decl type-name inductive; - - %% Add constructors. - ctors = let for-each : List Sexp -> Sexp -> Sexp; - for-each ctr acc = case ctr - | cons hd tl => - let acc2 = chain-decl (make-cons (get-name hd) - type-name) - acc - in for-each tl acc2 - | nil => acc - in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil) - - %% return decls - in IO_return (chain-decl3 type-decl % type as a function declaration - decl % inductive type declaration - ctors); % constructor declarations - -type_ = macro type-impl; - -%%%% An inductive type to wrap Sexp - -type Sexp_wrapper - | node Sexp (List Sexp) - | symbol String - | string String - | integer Integer - | float Float - | block Sexp; - -Sexp_wrap s = Sexp_dispatch s node symbol string integer float block; - -%%%% Tuples - -%% Sample tuple: a module holding Bool and its constructors. -BoolMod = (##datacons - %% We need the `?` metavars to be lexically outside of the - %% `typecons` expression, otherwise they end up generalized, so - %% we end up with a type constructor like - %% - %% typecons _ (cons (τ₁ : Type) (t : τ₁) - %% (τ₂ : Type) (true : τ₂) - %% (τ₃ : Type) (false : τ₃)) - %% - %% And it's actually even worse because it tries to generalize - %% over the level of those `Type`s, so we end up with an invalid - %% inductive type. - ((lambda t1 t2 t3 - -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) - ? ? ?) - cons) - (_ := Bool) (_ := true) (_ := false); - -Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); -pair = datacons Pair pair; - -__.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); - -%% Triplet (tuple with 3 values) -type Triplet (a : Type) (b : Type) (c : Type) - | triplet (x : a) (y : b) (z : c); - -%%%% List with tuple - -%% Merge two List to a List of Pair -%% Both List must be of same length -List_merge : List ?a -> List ?b -> List (Pair ?a ?b); -List_merge xs ys = case xs - | cons x xs => ( case ys - | cons y ys => cons (pair x y) (List_merge xs ys) - | nil => nil ) % error - | nil => nil; - -%% `Unmerge` a List of Pair -%% The two functions name said it all -List_map-fst xs = let - mf p = case p | pair x _ => x; -in List_map mf xs; - -List_map-snd xs = let - mf p = case p | pair _ y => y; -in List_map mf xs; - -%%%% Logic - -%% `False` should be one of the many empty types. -%% Other popular choices are False = ∀a.a and True = ∃a.a. -False = Void; -True = Unit; - -Not prop = prop -> False; - -%% Like Bool, except that it additionally carries the meaning of its value. -%% We don't use the `type` macro here because it would make these `true` -%% and `false` constructors override `Bool`'s, and we currently don't -%% want that. -Decidable = typecons (Decidable (prop : Type_ ?ℓ)) - (true (p ::: prop)) (false (p ::: Not prop)); - -%% Testing generalization in inductive type constructors. -LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient! -type LList (a : Type) (n : Int) - | vnil (p ::: Eq n 0) - | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound! - -%%%% If - -define-operator "if" () 2; -define-operator "then" 2 1; -define-operator "else" 1 66; - -if_then_else_ - = macro (lambda args -> - let e1 = List_nth 0 args Sexp_error; - e2 = List_nth 1 args Sexp_error; - e3 = List_nth 2 args Sexp_error; - in IO_return (quote (case uquote e1 - | true => uquote e2 - | false => uquote e3))); - -%%%% More boolean - -%% FIXME: Type annotations should not be needed below. -not : Bool -> Bool; -%% FIXME: We use braces here to delay parsing, otherwise the if/then/else -%% part of the grammar declared above is not yet taken into account. -not x = { if x then false else true }; - -or : Bool -> Bool -> Bool; -or x y = { if x then x else y }; - -and : Bool -> Bool -> Bool; -and x y = { if x then y else x }; - -xor : Bool -> Bool -> Bool; -xor x y = { if x then (not y) else y }; - -%% FIXME: Can't use ?a because that is generalized to be universe-polymorphic, -%% which we don't support in `load` yet. -fold : Bool -> (a : Type) ≡> a -> a -> a; -fold x t e = { if x then t else e}; - -%%%% Test -test1 : ?; -test2 : Option Int; -test3 : Option Int; -test1 = test2; -%% In earlier versions of Typer, we could use `?` in declarations -%% to mean "fill this for me by unifying with later type information", -%% but this is incompatible with the use of generalization to introduce -%% implicit arguments. -%% test4 : Option ?; -test2 = none; -test4 : Option Int; -test4 = test1 : Option ?; -test3 = test4; - -%%%% Rewrite of some builtins to use `Option` - -%% -%% If `Elab_nth-arg'` returns "_" it means: -%% A- The constructor isn't defined, or -%% B- The constructor has no n'th argument -%% -%% So in those case this function returns `none` -%% -Elab_nth-arg a b c = let - r = Elab_nth-arg' a b c; -in case (String_eq r "_") - | true => (none) - | false => (some r); - -%% -%% If `Elab_arg-pos'` returns (-1) it means: -%% A- The constructor isn't defined, or -%% B- The constructor has no argument named like this -%% -%% So in those case this function returns `none` -%% -Elab_arg-pos a b c = let - r = Elab_arg-pos' a b c; -in case (Int_eq r (-1)) - | true => (none) - | false => (some r); - -%%%% -%%%% Common library -%%%% - -%% -%% `<-` operator used in macro `do` and for tuple assignment -%% +none : (α : Type_ ?ℓ) ≡> Option (ℓ := ?ℓ) α; +none = lambda ℓ ≡> lambda α ≡> datacons (Option α) none;
-define-operator "<-" 80 96; +some : (α : Type_ ?ℓ) ≡> α -> Option (ℓ := ?ℓ) α; +some = lambda ℓ ≡> lambda α ≡> datacons (Option α) some;
-%% -%% `List` is the type and `list` is the module -%% -list = load "btl/list.typer"; - -%% -%% Macro `do` for easier series of IO operation -%% -%% e.g.: -%% do { IO_return true; }; -%% -do = let lib = load "btl/do.typer" in lib.do; - -%% -%% Module containing various macros for tuple -%% Used by `case_` -%% -tuple-lib = load "btl/tuple.typer"; - -%% -%% Get the nth element of a tuple -%% -%% e.g.: -%% tuple-nth tup 0; -%% -tuple-nth = tuple-lib.tuple-nth; - -%% -%% Affectation of tuple -%% -%% e.g.: -%% (x,y,z) <- tup; -%% -_<-_ = tuple-lib.assign-tuple; - -%% -%% Instantiate a tuple from expressions -%% -%% e.g.: -%% tup = (x,y,z); -%% -_,_ = tuple-lib.make-tuple; - -Tuple = tuple-lib.tuple-type; - -%% -%% Macro `case` for a some more complex pattern matching -%% -case_ = let lib = load "btl/case.typer" in lib.case-macro; - -%% -%% plain-let -%% Not recursive and not sequential -%% -%% e.g.: -%% plain-let x = 1; in x; -%% - -define-operator "plain-let" () 3; - -%% -%% Already defined: -%% define-operator "in" 3 67; -%% - -plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; - -%% -%% `case` at function level -%% -%% e.g.: -%% my-fun (x : Bool) -%% | true => false -%% | false => true; -%% -_|_ = let lib = load "btl/polyfun.typer" in lib._|_; - -%% -%% case_as_return_, case_return_ -%% A `case` for dependent elimination -%% - -define-operator "as" 42 42; -define-operator "return" 42 42; -depelim = load "btl/depelim.typer"; -case_as_return_ = depelim.case_as_return_; -case_return_ = depelim.case_return_; - -%%%% Unit tests function for doing file - -%% It's hard to do a primitive which execute test file -%% because of circular dependency... +%%%% List functions
-%% -%% A macro using `load` for unit testing purpose -%% -%% Takes a file name (String) as argument -%% Returns variable named `exec-test` from the loaded file -%% -%% `exec-test` should be a command doing unit tests -%% for other purpose than that just use `load` directly! -%% -Test_file = macro (lambda args -> let - - %% return an empty command on error - ret = Sexp_node - (Sexp_symbol "IO_return") - (cons (Sexp_symbol "unit") nil); - -%% Expecting a String and nothing else -in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) - (lambda _ _ -> ret) - (lambda _ -> ret) - %% `load` is a special form and takes a Sexp rather than a real `String` - (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test)) - (lambda _ -> ret) - (lambda _ -> ret) - (lambda _ -> ret)) -); - -%%% pervasive.typer ends here. +% Recursive defs aren't generalized :-( +List_length : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> List (ℓ := ℓ) α -> Int; +List_length = lambda ℓ ≡> lambda α ≡> lambda xs -> case xs + | nil => 0 + | cons hd tl => 1 + List_length (ℓ := ℓ) (α := α) tl; + +% %% ML's typical `head` function is not total, so can't be defined +% %% as-is in Typer. There are several workarounds: +% %% - Provide a default value : `a -> List a -> a`; +% %% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; +% %% - Return an Option/Error +% List_head1 xs = case xs +% | nil => none +% | cons hd tl => some hd; + +% List_head x = lambda xs -> case xs +% | cons x _ => x +% | nil => x; + +% List_tail xs = case xs +% | nil => nil +% | cons hd tl => tl; + +% List_map : (?a -> ?b) -> List ?a -> List ?b; +% List_map f = lambda xs -> case xs +% | nil => nil +% | cons x xs => cons (f x) (List_map f xs); + +% List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a; +% List_foldr f = lambda xs -> lambda i -> case xs +% | nil => i +% | cons x xs => f x (List_foldr f xs i); + +% List_find : (?a -> Bool) -> List ?a -> Option ?a; +% List_find f = lambda xs -> case xs +% | nil => none +% | cons x xs => case f x | true => some x | false => List_find f xs; + +% List_nth : Int -> List ?a -> ?a -> ?a; +% List_nth = lambda n -> lambda xs -> lambda d -> case xs +% | nil => d +% | cons x xs +% => case Int_<= n 0 +% | true => x +% | false => List_nth (n - 1) xs d; + +% %%%% A more flexible `lambda` + +% %% An `Sexp` which we use to represents an *error*. +% Sexp_error = Sexp_symbol "<error>"; + +% %% Sexp_to_list : Sexp -> List Sexp -> List Sexp; +% Sexp_to_list s = lambda exceptions -> +% let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"! +% Sexp_dispatch +% s +% (node := lambda head -> lambda tail +% -> case List_find (Sexp_eq head) exceptions +% | some _ => singleton () +% | none => cons head tail) +% (symbol := lambda s +% -> case String_eq "" s +% | true => nil +% | false => singleton ()) +% singleton singleton singleton singleton; + +% multiarg_lambda = +% %% This macro lets `lambda_->_` (and siblings) accept multiple arguments. +% %% TODO: We could additionally turn +% %% lambda (x :: t) y -> e +% %% into +% %% lambda (x : t) => lambda y -> e` +% %% thus providing an alternate syntax for lambdas which don't use +% %% => and ≡>. +% let exceptions = List_map Sexp_symbol +% (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in +% lambda name -> +% let sym = (Sexp_symbol name); +% mklambda = lambda arg -> lambda body -> +% Sexp_node sym (cons arg (cons body nil)) in +% lambda (margs : List Sexp) +% -> IO_return +% case margs +% | nil => Sexp_error +% | cons fargs margstail +% => case margstail +% | nil => Sexp_error +% | cons body bodytail +% => case bodytail +% | cons _ _ => Sexp_error +% | nil => List_foldr mklambda +% (Sexp_to_list fargs exceptions) +% body; + +% lambda_->_ = macro (multiarg_lambda "##lambda_->_"); +% lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); +% lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_"); + +% %%%% More list functions + +% List_reverse : List ?a -> List ?a -> List ?a; +% List_reverse l t = case l +% | nil => t +% | cons hd tl => List_reverse tl (cons hd t); + +% List_concat l t = List_reverse (List_reverse l nil) t; + +% List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a; +% List_foldl f i xs = case xs +% | nil => i +% | cons x xs => List_foldl f (f i x) xs; + +% List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; +% List_mapi f xs = let +% helper : (a -> Int -> b) -> Int -> List a -> List b; +% helper f i xs = case xs +% | nil => nil +% | cons x xs => cons (f x i) (helper f (i + 1) xs); +% in helper f 0 xs; + +% List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c; +% List_map2 f xs ys = case xs +% | nil => nil +% | cons x xs => case ys +% | nil => nil % error +% | cons y ys => cons (f x y) (List_map2 f xs ys); + +% %% Fold 2 List as long as both List are non-empty +% List_fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> List ?b -> List ?c -> ?a; +% List_fold2 f o xs ys = case xs +% | cons x xs => ( case ys +% | cons y ys => List_fold2 f (f o x y) xs ys +% | nil => o ) % may be an error +% | nil => o; % may or may not be an error + +% %% Is argument List empty? +% List_empty : List ?a -> Bool; +% List_empty xs = Int_eq (List_length xs) 0; + +% %%% Good 'ol combinators + +% I x = x; + +% %% Use explicit erasable annotations since with an annotation like +% %% K : ?a -> ?b -> ?a; +% %% Typer generalizes to +% %% K : (a : Type) ≡> (b : Type) ≡> a -> b -> a; +% %% Which is less general. +% %% FIXME: Change the generalizer to insert the `(b : Type) ≡>` +% %% more lazily (i.e. after the `a` argument). +% K : ?a -> (b : Type) ≡> b -> ?a; +% K x y = x; + +% %%%% Quasi-Quote macro + +% %% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) +% %% +% %% f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil)) +% %% +% %% => x + +% %% Takes an Sexp `x` as argument and return an Sexp which represents code +% %% which will construct an Sexp equivalent to `x` at run-time. +% %% This is basically *cross stage persistence* for Sexp. +% quote1 : Sexp -> Sexp; +% quote1 x = let +% qlist : List Sexp -> Sexp; +% qlist xs = case xs +% | nil => Sexp_symbol "nil" +% | cons x xs => Sexp_node (Sexp_symbol "cons") +% (cons (quote1 x) +% (cons (qlist xs) nil)); +% make_app str sexp = +% Sexp_node (Sexp_symbol str) (cons sexp nil); + +% node op y = case (Sexp_eq op (Sexp_symbol "uquote")) +% | true => List_head Sexp_error y +% | false => Sexp_node (Sexp_symbol "##Sexp.node") +% (cons (quote1 op) +% (cons (qlist y) nil)); +% symbol s = make_app "##Sexp.symbol" (Sexp_string s); +% string s = make_app "##Sexp.string" (Sexp_string s); +% integer i = make_app "##Sexp.integer" +% (make_app "##Int->Integer" (Sexp_integer i)); +% float f = make_app "##Sexp.float" (Sexp_float f); +% block sxp = +% %% FIXME ##Sexp.block takes a string (and prelexes +% %% it) but we have a sexp, what should we do? +% Sexp_symbol "<error FIXME block quoting>"; +% in Sexp_dispatch x node symbol string integer float block; + +% %% quote definition +% quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); + +% %%%% The `type` declaration macro + +% %% Build a declaration: +% %% var-name = value-expr; +% make-decl : Sexp -> Sexp -> Sexp; +% make-decl var-name value-expr = +% Sexp_node (Sexp_symbol "_=_") +% (cons var-name +% (cons value-expr nil)); + +% chain-decl : Sexp -> Sexp -> Sexp; +% chain-decl a b = +% Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil)); + +% chain-decl3 : Sexp -> Sexp -> Sexp -> Sexp; +% chain-decl3 a b c = +% Sexp_node (Sexp_symbol "_;_") (cons a (cons b (cons c nil))); + +% %% Build datacons: +% %% ctor-name = datacons type-name ctor-name; +% make-cons : Sexp -> Sexp -> Sexp; +% make-cons ctor-name type-name = +% make-decl ctor-name +% (Sexp_node (Sexp_symbol "datacons") +% (cons type-name +% (cons ctor-name nil))); + +% %% Build type annotation: +% %% var-name : type-expr; +% make-ann : Sexp -> Sexp -> Sexp; +% make-ann var-name type-expr = +% Sexp_node (Sexp_symbol "_:_") +% (cons var-name +% (cons type-expr nil)); + +% type-impl = lambda (x : List Sexp) -> +% %% `x` follow the mask -> +% %% (_|_ Nat zero (succ Nat)) +% %% Type name --^ ^------^ constructors + +% %% Return a list contained inside a node sexp. +% let knil = K nil; +% kerr = K Sexp_error; + +% get-list : Sexp -> List Sexp; +% get-list node = Sexp_dispatch node +% (lambda op lst -> lst) % Nodes +% knil % Symbol +% knil % String +% knil % Integer +% knil % Float +% knil; % List of Sexp + +% %% Get a name (symbol) from a sexp +% %% - (name t) -> name +% %% - name -> name +% get-name : Sexp -> Sexp; +% get-name sxp = +% Sexp_dispatch sxp +% (lambda op _ -> get-name op) % Nodes +% (lambda _ -> sxp) % Symbol +% kerr % String +% kerr % Integer +% kerr % Float +% kerr; % List of Sexp + +% get-args : Sexp -> List Sexp; +% get-args sxp = +% Sexp_dispatch sxp +% (lambda _ args -> args) % Nodes +% (lambda _ -> (nil : List Sexp)) % Symbol +% (lambda _ -> (nil : List Sexp)) % String +% (lambda _ -> (nil : List Sexp)) % Integer +% (lambda _ -> (nil : List Sexp)) % Float +% (lambda _ -> (nil : List Sexp)); % List of Sexp + +% get-type : Sexp -> Sexp; +% get-type sxp = +% Sexp_dispatch sxp +% (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) +% | true => List_nth 1 ss Sexp_error +% | false => sxp) +% (lambda _ -> sxp) +% (lambda _ -> Sexp_error) +% (lambda _ -> Sexp_error) +% (lambda _ -> Sexp_error) +% (lambda _ -> Sexp_error); + +% get-head = List_head Sexp_error; + +% %% Get expression. +% expr = get-head x; + +% %% Expression is Sexp_node (Sexp_symbol "|") (list) +% %% we only care about the list bit +% lst = get-list expr; + +% %% head is (Sexp_node type-name (arg list)) +% name = get-head lst; +% ctor = List_tail lst; + +% type-name = get-name name; + +% %% Create the inductive type definition. +% inductive = Sexp_node (Sexp_symbol "typecons") +% (cons name ctor); + +% %% Declare the inductive type as a function +% %% Useful for recursive type +% type-decl = quote ((uquote (get-name name)) : (uquote ( +% (List_foldl (lambda args arg -> +% Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil))) +% %% FIXME: Don't hardcode TypeLevel.z! +% (Sexp_symbol "Type") (List_reverse (get-args name) nil)) +% ))); + +% decl = make-decl type-name inductive; + +% %% Add constructors. +% ctors = let for-each : List Sexp -> Sexp -> Sexp; +% for-each ctr acc = case ctr +% | cons hd tl => +% let acc2 = chain-decl (make-cons (get-name hd) +% type-name) +% acc +% in for-each tl acc2 +% | nil => acc +% in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil) + +% %% return decls +% in IO_return (chain-decl3 type-decl % type as a function declaration +% decl % inductive type declaration +% ctors); % constructor declarations + +% type_ = macro type-impl; + +% %%%% An inductive type to wrap Sexp + +% type Sexp_wrapper +% | node Sexp (List Sexp) +% | symbol String +% | string String +% | integer Integer +% | float Float +% | block Sexp; + +% Sexp_wrap s = Sexp_dispatch s node symbol string integer float block; + +% %%%% Tuples + +% %% Sample tuple: a module holding Bool and its constructors. +% BoolMod = (##datacons +% %% We need the `?` metavars to be lexically outside of the +% %% `typecons` expression, otherwise they end up generalized, so +% %% we end up with a type constructor like +% %% +% %% typecons _ (cons (τ₁ : Type) (t : τ₁) +% %% (τ₂ : Type) (true : τ₂) +% %% (τ₃ : Type) (false : τ₃)) +% %% +% %% And it's actually even worse because it tries to generalize +% %% over the level of those `Type`s, so we end up with an invalid +% %% inductive type. +% ((lambda t1 t2 t3 +% -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) +% ? ? ?) +% cons) +% (_ := Bool) (_ := true) (_ := false); + +% Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); +% pair = datacons Pair pair; + +% __.__ = +% let mksel o f = +% let constructor = Sexp_node (Sexp_symbol "##datacons") +% (cons (Sexp_symbol "?") +% (cons (Sexp_symbol "cons") +% nil)); +% pattern = Sexp_node constructor +% (cons (Sexp_node (Sexp_symbol "_:=_") +% (cons f (cons (Sexp_symbol "v") +% nil))) +% nil); +% branch = Sexp_node (Sexp_symbol "_=>_") +% (cons pattern (cons (Sexp_symbol "v") nil)); +% in Sexp_node (Sexp_symbol "case_") +% (cons (Sexp_node (Sexp_symbol "_|_") +% (cons o (cons branch nil))) +% nil) +% in macro (lambda args +% -> IO_return +% case args +% | cons o tail +% => (case tail +% | cons f _ => mksel o f +% | nil => Sexp_error) +% | nil => Sexp_error); + +% %% Triplet (tuple with 3 values) +% type Triplet (a : Type) (b : Type) (c : Type) +% | triplet (x : a) (y : b) (z : c); + +% %%%% List with tuple + +% %% Merge two List to a List of Pair +% %% Both List must be of same length +% List_merge : List ?a -> List ?b -> List (Pair ?a ?b); +% List_merge xs ys = case xs +% | cons x xs => ( case ys +% | cons y ys => cons (pair x y) (List_merge xs ys) +% | nil => nil ) % error +% | nil => nil; + +% %% `Unmerge` a List of Pair +% %% The two functions name said it all +% List_map-fst xs = let +% mf p = case p | pair x _ => x; +% in List_map mf xs; + +% List_map-snd xs = let +% mf p = case p | pair _ y => y; +% in List_map mf xs; + +% %%%% Logic + +% %% `False` should be one of the many empty types. +% %% Other popular choices are False = ∀a.a and True = ∃a.a. +% False = Void; +% True = Unit; + +% Not prop = prop -> False; + +% %% Like Bool, except that it additionally carries the meaning of its value. +% %% We don't use the `type` macro here because it would make these `true` +% %% and `false` constructors override `Bool`'s, and we currently don't +% %% want that. +% Decidable = typecons (Decidable (prop : Type_ ?ℓ)) +% (true (p ::: prop)) (false (p ::: Not prop)); + +% %% Testing generalization in inductive type constructors. +% LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient! +% type LList (a : Type) (n : Int) +% | vnil (p ::: Eq n 0) +% | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound! + +% %%%% If + +% define-operator "if" () 2; +% define-operator "then" 2 1; +% define-operator "else" 1 66; + +% if_then_else_ +% = macro (lambda args -> +% let e1 = List_nth 0 args Sexp_error; +% e2 = List_nth 1 args Sexp_error; +% e3 = List_nth 2 args Sexp_error; +% in IO_return (quote (case uquote e1 +% | true => uquote e2 +% | false => uquote e3))); + +% %%%% More boolean + +% %% FIXME: Type annotations should not be needed below. +% not : Bool -> Bool; +% %% FIXME: We use braces here to delay parsing, otherwise the if/then/else +% %% part of the grammar declared above is not yet taken into account. +% not x = { if x then false else true }; + +% or : Bool -> Bool -> Bool; +% or x y = { if x then x else y }; + +% and : Bool -> Bool -> Bool; +% and x y = { if x then y else x }; + +% xor : Bool -> Bool -> Bool; +% xor x y = { if x then (not y) else y }; + +% %% FIXME: Can't use ?a because that is generalized to be universe-polymorphic, +% %% which we don't support in `load` yet. +% fold : Bool -> (a : Type) ≡> a -> a -> a; +% fold x t e = { if x then t else e}; + +% %%%% Test +% test1 : ?; +% test2 : Option Int; +% test3 : Option Int; +% test1 = test2; +% %% In earlier versions of Typer, we could use `?` in declarations +% %% to mean "fill this for me by unifying with later type information", +% %% but this is incompatible with the use of generalization to introduce +% %% implicit arguments. +% %% test4 : Option ?; +% test2 = none; +% test4 : Option Int; +% test4 = test1 : Option ?; +% test3 = test4; + +% %%%% Rewrite of some builtins to use `Option` + +% %% +% %% If `Elab_nth-arg'` returns "_" it means: +% %% A- The constructor isn't defined, or +% %% B- The constructor has no n'th argument +% %% +% %% So in those case this function returns `none` +% %% +% Elab_nth-arg a b c = let +% r = Elab_nth-arg' a b c; +% in case (String_eq r "_") +% | true => (none) +% | false => (some r); + +% %% +% %% If `Elab_arg-pos'` returns (-1) it means: +% %% A- The constructor isn't defined, or +% %% B- The constructor has no argument named like this +% %% +% %% So in those case this function returns `none` +% %% +% Elab_arg-pos a b c = let +% r = Elab_arg-pos' a b c; +% in case (Int_eq r (-1)) +% | true => (none) +% | false => (some r); + +% %%%% +% %%%% Common library +% %%%% + +% %% +% %% `<-` operator used in macro `do` and for tuple assignment +% %% + +% define-operator "<-" 80 96; + +% %% +% %% `List` is the type and `list` is the module +% %% +% list = load "btl/list.typer"; + +% %% +% %% Macro `do` for easier series of IO operation +% %% +% %% e.g.: +% %% do { IO_return true; }; +% %% +% do = let lib = load "btl/do.typer" in lib.do; + +% %% +% %% Module containing various macros for tuple +% %% Used by `case_` +% %% +% tuple-lib = load "btl/tuple.typer"; + +% %% +% %% Get the nth element of a tuple +% %% +% %% e.g.: +% %% tuple-nth tup 0; +% %% +% tuple-nth = tuple-lib.tuple-nth; + +% %% +% %% Affectation of tuple +% %% +% %% e.g.: +% %% (x,y,z) <- tup; +% %% +% _<-_ = tuple-lib.assign-tuple; + +% %% +% %% Instantiate a tuple from expressions +% %% +% %% e.g.: +% %% tup = (x,y,z); +% %% +% _,_ = tuple-lib.make-tuple; + +% Tuple = tuple-lib.tuple-type; + +% %% +% %% Macro `case` for a some more complex pattern matching +% %% +% case_ = let lib = load "btl/case.typer" in lib.case-macro; + +% %% +% %% plain-let +% %% Not recursive and not sequential +% %% +% %% e.g.: +% %% plain-let x = 1; in x; +% %% + +% define-operator "plain-let" () 3; + +% %% +% %% Already defined: +% %% define-operator "in" 3 67; +% %% + +% plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; + +% %% +% %% `case` at function level +% %% +% %% e.g.: +% %% my-fun (x : Bool) +% %% | true => false +% %% | false => true; +% %% +% _|_ = let lib = load "btl/polyfun.typer" in lib._|_; + +% %% +% %% case_as_return_, case_return_ +% %% A `case` for dependent elimination +% %% + +% define-operator "as" 42 42; +% define-operator "return" 42 42; +% depelim = load "btl/depelim.typer"; +% case_as_return_ = depelim.case_as_return_; +% case_return_ = depelim.case_return_; + +% %%%% Unit tests function for doing file + +% %% It's hard to do a primitive which execute test file +% %% because of circular dependency... + +% %% +% %% A macro using `load` for unit testing purpose +% %% +% %% Takes a file name (String) as argument +% %% Returns variable named `exec-test` from the loaded file +% %% +% %% `exec-test` should be a command doing unit tests +% %% for other purpose than that just use `load` directly! +% %% +% Test_file = macro (lambda args -> let + +% %% return an empty command on error +% ret = Sexp_node +% (Sexp_symbol "IO_return") +% (cons (Sexp_symbol "unit") nil); + +% %% Expecting a String and nothing else +% in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) +% (lambda _ _ -> ret) +% (lambda _ -> ret) +% %% `load` is a special form and takes a Sexp rather than a real `String` +% (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test)) +% (lambda _ -> ret) +% (lambda _ -> ret) +% (lambda _ -> ret)) +% ); + +% %%% pervasive.typer ends here.
===================================== src/elab.ml ===================================== @@ -443,28 +443,17 @@ let rec meta_to_var ids (e : lexp) = -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) - | Inductive (l, label, args, cases) - -> let alen = List.length args in - let (_, nargs) - = List.fold_right (fun (ak, v, t) (o', args) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: args)) - args (alen, []) in - let ncases - = SMap.map - (fun fields - -> let flen = List.length fields in - let (_, nfields) - = List.fold_right - (fun (ak, v, t) (o', fields) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: fields)) - fields (flen + alen, []) in - nfields) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, ((_, name) as label), cases) + -> let unmeta_field (ak, v, t) (o', fields) = + let o' = o' - 1 in + o', (ak, v, loop (o' + o) t) :: fields + in + let unmeta_constructor fields = + let flen = List.length fields in + let (_, nfields) = List.fold_right unmeta_field fields (flen, []) in + nfields + in + mkInductive (l, label, SMap.map unmeta_constructor cases) | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases @@ -689,7 +678,12 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = check_inferred ctx e inferred_t t
and unify_or_error lctx lxp ?lxp_name expect actual = - match Unif.unify expect actual lctx with + print_endline ("[unify_or_error] lexp = " ^ lexp_string lxp); + print_endline ("[unify_or_error] expect = " ^ lexp_string expect); + print_endline ("[unify_or_error] actual = " ^ lexp_string actual); + let res = Unif.unify expect actual lctx in + print_endline ("[unify_or_error] unify done"); + match res with | ((ck, _ctx, t1, t2)::_) -> lexp_error (lexp_location lxp) lxp ("Type mismatch" @@ -709,11 +703,17 @@ and unify_or_error lctx lxp ?lxp_name expect actual = * we use is to instantiate implicit arguments when needed, but we could/should * do lots of other things. *) and check_inferred ctx e inferred_t t = + print_endline ("[check_inferred] e = " ^ lexp_string e); + print_endline ("[check_inferred] inferred_t = " ^ lexp_string inferred_t); + print_endline ("[check_inferred] t = " ^ lexp_string t); let (e, inferred_t) = - match OL.lexp'_whnf t (ectx_to_lctx ctx) with + match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) - | _ -> instantiate_implicit e inferred_t ctx in + | _ -> instantiate_implicit e inferred_t ctx + in + print_endline ("[check_inferred] e = " ^ lexp_string e); + print_endline ("[check_inferred] inferred_t = " ^ lexp_string inferred_t); unify_or_error (ectx_to_lctx ctx) e t inferred_t; e
@@ -721,168 +721,176 @@ and check_inferred ctx e inferred_t t = and check_case rtype (loc, target, ppatterns) ctx = (* Helpers *)
+ print_endline ("[check_case] rtype = " ^ lexp_string rtype); + print_endline ("[check_case] target = " ^ sexp_string target); + let pat_string p = sexp_string (pexp_u_pat p) in
- let uniqueness_warn pat = - warning ~loc:(pexp_pat_location pat) - ("Pattern " ^ pat_string pat - ^ " is a duplicate. It will override previous pattern.") in - - let check_uniqueness pat name map = - if SMap.mem name map then uniqueness_warn pat in - - (* get target and its type *) - let tlxp, tltp = infer target ctx in - let tknd = OL.get_type (ectx_to_lctx ctx) tltp in - let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with - | Sort (_, Stype l) -> l - | _ -> fatal "Target lexp's kind is not a sort" in - let it_cs_as = ref None in - let ltarget = ref tlxp in - - let get_cs_as it' lctor = - let unify_ind expected actual = - match Unif.unify actual expected (ectx_to_lctx ctx) with - | (_::_) - -> lexp_error loc lctor - ("Expected pattern of type `" ^ lexp_string expected - ^ "` but got `" ^ lexp_string actual ^ "`") - | [] -> () in - match !it_cs_as with - | Some (it, cs, args) - -> unify_ind it it'; (cs, args) - | None - -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) - -> let (s, targs) = List.fold_left - (fun (s, targs) (ak, name, t) - -> let arg = newMetavar - (ectx_to_lctx ctx) - (ectx_to_scope_level ctx) - name (mkSusp t s) in - (S.cons arg s, (ak, arg) :: targs)) - (S.identity, []) - fargs in - let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); - it_cs_as := Some (it', cs, args); - (cs, args) - | _ -> let call_split e = - match OL.lexp'_whnf e (ectx_to_lctx ctx) with - | Call (f, args) -> (f, args) - | _ -> (e,[]) in + let uniqueness_warn pat = + warning ~loc:(pexp_pat_location pat) + ("Pattern " ^ pat_string pat + ^ " is a duplicate. It will override previous pattern.") in + + let check_uniqueness pat name map = + if SMap.mem name map then uniqueness_warn pat in + + (* get target and its type *) + let tlxp, tltp = infer target ctx in + print_endline ("[check_case] tlxp = " ^ lexp_string tlxp); + print_endline ("[check_case] ltlp = " ^ lexp_string tltp); + + let tknd = OL.get_type (ectx_to_lctx ctx) tltp in + print_endline ("[check_case] tknd = " ^ lexp_string tknd); + + let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with + | Sort (_, Stype l) -> l + | _ -> fatal "Target lexp's kind is not a sort" in + print_endline ("[check_case] tlvl = " ^ lexp_string tlvl); + + let it_cs_as = ref None in + let ltarget = ref tlxp in + + let get_cs_as it' lctor = + print_endline ("[get_cs_as] it' = " ^ lexp_string it'); + print_endline ("[get_cs_as] lctor = " ^ lexp_string lctor); + + let unify_ind expected actual = + match Unif.unify actual expected (ectx_to_lctx ctx) with + | (_::_) + -> lexp_error loc lctor + ("Expected pattern of type `" ^ lexp_string expected + ^ "` but got `" ^ lexp_string actual ^ "`") + | [] -> () + in + + match !it_cs_as with + | Some (it, cs, args) + -> print_endline "unify"; + unify_ind it it'; (cs, args) + | None + -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with + | Inductive (_, _, constructors) + -> print_endline "checking with inductive"; + ltarget := check_inferred ctx tlxp tltp (mkCall (it', [])); + print_endline ("[get_cs_as] ltarget = " ^ lexp_string !ltarget); + it_cs_as := Some (it', constructors, []); + (constructors, []) + | _ -> let call_split e = + match OL.lexp'_whnf e (ectx_to_lctx ctx) with + | Call (f, args) -> (f, args) + | _ -> (e, []) in let (it, targs) = call_split tltp in unify_ind it it'; let constructors = match OL.lexp'_whnf it (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) - -> assert (List.length fargs = List.length targs); - constructors + | Inductive (_, _, constructors) + -> assert (List.length targs == 0); + constructors | _ -> lexp_error (sexp_location target) tlxp - ("Can't `case` on objects of this type: " - ^ lexp_string tltp); - SMap.empty in + ("Can't `case` on objects of this type: " + ^ lexp_string tltp); + SMap.empty in it_cs_as := Some (it, constructors, targs); (constructors, targs) in
- (* Read patterns one by one *) - let fold_fun (lbranches, dflt) (pat, pexp) = + (* Read patterns one by one *) + let fold_fun (lbranches, dflt) (pat, pexp) =
- let shift_to_extended_ctx nctx lexp = - mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx) - - M.length (ectx_to_lctx ctx))) in + let shift_to_extended_ctx nctx lexp = + mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx) + - M.length (ectx_to_lctx ctx))) in
- let ctx_extend_with_eq nctx head_lexp = - (* Add a proof of equality between the target and the branch + let ctx_extend_with_eq nctx head_lexp = + (* Add a proof of equality between the target and the branch head to the context *) - let tlxp' = shift_to_extended_ctx nctx tlxp in - let tltp' = shift_to_extended_ctx nctx tltp in - let tlvl' = shift_to_extended_ctx nctx tlvl in - let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl'); (* Typelevel *) - (Aerasable, tltp'); (* Inductive type *) - (Anormal, head_lexp); (* Lexp of the branch head *) - (Anormal, tlxp')]) (* Target lexp *) - in ctx_extend nctx (loc, None) Variable eqty - in - - let add_default v = - (if dflt != None then uniqueness_warn pat); - let nctx = ctx_extend ctx v Variable tltp in - let head_lexp = mkVar (v, 0) in - let nctx = ctx_extend_with_eq nctx head_lexp in - let rtype' = shift_to_extended_ctx nctx rtype in - let lexp = check pexp rtype' nctx in - lbranches, Some (v, lexp) in - - let add_branch pctor pargs = - let loc = sexp_location pctor in - let lctor, ct = infer pctor ctx in - let rec inst_args ctx e = + let tlxp' = shift_to_extended_ctx nctx tlxp in + let tltp' = shift_to_extended_ctx nctx tltp in + let tlvl' = shift_to_extended_ctx nctx tlvl in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlvl'); (* Typelevel *) + (Aerasable, tltp'); (* Inductive type *) + (Anormal, head_lexp); (* Lexp of the branch head *) + (Anormal, tlxp')]) (* Target lexp *) + in ctx_extend nctx (loc, None) Variable eqty + in + + let add_default v = + (if dflt != None then uniqueness_warn pat); + let nctx = ctx_extend ctx v Variable tltp in + let head_lexp = mkVar (v, 0) in + let nctx = ctx_extend_with_eq nctx head_lexp in + let rtype' = shift_to_extended_ctx nctx rtype in + let lexp = check pexp rtype' nctx in + lbranches, Some (v, lexp) in + + let add_branch pctor pargs = + let loc = sexp_location pctor in + let lctor, ct = infer pctor ctx in + let rec inst_args ctx e = let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in - match lexp_lexp' lxp with - | Lambda (Aerasable, v, t, body) - -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - v t in - let nctx = ctx_extend ctx v Variable t in - let body = inst_args nctx body in - mkSusp body (S.substitute arg) - | e -> lxp in - match lexp_lexp' (nosusp (inst_args ctx lctor)) with - | Cons (it', (_, cons_name)) - -> let _ = check_uniqueness pat cons_name lbranches in - let (constructors, targs) = get_cs_as it' lctor in - let cargs - = try SMap.find cons_name constructors - with Not_found - -> lexp_error loc lctor + match lexp_lexp' lxp with + | Lambda (Aerasable, v, t, body) + -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) + v t in + let nctx = ctx_extend ctx v Variable t in + let body = inst_args nctx body in + mkSusp body (S.substitute arg) + | e -> lxp in + match lexp_lexp' (nosusp (inst_args ctx lctor)) with + | Cons (it', (_, cons_name)) + -> let _ = check_uniqueness pat cons_name lbranches in + let (constructors, targs) = get_cs_as it' lctor in + let cargs + = try SMap.find cons_name constructors + with Not_found + -> lexp_error loc lctor ("`" ^ (lexp_string it') ^ "` does not have a `" ^ cons_name ^ "` constructor"); [] in
- let subst = List.fold_left (fun s (_, t) -> S.cons t s) - S.identity targs in - let rec make_nctx ctx (* elab context. *) - s (* Pending substitution. *) - pargs (* Pattern arguments. *) - cargs (* Constructor arguments. *) - pe (* Pending explicit pattern args. *) - acc = (* Accumulated result. *) - match (pargs, cargs) with - | (_, []) when not (SMap.is_empty pe) - -> let pending = SMap.bindings pe in + let subst = List.fold_left (fun s (_, t) -> S.cons t s) + S.identity targs in + let rec make_nctx ctx (* elab context. *) + s (* Pending substitution. *) + pargs (* Pattern arguments. *) + cargs (* Constructor arguments. *) + pe (* Pending explicit pattern args. *) + acc = (* Accumulated result. *) + match (pargs, cargs) with + | (_, []) when not (SMap.is_empty pe) + -> let pending = SMap.bindings pe in sexp_error loc ("Explicit pattern args `" ^ String.concat ", " (List.map (fun (l, _) -> l) pending) ^ "` have no matching fields"); make_nctx ctx s pargs cargs SMap.empty acc - | [], [] -> ctx, List.rev acc - | (_, pat)::_, [] - -> lexp_error loc lctor + | [], [] -> ctx, List.rev acc + | (_, pat)::_, [] + -> lexp_error loc lctor "Too many pattern args to the constructor"; make_nctx ctx s [] [] pe acc - | (_, (ak, (_, Some fname), fty)::cargs) - when SMap.mem fname pe - -> let var = SMap.find fname pe in + | (_, (ak, (_, Some fname), fty)::cargs) + when SMap.mem fname pe + -> let var = SMap.find fname pe in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in make_nctx nctx (ssink var s) pargs cargs (SMap.remove fname pe) ((ak, var)::acc) - | ((ef, var)::pargs, (ak, _, fty)::cargs) - when (match (ef, ak) with - | (Some (_, "_"), _) | (None, Anormal) -> true - | _ -> false) - -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + | ((ef, var)::pargs, (ak, _, fty)::cargs) + when (match (ef, ak) with + | (Some (_, "_"), _) | (None, Anormal) -> true + | _ -> false) + -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) - | ((Some (l, fname), var)::pargs, cargs) - -> if SMap.mem fname pe then + | ((Some (l, fname), var)::pargs, cargs) + -> if SMap.mem fname pe then sexp_error l ("Duplicate explicit field `" ^ fname ^ "`"); make_nctx ctx s pargs cargs (SMap.add fname var pe) acc - | pargs, (ak, fname, fty)::cargs - -> let var = (loc, None) in + | pargs, (ak, fname, fty)::cargs + -> let var = (loc, None) in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in if ak = Anormal then sexp_error loc @@ -891,37 +899,37 @@ and check_case rtype (loc, target, ppatterns) ctx = | _ -> "")); make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) in - let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in - let head_lexp_ctor = - shift_to_extended_ctx nctx - (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in - let head_lexp_args = - List.mapi (fun i (ak, vname) -> - (ak, mkVar (vname, List.length fargs - i - 1))) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in - let nctx = ctx_extend_with_eq nctx head_lexp in - let rtype' = shift_to_extended_ctx nctx rtype in - let lexp = check pexp rtype' nctx in - SMap.add cons_name (loc, fargs, lexp) lbranches, - dflt - (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it - * and try again with the result. *) - | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt - in - - match pat with - | Ppatsym ((_, None) as var) -> add_default var - | Ppatsym ((l, Some name) as var) - -> if Eval.constructor_p name ctx then - add_branch (Symbol (l, name)) [] - else add_default var (* A named default branch. *) - - | Ppatcons (pctor, pargs) -> add_branch pctor pargs in - - let (lpattern, dflt) = - List.fold_left fold_fun (SMap.empty, None) ppatterns in - - mkCase (loc, tlxp, rtype, lpattern, dflt) + let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in + let head_lexp_ctor = + shift_to_extended_ctx nctx + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + let head_lexp_args = + List.mapi (fun i (ak, vname) -> + (ak, mkVar (vname, List.length fargs - i - 1))) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let nctx = ctx_extend_with_eq nctx head_lexp in + let rtype' = shift_to_extended_ctx nctx rtype in + let lexp = check pexp rtype' nctx in + SMap.add cons_name (loc, fargs, lexp) lbranches, + dflt + (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it + * and try again with the result. *) + | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt + in + + match pat with + | Ppatsym ((_, None) as var) -> add_default var + | Ppatsym ((l, Some name) as var) + -> if Eval.constructor_p name ctx then + add_branch (Symbol (l, name)) [] + else add_default var (* A named default branch. *) + + | Ppatcons (pctor, pargs) -> add_branch pctor pargs in + + let (lpattern, dflt) = + List.fold_left fold_fun (SMap.empty, None) ppatterns in + + mkCase (loc, tlxp, rtype, lpattern, dflt)
and elab_macro_call ctx func args ot = let t @@ -1156,11 +1164,11 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) match Myers.nth i (ectx_to_lctx nctx) with | (v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in - let e = check pexp adjusted_t nctx in - let (grm, ec, lc, sl) = nctx in - let d = (v', LetDef (i + 1, e), t) in - (IMap.add i ((l, Some vname), e, t) map, - (grm, ec, Myers.set_nth i d lc, sl)) + let e = check pexp adjusted_t nctx in + let (grm, ec, lc, sl) = nctx in + let d = (v', LetDef (i + 1, e), t) in + (IMap.add i ((l, Some vname), e, t) map, + (grm, ec, Myers.set_nth i d lc, sl)) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -1408,11 +1416,11 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp') in - if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error loc ("Unknown built-in `" ^ name ^ "`"); - BI.add_builtin_cst name bi; - (bi, Checked) + let bi = mkBuiltin ((loc, name), ltp') in + if not (SMap.mem name (!EV.builtin_functions)) then + sexp_error loc ("Unknown built-in `" ^ name ^ "`"); + BI.add_builtin_cst name bi; + (bi, Checked) | None -> error ~loc "Built-in's type not provided by context!"; sform_dummy_ret ctx loc)
@@ -1445,62 +1453,40 @@ let elab_datacons_arg s = match s with -> (elab_colon_to_ak k, elab_p_id s, t) | _ -> (Anormal, (sexp_location s, None), s)
-let elab_typecons_arg arg : (arg_kind * vname * sexp option) = - match arg with - | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e]) - -> (elab_colon_to_ak k, - (l, Some name), Some e) - | Symbol (l, name) -> (Anormal, (l, Some name), None) - | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) - (sexp_location arg) - "Unrecognized formal arg"; - (Anormal, (sexp_location arg, None), None) - let sform_typecons ctx loc sargs ot = match sargs with | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) - | formals :: constrs - -> let (label, formals) = match formals with - | Node (label, formals) -> (label, formals) - | _ -> (formals, []) in - let label = match label with + | label :: constrs + -> let (_, name) as 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) = elab_typecons_arg sformal in - let ltp = match opxp with - | Some pxp -> let (l,_) = infer pxp ctx in l - | None -> let (l,_) = var in - newMetatype (ectx_to_lctx ctx) - (ectx_to_scope_level ctx) l in - - parse_formals sformals ((kind, var, ltp) :: rformals) - (ectx_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 elab_datacons_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) + | _ + -> let loc = sexp_location label in + let message = + "Expected the inductive type name to be a symbol, but got " + ^ sexp_string label + in + sexp_error loc message; + (loc, "<error>") + 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 elab_datacons_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 ctx in + mkInductive (loc, label, map_ctor), Lazy
let sform_hastype ctx loc sargs ot = match sargs with @@ -1689,17 +1675,22 @@ let rec sform_lambda kind ctx loc sargs ot = let rec sform_case ctx loc sargs ot = match sargs with | [Node (Symbol (_, "_|_"), se :: scases)] -> let parse_case branch = match branch with - | Node (Symbol (_, "_=>_"), [pat; code]) - -> (pexp_p_pat pat, code) - | _ -> let l = (sexp_location branch) in - sexp_error l "Unrecognized simple case branch"; - (Ppatsym (l, None), Symbol (l, "?")) in - let pcases = List.map parse_case scases in - let t = match ot with - | Some t -> t - | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc in - let le = check_case t (loc, se, pcases) ctx in - (le, match ot with Some _ -> Checked | None -> Inferred t) + | Node (Symbol (_, "_=>_"), [pat; code]) + -> (pexp_p_pat pat, code) + | _ -> let l = (sexp_location branch) in + sexp_error l "Unrecognized simple case branch"; + (Ppatsym (l, None), Symbol (l, "?")) + in + let pcases = List.map parse_case scases in + + let t = match ot with + | Some t -> t + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc in + print_endline ("[sform_case] t = " ^ lexp_string t); + print_endline ("[sform_case] se = " ^ sexp_string se); + let le = check_case t (loc, se, pcases) ctx in + print_endline ("[sform_case] le = " ^ lexp_string le); + (le, match ot with Some _ -> Checked | None -> Inferred t)
(* In case there are no branches, pretend there was a | anyway. *) | [e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot
===================================== src/eval.ml ===================================== @@ -812,14 +812,18 @@ let erasable_p name nth ectx = | (k, _, _) -> k = Aerasable ) else false | _ -> false in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> is_erasable (get_inductive_ctor (get_inductive i)) - | _ -> false) - | _ -> false + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> is_erasable constructors + | _ -> false) + | _ -> false with Senv_Lookup_Fail _ -> false
let erasable_p2 t name ectx = @@ -833,14 +837,18 @@ let erasable_p2 t name ectx = | _ -> false) args) | _ -> false in - try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> is_erasable (get_inductive_ctor (get_inductive i)) - | _ -> false) - | _ -> false + try + let idx = senv_lookup t ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some t), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match env_lookup_expr ectx (get_var e) with + | Some (Inductive (_, _, constructors), _) -> is_erasable constructors + | _ -> false) + | _ -> false with Senv_Lookup_Fail _ -> false
let nth_ctor_arg name nth ectx = @@ -851,14 +859,18 @@ let nth_ctor_arg name nth ectx = | _ -> "_" | exception (Failure _) -> "_" ) | _ -> "_" in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> find_nth (get_inductive_ctor (get_inductive i)) - | _ -> "_") - | _ -> "_" + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> find_nth constructors + | _ -> "_") + | _ -> "_" with Senv_Lookup_Fail _ -> "_"
let ctor_arg_pos name arg ectx = @@ -872,14 +884,18 @@ let ctor_arg_pos name arg ectx = | None -> (-1) | Some n -> n ) | _ -> (-1) in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> find_arg (get_inductive_ctor (get_inductive i)) - | _ -> (-1)) - | _ -> (-1) + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> find_arg constructors + | _ -> (-1)) + | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)
let is_constructor loc depth args_val = match args_val with
===================================== src/inverse_subst.ml ===================================== @@ -197,9 +197,10 @@ let rec lookup_inv_subst (i : db_index) (s : subst) : db_index | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible | S.Identity o -> i - o | S.Cons (e, s, o) when pred_var e (fun e -> get_var_db_index e = i - o) - -> (try let i'' = lookup_inv_subst (get_var_db_index (get_var e)) s in - assert (i'' != 0); - raise Ambiguous + -> (try + let i'' = lookup_inv_subst (get_var_db_index (get_var e)) s in + assert (i'' != 0); + raise Ambiguous with Not_invertible -> 0) | S.Cons (e, s, o) -> assert (match lexp_lexp' e with Var _ -> true | _ -> e = impossible); @@ -281,22 +282,18 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Call (f, args) -> mkCall (apply_inv_subst f s, L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, apply_inv_subst t s) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let inv_subst_case args = + let (_, ncase) = + L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, apply_inv_subst t s) + :: nargs)) + (s, []) args + in + L.rev ncase + in + mkInductive (l, label, SMap.map inv_subst_case cases) | Cons (it, name) -> mkCons (apply_inv_subst it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,
===================================== src/lexp.ml ===================================== @@ -37,7 +37,7 @@ module S = Subst type vname = U.vname type vref = U.vref type meta_id = int (* Identifier of a meta variable. *) - +type location = U.location type label = symbol
(*************** Elaboration to Lexp *********************) @@ -55,9 +55,11 @@ type label = symbol * And the type of the 3rd binding is defined in the scope of the * surrounded context extended with the first and the second bindings. *)
+ type ltype = lexp and subst = lexp S.subst (* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *) + and inductive = location * label * ((arg_kind * vname * ltype) list) SMap.t and lexp = lexp' * int and lexp' = | Imm of sexp (* Used for strings, ... *) @@ -71,9 +73,7 @@ type ltype = lexp | Arrow of arg_kind * vname * ltype * U.location * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname * ltype) list) SMap.t + | Inductive of inductive | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp * ltype (* The type of the return value of all branches *) @@ -213,15 +213,10 @@ let lexp'_hash (lp : lexp') = -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) (U.combine_hash (lexp_hash t) (lexp_hash e))) - | Inductive (l, n, a, cs) + | Inductive (l, n, cs) -> U.combine_hash 9 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) - (U.combine_hash (U.combine_hashes - (List.map (fun e -> let (ak, n, lt) = e in - (U.combine_hash (Hashtbl.hash ak) - (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) - a)) - (Hashtbl.hash cs))) + (Hashtbl.hash cs)) | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) -> U.combine_hash 11 (U.combine_hash @@ -270,11 +265,11 @@ let hc_eq e1 e2 = | (Call (e1, as1), Call (e2, as2)) -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 - | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> let datacons_hc_eq (ak1, _, e1) (ak2, _, e2) = + ak1 = ak2 && e1 == e2 + in + l1 = l2 && SMap.equal (List.for_all2 datacons_hc_eq) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> e1 == e2 && r1 == r2 && SMap.equal @@ -300,18 +295,18 @@ let hc_table : WHC.t = WHC.create 1000 let hc (l : lexp') : lexp = WHC.merge hc_table (l, lexp'_hash l)
-let mkImm s = hc (Imm s) -let mkSortLevel l = hc (SortLevel l) -let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t) = hc (Builtin (v, t)) -let mkVar v = hc (Var v) -let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) -let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) -let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) -let mkCons (t, n) = hc (Cons (t, n)) -let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) -let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) +let mkImm s = hc (Imm s) +let mkSortLevel l = hc (SortLevel l) +let mkSort (l, s) = hc (Sort (l, s)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkVar v = hc (Var v) +let mkLet (l, ds, e) = hc (Let (l, ds, e)) +let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +let mkInductive (l, n, cs) = hc (Inductive (l, n, cs)) +let mkCons (t, n) = hc (Cons (t, n)) +let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) +let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) let mkCall (f, es) = match lexp_lexp' f, es with | Call (f', es'), _ -> hc (Call (f', es' @ es)) @@ -385,21 +380,16 @@ let get_var_db_index v = let get_var_vname v = let (n, idx) = v in n
-let pred_inductive l pred = +let pred_inductive l (pred : inductive -> bool) = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> pred (l, n, a, cs) - | _ -> false + | Inductive inductive -> pred inductive + | _ -> false
let get_inductive l = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> (l, n, a, cs) + | Inductive (l, n, cs) -> (l, n, cs) | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive "
-let get_inductive_ctor i = - let (l, n, a, cs) = i in cs - -let is_inductive l = pred_inductive l (fun e -> true) - (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -510,7 +500,7 @@ let rec lexp_location e = | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l | Call (f,_) -> lexp_location f - | Inductive (l,_,_,_) -> l + | Inductive (l,_,_) -> l | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e @@ -547,21 +537,17 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) | Call (f, args) -> mkCall (mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) + | Inductive (l, label, cases) + -> let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, - (ak, v, mkSusp t s) + (ak, v, mkSusp t s) :: nargs)) (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (mkSusp it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, @@ -614,21 +600,17 @@ let clean e = | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) | Call (f, args) -> mkCall (clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, clean s t) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, clean s t) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, clean s t) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, @@ -689,7 +671,7 @@ let rec lexp_unparse lxp = -> (* (vdef * lexp * ltype) list *) let sdecls = List.fold_left (fun acc (vdef, lxp, ltp) - -> Node (Symbol (U.dummy_location, "_=_"), + -> Node (Symbol (U.dummy_location, "_:_"), [Symbol (sname vdef); lexp_unparse ltp]) :: Node (Symbol (U.dummy_location, "_=_"), [Symbol (sname vdef); lexp_unparse lxp]) @@ -703,14 +685,9 @@ let rec lexp_unparse lxp = let sargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs)
- | Inductive(loc, label, lfargs, ctors) -> - (* (arg_kind * vdef * ltype) list *) - (* (arg_kind * pvar * pexp option) list *) - let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in - + | Inductive (loc, label, ctors) -> Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) + Symbol label :: List.map (fun (name, types) -> Node (Symbol (loc, name), @@ -783,7 +760,7 @@ and lexp_string lxp = sexp_string (lexp_unparse lxp)
and subst_string s = match s with | S.Identity o -> "↑" ^ string_of_int o - | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s + | S.Cons (l, s, 0) -> lexp_string l ^ " · " ^ subst_string s | S.Cons (l, s, o) -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"
@@ -943,9 +920,6 @@ and lexp_str ctx (exp : lexp) : string = let kind_str k = match k with | Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in
- let kindp_str k = match k with - | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in - let get_name fname = match lexp_lexp' fname with | Builtin ((_, name), _) -> name, 0 @@ -968,8 +942,8 @@ and lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx (push_susp e subst) - | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) + | MVal e -> lexp_str ctx (push_susp e subst) + | _ -> "?" ^ maybename name ^ " " ^ subst_string subst ^ index idx)
| Let (_, decls, body) -> (* Print first decls without indent *) @@ -1026,21 +1000,10 @@ and lexp_str ctx (exp : lexp) : string = | _ -> let args = List.fold_left print_arg "" args in "(" ^ (lexp_str' fname) ^ args ^ ")")
- | Inductive (_, (_, name), [], ctors) -> + | Inductive (_, (_, name), ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ (lexp_str_ctor ctx ctors)
- | Inductive (_, (_, name), args, ctors) - -> let args_str - = List.fold_left - (fun str (arg_kind, (_, name), ltype) - -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype) ^ ")") - "" args in - - (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ - (lexp_str_ctor ctx ctors) - | Case (_, target, _ret, map, dflt) ->( let str = (keyword "case ") ^ (lexp_str' target) in let arg_str arg @@ -1138,11 +1101,11 @@ let rec eq e1 e2 = | (Call (e1, as1), Call (e2, as2)) -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 - | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> let datacons_eq (ak1, _, e1) (ak2, _, e2) = + ak1 = ak2 && eq e1 e2 + in + l1 = l2 && SMap.equal (List.for_all2 datacons_eq) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> eq e1 e2 && eq r1 r2 && SMap.equal
===================================== src/opslexp.ml ===================================== @@ -26,6 +26,7 @@ module IMap = U.IMap (* open Lexer *) open Sexp module P = Pexp +open Pexp (* open Myers *) (* open Grammar *) open Lexp @@ -196,21 +197,17 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> Log.internal_error "" in mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in let reduce it name aargs = - let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with - | Inductive (_,_,fargs,_) -> fargs - | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in + let () = match lexp_lexp' (lexp_whnf_aux it ctx) with + | Inductive _ -> () + | _ -> Log.log_error "Case on a non-inductive type in whnf!" in try let (_, _, branch) = SMap.find name branches in - let (subst, _) - = List.fold_left - (fun (s, targs) (_, arg) -> - match targs with - | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) - | _targ::targs -> - (* Ignore the type arguments *) - (s, targs)) - (S.identity, targs) - aargs in + let subst = + List.fold_left + (fun s (_, arg) -> S.cons (lexp_whnf_aux arg ctx) s) + S.identity + aargs + in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) let subst = S.cons (get_refl e') subst in lexp_whnf_aux (push_susp branch subst) ctx @@ -322,9 +319,8 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in e1' == e2' || - let changed = not (e1 == e1' && e2 == e2') in - if changed && set_member_p vs e1' e2' then true else - let vs' = if changed then set_add vs e1' e2' else vs in + if set_member_p vs e1' e2' then true else + let vs' = set_add vs e1' e2' in let conv_p = conv_p' ctx vs' in match (lexp_lexp' e1', lexp_lexp' e2') with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 @@ -362,29 +358,23 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = && (conv_erase && ak1 = P.Aerasable || conv_p t1 t2)) true args1 args2 in conv_p f1 f2 && conv_arglist_p args1 args2 - | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) + + | (Inductive (_, ((_, name_l) as l1), cases1), Inductive (_, ((_, name_r) as l2), cases2)) -> let rec conv_fields ctx vs fields1 fields2 = - match fields1, fields2 with - | ([], []) -> true - | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) - (set_shift vs) - fields1 fields2 - | _,_ -> false in - let rec conv_args ctx vs args1 args2 = - match args1, args2 with - | ([], []) -> - (* Args checked alright, now go on with the fields, - * using the new context. *) - SMap.equal (conv_fields ctx vs) cases1 cases2 - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) - (set_shift vs) - args1 args2 - | _,_ -> false in - l1 == l2 && conv_args ctx vs' args1 args2 + match fields1, fields2 with + | [], [] -> true + | (ak1, vd1, t1) :: fields1, (ak2, vd2, t2) :: fields2 + -> ak1 == ak2 + && conv_p' ctx vs t1 t2 + && conv_fields + (DB.lexp_ctx_cons ctx vd1 Variable t1) + (set_shift vs) + fields1 + fields2 + | _, _ -> false + in + l1 == l2 && SMap.equal (conv_fields ctx vs') cases1 cases2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 | (Case (_, target1, r1, cases1, def1), Case (_, target2, r2, cases2, def2)) -> (* FIXME The termination of this case conversion is very @@ -410,13 +400,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | Call (f, args) -> (f, args) | _ -> (etype, []) in (* 2. Build the substitution for the inductive arguments *) - let fargs, ctors = + let ctors = (match lexp'_whnf it ctx with - | Inductive (_, _, fargs, constructors) - -> fargs, constructors + | Inductive (_, _, constructors) + -> constructors | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in - let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s) - S.identity fargs aargs in (* 3. Compare the branches *) let ctx_extend_with_eq ctx subst hlxp = let tlxp = mkSusp target subst in @@ -450,7 +438,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = vdefs1 vdefs2 fieldtypes else None | _,_,_ -> None in - match mkctx ctx [] fargs_subst (List.length fields1) + match mkctx ctx [] Subst.identity (List.length fields1) fields1 fields2 fieldtypes with | None -> false | Some (nctx, args, _subst) -> @@ -694,53 +682,42 @@ and check'' erased ctx e = ^ lexp_string ft ^ ")!"); ft)) ft args - | Inductive (l, label, args, cases) - -> let rec arg_loop ctx erased args = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _, _) = - List.fold_left - (fun (level, ictx, erased, n) (ak, v, t) -> - ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in - match lexp_lexp' lwhnf with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) - (mkSusp level' (L.sunshift n)) - | tt -> error_tc ~loc:(lexp_location t) - ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline () - ) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string lwhnf ^")"); - level), - DB.lctx_extend ictx v Variable t, - DB.set_sink 1 erased, - n + 1)) - (level, ctx, erased, 0) - case in - level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) - | (ak, v, t)::args - -> let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, lexp_location t, - arg_loop (DB.lctx_extend ctx v Variable t) - (dbset_push ak erased) - args) in - let tct = arg_loop ctx erased args in - tct + | Inductive (l, label, cases) + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _, _) = + List.fold_left + (fun (level, ictx, erased, n) (ak, v, t) -> + ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in + match lexp_lexp' lwhnf with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (* FIXME: If it does refer, + * we get an ugly error! *) + (mkSusp level' (L.sunshift n)) + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string lwhnf ^")"); + level), + DB.lctx_extend ictx v Variable t, + DB.set_sink 1 erased, + n + 1)) + (level, ctx, erased, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -757,17 +734,13 @@ and check'' erased ctx e = "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs -> - let rec mksubst s fargs aargs = - match fargs, aargs with - | [], [] -> s - | _farg::fargs, (_ak, aarg)::aargs - (* We don't check aarg's type, because we assume that `check` - * returns a valid type. *) - -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (error_tc ~loc:l - "Wrong arg number to inductive type!"; s) in - let s = mksubst S.identity fargs aargs in + | Inductive (_, _, constructors), aargs -> + let () = match aargs with + | [] -> () + | _ + -> let message = "Wrong arg number to inductive type!" in + error_tc ~loc:l message + in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in @@ -802,7 +775,7 @@ and check'' erased ctx e = mkCall (mkCons (it, (l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = - mkctx erased ctx s hctor vdefs fieldtypes in + mkctx erased ctx Subst.identity hctor vdefs fieldtypes in let subst = S.shift (List.length vdefs) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx branch @@ -830,29 +803,18 @@ and check'' erased ctx e = ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) + | Inductive (l, _, constructors) -> (try let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) + | [] -> let nargs = List.length fieldtypes in + mkCall (mkSusp t (S.shift nargs), []) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in - buildtype fargs + fieldargs ftypes) + in + fieldargs fieldtypes with Not_found -> (error_tc ~loc:l ("Constructor "" ^ name ^ "" does not exist"); @@ -939,23 +901,19 @@ and fv (e : lexp) : (DB.set * mv_set) = then fv_erase afvs else afvs)) (fv f) args - | Inductive (_, _, args, cases) - -> let alen = List.length args in - let s - = List.fold_left (fun s (_, _, t) - -> fv_sink 1 (fv_union s (fv t))) - fv_empty args in - let s - = SMap.fold - (fun _ fields s - -> fv_union + | Inductive (_, _, cases) + -> let s = + SMap.fold + (fun _ fields s + -> fv_union s (fv_hoist (List.length fields) (List.fold_left (fun s (_, _, t) -> fv_sink 1 (fv_union s (fv t))) fv_empty fields))) - cases s in - fv_hoist alen s + cases fv_empty + in + fv_hoist 0 s | Cons (t, _) -> fv_erase (fv t) | Case (_, e, t, cases, def) -> let s = fv_union (fv e) (fv_erase (fv t)) in @@ -1020,67 +978,48 @@ and get_type ctx e = -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args - | Inductive (l, label, args, cases) + | Inductive (l, label, cases) (* FIXME: Use `check` here but silencing errors? *) - -> let rec arg_loop args ctx = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _) = - List.fold_left - (fun (level, ictx, n) (ak, v, t) -> - ((match lexp'_whnf (get_type ictx t) ictx with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n)) - | tt -> level), - DB.lctx_extend ictx v Variable t, - n + 1)) - (level, ctx, 0) - case in - level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) - | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in - let tct = arg_loop args ctx in - tct + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _) = + List.fold_left + (fun (level, ictx, n) (ak, v, t) -> + ((match lexp'_whnf (get_type ictx t) ictx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) + | tt -> level), + DB.lctx_extend ictx v Variable t, + n + 1)) + (level, ctx, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) - -> (try - let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in - let rec fieldargs ftypes = - match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) - | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in - buildtype fargs - with Not_found -> DB.type_int) - | _ -> DB.type_int) + | Inductive (l, _, constructors) + -> (try + let fieldtypes = SMap.find name constructors in + let rec fieldargs ftypes = + match ftypes with + | [] -> let nargs = List.length fieldtypes in + mkCall (mkSusp t (S.shift nargs), + []) + | (ak, vd, ftype) :: ftypes + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in + fieldargs fieldtypes + with Not_found -> DB.type_int) + | _ -> DB.type_int) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> get_type ctx (push_susp e s) @@ -1122,11 +1061,11 @@ let rec erase_type (lxp: lexp): E.elexp = | L.Susp(l, s) -> erase_type (L.push_susp l s)
(* To be thrown out *) - | L.Arrow _ -> E.Type lxp - | L.SortLevel _ -> E.Type lxp - | L.Sort _ -> E.Type lxp + | L.Arrow _ -> E.Type lxp + | L.SortLevel _ -> E.Type lxp + | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp + | L.Inductive (l, label, _) -> E.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) @@ -1207,7 +1146,7 @@ let ctx2tup ctx nctx = let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*)
- mkCall (mkCons (mkInductive (loc, type_label, [], + mkCall (mkCons (mkInductive (loc, type_label, SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname,
===================================== src/pexp.ml ===================================== @@ -54,8 +54,10 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = [Symbol s; match t with Some e -> e | None -> Symbol (l, "_")])
-let pexp_p_pat_arg (s : sexp) = match s with - | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n)) +let pexp_p_pat_arg (s : sexp) = + print_endline ("+[pexp_p_pat_arg] s = " ^ sexp_string s); + match s with + | Symbol (l, n) -> (None, (l, match n with "_" -> None | _ -> Some n)) | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)]) -> (Some f, (l, Some n)) | _ -> let loc = sexp_location s in @@ -69,7 +71,9 @@ let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = | Some ((l,_) as n) -> Node (Symbol (l, "_:=_"), [Symbol n; pname])
-let pexp_p_pat (s : sexp) : ppat = match s with +let pexp_p_pat (s : sexp) : ppat = + print_endline ("+[pexp_p_pat] s = " ^ sexp_string s); + match s with | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n) | Node (c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args)
===================================== src/unification.ml ===================================== @@ -79,13 +79,13 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Lambda (_, _, t, e) -> oi t || oi e | Call (f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args - | Inductive (_, _, args, cases) + | Inductive (_, _, cases) -> SMap.fold (fun _ fields o -> List.fold_left (fun o (_, _, t) -> o || oi t) o fields) cases - (List.fold_left (fun o (_, _, t) -> o || oi t) false args) + false | Cons (t, _) -> oi t | Case (_, e, t, cases, def) -> let o = oi e || oi t in @@ -203,6 +203,8 @@ and unify' (e1: lexp) (e2: lexp) if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in + print_endline ("[unify'] e1' = " ^ lexp_string e1'); + print_endline ("[unify'] e2' = " ^ lexp_string e2'); if e1' == e2' then [] else let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then [] else @@ -296,6 +298,10 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = *) and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = + + print_endline ("[unify_metavar] lxp1 = " ^ lexp_string lxp1); + print_endline ("[unify_metavar] lxp2 = " ^ lexp_string lxp2); + let unif idx s lxp = let t = match metavar_lookup idx with | MVal _ -> Log.internal_error @@ -410,6 +416,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) *) and unify_var (var: lexp) (lxp: lexp) ctx vs : return_type = + print_endline ("[unify_var] var = " ^ lexp_string var); + print_endline ("[unify_var] lxp = " ^ lexp_string lxp); match (lexp_lexp' var, lexp_lexp' lxp) with | (Var _, Var _) when OL.conv_p ctx var lxp -> [] | (_, _) -> [(CKresidual, ctx, var, lxp)] @@ -565,12 +573,12 @@ and is_same arglist arglist2 =
and unify_inductive lxp1 lxp2 ctx vs = match lexp_lexp' lxp1, lexp_lexp' lxp2 with - | (Inductive (_loc1, label1, args1, consts1), - Inductive (_loc2, label2, args2, consts2)) - -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2 + | (Inductive (_loc1, label1, consts1), + Inductive (_loc2, label2, consts2)) + -> unify_inductive' ctx vs consts1 consts2 lxp1 lxp2 | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]
-and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive' ctx vs consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) @@ -582,7 +590,6 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = else (unify' t1 t2 ctx vs) @ residue)) (ctx, vs, []) (List.combine args1 args2) in - let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in if not (SMap.cardinal consts1 == SMap.cardinal consts2) then [(CKimpossible, ctx, e1, e2)] else @@ -592,7 +599,7 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = = unif_formals ctx vs args1 args2 in residue' @ residue | exception Not_found -> [(CKimpossible, ctx, e1, e2)]) - consts1 residue + consts1 []
(** unify the SMap of list in Inductive *) (* and unify_induct_sub_list l1 l2 subst =
===================================== tests/opslexp_test.ml ===================================== @@ -0,0 +1,72 @@ +(* Copyright (C) 2020 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +open Utest_lib +open Util + +let assert_conv_p + (name : string) + ?(setup : string option) + ?(close : bool = false) + (l : string) + (r : string) + : unit = + + let run () = + let ectx = Elab.default_ectx in + let ectx = + match setup with + | Some setup' -> snd (Elab.lexp_decl_str setup' ectx) + | None -> ectx + in + let last_metavar = !Unification.global_last_metavar in + + let ls = Elab.lexp_expr_str l ectx in + Unification.global_last_metavar := last_metavar; + let rs = Elab.lexp_expr_str r ectx in + + let lctx = Debruijn.ectx_to_lctx ectx in + let l' = + match ls with + | [l'] -> l' + | _ -> failwith "expected a single lexp" + in + let r' = + match rs with + | [r'] -> if close then Opslexp.lexp_close lctx r' else r' + | _ -> failwith "expected a single lexp" + in + + if Opslexp.conv_p lctx l' r' then success else failure + in + add_test "OPSLEXP" name run + +let () = + assert_conv_p + "Inductive type is convertible to its closure." + ~setup:{| + List* : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; + List* = lambda ℓ ≡> lambda α -> typecons List* (nil*) (cons* α (List* (ℓ := ℓ) α)); + |} + ~close:true + "List* Sexp" + "List* Sexp"; + + run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/71f837603183489fa3d925646634a66271...