From b0fe012f7b55245254294a2658516ac57452881d Mon Sep 17 00:00:00 2001 From: depsterr Date: Sat, 4 Feb 2023 16:58:16 +0100 Subject: [PATCH] forcing of meta variables --- lib/Core/Common.ml | 8 ++-- lib/Core/Convert.ml | 27 ++++++++--- lib/Core/Eval.ml | 103 +++++++++++++++++++++++++++++++---------- lib/Core/Metaenv.ml | 14 +++++- lib/Core/Term.ml | 7 +-- lib/Core/Value.ml | 15 +++--- lib/Raw/PostProcess.ml | 28 +++++------ lib/Raw/RawSyntax.ml | 41 ---------------- lib/Raw/dune | 1 - 9 files changed, 144 insertions(+), 100 deletions(-) delete mode 100644 lib/Raw/RawSyntax.ml diff --git a/lib/Core/Common.ml b/lib/Core/Common.ml index 92d9948..0c75935 100644 --- a/lib/Core/Common.ml +++ b/lib/Core/Common.ml @@ -1,6 +1,4 @@ -(* number ; is-hole? *) -type meta - = Mv of int * bool +type meta = Mv of int let cMV : int ref = ref 0 @@ -8,3 +6,7 @@ let getCMV (_ : unit) = let c = ! cMV in cMV.contents <- c + 1; c + +type icit + = Exp + | Imp diff --git a/lib/Core/Convert.ml b/lib/Core/Convert.ml index 9866e49..3b8b73c 100644 --- a/lib/Core/Convert.ml +++ b/lib/Core/Convert.ml @@ -1,5 +1,6 @@ module V = Value module E = Eval +module M = Metaenv exception Unequal (* todo, better exception *) @@ -10,7 +11,11 @@ let rec conv_tp (len : int) (v1 : V.value) (v2 : V.value) = | T1, T1 -> () | TNat, TNat -> () | TBool, TBool -> () - | Pi (a1, C (env1, b1)), Pi (a2, C (env2, b2)) (* fallthrough *) + | Pi (i1, a1, C (env1, b1)), Pi (i2, a2, C (env2, b2)) -> + if i1 != i2 then raise Unequal else + conv_tp len a1 a2; + let fresh = V.Stuck (V.Var (V.Lvl len), a1) in + conv_tp (len+1) (E.eval (fresh :: env1) b1) (E.eval (fresh :: env2) b2) | Sg (a1, C (env1, b1)), Sg (a2, C (env2, b2)) -> conv_tp len a1 a2; let fresh = V.Stuck (V.Var (V.Lvl len), a1) in @@ -23,9 +28,9 @@ and conv_tr (len : int) (ty : V.value) (v1 : V.value) (v2 : V.value) = | Type -> conv_tp len v1 v2 | T1 -> () (* unit η-law, this still requires evaluation :/ *) | T0 -> () (* might be nice, why not? *) - | Pi (a, C (env, b)) -> + | Pi (i, a, C (env, b)) -> let fresh = V.Stuck (V.Var (V.Lvl len), a) in - conv_tr (len+1) (E.eval (fresh :: env) b) (E.app v1 a) (E.app v2 a) + conv_tr (len+1) (E.eval (fresh :: env) b) (E.app i v1 a) (E.app i v2 a) | Sg (a, C (env, b)) -> let f1 = E.fst v1 in conv_tr len a f1 (E.fst v2); @@ -40,15 +45,24 @@ and conv_tr (len : int) (ty : V.value) (v1 : V.value) (v2 : V.value) = | _ -> raise Unequal end +and conv_sp (len : int) (sp1 : V.spine) (sp2 : V.spine) = + match sp1, sp2 with + | (x1, i1, t1) :: xs1 , (x2, i2, t2) :: xs2 -> + if i1 != i2 then failwith "TODO: MIXED ICITY WAAAA :((" else + conv_sp len xs1 xs2; + conv_tp len t1 t2; + conv_tr len t1 x1 x2 + | [] , [] -> () + | _ -> raise Unequal + and conv_stuck (len : int) (s1 : V.stuck) (s2 : V.stuck) = match s1, s2 with | Var (Lvl i), Var (Lvl j) -> if i == j then () else raise Unequal | Fst p1, Fst p2 -> conv_stuck len p1 p2 | Snd p1, Snd p2 -> conv_stuck len p1 p2 - | App (f1, x1, ty1), App (f2, x2, ty2) -> + | App (f1, xs1), App (f2, xs2) -> conv_stuck len f1 f2; - conv_tp len ty1 ty2; - conv_tr len ty1 x1 x2 + conv_sp len xs1 xs2 | Ind0 (C (env1, a1), _), Ind0 (C (env2, a2), _) -> (* _ are definitionally equal *) let fresh = V.Stuck (V.Var (V.Lvl len), V.T0) in conv_tp (len+1) (E.eval (fresh :: env1) a1) (E.eval (fresh :: env2) a2) @@ -68,4 +82,5 @@ and conv_stuck (len : int) (s1 : V.stuck) (s2 : V.stuck) = conv_tp (len+1) (E.eval (fresh :: env1) a1) (E.eval (fresh :: env2) a2); conv_tr len (E.eval (V.True :: env1) a1) t1 t2; conv_tr len (E.eval (V.False :: env1) a1) f1 f2 + | Meta (Mv i1), Meta (Mv i2) -> if i1 == i2 then () else raise Unequal | _ -> raise Unequal diff --git a/lib/Core/Eval.ml b/lib/Core/Eval.ml index b916e7d..ffc5a93 100644 --- a/lib/Core/Eval.ml +++ b/lib/Core/Eval.ml @@ -1,59 +1,77 @@ module V = Value module T = Term module M = Metaenv +module C = Common open List let rec eval (env : V.env) (tr : T.term) = match tr with | Var (Ix i) -> nth env i - | Meta (Mv (i, b)) -> V.Stuck (V.Meta (Mv (i, b)), M.getMetaType i) + | Meta (Mv i) -> V.Stuck (V.Meta (Mv i), M.getMetaType i) + | InsMeta (Mv i, c) -> appEnv (V.Stuck (V.Meta (Mv i), M.getMetaType i)) c env | Type -> V.Type | T0 -> V.T0 - | Ind0 (B b, t) -> begin - match eval env t with - | Stuck (s , T0) -> V.Stuck (V.Ind0 (V.C (env, b), s), V.T0) - | _ -> failwith "eval Ind0 impossible error" - end + | Ind0 (B b, t) -> ind0 env b (eval env t) | T1 -> V.T1 | T1tr -> V.T1vl | TNat -> V.TNat | Zero -> V.Zero | Suc n -> V.Suc (eval env n) - | IndN (B b, tz, B B ts, n) -> indN env b (eval env tz) ts (eval env n) + | IndN (B b, tz, B B ts, n) -> indN env env b (eval env tz) ts (eval env n) | TBool -> V.TBool | True -> V.True | False -> V.False - | IndB (B b, t, f, bo) -> begin - match eval env bo with - | True -> eval env t - | False -> eval env f - | Stuck (s, TBool) -> V.Stuck (V.IndB (V.C (env, b), eval env t, eval env f, s), V.TBool) - | _ -> failwith "eval IndB impossible error" - end - | Pi (dom, B cod) -> V.Pi (eval env dom, V.C (env, cod)) - | Lam (B scope) -> V.Lam (C (env, scope)) - | App (f, x) -> app (eval env f) (eval env x) + | IndB (B b, t, f, bo) -> indB env b (eval env t) (eval env f) (eval env bo) + | Pi (ic, dom, B cod) -> V.Pi (ic, eval env dom, V.C (env, cod)) + | Lam (ic, B scope) -> V.Lam (ic, C (env, scope)) + | App (ic, f, x) -> app ic (eval env f) (eval env x) | Sg (ty, B tr) -> V.Sg (eval env ty, V.C (env, tr)) | Pair (x, y) -> V.Pair (eval env x, eval env y) | Fst tr -> fst (eval env tr) | Snd tr -> snd (eval env tr) | Let (tr, _, B sc) -> eval (eval env tr :: env) sc +and ind0 (env : V.env) (b : T.term) (t : V.value) = + match t with + | Stuck (s , T0) -> V.Stuck (V.Ind0 (V.C (env, b), s), V.T0) + | _ -> failwith "eval Ind0 impossible error" + +and indB (env : V.env) (b : T.term) (t : V.value) (f : V.value) (bo : V.value) = + match bo with + | True -> t + | False -> f + | Stuck (s, TBool) -> V.Stuck (V.IndB (V.C (env, b), t, f, s), V.TBool) + | _ -> failwith "eval IndB impossible error" + (* B b, B B ts *) -and indN (env : V.env) (b : T.term) (tz : V.value) (ts : T.term) (n : V.value) = +and indN (envt : V.env) (envs : V.env) (b : T.term) (tz : V.value) (ts : T.term) (n : V.value) = match n with | Zero -> tz - | Suc m -> eval (indN env b tz ts m :: m :: env) ts - | Stuck (s, TNat) -> V.Stuck (V.IndN (V.C (env, b), tz, V.C2 (env, ts), s), V.TNat) + | Suc m -> eval (indN envt envs b tz ts m :: m :: envs) ts + | Stuck (s, TNat) -> V.Stuck (V.IndN (V.C (envt, b), tz, V.C2 (envs, ts), s), V.TNat) | _ -> failwith "eval IndN impossible error" -and app (f : V.value) (x : V.value) = + +and app (ic : C.icit) (f : V.value) (x : V.value) = match f with - | Lam (C (env, tr)) -> eval (x :: env) tr + | Lam (ic', C (env, tr)) -> if ic == ic' + then eval (x :: env) tr + else failwith "TODO: MIXED ICITY WAAAA :((" + | Stuck (App (f, sp), t) -> begin + match t with + | Pi (ic', b, C (env, tr)) -> if ic == ic' + then V.Stuck ( V.App (f, (x, ic, b) :: sp) + , eval (x :: env) tr) + else failwith "TODO: MIXED ICITY WAAAA :((" + | _ -> failwith "eval app stuck f not of pi type" + end | Stuck (s, t) -> begin match t with - | Pi (_, C (env, tr)) -> V.Stuck (V.App (s, x, t), eval (x :: env) tr) + | Pi (ic', b, C (env, tr)) -> if ic == ic' + then V.Stuck ( V.App (s, [(x, ic, b)]) + , eval (x :: env) tr) + else failwith "TODO: MIXED ICITY WAAAA :((" | _ -> failwith "eval app stuck f not of pi type" end | _ -> failwith "eval app impossible error" @@ -62,10 +80,45 @@ and fst (p : V.value) = match p with | Pair (a, _) -> a | Stuck (s, Sg (a, _)) -> V.Stuck (V.Fst s, a) - | _ -> failwith "eval fst impossible error" + | _ -> failwith "eval fst impossible error" and snd (p : V.value) = match p with | Pair (_, b) -> b | Stuck (s, Sg (_, C (env, b))) -> V.Stuck (V.Snd s, (eval (fst p :: env) b)) - | _ -> failwith "eval fst impossible error" + | _ -> failwith "eval fst impossible error" + +and appEnv (p : V.value) (c : int) (e : V.env) = + match c with + | 0 -> p + | n -> match e with + | [] -> failwith "env not big enough appenv" + | h :: t -> app Exp (appEnv p (n-1) t) h + +(* TODO? force only the first "layer" *) +and force (v : V.value) = + match v with + | Suc v -> V.Suc (force v) + | Pi (i, v, c) -> V.Pi (i, force v, c) + | Sg (v, c) -> V.Sg (force v, c) + | Pair (v1, v2) -> Pair (force v1, force v2) + | Stuck (Var l, t) -> V.Stuck (Var l, t) + | Stuck (s, _) -> forceStuck s + | x -> x + +and forceStuck (s : V.stuck) = + match s with + | Meta m -> M.resolveMeta m + | Ind0 (C (env, b), s) -> ind0 env b (forceStuck s) + | IndN (C (envt, ty), z, C2 (envs, s), st) -> indN envt envs ty z s (forceStuck st) + | IndB (C (env, b), t, f, st) -> indB env b t f (forceStuck st) + | App (_, []) -> failwith "weird forceStuck empty list" + | App (st, sp) -> forceStuckApp (forceStuck st) sp + | Fst st -> fst (forceStuck st) + | Snd st -> snd (forceStuck st) + | Var _ -> failwith "forceStuck var not caught" + +and forceStuckApp (s : V.value) (sp : V.spine) = + match sp with + | [] -> s + | ((x, i, _) :: xs) -> app i (forceStuckApp s xs) x diff --git a/lib/Core/Metaenv.ml b/lib/Core/Metaenv.ml index d303d7c..6e75f3a 100644 --- a/lib/Core/Metaenv.ml +++ b/lib/Core/Metaenv.ml @@ -3,11 +3,21 @@ module V = Value open List -type mentry = {m: C.meta; ty: V.value} +type mentry + = Unsolved of V.value (* type *) + | Solved of (V.value * V.value) (* solution : type *) let metaEntries : mentry list ref = ref [] let getMetaEntry (i : int) = nth (! metaEntries) i -let getMetaType (i : int) = (getMetaEntry i).ty +let getMetaType (i : int) = + match getMetaEntry i with + | Unsolved ty -> ty + | Solved (_, ty) -> ty + +let resolveMeta (Mv i : C.meta) = + match getMetaEntry i with + | Unsolved ty -> V.Stuck (V.Meta (Mv i), ty) + | Solved (tr, _) -> tr diff --git a/lib/Core/Term.ml b/lib/Core/Term.ml index a7cd614..eabe415 100644 --- a/lib/Core/Term.ml +++ b/lib/Core/Term.ml @@ -7,6 +7,7 @@ type 'a binder = B of 'a type term = Var of var | Meta of C.meta + | InsMeta of C.meta * int (* amount of things bound in ctx : int *) | Type @@ -26,9 +27,9 @@ type term | False | IndB of term binder * term * term * term (* ordered true, false *) - | Pi of term * term binder - | Lam of term binder - | App of term * term + | Pi of C.icit * term * term binder + | Lam of C.icit * term binder + | App of C.icit * term * term | Sg of term * term binder | Pair of term * term diff --git a/lib/Core/Value.ml b/lib/Core/Value.ml index 1fa188d..427c239 100644 --- a/lib/Core/Value.ml +++ b/lib/Core/Value.ml @@ -6,6 +6,9 @@ type lvl = Lvl of int type closure = C of env * T.term and closure2 = C2 of env * T.term (* 2 variables missing *) +(* tr , icit, ty *) +and spine = (value * C.icit * value) list + and env = value list and value @@ -19,11 +22,11 @@ and value | TBool | True | False - | Pi of value * closure - | Lam of closure - | Sg of value * closure - | Pair of value * value - | Stuck of stuck * value (* second arg is type *) + | Pi of C.icit * value * closure + | Lam of C.icit * closure + | Sg of value * closure + | Pair of value * value + | Stuck of stuck * value (* second arg is type *) and stuck = Var of lvl @@ -31,6 +34,6 @@ and stuck | Ind0 of closure * stuck | IndN of closure * value * closure2 * stuck | IndB of closure * value * value * stuck - | App of stuck * value * value (* fn; val; type of fn *) + | App of stuck * spine (* fn; vals; type of fn *) | Fst of stuck | Snd of stuck diff --git a/lib/Raw/PostProcess.ml b/lib/Raw/PostProcess.ml index 9beeba3..77b8d06 100644 --- a/lib/Raw/PostProcess.ml +++ b/lib/Raw/PostProcess.ml @@ -1,7 +1,9 @@ module P = AbsImplicitt -module R = RawSyntax +module T = Core.Term -open R +open List + +open T exception UnboundVar @@ -12,10 +14,10 @@ let rec lookup (k : P.id) (env : P.id list) = let rec proc (e : P.id list) (ex : P.exp) = match ex with - | ExpPiE (name, dom, cod) -> Pi (Exp, proc e dom, proc (name :: e) cod) - | ExpPiI (name, dom, cod) -> Pi (Imp, proc e dom, proc (name :: e) cod) - | ExpSig (name, ty, fib) -> Sg (proc e ty, proc (name :: e) fib) - | ExpLet (name, tr, ty, sc) -> Let (proc e tr, proc e ty, proc (name :: e) sc) + | ExpPiE (name, dom, cod) -> Pi (Exp, proc e dom, B (proc (name :: e) cod)) + | ExpPiI (name, dom, cod) -> Pi (Imp, proc e dom, B (proc (name :: e) cod)) + | ExpSig (name, ty, fib) -> Sg (proc e ty, B (proc (name :: e) fib)) + | ExpLet (name, tr, ty, sc) -> Let (proc e tr, proc e ty, B (proc (name :: e) sc)) | ExpLam ([], _) -> failwith "impossible empty lambda" | ExpLam (bs, sc) -> unwrapLambda e bs sc | ExpAppI (e1, e2) -> App (Imp, proc e e1, proc e e2) @@ -33,15 +35,15 @@ let rec proc (e : P.id list) (ex : P.exp) = | ExpPair (e1, e2) -> Pair (proc e e1, proc e e2) | ExpFst e1 -> Fst (proc e e1) | ExpSnd e1 -> Snd (proc e e1) - | ExpHole -> Hole - | ExpInd0 (i1, e1, e2) -> Ind0 (proc (i1 :: e) e1, proc e e2) + | ExpHole -> InsMeta (C.Mv (C.getCMV ()), length e) + | ExpInd0 (i1, e1, e2) -> Ind0 (B (proc (i1 :: e) e1), proc e e2) | ExpIndN (i1, e1, e2, i2, i3, e3, e4) -> - IndN (proc (i1 :: e) e1 + IndN (B (proc (i1 :: e) e1) , proc e e2 - , proc (i3 :: i2 :: e) e3 + , B (B (proc (i3 :: i2 :: e) e3)) , proc e e4) | ExpIndB (i1, e1, e2, e3, e4) -> - IndB (proc (i1 :: e) e1 + IndB (B (proc (i1 :: e) e1) , proc e e2 , proc e e3 , proc e e4) @@ -49,5 +51,5 @@ let rec proc (e : P.id list) (ex : P.exp) = and unwrapLambda (e : P.id list) (bs : P.bD list) (sc : P.exp) = match bs with | [] -> proc e sc - | BE n :: bs -> Lam (Exp, unwrapLambda (n :: e) bs sc) - | BI n :: bs -> Lam (Imp, unwrapLambda (n :: e) bs sc) + | BE n :: bs -> Lam (Exp, B (unwrapLambda (n :: e) bs sc)) + | BI n :: bs -> Lam (Imp, B (unwrapLambda (n :: e) bs sc)) diff --git a/lib/Raw/RawSyntax.ml b/lib/Raw/RawSyntax.ml deleted file mode 100644 index e7d5591..0000000 --- a/lib/Raw/RawSyntax.ml +++ /dev/null @@ -1,41 +0,0 @@ -module C = Core.Common - -type var = Ix of int -type name = string - -type icit - = Imp - | Exp - -type ast - = Var of var - | Hole - - | Type - - | T0 - | Ind0 of ast * ast - - | T1 - | T1tr (* Unit eta rule instead of elimination principle *) - - | TNat - | Zero - | Suc of ast - | IndN of ast * ast * ast * ast - - | TBool - | True - | False - | IndB of ast * ast * ast * ast (* ordered true, false *) - - | Pi of icit * ast * ast - | Lam of icit * ast - | App of icit * ast * ast - - | Sg of ast * ast - | Pair of ast * ast - | Fst of ast - | Snd of ast - - | Let of ast * ast * ast (* tr : ty in sc *) diff --git a/lib/Raw/dune b/lib/Raw/dune index 1f9a565..89cfe5b 100644 --- a/lib/Raw/dune +++ b/lib/Raw/dune @@ -20,5 +20,4 @@ BNFC_Util LexImplicitt ParImplicitt - RawSyntax PostProcess))