Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Mars 2020
- 1 participants
- 7 discussions
27 Mar '20
Stefan pushed to branch master at Stefan / Typer
Commits:
402bdbe0 by Stefan Monnier at 2020-03-27T16:04:24-04:00
Infer type of `case` target from patterns
* src/elab.ml (check_case): Infer the type of the target from the
patterns when applicable.
* src/opslexp.ml (check''): Be careful to always pass the inferred type
and the expected type in the same order.
* src/unification.ml (create_metavar_1): New function extracted from
create_metavar.
(create_metavar): Use it.
(common_subset, s_offset): New functions.
(unify_metavar): Use them to properly handle the case of unifying
a metavar with itself where the two substitutions are different.
* btl/builtins.typer (Eq_comm): Simplify type annotation a bit.
* btl/pervasive.typer (List_head1, List_head, List_tail, List_concat)
(I, List_map-fst, List_map-snd): Remove unnecessary type annotation.
- - - - -
6 changed files:
- btl/builtins.typer
- btl/pervasive.typer
- samples/hott.typer
- src/elab.ml
- src/opslexp.ml
- src/unification.ml
Changes:
=====================================
btl/builtins.typer
=====================================
@@ -1,6 +1,6 @@
%%% builtins.typer --- Initialize the builtin functions
-%% Copyright (C) 2011-2018 Free Software Foundation, Inc.
+%% Copyright (C) 2011-2020 Free Software Foundation, Inc.
%%
%% Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
%% Keywords: languages, lisp, dependent types.
@@ -48,18 +48,18 @@ Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error!
Eq_refl = Built-in "Eq.refl";
Eq_cast : (x : ?) ≡> (y : ?)
- ≡> (p : Eq x y)
+ ≡> Eq x y
≡> (f : ? -> ?)
≡> f x -> f y;
%% FIXME: I'd like to just say:
-%% Eq_cast : (p : Eq ?x ?y) ≡> ?f ?x -> ?f ?y;
+%% Eq_cast : Eq ?x ?y ≡> ?f ?x -> ?f ?y;
Eq_cast = Built-in "Eq.cast";
%% Commutativity of equality!
%% FIXME: I'd like to just say:
-%% Eq_comm : (p : Eq ?x ?y) -> Eq ?y ?x`;
-Eq_comm : (x : ?t) ≡> (y : ?t) ≡> (p : Eq x y) -> Eq (t := ?t) y x;
-Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x)
+%% Eq_comm : Eq ?x ?y -> Eq ?y ?x`;
+Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x;
+Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x)
%% FIXME: I can't figure out how `(p := p)`
%% gets inferred here, yet it seems to work!?!
Eq_refl;
=====================================
btl/pervasive.typer
=====================================
@@ -1,6 +1,6 @@
%%% pervasive --- Always available definitions
-%% Copyright (C) 2011-2018 Free Software Foundation, Inc.
+%% Copyright (C) 2011-2020 Free Software Foundation, Inc.
%%
%% Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
%% Keywords: languages, lisp, dependent types.
@@ -38,7 +38,7 @@ none = datacons Option none;
%%%% List functions
-List_length : List ?a -> Int;
+List_length : List ?a -> Int; % Recursive defs aren't generalized :-(
List_length xs = case xs
| nil => 0
| cons hd tl =>
@@ -49,18 +49,15 @@ List_length xs = case xs
%% - Provide a default value : `a -> List a -> a`;
%% - Disallow problem case : `(l : List a) -> (l != nil) -> a`;
%% - Return an Option/Error
-List_head1 : List ?a -> Option ?a;
-List_head1 : (a : Type) ≡> List a -> Option a;
List_head1 xs = case xs
| nil => none
| cons hd tl => some hd;
-List_head x = lambda xs -> case (xs : List ?a)
- %% FIXME: We shouldn't need to annotate `xs` above!
+List_head x = lambda xs -> case xs
| cons x _ => x
| nil => x;
-List_tail xs = case (xs : List ?a) % FIXME: Same here.
+List_tail xs = case xs
| nil => nil
| cons hd tl => tl;
@@ -146,7 +143,6 @@ List_reverse l t = case l
| nil => t
| cons hd tl => List_reverse tl (cons hd t);
-List_concat : List ?a -> List ?a -> List ?a;
List_concat l t = List_reverse (List_reverse l nil) t;
List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a;
@@ -183,7 +179,6 @@ List_empty xs = Int_eq (List_length xs) 0;
%%% Good 'ol combinators
-I : ?a -> ?a;
I x = x;
%% Use explicit erasable annotations since with an annotation like
@@ -429,15 +424,11 @@ List_merge xs ys = case xs
%% `Unmerge` a List of Pair
%% The two functions name said it all
-List_map-fst : List (Pair ?a ?b) -> List ?a;
List_map-fst xs = let
- mf : Pair ?a ?b -> ?a;
mf p = case p | pair x _ => x;
in List_map mf xs;
-List_map-snd : List (Pair ?a ?b) -> List ?b;
List_map-snd xs = let
- mf : Pair ?a ?b -> ?b;
mf p = case p | pair _ y => y;
in List_map mf xs;
=====================================
samples/hott.typer
=====================================
@@ -106,6 +106,9 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x));
%% similarly restrict the univalent universes so they're always erased
%% before runtime (so we don't need to have the non-nop form of "cast"
%% at run-time).
+%% This can be thought of as adding a new equality to some universes,
+%% aka making a "quotient universe", which, like HIT, requires proving
+%% that every time we use types from this universe we obey those equalities.
%%%% Propositions, resizing, etc...
=====================================
src/elab.ml
=====================================
@@ -240,7 +240,7 @@ let ctx_define_rec (ctx: elab_context) decls =
* infer the types and perform macro-expansion.
*
* More specifically, we do it with 2 mutually recursive functions:
- * - `check` takes a Pexp along with its expected type and return an Lexp
+ * - `check` takes a Pexp along with its expected type and returns an Lexp
* of that type (hopefully)
* - `infer` takes a Pexp and infers its type (which it returns along with
* the Lexp).
@@ -251,8 +251,8 @@ let ctx_define_rec (ctx: elab_context) decls =
* metavars we create/instantiate/dereference as well as the number of call to
* the unification algorithm.
* Basically guessing/annotations is only needed at those few places where the
- * code is not fully-normalized, which in normal programs is only in "let"
- * definitions.
+ * code is not fully-normalized (which in normal programs is only in "let"
+ * definitions) as well as when we fill implicit arguments.
*)
let newMetavar (ctx : lexp_context) sl name t =
@@ -462,8 +462,8 @@ let rec elaborate ctx se ot =
* elaborate ctx (Node (Symbol (l, "typer-funcall"), func::args)) ot
* but that forces `typer-funcall` to elaborate `func` a second time!
* Maybe I should only elaborate `func` above if it's a symbol
- * (and maybe even use `elaborate_varref` rather than indirecting
- * through `typr-identifier`)? *)
+ * (and maybe even use `elab_varref` rather than indirecting
+ * through `typer-identifier`)? *)
elab_call ctx ft args
and infer (p : sexp) (ctx : elab_context): lexp * ltype =
@@ -626,24 +626,49 @@ and check_case rtype (loc, target, ppatterns) ctx =
(* get target and its type *)
let tlxp, tltp = infer target ctx in
- (* FIXME: We need to be careful with whnf: while the output is "equivalent"
- * to the input, it's not necessarily as readable/efficient.
- * So try to reuse the "non-whnf" form whenever possible. *)
- 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
- let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with
- (* FIXME: Check that it's `Inductive' only after performing Unif.unify
- * with the various branches, so that we can infer the type
- * of the target from the type of the patterns. *)
- | Inductive (_, _, fargs, constructors)
- -> assert (List.length fargs = List.length targs);
- constructors
- | _ -> lexp_error (sexp_location target) tlxp
- ("Can't `case` on objects of this type: "
- ^ lexp_string tltp);
- SMap.empty in
+ let it_cs_as = ref None in
+ let ltarget = ref tlxp in
+
+ let get_cs_as it' lctor =
+ match !it_cs_as with
+ | Some (it, cs, args)
+ -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with
+ | (_::_)
+ -> lexp_error loc lctor
+ ("Expected pattern of type `"
+ ^ lexp_string it ^ "` but got `"
+ ^ lexp_string it' ^ "`")
+ | [] -> () in
+ (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 (it, targs) = call_split tltp in
+ let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with
+ | Inductive (_, _, fargs, constructors)
+ -> assert (List.length fargs = List.length targs);
+ constructors
+ | _ -> lexp_error (sexp_location target) tlxp
+ ("Can't `case` on objects of this type: "
+ ^ lexp_string tltp);
+ SMap.empty in
+ (constructors, targs) in
(* Read patterns one by one *)
let fold_fun (lbranches, dflt) (pat, pexp) =
@@ -669,19 +694,13 @@ and check_case rtype (loc, target, ppatterns) ctx =
| e -> e in
match nosusp (inst_args ctx lctor) with
| Cons (it', (_, cons_name))
- -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with
- | (_::_)
- -> lexp_error loc lctor
- ("Expected pattern of type `"
- ^ lexp_string it ^ "` but got `"
- ^ lexp_string it' ^ "`")
- | [] -> () in
- let _ = check_uniqueness pat cons_name lbranches in
+ -> 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)
+ ("`" ^ (lexp_string it')
^ "` does not have a `"
^ cons_name ^ "` constructor");
[] in
@@ -972,10 +991,16 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp =
with e ->
fatal ~loc ("Macro `" ^ mname ^ "` not found")
+(* Elaborate a bunch of mutually-recursive definitions.
+ * FIXME: Currently, we never apply generalization to recursive definitions,
+ * which means we can't define `List_length` or `List_map` without adding
+ * explicit type annotations :-( *)
and lexp_check_decls (ectx : elab_context) (* External context. *)
(nctx : elab_context) (* Context with type declarations. *)
(defs : (symbol * sexp) list)
: (vname * lexp * ltype) list * elab_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
=====================================
src/opslexp.ml
=====================================
@@ -486,11 +486,11 @@ let rec check'' erased ctx e =
let _ = List.fold_left (fun n (v, e, t)
-> assert_type
nctx e
- (push_susp t (S.shift n))
(check (if DB.set_mem (n - 1) nerased
then DB.set_empty
else nerased)
- nctx e);
+ nctx e)
+ (push_susp t (S.shift n));
n - 1)
(List.length defs) defs in
mkSusp (check nerased nctx e)
@@ -530,7 +530,7 @@ let rec check'' erased ctx e =
(error_tc ~loc:(lexp_location arg)
"arg kind mismatch"; ())
else ();
- assert_type ctx arg t1 at;
+ assert_type ctx arg at t1;
mkSusp t2 (S.substitute arg)
| _ -> (error_tc ~loc:(lexp_location arg)
("Calling a non function (type = "
@@ -620,8 +620,8 @@ let rec check'' erased ctx e =
(erased, ctx)) in
let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in
assert_type nctx branch
- (mkSusp ret (S.shift (List.length fieldtypes)))
- (check nerased nctx branch))
+ (check nerased nctx branch)
+ (mkSusp ret (S.shift (List.length fieldtypes))))
branches;
let diff = SMap.cardinal constructors - SMap.cardinal branches in
(match default with
@@ -629,8 +629,8 @@ let rec check'' erased ctx e =
-> if diff <= 0 then
warning_tc ~loc:l "Redundant default clause";
let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in
- assert_type nctx d (mkSusp ret (S.shift 1))
- (check (DB.set_sink 1 erased) nctx d)
+ assert_type nctx d (check (DB.set_sink 1 erased) nctx d)
+ (mkSusp ret (S.shift 1))
| None
-> if diff > 0 then
error_tc ~loc:l ("Non-exhaustive match: "
=====================================
src/unification.ml
=====================================
@@ -32,13 +32,16 @@ let log_info = Log.log_info ~section:"UNIF"
(* :-( *)
let global_last_metavar = ref (-1) (*The first metavar is 0*)
-let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype)
+let create_metavar_1 (sl : scope_level) (t : ltype) (clen : int)
= let idx = !global_last_metavar + 1 in
global_last_metavar := idx;
- metavar_table := U.IMap.add idx (MVar (sl, t, Myers.length ctx))
+ metavar_table := U.IMap.add idx (MVar (sl, t, clen))
(!metavar_table);
idx
+let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype)
+ = create_metavar_1 sl t (Myers.length ctx)
+
(* For convenience *)
type constraint_kind =
| CKimpossible (* Unification is simply impossible. *)
@@ -110,8 +113,60 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
var after all! *)
(metavar_table := old_mvt; true)
else false
-
-(****************************** Top level unify *************************************)
+
+(* When unifying a metavar with itself, if the two metavars don't
+ * have the same substitution applied, then we should take the "common subset"
+ * of those two substitutions: e.g.
+ *
+ * ?a[0 => x, 1 => y, 2 => z, ...] =?= ?a[0 => x, 1 => b, 2 => z, ...]
+ *
+ * then we know `?a` can't use variable #1 since if it did then the two
+ * substitutions would result in different terms.
+ * We can do that by instantiating `?a` with a new metavar:
+ *
+ * ?a = ?b[0 => 0, 1 => 2, ...]
+ * aka
+ * ?a = ?b[0 => 0 · ↑1]
+ *)
+let common_subset ctx s1 s2 =
+ let rec loop s1 s2 o1 o2 o =
+ match (s1, s2) with
+ | (S.Cons (le1, s1', o1'), S.Cons (le2, s2', o2'))
+ -> let o1 = o1 + o1' in
+ let o2 = o2 + o2' in
+ (* FIXME: We should check if le1 and le2 are *unifiable* instead! *)
+ if not (le1 = impossible || le1 = impossible)
+ && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2))
+ then match loop s1' s2' o1 o2 1 with
+ | S.Identity 1 -> S.Identity o (* Optimization! *)
+ | s' -> S.Cons (mkVar ((lexp_location le1, None), 0),
+ s', o)
+ else loop s1' s2' o1 o2 (o + 1)
+ (* If one of them reached `Identity`, unroll it, knowing that
+ *
+ * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1)
+ *)
+ | (S.Cons _, S.Identity o2')
+ -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0),
+ S.Identity 1, o2'))
+ o1 o2 o
+ | (S.Identity o1', S.Cons _)
+ -> loop (S.Cons (mkVar ((U.dummy_location, None), 0),
+ S.Identity 1, o1'))
+ s2 o1 o2 o
+ | (S.Identity o1', S.Identity o2')
+ -> assert (o1 + o1' = o2 + o2');
+ S.Identity o
+ in loop s1 s2 0 0 0
+
+(* Return the number of vars difference between input and output context. *
+ * Could be returned directly by `common_subset`, but it's pretty easy to
+ * compute it here instead. *)
+let rec s_offset s = match s with
+ | S.Identity o -> o
+ | S.Cons (_, s', o) -> o - 1 + s_offset s'
+
+(************************** Top level unify **********************************)
(** Dispatch to the right unifier.
@@ -161,7 +216,7 @@ and unify' (e1: lexp) (e2: lexp)
else ((* print_string "Unification failure on default\n"; *)
[(CKresidual, ctx, e1, e2)]))
-(********************************* Type specific unify *******************************)
+(************************* Type specific unify *******************************)
(** Unify a Arrow and a lexp if possible
- (Arrow, Arrow) -> if var_kind = var_kind
@@ -218,7 +273,7 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type =
- metavar , metavar -> if Metavar = Metavar then OK else ERROR
- metavar , lexp -> OK
*)
-and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp)
+and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp)
: return_type =
let unif idx s lxp =
let t = match metavar_lookup idx with
@@ -246,17 +301,68 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp)
^ "\n" ^ "for " ^ lexp_string lxp ^ "\n");
[(CKresidual, ctx, lxp1, lxp2)] in
match lxp2 with
- | Metavar (idx2, s2, _)
+ | Metavar (idx2, s2, name)
-> if idx = idx2 then
- (* FIXME: handle the case where s1 != s2 !! *)
- []
+ match common_subset ctx s1 s2 with
+ | S.Identity 0 -> [] (* Optimization! *)
+ (* ¡ s1 != s2 !
+ * Create a new metavar that can only refer to those vars
+ * which are mapped identically by `s1` and `s2`
+ * (as found by `common_subset`).
+ * This metavar doesn't necessarily live exactly in `ctx`
+ * nor even a proper prefix of it, tho :-( !!
+ *)
+ | s ->
+ (* print_string "Metavar idx-idx s1!=s2\n"; *)
+ assert (not (OL.conv_p ctx lxp1 lxp2));
+ match (Inverse_subst.inverse s,
+ metavar_lookup idx) with
+ | (None, _)
+ -> Log.internal_error
+ "Can't inverse subst returned by common_subset!"
+ | (_, MVal _)
+ -> Log.internal_error
+ "`lexp_whnf` returned an instantiated metavar!!"
+ | (Some s_inv, MVar (sl, t, clen))
+ -> let clen' = clen - s_offset s in
+ let t' = mkSusp t s_inv in
+ let newmv = create_metavar_1 sl t' clen' in
+ let lexp = mkMetavar (newmv, s, name) in
+ assert (sl <= clen);
+ assert (sl <= clen');
+ assert (OL.conv_p ctx (mkSusp t' s) t);
+ (* if (OL.conv_p ctx (mkSusp lexp s1) (mkSusp lexp s2)) then
+ * print_string ("common_subset successful:\n "
+ * ^ subst_string s
+ * ^ "\n =\n "
+ * ^ subst_string s1
+ * ^ "\n ∩\n "
+ * ^ subst_string s2
+ * ^ "\n")
+ * else
+ * print_string ("common_subset failed:\n "
+ * ^ subst_string s
+ * ^ "\n ∘\n "
+ * ^ subst_string s1
+ * ^ "\n =\n "
+ * ^ subst_string (scompose s s1)
+ * ^ "\n!=\n "
+ * ^ subst_string s
+ * ^ "\n ∘\n "
+ * ^ subst_string s2
+ * ^ "\n =\n "
+ * ^ subst_string (scompose s s2)
+ * ^ "\n"); *)
+ metavar_table := associate idx lexp (!metavar_table);
+ assert (OL.conv_p ctx lxp1 lxp2);
+ []
else
(* If one of the two subst can't be inverted, try the other.
* FIXME: There's probably a more general solution. *)
- (match unif idx s lxp2 with
+ (match unif idx s1 lxp2 with
| [] -> []
| _ -> unif idx2 s2 lxp1)
- | _ -> unif idx s lxp2
+ | _ -> unif idx s1 lxp2
(** Unify a Call (call) and a lexp (lxp)
- Call , Call -> UNIFY
@@ -359,7 +465,7 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type =
| Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)]
| _, _ -> [(CKimpossible, ctx, sort_, lxp)]
-(************************ Helper function **************************************)
+(************************ Helper function ************************************)
(***** for Case *****)
(** Check arg_king in <code>(arg_kind * vdef option) list </code> in Case *)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/402bdbe074bfa0149141759cb37733846…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/402bdbe074bfa0149141759cb37733846…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][master] * unification.ml: Return just a list rather than an list option
by Stefan 21 Mar '20
by Stefan 21 Mar '20
21 Mar '20
Stefan pushed to branch master at Stefan / Typer
Commits:
86d4a83d by Stefan Monnier at 2020-03-21T18:02:02-04:00
* unification.ml: Return just a list rather than an list option
Additionally, keep track of the ctx and annotate whether there's
a possibility unification could succeed at some other time.
* src/lexp.ml (constraints): Move to unification.ml
* src/unification.ml (constraint_kind): New type.
(constraints): Rewrite.
(unify_and): Remove, use `@` instead.
- - - - -
5 changed files:
- src/debruijn.ml
- src/elab.ml
- src/lexp.ml
- src/unification.ml
- tests/unify_test.ml
Changes:
=====================================
src/debruijn.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2019 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2020 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
=====================================
src/elab.ml
=====================================
@@ -550,7 +550,7 @@ and infer_type pexp ectx var =
l)))
s
(ectx_to_lctx ectx) with
- | (None | Some (_::_))
+ | (_::_)
-> (let lexp_string e = lexp_string (L.clean e) in
let typestr = lexp_string t ^ " : " ^ lexp_string s in
match var with
@@ -560,7 +560,7 @@ and infer_type pexp ectx var =
-> lexp_error l t
("Type of `" ^ name ^ "` is not a proper type: "
^ typestr))
- | Some [] -> ());
+ | [] -> ());
t
and lexp_let_decls declss (body: lexp) ctx =
@@ -576,18 +576,13 @@ and unify_with_arrow ctx tloc lxp kind var aty
let (l, _) = var in
let arrow = mkArrow (kind, var, arg, l, body) in
match Unif.unify arrow lxp (ectx_to_lctx ctx) with
- | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp
- ^ " and "
- ^ lexp_string arrow
- ^ " does not match");
- (mkDummy_type ctx l, mkDummy_type nctx l)
- | Some ((t1,t2)::_)
+ | ((_ck, _ctx, t1, t2)::_)
-> lexp_error tloc lxp ("Types:\n " ^ lexp_string t1
^ "\n and:\n "
^ lexp_string t2
^ "\n do not match!");
(mkDummy_type ctx l, mkDummy_type nctx l)
- | Some [] -> arg, body
+ | [] -> arg, body
and check (p : sexp) (t : ltype) (ctx : elab_context): lexp =
let (e, ot) = elaborate ctx p (Some t) in
@@ -607,17 +602,12 @@ and check_inferred ctx e inferred_t t =
-> (e, inferred_t)
| _ -> instantiate_implicit e inferred_t ctx in
(match Unif.unify inferred_t t (ectx_to_lctx ctx) with
- | None
- -> lexp_error (lexp_location e) e
- ("Type mismatch! Context expected `"
- ^ lexp_string t ^ "` but expression has type `"
- ^ lexp_string inferred_t ^ "`")
- | Some ((t1,t2)::_)
+ | ((_ck, _ctx, t1, t2)::_)
-> lexp_error (lexp_location e) e
("Type mismatch! Context expected `"
^ lexp_string t2 ^ "` but expression has type `"
^ lexp_string t1 ^ "`")
- | Some [] -> ());
+ | [] -> ());
e
(* Lexp.case can sometimes be inferred, but we prefer to always check. *)
@@ -680,12 +670,12 @@ and check_case rtype (loc, target, ppatterns) ctx =
match nosusp (inst_args ctx lctor) with
| Cons (it', (_, cons_name))
-> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with
- | (None | Some (_::_))
+ | (_::_)
-> lexp_error loc lctor
("Expected pattern of type `"
^ lexp_string it ^ "` but got `"
^ lexp_string it' ^ "`")
- | Some [] -> () in
+ | [] -> () in
let _ = check_uniqueness pat cons_name lbranches in
let cargs
= try SMap.find cons_name constructors
@@ -1073,12 +1063,12 @@ and lexp_decls_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
- | (None | Some (_::_))
+ | (_::_)
-> lexp_error loc ltp
("New type annotation `"
^ lexp_string ltp ^ "` incompatible with previous `"
^ lexp_string pt ^ "`")
- | Some [] -> () in
+ | [] -> () in
lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
else if List.exists (fun ((_, vname'), _) -> vname = vname')
pending_defs then
=====================================
src/lexp.ml
=====================================
@@ -155,7 +155,6 @@ type metavar_info =
* so we just keep the length of the lexp_context. *)
* ctx_length
type meta_subst = metavar_info U.IMap.t
-type constraints = (lexp * lexp) list
let dummy_scope_level = 0
let impossible = Imm Sexp.dummy_epsilon
=====================================
src/unification.ml
=====================================
@@ -40,7 +40,15 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype)
idx
(* For convenience *)
-type return_type = constraints option
+type constraint_kind =
+ | CKimpossible (* Unification is simply impossible. *)
+ | CKresidual (* We failed to find a unifier. *)
+(* 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). *)
+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
@@ -103,21 +111,6 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
(metavar_table := old_mvt; true)
else false
-(**
- lexp is equivalent to _ in ocaml
- (Let , lexp) == (lexp , Let)
- UNIFY -> recursive call or dispatching
- OK -> add a substituion to the list of substitution
- CONSTRAINT -> returns a constraint
-*)
-
-let unify_and res op = match res with
- | None -> None
- | Some constraints1
- -> match op with
- | None -> None
- | Some constraints2 -> Some (constraints2@constraints1)
-
(****************************** Top level unify *************************************)
(** Dispatch to the right unifier.
@@ -134,17 +127,17 @@ let rec unify (e1: lexp) (e2: lexp)
and unify' (e1: lexp) (e2: lexp)
(ctx : DB.lexp_context) (vs : OL.set_plexp)
: return_type =
- if e1 == e2 then Some [] else
+ if e1 == e2 then [] else
let e1' = OL.lexp_whnf e1 ctx in
let e2' = OL.lexp_whnf e2 ctx in
- if e1' == e2' then Some [] else
+ if e1' == e2' then [] else
let changed = true (* not (e1 == e1' && e2 == e2') *) in
- if changed && OL.set_member_p vs e1' e2' then Some [] else
+ 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 _))
- -> if OL.conv_p ctx e1' e2' then Some [] else None
+ -> 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'
@@ -163,10 +156,10 @@ and unify' (e1: lexp) (e2: lexp)
* ^ " and "
* ^ snd label2
* ^ "\n"); *)
- unify_inductive ctx vs' args1 args2 consts1 consts2
- | _ -> Some (if OL.conv_p ctx e1' e2' then []
- else ((* print_string "Unification failure on default\n"; *)
- [(e1, e2)]))
+ unify_inductive 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)]))
(********************************* Type specific unify *******************************)
@@ -183,15 +176,15 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs
| (Arrow (var_kind1, v1, ltype1, _, lexp1),
Arrow (var_kind2, _, ltype2, _, lexp2))
-> if var_kind1 = var_kind2
- then unify_and (unify' ltype1 ltype2 ctx vs)
- (unify' lexp1 lexp2
- (DB.lexp_ctx_cons ctx v1 Variable ltype1)
- (OL.set_shift vs))
- else None
- | (Arrow _, Imm _) -> None
- | (Arrow _, Var _) -> Some ([(arrow, lxp)])
+ then (unify' ltype1 ltype2 ctx vs)
+ @(unify' lexp1 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
- | (_, _) -> None
+ | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]
(** Unify a Lambda and a lexp if possible
- Lamda , Lambda -> if var_kind = var_kind
@@ -206,18 +199,18 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type =
| (Lambda (var_kind1, v1, ltype1, lexp1),
Lambda (var_kind2, _, ltype2, lexp2))
-> if var_kind1 = var_kind2
- then unify_and (unify' ltype1 ltype2 ctx vs)
- (unify' lexp1 lexp2
- (DB.lexp_ctx_cons ctx v1 Variable ltype1)
- (OL.set_shift vs))
- else None
+ then (unify' ltype1 ltype2 ctx vs)
+ @(unify' lexp1 lexp2
+ (DB.lexp_ctx_cons ctx v1 Variable ltype1)
+ (OL.set_shift vs))
+ else [(CKimpossible, ctx, lambda, lxp)]
| ((Lambda _, Var _)
| (Lambda _, Let _)
- | (Lambda _, Call _)) -> Some [(lambda, lxp)]
- | (Lambda _, Arrow _) -> None
- | (Lambda _, Imm _) -> None
+ | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)]
+ | (Lambda _, Arrow _)
+ | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)]
| (Lambda _, _) -> unify' lxp lambda ctx vs
- | (_, _) -> None
+ | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]
(** Unify a Metavar and a lexp if possible
- lexp , {metavar <-> none} -> UNIFY
@@ -235,15 +228,15 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp)
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");
- None
- | lxp' when occurs_in idx lxp' -> None
+ ^ "?[" ^ 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
- | Some [] as r -> r
+ | [] as r -> r
(* FIXME: Let's ignore the error for now. *)
| _
-> log_info ?loc:None
@@ -251,21 +244,18 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp)
^ lexp_string (Lexp.clean t) ^ " != "
^ lexp_string (Lexp.clean (OL.get_type ctx lxp))
^ "\n" ^ "for " ^ lexp_string lxp ^ "\n");
- Some [] in
+ [(CKresidual, ctx, lxp1, lxp2)] in
match lxp2 with
| Metavar (idx2, s2, _)
-> if idx = idx2 then
(* FIXME: handle the case where s1 != s2 !! *)
- Some []
+ []
else
(* If one of the two subst can't be inverted, try the other.
* FIXME: There's probably a more general solution. *)
(match unif idx s lxp2 with
- | Some s -> Some s
- | None ->
- match unif idx2 s2 lxp1 with
- | Some s -> Some s
- | None -> None)
+ | [] -> []
+ | _ -> unif idx2 s2 lxp1)
| _ -> unif idx s lxp2
(** Unify a Call (call) and a lexp (lxp)
@@ -279,12 +269,11 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs
when OL.conv_p ctx lxp_left lxp_right
-> List.fold_left (fun op ((ak1, e1), (ak2, e2))
-> if ak1 == ak2 then
- unify_and (unify' e1 e2 ctx vs) op
- else None)
- (Some [])
+ (unify' e1 e2 ctx vs)@op
+ else [(CKimpossible, ctx, call, lxp)])
+ []
(List.combine lxp_list1 lxp_list2)
- | (Call _, _) -> Some [(call, lxp)]
- | (_, _) -> None
+ | (_, _) -> [(CKresidual, ctx, call, lxp)]
(** Unify a Case with a lexp
- Case, Case -> try to unify
@@ -346,16 +335,14 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs
and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type =
match sortlvl, lxp with
| (SortLevel s, SortLevel s2) -> (match s, s2 with
- | SLz, SLz -> Some []
+ | SLz, SLz -> []
| SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs
| SLlub (l11, l12), SLlub (l21, l22)
-> (* FIXME: This SLlub representation needs to be
* more "canonicalized" otherwise it's too restrictive! *)
- (match (unify' l11 l21 ctx vs, unify' l12 l22 ctx vs) with
- | (Some cs1, Some cs2) -> Some (cs1 @ cs2)
- | _ -> None)
- | _, _ -> None)
- | _, _ -> None
+ (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs)
+ | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)])
+ | _, _ -> [(CKresidual, ctx, sortlvl, lxp)]
(** Unify a Sort and a lexp
- Sort, Sort -> if Sort ~= Sort then OK else ERROR
@@ -366,11 +353,11 @@ and unify_sort (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
- | StypeOmega, StypeOmega -> Some []
- | StypeLevel, StypeLevel -> Some []
- | _, _ -> None)
- | Sort _, Var _ -> Some [(sort_, lxp)]
- | _, _ -> None
+ | StypeOmega, StypeOmega -> []
+ | StypeLevel, StypeLevel -> []
+ | _, _ -> [(CKimpossible, ctx, sort_, lxp)])
+ | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)]
+ | _, _ -> [(CKimpossible, ctx, sort_, lxp)]
(************************ Helper function **************************************)
@@ -420,24 +407,28 @@ and is_same arglist arglist2 =
* | None -> test e subst)
* ) None lst *)
-and unify_inductive ctx vs args1 args2 consts1 consts2 =
+and unify_inductive 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, None) else
+ = if not (List.length args1 == List.length args2) then
+ (ctx, vs, [(CKimpossible, ctx, e1, e2)])
+ else
List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, v2, t2))
-> (DB.lexp_ctx_cons ctx v1 Variable t1,
OL.set_shift vs,
- if not (ak1 == ak2) then None
- else unify_and (unify' t1 t2 ctx vs) residue))
- (ctx, vs, Some [])
+ if not (ak1 == ak2) then [(CKimpossible, ctx, 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 None else
+ if not (SMap.cardinal consts1 == SMap.cardinal consts2) then
+ [(CKimpossible, ctx, e1, e2)]
+ else
SMap.fold (fun cname args1 residue
-> match SMap.find cname consts2 with
| args2 -> let (_ctx, _vs, residue')
= unif_formals ctx vs args1 args2 in
- unify_and residue' residue
- | exception Not_found -> None)
+ residue' @ residue
+ | exception Not_found -> [(CKimpossible, ctx, e1, e2)])
consts1 residue
(** unify the SMap of list in Inductive *)
=====================================
tests/unify_test.ml
=====================================
@@ -1,6 +1,6 @@
(* unify_test.ml --- Test the unification algorithm
*
- * Copyright (C) 2016-2019 Free Software Foundation, Inc.
+ * Copyright (C) 2016-2020 Free Software Foundation, Inc.
*
* Author: Vincent Bonnevalle <tiv.crb(a)gmail.com>
*
@@ -43,7 +43,7 @@ type result =
| Equivalent
| Nothing
-type unif_res = (result * (constraints) option * lexp * lexp)
+type unif_res = (result * (constraints) * lexp * lexp)
type triplet = string * string * string
@@ -192,13 +192,13 @@ let test_input (lxp1: lexp) (lxp2: lexp): unif_res =
let orig_subst = !metavar_table in
let res = unify lxp1 lxp2 Myers.nil in
match res with
- | Some []
+ | []
-> let new_subst = !metavar_table in
if orig_subst == new_subst
then (Equivalent, res, lxp1, lxp2)
else (Unification, res, lxp1, lxp2)
- | Some _ -> (Constraint, res, lxp1, lxp2)
- | None -> (Nothing, res, lxp1, lxp2)
+ | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2)
+ | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2)
let check (lxp1: lexp) (lxp2: lexp) (res: result): bool =
let r, _, _, _ = test_input lxp1 lxp2
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/86d4a83db13b23cac91152ae7bff6858d…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/86d4a83db13b23cac91152ae7bff6858d…
You're receiving this email because of your account on gitlab.com.
1
0
Stefan pushed to branch master at Stefan / Typer
Commits:
c081c586 by Stefan Monnier at 2020-03-20T11:28:31-04:00
-
- - - - -
1 changed file:
- samples/hott.typer
Changes:
=====================================
samples/hott.typer
=====================================
@@ -47,8 +47,8 @@
%% We additionally need some kind of elimination on paths like:
%%
%% Eq_call : Eq(_ := ?t) ?x ?y ≡> I ≡> ?t;
-%% Eq_call _ i₀ ↝ ?x
-%% Eq_call _ i₁ ↝ ?y
+%% Eq_call (_ : Eq x y) i₀ ↝ x
+%% Eq_call (_ : Eq x y) i₁ ↝ y
%%
%% Heterogenous equality could look like:
%%
@@ -81,7 +81,7 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x));
%%
%% It'd be great to support univalence without losing `Eq_cast`, but
%% it's not at all clear how:
-%% - One way is to make it a non-axiom and replace it with a system that
+%% - One way is to make it a non-axiom and implement it as a system that
%% proves it directly on a case-by-case basis, as in the paper
%% "Equivalence for Free!".
%% - Another is to make `Eq_cast` take a proof of `isSet T`,
@@ -95,6 +95,17 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x));
%%
%% but that begs the question: how could we prevent "promoting"
%% a non-erasable proof to an erasable one?
+%% - Another is to distinguish univalent universes, as done in the paper
+%% "Extending Homotopy Type Theory with Strict Equality".
+%% E.g. Our sorts `Type ℓ` would be refined to `Type k ℓ` where `k`
+%% would be a boolean indicating if the universe admits univalence or not,
+%% and then the J (aka "cast") rule would be restricted so that a proof
+%% about equality between univalent types can only be used to coerce
+%% between univalent types.
+%% This is reminiscent of the confinement of Prop in Coq, so we could
+%% similarly restrict the univalent universes so they're always erased
+%% before runtime (so we don't need to have the non-nop form of "cast"
+%% at run-time).
%%%% Propositions, resizing, etc...
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c081c5869f90f7f00b87a1ac179557bb1…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c081c5869f90f7f00b87a1ac179557bb1…
You're receiving this email because of your account on gitlab.com.
1
0
19 Mar '20
Stefan pushed to branch master at Stefan / Typer
Commits:
93cb1223 by Stefan Monnier at 2020-03-18T23:30:00-04:00
Fix up various issues with universe levels
* src/builtin.ml (type_eq): Use `mkVar`.
* src/elab.ml (elaborate): Use `mkVar`.
(infer_level): Add suport for ∪ in type level expressions.
* src/lexp.ml (mkSLlub'): Add a crutch.
(lexp_unparse, lexp_print): Clarify output of TypeLevel.
* src/opslexp.ml (level_canon, level_leq): Move earlier.
(conv_p'): Use to fix handling of `SLlub`.
(mkSLlub): Fix thinko.
(check'', get_type): Use `mkVar`.
* src/unification.ml (unify): Improve unification of SLlub.
- - - - -
5 changed files:
- src/builtin.ml
- src/elab.ml
- src/lexp.ml
- src/opslexp.ml
- src/unification.ml
Changes:
=====================================
src/builtin.ml
=====================================
@@ -1,6 +1,6 @@
(* builtin.ml --- Infrastructure to define built-in primitives
*
- * Copyright (C) 2016-2019 Free Software Foundation, Inc.
+ * Copyright (C) 2016-2020 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -105,12 +105,12 @@ let type_eq =
mkArrow (Aerasable, lv,
DB.type_level, dloc,
mkArrow (Aerasable, tv,
- mkSort (dloc, Stype (Var (lv, 0))), dloc,
+ mkSort (dloc, Stype (mkVar (lv, 0))), dloc,
mkArrow (Anormal, (dloc, None),
- Var (tv, 0), dloc,
+ mkVar (tv, 0), dloc,
mkArrow (Anormal, (dloc, None),
mkVar (tv, 1), dloc,
- mkSort (dloc, Stype (Var (lv, 3)))))))
+ mkSort (dloc, Stype (mkVar (lv, 3)))))))
let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx
=====================================
src/elab.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2019 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2020 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -491,7 +491,7 @@ and get_implicit_arg ctx loc oname t =
match
try (* FIXME: We shouldn't hard code as popular a name as `default`. *)
let pidx, pname = (senv_lookup "default" ctx), "default" in
- let default = Var ((dloc, Some pname), pidx) in
+ let default = mkVar ((dloc, Some pname), pidx) in
get_attribute ctx loc [default; t]
with e -> None with
| Some attr
@@ -1562,6 +1562,8 @@ let rec infer_level ctx se : lexp =
| Symbol _ -> check se type_level ctx
| Node (Symbol (_, "s"), [se])
-> mkSortLevel (SLsucc (infer_level ctx se))
+ | Node (Symbol (_, "_∪_"), [se1; se2])
+ -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2)
| _ -> let l = (sexp_location se) in
(sexp_error l ("Unrecognized TypeLevel: " ^ sexp_string se);
newMetavar (ectx_to_lctx ctx) dummy_scope_level (l, None) type_level)
=====================================
src/lexp.ml
=====================================
@@ -206,6 +206,8 @@ let mkCall (f, es)
| _ -> hc (Call (f, es))
let mkSLlub' (e1, e2) = match (e1, e2) with
+ (* FIXME: This first case should be handled by calling `mkSLlub` instead! *)
+ | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l
| (SortLevel SLz, _) | (_, SortLevel SLz)
-> Log.log_fatal ~section:"internal" "lub of SLz"
| (SortLevel (SLsucc _), SortLevel (SLsucc _))
@@ -582,7 +584,7 @@ let rec lexp_unparse lxp =
-> Node (Symbol (lexp_location l1, "##TypeLevel.∪"),
[lexp_unparse l1; lexp_unparse l2])
| Sort (l, StypeOmega) -> Symbol (l, "##Type_ω")
- | Sort (l, StypeLevel) -> Symbol (l, "##Type_ℓ")
+ | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel")
| Sort (l, Stype sl)
-> Node (Symbol (lexp_location sl, "##Type_"),
[lexp_unparse sl])
@@ -904,13 +906,13 @@ and lexp_str ctx (exp : lexp) : string =
| Sort (_, Stype (SortLevel SLz)) -> "##Type"
| Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1"
| Sort (_, Stype l) -> "(##Type_ " ^ lexp_string l ^ ")"
- | Sort (_, StypeLevel) -> "##Type_ℓ"
+ | Sort (_, StypeLevel) -> "##TypeLevel"
| Sort (_, StypeOmega) -> "##Type_ω"
| SortLevel (SLz) -> "##TypeLevel.z"
| SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")"
| SortLevel (SLlub (e1, e2))
- -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e1 ^ ")"
+ -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"
and lexp_str_ctor ctx ctors =
=====================================
src/opslexp.ml
=====================================
@@ -216,6 +216,36 @@ let set_shift s : set_plexp = set_shift_n s 1
(********* Testing if two types are "convertible" aka "equivalent" *********)
+(* Turn e (presumably of type TypeLevel) into a canonical representation,
+ * which is basically the set of vars it references along with the number of
+ * `succ` applied to them.
+ * `c` is the maximum "constant" level that occurs in `e`
+ * and `m` maps variable indices to the maxmimum depth at which they were
+ * found. *)
+let level_canon e =
+ let add_var_depth v d ((c,m) as acc) =
+ let o = try IMap.find v m with Not_found -> -1 in
+ if o < d then (c, IMap.add v d m) else acc in
+
+ let rec canon e d ((c,m) as acc) = match e with
+ | SortLevel SLz -> if c < d then (d, m) else acc
+ | SortLevel (SLsucc e) -> canon e (d + 1) acc
+ | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc)
+ | Var (_, i) -> add_var_depth i d acc
+ | Metavar (i, s, _)
+ -> (match metavar_lookup i with
+ | MVal e -> canon (push_susp e s) d acc
+ | _ -> add_var_depth (- i) d acc)
+ | Susp (e, s) -> canon (push_susp e s) d acc
+ | _ -> (max_int, m)
+ in canon e 0 (0,IMap.empty)
+
+let level_leq (c1, m1) (c2, m2) =
+ c1 <= c2
+ && c1 != max_int
+ && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false)
+ m1
+
(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *)
let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
let e1' = lexp_whnf e1 ctx in
@@ -233,13 +263,9 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
-> (match (sl1, sl2) with
| (SLz, SLz) -> true
| (SLsucc sl1, SLsucc sl2) -> conv_p sl1 sl2
- | (SLlub (sl11, sl12), sl2)
- (* FIXME: This should be "<=" rather than equality! *)
- -> conv_p sl11 e2' && conv_p sl12 e2'
- | (sl1, SLlub (sl21, sl22))
- (* FIXME: This should be "<=" rather than equality! *)
- -> conv_p e1' sl21 && conv_p e1' sl22
- | _ -> false)
+ | _ -> let ce1 = level_canon (L.clean e1') in
+ let ce2 = level_canon (L.clean e2') in
+ level_leq ce1 ce2 && level_leq ce2 ce1)
| (Sort (_, s1), Sort (_, s2))
-> s1 == s2
|| (match (s1, s2) with
@@ -301,47 +327,17 @@ let conv_p (ctx : DB.lexp_context) e1 e2
(********* Testing if a lexp is properly typed *********)
-(* Turn e (presumably of type TypeLevel) into its canonical representation,
- * which is basically the set of vars it references along with the number of
- * `succ` applied to them.
- * `c` is the maximum "constant" level that occurs in `e`
- * and `m` maps variable indices to the maxmimum depth at which they were
- * found. *)
-let level_canon e =
- let add_var_depth v d ((c,m) as acc) =
- let o = try IMap.find v m with Not_found -> -1 in
- if o < d then (c, IMap.add v d m) else acc in
-
- let rec canon e d ((c,m) as acc) = match e with
- | SortLevel SLz -> if c < d then (d, m) else acc
- | SortLevel (SLsucc e) -> canon e (d + 1) acc
- | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc)
- | Var (_, i) -> add_var_depth i d acc
- | Metavar (i, s, _)
- -> (match metavar_lookup i with
- | MVal e -> canon (push_susp e s) d acc
- | _ -> add_var_depth (- i) d acc)
- | Susp (e, s) -> canon (push_susp e s) d acc
- | _ -> (max_int, m)
- in canon e 0 (0,IMap.empty)
-
-let level_leq (c1, m1) (c2, m2) =
- c1 <= c2
- && c1 != max_int
- && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false)
- m1
-
let rec mkSLlub ctx e1 e2 =
match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with
- | (SortLevel SLz, e2) -> e2
- | (e1, SortLevel SLz) -> e1
+ | (SortLevel SLz, _) -> e2
+ | (_, SortLevel SLz) -> e1
| (SortLevel (SLsucc e1), SortLevel (SLsucc e2))
-> mkSortLevel (SLsucc (mkSLlub ctx e1 e2))
| (e1', e2')
-> let ce1 = level_canon (L.clean e1') in
let ce2 = level_canon (L.clean e2') in
- if level_leq ce1 ce2 then e1
- else if level_leq ce2 ce1 then e2
+ if level_leq ce1 ce2 then e2
+ else if level_leq ce2 ce1 then e1
else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)
type sort_compose_result
@@ -360,6 +356,10 @@ let sort_compose ctx1 ctx2 l ak k1 k2 =
-> if ak == P.Aerasable && impredicative_erase
then SortResult (mkSusp k2 (S.substitute impossible))
else let l2' = (mkSusp l2 (S.substitute impossible)) in
+ (* print_string ("Normal: " ^ lexp_string l1 ^ " -> "
+ * ^ lexp_string l2' ^ " ==> "
+ * ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2')))
+ * ^ "\n"); *)
SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')))
| (StypeLevel, Stype l2)
when ak == P.Aerasable && impredicative_universe_poly
@@ -367,7 +367,11 @@ let sort_compose ctx1 ctx2 l ak k1 k2 =
* It's pretty powerful, e.g. allows tuples containing
* level-polymorphic functions, and makes impredicative-encoding
* of data types almost(just?) as flexible as inductive types. *)
- -> SortResult (mkSusp k2 (S.substitute DB.level0))
+ -> (* print_string ("ImpUniv: " ^ lexp_string k1 ^ " ≡> "
+ * ^ lexp_string k2 ^ " ==> "
+ * ^ lexp_string (mkSusp k2 (S.substitute DB.level0))
+ * ^ "\n"); *)
+ SortResult (mkSusp k2 (S.substitute DB.level0))
| (StypeLevel, Stype _)
| (StypeLevel, StypeOmega)
(* This might be safe, but I don't think it adds much power.
@@ -608,7 +612,7 @@ let rec check'' erased ctx e =
| (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes
-> mkctx (dbset_push ak erased)
(DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s))
- (S.cons (Var (vdef, 0))
+ (S.cons (mkVar (vdef, 0))
(S.mkShift s 1))
vdefs fieldtypes
| _,_ -> (error_tc ~loc:l
@@ -641,7 +645,7 @@ let rec check'' erased ctx e =
let rec indtype fargs start_index =
match fargs with
| [] -> []
- | (ak, vd, _)::fargs -> (ak, Var (vd, start_index))
+ | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index))
:: indtype fargs (start_index - 1) in
let rec fieldargs ftypes =
match ftypes with
@@ -875,7 +879,7 @@ let rec get_type ctx e =
let rec indtype fargs start_index =
match fargs with
| [] -> []
- | (ak, vd, _)::fargs -> (ak, Var (vd, start_index))
+ | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index))
:: indtype fargs (start_index - 1) in
let rec fieldargs ftypes =
match ftypes with
@@ -1007,7 +1011,7 @@ let ctx2tup ctx nctx =
SMap.empty),
cons_label),
List.mapi (fun i (oname, t)
- -> (P.Aimplicit, Var (oname, offset - i - 1)))
+ -> (P.Aimplicit, mkVar (oname, offset - i - 1)))
types)
| (DB.CVlet (name, LetDef (_, e), t, _) :: blocs)
-> Let (loc, [(name, mkSusp e (S.shift 1), t)],
=====================================
src/unification.ml
=====================================
@@ -1,6 +1,6 @@
(* unification.ml --- Unification of Lexp terms
-Copyright (C) 2016-2019 Free Software Foundation, Inc.
+Copyright (C) 2016-2020 Free Software Foundation, Inc.
Author: Vincent Bonnevalle <tiv.crb(a)gmail.com>
@@ -348,8 +348,13 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type =
| (SortLevel s, SortLevel s2) -> (match s, s2 with
| SLz, SLz -> Some []
| SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs
- (* FIXME: Handle SLsub! *)
- | _, _ -> None)
+ | SLlub (l11, l12), SLlub (l21, l22)
+ -> (* FIXME: This SLlub representation needs to be
+ * more "canonicalized" otherwise it's too restrictive! *)
+ (match (unify' l11 l21 ctx vs, unify' l12 l22 ctx vs) with
+ | (Some cs1, Some cs2) -> Some (cs1 @ cs2)
+ | _ -> None)
+ | _, _ -> None)
| _, _ -> None
(** Unify a Sort and a lexp
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93cb1223b53de871422205d2635b24a1e…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93cb1223b53de871422205d2635b24a1e…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][master] * src/opslexp.ml (impredicative_erase): Disable it
by Stefan 17 Mar '20
by Stefan 17 Mar '20
17 Mar '20
Stefan pushed to branch master at Stefan / Typer
Commits:
b4bacaf0 by Stefan Monnier at 2020-03-17T14:26:41-04:00
* src/opslexp.ml (impredicative_erase): Disable it
(impredicative_universe_poly): Rename from deep_universe_poly.
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
=====================================
src/opslexp.ml
=====================================
@@ -1,6 +1,6 @@
(* opslexp.ml --- Operations on Lexps
-Copyright (C) 2011-2019 Free Software Foundation, Inc.
+Copyright (C) 2011-2020 Free Software Foundation, Inc.
Author: Stefan Monnier <monnier(a)iro.umontreal.ca>
Keywords: languages, lisp, dependent types.
@@ -46,11 +46,13 @@ let conv_erase = true (* Makes conv ignore erased terms. *)
(* `impredicative_erase` is inconsistent: as shown in samples/hurkens.typer
* it allows the definition of an inf-looping expression of type ⊥. *)
-let impredicative_erase = true (* Allows erasable args to be impredicative. *)
+let impredicative_erase = false (* Allows erasable args to be impredicative. *)
-(* The safety of `deep_universe_poly` is unknown.
- * But I also like the idea. *)
-let deep_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *)
+(* The safety of `impredicative_universe_poly` is unknown.
+ * But I also like the idea.
+ * Furthermore it is sufficient to be able to encode System-F (tho
+ * I haven't been able to generalize this result to Fω). *)
+let impredicative_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *)
(* Lexp context *)
@@ -360,7 +362,7 @@ let sort_compose ctx1 ctx2 l ak k1 k2 =
else let l2' = (mkSusp l2 (S.substitute impossible)) in
SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')))
| (StypeLevel, Stype l2)
- when ak == P.Aerasable && deep_universe_poly
+ when ak == P.Aerasable && impredicative_universe_poly
(* The safety/soundness of this rule is completely unknown.
* It's pretty powerful, e.g. allows tuples containing
* level-polymorphic functions, and makes impredicative-encoding
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b4bacaf063bc0fbdd54347c6f9e8b9068…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b4bacaf063bc0fbdd54347c6f9e8b9068…
You're receiving this email because of your account on gitlab.com.
1
0
Stefan pushed to branch master at Stefan / Typer
Commits:
93c051db by Stefan Monnier at 2020-03-17T14:06:01-04:00
* samples/hott.typer: New file
- - - - -
1 changed file:
- + samples/hott.typer
Changes:
=====================================
samples/hott.typer
=====================================
@@ -0,0 +1,132 @@
+%%% HoTT -- Homotopy Type-Theory
+
+%% Copyright (C) 2020 Free Software Foundation, Inc.
+%%
+%% Author: Stefan Monnier <monnier(a)iro.umontreal.ca>
+%%
+%% 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/>.
+
+%%% Commentary:
+
+%% Various definitions inspired from the HoTT book.
+
+%%% Code:
+
+%%%% Paths
+
+%% Cubical interval type `I`
+%% Path type:
+%%
+%% I : Type0?
+%% i₀ : I;
+%% i₁ : I;
+%%
+%% Note: while one cannot eliminate (no `if`) on `I`, one can use
+%% `∨`, `∧`, and `¬` on values of this type, and maybe one could do
+%% `type I | i₀ | i₁` and allow elimination with the simple restriction
+%% that you can only eliminate an `I` to another `I` (so one could define
+%% `∨` by hand). Better yet, maybe instead of a special `I` we could simply
+%% use a normal `Bool`, since the `≡>` already prevents elimination?
+%%
+%% Eq : (t : Type) ≡> t → t → Type;
+%% path : (p : I ≡> t) → Eq (p(_ := i₀)) (p(_ := i₁));
+%%
+%% We additionally need some kind of elimination on paths like:
+%%
+%% Eq_call : Eq(_ := ?t) ?x ?y ≡> I ≡> ?t;
+%% Eq_call _ i₀ ↝ ?x
+%% Eq_call _ i₁ ↝ ?y
+%%
+%% Heterogenous equality could look like:
+%%
+%% HEq (t₁ : Type) ≡> (t₂ : Type) ≡> t₁ → t₂ → Type;
+%% type HEq x₁ x₂
+%% | Hrefl (p : Eq t₁ t₂) (Eq (coe p x₁) x₂);
+%% type HEq (t : (i : I) ≡> Type)
+%% (x₁ : t(i := i₀)) (x₂ : t(i := i₁))
+%% | Hrefl (p : Eq t₁ t₂) (Eq (coe p x₁) x₂);
+
+%%%% Univalence
+
+%% type Equiv_function (f : ?A -> ?B) (g : ?A -> ?B)
+%% | equiv_function ((x : ?) -> Eq (f x) (g x));
+Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x));
+%% Equiv_function_axiom : Equiv_function ?f ?g -> Eq ?f ?g;
+
+%% type HoTT_IsEquiv (f : ?A -> ?B)
+%% | hott_isequiv (Equiv_function (compose f ?g) identity)
+%% (Equiv_function (compose ?h f) identity);
+
+%% type Equiv_type (A : Type) (B : Type)
+%% | equiv_type (f : A -> B) (HoTT_Isequiv f);
+%% univalence_axiom : Equiv_type A B -> Eq A B;
+
+%% FIXME: Univalence is incompatible with Typer's `Eq_cast` because
+%% it allows casting between, say, `Nat` and `BinNat` which is not
+%% a no-op. Cubical Agda supports it by making its "Eq elimination" into a
+%% non-trivial operation whose `Eq` proof is very much non-erasable.
+%%
+%% It'd be great to support univalence without losing `Eq_cast`, but
+%% it's not at all clear how:
+%% - One way is to make it a non-axiom and replace it with a system that
+%% proves it directly on a case-by-case basis, as in the paper
+%% "Equivalence for Free!".
+%% - Another is to make `Eq_cast` take a proof of `isSet T`,
+%% but that prevents use of `Eq_cast` between `Nat` and `α`
+%% since `isSet Type` is not true.
+%% It would also prevent use of `Eq_cast` on HIT.
+%% - Ideally another would be to require `Eq_cast` to take an additional
+%% proof that the equality proof is equal to `eq_refl` or more generally:
+%%
+%% Eq_cast: (eq: Eq ?x ?y) ≡> Eq_erasable eq ≡> ....
+%%
+%% but that begs the question: how could we prevent "promoting"
+%% a non-erasable proof to an erasable one?
+
+%%%% Propositions, resizing, etc...
+
+HoTT_isSet A = (x : A) -> (y : A) -> (p : Eq x y) -> (q : Eq x y) -> Eq p q;
+%% `isProp` basically implies proof irrelevance.
+%% So it also implies erasability. Note that if we use the double-negation
+%% encoding of classical `or` in type-theory, then it preserves `isProp`!
+HoTT_isProp P = (x : P) -> (y : P) -> Eq x y;
+
+%% Provable without axioms:
+%%
+%% ¬¬¬A -> ¬A
+
+Inverse_double_negation : ?A -> Not (Not ?A);
+Inverse_double_negation a na = na a;
+
+Weak_double_negation : Not (Not (Not ?A)) -> Not ?A;
+Weak_double_negation nnna a = nnna (lambda na -> na a);
+
+%% BEWARE: univalence_axiom incompatible with general LEM!
+%% HoTT_LEM_axiom : HoTT_isProp A -> ¬¬A -> A;
+
+%% "mere propositions" can be treated impredicatively!!
+%% HoTT_propositional_resizing_axiom :
+%% Equiv_type { A : Type l | isProp A} { A : Type (l + 1) | isProp A}
+
+%% Propositional truncation: ||A|| is equivalent to A but is a mere proposition.
+%% One way to approximate could be:
+Propositional_truncation A = (P : ?) ≡> HoTT_isProp P ≡> (A -> P) -> P;
+propositional_truncation : ?A -> Propositional_truncation ?A;
+propositional_truncation a f = f a;
+
+
+
+%%% hott.typer ends here.
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93c051dbed31e0ccc2969fea85ca5d25f…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93c051dbed31e0ccc2969fea85ca5d25f…
You're receiving this email because of your account on gitlab.com.
1
0
17 Mar '20
Stefan pushed to branch master at Stefan / Typer
Commits:
4bcb4b11 by Stefan Monnier at 2020-03-17T13:59:49-04:00
* src/env.ml (BI): Use `Z` rather than `Big_int`
* GNUmakefile (OBFLAGS): Use Zarith rather than Num
- - - - -
3 changed files:
- GNUmakefile
- src/env.ml
- src/eval.ml
Changes:
=====================================
GNUmakefile
=====================================
@@ -8,7 +8,7 @@ SRC_FILES := $(wildcard ./src/*.ml)
CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo)
TEST_FILES := $(wildcard ./tests/*_test.ml)
-OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg num
+OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith
# OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str
# OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)"
# OBFLAGS_RELEASE := -tag unsafe -tag inline
=====================================
src/env.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2018 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018, 2020 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -37,7 +37,7 @@ open Sexp
open Elexp
module M = Myers
module L = Lexp
-module BI = Big_int
+module BI = Z (* Was Big_int *)
module DB = Debruijn
let dloc = Util.dummy_location
@@ -49,7 +49,7 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]"
type value_type =
| Vint of int
- | Vinteger of BI.big_int
+ | Vinteger of BI.t
| Vstring of string
| Vcons of symbol * value_type list
| Vbuiltin of string
@@ -72,7 +72,7 @@ type value_type =
let rec value_equal a b =
match a, b with
| Vint (i1), Vint (i2) -> i1 = i2
- | Vinteger (i1), Vinteger (i2) -> BI.eq_big_int i1 i2
+ | Vinteger (i1), Vinteger (i2) -> i1 = i2
| Vstring (s1), Vstring (s2) -> s1 = s2
| Vbuiltin (s1), Vbuiltin (s2) -> s1 = s2
| Vfloat (f1), Vfloat (f2) -> f1 = f2
@@ -142,7 +142,7 @@ let rec value_string v =
| Vstring s -> "\"" ^ s ^ "\""
| Vbuiltin s -> s
| Vint i -> string_of_int i
- | Vinteger i -> BI.string_of_big_int i
+ | Vinteger i -> BI.to_string i
| Vfloat f -> string_of_float f
| Vsexp s -> sexp_string s
| Vtype e -> L.lexp_string e
=====================================
src/eval.ml
=====================================
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2018 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2018, 2020 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -196,10 +196,10 @@ let add_binary_biop name f =
| _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in
add_builtin_function name f 2
-let _ = add_binary_biop "+" BI.add_big_int;
- add_binary_biop "-" BI.sub_big_int;
- add_binary_biop "*" BI.mult_big_int;
- add_binary_biop "/" BI.div_big_int
+let _ = add_binary_biop "+" BI.add;
+ add_binary_biop "-" BI.sub;
+ add_binary_biop "*" BI.mul;
+ add_binary_biop "/" BI.div
let add_binary_bool_biop name f =
let name = "Integer." ^ name in
@@ -209,17 +209,17 @@ let add_binary_bool_biop name f =
| _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in
add_builtin_function name f 2
-let _ = add_binary_bool_biop "<" BI.lt_big_int;
- add_binary_bool_biop ">" BI.gt_big_int;
- add_binary_bool_biop "=" BI.eq_big_int;
- add_binary_bool_biop ">=" BI.ge_big_int;
- add_binary_bool_biop "<=" BI.le_big_int;
+let _ = add_binary_bool_biop "<" BI.lt;
+ add_binary_bool_biop ">" BI.gt;
+ add_binary_bool_biop "=" BI.equal;
+ add_binary_bool_biop ">=" BI.geq;
+ add_binary_bool_biop "<=" BI.leq;
let name = "Int->Integer" in
add_builtin_function
name
(fun loc (depth : eval_debug_info) (args_val: value_type list)
-> match args_val with
- | [Vint v] -> Vinteger (BI.big_int_of_int v)
+ | [Vint v] -> Vinteger (BI.of_int v)
| _ -> error loc ("`" ^ name ^ "` expects 1 Int argument"))
1
@@ -283,7 +283,7 @@ let make_string loc depth args_val = match args_val with
| _ -> error loc "Sexp.string expects one string as argument"
let make_integer loc depth args_val = match args_val with
- | [Vinteger n] -> Vsexp (Integer (loc, BI.int_of_big_int n))
+ | [Vinteger n] -> Vsexp (Integer (loc, BI.to_int n))
| _ -> error loc "Sexp.integer expects one integer as argument"
let make_float loc depth args_val = match args_val with
@@ -589,7 +589,7 @@ and sexp_dispatch loc depth args =
eval str (add_rte_variable vdummy (Vstring s) rctx)
| Integer (_ , i) ->
let rctx = ctx_it in
- eval it (add_rte_variable vdummy (Vinteger (BI.big_int_of_int i))
+ eval it (add_rte_variable vdummy (Vinteger (BI.of_int i))
rctx)
| Float (_ , f) ->
let rctx = ctx_flt in
@@ -691,7 +691,7 @@ let int_to_string loc depth args_val = match args_val with
| _ -> error loc "Int->String expects one Int argument"
let integer_to_string loc depth args_val = match args_val with
- | [Vinteger x] -> Vstring (BI.string_of_big_int x)
+ | [Vinteger x] -> Vstring (BI.to_string x)
| _ -> error loc "Integer->String expects one Integer argument"
let sys_exit loc depth args_val = match args_val with
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4bcb4b11c4467ed7e5859436caa46fb1b…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4bcb4b11c4467ed7e5859436caa46fb1b…
You're receiving this email because of your account on gitlab.com.
1
0