mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
Unification metavariables (holes)
This commit is contained in:
Victor Maia
parent
50fab9e81f
commit
b3860e34d0
@ -6,6 +6,6 @@ edition = "2021"
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
hvm = "0.1.44"
|
||||
hvm = "0.1.46"
|
||||
highlight_error = "0.1.1"
|
||||
clap = { version = "3.1.8", features = ["derive"] }
|
||||
|
||||
@ -51,9 +51,27 @@ Equal.apply t u a b f (Refl v k) = (Refl v (f k))
|
||||
Equal.rewrite (t: Type) (a: t) (b: t) (e: (Equal t a b)) (p: t -> Type) (x: (p a)) : (p b)
|
||||
Equal.rewrite t a b (Refl u k) p x = {x :: (p k)}
|
||||
|
||||
Foo (f: Bool -> Bool) (x: Bool) : Nat
|
||||
Foo f x = x
|
||||
Example.hole : (List Bool) {
|
||||
(Cons _ True (Cons _ False (Cons _ True (Nil _))))
|
||||
}
|
||||
|
||||
Main : (List Bool) {
|
||||
(Cons Bool True (Nil _))
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
//Main : Nat {
|
||||
//(Succ True)
|
||||
//}
|
||||
|
||||
334
src/checker.hvm
334
src/checker.hvm
@ -80,6 +80,31 @@ Main = API.check_all
|
||||
// Line : String
|
||||
Line = (String.cons 10 String.nil)
|
||||
|
||||
// Subst
|
||||
// -----
|
||||
|
||||
// type Subst {
|
||||
// (End) // end of subst list
|
||||
// (Unf (rest: Subst)) // unfilled hole
|
||||
// (Sub (term: Term) (rest: Subst)) // subst hole
|
||||
// }
|
||||
|
||||
// Subst.look Subst U60 : (Maybe Term)
|
||||
(Subst.look End 0) = None
|
||||
(Subst.look (Unf rest) 0) = None
|
||||
(Subst.look (Sub term rest) 0) = (Some term)
|
||||
(Subst.look End n) = None
|
||||
(Subst.look (Unf rest) n) = (Subst.look rest (- n 1))
|
||||
(Subst.look (Sub term rest) n) = (Subst.look rest (- n 1))
|
||||
|
||||
// Subst.fill Subst U60 Term : Subst
|
||||
(Subst.fill End 0 term) = (Sub term End)
|
||||
(Subst.fill (Unf rest) 0 term) = (Sub term rest)
|
||||
(Subst.fill (Sub lost rest) 0 term) = (Sub term rest)
|
||||
(Subst.fill End n term) = (Unf (Subst.fill End (- n 1) term))
|
||||
(Subst.fill (Unf rest) n term) = (Unf (Subst.fill rest (- n 1) term))
|
||||
(Subst.fill (Sub keep rest) n term) = (Sub keep (Subst.fill rest (- n 1) term))
|
||||
|
||||
// Context
|
||||
// -------
|
||||
|
||||
@ -119,48 +144,61 @@ Line = (String.cons 10 String.nil)
|
||||
// -------------
|
||||
|
||||
// type Result (a : Type) {
|
||||
// (Checked (ctx: Context) (dep: U60) (rhs: Bool) (ret: a))
|
||||
// (Errored (ctx: Context) Error)
|
||||
// (Checked (ctx: Context) (dep: U60) (rhs: Bool) (sub: Subst) (ret: a))
|
||||
// (Errored (ctx: Context) (sub: Subst) (err: Error))
|
||||
// }
|
||||
|
||||
// Checker (a : Type) : Type {
|
||||
// (context : Context)
|
||||
// (depth : U60)
|
||||
// (right_hand_side : Bool)
|
||||
// (substitutions : Subst)
|
||||
// (Result a)
|
||||
// }
|
||||
|
||||
// type Checker (a : Type) = (context: (List Term)) (depth: U60) (rhs: Bool) (Result a)
|
||||
|
||||
// Checker.bind -(a: Type) -(b: Type) (Checker a) : (a -> Checker b) (Checker b)
|
||||
(Checker.bind checker) = λnext λctx λdep λrhs ((Checker.bind.result (checker ctx dep rhs)) next)
|
||||
(Checker.bind checker) = λnext λctx λdep λrhs λsub ((Checker.bind.result (checker ctx dep rhs sub)) next)
|
||||
|
||||
// Checker.bind.result -(a: Type) -(b: Type) (Result a) : (a -> Checker b) (Result b)
|
||||
(Checker.bind.result (Checked ctx dep rhs val)) = λnext (next val ctx dep rhs)
|
||||
(Checker.bind.result (Errored ctx err)) = λnext (Errored ctx err)
|
||||
(Checker.bind.result (Checked ctx dep rhs sub val)) = λnext (next val ctx dep rhs sub)
|
||||
(Checker.bind.result (Errored ctx sub err)) = λnext (Errored ctx sub err)
|
||||
|
||||
// Checker.done -(a: Type) (x: a) : (Checker a)
|
||||
(Checker.done val) = λctx λdep λrhs (Checked ctx dep rhs val)
|
||||
(Checker.done val) = λctx λdep λrhs λsub (Checked ctx dep rhs sub val)
|
||||
|
||||
// Checker.fail -(a: Type) (err: (List Term) -> U60 -> Error) : (Checker a)
|
||||
(Checker.fail err) = λctx λdep λrhs (Errored ctx err)
|
||||
// Checker.fail -(a: Type) (err: Error) : (Checker a)
|
||||
(Checker.fail err) = λctx λdep λrhs λsub (Errored ctx sub err)
|
||||
|
||||
// Checker.get_context -(a: Type) : (Checker Context)
|
||||
(Checker.get_context) = λctx λdep λrhs
|
||||
(Checked ctx dep rhs ctx)
|
||||
// Checker.run -(a: Type) (Checker a) : (Result a)
|
||||
(Checker.run chk) = (chk Empty 0 False End)
|
||||
|
||||
// Checker.get_depth -(a: Type) : (Checker U60)
|
||||
(Checker.get_depth) = λctx λdep λrhs
|
||||
(Checked ctx dep rhs dep)
|
||||
// Checker.get_context : (Checker Context)
|
||||
(Checker.get_context) = λctx λdep λrhs λsub
|
||||
(Checked ctx dep rhs sub ctx)
|
||||
|
||||
// Checker.get_right_hand_side -(a: Type) : (Checker U60)
|
||||
(Checker.get_right_hand_side) = λctx λdep λrhs
|
||||
(Checked ctx dep rhs rhs)
|
||||
// Checker.get_depth : (Checker U60)
|
||||
(Checker.get_depth) = λctx λdep λrhs λsub
|
||||
(Checked ctx dep rhs sub dep)
|
||||
|
||||
// Checker.set_right_hand_side -(a: Type) Bool : (Checker Unit)
|
||||
(Checker.set_right_hand_side rhs) = λctx λdep λold_rhs
|
||||
(Checked ctx dep rhs Unit)
|
||||
// Checker.get_subst : (Checker Subst)
|
||||
(Checker.get_subst) = λctx λdep λrhs λsub
|
||||
(Checked ctx dep rhs sub sub)
|
||||
|
||||
// Checker.get_right_hand_side : (Checker U60)
|
||||
(Checker.get_right_hand_side) = λctx λdep λrhs λsub
|
||||
(Checked ctx dep rhs sub rhs)
|
||||
|
||||
// Checker.set_right_hand_side Bool : (Checker Unit)
|
||||
(Checker.set_right_hand_side rhs) = λctx λdep λold_rhs λsub
|
||||
(Checked ctx dep rhs sub Unit)
|
||||
|
||||
// Checker.extend U60 Term (List Term) : (Checker Unit)
|
||||
(Checker.extend name type vals) = λctx λdep λrhs
|
||||
(Checked (Context.extend ctx name type vals) (+ dep 1) rhs Unit)
|
||||
(Checker.extend name type vals) = λctx λdep λrhs λsub
|
||||
(Checked (Context.extend ctx name type vals) (+ dep 1) rhs sub Unit)
|
||||
|
||||
// Checker.shrink -(a: Term) : (Checker Unit)
|
||||
(Checker.shrink) = λctx λdep λrhs
|
||||
(Checked (Context.tail ctx) (- dep 1) rhs Unit)
|
||||
// Checker.shrink : (Checker Unit)
|
||||
(Checker.shrink) = λctx λdep λrhs λsub
|
||||
(Checked (Context.tail ctx) (- dep 1) rhs sub Unit)
|
||||
|
||||
// Checker.extended -(a: Type) (Checker a) U60 Term Term : (Checker a)
|
||||
(Checker.extended checker name type vals) =
|
||||
@ -169,13 +207,27 @@ Line = (String.cons 10 String.nil)
|
||||
ask (Checker.bind Checker.shrink)
|
||||
(Checker.done got)
|
||||
|
||||
// Checker.get_type_of -(r: Type) U60 r (U60 -> Term -> (List Term) -> r) : (Checker r)
|
||||
(Checker.find idx d f) = λctx λdep λrhs
|
||||
(Checked ctx dep rhs (Context.find ctx idx d f))
|
||||
// Checker.find -(r: Type) U60 r (U60 -> Term -> (List Term) -> r) : (Checker r)
|
||||
(Checker.find idx d f) = λctx λdep λrhs λsub
|
||||
(Checked ctx dep rhs sub (Context.find ctx idx d f))
|
||||
|
||||
// Checker.add_value -(a: Type) (idx: U60) (val: Term) : (Checker Unit)
|
||||
(Checker.add_value idx val) = λctx λdep λrhs
|
||||
(Checked (Context.add_value ctx idx val) dep rhs Unit)
|
||||
// Checker.add_value (idx: U60) (val: Term) : (Checker Unit)
|
||||
(Checker.add_value idx val) = λctx λdep λrhs λsub
|
||||
(Checked (Context.add_value ctx idx val) dep rhs sub Unit)
|
||||
|
||||
// Checker.find -(r: Type) U60 r (U60 -> Term -> (List Term) -> r) : (Checker r)
|
||||
(Checker.find idx d f) = λctx λdep λrhs λsub
|
||||
(Checked ctx dep rhs sub (Context.find ctx idx d f))
|
||||
|
||||
// Checker.fill (idx: U60) (val: Term) : (Checker Unit)
|
||||
(Checker.fill idx val) = λctx λdep λrhs λsub
|
||||
//(HVM.log (FILL idx (Show val))
|
||||
(Checked ctx dep rhs (Subst.fill sub idx val) Unit)
|
||||
//)
|
||||
|
||||
// Checker.look (idx: U60) : (Checker (Maybe Term))
|
||||
(Checker.look idx) = λctx λdep λrhs λsub
|
||||
(Checked ctx dep rhs sub (Subst.look sub idx))
|
||||
|
||||
// Term utils
|
||||
// ----------
|
||||
@ -185,62 +237,93 @@ Line = (String.cons 10 String.nil)
|
||||
(Term.if_all other then else) = else
|
||||
|
||||
// Term.orig
|
||||
(Term.get_origin (Typ orig)) = orig
|
||||
(Term.get_origin (Var orig name index)) = orig
|
||||
(Term.get_origin (All orig name type body)) = orig
|
||||
(Term.get_origin (Lam orig name body)) = orig
|
||||
(Term.get_origin (App orig func argm)) = orig
|
||||
(Term.get_origin (Let orig name expr body)) = orig
|
||||
(Term.get_origin (Ann orig expr type)) = orig
|
||||
(Term.get_origin (Ct0 name orig)) = orig
|
||||
(Term.get_origin (Ct1 name orig a)) = orig
|
||||
(Term.get_origin (Ct2 name orig a b)) = orig
|
||||
(Term.get_origin (Ct3 name orig a b c)) = orig
|
||||
(Term.get_origin (Ct4 name orig a b c d)) = orig
|
||||
(Term.get_origin (Ct5 name orig a b c d e)) = orig
|
||||
(Term.get_origin (Ct6 name orig a b c d e f)) = orig
|
||||
(Term.get_origin (Ct7 name orig a b c d e f g)) = orig
|
||||
(Term.get_origin (Typ orig)) = orig
|
||||
(Term.get_origin (Var orig name index)) = orig
|
||||
(Term.get_origin (Hol orig numb)) = orig
|
||||
(Term.get_origin (All orig name type body)) = orig
|
||||
(Term.get_origin (Lam orig name body)) = orig
|
||||
(Term.get_origin (App orig func argm)) = orig
|
||||
(Term.get_origin (Let orig name expr body)) = orig
|
||||
(Term.get_origin (Ann orig expr type)) = orig
|
||||
(Term.get_origin (Ct0 name orig)) = orig
|
||||
(Term.get_origin (Ct1 name orig a)) = orig
|
||||
(Term.get_origin (Ct2 name orig a b)) = orig
|
||||
(Term.get_origin (Ct3 name orig a b c)) = orig
|
||||
(Term.get_origin (Ct4 name orig a b c d)) = orig
|
||||
(Term.get_origin (Ct5 name orig a b c d e)) = orig
|
||||
(Term.get_origin (Ct6 name orig a b c d e f)) = orig
|
||||
(Term.get_origin (Ct7 name orig a b c d e f g)) = orig
|
||||
(Term.get_origin (Ct8 name orig a b c d e f g h)) = orig
|
||||
(Term.get_origin (Fn0 name orig)) = orig
|
||||
(Term.get_origin (Fn1 name orig a)) = orig
|
||||
(Term.get_origin (Fn2 name orig a b)) = orig
|
||||
(Term.get_origin (Fn3 name orig a b c)) = orig
|
||||
(Term.get_origin (Fn4 name orig a b c d)) = orig
|
||||
(Term.get_origin (Fn5 name orig a b c d e)) = orig
|
||||
(Term.get_origin (Fn6 name orig a b c d e f)) = orig
|
||||
(Term.get_origin (Fn7 name orig a b c d e f g)) = orig
|
||||
(Term.get_origin (Fn0 name orig)) = orig
|
||||
(Term.get_origin (Fn1 name orig a)) = orig
|
||||
(Term.get_origin (Fn2 name orig a b)) = orig
|
||||
(Term.get_origin (Fn3 name orig a b c)) = orig
|
||||
(Term.get_origin (Fn4 name orig a b c d)) = orig
|
||||
(Term.get_origin (Fn5 name orig a b c d e)) = orig
|
||||
(Term.get_origin (Fn6 name orig a b c d e f)) = orig
|
||||
(Term.get_origin (Fn7 name orig a b c d e f g)) = orig
|
||||
(Term.get_origin (Fn8 name orig a b c d e f g h)) = orig
|
||||
|
||||
// Term.set_origin
|
||||
(Term.set_origin new_orig (Typ orig)) = (Typ new_orig)
|
||||
(Term.set_origin new_orig (Var orig name index)) = (Var new_orig name index)
|
||||
(Term.set_origin new_orig (All orig name type body)) = (All new_orig name type body)
|
||||
(Term.set_origin new_orig (Lam orig name body)) = (Lam new_orig name body)
|
||||
(Term.set_origin new_orig (App orig func argm)) = (App new_orig func argm)
|
||||
(Term.set_origin new_orig (Let orig name expr body)) = (Let new_orig name expr body)
|
||||
(Term.set_origin new_orig (Ann orig expr type)) = (Ann new_orig expr type)
|
||||
(Term.set_origin new_orig (Ct0 name orig)) = (Ct0 name new_orig)
|
||||
(Term.set_origin new_orig (Ct1 name orig a)) = (Ct1 name new_orig a)
|
||||
(Term.set_origin new_orig (Ct2 name orig a b)) = (Ct2 name new_orig a b)
|
||||
(Term.set_origin new_orig (Ct3 name orig a b c)) = (Ct3 name new_orig a b c)
|
||||
(Term.set_origin new_orig (Ct4 name orig a b c d)) = (Ct4 name new_orig a b c d)
|
||||
(Term.set_origin new_orig (Ct5 name orig a b c d e)) = (Ct5 name new_orig a b c d e)
|
||||
(Term.set_origin new_orig (Ct6 name orig a b c d e f)) = (Ct6 name new_orig a b c d e f)
|
||||
(Term.set_origin new_orig (Ct7 name orig a b c d e f g)) = (Ct7 name new_orig a b c d e f g)
|
||||
(Term.set_origin new_orig (Typ orig)) = (Typ new_orig)
|
||||
(Term.set_origin new_orig (Var orig name index)) = (Var new_orig name index)
|
||||
(Term.set_origin new_orig (Hol orig numb)) = (Hol new_orig numb)
|
||||
(Term.set_origin new_orig (All orig name type body)) = (All new_orig name type body)
|
||||
(Term.set_origin new_orig (Lam orig name body)) = (Lam new_orig name body)
|
||||
(Term.set_origin new_orig (App orig func argm)) = (App new_orig func argm)
|
||||
(Term.set_origin new_orig (Let orig name expr body)) = (Let new_orig name expr body)
|
||||
(Term.set_origin new_orig (Ann orig expr type)) = (Ann new_orig expr type)
|
||||
(Term.set_origin new_orig (Ct0 name orig)) = (Ct0 name new_orig)
|
||||
(Term.set_origin new_orig (Ct1 name orig a)) = (Ct1 name new_orig a)
|
||||
(Term.set_origin new_orig (Ct2 name orig a b)) = (Ct2 name new_orig a b)
|
||||
(Term.set_origin new_orig (Ct3 name orig a b c)) = (Ct3 name new_orig a b c)
|
||||
(Term.set_origin new_orig (Ct4 name orig a b c d)) = (Ct4 name new_orig a b c d)
|
||||
(Term.set_origin new_orig (Ct5 name orig a b c d e)) = (Ct5 name new_orig a b c d e)
|
||||
(Term.set_origin new_orig (Ct6 name orig a b c d e f)) = (Ct6 name new_orig a b c d e f)
|
||||
(Term.set_origin new_orig (Ct7 name orig a b c d e f g)) = (Ct7 name new_orig a b c d e f g)
|
||||
(Term.set_origin new_orig (Ct8 name orig a b c d e f g h)) = (Ct8 name new_orig a b c d e f g h)
|
||||
(Term.set_origin new_orig (Fn0 name orig)) = (Fn0 name new_orig)
|
||||
(Term.set_origin new_orig (Fn1 name orig a)) = (Fn1 name new_orig a)
|
||||
(Term.set_origin new_orig (Fn2 name orig a b)) = (Fn2 name new_orig a b)
|
||||
(Term.set_origin new_orig (Fn3 name orig a b c)) = (Fn3 name new_orig a b c)
|
||||
(Term.set_origin new_orig (Fn4 name orig a b c d)) = (Fn4 name new_orig a b c d)
|
||||
(Term.set_origin new_orig (Fn5 name orig a b c d e)) = (Fn5 name new_orig a b c d e)
|
||||
(Term.set_origin new_orig (Fn6 name orig a b c d e f)) = (Fn6 name new_orig a b c d e f)
|
||||
(Term.set_origin new_orig (Fn7 name orig a b c d e f g)) = (Fn7 name new_orig a b c d e f g)
|
||||
(Term.set_origin new_orig (Fn0 name orig)) = (Fn0 name new_orig)
|
||||
(Term.set_origin new_orig (Fn1 name orig a)) = (Fn1 name new_orig a)
|
||||
(Term.set_origin new_orig (Fn2 name orig a b)) = (Fn2 name new_orig a b)
|
||||
(Term.set_origin new_orig (Fn3 name orig a b c)) = (Fn3 name new_orig a b c)
|
||||
(Term.set_origin new_orig (Fn4 name orig a b c d)) = (Fn4 name new_orig a b c d)
|
||||
(Term.set_origin new_orig (Fn5 name orig a b c d e)) = (Fn5 name new_orig a b c d e)
|
||||
(Term.set_origin new_orig (Fn6 name orig a b c d e f)) = (Fn6 name new_orig a b c d e f)
|
||||
(Term.set_origin new_orig (Fn7 name orig a b c d e f g)) = (Fn7 name new_orig a b c d e f g)
|
||||
(Term.set_origin new_orig (Fn8 name orig a b c d e f g h)) = (Fn8 name new_orig a b c d e f g h)
|
||||
|
||||
// SO = Term.set_origin
|
||||
(SO new_orig term) = (Term.set_origin new_orig term)
|
||||
|
||||
// TODO
|
||||
// Term.fill Term (List Term) : Term
|
||||
(Term.fill (Typ orig) sub) = (Typ orig)
|
||||
(Term.fill (Var orig name index) sub) = (Var orig name index)
|
||||
(Term.fill (All orig name type body) sub) = (All orig name (Term.fill type sub) (Term.fill body sub))
|
||||
(Term.fill (Lam orig name body) sub) = (Lam orig (Term.fill name sub) (Term.fill body sub))
|
||||
(Term.fill (App orig func argm) sub) = (App orig (Term.fill func sub) (Term.fill argm sub))
|
||||
(Term.fill (Let orig name expr body) sub) = (Let orig name (Term.fill expr sub) (Term.fill body sub))
|
||||
(Term.fill (Ann orig expr type) sub) = (Ann orig (Term.fill expr sub) (Term.fill type sub))
|
||||
(Term.fill (Ct0 name orig) sub) = (Ct0 name orig)
|
||||
(Term.fill (Ct1 name orig a) sub) = (Ct1 name orig (Term.fill a sub))
|
||||
(Term.fill (Ct2 name orig a b) sub) = (Ct2 name orig (Term.fill a sub) (Term.fill b sub))
|
||||
(Term.fill (Ct3 name orig a b c) sub) = (Ct3 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub))
|
||||
(Term.fill (Ct4 name orig a b c d) sub) = (Ct4 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub))
|
||||
(Term.fill (Ct5 name orig a b c d e) sub) = (Ct5 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub))
|
||||
(Term.fill (Ct6 name orig a b c d e f) sub) = (Ct6 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub) (Term.fill f sub))
|
||||
(Term.fill (Ct7 name orig a b c d e f g) sub) = (Ct7 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub) (Term.fill f sub) (Term.fill g sub))
|
||||
(Term.fill (Ct8 name orig a b c d e f g h) sub) = (Ct8 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub) (Term.fill f sub) (Term.fill g sub) (Term.fill h sub))
|
||||
(Term.fill (Fn0 name orig) sub) = (Fn0 name orig)
|
||||
(Term.fill (Fn1 name orig a) sub) = (Fn1 name orig (Term.fill a sub))
|
||||
(Term.fill (Fn2 name orig a b) sub) = (Fn2 name orig (Term.fill a sub) (Term.fill b sub))
|
||||
(Term.fill (Fn3 name orig a b c) sub) = (Fn3 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub))
|
||||
(Term.fill (Fn4 name orig a b c d) sub) = (Fn4 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub))
|
||||
(Term.fill (Fn5 name orig a b c d e) sub) = (Fn5 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub))
|
||||
(Term.fill (Fn6 name orig a b c d e f) sub) = (Fn6 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub) (Term.fill f sub))
|
||||
(Term.fill (Fn7 name orig a b c d e f g) sub) = (Fn7 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub) (Term.fill f sub) (Term.fill g sub))
|
||||
(Term.fill (Fn8 name orig a b c d e f g h) sub) = (Fn8 name orig (Term.fill a sub) (Term.fill b sub) (Term.fill c sub) (Term.fill d sub) (Term.fill e sub) (Term.fill f sub) (Term.fill g sub) (Term.fill h sub))
|
||||
(Term.fill (Hol orig numb) sub) = (Maybe.case (Subst.look sub numb) (Hol orig numb) λval (Term.fill val sub))
|
||||
|
||||
// Equal Term Term : (Checker Bool)
|
||||
// --------------------------------
|
||||
|
||||
@ -361,6 +444,14 @@ Line = (String.cons 10 String.nil)
|
||||
ask x7 = (Checker.bind (Equal a.x7 b.x7))
|
||||
(Checker.done (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 x7)))))))))
|
||||
|
||||
// Hol equality #0
|
||||
(Equal (Hol a.orig a.numb) b) =
|
||||
(Equal.hol a.orig a.numb b)
|
||||
|
||||
// Hol equality #1
|
||||
(Equal a (Hol b.orig b.numb)) =
|
||||
(Equal.hol b.orig b.numb a)
|
||||
|
||||
// Var equality #0
|
||||
(Equal (Var a.orig a.name a.index) b) =
|
||||
ask rhs = (Checker.bind (Checker.get_right_hand_side))
|
||||
@ -375,14 +466,14 @@ Line = (String.cons 10 String.nil)
|
||||
(Equal a b) =
|
||||
(Checker.done False)
|
||||
|
||||
// Equal.var (rhs : Bool) (index : U60) (b: Term) : (Checker bool)
|
||||
// ---------------------------------------------------------------
|
||||
// Equal.var (rhs: Bool) (origin: U60) (index: U60) (b: Term) : (Checker bool)
|
||||
// ---------------------------------------------------------------------------
|
||||
// A variable is equal to a term when any of its reductions is
|
||||
|
||||
// If on LHS, extend the variable's equality list
|
||||
// If on RHS, check if a and b are equal
|
||||
|
||||
// Var-Var checker
|
||||
// Variable checker
|
||||
(Equal.var False a.orig a.name a.index b) =
|
||||
ask (Checker.bind (Checker.add_value a.index b))
|
||||
(Checker.done True)
|
||||
@ -407,6 +498,30 @@ Line = (String.cons 10 String.nil)
|
||||
(Equal.var.try_values Nil b) =
|
||||
(Checker.done False)
|
||||
|
||||
// Equal.hol (origin: U60) (numb: U60) (b: Term) : (Checker bool)
|
||||
// --------------------------------------------------------------
|
||||
|
||||
//hole_0 == A
|
||||
//- se hole_0 não tiver um valor...
|
||||
//- seta o valor de hole_0 como A
|
||||
//- se hole_0 tiver um valor...
|
||||
//- checa se esse valor é igual a A
|
||||
|
||||
// Hole checker
|
||||
(Equal.hol a.orig a.numb b) =
|
||||
ask sub = (Checker.bind (Checker.get_subst))
|
||||
ask got = (Checker.bind (Checker.look a.numb))
|
||||
(Equal.hol.val got a.orig a.numb b)
|
||||
|
||||
// Hole has no value yet, so we set it
|
||||
(Equal.hol.val None a.orig a.numb b) =
|
||||
ask (Checker.bind (Checker.fill a.numb b))
|
||||
(Checker.done True)
|
||||
|
||||
// Hole has a value, so we compare it
|
||||
(Equal.hol.val (Some a.val) a.orig a.numb b) =
|
||||
(Equal a.val b)
|
||||
|
||||
// Infer Term : (Checker Term)
|
||||
// ---------------------------
|
||||
|
||||
@ -417,6 +532,10 @@ Line = (String.cons 10 String.nil)
|
||||
(Checker.fail (UnboundVariable (Var orig name index)))
|
||||
λvar_type (Checker.done var_type))
|
||||
|
||||
// Infers Hol
|
||||
(Infer (Hol orig numb)) =
|
||||
(Checker.fail (CantInferHole (Hol orig numb)))
|
||||
|
||||
// Infers Typ
|
||||
(Infer (Typ orig)) =
|
||||
(Checker.done (Typ orig))
|
||||
@ -550,6 +669,10 @@ Line = (String.cons 10 String.nil)
|
||||
(Check.compare (Var orig name index) type)
|
||||
(Checker.extend name type Nil))
|
||||
|
||||
// Checks Hol
|
||||
(Check (Hol orig numb) type) =
|
||||
(Checker.done Unit)
|
||||
|
||||
// Checks others
|
||||
(Check term type) =
|
||||
(Check.compare term type)
|
||||
@ -599,6 +722,10 @@ Line = (String.cons 10 String.nil)
|
||||
(Show.name name)
|
||||
])
|
||||
|
||||
(Show (Hol orig numb)) = (Text [
|
||||
"_" (Show.u60 numb)
|
||||
])
|
||||
|
||||
(Show (Typ orig)) = (Text [
|
||||
"Type"
|
||||
])
|
||||
@ -830,6 +957,16 @@ Line = (String.cons 10 String.nil)
|
||||
(Show.context.vals name vals pad)
|
||||
])
|
||||
|
||||
(Show.subst End) = "|"
|
||||
(Show.subst (Unf rest)) = (Text [
|
||||
"~ ?" Line
|
||||
(Show.subst rest)
|
||||
])
|
||||
(Show.subst (Sub expr rest)) = (Text [
|
||||
"~ " (Show expr) Line
|
||||
(Show.subst rest)
|
||||
])
|
||||
|
||||
// Show.u60 U60 : String
|
||||
(Show.u60 n) = (Show.u60.build n String.nil)
|
||||
(Show.u60.build n str) =
|
||||
@ -878,7 +1015,7 @@ API.run_main = (Text [
|
||||
|
||||
(API.check_function.verifiers Nil type) = Nil
|
||||
(API.check_function.verifiers (Cons verifier verifiers) type) =
|
||||
let head = ((Check.verify verifier type) Empty 0 False)
|
||||
let head = (Checker.run (Check.verify verifier type))
|
||||
let tail = (API.check_function.verifiers verifiers type)
|
||||
(Cons head tail)
|
||||
|
||||
@ -892,40 +1029,49 @@ API.run_main = (Text [
|
||||
|
||||
(API.output.function fnid Nil) =
|
||||
String.nil
|
||||
(API.output.function fnid (Cons (Checked ctx dep rhs val) checks)) =
|
||||
(API.output.function fnid checks)
|
||||
(API.output.function fnid (Cons (Errored ctx err) checks)) =
|
||||
(API.output.function fnid (Cons (Checked ctx dep rhs sub val) checks)) =
|
||||
(Text [
|
||||
//(NameOf fnid) Line
|
||||
//(Show.subst sub) Line
|
||||
(API.output.function fnid checks)
|
||||
])
|
||||
(API.output.function fnid (Cons (Errored ctx sub err) checks)) =
|
||||
(Text [
|
||||
(Color "1") "[" (NameOf fnid) "] " (Color "0") Line
|
||||
(API.output.error err ctx) Line
|
||||
(API.output.error err ctx sub) Line
|
||||
(API.output.function fnid checks)
|
||||
])
|
||||
|
||||
(API.output.error (UnboundVariable term) ctx) =
|
||||
(API.output.error (UnboundVariable term) ctx sub) =
|
||||
(Text [
|
||||
(Color "4") "Unbound Variable." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (CantInferLambda term) ctx) =
|
||||
(API.output.error (CantInferLambda term) ctx sub) =
|
||||
(Text [
|
||||
(Color "4") "Can't infer lambda." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (TooManyArguments term) ctx) =
|
||||
(API.output.error (CantInferHole term) ctx sub) =
|
||||
(Text [
|
||||
(Color "4") "Can't infer hole." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (TooManyArguments term) ctx sub) =
|
||||
(Text [
|
||||
(Color "4") "Too many arguments." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (InvalidCall term) ctx) =
|
||||
(API.output.error (InvalidCall term) ctx sub) =
|
||||
(Text [
|
||||
(Color "4") "Invalid call." (Color "0") Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
(API.output.error (TypeMismatch term expected detected) ctx) =
|
||||
(API.output.error (TypeMismatch term expected detected) ctx sub) =
|
||||
(Text [
|
||||
(Color "4") "Type mismatch." (Color "0") Line
|
||||
"- Expected: " (Show expected) Line
|
||||
"- Detected: " (Show detected) Line
|
||||
"- Expected: " (Show (Term.fill expected sub)) Line
|
||||
"- Detected: " (Show (Term.fill detected sub)) Line
|
||||
(API.output.error.details ctx term)
|
||||
])
|
||||
|
||||
|
||||
@ -4,7 +4,8 @@ use hvm::parser as parser;
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct File {
|
||||
names: Vec<String>,
|
||||
entries: HashMap<String, Box<Entry>>
|
||||
entrs: HashMap<String, Box<Entry>>,
|
||||
holes: u64,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
@ -40,6 +41,7 @@ pub enum Term {
|
||||
Ann { orig: u64, expr: Box<Term>, tipo: Box<Term> },
|
||||
Ctr { orig: u64, name: String, args: Vec<Box<Term>> },
|
||||
Fun { orig: u64, name: String, args: Vec<Box<Term>> },
|
||||
Hol { orig: u64, numb: u64 },
|
||||
}
|
||||
|
||||
// Adjuster
|
||||
@ -47,49 +49,50 @@ pub enum Term {
|
||||
|
||||
pub fn adjust_file(file: &File) -> File {
|
||||
let mut names = Vec::new();
|
||||
let mut entries = HashMap::new();
|
||||
let mut entrs = HashMap::new();
|
||||
let mut holes = 0;
|
||||
for name in &file.names {
|
||||
let entry = file.entries.get(name).unwrap();
|
||||
let entry = file.entrs.get(name).unwrap();
|
||||
names.push(name.clone());
|
||||
entries.insert(name.clone(), Box::new(adjust_entry(file, &entry)));
|
||||
entrs.insert(name.clone(), Box::new(adjust_entry(file, &entry, &mut holes)));
|
||||
}
|
||||
return File { names, entries };
|
||||
return File { names, entrs, holes };
|
||||
}
|
||||
|
||||
pub fn adjust_entry(file: &File, entry: &Entry) -> Entry {
|
||||
pub fn adjust_entry(file: &File, entry: &Entry, holes: &mut u64) -> Entry {
|
||||
let name = entry.name.clone();
|
||||
let mut args = Vec::new();
|
||||
for arg in &entry.args {
|
||||
args.push(Box::new(adjust_argument(file, arg)));
|
||||
args.push(Box::new(adjust_argument(file, arg, holes)));
|
||||
}
|
||||
let tipo = Box::new(adjust_term(file, &*entry.tipo));
|
||||
let tipo = Box::new(adjust_term(file, &*entry.tipo, holes));
|
||||
let mut rules = Vec::new();
|
||||
for rule in &entry.rules {
|
||||
rules.push(Box::new(adjust_rule(file, &*rule)));
|
||||
rules.push(Box::new(adjust_rule(file, &*rule, holes)));
|
||||
}
|
||||
return Entry { name, args, tipo, rules };
|
||||
}
|
||||
|
||||
pub fn adjust_argument(file: &File, arg: &Argument) -> Argument {
|
||||
pub fn adjust_argument(file: &File, arg: &Argument, holes: &mut u64) -> Argument {
|
||||
let eras = arg.eras;
|
||||
let name = arg.name.clone();
|
||||
let tipo = Box::new(adjust_term(file, &*arg.tipo));
|
||||
let tipo = Box::new(adjust_term(file, &*arg.tipo, holes));
|
||||
return Argument { eras, name, tipo };
|
||||
}
|
||||
|
||||
pub fn adjust_rule(file: &File, rule: &Rule) -> Rule {
|
||||
pub fn adjust_rule(file: &File, rule: &Rule, holes: &mut u64) -> Rule {
|
||||
let name = rule.name.clone();
|
||||
let mut pats = Vec::new();
|
||||
for pat in &rule.pats {
|
||||
pats.push(Box::new(adjust_term(file, &*pat)));
|
||||
pats.push(Box::new(adjust_term(file, &*pat, holes)));
|
||||
}
|
||||
let body = Box::new(adjust_term(file, &*rule.body));
|
||||
let body = Box::new(adjust_term(file, &*rule.body, holes));
|
||||
return Rule { name, pats, body };
|
||||
}
|
||||
|
||||
// TODO: check unbound variables
|
||||
// TODO: prevent defining the same name twice
|
||||
pub fn adjust_term(file: &File, term: &Term) -> Term {
|
||||
pub fn adjust_term(file: &File, term: &Term, holes: &mut u64) -> Term {
|
||||
match *term {
|
||||
Term::Typ { orig } => {
|
||||
Term::Typ { orig }
|
||||
@ -100,39 +103,39 @@ pub fn adjust_term(file: &File, term: &Term) -> Term {
|
||||
},
|
||||
Term::Let { ref orig, ref name, ref expr, ref body } => {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(adjust_term(file, &*expr));
|
||||
let body = Box::new(adjust_term(file, &*body));
|
||||
let expr = Box::new(adjust_term(file, &*expr, holes));
|
||||
let body = Box::new(adjust_term(file, &*body, holes));
|
||||
Term::Let { orig, name: name.clone(), expr, body }
|
||||
},
|
||||
Term::Ann { ref orig, ref expr, ref tipo } => {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(adjust_term(file, &*expr));
|
||||
let tipo = Box::new(adjust_term(file, &*tipo));
|
||||
let expr = Box::new(adjust_term(file, &*expr, holes));
|
||||
let tipo = Box::new(adjust_term(file, &*tipo, holes));
|
||||
Term::Ann { orig, expr, tipo }
|
||||
},
|
||||
Term::All { ref orig, ref name, ref tipo, ref body } => {
|
||||
let orig = *orig;
|
||||
let tipo = Box::new(adjust_term(file, &*tipo));
|
||||
let body = Box::new(adjust_term(file, &*body));
|
||||
let tipo = Box::new(adjust_term(file, &*tipo, holes));
|
||||
let body = Box::new(adjust_term(file, &*body, holes));
|
||||
Term::All { orig, name: name.clone(), tipo, body }
|
||||
},
|
||||
Term::Lam { ref orig, ref name, ref body } => {
|
||||
let orig = *orig;
|
||||
let body = Box::new(adjust_term(file, &*body));
|
||||
let body = Box::new(adjust_term(file, &*body, holes));
|
||||
Term::Lam { orig, name: name.clone(), body }
|
||||
},
|
||||
Term::App { ref orig, ref func, ref argm } => {
|
||||
let orig = *orig;
|
||||
let func = Box::new(adjust_term(file, &*func));
|
||||
let argm = Box::new(adjust_term(file, &*argm));
|
||||
let func = Box::new(adjust_term(file, &*func, holes));
|
||||
let argm = Box::new(adjust_term(file, &*argm, holes));
|
||||
Term::App { orig, func, argm }
|
||||
},
|
||||
Term::Ctr { ref orig, ref name, ref args } => {
|
||||
let orig = *orig;
|
||||
if let Some(entry) = file.entries.get(name) {
|
||||
if let Some(entry) = file.entrs.get(name) {
|
||||
let mut new_args = Vec::new();
|
||||
for arg in args {
|
||||
new_args.push(Box::new(adjust_term(file, &*arg)));
|
||||
new_args.push(Box::new(adjust_term(file, &*arg, holes)));
|
||||
}
|
||||
if entry.rules.len() > 0 {
|
||||
Term::Fun { orig, name: name.clone(), args: new_args }
|
||||
@ -146,6 +149,12 @@ pub fn adjust_term(file: &File, term: &Term) -> Term {
|
||||
Term::Fun { ref orig, ref name, ref args } => {
|
||||
panic!("Internal error."); // shouldn't happen since we can't parse Fun{}
|
||||
},
|
||||
Term::Hol { ref orig, numb: _ } => {
|
||||
let orig = *orig;
|
||||
let numb = *holes;
|
||||
*holes = *holes + 1;
|
||||
Term::Hol { orig, numb }
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
@ -210,6 +219,20 @@ pub fn parse_var(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
)
|
||||
}
|
||||
|
||||
pub fn parse_hol(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
parser::guard(
|
||||
parser::text_parser("_"),
|
||||
Box::new(|state| {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, _) = parser::consume("_", state)?;
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(init, last);
|
||||
Ok((state, Box::new(Term::Hol { orig, numb: 0 })))
|
||||
}),
|
||||
state,
|
||||
)
|
||||
}
|
||||
|
||||
pub fn parse_lam(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
parser::guard(
|
||||
parser::text_parser("@"),
|
||||
@ -403,6 +426,7 @@ pub fn parse_term_prefix(state: parser::State) -> parser::Answer<Box<Term>> {
|
||||
Box::new(parse_let), // `let `
|
||||
Box::new(parse_ann), // `{x::`
|
||||
Box::new(parse_hlp), // `?`
|
||||
Box::new(parse_hol), // `_`
|
||||
Box::new(parse_var), //
|
||||
Box::new(|state| Ok((state, None))),
|
||||
], state)
|
||||
@ -485,12 +509,12 @@ pub fn parse_argument(state: parser::State) -> parser::Answer<Box<Argument>> {
|
||||
pub fn parse_file(state: parser::State) -> parser::Answer<Box<File>> {
|
||||
let (state, entry_vec) = parser::until(Box::new(parser::done), Box::new(parse_entry), state)?;
|
||||
let mut names = Vec::new();
|
||||
let mut entries = HashMap::new();
|
||||
let mut entrs = HashMap::new();
|
||||
for entry in entry_vec {
|
||||
names.push(entry.name.clone());
|
||||
entries.insert(entry.name.clone(), entry);
|
||||
entrs.insert(entry.name.clone(), entry);
|
||||
}
|
||||
return Ok((state, Box::new(File { names, entries })));
|
||||
return Ok((state, Box::new(File { holes: 0, names, entrs })));
|
||||
}
|
||||
|
||||
pub fn show_term(term: &Term) -> String {
|
||||
@ -535,6 +559,9 @@ pub fn show_term(term: &Term) -> String {
|
||||
Term::Fun { orig: _, name, args } => {
|
||||
format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
|
||||
}
|
||||
Term::Hol { orig: _, numb } => {
|
||||
format!("_")
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -568,7 +595,7 @@ pub fn show_entry(entry: &Entry) -> String {
|
||||
pub fn show_file(file: &File) -> String {
|
||||
let mut lines = vec![];
|
||||
for name in &file.names {
|
||||
lines.push(show_entry(file.entries.get(name).unwrap()));
|
||||
lines.push(show_entry(file.entrs.get(name).unwrap()));
|
||||
}
|
||||
lines.join("\n")
|
||||
}
|
||||
@ -646,6 +673,9 @@ pub fn compile_term(term: &Term, quote: bool, lhs: bool) -> String {
|
||||
}
|
||||
format!("({}{} {}. {}{})", if quote { "Fn" } else { "FN" }, args.len(), name, hide(orig,lhs), args_strs.join(""))
|
||||
}
|
||||
Term::Hol { orig, numb } => {
|
||||
format!("(Hol {} {})", orig, numb)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -745,12 +775,12 @@ pub fn compile_file(file: &File) -> String {
|
||||
result.push_str(&format!("\nFunctions =\n"));
|
||||
result.push_str(&format!(" let fns = Nil\n"));
|
||||
for name in &file.names {
|
||||
let entry = file.entries.get(name).unwrap();
|
||||
let entry = file.entrs.get(name).unwrap();
|
||||
result.push_str(&format!(" let fns = (Cons {}. fns)\n", entry. name));
|
||||
}
|
||||
result.push_str(&format!(" fns\n\n"));
|
||||
for name in &file.names {
|
||||
let entry = file.entries.get(name).unwrap();
|
||||
let entry = file.entrs.get(name).unwrap();
|
||||
result.push_str(&format!("// {}\n", name));
|
||||
result.push_str(&format!("// {}\n", "-".repeat(name.len())));
|
||||
result.push_str(&format!("\n"));
|
||||
|
||||
@ -11,7 +11,6 @@ use hvm::parser as parser;
|
||||
const CHECKER_HVM: &str = include_str!("checker.hvm");
|
||||
|
||||
fn main() {
|
||||
println!("{}", name_to_u64("_"));
|
||||
match run_cli() {
|
||||
Ok(..) => {}
|
||||
Err(err) => {
|
||||
|
||||
Loading…
Reference in New Issue
Block a user