Skip to content

Commit d7405d1

Browse files
johnchandlerburnhamjohnchandlerburnham
committed
fixup for comments and clippy
1 parent dff99c9 commit d7405d1

File tree

12 files changed

+3171
-3445
lines changed

12 files changed

+3171
-3445
lines changed

‎Ix/Common.lean‎

Lines changed: 0 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -177,88 +177,6 @@ def joinM [Monad μ] : List (List α) → μ (List α)
177177
| [] => return []
178178
| a :: as => do return a ++ (← joinM as)
179179

180-
-- Combined sort and group operations over (List (List α))
181-
182-
-- Merge two sorted lists of groups, combining groups with equal elements
183-
partial def mergeGroupsM [Monad μ] (cmp : α → α → μ Ordering)
184-
: List (List α) → List (List α) → μ (List (List α))
185-
| gs@((g@(a::_))::gs'), hs@((h@(b::_))::hs') => do
186-
match (← cmp a b) with
187-
| Ordering.lt => List.cons g <$> mergeGroupsM cmp gs' hs
188-
| Ordering.gt => List.cons h <$> mergeGroupsM cmp gs hs'
189-
| Ordering.eq => List.cons (g ++ h) <$> mergeGroupsM cmp gs' hs' -- Combine equal groups
190-
| [], hs => return hs
191-
| gs, [] => return gs
192-
| _, _ => return []
193-
194-
-- Merge pairs of grouped lists
195-
def mergePairsGroupsM [Monad μ] (cmp: α → α → μ Ordering)
196-
: List (List (List α)) → μ (List (List (List α)))
197-
| a::b::xs => List.cons <$> (mergeGroupsM cmp a b) <*> mergePairsGroupsM cmp xs
198-
| xs => return xs
199-
200-
-- Merge all grouped lists
201-
partial def mergeAllGroupsM [Monad μ] (cmp: α → α → μ Ordering)
202-
: List (List (List α)) → μ (List (List α))
203-
| [] => return []
204-
| [x] => return x
205-
| xs => mergePairsGroupsM cmp xs >>= mergeAllGroupsM cmp
206-
207-
-- Helper to collect equal consecutive elements into a group
208-
def collectEqualM [Monad μ] (cmp : α → α → μ Ordering) (x : α)
209-
: List α → μ (List α × List α)
210-
| y::ys => do
211-
if (← cmp x y) == Ordering.eq
212-
then do
213-
let (group, rest) ← collectEqualM cmp x ys
214-
return (y::group, rest)
215-
else return ([x], y::ys)
216-
| [] => return ([x], [])
217-
218-
mutual
219-
-- Build sequences of groups (ascending/descending runs with grouping)
220-
partial def sequencesGroupedM [Monad μ] (cmp : α → α → μ Ordering)
221-
: List α → μ (List (List (List α)))
222-
| [] => return []
223-
| a::xs => do
224-
let (aGroup, rest) ← collectEqualM cmp a xs
225-
match rest with
226-
| [] => return [[aGroup]]
227-
| b::bs => do
228-
let (bGroup, rest') ← collectEqualM cmp b bs
229-
if (← cmp a b) == .gt
230-
then descendingGroupedM cmp b bGroup [aGroup] rest'
231-
else ascendingGroupedM cmp b bGroup (fun gs => aGroup :: gs) rest'
232-
233-
partial def descendingGroupedM [Monad μ]
234-
(cmp : α → α → μ Ordering) (rep : α) (curr : List α) (acc : List (List α))
235-
: List α → μ (List (List (List α)))
236-
| [] => return [curr::acc]
237-
| x::xs => do
238-
let (xGroup, rest) ← collectEqualM cmp x xs
239-
if (← cmp rep x) == .gt
240-
then descendingGroupedM cmp x xGroup (curr::acc) rest
241-
else List.cons (curr::acc) <$> sequencesGroupedM cmp (x::xs)
242-
243-
partial def ascendingGroupedM [Monad μ]
244-
(cmp : α → α → μ Ordering) (rep : α) (curr : List α)
245-
(acc : List (List α) → List (List α))
246-
: List α → μ (List (List (List α)))
247-
| [] => return [acc [curr]]
248-
| x::xs => do
249-
let (xGroup, rest) ← collectEqualM cmp x xs
250-
if (← cmp rep x) != .gt
251-
then ascendingGroupedM cmp x xGroup (fun gs => acc (curr :: gs)) rest
252-
else List.cons (acc [curr]) <$> sequencesGroupedM cmp (x::xs)
253-
end
254-
255-
def sortAndGroupByM [Monad μ] (xs: List α) (cmp: α -> α -> μ Ordering)
256-
: μ (List (List α)) :=
257-
sequencesGroupedM cmp xs >>= mergeAllGroupsM cmp
258-
259-
def sortGroupsByM [Monad μ] (xs: List (List α)) (cmp: α -> α -> μ Ordering)
260-
: μ (List (List α)) := sortAndGroupByM xs.flatten cmp
261-
262180
end List
263181

264182
def Std.HashMap.find? {A B} [BEq A] [Hashable A] (map: Std.HashMap A B) (a: A)

‎Ix/Ixon.lean‎

Lines changed: 3 additions & 219 deletions
Original file line numberDiff line numberDiff line change
@@ -842,10 +842,10 @@ inductive Ixon where
842842
| rprj : RecursorProj -> Ixon -- 0xA5, recr projection
843843
| iprj : InductiveProj -> Ixon -- 0xA6, indc projection
844844
| dprj : DefinitionProj -> Ixon -- 0xA7, defn projection
845-
| muts : List MutConst -> Ixon -- 0xBX, mutual inductive types
845+
| muts : List MutConst -> Ixon -- 0xBX, mutual constants
846846
| prof : Proof -> Ixon -- 0xE0, zero-knowledge proof
847-
| eval : EvalClaim -> Ixon -- 0xE1, cryptographic claim
848-
| chck : CheckClaim -> Ixon -- 0xE2, cryptographic claim
847+
| eval : EvalClaim -> Ixon -- 0xE1, evaluation claim
848+
| chck : CheckClaim -> Ixon -- 0xE2, typechecking claim
849849
| comm : Comm -> Ixon -- 0xE3, cryptographic commitment
850850
| envn : Env -> Ixon -- 0xE4, Lean4 environment
851851
| prim : BuiltIn -> Ixon -- 0xE5, compiler builtins
@@ -949,220 +949,4 @@ instance : Serialize Ixon where
949949

950950
def Ixon.address (ixon: Ixon): Address := Address.blake3 (ser ixon)
951951

952-
953-
--
954-
----section FFI
955-
----
956-
----/--
957-
----# Ixon FFI types
958-
----
959-
----This section defines FFI-friendly versions of the original Ixon datatypes by
960-
----* Replacing `Nat` by `ByteArray` containing the corresponding bytes in LE
961-
----* Replacing `List` by `Array`
962-
----* Replacing maps by `Array`s of pairs
963-
-----/
964-
----
965-
----@[inline] def nat2Bytes (n : Nat) : ByteArray :=
966-
---- ⟨natToBytesLE n⟩
967-
----
968-
----structure DefinitionFFI where
969-
---- kind: Ix.DefKind
970-
---- safety : Lean.DefinitionSafety
971-
---- lvls : ByteArray
972-
---- type : Address
973-
---- value : Address
974-
----
975-
----def Definition.toFFI : Definition → DefinitionFFI
976-
---- | ⟨kind, safety, lvls, type, value⟩ =>
977-
---- ⟨kind, safety, nat2Bytes lvls, type, value⟩
978-
----
979-
----structure AxiomFFI where
980-
---- lvls : ByteArray
981-
---- type : Address
982-
---- isUnsafe: Bool
983-
----
984-
----def Axiom.toFFI : Axiom → AxiomFFI
985-
---- | ⟨isUnsafe, lvls, type⟩ => ⟨nat2Bytes lvls, type, isUnsafe⟩
986-
----
987-
----structure QuotientFFI where
988-
---- lvls : ByteArray
989-
---- type : Address
990-
---- kind : Lean.QuotKind
991-
----
992-
----def Quotient.toFFI : Quotient → QuotientFFI
993-
---- | ⟨kind, lvls, type⟩ => ⟨nat2Bytes lvls, type, kind⟩
994-
----
995-
----structure ConstructorProjFFI where
996-
---- block : Address
997-
---- idx : ByteArray
998-
---- cidx : ByteArray
999-
----
1000-
----def ConstructorProj.toFFI : ConstructorProj → ConstructorProjFFI
1001-
---- | ⟨idx, cidx, block⟩ => ⟨block, nat2Bytes idx, nat2Bytes cidx⟩
1002-
----
1003-
----structure RecursorProjFFI where
1004-
---- block : Address
1005-
---- idx : ByteArray
1006-
---- ridx : ByteArray
1007-
----
1008-
----def RecursorProj.toFFI : RecursorProj → RecursorProjFFI
1009-
---- | ⟨idx, ridx, block⟩ => ⟨block, nat2Bytes idx, nat2Bytes ridx⟩
1010-
----
1011-
----structure InductiveProjFFI where
1012-
---- block : Address
1013-
---- idx : ByteArray
1014-
----
1015-
----def InductiveProj.toFFI : InductiveProj → InductiveProjFFI
1016-
---- | ⟨idx, block⟩ => ⟨block, nat2Bytes idx⟩
1017-
----
1018-
----structure DefinitionProjFFI where
1019-
---- block : Address
1020-
---- idx : ByteArray
1021-
----
1022-
----def DefinitionProj.toFFI : DefinitionProj → DefinitionProjFFI
1023-
---- | ⟨idx, block⟩ => ⟨block, nat2Bytes idx⟩
1024-
----
1025-
----structure RecursorRuleFFI where
1026-
---- fields : ByteArray
1027-
---- rhs : Address
1028-
----
1029-
----def RecursorRule.toFFI : RecursorRule → RecursorRuleFFI
1030-
---- | ⟨fields, rhs⟩ => ⟨nat2Bytes fields, rhs⟩
1031-
----
1032-
----structure RecursorFFI where
1033-
---- lvls : ByteArray
1034-
---- type : Address
1035-
---- params : ByteArray
1036-
---- indices : ByteArray
1037-
---- motives : ByteArray
1038-
---- minors : ByteArray
1039-
---- rules : Array RecursorRuleFFI
1040-
---- k : Bool
1041-
---- isUnsafe: Bool
1042-
----
1043-
----def Recursor.toFFI : Recursor → RecursorFFI
1044-
---- | ⟨k, isUnsafe, lvls, params, indices, motives, minors, type, rules⟩ =>
1045-
---- ⟨nat2Bytes lvls, type, nat2Bytes params, nat2Bytes indices,
1046-
---- nat2Bytes motives, nat2Bytes minors, rules.toArray.map RecursorRule.toFFI,
1047-
---- k, isUnsafe⟩
1048-
----
1049-
----structure ConstructorFFI where
1050-
---- lvls : ByteArray
1051-
---- type : Address
1052-
---- cidx : ByteArray
1053-
---- params : ByteArray
1054-
---- fields : ByteArray
1055-
---- isUnsafe: Bool
1056-
----
1057-
----def Constructor.toFFI : Constructor → ConstructorFFI
1058-
---- | ⟨isUnsafe, lvls, cidx, params, fields, type⟩ =>
1059-
---- ⟨nat2Bytes lvls, type, nat2Bytes cidx, nat2Bytes params, nat2Bytes fields, isUnsafe⟩
1060-
----
1061-
----structure InductiveFFI where
1062-
---- lvls : ByteArray
1063-
---- type : Address
1064-
---- params : ByteArray
1065-
---- indices : ByteArray
1066-
---- ctors : Array ConstructorFFI
1067-
---- recrs : Array RecursorFFI
1068-
---- nested : ByteArray
1069-
---- recr : Bool
1070-
---- refl : Bool
1071-
---- isUnsafe: Bool
1072-
----
1073-
----def Inductive.toFFI : Inductive → InductiveFFI
1074-
---- | ⟨recr, refl, isUnsafe, lvls, params, indices, nested, type, ctors, recrs⟩ =>
1075-
---- ⟨nat2Bytes lvls, type, nat2Bytes params, nat2Bytes indices,
1076-
---- ctors.toArray.map Constructor.toFFI, recrs.toArray.map Recursor.toFFI,
1077-
---- nat2Bytes nested, recr, refl, isUnsafe⟩
1078-
----
1079-
----inductive NameFFI
1080-
---- | anonymous
1081-
---- | str : NameFFI → String → NameFFI
1082-
---- | num : NameFFI → ByteArray → NameFFI
1083-
----
1084-
----def _root_.Lean.Name.toFFI : Lean.Name → NameFFI
1085-
---- | .anonymous => .anonymous
1086-
---- | .str name s => .str name.toFFI s
1087-
---- | .num name n => .num name.toFFI (nat2Bytes n)
1088-
----
1089-
----inductive MetadatumFFI where
1090-
----| name : NameFFI -> MetadatumFFI
1091-
----| info : Lean.BinderInfo -> MetadatumFFI
1092-
----| link : Address -> MetadatumFFI
1093-
----| hints : Lean.ReducibilityHints -> MetadatumFFI
1094-
----| all : Array NameFFI -> MetadatumFFI
1095-
----| mutCtx : Array (Array NameFFI) -> MetadatumFFI
1096-
----
1097-
----def Metadatum.toFFI : Metadatum → MetadatumFFI
1098-
---- | .name n => .name n.toFFI
1099-
---- | .info i => .info i
1100-
---- | .link addr => .link addr
1101-
---- | .hints h => .hints h
1102-
---- | .all ns => .all (ns.toArray.map Lean.Name.toFFI)
1103-
---- | .mutCtx ctx => .mutCtx $ ctx.toArray.map (·.toArray.map Lean.Name.toFFI)
1104-
----
1105-
----inductive IxonFFI where
1106-
----| vari : UInt64 -> IxonFFI
1107-
----| refr : Address -> Array Univ -> IxonFFI
1108-
----| recr : UInt64 -> Array Univ -> IxonFFI
1109-
----| proj : Address -> UInt64 -> Address -> IxonFFI
1110-
----| sort : Univ -> IxonFFI
1111-
----| strl : Address -> IxonFFI
1112-
----| natl : Address -> IxonFFI
1113-
----| appl : Address -> Address -> IxonFFI
1114-
----| lamb : Address -> Address -> IxonFFI
1115-
----| allE : Address -> Address -> IxonFFI
1116-
----| letE : Address -> Address -> Address -> IxonFFI
1117-
----| letD : Address -> Address -> Address -> IxonFFI
1118-
----| list : Array IxonFFI -> IxonFFI
1119-
----| defn : DefinitionFFI -> IxonFFI
1120-
----| axio : AxiomFFI -> IxonFFI
1121-
----| quot : QuotientFFI -> IxonFFI
1122-
----| cprj : ConstructorProjFFI -> IxonFFI
1123-
----| rprj : RecursorProjFFI -> IxonFFI
1124-
----| iprj : InductiveProjFFI -> IxonFFI
1125-
----| dprj : DefinitionProjFFI -> IxonFFI
1126-
----| inds : Array InductiveFFI -> IxonFFI
1127-
----| defs : Array DefinitionFFI -> IxonFFI
1128-
----| meta : Array (ByteArray × (Array MetadatumFFI)) -> IxonFFI
1129-
----| prof : Proof -> IxonFFI
1130-
----| eval : EvalClaim -> IxonFFI
1131-
----| chck : CheckClaim -> IxonFFI
1132-
----| comm : Comm -> IxonFFI
1133-
----| envn : Array (Address × Address) -> IxonFFI
1134-
----
1135-
----def Ixon.toFFI : Ixon → IxonFFI
1136-
---- | .vari i => .vari i
1137-
---- | .sort u => .sort u
1138-
---- | .refr addr univs => .refr addr univs.toArray
1139-
---- | .recr i us => .recr i us.toArray
1140-
---- | .appl f a => .appl f a
1141-
---- | .lamb t b => .lamb t b
1142-
---- | .allE t b => .allE t b
1143-
---- | .proj addr i x => .proj addr i x
1144-
---- | .strl s => .strl s
1145-
---- | .natl n => .natl n
1146-
---- | .letE v t b => .letE v t b
1147-
---- | .letD v t b => .letD v t b
1148-
---- | .list xs => .list (xs.map Ixon.toFFI).toArray
1149-
---- | .defn d => .defn d.toFFI
1150-
---- | .axio a => .axio a.toFFI
1151-
---- | .quot q => .quot q.toFFI
1152-
---- | .cprj c => .cprj c.toFFI
1153-
---- | .rprj r => .rprj r.toFFI
1154-
---- | .iprj i => .iprj i.toFFI
1155-
---- | .dprj d => .dprj d.toFFI
1156-
---- | .inds is => .inds (is.map Inductive.toFFI).toArray
1157-
---- | .defs d => .defs (d.map Definition.toFFI).toArray
1158-
---- | .meta ⟨map⟩ => .meta $ map.toArray.map
1159-
---- fun (x, y) => (nat2Bytes x, y.toArray.map Metadatum.toFFI)
1160-
---- | .prof p => .prof p
1161-
---- | .eval x => .eval x
1162-
---- | .chck x => .chck x
1163-
---- | .comm x => .comm x
1164-
---- | .envn x => .envn x.env.toArray
1165-
----
1166-
----end FFI
1167-
--
1168952
end Ixon

0 commit comments

Comments
 (0)