forcing of meta variables

lib/Core/Common.ml

@@ -1,6 +1,4 @@
-(* number ; is-hole? *)
+type meta = Mv of int
-type meta
-  = Mv of int * bool
 
 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

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_sp len xs1 xs2
-    conv_tr len ty1 x1 x2
   | 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

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
+  | Ind0 (B b, t)             -> ind0 env b (eval env t)
-    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
   | 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
+  | IndB (B b, t, f, bo)      -> indB env b (eval env t) (eval env f) (eval env bo)
-    match eval env bo with
+  | Pi   (ic, dom, B cod)     -> V.Pi (ic, eval env dom, V.C (env, cod))
-    | True             -> eval env t
+  | Lam  (ic, B scope)        -> V.Lam (ic, C (env, scope))
-    | False            -> eval env f
+  | App  (ic, f, x)           -> app ic (eval env f) (eval env x)
-    | 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)
   | 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
+  | Suc m           -> eval (indN envt envs b tz ts m :: m :: envs) ts
-  | Stuck (s, TNat) -> V.Stuck (V.IndN (V.C (env, b), tz, V.C2 (env, ts), s), V.TNat)
+  | 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

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

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
+  | Pi   of C.icit * term * term binder
-  | Lam  of term binder
+  | Lam  of C.icit * term binder
-  | App  of term * term
+  | App  of C.icit * term * term
 
   | Sg   of term * term binder
   | Pair of term * term

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
+  | Pi    of C.icit * value  * closure
-  | Lam   of closure
+  | Lam   of C.icit * closure
-  | Sg    of value * closure
+  | Sg    of value  * closure
-  | Pair  of value * value
+  | Pair  of value  * value
-  | Stuck of stuck * value (* second arg is type *)
+  | 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

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)
+  | ExpPiE (name, dom, cod) -> Pi (Exp, proc e dom, B (proc (name :: e) cod))
-  | ExpPiI (name, dom, cod) -> Pi (Imp, proc e dom, 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, proc (name :: e) fib)
+  | 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, proc (name :: e) sc)
+  | 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
+  | ExpHole -> InsMeta (C.Mv (C.getCMV ()), length e)
-  | ExpInd0 (i1, e1, e2) -> Ind0 (proc (i1 :: e) e1, proc e e2)
+  | 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)
+  | BE n :: bs -> Lam (Exp, B (unwrapLambda (n :: e) bs sc))
-  | BI n :: bs -> Lam (Imp, unwrapLambda (n :: e) bs sc)
+  | BI n :: bs -> Lam (Imp, B (unwrapLambda (n :: e) bs sc))

lib/Raw/RawSyntax.ml

@@ -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 *)

lib/Raw/dune

@@ -20,5 +20,4 @@
           BNFC_Util
           LexImplicitt
           ParImplicitt
-          RawSyntax
           PostProcess))