Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer

Commits: a08107b5 by Jean-Alexandre Barszcz at 2020-07-28T22:09:10-04:00 Delay parsing of declarations until elaboration for define-operator

* elab.ml (lexp_p_decls): Add a parameter for unparsed tokens, so that later declarations can be parsed in a context with newly declared operators

- - - - - 631d652e by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 Remove the parsing error for tightly binding postfix operators

- - - - - cdfc117c by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 Dump the evaluation context when the variable names don't match

- - - - - 63ae1fea by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 Assign the builtins Int.+, etc to suitable variables Int_+, etc.

_+_ can be Int.+ by default, but we should also keep that value in Int_+ in case _+_ gets reassigned (with a num typeclass, for instance).

- - - - - bfdee451 by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 [WIP] Make unification symmetric

- - - - - b8f917be by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 [WIP] Handle variables earlier during unification

- - - - - ac2ecf96 by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 [WIP] experiments with Decidable and proofs

- - - - - ec06f4fc by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 [WIP] unify instead of conv_p in sform_lambda

- - - - - 7c30e0eb by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 [WIP] proof of Decidable (a < b)

- - - - - 5bc4b6bb by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 [WIP] First draft of an instance search algorithm

- - - - - c767b2e9 by Jean-Alexandre Barszcz at 2020-07-28T22:10:13-04:00 WIP WIP WIP

- - - - - c1a000e6 by Jean-Alexandre Barszcz at 2020-07-28T22:18:32-04:00 WIP WIP getting there

- - - - - 45d83e1a by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 [WIP] Add a set of typeclasses to the elab context

- - - - - 7546e4f6 by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 [WIP] Add a syntax for records

- - - - - 040f8943 by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 [WIP] Extend the Decidable sample with conjunction (dep on records)

- - - - - 9a59263b by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 Resolve instances in the REPL (since exprs. are not generalized)

- - - - - 2f880b02 by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 [WIP] Do the set_getenv

IIRC these were missing to correctly handle the elab context for macro expansion and Elab_... primitives. Perhaps it would be simpler to call set_getenv once before macro expansion rather than everywhere where the context can change. Needs some experimentation and tests.

- - - - - 9a930f76 by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 Num class example

- - - - - 28c78ffc by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 Num class (with records)

- - - - - dff7b36f by Jean-Alexandre Barszcz at 2020-07-28T22:19:22-04:00 Move the Eq builtin to debruijn.ml to make it available for elab.

- - - - - 0da3daa9 by Jean-Alexandre Barszcz at 2020-07-28T22:42:59-04:00 [WIP] (Broken) Add Eq to case

- - - - -

20 changed files:

- btl/builtins.typer - btl/pervasive.typer - + btl/records.typer - + samples/decidable.typer - + samples/num_class.typer - + samples/num_class_recs.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elab.ml - src/env.ml - src/eval.ml - + src/instances.ml - src/log.ml - src/myers.ml - src/opslexp.ml - src/sexp.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -100,10 +100,15 @@ true = datacons Bool true; false = datacons Bool false;

%% Basic operators -_+_ = Built-in "Int.+" : Int -> Int -> Int; -_-_ = Built-in "Int.-" : Int -> Int -> Int; -_*_ = Built-in "Int.*" : Int -> Int -> Int; -_/_ = Built-in "Int./" : Int -> Int -> Int; +Int_+ = Built-in "Int.+" : Int -> Int -> Int; +Int_- = Built-in "Int.-" : Int -> Int -> Int; +Int_* = Built-in "Int.*" : Int -> Int -> Int; +Int_/ = Built-in "Int./" : Int -> Int -> Int; + +_+_ = Int_+; +_-_ = Int_-; +_*_ = Int_*; +_/_ = Int_/;

%% modulo Int_mod = Built-in "Int.mod" : Int -> Int -> Int; @@ -355,6 +360,12 @@ Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool; Elab_isconstructor = Built-in "Elab.isconstructor" : String -> Elab_Context -> Bool;

+%% +%% Check if a symbol is an inductive in a particular context +%% +Elab_isinductive = Built-in "Elab.isinductive" + : String -> Elab_Context -> Bool; + %% %% Check if the n'th field of a constructor is erasable %% If the constructor isn't defined it will always return false @@ -381,6 +392,20 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin %% Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int;

+%% +%% Get the position of a field in a constructor +%% It return -1 in case the field isn't defined +%% see pervasive.typer for a more convenient function +%% +Elab_ind-ctor-arg-pos' = Built-in "Elab.ind-ctor-arg-pos" : String -> String -> String -> Elab_Context -> Int; + +%% +%% Get the number of fields in a constructor +%% It return -1 in case the field isn't defined +%% see pervasive.typer for a more convenient function +%% +Elab_count-ctor-args' = Built-in "Elab.count-ctor-args" : String -> String -> Elab_Context -> Int; + %% %% Get the docstring associated with a symbol %%

===================================== btl/pervasive.typer ===================================== @@ -394,7 +394,7 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair;

-__.__ = +dot-impl = let mksel o f = let constructor = Sexp_node (Sexp_symbol "##datacons") (cons (Sexp_symbol "?") @@ -411,14 +411,15 @@ __.__ = (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); + in (lambda args -> + IO_return case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error); + +__.__ = macro dot-impl;

%% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) @@ -458,7 +459,8 @@ Not prop = prop -> False; %% 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_ ?ℓ)) +%% FIXME generalize typecons formal arguments +Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) (true (p ::: prop)) (false (p ::: Not prop));

%% Testing generalization in inductive type constructors. @@ -547,6 +549,32 @@ in case (Int_eq r (-1)) | true => (none) | false => (some r);

+%% +%% If `Elab_ind-ctor-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_ind-ctor-arg-pos a b c d = let + r = Elab_ind-ctor-arg-pos' a b c d; +in case (Int_eq r (-1)) + | true => (none) + | false => (some r); + +%% +%% If `Elab_count-ctor-args'` 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_count-ctor-args a b c = let + r = Elab_count-ctor-args' a b c; +in case (Int_eq r (-1)) + | true => (none) + | false => (some r); + %%%% %%%% Common library %%%% @@ -634,6 +662,15 @@ plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; %% _|_ = let lib = load "btl/polyfun.typer" in lib._|_;

+%% +%% records : a simple datatype when there is only one case +%% +define-operator "#" 200 (); +records = load "btl/records.typer"; +record = records.record; +__.__ = records.__.__; +_# = records._#; + %%%% Unit tests function for doing file

%% It's hard to do a primitive which execute test file

===================================== btl/records.typer ===================================== @@ -0,0 +1,82 @@ +record-impl : List Sexp -> IO Sexp; +record-impl args = + let + %% Get a name (symbol) from a sexp + %% - (name t) -> name + %% - name -> name + get-name : Sexp -> Sexp; + get-name sxp = + case Sexp_wrap sxp + | node op _ => get-name op + | symbol _ => sxp + | _ => Sexp_error; + + %% head is (Sexp_node type-name (arg list)) + name-args = List_head Sexp_error args; + fields = List_tail args; + + type-name = get-name name-args; + + %% Create the inductive type definition. + inductive = Sexp_node (Sexp_symbol "typecons") + (cons name-args + (cons (Sexp_node (Sexp_symbol "rec") fields) + nil)); + + decl = make-decl type-name inductive; + + in IO_return decl; + +record = macro record-impl; + +record-get-impl : List Sexp -> IO Sexp; +record-get-impl args = + let + get tc f idx nargs ectx = + let arg_pats : Sexp -> Int -> Int -> List Sexp; + arg_pats s i n = + if (Int_eq n 0) then nil + else (if (Int_eq i 0) + then (cons s (arg_pats s (i - 1) (n - 1))) + else (cons (Sexp_symbol "_") (arg_pats s (i - 1) (n - 1)))); + + pat = (Sexp_node (quote (datacons (uquote (Sexp_symbol tc)) rec)) + (arg_pats (Sexp_symbol "v") idx nargs)); + + branch = (quote ((uquote pat) => v)); + in + (quote (lambda rec -> (##case_ (_|_ rec (uquote branch))))); + + try-rec-get : List Sexp -> Elab_Context -> Option Sexp; + try-rec-get arg ectx = + case args + | (cons tc (cons f nil)) => + (case (Sexp_wrap tc, Sexp_wrap f) + | (symbol tcstr, symbol fstr) => + (case (Elab_count-ctor-args tcstr "rec" ectx, + Elab_ind-ctor-arg-pos tcstr "rec" fstr ectx) + | (some nargs, some idx) => some (get tcstr fstr idx nargs ectx) + | _ => none) + | _ => none) + | _ => none; + in + do { + ectx <- Elab_getenv (); + case try-rec-get args ectx + | some sxp => IO_return sxp + | _ => dot-impl args; %% Fallback on default dot implementation + }; + +__.__ = macro record-get-impl; + +record-make-impl : List Sexp -> IO Sexp; +record-make-impl args = + IO_return case args + | (cons tc nil) => (quote (datacons (uquote tc) rec)) + | _ => Sexp_error; + +_# = macro record-make-impl; %% I was going for a syntax close to + %% Erlang's, but the # doesn't separate + %% tokens ... Meh. + +record (Pair (a : Type) (b : Type)) (fst : a) (snd : a);

===================================== samples/decidable.typer ===================================== @@ -0,0 +1,168 @@ +False = Void; +True = Unit; + +% FIXME improved "case" fails with no branches +exfalso : False -> ?a; +exfalso f = ##case_ f; + +%type Decidable (prop : Type) +% | yes (p ::: prop) +% | no (p ::: Not prop); +yes = datacons Decidable true; +no = datacons Decidable false; + +typeclass Decidable; + +Eq_trans : + (x : ?t) => (y : ?t) => (a : ?t) -> + (ax : Eq a x) => (ay : Eq a y) => Eq x y; +Eq_trans a = + lambda (ax : Eq a x) (ay : Eq a y) => + Eq_cast (f := lambda ax -> Eq ax y) ay; + +Eq_cong : % not sure about levels here + (t : (Type_ ?ℓ)) ≡> (r : (Type_ ?ℓ)) ≡> + (x : t) ≡> (y : t) ≡> (p : (Eq x y)) ≡> + (f : (t -> r)) -> (Eq (f x) (f y)); +Eq_cong f = + Eq_cast (p := p) (f := lambda xy -> Eq (f x) (f xy)) Eq_refl; + +discriminate_nocheck = + macro (lambda args -> + case args + | cons x (cons y nil) => + do { + sd <- gensym (); + sp <- gensym (); + IO_return + (quote ((lambda (uquote sp) -> + (Eq_cast (p := (uquote sp)) + (f := (lambda (uquote sd) -> + (case uquote sd + | (uquote x) => True + | _ => False))) + ())) : Not (Eq (uquote x) (uquote y)))) + } + | _ => IO_return Sexp_error); + +discriminate = + macro (lambda args -> + case args + | cons x (cons y nil) => + (case (Sexp_wrap x, Sexp_wrap y) + | (symbol sx, symbol sy) => % FIXME get the constructor even when its a call + do { + env <- Elab_getenv (); + if (and (Elab_isconstructor sx env) + (and (Elab_isconstructor sy env) + (not (Sexp_eq x y)))) + then + Macro_expand discriminate_nocheck args + else (IO_return Sexp_error) + } + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error); + +test : (Not (Eq true false)); +test = discriminate true false; + +absurd = + lambda (p : ?prop) -> + lambda (contra : (Not ?prop)) -> + contra p; + +% We can't (usefully) have a `Decidable Bool` because it's +% impossible to have a `Not Bool`. Instead, we can decide boolean +% equality: + +decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b); +decideBoolEq = + lambda (a : Bool) (b : Bool) => + case (a, b) + | (false, false) => yes (p := Eq_trans false) + | (false, true) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate false true)) + | (true, false) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate true false)) + | (true, true) => yes (p := Eq_trans true); + +type Nat + | zero + | succ Nat; + +type even (a : Nat) + | eZ (p ::: Eq a zero) + | eSS (p :: even ?a) (pss ::: Eq a (succ (succ ?a))); + +decideEven : (a : Nat) => Decidable (even a); +decideEven = + lambda (a : Nat) => + case a + | zero => yes (p := eZ) + | succ zero => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ zero)) + | eSS => absurd (Eq_trans a) (discriminate_nocheck (succ (succ ?)) (succ zero))) + | succ (succ a') => + case (decideEven : Decidable (even a')) + | yes => yes (p := eSS) + | no => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ (succ ?))) + | eSS => absurd (? : even a') (? : Not (even a'))); + +type _<_ (a : Nat) (b : Nat) + | ltZ (pa ::: Eq a zero) (pb ::: Eq b (succ ?b)) + | ltS (p :: (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b)); + +decideLT : (a : Nat) => (b : Nat) => Decidable (a < b); +decideLT = + lambda a b => + case b + | zero => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?))) + | succ b' => + case a + | zero => yes (p := ltZ) + | succ a' => + case (decideLT : (Decidable (a' < b'))) + | yes => yes (p := ltS) + | no => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (? : (a' < b')) (? : Not (a' < b'))); + +define-operator "∧" 111 130; + +record ((a : Type) ∧ (b : Type)) (fst : a) (snd : b); + +decideAnd : (P : Type) ≡> (Q : Type) ≡> + (Decidable P) => (Decidable Q) => (Decidable (P ∧ Q)); +decideAnd = + lambda P Q ≡> + lambda (decP : Decidable P) (decQ : Decidable Q) => + case (decP, decQ) + | (yes (p := pP), yes (p := pQ)) => yes (p := _∧_ # pP pQ) + | (no (p := nP), _) => + no (p := (lambda (proofs : P ∧ Q) -> absurd (_∧_.fst proofs) nP)) + | (_, no (p := nQ)) => + no (p := (lambda (proofs : P ∧ Q) -> absurd (_∧_.snd proofs) nQ)); + +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 (instance () : (Decidable (uquote e1))) + | yes => uquote e2 + | no => uquote e3))); + +test2 : Bool; +test2 = if ((even (succ zero)) ∧ (zero < zero)) then false else true; +

===================================== samples/num_class.typer ===================================== @@ -0,0 +1,39 @@ +type Num (α : Type) + | mkNum (Num_+ : α -> α -> α) + (Num_- : α -> α -> α) + (Num_* : α -> α -> α) + (Num_/ : α -> α -> α); + +typeclass Num; + +_+_ = lambda numInst => case numInst | mkNum _+_ _ _ _ => _+_; +_-_ = lambda numInst => case numInst | mkNum _ _-_ _ _ => _-_; +_*_ = lambda numInst => case numInst | mkNum _ _ _*_ _ => _*_; +_/_ = lambda numInst => case numInst | mkNum _ _ _ _/_ => _/_; + +IntNum : Num Int; +IntNum = + mkNum (Num_+ := Int_+) (Num_- := Int_-) (Num_* := Int_*) (Num_/ := Int_/); + +IntegerNum : Num Integer; +IntegerNum = + mkNum (Num_+ := Integer_+) (Num_- := Integer_-) + (Num_* := Integer_*) (Num_/ := Integer_/); + +FloatNum : Num Float; +FloatNum = + mkNum (Num_+ := Float_+) (Num_- := Float_-) + (Num_* := Float_*) (Num_/ := Float_/); + +type FromInt (α : Type) + | mkFromInt (FromInt_fromInt : Int -> α); + +typeclass FromInt; + +fromInt = lambda fromIntInst => case fromIntInst | mkFromInt fromInt => fromInt; + +IntFromInt : FromInt Int; +IntFromInt = mkFromInt (lambda x -> x); + +IntegerFromInt : FromInt Integer; +IntegerFromInt = mkFromInt Int->Integer;

===================================== samples/num_class_recs.typer ===================================== @@ -0,0 +1,33 @@ +record (Num (α : Type)) + (_+_ : α -> α -> α) + (_-_ : α -> α -> α) + (_*_ : α -> α -> α) + (_/_ : α -> α -> α); + +typeclass Num; + +_+_ = lambda numInst => Num._+_ numInst; +_-_ = lambda numInst => Num._-_ numInst; +_*_ = lambda numInst => Num._*_ numInst; +_/_ = lambda numInst => Num._/_ numInst; + +IntNum : Num Int; +IntNum = Num # Int_+ Int_- Int_* Int_/; + +IntegerNum : Num Integer; +IntegerNum = Num # Integer_+ Integer_- Integer_* Integer_/; + +FloatNum : Num Float; +FloatNum = Num # Float_+ Float_- Float_* Float_/; + +record (FromInt (α : Type)) (fromInt : Int -> α); + +typeclass FromInt; + +fromInt = lambda fromIntInst => FromInt.fromInt fromIntInst; + +IntFromInt : FromInt Int; +IntFromInt = FromInt # (lambda x -> x); + +IntegerFromInt : FromInt Integer; +IntegerFromInt = FromInt # Int->Integer;

===================================== src/REPL.ml ===================================== @@ -135,8 +135,11 @@ let ierase_type (lexps: (ldecl list list * lexpr list)) =

let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in - let ldecls, lctx = Elab.lexp_p_decls pdecls lctx in + (* FIXME We take the parsed input here but we should take the + unparsed tokens directly instead *) + let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in let lexprs = Elab.lexp_parse_all pexprs lctx in + List.iter Elab.resolve_instances lexprs; List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) lexprs; (ldecls, lexprs), lctx @@ -164,8 +167,7 @@ let ieval f str ectx rctx = let raw_eval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in - let lxps, ectx = Elab.lexp_p_decls nods ectx in + let lxps, ectx = Elab.lexp_p_decls [] sxps ectx in let elxps = List.map OL.clean_decls lxps in (* At this point, `elxps` is a `(vname * elexp) list list`, where: * - each `(vname * elexp)` is a definition

===================================== src/builtin.ml ===================================== @@ -99,19 +99,6 @@ let dloc = DB.dloc let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, mkArrow (Anormal, (dloc, None), t, dloc, t))

-let type_eq = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - DB.type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) - let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx

(* Typer list as seen during runtime. *) @@ -161,7 +148,8 @@ let register_builtin_csts () = add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string; - add_builtin_cst "Elab_Context" DB.type_elabctx + add_builtin_cst "Elab_Context" DB.type_elabctx; + add_builtin_cst "Eq" DB.type_eq

let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in @@ -175,7 +163,6 @@ let register_builtin_types () = "Array" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type "FileHandle" DB.type0 in - let _ = new_builtin_type "Eq" type_eq in ()

let _ = register_builtin_csts ();

===================================== src/debruijn.ml ===================================== @@ -94,6 +94,20 @@ let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None) +let type_eq_type = + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + mkArrow (Aerasable, lv, + type_level, dloc, + mkArrow (Aerasable, tv, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 0), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 1), dloc, + mkSort (dloc, Stype (mkVar (lv, 3))))))) +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None) +

(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype) @@ -112,26 +126,29 @@ type meta_scope * lctx_length (* Length of ctx when the scope is added. *) * (meta_id SMap.t ref) (* Metavars already known in this scope. *)

+type typeclass_ctx + = (ltype * lctx_length) list (* FIXME make it a set of lexps ? *) + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * meta_scope + = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx

let get_size (ctx : elab_context) - = let (_, (n, _), lctx, _) = ctx in + = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n

let ectx_to_grm (ectx : elab_context) : Grammar.grammar = - let (grm,_, _, _) = ectx in grm + let (grm,_, _, _, _) = ectx in grm

(* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_,_, lctx, _) = ectx in lctx + let (_,_, lctx, _, _) = ectx in lctx

-let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level +let ectx_to_scope_level ((_, _, _, (sl, _, _), _) : elab_context) : scope_level = sl

-let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int +let ectx_local_scope_size ((_, (n, _), _, (_, slen, _), _) as ectx) : int = get_size ectx - slen

(* Public methods: DO USE @@ -142,7 +159,7 @@ let empty_lctx = M.nil

let empty_elab_context : elab_context = (Grammar.default_grammar, empty_senv, empty_lctx, - (0, 0, ref SMap.empty)) + (0, 0, ref SMap.empty), [])

(* senv_lookup caller were using Not_found exception *) exception Senv_Lookup_Fail of (string list) @@ -150,7 +167,7 @@ let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds)

(* Return its current DeBruijn index. *) let senv_lookup (name: string) (ctx: elab_context): int = - let (_, (n, map), _, _) = ctx in + let (_, (n, map), _, _, _) = ctx in try n - (SMap.find name map) - 1 with Not_found -> let get_related_names (n : db_ridx) name map = @@ -189,11 +206,11 @@ let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) =

let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, oname) = def in - let (grm, (n, map), env, sl) = ctx in + let (grm, (n, map), env, sl, tcctx) = ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), lexp_ctx_cons env def v t, - sl) + sl, tcctx)

let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t

@@ -207,28 +224,33 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = ctx

let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = - let (grm, (n, senv), lctx, sl) = ctx in + let (grm, (n, senv), lctx, sl, tcctx) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, oname), _, _) -> (match oname with None -> senv | Some name -> SMap.add name i senv), i + 1) (senv, n) defs in - (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) + (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl, tcctx)

let ectx_new_scope (ectx : elab_context) : elab_context = - let (grm, senv, lctx, (scope, _, rmmap)) = ectx in - (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap))) + let (grm, senv, lctx, (scope, _, rmmap), tcctx) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)), tcctx)

let ectx_get_scope (ectx : elab_context) : meta_scope = - let (_, _, _, sl) = ectx in sl + let (_, _, _, sl, _) = ectx in sl

let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = - let (grm, _, _, _) = ectx in grm + let (grm, _, _, _, _) = ectx in grm

let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx

+let env_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = + let (grm, senv, lctx, sl, tcctx) = ectx in + let ntcctx = ((t, get_size ectx) :: tcctx) in + (grm, senv, lctx, sl, ntcctx) + (* Print context *) let print_lexp_ctx_n (ctx : lexp_context) start = let n = (M.length ctx) - 1 in

===================================== src/debug_util.ml ===================================== @@ -138,8 +138,6 @@ let arg_defs = [ Arg.Unit (add_p_option "pretok"), " Print pretok debug info"); ("-tok", Arg.Unit (add_p_option "tok"), " Print tok debug info"); - ("-sexp", - Arg.Unit (add_p_option "sexp"), " Print sexp debug info"); ("-pexp", Arg.Unit (add_p_option "pexp"), " Print pexp debug info"); ("-lexp", @@ -152,7 +150,6 @@ let arg_defs = [ Arg.Unit (fun () -> add_p_option "pretok" (); add_p_option "tok" (); - add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" (); add_p_option "lctx" (); @@ -165,7 +162,6 @@ let parse_args () =

let make_default () = arg_print_options := SMap.empty; - add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" ()

@@ -176,10 +172,8 @@ let format_source () = let filename = List.hd (!arg_files) in let pretoks = prelex_file filename in let toks = lex default_stt pretoks in - let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) - toks (Some ";") in let ctx = Elab.default_ectx in - let lexps, _ = Elab.lexp_p_decls nodes ctx in + let lexps, _ = Elab.lexp_p_decls [] toks ctx in

print_string (make_sep '-'); print_string "\n";

@@ -235,26 +229,12 @@ let main () = print_string (make_title " Base Sexp"); debug_sexp_print_all toks; print_string "\n"));

- (* get node sexp *) - print_string yellow; - let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) - toks (Some ";") in - print_string reset; - - (if (get_p_option "sexp") then( - print_string (make_title " Node Sexp "); - debug_sexp_print_all nodes; print_string "\n")); - - (* Parse All Declaration *) - print_string yellow; - print_string reset; - (* get lexp *) let octx = Elab.default_ectx in

(* debug lexp parsing once merged *) print_string yellow; - let lexps, nctx = try Elab.lexp_p_decls nodes octx + let lexps, nctx = try Elab.lexp_p_decls [] toks octx with e -> print_string reset; raise e in

===================================== src/elab.ml ===================================== @@ -57,6 +57,7 @@ open Grammar module BI = Builtin

module Unif = Unification +module Inst = Instances

module OL = Opslexp module EL = Elexp @@ -257,6 +258,13 @@ let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.identity, name)

+let newInstanceMetavar (ctx : elab_context) name t = + let lctx = ectx_to_lctx ctx in + let sl = ectx_to_scope_level ctx in + let meta = Unif.create_metavar lctx sl t in + Inst.add_instance_metavar meta ctx (fst name); + mkMetavar (meta, S.identity, name) + let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level

@@ -280,8 +288,8 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | Symbol (_, "") -> None | Integer (_, n) -> Some n | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in - let (grm, a, b, c) = ctx in - (SMap.add name (level l, level r) grm, a, b, c) + let (grm, a, b, c, d) = ctx in + (SMap.add name (level l, level r) grm, a, b, c, d) | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ @@ -625,12 +633,83 @@ and get_implicit_arg ctx loc oname t = and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp_whnf t (ectx_to_lctx ctx) with + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass ctx t1 + -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in + instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (e, List.rev args), t) in instantiate t []

+and myers_filter_map_index (f : int -> 'a -> 'b option) (m : 'a M.myers) + : ('b M.myers) + = snd (M.fold_right + (fun x (i, l') -> + match (f i x) with + | Some y -> (i - 1, M.cons y l') + | None -> (i - 1, l')) + m (M.length m - 1, M.nil)) + +and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp option = + Log.log_debug ~loc ("Searching for t = `" ^ (lexp_string t) ^ "`"); + let ctx = ectx_new_scope ctx in + let lctx = (ectx_to_lctx ctx) in + let sl = (ectx_to_scope_level ctx) in + let env_elem_match (i : int) (elem : DB.env_elem) : (int * DB.env_elem * lexp * ltype) option = + let ((_, namopt), _, t') = elem in + let var = mkVar ((loc,namopt), i) in + let t' = mkSusp t' (S.shift (i + 1)) in + let (e, t') = instantiate_implicit var t' ctx in + (* All candidates should have a type that is a typeclass *) + if not (Inst.is_typeclass ctx t') then None else + match Inst.check_typeclass_match t t' lctx sl with + | (Impossible | Possible) -> None + (* | Possible -> None *) + | (Match) -> Some (i, elem, e, t') in + let candidates = + myers_filter_map_index env_elem_match lctx in + Log.log_debug ("Candidates for instance of type `" ^ lexp_string t ^ "`:") + ~print_action:(fun () -> + M.iter (fun (i, ((_, so),_,t'),_, _) -> + lalign_print_int i 4; + lalign_print_string (match so with | Some s -> s | None -> "<none>") 10; + print_endline (lexp_string t')) candidates); + match M.safe_car candidates with + | None -> None + | Some (i, (vname, _, t'),e,t) -> + let t' = mkSusp t' (S.shift (i + 1)) in + Log.log_debug ~loc + ("Found candidate at index " ^ (string_of_int i) ^ ": `" ^ + (lexp_string (Var (vname, i))) ^ " : " ^ (lexp_string t') ^ "`"); + Some e + +and resolve_instances e = + let (_, (fv_map, _)) = OL.fv e in + U.IMap.iter (fun i (sl, t, cl, vn) -> + match Inst.instance_metavar_lookup i with + | Some (ctx, loc) -> + (match search_instance ctx loc t with + | Some e -> Unif.associate i e; resolve_instances e + | None -> + error ~loc ("No instance found for type `" ^ (lexp_string t) ^ "`") + ) + | None -> () + ) fv_map + + +and resolve_instances_and_generalize ctx e = + resolve_instances e; + generalize ctx e + +and sdform_typeclass (ctx : elab_context) loc sargs _ot : elab_context = + match sargs with + | [se] -> + let (t, _) = infer se ctx in + Inst.add_typeclass ctx t + | _ + -> sexp_error loc "typeclass expects 1 argument"; ctx + and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated @@ -707,7 +786,8 @@ and check_inferred ctx e inferred_t t = -> lexp_error (lexp_location e) e ("Type mismatch(" ^ (match ck with | Unif.CKimpossible -> "impossible" - | Unif.CKresidual -> "residue") + | Unif.CKresidual -> "residue" + | _ -> failwith "impossible" ) ^ ")! Context expected:\n " ^ lexp_string t ^ "\nbut expression has type:\n " ^ lexp_string inferred_t ^ "\ncan't unify:\n " @@ -781,9 +861,36 @@ and check_case rtype (loc, target, ppatterns) ctx = (* 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 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 tkind = OL.get_type (ectx_to_lctx nctx) tltp' in + let tlevel = (match OL.lexp_whnf tkind (ectx_to_lctx nctx) with + | Sort (_, Stype l) -> l + | _ -> error "HMMM"; DB.level0) in + let head_lexp_type = OL.get_type (ectx_to_lctx nctx) head_lexp in + (match Unif.unify tltp' head_lexp_type (ectx_to_lctx nctx) with + | [] -> () + | constraints -> Log.log_error "Unification failed for case Eq"); + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlevel); (* Typelevel *) + (Aerasable, tltp'); (* Inductive type *) + (Anormal, tlxp'); (* Target lexp *) + (Anormal, head_lexp)]) (* Lexp of the branch head *) + 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' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in let lexp = check pexp rtype' nctx in @@ -864,6 +971,15 @@ 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) -> + (* This is not pretty :( *) + (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' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in @@ -946,11 +1062,13 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) - -> let larg = get_implicit_arg - ctx (match sargs with - | [] -> loc - | sarg::_ -> sexp_location sarg) - v arg_type in + -> let larg = if Inst.is_typeclass ctx arg_type + then newInstanceMetavar ctx (loc, v) arg_type + else get_implicit_arg + ctx (match sargs with + | [] -> loc + | sarg::_ -> sexp_location sarg) + v arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) | [], _ @@ -996,7 +1114,7 @@ and lexp_parse_inductive ctors ctx = (fun (ak, n, t) aa -> Arrow (ak, n, t, dummy_location, aa)) acc impossible in - let g = generalize nctx altacc in + let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t l e -> Arrow (Aerasable, vname, t, l, e)) altacc in @@ -1110,9 +1228,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* FIXME: Generalize when/where possible, so things like `map` can be defined without type annotations! *) (* Preserve the new operators added to nctx. *) - let ectx = let (_, a, b, c) = ectx in - let (grm, _, _, _) = nctx in - (grm, a, b, c) in + let ectx = let (_, a, b, c, _) = ectx in + let (grm, _, _, _, tcctx) = nctx in + (grm, a, b, c, tcctx) in let (declmap, nctx) = List.fold_right (fun ((l, vname), pexp) (map, nctx) -> @@ -1122,10 +1240,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) | (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 (grm, ec, lc, sl, tcctx) = 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)) + (grm, ec, Myers.set_nth i d lc, sl, tcctx)) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -1161,7 +1279,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in - let g = generalize nctx (strip_rettype t) in + let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e -> mkArrow (Aerasable, name, t, l, e)) t @@ -1169,7 +1287,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in - let g = generalize nctx e in + let g = resolve_instances_and_generalize nctx e in let e' = g (fun ne vname t l e -> mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e)) @@ -1181,142 +1299,162 @@ and infer_and_generalize_def (ctx : elab_context) se = (e', t')

and lexp_decls_1 - (sdecls : sexp list) + (sdecls : sexp list) (* What's already parsed *) + (tokens : token list) (* Rest of input *) (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : location SMap.t) (* Pending type decls. *) (pending_defs : (symbol * sexp) list) (* Pending definitions. *) - : (vname * lexp * ltype) list * sexp list * elab_context = - - let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = - match sdecls with - | [] -> (if not (SMap.is_empty pending_decls) then - let (s, loc) = SMap.choose pending_decls in - error ~loc ("Variable `" ^ s ^ "` declared but not defined!") - else - assert (pending_defs == [])); - [], [], nctx - - | Symbol (_, "") :: sdecls - -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - | Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls - -> lexp_decls_1 (List.append sdecls' sdecls) - ectx nctx pending_decls pending_defs - - | Node (Symbol (loc, "_:_"), args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in - if SMap.mem vname pending_decls then - (* Don't burp: take'em all and unify! *) - let pt_idx = senv_lookup vname nctx in - (* Take the previous type annotation. *) - let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> Log.internal_error "Var not found at its index!" in - (* Unify it with the new one. *) - let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with - | (_::_) - -> lexp_error loc ltp - ("New type annotation `" - ^ lexp_string ltp ^ "` incompatible with previous `" - ^ lexp_string pt ^ "`") - | [] -> () in - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - else if List.exists (fun ((_, vname'), _) -> vname = vname') - pending_defs then - (error ~loc ("Variable `" ^ vname ^ "` already defined!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else lexp_decls_1 sdecls ectx - (ectx_extend nctx (loc, Some vname) ForwardRef ltp) - (SMap.add vname loc pending_decls) - pending_defs - | _ -> error ~loc "Invalid type declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | Node (Symbol (l, "_=_") as head, args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol ((l, vname)); sexp] - when SMap.is_empty pending_decls - -> assert (pending_defs == []); - (* Used to be true before we added define-operator. *) - (* assert (ectx == nctx); *) - let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in - (* Lexp decls are always recursive, so we have to shift by 1 to - * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, - ctx_define nctx var lexp ltp - - | [Symbol (l, vname); sexp] - -> if SMap.mem vname pending_decls then - let decl_loc = SMap.find vname pending_decls in - let v = ({file = l.file; - line = l.line; - column = l.column; - docstr = String.concat "\n" [decl_loc.docstr; l.docstr]}, - vname) in - let pending_decls = SMap.remove vname pending_decls in - let pending_defs = ((v, sexp) :: pending_defs) in - if SMap.is_empty pending_decls then - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, sdecls, nctx - else - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - else - (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | [Node (Symbol s, args) as d; body] - -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - lexp_decls_1 ((Node (head, - [Symbol s; - Node (Symbol (sexp_location d, "lambda_->_"), - [sexp_u_list args; body])])) - :: sdecls) - ectx nctx pending_decls pending_defs - - | _ -> error ~loc:l "Invalid definition syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - - | Node (Symbol (l, "define-operator"), args) :: sdecls - (* FIXME: Move this to a "special form"! *) - -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) - pending_decls pending_defs - - | Node (Symbol ((l, _) as v), sargs) :: sdecls - -> (* expand macro and get the generated declarations *) - let sdecl' = lexp_decls_macro v sargs nctx in - lexp_decls_1 (sdecl' :: sdecls) ectx nctx - pending_decls pending_defs - - | sexp :: sdecls - -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + : (vname * lexp * ltype) list * sexp list * token list * elab_context = + + let rec lexp_decls_1 sdecls tokens nctx pending_decls pending_defs = + let sdecl, sdecls, toks = + match (sdecls, tokens) with + | (s :: sdecls, _) -> Some s, sdecls, tokens + | ([], []) -> None, [], [] + | ([], _) -> + Log.log_debug "Parsing the next declaration sexp"; + let (s, toks) = sexp_parse_all (ectx_get_grammar nctx) + tokens (Some ";") in + Log.log_debug ("Parsed decl : `" ^ (sexp_string s) ^ "`"); + Some s, [], toks in + let recur prepend_sdecls nctx pending_decls pending_defs = + lexp_decls_1 (List.append prepend_sdecls sdecls) + toks nctx pending_decls pending_defs in + match sdecl with + | None -> (if not (SMap.is_empty pending_decls) then + let (s, loc) = SMap.choose pending_decls in + error ~loc ("Variable `" ^ s ^ "` declared but not defined!") + else + assert (pending_defs == [])); + [], [], [], nctx + + | Some (Symbol (_, "")) + -> recur [] nctx pending_decls pending_defs + + | Some (Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls')) + -> recur sdecls' nctx pending_decls pending_defs + + | Some (Node (Symbol (loc, "_:_"), args) as thesexp) + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol (loc, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in + if SMap.mem vname pending_decls then + (* Don't burp: take'em all and unify! *) + let pt_idx = senv_lookup vname nctx in + (* Take the previous type annotation. *) + let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with + | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) + | _ -> Log.internal_error "Var not found at its index!" in + (* Unify it with the new one. *) + let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with + | (_::_) + -> lexp_error loc ltp + ("New type annotation `" + ^ lexp_string ltp ^ "` incompatible with previous `" + ^ lexp_string pt ^ "`") + | [] -> () in + recur [] nctx pending_decls pending_defs + else if List.exists (fun ((_, vname'), _) -> vname = vname') + pending_defs then + (error ~loc ("Variable `" ^ vname ^ "` already defined!"); + recur [] nctx pending_decls pending_defs) + else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + (SMap.add vname loc pending_decls) + pending_defs + | _ -> error ~loc ("Invalid type declaration syntax : `" ^ + (sexp_string thesexp) ^ "`"); + recur [] nctx pending_decls pending_defs) + + | Some (Node (Symbol (l, "_=_") as head, args) as thesexp) + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol ((l, vname)); sexp] + when SMap.is_empty pending_decls + -> assert (pending_defs == []); + (* Used to be true before we added define-operator. *) + (* assert (ectx == nctx); *) + let (lexp, ltp) = infer_and_generalize_def nctx sexp in + let var = (l, Some vname) in + (* Lexp decls are always recursive, so we have to shift by 1 to + * account for the extra var (ourselves). *) + [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, + ctx_define nctx var lexp ltp + + | [Symbol (l, vname); sexp] + -> if SMap.mem vname pending_decls then + let decl_loc = SMap.find vname pending_decls in + let v = ({file = l.file; + line = l.line; + column = l.column; + docstr = String.concat "\n" [decl_loc.docstr; + l.docstr]}, + vname) in + let pending_decls = SMap.remove vname pending_decls in + let pending_defs = ((v, sexp) :: pending_defs) in + if SMap.is_empty pending_decls then + let nctx = ectx_new_scope nctx in + let decls, nctx = lexp_check_decls ectx nctx pending_defs in + decls, sdecls, toks, nctx + else + recur [] nctx pending_decls pending_defs + + else + (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); + recur [] nctx pending_decls pending_defs) + + | [Node (Symbol s, args) as d; body] + -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) + recur [Node (head, + [Symbol s; + Node (Symbol (sexp_location d, "lambda_->_"), + [sexp_u_list args; body])])] + nctx pending_decls pending_defs + + | _ -> error ~loc:l ("Invalid definition syntax : `" ^ + (sexp_string thesexp) ^ "`"); + recur [] nctx pending_decls pending_defs) + + | Some (Node (Symbol (l, "define-operator"), args)) + (* FIXME: Move this to a "special form"! *) + -> recur [] (sdform_define_operator nctx l args None) + pending_decls pending_defs + + | Some (Node (Symbol ((l, _) as v), sargs)) + -> (* expand macro and get the generated declarations *) + let sdecl' = lexp_decls_macro v sargs nctx in + recur [sdecl'] nctx pending_decls pending_defs + + | Some sexp + -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; + recur [] nctx pending_decls pending_defs

in (EV.set_getenv nctx; - let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in + let res = lexp_decls_1 sdecls tokens nctx + pending_decls pending_defs in (Log.stop_on_error (); res))

-and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) +and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = - let impl sdecls ctx = match sdecls with - | [] -> [], ectx_new_scope ctx - | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in - let declss, nnctx = lexp_p_decls sdecls nctx in - decls :: declss, nnctx in - let res = impl sdecls ctx in (Log.stop_on_error (); res) + let rec impl sdecls tokens ctx = + match (sdecls, tokens) with + | ([], []) -> [], ectx_new_scope ctx + | _ -> + let decls, sdecls, tokens, nctx = + lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in + Log.stop_on_error (); + let declss, nnctx = impl sdecls tokens nctx in + decls :: declss, nnctx in + impl sdecls tokens ctx

and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = + Eval.set_getenv ctx; let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in (Log.stop_on_error (); res)

and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = + Eval.set_getenv ctx; let e, _ = infer e ctx in (Log.stop_on_error (); e)

(* -------------------------------------------------------------------------- @@ -1641,10 +1779,21 @@ let rec sform_lambda kind ctx loc sargs ot = -> (match olt1 with | None -> () | Some lt1' - -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1') - then lexp_error (lexp_location lt1') lt1' - ("Type mismatch! Context expected `" - ^ lexp_string lt1 ^ "`")); + -> (match Unif.unify lt1' lt1 (ectx_to_lctx ctx) with + | ((ck, _ctx, t1, t2)::_) + -> lexp_error (lexp_location lt1') lt1' + ("Type mismatch(" + ^ (match ck with | Unif.CKimpossible -> "impossible" + | Unif.CKresidual -> "residue" + | _ -> failwith "impossible") + ^ ")! Context expected:\n " + ^ lexp_string lt1 ^ "\nbut parameter has type:\n " + ^ lexp_string lt1' ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p (ectx_to_lctx ctx) lt1' lt1)) + | [] -> ())); mklam lt1 (Some lt2)

| Arrow (ak2, v, lt1, _, lt2) when kind = Anormal @@ -1695,7 +1844,7 @@ let rec sform_case ctx loc sargs ot = match sargs with

let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] - -> let declss, nctx = lexp_p_decls [sdecls] ctx in + -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in (* FIXME: Use `elaborate`. *) let bdy, ltp = infer sbody (ectx_new_scope nctx) in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in @@ -1772,9 +1921,7 @@ let sform_load usr_elctx loc sargs ot = let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) - sxps (Some ";") in - let _, elctx = lexp_p_decls nods elctx + let _, elctx = lexp_p_decls [] sxps elctx in elctx in

(* read file as elab_context *) @@ -1810,6 +1957,22 @@ let sform_load usr_elctx loc sargs ot =

(tuple',Lazy)

+(** + Draft of a special form "instance" that gets refers to a variable + of the requested type in the context. + **) +let sform_instance ctx loc sargs ot = + match sargs, ot with + | ([se; _], _) -> (* Dummy param to trigger the special form *) + let t = infer_type se ctx (loc, None) in + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Inferred t) + | ([_], Some t) -> (* Dummy param to trigger the special form *) + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Checked) + | _ -> (sexp_error loc "##instance expects a type argument if not checked"; + sform_dummy_ret ctx loc) + (* Register special forms. *) let register_special_forms () = List.iter add_special_form @@ -1839,6 +2002,7 @@ let register_special_forms () = (* FIXME: These should be functions! *) ("decltype", sform_decltype); ("declexpr", sform_declexpr); + ("instance", sform_instance); ]

(* Default context with builtin types @@ -1860,9 +2024,7 @@ let default_ectx let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) - sxps (Some ";") in - let _, lctx = lexp_p_decls nods elctx + let _, lctx = lexp_p_decls [] sxps elctx in lctx in

(* Register predef *) @@ -1922,10 +2084,8 @@ let lexp_expr_str str ctx =

let lexp_decl_str str ctx = try let tenv = default_stt in - let grm = ectx_get_grammar ctx in - let limit = Some ";" in - let sdecls = sexp_parse_str str tenv grm limit in - lexp_p_decls sdecls ctx + let tokens = lex_str str tenv in + lexp_p_decls [] tokens ctx with Log.Stop_Compilation s -> ([],ctx)

===================================== src/env.ml ===================================== @@ -167,6 +167,41 @@ let make_runtime_ctx = M.nil

let get_rte_size (ctx: runtime_env): int = M.length ctx

+let print_myers_list l print_fun start = + let n = (M.length l) - 1 in + print_string (make_title " ENVIRONMENT "); + make_rheader [(None, "INDEX"); + (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; + print_string (make_sep '-'); + + for i = start to n do + print_string " | "; + ralign_print_int (n - i) 5; + print_string " | "; + print_fun (M.nth (n - i) l); + done; + print_string (make_sep '=') + +let print_rte_ctx_n (ctx: runtime_env) start = + print_myers_list + ctx + (fun (n, vref) -> + let g = !vref in + let _ = + match n with + | (_, Some m) -> lalign_print_string m 12; print_string " | " + | _ -> print_string (make_line ' ' 12); print_string " | " in + + value_print g; print_string "\n") start + +(* Only print user defined variables *) +let print_rte_ctx ctx = + print_rte_ctx_n ctx (!L.builtin_size) + +(* Dump the whole context *) +let dump_rte_ctx ctx = + print_rte_ctx_n ctx 0 + let get_rte_variable (name: vname) (idx: int) (ctx: runtime_env): value_type = try ( @@ -177,7 +212,7 @@ let get_rte_variable (name: vname) (idx: int) if n1 = n2 then x else ( - fatal + fatal ~print_action:(fun () -> dump_rte_ctx ctx) ("Variable lookup failure. Expected: "" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """)))

@@ -212,37 +247,3 @@ let nfirst_rte_var n ctx = List.rev acc in loop 0 []

-let print_myers_list l print_fun start = - let n = (M.length l) - 1 in - print_string (make_title " ENVIRONMENT "); - make_rheader [(None, "INDEX"); - (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; - print_string (make_sep '-'); - - for i = start to n do - print_string " | "; - ralign_print_int (n - i) 5; - print_string " | "; - print_fun (M.nth (n - i) l); - done; - print_string (make_sep '=') - -let print_rte_ctx_n (ctx: runtime_env) start = - print_myers_list - ctx - (fun (n, vref) -> - let g = !vref in - let _ = - match n with - | (_, Some m) -> lalign_print_string m 12; print_string " | " - | _ -> print_string (make_line ' ' 12); print_string " | " in - - value_print g; print_string "\n") start - -(* Only print user defined variables *) -let print_rte_ctx ctx = - print_rte_ctx_n ctx (!L.builtin_size) - -(* Dump the whole context *) -let dump_rte_ctx ctx = - print_rte_ctx_n ctx 0

===================================== src/eval.ml ===================================== @@ -744,6 +744,14 @@ let constructor_p name ectx = | _ -> false with Senv_Lookup_Fail _ -> false

+let inductive_p name ectx = + try let idx = senv_lookup name ectx in + match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with + | Inductive _ -> true + | _ -> false + with Senv_Lookup_Fail _ -> false + let erasable_p name nth ectx = let is_erasable ctors = match (smap_find_opt name ctors) with | (Some args) -> @@ -821,10 +829,43 @@ let ctor_arg_pos name arg ectx = | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)

+let ind_ctor_arg_pos indname ctorname arg ectx = + let rec find_opt xs n = match xs with + | [] -> None + | (_, (_, Some x), _)::xs -> if x = arg then Some n else find_opt xs (n + 1) + | _::xs -> find_opt xs (n + 1) in + try let idx = senv_lookup indname ectx in + match OL.lexp_whnf (mkVar ((dummy_location, Some indname), idx)) + (ectx_to_lctx ectx) with + | Inductive (_, _, _, ctors) -> + (match smap_find_opt ctorname ctors with + | (Some args) -> + (match (find_opt args 0) with + | None -> (-1) + | Some n -> n) + | _ -> (-1)) + | _ -> (-1) + with Senv_Lookup_Fail _ -> (-1) + +let count_ctor_args indname ctorname ectx = + try let idx = senv_lookup indname ectx in + match OL.lexp_whnf (mkVar ((dummy_location, Some indname), idx)) + (ectx_to_lctx ectx) with + | Inductive (_,_,_,ctors) -> + (match smap_find_opt ctorname ctors with + | Some args -> List.length args + | None -> (-1)) + | _ -> (-1) + with Senv_Lookup_Fail _ -> (-1) + let is_constructor loc depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx) | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments"

+let is_inductive loc depth args_val = match args_val with + | [Vstring name; Velabctx ectx] -> o2v_bool (inductive_p name ectx) + | _ -> error loc "Elab.isinductive takes a String and an Elab_Context as arguments" + let is_nth_erasable loc depth args_val = match args_val with | [Vstring name; Vint nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name nth_arg ectx) | _ -> error loc "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments" @@ -841,6 +882,14 @@ let arg_pos loc depth args_val = match args_val with | [Vstring t; Vstring a; Velabctx ectx] -> Vint (ctor_arg_pos t a ectx) | _ -> error loc "Elab.arg-pos takes two String and an Elab_Context as arguments"

+let ind_ctor_arg_pos loc depth args_val = match args_val with + | [Vstring ind; Vstring ctor; Vstring field; Velabctx ectx] -> Vint (ind_ctor_arg_pos ind ctor field ectx) + | _ -> error loc "Elab.ind-ctor-arg-pos takes three String and an Elab_Context as arguments" + +let count_ctor_args loc depth args_val = match args_val with + | [Vstring ind; Vstring ctor; Velabctx ectx] -> Vint (count_ctor_args ind ctor ectx) + | _ -> error loc "Elab.count-ctor-args takes two String and an Elab_Context as arguments" + let array_append loc depth args_val = match args_val with | [v; Varray a] -> Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v)) @@ -996,10 +1045,13 @@ let register_builtin_functions () = ("Elab.debug-doc", debug_doc, 2); ("Elab.isbound" , is_bound, 2); ("Elab.isconstructor", is_constructor, 2); + ("Elab.isinductive", is_inductive, 2); ("Elab.is-nth-erasable", is_nth_erasable, 3); ("Elab.is-arg-erasable", is_arg_erasable, 3); ("Elab.nth-arg" , nth_arg, 3); ("Elab.arg-pos" , arg_pos, 3); + ("Elab.ind-ctor-arg-pos", ind_ctor_arg_pos, 4); + ("Elab.count-ctor-args", count_ctor_args, 3); ("Array.append" , array_append,2); ("Array.create" , array_create,2); ("Array.length" , array_length,1);

===================================== src/instances.ml ===================================== @@ -0,0 +1,61 @@ +module Unif = Unification +module U = Util +module DB = Debruijn +module L = Lexp +module S = Subst +module OL = Opslexp + +(* FIXME Is it possible to have multiple references to the same + instance metavar? It would break the following code *) +let instance_metavar_table = ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) +let instance_metavar_lookup (id : L.meta_id) : (DB.elab_context * U.location) option + = U.IMap.find_opt id (!instance_metavar_table) +let add_instance_metavar (id : L.meta_id) (ctx : DB.elab_context) (loc : U.location) : unit + = instance_metavar_table := U.IMap.add id (ctx, loc) !instance_metavar_table + +let env_is_typeclass (ectx : DB.elab_context) (t : L.ltype) : bool = + let (_, _, _, _, tcctx) = ectx in + let cl = DB.get_size ectx in + List.exists (fun (t', cl') -> + let i = cl - cl' in + let t' = L.mkSusp t' (S.shift i) in + OL.conv_p (DB.ectx_to_lctx ectx) t t' + (*(Unif.unify ~checking:(max_int (* FIXME *)) t t' (DB.ectx_to_lctx ectx)) = []*) + ) tcctx + + +let get_ind (lctx : DB.lexp_context) (t : L.ltype) : L.ltype option = + match OL.lexp_whnf t lctx with + | L.Call (typecons, _) -> + (match OL.lexp_whnf typecons lctx with + | L.Inductive _ as ind -> Some ind + | _ -> None + ) + | L.Inductive _ as ind -> Some ind + | _ -> None + + +let is_typeclass (ctx : DB.elab_context) (t : L.ltype) = + let lctx = DB.ectx_to_lctx ctx in + match get_ind lctx t with + | Some ind -> env_is_typeclass ctx ind + | None -> false + +let add_typeclass (ctx : DB.elab_context) (t : L.ltype) : DB.elab_context = + let lctx = DB.ectx_to_lctx ctx in + match get_ind lctx t with + | Some ind -> DB.env_add_typeclass ctx ind + | None -> Log.log_error ("Failed to add type class to context " + ^ " because it is not an inductive : `" + ^ (L.lexp_string t) ^ "`"); ctx + +type match_res = Impossible | Possible | Match + +let check_typeclass_match t1 t2 lctx sl = + match Unif.unify ~checking:sl t1 t2 lctx with + | [] -> Match + | constraints when List.exists (function | (Unif.CKimpossible,_,_,_) -> true + | _ -> false) + constraints -> Impossible + | _ -> Possible +

===================================== src/log.ml ===================================== @@ -133,11 +133,13 @@ let print_entry entry = let log_entry (entry : log_entry) = if (entry.level <= typer_log_config.level) then ( - log_push entry; - if (typer_log_config.print_at_log) + if (typer_log_config.print_at_log || + entry.level >= Debug) then (print_entry entry; flush stdout) + else + log_push entry )

let count_msgs (lvlp : log_level -> bool) =

===================================== src/myers.ml ===================================== @@ -54,11 +54,21 @@ let car l = | Mnil -> raise Not_found | Mcons (x, _, _, _) -> x

+let safe_car l = + match l with + | Mnil -> None + | Mcons (x, _, _, _) -> Some x + let cdr l = match l with | Mnil -> Mnil | Mcons (_, l, _, _) -> l

+let safe_cdr l = + match l with + | Mnil -> None + | Mcons (_, l, _, _) -> Some l + let case l n c = match l with | Mnil -> n () @@ -136,3 +146,6 @@ let rec fold_right f l i = match l with let map f l = fold_right (fun x l' -> cons (f x) l') l nil

let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l + +let iter (f : 'a -> unit) (l : 'a myers) : unit + = fold_left (fun _ x -> f x; ()) () l

===================================== src/opslexp.ml ===================================== @@ -166,7 +166,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = d + 1)) (S.identity, 0) aargs in - lexp_whnf (push_susp branch subst) ctx + lexp_whnf (push_susp branch (S.mkShift subst 1)) ctx (* FIXME not sure about the subt here *) with Not_found -> match default with | Some (v,default) @@ -610,9 +610,9 @@ let rec check'' erased ctx e = SMap.iter (fun name (l, vdefs, branch) -> let fieldtypes = SMap.find name constructors in - let rec mkctx erased ctx s vdefs fieldtypes = + let rec mkctx erased ctx s hlxp vdefs fieldtypes = match vdefs, fieldtypes with - | [], [] -> (erased, ctx) + | [], [] -> (erased, ctx, s, hlxp) (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes @@ -620,14 +620,27 @@ let rec check'' erased ctx e = (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) (S.cons (mkVar (vdef, 0)) (S.mkShift s 1)) + (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; - (erased, ctx)) in - let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in + (erased, ctx, s, hlxp)) in + let (nerased, nctx, subst, hlxp) = + mkctx erased ctx s (mkCons (it, (l, name))) vdefs fieldtypes in + (* Create Eq type between target and lexp matching the + branch head, and add it (erasable) to the context *) + let tlxp = mkSusp e subst in + let tltp = mkSusp etype subst in + let eqty = mkCall (DB.type_eq, + [(Aerasable, DB.type0); (* Typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, tlxp); (* Target lexp *) + (Anormal, hlxp)]) in (* Lexp of the branch head *) + let nerased = dbset_push Aerasable nerased in + let nctx = DB.lexp_ctx_cons nctx (l, None) Variable eqty in assert_type nctx branch (check nerased nctx branch) - (mkSusp ret (S.shift (List.length fieldtypes)))) + (mkSusp ret (S.shift ((List.length fieldtypes) + 1)))) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -723,6 +736,7 @@ module LMap = Hashtbl.Make (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) let fv_memo = LMap.create 1000 +let fv_flush () = LMap.clear fv_memo

let fv_empty = (DB.set_empty, mv_set_empty) let fv_union (fv1, mv1) (fv2, mv2)

===================================== src/sexp.ml ===================================== @@ -160,13 +160,10 @@ let rec sexp_parse (g : grammar) (rest : sexp list) mk_node ((l,"")::op) largs rargs true), rest) | (Some ll, None) when ll > level - (* A closer without matching opener. - * It might simply be a postfix symbol that binds very tightly. - * We currently signal an error because it's more common for - * it to be a closer with missing opener. *) - -> sexp_error l ("Lonely postfix/closer ""^name^"""); - sexp_parse rest' level op largs - [mk_node [(l,name);(l,"")] [] rargs true] + (* A closer without matching opener or it might simply be + * a postfix symbol that binds very tightly. *) + -> sexp_parse rest' level op largs + [mk_node [(l,name);(l,"")] [] rargs true] | (Some ll, Some rl) when ll > level (* A new infix which binds more tightly, i.e. does not close * the current `op' but takes its `rargs' instead. *)

===================================== src/unification.ml ===================================== @@ -46,6 +46,7 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) | CKresidual (* We failed to find a unifier. *) + | CKassoc (* Couldn't associate because of checking mode *) (* FIXME: Each constraint should additionally come with a description of how it relates to its "top-level" or some other info which might let us fix the problem (e.g. by introducing coercions). *) @@ -54,8 +55,9 @@ type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list type return_type = constraints

(** Alias for VMap.add*) -let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst - = U.IMap.add id (MVal lxp) subst +let associate (id: meta_id) (lxp: lexp) : unit + = metavar_table := U.IMap.add id (MVal lxp) (!metavar_table); + OL.fv_flush ()

let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | MVal _ -> Log.internal_error @@ -174,13 +176,15 @@ let rec s_offset s = match s with

The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) *) -let rec unify (e1: lexp) (e2: lexp) +let rec unify ?checking + (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) : return_type = - unify' e1 e2 ctx OL.set_empty + unify' e1 e2 ctx OL.set_empty checking

and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) + (c : scope_level option) (* checking mode scope level *) : return_type = if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in @@ -190,20 +194,26 @@ and unify' (e1: lexp) (e2: lexp) if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (e1', e2') with - | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _)) + | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] - | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l - | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> unify_call r l ctx vs' - (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ as l, r) -> unify_arrow l r ctx vs' - | (Lambda _ as l, r) -> unify_lambda l r ctx vs' - | (Call _ as l, r) -> unify_call l r ctx vs' - (* | (Case _ as l, r) -> unify_case l r subst *) - (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _ as l, r) -> unify_sort l r ctx vs' - | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' + | (l, (Metavar (idx, s, _) as r)) -> unify_metavar c ctx idx s r l + | ((Metavar (idx, s, _) as l), r) -> unify_metavar c ctx idx s l r + | (l, (Call _ as r)) -> unify_call c r l ctx vs' + | ((Call _ as l), r) -> unify_call c l r ctx vs' + | (l, (Var _ as r)) -> unify_var r l ctx vs' + | ((Var _ as l), r) -> unify_var l r ctx vs' + | (l, (Arrow _ as r)) -> unify_arrow c r l ctx vs' + | ((Arrow _ as l), r) -> unify_arrow c l r ctx vs' + | (l, (Lambda _ as r)) -> unify_lambda c r l ctx vs' + | ((Lambda _ as l), r) -> unify_lambda c l r ctx vs' + (* | (l, (Case _ as r)) -> unify_case r l subst *) + (* | ((Case _ as l), r) -> unify_case l r subst *) + (* | (l, (Inductive _ as r)) -> unify_induct r l subst *) + (* | ((Inductive _ as l), r) -> unify_induct l r subst *) + | (l, (Sort _ as r)) -> unify_sort c r l ctx vs' + | ((Sort _ as l), r) -> unify_sort c l r ctx vs' + | (l, (SortLevel _ as r)) -> unify_sortlvl c r l ctx vs' + | ((SortLevel _ as l), r) -> unify_sortlvl c l r ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -211,7 +221,7 @@ and unify' (e1: lexp) (e2: lexp) * ^ " and " * ^ snd label2 * ^ "\n"); *) - unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2 + unify_inductive c ctx vs' args1 args2 consts1 consts2 e1 e2 | _ -> (if OL.conv_p ctx e1' e2' then [] else ((* print_string "Unification failure on default\n"; *) [(CKresidual, ctx, e1, e2)])) @@ -222,87 +232,77 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) else None - - (Arrow, Var) -> Constraint - (_, _) -> None *) -and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs +and unify_arrow (checking : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then (unify' ltype1 ltype2 ctx vs) + then (unify' ltype1 ltype2 ctx vs checking) @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) - else [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)]) - | (Arrow _, _) -> unify' lxp arrow ctx vs + (OL.set_shift vs) checking) + else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]

(** Unify a Lambda and a lexp if possible - - Lamda , Lambda -> if var_kind = var_kind + - Lambda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - - Lambda , Var -> CONSTRAINT - - Lambda , Call -> Constraint - - Lambda , Let -> Constraint - - Lambda , lexp -> unify lexp lambda subst + - Lambda , _ -> Impossible *) -and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = +and unify_lambda (checking : scope_level option) (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then (unify' ltype1 ltype2 ctx vs) + then (unify' ltype1 ltype2 ctx vs checking) @(unify' lexp1 lexp2 (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) + (OL.set_shift vs) checking) else [(CKimpossible, ctx, lambda, lxp)] - | ((Lambda _, Var _) - | (Lambda _, Let _) - | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)] - | (Lambda _, Arrow _) - | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)] - | (Lambda _, _) -> unify' lxp lambda ctx vs - | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] + | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

(** Unify a Metavar and a lexp if possible - - lexp , {metavar <-> none} -> UNIFY - - lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] - - metavar , metavar -> if Metavar = Metavar then OK else ERROR - - metavar , lexp -> OK + - metavar , metavar -> if Metavar = Metavar then intersect + - metavar , metavar -> inverse subst (both sides) + - metavar , lexp -> inverse subst *) -and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) +and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = - let t = match metavar_lookup idx with + let t, sl = match metavar_lookup idx with | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" - | MVar (_, t, _) -> push_susp t s in + | MVar (_, t, sl) -> push_susp t s, sl in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> log_info ?loc:None ("Unification of metavar failed:\n " - ^ "?[" ^ subst_string s ^ "]" - ^ "\nAgainst:\n " - ^ lexp_string lxp ^ "\n"); + -> log_info ~loc:(lexp_location lxp) + ("Unification of metavar failed:\n " + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' - -> metavar_table := associate idx lxp' (!metavar_table); - match unify t (OL.get_type ctx lxp) ctx with - | [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> log_info ?loc:None - ("Unification of metavar type failed:\n " - ^ lexp_string t ^ " != " - ^ lexp_string (OL.get_type ctx lxp) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - [(CKresidual, ctx, lxp1, lxp2)] in + -> match checking with + | Some l when l >= sl -> [(CKassoc, ctx, lxp1, lxp2)] + | _ -> ( + associate idx lxp'; + match unify t (OL.get_type ctx lxp) ctx with + | [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + [(CKresidual, ctx, lxp1, lxp2)]) in match lxp2 with | Metavar (idx2, s2, name) - -> if idx = idx2 then + -> if idx = idx2 && checking == None then match common_subset ctx s1 s2 with | S.Identity 0 -> [] (* Optimization! *) (* ¡ s1 != s2 ! @@ -353,7 +353,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) * ^ "\n =\n " * ^ subst_string (scompose s s2) * ^ "\n"); *) - metavar_table := associate idx lexp (!metavar_table); + associate idx lexp; assert (OL.conv_p ctx lxp1 lxp2); [] else @@ -364,18 +364,28 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> unif idx2 s2 lxp1) | _ -> unif idx s1 lxp2

+(** Unify a Var (var) and a lexp (lxp) + - Var , Var -> IF same var THEN ok ELSE constraint + - Var , lexp -> Constraint +*) +and unify_var (var: lexp) (lxp: lexp) ctx vs + : return_type = + match (var, lxp) with + | (Var _, Var _) when OL.conv_p ctx var lxp -> [] + | (_, _) -> [(CKresidual, ctx, var, lxp)] + (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and unify_call (call: lexp) (lxp: lexp) ctx vs +and unify_call (checking : scope_level option) (call: lexp) (lxp: lexp) ctx vs : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then - (unify' e1 e2 ctx vs)@op + (unify' e1 e2 ctx vs checking)@op else [(CKimpossible, ctx, call, lxp)]) [] (List.combine lxp_list1 lxp_list2) @@ -438,31 +448,29 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sortlvl (checking : scope_level option) (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] - | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs + | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs checking | SLlub (l11, l12), SLlub (l21, l22) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) - (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs) + (unify' l11 l21 ctx vs checking)@(unify' l12 l22 ctx vs checking) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) | _, _ -> [(CKresidual, ctx, sortlvl, lxp)]

(** Unify a Sort and a lexp - Sort, Sort -> if Sort ~= Sort then OK else ERROR - - Sort, Var -> Constraint - Sort, lexp -> ERROR *) -and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sort (checking : scope_level option) (sort_: lexp) (lxp: lexp) ctx vs : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with - | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs + | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs checking | StypeOmega, StypeOmega -> [] | StypeLevel, StypeLevel -> [] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) - | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]

(************************ Helper function ************************************) @@ -513,7 +521,7 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

-and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive (checking : scope_level option) ctx vs args1 args2 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)]) @@ -522,7 +530,7 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = -> (DB.lexp_ctx_cons ctx v1 Variable t1, OL.set_shift vs, if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] - else (unify' t1 t2 ctx vs) @ residue)) + else (unify' t1 t2 ctx vs checking) @ residue)) (ctx, vs, []) (List.combine args1 args2) in let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in

===================================== tests/unify_test.ml ===================================== @@ -199,6 +199,7 @@ let test_input (lxp1: lexp) (lxp2: lexp): unif_res = else (Unification, res, lxp1, lxp2) | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2) | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2) + | _ -> failwith "impossible"

let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = let r, _, _, _ = test_input lxp1 lxp2

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/2a7b7e3f99aaa3880c58e70a49b0f5195...