From f8f56ba8aa2142e13f185019c16cd77dda40dea5 Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Mon, 23 Oct 2023 23:21:22 +0700 Subject: [PATCH] at least it works --- library/data/equiv.anders | 17 +++++++--- .../syntaxes/anders.tmLanguage.json | 2 +- src/frontend/decl.ml | 1 + src/frontend/module.ml | 32 +++++++++---------- src/frontend/parser.ml | 5 +-- src/frontend/radio.ml | 1 + src/kernel/check.ml | 26 +++++++++++---- src/kernel/chm.ml | 10 ++++-- src/kernel/term.ml | 8 +++-- src/language/decode.ml | 3 +- src/language/encode.ml | 3 +- src/language/spec.ml | 1 + 12 files changed, 70 insertions(+), 39 deletions(-) diff --git a/library/data/equiv.anders b/library/data/equiv.anders index a19b6b4..4a4f51a 100644 --- a/library/data/equiv.anders +++ b/library/data/equiv.anders @@ -63,8 +63,14 @@ section hcomp (Glue A φ [(φ = 1) → e 1=1]) ψ (λ (i : I), [(ψ = 1) → u i 1=1]) (ouc u₀) end +def transportε (A B : U) (p : PathP (<_> U) A B) : A → B := +λ (x : A), transp p 0 (transp (<_> A) 0 x) + +def transportεIsEquiv (A B : U) (p : PathP (<_> U) A B) : isEquiv A B (transportε A B p) := +(transp ( equiv A (p @ i)) 0 (idEquiv A)).2 + def idtoeqv (A B : U) (p : PathP (<_> U) A B) : equiv A B := -transp ( equiv A (p @ i)) 0 (idEquiv A) +(transportε A B p, transportεIsEquiv A B p) def ua (A B : U) (e : equiv A B) : PathP (<_> U) A B := Glue B (∂ i) [(i = 0) → (A, e), (i = 1) → (B, idEquiv B)] @@ -84,9 +90,10 @@ propPi B (λ (y : B), isContr (fiber A B f y)) def idtoeqv→trans (A B : U) (p : PathP (<_> U) A B) : Path (A → B) (idtoeqv A B p).1 (trans A B p) := λ (a : A), transp p 0 (transp (<_> A) i a) -def ideqv-compute (A B : U) (e : equiv A B) : Path (A → B) (idtoeqv A B (ua A B e)).1 e.1 := +def ideqv-compute (A B : U) (e : equiv A B) : Path (A → B) (transportε A B (ua A B e)) e.1 := comp-Path (A → B) (idtoeqv A B (ua A B e)).1 (trans A B (ua A B e)) e.1 (idtoeqv→trans A B (ua A B e)) (ua-β A B e) --- should “isEquiv” be opaque? ---def idtoeqv-ua (A B : U) (e : equiv A B) : Path (equiv A B) (idtoeqv A B (ua A B e)) e := ---lemSig (A → B) (isEquiv A B) (isEquivProp A B) (idtoeqv A B (ua A B e)) e (ideqv-compute A B e) \ No newline at end of file +opaque transportεIsEquiv + +def idtoeqv-ua (A B : U) (e : equiv A B) : Path (equiv A B) (idtoeqv A B (ua A B e)) e := +lemSig (A → B) (isEquiv A B) (isEquivProp A B) (idtoeqv A B (ua A B e)) e (ideqv-compute A B e) \ No newline at end of file diff --git a/share/anders-vscode/syntaxes/anders.tmLanguage.json b/share/anders-vscode/syntaxes/anders.tmLanguage.json index 6958810..289a9ec 100644 --- a/share/anders-vscode/syntaxes/anders.tmLanguage.json +++ b/share/anders-vscode/syntaxes/anders.tmLanguage.json @@ -14,7 +14,7 @@ "name": "comment.line.double-dash.anders" }, { - "match": "(?<=^|[\\s()\\[\\]])(token|unsafe|macro|macrovariables|prefix|postfix|infix|infixr|infixl|#eval|#infer|#macroexpand|option|axiom|postulate|def|definition|theorem|lemma|corollary|proposition|import|with|begin|section|end|variables|let|in)(?=$|[\\s()\\[\\]])", + "match": "(?<=^|[\\s()\\[\\]])(token|unsafe|macro|macrovariables|prefix|postfix|infix|infixr|infixl|#eval|#infer|#macroexpand|option|opaque|axiom|postulate|def|definition|theorem|lemma|corollary|proposition|import|with|begin|section|end|variables|let|in)(?=$|[\\s()\\[\\]])", "name": "keyword.other.anders" }, { diff --git a/src/frontend/decl.ml b/src/frontend/decl.ml index 082940d..981247d 100644 --- a/src/frontend/decl.ml +++ b/src/frontend/decl.ml @@ -45,6 +45,7 @@ let rec checkLine conf = function | Infer e -> Printf.printf "INFER: %s\n" (Prettyprinter.showExp (infer e)); flush_all (); conf | Eval e -> Printf.printf "EVAL: %s\n" (Prettyprinter.showExp (eval e)); flush_all (); conf | Operator (op, prec, is) -> List.iter (fun i -> Parser.operators := Dict.add i (op, prec) !Parser.operators) is; conf + | Opaque x -> opaque x; conf | Decl d -> if !Prefs.verbose then begin Printf.printf "Checking: %s\n" (getDeclName d); flush_all () diff --git a/src/frontend/module.ml b/src/frontend/module.ml index 7583551..5301f91 100644 --- a/src/frontend/module.ml +++ b/src/frontend/module.ml @@ -13,29 +13,28 @@ type command = | Command of string * exp type decl = - | Def of string * exp option * exp - | Ext of string * exp * string + | Def of string * exp option * exp + | Ext of string * exp * string | Axiom of string * exp type associativity = Left | Right | Neither type operator = Infix of associativity | Prefix | Postfix type line = - | Operator of operator * float * string list - | Import of string list - | Plugin of string - | Option of string * string - | Variables of tele list + | Operator of operator * float * string list + | Import of string list + | Plugin of string + | Option of string * string + | Opaque of string + | Variables of tele list | Macrovariables of string list - | Token of string list - | Macro of bool * syntax * syntax - | Macroexpand of syntax - | Decl of decl - | Infer of exp - | Eval of exp - | Section | End - | Skip - | Eof + | Token of string list + | Macro of bool * syntax * syntax + | Macroexpand of syntax + | Decl of decl + | Infer of exp + | Eval of exp + | Section | End | Skip | Eof type content = line list type file = content @@ -86,6 +85,7 @@ let showLine = function | Plugin p -> Printf.sprintf "plugin %s" p | Option (opt, value) -> Printf.sprintf "option %s %s" opt value | Decl d -> showDecl d + | Opaque x -> Printf.sprintf "opaque %s" x | Section -> "section" | End -> "end" | Variables xs -> Printf.sprintf "variables%s" (showTeles xs) | Macrovariables is -> Printf.sprintf "macrovariables %s" (String.concat " " is) diff --git a/src/frontend/parser.ml b/src/frontend/parser.ml index 9696654..53695b0 100644 --- a/src/frontend/parser.ml +++ b/src/frontend/parser.ml @@ -434,7 +434,7 @@ let ws = str isWhitespace >> eps let nl = str (fun c -> c = '\n' || c = '\r') >> eps let keywords = ["def"; "definition"; "theorem"; "lemma"; "proposition"; "macro"; "import"; "prefix"; "postfix"; "infixl"; "infixr"; "infix"; "postulate"; "axiom"; - "macrovariables"; "option"; "unsafe"; "variables"; "section"; "end"; + "macrovariables"; "option"; "opaque"; "unsafe"; "variables"; "section"; "end"; "token"; "#macroexpand"; "#infer"; "#eval"; "--"; "{-"; "-}"] let reserved = ['('; ')'; '['; ']'; '<'; '>'; '\n'; '\t'; '\r'; ' '; '.'; ','] @@ -543,9 +543,10 @@ let tokens = token "token" >> ws >> sepBy1 ws ident >>= fun is -> pure ( let variables = token "variables" >> ws >> binders >>= fun bs -> pure (Variables bs) let import = token "import" >> ws >> sepBy1 ws ident >>= fun fs -> pure (Import fs) let options = token "option" >> ws >> ident >>= fun i -> ws >> ident >>= fun v -> pure (Option (i, v)) +let opaque = token "opaque" >> ws >> ident >>= fun x -> pure (Opaque x) let section = (token "section" >> pure Section) <|> (token "end" >> pure End) -let commands = import <|> variables <|> options <|> operator <|> macroexpand <|> infer <|> eval <|> macrovariables <|> tokens +let commands = import <|> variables <|> options <|> opaque <|> operator <|> macroexpand <|> infer <|> eval <|> macrovariables <|> tokens let cmdeof = eof >> pure Eof let cmdline = def <|> axm <|> macro <|> commands <|> section <|> comment <|> cmdeof let cmd = optional ws >> cmdline diff --git a/src/frontend/radio.ml b/src/frontend/radio.ml index c6ba22a..a4ff37a 100644 --- a/src/frontend/radio.ml +++ b/src/frontend/radio.ml @@ -78,6 +78,7 @@ let transmit mesg = let def p t e = transmit (Def (p, t, e)) let assign p t e = transmit (Assign (p, t, e)) let assume p t = transmit (Assume (p, t)) +let opaque x = transmit (Opaque x) let set p x = transmit (Set (p, x)) let wipe () = transmit Wipe diff --git a/src/kernel/check.ml b/src/kernel/check.ml index fa13f72..cb0108f 100644 --- a/src/kernel/check.ml +++ b/src/kernel/check.ml @@ -364,16 +364,28 @@ and app (f, x) = match f, x with and evalSystem ctx = bimap (getDef ctx) (fun mu t -> eval (faceEnv mu ctx) t) -and getType ctx x = match Env.find_opt x ctx.local, Env.find_opt x !(ctx.global) with +and evalTerm ctx = function + | Exp e -> eval ctx e + | Value v -> v + +and getType ctx x = + match Env.find_opt x ctx.local, Env.find_opt x !(ctx.global) with | Some (t, _), _ -> t - | _, Some (t, _) -> t + | _, Some t -> evalTerm ctx t.typval | _, _ -> raise (Internal (VariableNotFound x)) -and getDef ctx x = match Env.find_opt x ctx.local, Env.find_opt x !(ctx.global) with - | Some (_, v), _ -> v - | _, Some (_, Value v) -> v - | _, Some (t, Exp e) -> let v = eval ctx e in upGlobal ctx x t (Value v); v - | _, _ -> raise (Internal (VariableNotFound x)) +and getGlobalDef ctx x = + match Env.find_opt x !(ctx.global) with + | None -> raise (Internal (VariableNotFound x)) + | Some t -> + if t.opaque then Var (x, evalTerm ctx t.typval) + else match t.defval with + | Value v -> v + | Exp e -> let v = eval ctx e in upGlobal ctx x { t with defval = Value v }; v + +and getDef ctx x = match Env.find_opt x ctx.local with + | Some (_, v) -> v + | None -> getGlobalDef ctx x and appFormulaE ctx e i = eval ctx (EAppFormula (e, i)) diff --git a/src/kernel/chm.ml b/src/kernel/chm.ml index e075a8c..a85d94e 100644 --- a/src/kernel/chm.ml +++ b/src/kernel/chm.ml @@ -32,13 +32,17 @@ let proto : req -> resp = function | Def (x, t0, e0) -> promote (fun () -> let t = freshExp t0 in let e = freshExp e0 in isType (infer ctx t); let t' = eval ctx t in - check ctx e t'; assign ctx x t' (getTerm e); OK) + check ctx e t'; assign ctx x (Value t') (getTerm e); OK) + | Opaque x -> let y = ident x in + promote (fun () -> match Env.find_opt y !(ctx.global) with + | Some t -> upGlobal ctx y { t with opaque = true }; OK + | None -> Error (VariableNotFound y)) | Assign (x, t0, e0) -> promote (fun () -> let t = freshExp t0 in isType (infer ctx t); - assign ctx x (eval ctx t) (getTerm (freshExp e0)); OK) + assign ctx x (Value (eval ctx t)) (getTerm (freshExp e0)); OK) | Assume (x, t0) -> promote (fun () -> let t = freshExp t0 in isType (infer ctx t); let t' = eval ctx t in - assign ctx x t' (Value (Var (ident x, t'))); OK) + assign ctx x (Value t') (Value (Var (ident x, t'))); OK) | Erase x -> ctx.global := Env.remove (ident x) !(ctx.global); OK | Wipe -> ctx.global := Env.empty; OK | Set (p, x) -> diff --git a/src/kernel/term.ml b/src/kernel/term.ml index 49fd4cb..1bf7197 100644 --- a/src/kernel/term.ml +++ b/src/kernel/term.ml @@ -74,9 +74,11 @@ and clos = ident * (value -> value) type term = Exp of exp | Value of value +type decl = { typval : term; defval : term; opaque : bool } + type ctx = { local : (value * value) Env.t; - global : (value * term) Env.t ref } + global : decl Env.t ref } (* Implementation *) @@ -103,12 +105,12 @@ exception IncompatibleFaces let upVar p x ctx = match p with Irrefutable -> ctx | _ -> Env.add p x ctx let upLocal ctx p t v = { ctx with local = upVar p (t, v) ctx.local } -let upGlobal ctx p t v = ctx.global := upVar p (t, v) !(ctx.global) +let upGlobal ctx p t = ctx.global := upVar p t !(ctx.global) let assign ctx x t e = if Env.mem (ident x) !(ctx.global) then raise (Internal (AlreadyDeclared x)) - else upGlobal ctx (ident x) t e + else upGlobal ctx (ident x) { typval = t; defval = e; opaque = false } let freshVar ns n = match Env.find_opt n ns with Some x -> x | None -> n let mapFace fn phi = Env.fold (fun p d -> Env.add (fn p) d) phi Env.empty diff --git a/src/language/decode.ml b/src/language/decode.ml index b114272..5fe2dd7 100644 --- a/src/language/decode.ml +++ b/src/language/decode.ml @@ -144,7 +144,8 @@ struct | '\x21' -> let x = string () in let (t, e) = exp2 () in Assign (x, t, e) | '\x22' -> let x = string () in let t = exp () in Assume (x, t) | '\x23' -> Erase (string ()) - | '\x24' -> Wipe + | '\x24' -> Opaque (string ()) + | '\x25' -> Wipe | '\x30' -> let p = string () in let x = string () in Set (p, x) | '\x31' -> Version | '\x32' -> Ping diff --git a/src/language/encode.ml b/src/language/encode.ml index 0e470e2..eb0d5eb 100644 --- a/src/language/encode.ml +++ b/src/language/encode.ml @@ -133,7 +133,8 @@ struct | Assign (x, t, e) -> W.put '\x21'; string x; exp2 t e | Assume (x, t) -> W.put '\x22'; string x; exp t | Erase x -> W.put '\x23'; string x - | Wipe -> W.put '\x24' + | Opaque x -> W.put '\x24'; string x + | Wipe -> W.put '\x25' | Set (p, x) -> W.put '\x30'; string p; string x | Version -> W.put '\x31' | Ping -> W.put '\x32' diff --git a/src/language/spec.ml b/src/language/spec.ml index e023249..3fad3f4 100644 --- a/src/language/spec.ml +++ b/src/language/spec.ml @@ -119,6 +119,7 @@ type req = | Assign of string * exp * exp | Assume of string * exp | Erase of string + | Opaque of string | Wipe (* configuration *) | Set of string * string