+17 -3

Main.lean

View file Reviewed

··· 18 18 | _ => judgment 19 19 | _ => judgment 20 20 21 21 + def renderValueForJudgment (value : Value) (judgment : Judgment) : String := 22 22 + match judgment.ty, value with 23 23 + | .decimal, .number (.exact q) => renderDecimal q 24 24 + | .int, .number (.exact q) => 25 25 + if q.den = 1 then toString q.num else renderValue value 26 26 + | _, _ => renderValue value 27 27 + 28 28 + def renderNumericStability (value : Value) (judgment : Judgment) : String := 29 29 + match judgment.ty with 30 30 + | .number => 31 31 + s!" [rational={rationalStabilityOfValue value}, decimal={decimalStabilityOfValue value}]" 32 32 + | _ => "" 33 33 + 21 34 def renderResult (value : Value) (judgment : Judgment) : String := 22 22 - s!"{renderValue value} : {renderJudgment (refineJudgmentFromValue value judgment)}" 35 35 + let refined := refineJudgmentFromValue value judgment 36 36 + s!"{renderValueForJudgment value refined} : {renderJudgment refined}{renderNumericStability value refined}" 23 37 24 38 unsafe def checkExprsWith (tyEnv : TyEnv) (env : Env) (exprs : List Expr) : IO (Except String (List (Value × Judgment))) := do 25 39 let rec loop (pending : List Expr) (acc : List (Value × Judgment)) : IO (Except String (List (Value × Judgment))) := do ··· 28 42 | expr :: rest => 29 43 match inferType tyEnv expr with 30 44 | .error err => 31 31 - pure (.error s!"type error: {reprStr err}") 45 45 + pure (.error s!"type error: {renderTypeError err}") 32 46 | .ok judgment => 33 47 match (← (eval env expr).toIO') with 34 48 | .ok value => ··· 86 100 | .bind name value => 87 101 match inferType tyEnv value with 88 102 | .error err => 89 89 - IO.eprintln s!"type error: {reprStr err}" 103 103 + IO.eprintln s!"type error: {renderTypeError err}" 90 104 repl tyEnv env 91 105 | .ok judgment => 92 106 match (← (eval env value).toIO') with

+1

Mlang/Http.lean

View file Reviewed

··· 1 1 namespace Mlang.Http 2 2 3 3 @[extern "mlang_http_get"] opaque httpGet (url : @& String) : IO String 4 4 + @[extern "mlang_aturi_parse_string"] opaque parseAturi (source : @& String) : IO String 4 5 5 6 end Mlang.Http

+945 -84

Mlang/Interpreter.lean

View file Reviewed

··· 7 7 open Nickel 8 8 9 9 abbrev Name := String 10 10 + structure Rational where 11 11 + num : Int 12 12 + den : Nat 13 13 + deriving Repr, Inhabited, BEq 14 14 + 15 15 + abbrev Decimal := Rational 16 16 + 17 17 + mutual 18 18 + inductive Generator where 19 19 + | exactRatio : Rational → Generator 20 20 + | exactDecimal : Decimal → Generator 21 21 + | rationalRefiner : LazyReal → Generator 22 22 + | decimalRefiner : LazyReal → Generator 23 23 + | piChudnovsky : Generator 24 24 + | sqrt : Decimal → Generator 25 25 + | add : Generator → Generator → Generator 26 26 + | sub : Generator → Generator → Generator 27 27 + | mul : Generator → Generator → Generator 28 28 + | div : Generator → Generator → Generator 29 29 + deriving Repr, Inhabited, BEq 30 30 + 31 31 + inductive LazyReal where 32 32 + | exact : Decimal → LazyReal 33 33 + | ratioProcess : Rational → LazyReal 34 34 + | decimalProcess : Decimal → LazyReal 35 35 + | pi : LazyReal 36 36 + | sqrt : Decimal → LazyReal 37 37 + | add : LazyReal → LazyReal → LazyReal 38 38 + | sub : LazyReal → LazyReal → LazyReal 39 39 + | mul : LazyReal → LazyReal → LazyReal 40 40 + | div : LazyReal → LazyReal → LazyReal 41 41 + | generated : Generator → LazyReal 42 42 + deriving Repr, Inhabited, BEq 43 43 + end 44 44 + 45 45 + def normalizeDecimalParts (negative : Bool) (whole frac : String) : String := 46 46 + let wholeChars := whole.toList.dropWhile (· = '0') 47 47 + let whole' := if wholeChars.isEmpty then "0" else String.ofList wholeChars 48 48 + let fracChars := frac.toList.reverse.dropWhile (· = '0') |>.reverse 49 49 + let frac' := if fracChars.isEmpty then "0" else String.ofList fracChars 50 50 + let sign := if negative && !(whole' = "0" && frac' = "0") then "-" else "" 51 51 + sign ++ whole' ++ "." ++ frac' 52 52 + 53 53 + def parseDecimalParts (repr : String) : Bool × String × String := 54 54 + let chars := repr.toList 55 55 + let (negative, chars) := 56 56 + match chars with 57 57 + | '-' :: rest => (true, rest) 58 58 + | _ => (false, chars) 59 59 + let rec split (acc : List Char) : List Char → List Char × List Char 60 60 + | [] => (acc.reverse, []) 61 61 + | '.' :: rest => (acc.reverse, rest) 62 62 + | c :: rest => split (c :: acc) rest 63 63 + let (wholeChars, fracChars) := split [] chars 64 64 + (negative, String.ofList wholeChars, String.ofList fracChars) 65 65 + 66 66 + def pow10 : Nat → Int 67 67 + | 0 => 1 68 68 + | n + 1 => 10 * pow10 n 69 69 + 70 70 + def powNat (base : Nat) : Nat → Nat 71 71 + | 0 => 1 72 72 + | n + 1 => base * powNat base n 73 73 + 74 74 + def mkRational (num : Int) (den : Nat) : Rational := 75 75 + if den = 0 then 76 76 + { num := 0, den := 1 } 77 77 + else if num = 0 then 78 78 + { num := 0, den := 1 } 79 79 + else 80 80 + let g := Nat.gcd num.natAbs den 81 81 + { num := num / Int.ofNat g, den := den / g } 82 82 + 83 83 + def parseDecimal (repr : String) : Decimal := 84 84 + let (negative, whole, frac) := parseDecimalParts repr 85 85 + let digits := whole ++ frac 86 86 + let magnitude := String.toInt? digits |>.getD 0 87 87 + let signed := if negative then -magnitude else magnitude 88 88 + mkRational signed (powNat 10 frac.length) 89 89 + 90 90 + def renderDecimalScaled (scaled : Int) (scale : Nat) : String := 91 91 + let negative := scaled < 0 92 92 + let mag := scaled.natAbs 93 93 + let digits := toString mag 94 94 + if scale = 0 then 95 95 + normalizeDecimalParts negative digits "0" 96 96 + else if digits.length <= scale then 97 97 + let zeros := String.ofList (List.replicate (scale - digits.length + 1) '0') 98 98 + let padded := zeros ++ digits 99 99 + let wholeLen := padded.length - scale 100 100 + normalizeDecimalParts negative (padded.take wholeLen |>.toString) (padded.drop wholeLen |>.toString) 101 101 + else 102 102 + let wholeLen := digits.length - scale 103 103 + normalizeDecimalParts negative (digits.take wholeLen |>.toString) (digits.drop wholeLen |>.toString) 104 104 + 105 105 + def decimalOfInt (n : Int) : Decimal := 106 106 + mkRational n 1 107 107 + 108 108 + def addDecimals (lhs rhs : Decimal) : Decimal := 109 109 + mkRational (lhs.num * Int.ofNat rhs.den + rhs.num * Int.ofNat lhs.den) (lhs.den * rhs.den) 110 110 + 111 111 + def subDecimals (lhs rhs : Decimal) : Decimal := 112 112 + mkRational (lhs.num * Int.ofNat rhs.den - rhs.num * Int.ofNat lhs.den) (lhs.den * rhs.den) 113 113 + 114 114 + def mulDecimals (lhs rhs : Decimal) : Decimal := 115 115 + mkRational (lhs.num * rhs.num) (lhs.den * rhs.den) 116 116 + 117 117 + def rationalEq (lhs rhs : Decimal) : Bool := 118 118 + lhs.num == rhs.num && lhs.den == rhs.den 119 119 + 120 120 + partial def countFactor (factor : Nat) (n : Nat) : Nat := 121 121 + let rec loop (count current : Nat) := 122 122 + if current = 0 then count 123 123 + else if current % factor = 0 then loop (count + 1) (current / factor) 124 124 + else count 125 125 + loop 0 n 126 126 + 127 127 + partial def stripFactor (factor : Nat) (n : Nat) : Nat := 128 128 + let rec loop (current : Nat) := 129 129 + if current = 0 then 0 130 130 + else if current % factor = 0 then loop (current / factor) 131 131 + else current 132 132 + loop n 133 133 + 134 134 + def renderDecimal (d : Decimal) : String := 135 135 + if d.den = 1 then 136 136 + renderDecimalScaled d.num 0 137 137 + else 138 138 + let twos := countFactor 2 d.den 139 139 + let withoutTwos := stripFactor 2 d.den 140 140 + let fives := countFactor 5 withoutTwos 141 141 + let rest := stripFactor 5 withoutTwos 142 142 + if rest = 1 then 143 143 + let scale := max twos fives 144 144 + let mult2 := powNat 2 (scale - twos) 145 145 + let mult5 := powNat 5 (scale - fives) 146 146 + let scaledNum := d.num * Int.ofNat (mult2 * mult5) 147 147 + renderDecimalScaled scaledNum scale 148 148 + else 149 149 + s!"{d.num}/{d.den}" 150 150 + 151 151 + def isTerminatingDecimal (q : Rational) : Bool := 152 152 + if q.den = 1 then 153 153 + true 154 154 + else 155 155 + let withoutTwos := stripFactor 2 q.den 156 156 + let withoutFives := stripFactor 5 withoutTwos 157 157 + withoutFives = 1 10 158 11 159 inductive Effect where 12 160 | error : Effect ··· 36 184 "{" ++ String.intercalate ", " names ++ "}" 37 185 38 186 inductive Ty where 187 187 + | number : Ty 39 188 | int : Ty 189 189 + | decimal : Ty 190 190 + | rational : Ty 191 191 + | lazyReal : Ty 192 192 + | stability : Ty 40 193 | bool : Ty 41 194 | string : Ty 42 195 | data : Ty 43 196 | dataInt : Ty 197 197 + | dataDecimal : Ty 198 198 + | dataRational : Ty 44 199 | dataBool : Ty 45 200 | dataString : Ty 46 201 | dataNull : Ty ··· 56 211 | null : Data 57 212 | bool : Bool → Data 58 213 | int : Int → Data 214 214 + | decimal : Decimal → Data 59 215 | string : String → Data 60 216 | array : List Data → Data 61 217 | record : List (String × Data) → Data ··· 63 219 64 220 inductive Expr where 65 221 | int : Int → Expr 222 222 + | decimal : Decimal → Expr 66 223 | bool : Bool → Expr 67 224 | string : String → Expr 68 225 | null : Expr ··· 81 238 | lam : Name → Ty → Expr → Expr 82 239 | app : Expr → Expr → Expr 83 240 deriving Repr, Inhabited 241 241 + 242 242 + inductive Numeric where 243 243 + | exact : Rational → Numeric 244 244 + | composite : LazyReal → Numeric 245 245 + deriving Repr, Inhabited, BEq 84 246 85 247 inductive Value where 86 86 - | int : Int → Value 248 248 + | number : Numeric → Value 249 249 + | stability : String → Value 87 250 | bool : Bool → Value 88 251 | string : String → Value 89 252 | data : Data → Value ··· 96 259 | builtinReadFileNickel : Value 97 260 | builtinParseNickel : Value 98 261 | builtinParseJson : Value 262 262 + | builtinGetAturi : Value 99 263 | builtinDataGet : Value 100 100 - | builtinDataGetField : Data → Value 264 264 + | builtinDataGetField : Value → Value 101 265 | builtinDataAt : Value 102 102 - | builtinDataAtIndex : Data → Value 266 266 + | builtinDataAtIndex : Value → Value 103 267 | builtinDataAsInt : Value 268 268 + | builtinDataAsDecimal : Value 269 269 + | builtinRationalToInt : Value 270 270 + | builtinRationalToDecimal : Value 104 271 | builtinDataAsString : Value 105 272 | builtinDataAsBool : Value 106 273 | builtinDataToJson : Value 107 274 | builtinDataToNickel : Value 275 275 + | builtinSqrt : Value 276 276 + | builtinProcess : Value 277 277 + | builtinSynthesize : Value 278 278 + | builtinFormula : Value 279 279 + | builtinApprox : Value 280 280 + | builtinApproxStep : Value → Value 281 281 + | builtinStabilize : Value 282 282 + | builtinStabilizeStep : Value → Value 283 283 + | builtinBounds : Value 284 284 + | builtinBoundsStep : Value → Value 285 285 + | builtinRationalStability : Value 286 286 + | builtinDecimalStability : Value 108 287 | closure : Name → Expr → List (Name × Value) → Value 109 288 deriving Repr, Inhabited 110 289 111 290 abbrev Env := List (Name × Value) 112 291 292 292 + inductive Observation where 293 293 + | asRational : Observation 294 294 + | asDecimal : Observation 295 295 + | asInt : Observation 296 296 + | rationalStability : Observation 297 297 + | decimalStability : Observation 298 298 + | getField : String → Observation 299 299 + | atIndex : Nat → Observation 300 300 + | approx : Nat → Observation 301 301 + | bounds : Nat → Observation 302 302 + deriving Repr, Inhabited 303 303 + 304 304 + inductive ObservationResult where 305 305 + | rational : Rational → ObservationResult 306 306 + | decimal : Decimal → ObservationResult 307 307 + | int : Int → ObservationResult 308 308 + | stability : String → ObservationResult 309 309 + | data : Data → ObservationResult 310 310 + | bounds : Decimal → Decimal → ObservationResult 311 311 + deriving Repr, Inhabited 312 312 + 113 313 inductive RuntimeError where 114 314 | unboundVariable : Name → RuntimeError 115 315 | typeError : String → RuntimeError ··· 119 319 120 320 abbrev EvalM := EIO RuntimeError 121 321 322 322 + def numericOfInt (n : Int) : Numeric := 323 323 + .exact (decimalOfInt n) 324 324 + 325 325 + def numericOfDecimal (d : Decimal) : Numeric := 326 326 + .exact d 327 327 + 328 328 + def valueToDecimal : Value → EvalM Decimal 329 329 + | .number (.exact q) => pure q 330 330 + | _ => throw (.typeError "expected a numeric value") 331 331 + 332 332 + def divDecimals (lhs rhs : Decimal) : EvalM Decimal := do 333 333 + if rhs.num = 0 then 334 334 + throw .divisionByZero 335 335 + else 336 336 + pure (mkRational (lhs.num * Int.ofNat rhs.den) (lhs.den * rhs.num.natAbs) |> 337 337 + fun q => if rhs.num < 0 then { q with num := -q.num } else q) 338 338 + 339 339 + def valueToLazyReal : Value → EvalM LazyReal 340 340 + | .number (.composite r) => pure r 341 341 + | .number (.exact q) => pure (.exact q) 342 342 + | _ => throw (.typeError "expected a numeric or LazyReal value") 343 343 + 344 344 + def generatorComplexity : Generator → Nat 345 345 + | .exactRatio _ => 1 346 346 + | .exactDecimal _ => 1 347 347 + | .rationalRefiner _ => 2 348 348 + | .decimalRefiner _ => 2 349 349 + | .piChudnovsky => 3 350 350 + | .sqrt _ => 2 351 351 + | .add lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs 352 352 + | .sub lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs 353 353 + | .mul lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs 354 354 + | .div lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs 355 355 + 356 356 + def selectFirstGoodEnough [Inhabited α] (candidates : List α) (goodEnough : α → Bool) : α := 357 357 + match candidates.find? goodEnough with 358 358 + | some candidate => candidate 359 359 + | none => 360 360 + match candidates with 361 361 + | candidate :: _ => candidate 362 362 + | [] => default 363 363 + 364 364 + def generatorGoodEnough : Generator → Bool 365 365 + | .exactRatio _ => true 366 366 + | .exactDecimal _ => true 367 367 + | .rationalRefiner _ => true 368 368 + | .decimalRefiner _ => true 369 369 + | .piChudnovsky => true 370 370 + | .sqrt _ => true 371 371 + | .add lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs 372 372 + | .sub lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs 373 373 + | .mul lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs 374 374 + | .div lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs 375 375 + 376 376 + partial def synthesizedCandidates (r : LazyReal) : List Generator := 377 377 + match r with 378 378 + | .exact q => 379 379 + if isTerminatingDecimal q then 380 380 + [.exactDecimal q, .exactRatio q] 381 381 + else 382 382 + [.exactRatio q, .decimalRefiner (.exact q)] 383 383 + | .ratioProcess q => 384 384 + if isTerminatingDecimal q then 385 385 + [.exactDecimal q, .exactRatio q] 386 386 + else 387 387 + [.exactRatio q, .decimalRefiner (.ratioProcess q)] 388 388 + | .decimalProcess d => 389 389 + [.exactDecimal d, .exactRatio d] 390 390 + | .generated g => 391 391 + [g, .decimalRefiner (.generated g), .rationalRefiner (.generated g)] 392 392 + | .pi => 393 393 + [.decimalRefiner .pi, .rationalRefiner .pi, .piChudnovsky] 394 394 + | .sqrt d => 395 395 + [.decimalRefiner (.sqrt d), .rationalRefiner (.sqrt d), .sqrt d] 396 396 + | .add lhs rhs => 397 397 + let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough 398 398 + let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough 399 399 + [.add lhsGen rhsGen, .decimalRefiner (.add lhs rhs), .rationalRefiner (.add lhs rhs)] 400 400 + | .sub lhs rhs => 401 401 + let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough 402 402 + let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough 403 403 + [.sub lhsGen rhsGen, .decimalRefiner (.sub lhs rhs), .rationalRefiner (.sub lhs rhs)] 404 404 + | .mul lhs rhs => 405 405 + let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough 406 406 + let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough 407 407 + [.mul lhsGen rhsGen, .decimalRefiner (.mul lhs rhs), .rationalRefiner (.mul lhs rhs)] 408 408 + | .div lhs rhs => 409 409 + let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough 410 410 + let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough 411 411 + [.div lhsGen rhsGen, .decimalRefiner (.div lhs rhs), .rationalRefiner (.div lhs rhs)] 412 412 + 413 413 + def chooseSynthesizedGenerator (r : LazyReal) : Generator := 414 414 + selectFirstGoodEnough (synthesizedCandidates r) generatorGoodEnough 415 415 + 416 416 + mutual 417 417 + partial def renderGeneratorFormula : Generator → String 418 418 + | .exactRatio q => s!"{q.num}/{q.den}" 419 419 + | .exactDecimal d => renderDecimal d 420 420 + | .rationalRefiner r => s!"rationalRefine({renderLazyFormula r})" 421 421 + | .decimalRefiner r => s!"decimalRefine({renderLazyFormula r})" 422 422 + | .piChudnovsky => 423 423 + "426880 * sqrt(10005) / sum(k => ((-1)^k * (6k)! * (13591409 + 545140134k)) / ((3k)! * (k!)^3 * 640320^(3k)), k = 0..inf)" 424 424 + | .sqrt d => s!"sqrt({renderDecimal d})" 425 425 + | .add lhs rhs => s!"({renderGeneratorFormula lhs}) + ({renderGeneratorFormula rhs})" 426 426 + | .sub lhs rhs => s!"({renderGeneratorFormula lhs}) - ({renderGeneratorFormula rhs})" 427 427 + | .mul lhs rhs => s!"({renderGeneratorFormula lhs}) * ({renderGeneratorFormula rhs})" 428 428 + | .div lhs rhs => s!"({renderGeneratorFormula lhs}) / ({renderGeneratorFormula rhs})" 429 429 + 430 430 + partial def renderLazyFormula : LazyReal → String 431 431 + | .exact q => renderDecimal q 432 432 + | .ratioProcess q => s!"ratio({q.num}/{q.den})" 433 433 + | .decimalProcess d => s!"decimal({renderDecimal d})" 434 434 + | .pi => "pi" 435 435 + | .sqrt d => s!"sqrt({renderDecimal d})" 436 436 + | .add lhs rhs => s!"({renderLazyFormula lhs}) + ({renderLazyFormula rhs})" 437 437 + | .sub lhs rhs => s!"({renderLazyFormula lhs}) - ({renderLazyFormula rhs})" 438 438 + | .mul lhs rhs => s!"({renderLazyFormula lhs}) * ({renderLazyFormula rhs})" 439 439 + | .div lhs rhs => s!"({renderLazyFormula lhs}) / ({renderLazyFormula rhs})" 440 440 + | .generated g => renderGeneratorFormula g 441 441 + end 442 442 + 443 443 + def formulaOfValue (value : Value) : EvalM String := do 444 444 + match value with 445 445 + | .number (.exact q) => 446 446 + pure (renderGeneratorFormula (chooseSynthesizedGenerator (.exact q))) 447 447 + | .number (.composite r) => 448 448 + pure (renderGeneratorFormula (chooseSynthesizedGenerator r)) 449 449 + | _ => 450 450 + let q ← valueToDecimal value 451 451 + pure (renderGeneratorFormula (chooseSynthesizedGenerator (.exact q))) 452 452 + 453 453 + def synthesizeNumeric (value : Value) : EvalM Numeric := do 454 454 + match value with 455 455 + | .number (.exact q) => 456 456 + pure (.composite (.generated (chooseSynthesizedGenerator (.exact q)))) 457 457 + | .number (.composite r) => 458 458 + pure (.composite (.generated (chooseSynthesizedGenerator r))) 459 459 + | _ => 460 460 + let q ← valueToDecimal value 461 461 + pure (.composite (.generated (chooseSynthesizedGenerator (.exact q)))) 462 462 + 463 463 + partial def natSqrtSearch (target lo hi : Nat) : Nat := 464 464 + if lo + 1 >= hi then 465 465 + lo 466 466 + else 467 467 + let mid := lo + (hi - lo) / 2 468 468 + if mid * mid ≤ target then 469 469 + natSqrtSearch target mid hi 470 470 + else 471 471 + natSqrtSearch target lo mid 472 472 + 473 473 + def natSqrtFloor (target : Nat) : Nat := 474 474 + natSqrtSearch target 0 (target + 1) 475 475 + 476 476 + def sqrtBoundsOfDecimal (d : Decimal) (steps : Nat) : EvalM (Decimal × Decimal) := do 477 477 + if d.num < 0 then 478 478 + throw (.typeError "sqrt expects a non-negative decimal") 479 479 + else 480 480 + let scale := steps 481 481 + let scaledTarget := d.num.natAbs * powNat 10 (2 * scale) / d.den 482 482 + let loNat := natSqrtFloor scaledTarget 483 483 + let lo := mkRational (Int.ofNat loNat) (powNat 10 scale) 484 484 + let step := mkRational 1 (powNat 10 scale) 485 485 + pure (lo, addDecimals lo step) 486 486 + 487 487 + def natFactorial : Nat → Nat 488 488 + | 0 => 1 489 489 + | n + 1 => (n + 1) * natFactorial n 490 490 + 491 491 + def chudnovskyTermMag (k : Nat) : Decimal := 492 492 + let sixFact := natFactorial (6 * k) 493 493 + let threeFact := natFactorial (3 * k) 494 494 + let kFact := natFactorial k 495 495 + let coeff : Int := 13591409 + 545140134 * Int.ofNat k 496 496 + let num := Int.ofNat sixFact * coeff 497 497 + let den := threeFact * kFact * kFact * kFact * powNat 640320 (3 * k) 498 498 + mkRational num den 499 499 + 500 500 + def chudnovskySignedTerm (k : Nat) : Decimal := 501 501 + let mag := chudnovskyTermMag k 502 502 + if k % 2 = 0 then mag else { mag with num := -mag.num } 503 503 + 504 504 + def chudnovskySum (terms : Nat) : Decimal := 505 505 + let rec loop (k : Nat) (acc : Decimal) := 506 506 + if k < terms then 507 507 + loop (k + 1) (addDecimals acc (chudnovskySignedTerm k)) 508 508 + else 509 509 + acc 510 510 + loop 0 (decimalOfInt 0) 511 511 + 512 512 + def piBounds (steps : Nat) : EvalM (Decimal × Decimal) := do 513 513 + let terms := steps / 14 + 1 514 514 + let sum := chudnovskySum terms 515 515 + let tail := chudnovskyTermMag terms 516 516 + let sumLo := subDecimals sum tail 517 517 + let sumHi := addDecimals sum tail 518 518 + let (sqrtLo, sqrtHi) ← sqrtBoundsOfDecimal (decimalOfInt 10005) (steps + 2) 519 519 + let coeff := decimalOfInt 426880 520 520 + let cLo := mulDecimals coeff sqrtLo 521 521 + let cHi := mulDecimals coeff sqrtHi 522 522 + let lo ← divDecimals cLo sumHi 523 523 + let hi ← divDecimals cHi sumLo 524 524 + pure (lo, hi) 525 525 + 526 526 + def minDecimal (a b : Decimal) : Decimal := 527 527 + if a.num * Int.ofNat b.den <= b.num * Int.ofNat a.den then a else b 528 528 + 529 529 + def maxDecimal (a b : Decimal) : Decimal := 530 530 + if a.num * Int.ofNat b.den >= b.num * Int.ofNat a.den then a else b 531 531 + 532 532 + def roundRationalToScale (q : Rational) (scale : Nat) : Rational := 533 533 + let factor := powNat 10 scale 534 534 + let scaledNum := q.num * Int.ofNat factor 535 535 + let denInt := Int.ofNat q.den 536 536 + let adjust := Int.ofNat (q.den / 2) 537 537 + let rounded := 538 538 + if scaledNum < 0 then 539 539 + (scaledNum - adjust) / denInt 540 540 + else 541 541 + (scaledNum + adjust) / denInt 542 542 + mkRational rounded factor 543 543 + 544 544 + def mulBounds (lo1 hi1 lo2 hi2 : Decimal) : Decimal × Decimal := 545 545 + let p1 := mulDecimals lo1 lo2 546 546 + let p2 := mulDecimals lo1 hi2 547 547 + let p3 := mulDecimals hi1 lo2 548 548 + let p4 := mulDecimals hi1 hi2 549 549 + let lo := minDecimal (minDecimal p1 p2) (minDecimal p3 p4) 550 550 + let hi := maxDecimal (maxDecimal p1 p2) (maxDecimal p3 p4) 551 551 + (lo, hi) 552 552 + 553 553 + mutual 554 554 + partial def boundsGenerator (g : Generator) (steps : Nat) : EvalM (Decimal × Decimal) := do 555 555 + match g with 556 556 + | .exactRatio q => pure (q, q) 557 557 + | .exactDecimal d => pure (d, d) 558 558 + | .rationalRefiner r => 559 559 + let q ← approxLazyReal r steps 560 560 + pure (q, q) 561 561 + | .decimalRefiner r => 562 562 + let q ← approxLazyReal r steps 563 563 + pure (roundRationalToScale q steps, roundRationalToScale q steps) 564 564 + | .piChudnovsky => piBounds steps 565 565 + | .sqrt d => sqrtBoundsOfDecimal d steps 566 566 + | .add lhs rhs => 567 567 + let (llo, lhi) ← boundsGenerator lhs steps 568 568 + let (rlo, rhi) ← boundsGenerator rhs steps 569 569 + pure (addDecimals llo rlo, addDecimals lhi rhi) 570 570 + | .sub lhs rhs => 571 571 + let (llo, lhi) ← boundsGenerator lhs steps 572 572 + let (rlo, rhi) ← boundsGenerator rhs steps 573 573 + pure (subDecimals llo rhi, subDecimals lhi rlo) 574 574 + | .mul lhs rhs => 575 575 + let (llo, lhi) ← boundsGenerator lhs steps 576 576 + let (rlo, rhi) ← boundsGenerator rhs steps 577 577 + pure (mulBounds llo lhi rlo rhi) 578 578 + | .div lhs rhs => 579 579 + let (llo, lhi) ← boundsGenerator lhs steps 580 580 + let (rlo, rhi) ← boundsGenerator rhs steps 581 581 + if rlo.num <= 0 && 0 <= rhi.num then 582 582 + throw (.typeError "generated division interval crosses zero") 583 583 + else 584 584 + let invLo ← divDecimals (decimalOfInt 1) rhi 585 585 + let invHi ← divDecimals (decimalOfInt 1) rlo 586 586 + pure (mulBounds llo lhi invLo invHi) 587 587 + 588 588 + partial def approxGenerator (g : Generator) (steps : Nat) : EvalM Decimal := do 589 589 + match g with 590 590 + | .exactRatio q => pure q 591 591 + | .exactDecimal d => pure d 592 592 + | .rationalRefiner r => approxLazyReal r steps 593 593 + | .decimalRefiner r => 594 594 + let q ← approxLazyReal r steps 595 595 + pure (roundRationalToScale q steps) 596 596 + | .piChudnovsky => 597 597 + let (lo, hi) ← piBounds steps 598 598 + divDecimals (addDecimals lo hi) (decimalOfInt 2) 599 599 + | .sqrt d => 600 600 + let (lo, hi) ← sqrtBoundsOfDecimal d steps 601 601 + divDecimals (addDecimals lo hi) (decimalOfInt 2) 602 602 + | .add _ _ | .sub _ _ | .mul _ _ | .div _ _ => 603 603 + let (lo, hi) ← boundsGenerator g steps 604 604 + divDecimals (addDecimals lo hi) (decimalOfInt 2) 605 605 + 606 606 + partial def boundsLazyReal (r : LazyReal) (steps : Nat) : EvalM (Decimal × Decimal) := do 607 607 + match r with 608 608 + | .exact d => pure (d, d) 609 609 + | .ratioProcess q => pure (q, q) 610 610 + | .decimalProcess d => pure (d, d) 611 611 + | .generated g => boundsGenerator g steps 612 612 + | .pi => piBounds steps 613 613 + | .sqrt d => sqrtBoundsOfDecimal d steps 614 614 + | .add lhs rhs => 615 615 + let (llo, lhi) ← boundsLazyReal lhs steps 616 616 + let (rlo, rhi) ← boundsLazyReal rhs steps 617 617 + pure (addDecimals llo rlo, addDecimals lhi rhi) 618 618 + | .sub lhs rhs => 619 619 + let (llo, lhi) ← boundsLazyReal lhs steps 620 620 + let (rlo, rhi) ← boundsLazyReal rhs steps 621 621 + pure (subDecimals llo rhi, subDecimals lhi rlo) 622 622 + | .mul lhs rhs => 623 623 + let (llo, lhi) ← boundsLazyReal lhs steps 624 624 + let (rlo, rhi) ← boundsLazyReal rhs steps 625 625 + pure (mulBounds llo lhi rlo rhi) 626 626 + | .div lhs rhs => 627 627 + let (llo, lhi) ← boundsLazyReal lhs steps 628 628 + let (rlo, rhi) ← boundsLazyReal rhs steps 629 629 + if rlo.num <= 0 && 0 <= rhi.num then 630 630 + throw (.typeError "lazy division interval crosses zero") 631 631 + else 632 632 + let invLo ← divDecimals (decimalOfInt 1) rhi 633 633 + let invHi ← divDecimals (decimalOfInt 1) rlo 634 634 + pure (mulBounds llo lhi invLo invHi) 635 635 + 636 636 + partial def approxLazyReal (r : LazyReal) (steps : Nat) : EvalM Decimal := do 637 637 + match r with 638 638 + | .exact d => pure d 639 639 + | .ratioProcess q => pure q 640 640 + | .decimalProcess d => pure d 641 641 + | .generated g => approxGenerator g steps 642 642 + | .pi => 643 643 + let (lo, hi) ← piBounds steps 644 644 + divDecimals (addDecimals lo hi) (decimalOfInt 2) 645 645 + | .sqrt d => 646 646 + let (lo, hi) ← sqrtBoundsOfDecimal d steps 647 647 + divDecimals (addDecimals lo hi) (decimalOfInt 2) 648 648 + | .add _ _ | .sub _ _ | .mul _ _ | .div _ _ => 649 649 + let (lo, hi) ← boundsLazyReal r steps 650 650 + divDecimals (addDecimals lo hi) (decimalOfInt 2) 651 651 + end 652 652 + 653 653 + def stabilizeNumeric (value : Value) (steps : Nat) : EvalM Rational := do 654 654 + match value with 655 655 + | .number (.exact q) => pure (roundRationalToScale q steps) 656 656 + | .number (.composite r) => 657 657 + let q ← approxLazyReal r steps 658 658 + pure (roundRationalToScale q steps) 659 659 + | _ => 660 660 + let q ← valueToDecimal value 661 661 + pure (roundRationalToScale q steps) 662 662 + 122 663 def Env.lookup (env : Env) (name : Name) : Option Value := 123 664 match env with 124 665 | [] => none 125 666 | (n, v) :: rest => if n = name then some v else rest.lookup name 126 667 127 668 def expectInt : Value → EvalM Int 128 128 - | .int n => pure n 669 669 + | .number (.exact q) => 670 670 + if q.den = 1 then pure q.num else throw (.typeError "expected an integer") 129 671 | _ => throw (.typeError "expected an integer") 130 672 673 673 + def expectDecimal : Value → EvalM Decimal 674 674 + | .number (.exact q) => pure q 675 675 + | _ => throw (.typeError "expected a decimal") 676 676 + 677 677 + def expectLazyReal : Value → EvalM LazyReal 678 678 + | .number (.composite r) => pure r 679 679 + | _ => throw (.typeError "expected a LazyReal") 680 680 + 131 681 def expectBool : Value → EvalM Bool 132 682 | .bool b => pure b 133 683 | _ => throw (.typeError "expected a boolean") ··· 140 690 | .data term => pure term 141 691 | _ => throw (.typeError "expected a data value") 142 692 693 693 + def expectWholeNat (value : Value) : EvalM Nat := do 694 694 + let q ← valueToDecimal value 695 695 + if q.den ≠ 1 then 696 696 + throw (.typeError "expected a whole rational") 697 697 + else if q.num < 0 then 698 698 + throw (.typeError "expected a non-negative whole rational") 699 699 + else 700 700 + pure q.num.toNat 701 701 + 702 702 + def rationalStabilityOfValue (value : Value) : String := 703 703 + match value with 704 704 + | .number (.composite (.ratioProcess _)) => "Immediate" 705 705 + | .number (.composite (.decimalProcess _)) => "Immediate" 706 706 + | .number (.composite (.generated (.exactRatio _))) => "Immediate" 707 707 + | .number (.composite (.generated (.exactDecimal _))) => "Immediate" 708 708 + | .number (.exact _) => "Immediate" 709 709 + | .number (.composite _) => "Refining" 710 710 + | _ => "Unavailable" 711 711 + 712 712 + def decimalStabilityOfRational (q : Rational) : String := 713 713 + if isTerminatingDecimal q then "Terminating" else "Periodic" 714 714 + 715 715 + def decimalStabilityOfValue (value : Value) : String := 716 716 + match value with 717 717 + | .number (.composite (.ratioProcess q)) => decimalStabilityOfRational q 718 718 + | .number (.composite (.decimalProcess d)) => decimalStabilityOfRational d 719 719 + | .number (.composite (.generated (.exactRatio q))) => decimalStabilityOfRational q 720 720 + | .number (.composite (.generated (.exactDecimal d))) => decimalStabilityOfRational d 721 721 + | .number (.exact q) => decimalStabilityOfRational q 722 722 + | .number (.composite _) => "Refining" 723 723 + | _ => "Unavailable" 724 724 + 725 725 + def observeValue (value : Value) (obs : Observation) : EvalM ObservationResult := do 726 726 + match obs with 727 727 + | .asRational => 728 728 + match value with 729 729 + | .number (.exact q) => pure (.rational q) 730 730 + | .number (.composite _) => 731 731 + throw (.typeError s!"rational observation failed: number is {rationalStabilityOfValue value}, not Immediate") 732 732 + | _ => 733 733 + pure (.rational (← valueToDecimal value)) 734 734 + | .asDecimal => 735 735 + match value with 736 736 + | .number (.exact q) => 737 737 + if isTerminatingDecimal q then 738 738 + pure (.decimal q) 739 739 + else 740 740 + throw (.typeError s!"decimal observation failed: number is {decimalStabilityOfValue value}, not Terminating") 741 741 + | .number (.composite _) => 742 742 + throw (.typeError s!"decimal observation failed: number is {decimalStabilityOfValue value}, not Terminating") 743 743 + | _ => 744 744 + let q ← valueToDecimal value 745 745 + if isTerminatingDecimal q then 746 746 + pure (.decimal q) 747 747 + else 748 748 + throw (.typeError s!"decimal observation failed: number is {decimalStabilityOfValue value}, not Terminating") 749 749 + | .asInt => 750 750 + match value with 751 751 + | .number (.exact q) => 752 752 + if q.den = 1 then 753 753 + pure (.int q.num) 754 754 + else 755 755 + throw (.typeError "integer observation failed: number is not whole") 756 756 + | .number (.composite _) => 757 757 + throw (.typeError s!"integer observation failed: number is {rationalStabilityOfValue value}, not Immediate") 758 758 + | _ => 759 759 + let q ← valueToDecimal value 760 760 + if q.den = 1 then 761 761 + pure (.int q.num) 762 762 + else 763 763 + throw (.typeError "integer observation failed: number is not whole") 764 764 + | .rationalStability => 765 765 + pure (.stability (rationalStabilityOfValue value)) 766 766 + | .decimalStability => 767 767 + pure (.stability (decimalStabilityOfValue value)) 768 768 + | .getField key => 769 769 + match value with 770 770 + | .data (.record fields) => 771 771 + match fields.find? (fun (name, _) => name = key) with 772 772 + | some (_, field) => pure (.data field) 773 773 + | none => throw (.typeError s!"missing field: {key}") 774 774 + | _ => throw (.typeError "get expects a record") 775 775 + | .atIndex idx => 776 776 + let rec arrayGet? : List Data → Nat → Option Data 777 777 + | [], _ => none 778 778 + | x :: _, 0 => some x 779 779 + | _ :: xs, n + 1 => arrayGet? xs n 780 780 + match value with 781 781 + | .data (.array items) => 782 782 + match arrayGet? items idx with 783 783 + | some item => pure (.data item) 784 784 + | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}") 785 785 + | _ => throw (RuntimeError.typeError "at expects an array") 786 786 + | .approx steps => 787 787 + let r ← valueToLazyReal value 788 788 + pure (.rational (← approxLazyReal r steps)) 789 789 + | .bounds steps => 790 790 + let r ← valueToLazyReal value 791 791 + let (lo, hi) ← boundsLazyReal r steps 792 792 + pure (.bounds lo hi) 793 793 + 143 794 def valueToData : Value → EvalM Data 144 795 | .data term => pure term 145 145 - | .int n => pure (.int n) 796 796 + | .number (.exact q) => pure (.decimal q) 146 797 | .bool b => pure (.bool b) 147 798 | .string s => pure (.string s) 148 148 - | _ => throw (.typeError "data literals only support Int, Bool, String, and Data values") 799 799 + | _ => throw (.typeError "data literals only support Int, Decimal, Bool, String, and Data values") 149 800 150 801 partial def dataType : Data → Ty 151 802 | .null => .dataNull 152 803 | .bool _ => .dataBool 153 804 | .int _ => .dataInt 805 805 + | .decimal _ => .dataRational 154 806 | .string _ => .dataString 155 807 | .array [] => .dataArray .data 156 808 | .array (x :: xs) => ··· 169 821 170 822 def liftScalarDataTy : Ty → Ty 171 823 | .dataInt => .int 824 824 + | .dataDecimal => .decimal 825 825 + | .dataRational => .rational 172 826 | .dataBool => .bool 173 827 | .dataString => .string 174 828 | ty => ty ··· 176 830 partial def refineKnownDataTy (ty : Ty) : Ty := 177 831 match ty with 178 832 | .dataInt => .int 833 833 + | .dataDecimal => .decimal 834 834 + | .dataRational => .rational 179 835 | .dataBool => .bool 180 836 | .dataString => .string 181 837 | .dataNull => .data ··· 205 861 | .null => .null 206 862 | .bool b => .bool b 207 863 | .int n => .int n 864 864 + | .decimal d => .decimal (parseDecimal d) 208 865 | .string s => .string s 209 866 | .array xs => .array (xs.map Data.ofNickel) 210 867 | .record fields => .record (fields.map (fun (k, v) => (k, Data.ofNickel v))) ··· 248 905 | .null => "null" 249 906 | .bool b => toString b 250 907 | .int n => toString n 908 908 + | .decimal d => renderDecimal d 251 909 | .string s => renderJsonString s 252 910 | .array xs => "[" ++ String.intercalate ", " (xs.map renderNickelData) ++ "]" 253 911 | .record fields => ··· 258 916 | .null => "null" 259 917 | .bool b => if b then "true" else "false" 260 918 | .int n => toString n 919 919 + | .decimal d => renderDecimal d 261 920 | .string s => renderJsonString s 262 921 | .array xs => "[" ++ String.intercalate ", " (xs.map renderJsonData) ++ "]" 263 922 | .record fields => ··· 271 930 | "readFileNickel" => some (.funTy .string [.error, .io] .data) 272 931 | "parseNickel" => some (.funTy .string [.error] .data) 273 932 | "parseJson" => some (.funTy .string [.error] .data) 933 933 + | "getAturi" => some (.funTy .string [.error, .io] .data) 274 934 | "get" => some (.funTy .data [] (.funTy .string [.error] .data)) 275 275 - | "at" => some (.funTy .data [] (.funTy .int [.error] .data)) 935 935 + | "at" => some (.funTy .data [] (.funTy .number [.error] .data)) 276 936 | "asInt" => some (.funTy .data [.error] .int) 937 937 + | "asDecimal" => some (.funTy .data [.error] .decimal) 938 938 + | "toInt" => some (.funTy .number [.error] .int) 939 939 + | "toDecimal" => some (.funTy .number [.error] .decimal) 277 940 | "asString" => some (.funTy .data [.error] .string) 278 941 | "asBool" => some (.funTy .data [.error] .bool) 279 942 | "toJson" => some (.funTy .data [] .string) 280 943 | "toNickel" => some (.funTy .data [] .string) 944 944 + | "rationalStability" => some (.funTy .number [] .stability) 945 945 + | "decimalStability" => some (.funTy .number [] .stability) 946 946 + | "pi" => some .number 947 947 + | "sqrt" => some (.funTy .number [.error] .number) 948 948 + | "process" => some (.funTy .number [] .number) 949 949 + | "synthesize" => some (.funTy .number [.error] .number) 950 950 + | "formula" => some (.funTy .number [.error] .string) 951 951 + | "lazyRationalStability" => some (.funTy .number [] .stability) 952 952 + | "lazyDecimalStability" => some (.funTy .number [] .stability) 953 953 + | "stabilize" => some (.funTy .number [] (.funTy .number [.error] .number)) 954 954 + | "approx" => some (.funTy .number [] (.funTy .number [.error] .number)) 955 955 + | "bounds" => some (.funTy .number [] (.funTy .number [.error] .data)) 281 956 | _ => none 282 957 283 958 def builtinValue? (name : Name) : Option Value := ··· 287 962 | "readFileNickel" => some .builtinReadFileNickel 288 963 | "parseNickel" => some .builtinParseNickel 289 964 | "parseJson" => some .builtinParseJson 965 965 + | "getAturi" => some .builtinGetAturi 290 966 | "get" => some .builtinDataGet 291 967 | "at" => some .builtinDataAt 292 968 | "asInt" => some .builtinDataAsInt 969 969 + | "asDecimal" => some .builtinDataAsDecimal 970 970 + | "toInt" => some .builtinRationalToInt 971 971 + | "toDecimal" => some .builtinRationalToDecimal 293 972 | "asString" => some .builtinDataAsString 294 973 | "asBool" => some .builtinDataAsBool 295 974 | "toJson" => some .builtinDataToJson 296 975 | "toNickel" => some .builtinDataToNickel 976 976 + | "rationalStability" => some .builtinRationalStability 977 977 + | "decimalStability" => some .builtinDecimalStability 978 978 + | "pi" => some (.number (.composite .pi)) 979 979 + | "sqrt" => some .builtinSqrt 980 980 + | "process" => some .builtinProcess 981 981 + | "synthesize" => some .builtinSynthesize 982 982 + | "formula" => some .builtinFormula 983 983 + | "lazyRationalStability" => some .builtinRationalStability 984 984 + | "lazyDecimalStability" => some .builtinDecimalStability 985 985 + | "stabilize" => some .builtinStabilize 986 986 + | "approx" => some .builtinApprox 987 987 + | "bounds" => some .builtinBounds 297 988 | _ => none 298 989 299 990 mutual ··· 321 1012 let source ← expectString argVal 322 1013 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalJsonString source) 323 1014 pure (.data (← parseRenderedData rendered)) 324 324 - | .builtinDataGet => do 325 325 - let term ← expectData argVal 326 326 - pure (.builtinDataGetField term) 327 327 - | .builtinDataGetField term => do 1015 1015 + | .builtinGetAturi => do 1016 1016 + let source ← expectString argVal 1017 1017 + let rendered ← IO.toEIO (fun err => .ioError (toString err)) (Http.parseAturi source) 1018 1018 + pure (.data (← parseRenderedData rendered)) 1019 1019 + | .builtinDataGet => pure (.builtinDataGetField argVal) 1020 1020 + | .builtinDataGetField target => do 328 1021 let key ← expectString argVal 329 329 - match term with 330 330 - | .record fields => 331 331 - match fields.find? (fun (name, _) => name = key) with 332 332 - | some (_, value) => pure (.data value) 333 333 - | none => throw (.typeError s!"missing field: {key}") 334 334 - | _ => throw (.typeError "get expects a record") 335 335 - | .builtinDataAt => do 336 336 - let term ← expectData argVal 337 337 - pure (.builtinDataAtIndex term) 338 338 - | .builtinDataAtIndex term => do 339 339 - let idx ← expectInt argVal 340 340 - if idx < 0 then 341 341 - throw (.typeError s!"negative index: {idx}") 342 342 - else 343 343 - match term with 344 344 - | .array items => 345 345 - match dataArrayGet? items idx.toNat with 346 346 - | some value => pure (.data value) 347 347 - | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}") 348 348 - | _ => throw (.typeError "at expects an array") 1022 1022 + match (← observeValue target (.getField key)) with 1023 1023 + | .data value => pure (.data value) 1024 1024 + | _ => throw (.typeError "get observation returned non-data") 1025 1025 + | .builtinDataAt => pure (.builtinDataAtIndex argVal) 1026 1026 + | .builtinDataAtIndex target => do 1027 1027 + let idx ← expectWholeNat argVal 1028 1028 + match (← observeValue target (.atIndex idx)) with 1029 1029 + | .data value => pure (.data value) 1030 1030 + | _ => throw (.typeError "at observation returned non-data") 349 1031 | .builtinDataAsInt => do 350 1032 let term ← expectData argVal 351 1033 match term with 352 352 - | .int n => pure (.int n) 1034 1034 + | .int n => pure (.number (numericOfInt n)) 353 1035 | _ => throw (.typeError "asInt expects an integer") 1036 1036 + | .builtinDataAsDecimal => do 1037 1037 + let term ← expectData argVal 1038 1038 + match term with 1039 1039 + | .decimal d => pure (.number (numericOfDecimal d)) 1040 1040 + | _ => throw (.typeError "asDecimal expects a decimal") 1041 1041 + | .builtinRationalToInt => do 1042 1042 + match (← observeValue argVal .asInt) with 1043 1043 + | .int n => pure (.number (numericOfInt n)) 1044 1044 + | _ => throw (.typeError "toInt observation returned non-int") 1045 1045 + | .builtinRationalToDecimal => do 1046 1046 + match (← observeValue argVal .asDecimal) with 1047 1047 + | .decimal d => pure (.number (numericOfDecimal d)) 1048 1048 + | _ => throw (.typeError "toDecimal observation returned non-decimal") 354 1049 | .builtinDataAsString => do 355 1050 let term ← expectData argVal 356 1051 match term with ··· 367 1062 | .builtinDataToNickel => do 368 1063 let term ← expectData argVal 369 1064 pure (.string (renderNickelData term)) 1065 1065 + | .builtinRationalStability => do 1066 1066 + match (← observeValue argVal .rationalStability) with 1067 1067 + | .stability label => pure (.stability label) 1068 1068 + | _ => throw (.typeError "rationalStability observation returned non-stability") 1069 1069 + | .builtinDecimalStability => do 1070 1070 + match (← observeValue argVal .decimalStability) with 1071 1071 + | .stability label => pure (.stability label) 1072 1072 + | _ => throw (.typeError "decimalStability observation returned non-stability") 1073 1073 + | .builtinSqrt => do 1074 1074 + let d ← valueToDecimal argVal 1075 1075 + if d.num < 0 then 1076 1076 + throw (.typeError "sqrt expects a non-negative decimal") 1077 1077 + else 1078 1078 + pure (.number (.composite (.sqrt d))) 1079 1079 + | .builtinProcess => do 1080 1080 + match argVal with 1081 1081 + | .number (.exact q) => pure (.number (.composite (.exact q))) 1082 1082 + | .number (.composite r) => pure (.number (.composite r)) 1083 1083 + | _ => throw (.typeError "process expects a number") 1084 1084 + | .builtinSynthesize => do 1085 1085 + pure (.number (← synthesizeNumeric argVal)) 1086 1086 + | .builtinFormula => do 1087 1087 + pure (.string (← formulaOfValue argVal)) 1088 1088 + | .builtinStabilize => pure (.builtinStabilizeStep argVal) 1089 1089 + | .builtinStabilizeStep target => do 1090 1090 + let steps ← expectWholeNat argVal 1091 1091 + pure (.number (.exact (← stabilizeNumeric target steps))) 1092 1092 + | .builtinApprox => pure (.builtinApproxStep argVal) 1093 1093 + | .builtinApproxStep target => do 1094 1094 + let steps ← expectWholeNat argVal 1095 1095 + match (← observeValue target (.approx steps)) with 1096 1096 + | .rational q => pure (.number (.exact q)) 1097 1097 + | _ => throw (.typeError "approx observation returned non-rational") 1098 1098 + | .builtinBounds => pure (.builtinBoundsStep argVal) 1099 1099 + | .builtinBoundsStep target => do 1100 1100 + let steps ← expectWholeNat argVal 1101 1101 + match (← observeValue target (.bounds steps)) with 1102 1102 + | .bounds lo hi => pure (.data (.record [("lo", .decimal lo), ("hi", .decimal hi)])) 1103 1103 + | _ => throw (.typeError "bounds observation returned non-bounds") 1104 1104 + | .data (.record fields) => 1105 1105 + let key ← expectString argVal 1106 1106 + match fields.find? (fun (name, _) => name = key) with 1107 1107 + | some (_, value) => pure (.data value) 1108 1108 + | none => throw (.typeError s!"missing field: {key}") 1109 1109 + | .data (.array items) => 1110 1110 + let idx ← expectWholeNat argVal 1111 1111 + match dataArrayGet? items idx with 1112 1112 + | some value => pure (.data value) 1113 1113 + | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}") 1114 1114 + | .data _ => 1115 1115 + throw (.typeError "data value is not callable with this argument") 370 1116 | _ => 371 371 - match fnVal, argVal with 372 372 - | .data (.record fields), .string key => 373 373 - match fields.find? (fun (name, _) => name = key) with 374 374 - | some (_, value) => pure (.data value) 375 375 - | none => throw (.typeError s!"missing field: {key}") 376 376 - | .data (.array items), .int idx => 377 377 - if idx < 0 then 378 378 - throw (.typeError s!"negative index: {idx}") 379 379 - else 380 380 - match dataArrayGet? items idx.toNat with 381 381 - | some value => pure (.data value) 382 382 - | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}") 383 383 - | .data _, .string _ => 384 384 - throw (.typeError "string dispatch expects a record") 385 385 - | .data _, .int _ => 386 386 - throw (.typeError "int dispatch expects an array") 387 387 - | _, _ => 388 388 - throw (.typeError "expected a function") 1117 1117 + throw (.typeError "expected a function") 389 1118 390 1119 partial def eval (env : Env) : Expr → EvalM Value 391 391 - | .int n => pure (.int n) 1120 1120 + | .int n => pure (.number (numericOfInt n)) 1121 1121 + | .decimal d => pure (.number (numericOfDecimal d)) 392 1122 | .bool b => pure (.bool b) 393 1123 | .string s => pure (.string s) 394 1124 | .null => pure (.data .null) ··· 408 1138 pure (name, (← valueToData value'))) 409 1139 pure (.data (.record fields')) 410 1140 | .add lhs rhs => do 411 411 - let l ← expectInt (← eval env lhs) 412 412 - let r ← expectInt (← eval env rhs) 413 413 - pure (.int (l + r)) 1141 1141 + let lVal ← eval env lhs 1142 1142 + let rVal ← eval env rhs 1143 1143 + match lVal, rVal with 1144 1144 + | .number (.composite _), _ | _, .number (.composite _) => 1145 1145 + pure (.number (.composite (.add (← valueToLazyReal lVal) (← valueToLazyReal rVal)))) 1146 1146 + | _, _ => 1147 1147 + pure (.number (.exact (addDecimals (← valueToDecimal lVal) (← valueToDecimal rVal)))) 414 1148 | .sub lhs rhs => do 415 415 - let l ← expectInt (← eval env lhs) 416 416 - let r ← expectInt (← eval env rhs) 417 417 - pure (.int (l - r)) 1149 1149 + let lVal ← eval env lhs 1150 1150 + let rVal ← eval env rhs 1151 1151 + match lVal, rVal with 1152 1152 + | .number (.composite _), _ | _, .number (.composite _) => 1153 1153 + pure (.number (.composite (.sub (← valueToLazyReal lVal) (← valueToLazyReal rVal)))) 1154 1154 + | _, _ => 1155 1155 + pure (.number (.exact (subDecimals (← valueToDecimal lVal) (← valueToDecimal rVal)))) 418 1156 | .mul lhs rhs => do 419 419 - let l ← expectInt (← eval env lhs) 420 420 - let r ← expectInt (← eval env rhs) 421 421 - pure (.int (l * r)) 1157 1157 + let lVal ← eval env lhs 1158 1158 + let rVal ← eval env rhs 1159 1159 + match lVal, rVal with 1160 1160 + | .number (.composite _), _ | _, .number (.composite _) => 1161 1161 + pure (.number (.composite (.mul (← valueToLazyReal lVal) (← valueToLazyReal rVal)))) 1162 1162 + | _, _ => 1163 1163 + pure (.number (.exact (mulDecimals (← valueToDecimal lVal) (← valueToDecimal rVal)))) 422 1164 | .div lhs rhs => do 423 423 - let l ← expectInt (← eval env lhs) 424 424 - let r ← expectInt (← eval env rhs) 425 425 - if r = 0 then 426 426 - throw .divisionByZero 427 427 - else 428 428 - pure (.int (l / r)) 1165 1165 + let lVal ← eval env lhs 1166 1166 + let rVal ← eval env rhs 1167 1167 + match lVal, rVal with 1168 1168 + | .number (.composite _), _ | _, .number (.composite _) => 1169 1169 + pure (.number (.composite (.div (← valueToLazyReal lVal) (← valueToLazyReal rVal)))) 1170 1170 + | _, _ => 1171 1171 + pure (.number (.exact (← divDecimals (← valueToDecimal lVal) (← valueToDecimal rVal)))) 429 1172 | .eq lhs rhs => do 430 430 - let l ← expectInt (← eval env lhs) 431 431 - let r ← expectInt (← eval env rhs) 432 432 - pure (.bool (l = r)) 1173 1173 + let l ← eval env lhs 1174 1174 + let r ← eval env rhs 1175 1175 + match l, r with 1176 1176 + | .number _, .number _ => pure (.bool (rationalEq (← valueToDecimal l) (← valueToDecimal r))) 1177 1177 + | _, _ => throw (.typeError "equality expects matching Int or Decimal operands") 433 1178 | .letE name value body => do 434 1179 let value' ← eval env value 435 1180 eval ((name, value') :: env) body ··· 464 1209 465 1210 def renderData : Data → String := renderNickelData 466 1211 1212 1212 + def renderObservedScalar (value : Value) : Option String := 1213 1213 + match value with 1214 1214 + | .number (.exact q) => some s!"{q.num}/{q.den}" 1215 1215 + | _ => none 1216 1216 + 467 1217 def renderValue : Value → String 468 468 - | .int n => toString n 1218 1218 + | value@(.number (.exact _)) => 1219 1219 + match renderObservedScalar value with 1220 1220 + | some rendered => rendered 1221 1221 + | none => "<number>" 1222 1222 + | .stability label => label 1223 1223 + | .number (.composite (.ratioProcess q)) => s!"<process:ratio({q.num}/{q.den})>" 1224 1224 + | .number (.composite (.decimalProcess d)) => s!"<process:decimal({renderDecimal d})>" 1225 1225 + | .number (.composite (.generated (.exactRatio q))) => s!"<generator:ratio({q.num}/{q.den})>" 1226 1226 + | .number (.composite (.generated (.exactDecimal d))) => s!"<generator:decimal({renderDecimal d})>" 1227 1227 + | .number (.composite (.generated (.rationalRefiner _))) => "<generator:rational-refiner>" 1228 1228 + | .number (.composite (.generated (.decimalRefiner _))) => "<generator:decimal-refiner>" 1229 1229 + | .number (.composite (.generated .piChudnovsky)) => "<generator:pi[chudnovsky]>" 1230 1230 + | .number (.composite (.generated (.sqrt d))) => s!"<generator:sqrt({renderDecimal d})>" 1231 1231 + | .number (.composite (.generated (.add _ _))) => "<generator:add>" 1232 1232 + | .number (.composite (.generated (.sub _ _))) => "<generator:sub>" 1233 1233 + | .number (.composite (.generated (.mul _ _))) => "<generator:mul>" 1234 1234 + | .number (.composite (.generated (.div _ _))) => "<generator:div>" 1235 1235 + | .number (.composite (.exact d)) => s!"<lazy:{renderDecimal d}>" 1236 1236 + | .number (.composite .pi) => "<lazy:pi>" 1237 1237 + | .number (.composite (.sqrt d)) => s!"<lazy:sqrt({renderDecimal d})>" 1238 1238 + | .number (.composite (.add _ _)) => "<lazy:add>" 1239 1239 + | .number (.composite (.sub _ _)) => "<lazy:sub>" 1240 1240 + | .number (.composite (.mul _ _)) => "<lazy:mul>" 1241 1241 + | .number (.composite (.div _ _)) => "<lazy:div>" 469 1242 | .bool b => toString b 470 1243 | .string s => s!"\"{s}\"" 471 1244 | .data data => renderData data ··· 478 1251 | .builtinReadFileNickel => "<builtin:readFileNickel>" 479 1252 | .builtinParseNickel => "<builtin:parseNickel>" 480 1253 | .builtinParseJson => "<builtin:parseJson>" 1254 1254 + | .builtinGetAturi => "<builtin:getAturi>" 481 1255 | .builtinDataGet => "<builtin:get>" 482 1256 | .builtinDataGetField _ => "<builtin:getField>" 483 1257 | .builtinDataAt => "<builtin:at>" 484 1258 | .builtinDataAtIndex _ => "<builtin:atIndex>" 485 1259 | .builtinDataAsInt => "<builtin:asInt>" 1260 1260 + | .builtinDataAsDecimal => "<builtin:asDecimal>" 1261 1261 + | .builtinRationalToInt => "<builtin:toInt>" 1262 1262 + | .builtinRationalToDecimal => "<builtin:toDecimal>" 486 1263 | .builtinDataAsString => "<builtin:asString>" 487 1264 | .builtinDataAsBool => "<builtin:asBool>" 488 1265 | .builtinDataToJson => "<builtin:toJson>" 489 1266 | .builtinDataToNickel => "<builtin:toNickel>" 1267 1267 + | .builtinRationalStability => "<builtin:rationalStability>" 1268 1268 + | .builtinDecimalStability => "<builtin:decimalStability>" 1269 1269 + | .builtinSqrt => "<builtin:sqrt>" 1270 1270 + | .builtinProcess => "<builtin:process>" 1271 1271 + | .builtinSynthesize => "<builtin:synthesize>" 1272 1272 + | .builtinFormula => "<builtin:formula>" 1273 1273 + | .builtinStabilize => "<builtin:stabilize>" 1274 1274 + | .builtinStabilizeStep _ => "<builtin:stabilizeStep>" 1275 1275 + | .builtinApprox => "<builtin:approx>" 1276 1276 + | .builtinApproxStep _ => "<builtin:approxStep>" 1277 1277 + | .builtinBounds => "<builtin:bounds>" 1278 1278 + | .builtinBoundsStep _ => "<builtin:boundsStep>" 490 1279 | .closure _ _ _ => "<closure>" 491 1280 492 1281 abbrev TyEnv := List (Name × Ty) ··· 514 1303 pure () 515 1304 else 516 1305 throw (.mismatch expected actual) 1306 1306 + 1307 1307 + def isNumericTy : Ty → Bool 1308 1308 + | .number | .int | .decimal | .rational | .lazyReal => true 1309 1309 + | _ => false 517 1310 518 1311 def pureJudgment (ty : Ty) : Judgment := 519 1312 { ty := ty, effects := [] } 520 1313 521 1314 def eraseDataRefinement : Ty → Ty 522 522 - | .dataInt | .dataBool | .dataString | .dataNull | .dataArray _ | .dataRecord _ => .data 1315 1315 + | .dataInt | .dataDecimal | .dataRational | .dataBool | .dataString | .dataNull | .dataArray _ | .dataRecord _ => .data 523 1316 | ty => ty 524 1317 525 1318 def canFlowTo (actual expected : Ty) : Bool := ··· 527 1320 true 528 1321 else 529 1322 match actual, expected with 1323 1323 + | .number, .number => true 1324 1324 + | .int, .number => true 1325 1325 + | .decimal, .number => true 1326 1326 + | .rational, .number => true 1327 1327 + | .lazyReal, .number => true 1328 1328 + | .number, .decimal => true 1329 1329 + | .number, .rational => true 1330 1330 + | .int, .decimal => true 1331 1331 + | .int, .rational => true 1332 1332 + | .decimal, .rational => true 1333 1333 + | .rational, .decimal => true 530 1334 | .dataInt, .data => true 1335 1335 + | .dataDecimal, .data => true 1336 1336 + | .dataRational, .data => true 531 1337 | .dataBool, .data => true 532 1338 | .dataString, .data => true 533 1339 | .dataNull, .data => true ··· 544 1350 | .null => some .null 545 1351 | .string s => some (.string s) 546 1352 | .int n => some (.int n) 1353 1353 + | .decimal d => some (.decimal d) 547 1354 | .bool b => some (.bool b) 548 1355 | .var name => env.lookup name 549 1356 | .arrayE items => do ··· 592 1399 | .ok body => some (.string body) 593 1400 | .error _ => none 594 1401 | _ => none 1402 1402 + | .var "getAturi" => 1403 1403 + let source ← evalConstData? env arg 1404 1404 + match source with 1405 1405 + | .string s => 1406 1406 + match unsafeIO (Http.parseAturi s) with 1407 1407 + | .ok rendered => 1408 1408 + match Nickel.parse rendered with 1409 1409 + | .ok term => some (Data.ofNickel term) 1410 1410 + | .error _ => none 1411 1411 + | .error _ => none 1412 1412 + | _ => none 595 1413 | .var "readFileNickel" => 596 1414 let path ← evalConstData? env arg 597 1415 match path with ··· 623 1441 | _ => none 624 1442 625 1443 unsafe def inferType (env : TyEnv) : Expr → CheckM Judgment 626 626 - | .int _ => pure (pureJudgment .int) 1444 1444 + | .int _ => pure (pureJudgment .number) 1445 1445 + | .decimal _ => pure (pureJudgment .number) 627 1446 | .bool _ => pure (pureJudgment .bool) 628 1447 | .string _ => pure (pureJudgment .string) 629 1448 | .null => pure (pureJudgment .dataNull) ··· 638 1457 let itemJs ← items.mapM (inferType env) 639 1458 let dataTys ← itemJs.mapM (fun j => 640 1459 match j.ty with 1460 1460 + | .number => pure .dataRational 641 1461 | .int => pure .dataInt 1462 1462 + | .decimal => pure .dataDecimal 1463 1463 + | .rational => pure .dataRational 642 1464 | .bool => pure .dataBool 643 1465 | .string => pure .dataString 644 1466 | .data => pure .data 645 1467 | .dataInt => pure .dataInt 1468 1468 + | .dataDecimal => pure .dataDecimal 1469 1469 + | .dataRational => pure .dataRational 646 1470 | .dataBool => pure .dataBool 647 1471 | .dataString => pure .dataString 648 1472 | .dataNull => pure .dataNull ··· 661 1485 let fieldJs ← fields.mapM (fun (name, value) => do pure (name, ← inferType env value)) 662 1486 let fieldTys ← fieldJs.mapM (fun (name, j) => do 663 1487 let ty ← match j.ty with 1488 1488 + | .number => pure .dataRational 664 1489 | .int => pure .dataInt 1490 1490 + | .decimal => pure .dataDecimal 1491 1491 + | .rational => pure .dataRational 665 1492 | .bool => pure .dataBool 666 1493 | .string => pure .dataString 667 1494 | .data => pure .data 668 1495 | .dataInt => pure .dataInt 1496 1496 + | .dataDecimal => pure .dataDecimal 1497 1497 + | .dataRational => pure .dataRational 669 1498 | .dataBool => pure .dataBool 670 1499 | .dataString => pure .dataString 671 1500 | .dataNull => pure .dataNull ··· 682 1511 | .mul lhs rhs => do 683 1512 let lhsJ ← inferType env lhs 684 1513 let rhsJ ← inferType env rhs 685 685 - ensureType .int lhsJ.ty 686 686 - ensureType .int rhsJ.ty 687 687 - pure { ty := .int, effects := lhsJ.effects.union rhsJ.effects } 1514 1514 + if isNumericTy lhsJ.ty && isNumericTy rhsJ.ty then 1515 1515 + pure { 1516 1516 + ty := .number 1517 1517 + effects := lhsJ.effects.union rhsJ.effects 1518 1518 + } 1519 1519 + else 1520 1520 + throw (.mismatch lhsJ.ty rhsJ.ty) 688 1521 | .div lhs rhs => do 689 1522 let lhsJ ← inferType env lhs 690 1523 let rhsJ ← inferType env rhs 691 691 - ensureType .int lhsJ.ty 692 692 - ensureType .int rhsJ.ty 693 693 - pure { 694 694 - ty := .int 695 695 - effects := (lhsJ.effects.union rhsJ.effects).insert .error 696 696 - } 1524 1524 + if isNumericTy lhsJ.ty && isNumericTy rhsJ.ty then 1525 1525 + pure { 1526 1526 + ty := .number 1527 1527 + effects := (lhsJ.effects.union rhsJ.effects).insert .error 1528 1528 + } 1529 1529 + else 1530 1530 + throw (.mismatch lhsJ.ty rhsJ.ty) 697 1531 | .eq lhs rhs => do 698 1532 let lhsJ ← inferType env lhs 699 1533 let rhsJ ← inferType env rhs 700 700 - ensureType .int lhsJ.ty 701 701 - ensureType .int rhsJ.ty 702 702 - pure { ty := .bool, effects := lhsJ.effects.union rhsJ.effects } 1534 1534 + if isNumericTy lhsJ.ty && isNumericTy rhsJ.ty then 1535 1535 + pure { ty := .bool, effects := lhsJ.effects.union rhsJ.effects } 1536 1536 + else 1537 1537 + throw (.mismatch lhsJ.ty rhsJ.ty) 703 1538 | .letE name value body => do 704 1539 let valueJ ← inferType env value 705 1540 let bodyJ ← inferType ((name, valueJ.ty) :: env) body ··· 791 1626 match argJ.ty with 792 1627 | .dataInt => .int 793 1628 | _ => .int 1629 1629 + | .var "asDecimal", _, .decimal => 1630 1630 + match argJ.ty with 1631 1631 + | .dataDecimal => .decimal 1632 1632 + | _ => .decimal 1633 1633 + | .var "toInt", _, .int => 1634 1634 + .int 1635 1635 + | .var "toDecimal", _, .decimal => 1636 1636 + .decimal 794 1637 | .var "asString", _, .string => 795 1638 match argJ.ty with 796 1639 | .dataString => .string ··· 799 1642 match argJ.ty with 800 1643 | .dataBool => .bool 801 1644 | _ => .bool 1645 1645 + | .app (.var "approx") _, _, .number => 1646 1646 + .number 1647 1647 + | .app (.var "stabilize") _, _, .number => 1648 1648 + .number 1649 1649 + | .app (.var "bounds") _, _, .data => 1650 1650 + .data 802 1651 | _, _, _ => resultTy 803 1652 pure { 804 1653 ty := refinedResultTy ··· 810 1659 throw (.expectedFunction fnJ.ty) 811 1660 812 1661 partial def renderType : Ty → String 1662 1662 + | .number => "Number" 813 1663 | .int => "Int" 1664 1664 + | .decimal => "Decimal" 1665 1665 + | .rational => "Number" 1666 1666 + | .lazyReal => "Number" 1667 1667 + | .stability => "Stability" 814 1668 | .bool => "Bool" 815 1669 | .string => "String" 816 1670 | .data => "Data" 817 1671 | .dataInt => "Data:Int" 1672 1672 + | .dataDecimal => "Data:Decimal" 1673 1673 + | .dataRational => "Data:Rational" 818 1674 | .dataBool => "Data:Bool" 819 1675 | .dataString => "Data:String" 820 1676 | .dataNull => "Data:Null" ··· 826 1682 | .result => "Result" 827 1683 | .error => "Error" 828 1684 | .funTy lhs effects rhs => s!"({renderType lhs} -> {renderType rhs} ! {effects.render})" 1685 1685 + 1686 1686 + def renderTypeError : TypeError → String 1687 1687 + | .unboundVariable name => s!"unbound variable {name}" 1688 1688 + | .mismatch expected actual => s!"expected {renderType expected}, got {renderType actual}" 1689 1689 + | .expectedFunction actual => s!"expected function, got {renderType actual}" 829 1690 830 1691 def renderJudgment (judgment : Judgment) : String := 831 1692 s!"{renderType judgment.ty} ! {judgment.effects.render}"

+27 -4

Mlang/Nickel.lean

View file Reviewed

··· 1 1 namespace Mlang.Nickel 2 2 3 3 + abbrev Decimal := String 4 4 + 3 5 inductive Term where 4 6 | null : Term 5 7 | bool : Bool → Term 6 8 | int : Int → Term 9 9 + | decimal : Decimal → Term 7 10 | string : String → Term 8 11 | array : List Term → Term 9 12 | record : List (String × Term) → Term ··· 77 80 | some n => pure (n, rest) 78 81 | none => throw "invalid integer literal" 79 82 83 83 + def parseNumber (input : Input) : ParseM (Term × Input) := do 84 84 + let (sign, rest) := 85 85 + match input with 86 86 + | '-' :: tail => ("-", tail) 87 87 + | _ => ("", input) 88 88 + let (wholeDigits, rest) := spanChars isDigit rest 89 89 + if wholeDigits.isEmpty then 90 90 + throw "expected numeric literal" 91 91 + else 92 92 + match rest with 93 93 + | '.' :: fracRest => 94 94 + let (fracDigits, tail) := spanChars isDigit fracRest 95 95 + if fracDigits.isEmpty then 96 96 + throw "invalid decimal literal" 97 97 + else 98 98 + pure (.decimal (sign ++ charsToString wholeDigits ++ "." ++ charsToString fracDigits), tail) 99 99 + | _ => 100 100 + match String.toInt? (sign ++ charsToString wholeDigits) with 101 101 + | some n => pure (.int n, rest) 102 102 + | none => throw "invalid integer literal" 103 103 + 80 104 def parseIdent (input : Input) : ParseM (String × Input) := do 81 105 match input with 82 106 | c :: rest => ··· 107 131 | "null" => pure (.null, rest) 108 132 | _ => throw s!"unexpected identifier '{name}'" 109 133 | '-' :: _ => 110 110 - let (n, rest) ← parseInt input 111 111 - pure (.int n, rest) 134 134 + parseNumber input 112 135 | c :: _ => 113 136 if isDigit c then 114 114 - let (n, rest) ← parseInt input 115 115 - pure (.int n, rest) 137 137 + parseNumber input 116 138 else 117 139 throw s!"unexpected character '{c}'" 118 140 ··· 178 200 | .bool true => "true" 179 201 | .bool false => "false" 180 202 | .int n => toString n 203 203 + | .decimal d => d 181 204 | .string s => s!"\"{s}\"" 182 205 | .array xs => 183 206 "[" ++ String.intercalate ", " (xs.map render) ++ "]"

+19 -4

Mlang/Parser.lean

View file Reviewed

··· 4 4 5 5 inductive Token where 6 6 | int : Int → Token 7 7 + | decimal : Decimal → Token 7 8 | bool : Bool → Token 8 9 | string : String → Token 9 10 | ident : String → Token ··· 54 55 isIdentStart c || isDigit c 55 56 56 57 def isAtomStart : Token → Bool 57 57 - | .int _ | .bool _ | .string _ | .ident _ | .lparen | .lbracket | .lbrace | .kwNull => true 58 58 + | .int _ | .decimal _ | .bool _ | .string _ | .ident _ | .lparen | .lbracket | .lbrace | .kwNull => true 58 59 | _ => false 59 60 60 61 partial def spanChars (p : Char → Bool) : List Char → List Char × List Char ··· 91 92 92 93 def lexNumber (chars : List Char) : ParseM (Token × List Char) := do 93 94 let (digits, rest) := spanChars isDigit chars 94 94 - match String.toInt? (charsToString digits) with 95 95 - | some n => pure (.int n, rest) 96 96 - | none => throw (.lexError "invalid integer literal") 95 95 + match rest with 96 96 + | '.' :: fracRest => 97 97 + let (fracDigits, tail) := spanChars isDigit fracRest 98 98 + if fracDigits.isEmpty then 99 99 + throw (.lexError "invalid decimal literal") 100 100 + else 101 101 + pure (.decimal (parseDecimal (charsToString digits ++ "." ++ charsToString fracDigits)), tail) 102 102 + | _ => 103 103 + match String.toInt? (charsToString digits) with 104 104 + | some n => pure (.int n, rest) 105 105 + | none => throw (.lexError "invalid integer literal") 97 106 98 107 partial def takeStringChars : List Char → ParseM (List Char × List Char) 99 108 | [] => throw (.lexError "unterminated string literal") ··· 186 195 | _ => pure (lhs, rest) 187 196 188 197 partial def parseTyAtom : ParserState → ParseM (Ty × ParserState) 198 198 + | .ident "Number" :: rest => pure (.number, rest) 189 199 | .ident "Int" :: rest => pure (.int, rest) 200 200 + | .ident "Decimal" :: rest => pure (.decimal, rest) 201 201 + | .ident "Rational" :: rest => pure (.number, rest) 202 202 + | .ident "Stability" :: rest => pure (.stability, rest) 190 203 | .ident "Bool" :: rest => pure (.bool, rest) 204 204 + | .ident "LazyReal" :: rest => pure (.number, rest) 191 205 | .ident "String" :: rest => pure (.string, rest) 192 206 | .ident "Data" :: rest => pure (.data, rest) 193 207 | .ident "List" :: rest => pure (.list, rest) ··· 347 361 348 362 partial def parseAtom : ParserState → ParseM (Expr × ParserState) 349 363 | .int n :: rest => pure (.int n, rest) 364 364 + | .decimal d :: rest => pure (.decimal d, rest) 350 365 | .bool b :: rest => pure (.bool b, rest) 351 366 | .string s :: rest => pure (.string s, rest) 352 367 | .kwNull :: rest => pure (.null, rest)

+41 -9

README.md

View file Reviewed

··· 4 4 5 5 Current scope: 6 6 7 7 - - integer and boolean literals 7 7 + - integer, decimal, and boolean literals 8 8 - variables 9 9 - `let` 10 10 - `if` 11 11 - typed lambdas 12 12 - function application 13 13 - - integer arithmetic 14 14 - - integer division 13 13 + - decimal arithmetic with implicit `Int` promotion 15 14 - strings 16 15 - native parsed data values 17 16 - lexical closures ··· 68 67 | { key = expr, ... } 69 68 | null 70 69 | (expr) 71 71 - | true | false | 123 | "text" | name 70 70 + | true | false | 123 | 1.23 | "text" | name 72 71 73 72 program ::= expr (';' expr)* 74 73 75 75 - type ::= Int | Bool | String | Data | List | Result | Error | type -> type | (type) 74 74 + type ::= Int | Decimal | LazyReal | Bool | String | Data | List | Result | Error | type -> type | (type) 76 75 ``` 77 76 78 77 Inside the REPL, there is also a top-level binding form: ··· 88 87 x + 1 89 88 ``` 90 89 91 91 - Expressions are checked as `Type ! Effects`. Pure expressions get `{}`; division carries `{Error}` implicitly. `readFile` is a builtin with type `String -> String ! {IO, Error}`. `readFileNickel` is a builtin with type `String -> Data ! {IO, Error}`. `parseNickel` is a builtin with type `String -> Data ! {Error}` and is backed by the real Nickel Rust crate. Nickel source is evaluated on the host side and converted back into `mlang` `Data`. Parsed data inspection is available through: 90 90 + Expressions are checked as `Type ! Effects`. Plain numeric literals now default to `Rational`, so `1`, `1.25`, `1 + 2`, and `5 / 2` are all rational values unless you explicitly cast them. Division carries `{Error}` implicitly. `readFile` is a builtin with type `String -> String ! {IO, Error}`. `readFileNickel` is a builtin with type `String -> Data ! {IO, Error}`. `parseNickel` is a builtin with type `String -> Data ! {Error}` and is backed by the real Nickel Rust crate. Nickel source is evaluated on the host side and converted back into `mlang` `Data`. Parsed data inspection is available through: 92 91 93 92 - `httpGet : String -> String ! {IO, Error}` 94 93 - `parseJson : String -> Data ! {Error}` 95 94 96 95 - `get : Data -> String -> Data ! {Error}` 97 97 - - `at : Data -> Int -> Data ! {Error}` 96 96 + - `at : Data -> Rational -> Data ! {Error}` 98 97 - `asInt : Data -> Int ! {Error}` 98 98 + - `asDecimal : Data -> Decimal ! {Error}` 99 99 - `asString : Data -> String ! {Error}` 100 100 - `asBool : Data -> Bool ! {Error}` 101 101 + - `toInt : Rational -> Int ! {Error}` 102 102 + - `toDecimal : Rational -> Decimal ! {Error}` 101 103 - `toJson : Data -> String` 102 104 - `toNickel : Data -> String` 105 105 + - `rationalStability : Rational -> Stability` 106 106 + - `decimalStability : Rational -> Stability` 107 107 + - `sqrt : Decimal -> LazyReal ! {Error}` 108 108 + - `pi : LazyReal` 109 109 + - `lazyRationalStability : LazyReal -> Stability` 110 110 + - `lazyDecimalStability : LazyReal -> Stability` 111 111 + - `approx : LazyReal -> Rational -> Rational ! {Error}` 112 112 + - `bounds : LazyReal -> Rational -> Data ! {Error}` 103 113 104 114 `httpGet` is implemented through a thin Rust host library plus a small C shim for Lean FFI. The Rust layer uses a real HTTP client crate rather than spawning an external tool. 105 115 `try ... with name => ...` handles `Error`, binds the caught error as an `Error` value, and removes `Error` from the resulting effect set when recovered locally. ··· 108 118 - `null` 109 119 - booleans 110 120 - integers 121 121 + - decimals 111 122 - strings 112 123 - arrays 113 124 - records 114 125 115 115 - Non-integer numeric Nickel values are not supported yet by `mlang`'s `Data` model. 126 126 + Exact rational values are supported in native literals and in `Data` values coming from JSON or Nickel. 116 127 117 128 Native `Data` literals are also supported directly in `mlang`: 118 129 ··· 120 131 { answer = 42, flags = [true, false], note = "ok", empty = null } 121 132 ``` 122 133 123 123 - Fields and array elements may be `Int`, `Bool`, `String`, or existing `Data` expressions. 134 134 + Fields and array elements may be `Rational`, `Bool`, `String`, or existing `Data` expressions. 135 135 + 136 136 + `LazyReal` represents process-like numeric values that are observed through refinement. The current implementation supports decimal input to `sqrt`, while `approx` and `bounds` observe lazies as rationals: 137 137 + 138 138 + ```mlang 139 139 + let r = sqrt 2.0 140 140 + approx r 4 141 141 + bounds r 4 142 142 + approx pi 4 143 143 + toDecimal (approx pi 4) 144 144 + ``` 145 145 + 146 146 + Ordinary arithmetic lifts over `LazyReal`, so expressions like `sqrt 2.0 + 3.0` stay lazy until observed with `approx` or `bounds`. 147 147 + 148 148 + Stability observations classify how a number settles under rational and decimal observation: 149 149 + 150 150 + ```mlang 151 151 + rationalStability (1 / 3) -- Immediate 152 152 + decimalStability (1 / 3) -- Periodic 153 153 + lazyRationalStability pi -- Refining 154 154 + lazyDecimalStability (sqrt 2) -- Refining 155 155 + ``` 124 156 125 157 `pmap name in expr => body` expects `expr` to evaluate to a native `Data` array. It evaluates `body` concurrently for each element bound to `name`, preserves input order, and returns a native `List` of native `Result` values instead of failing the whole traversal. 126 158

+18

examples/samples.mlg

View file Reviewed

··· 1 1 let inc = fun (x : Int) => x + 1 in inc 41; 2 2 + 1.25; 3 3 + 1.25 = 1.250; 4 4 + 5 / 2; 5 5 + 1 + 2.5; 6 6 + toInt 2; 7 7 + toDecimal (1 / 2); 8 8 + rationalStability (1 / 3); 9 9 + decimalStability (1 / 3); 10 10 + approx (sqrt 2.0) 4; 11 11 + bounds (sqrt 2.0) 4; 12 12 + approx (sqrt 2.0 + 3.0) 4; 13 13 + approx pi 4; 14 14 + approx (pi + 1.0) 4; 15 15 + lazyRationalStability pi; 16 16 + lazyDecimalStability (sqrt 2.0); 2 17 let x = 10 in let f = fun (y : Int) => x + y in let x = 100 in f 5; 3 18 if 6 * 7 = 42 then 1 else 0; 4 19 10 / 2; ··· 6 21 readFileNickel "examples/sample.ncl"; 7 22 parseNickel "{ answer = 42, flags = [true, false], note = \"ok\" }"; 8 23 parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"empty\":null}"; 24 24 + parseJson "{\"price\":12.50,\"tax\":0.075}"; 9 25 { answer = 42, flags = [true, false], note = "ok", empty = null }; 26 26 + { price = 12.50, tax = 0.075 }; 10 27 toJson (parseNickel "{ answer = 42, flags = [true, false], note = \"ok\" }"); 11 28 toJson (parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"empty\":null}"); 12 29 toJson { answer = 42, flags = [true, false], note = "ok", empty = null }; 13 30 toNickel (parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"odd key\":null}"); 14 31 get (parseNickel "{ answer = 42, flags = [true, false] }") "answer"; 15 32 get (parseJson "{\"answer\":42,\"flags\":[true,false]}") "answer"; 33 33 + get (parseJson "{\"price\":12.50}") "price"; 16 34 get { answer = 42, flags = [true, false] } "answer"; 17 35 at (get (parseNickel "{ flags = [true, false] }") "flags") 1; 18 36 -> "examples/sample.ncl" readFileNickel (get "answer");

+1734 -20

native/mlang_http/Cargo.lock

View file Reviewed

··· 33 33 checksum = "250f629c0161ad8107cf89319e990051fae62832fd343083bea452d93e2205fd" 34 34 35 35 [[package]] 36 36 + name = "allocator-api2" 37 37 + version = "0.2.21" 38 38 + source = "registry+https://github.com/rust-lang/crates.io-index" 39 39 + checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" 40 40 + 41 41 + [[package]] 36 42 name = "anstream" 37 43 version = "1.0.0" 38 44 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 83 89 ] 84 90 85 91 [[package]] 92 92 + name = "anyhow" 93 93 + version = "1.0.102" 94 94 + source = "registry+https://github.com/rust-lang/crates.io-index" 95 95 + checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" 96 96 + 97 97 + [[package]] 86 98 name = "arraydeque" 87 99 version = "0.5.1" 88 100 source = "registry+https://github.com/rust-lang/crates.io-index" 89 101 checksum = "7d902e3d592a523def97af8f317b08ce16b7ab854c1985a0c671e6f15cebc236" 90 102 91 103 [[package]] 104 104 + name = "arrayref" 105 105 + version = "0.3.9" 106 106 + source = "registry+https://github.com/rust-lang/crates.io-index" 107 107 + checksum = "76a2e8124351fda1ef8aaaa3bbd7ebbcb486bbcd4225aca0aa0d84bb2db8fecb" 108 108 + 109 109 + [[package]] 92 110 name = "arrayvec" 93 111 version = "0.5.2" 94 112 source = "registry+https://github.com/rust-lang/crates.io-index" 95 113 checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b" 96 114 97 115 [[package]] 116 116 + name = "arrayvec" 117 117 + version = "0.7.6" 118 118 + source = "registry+https://github.com/rust-lang/crates.io-index" 119 119 + checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50" 120 120 + 121 121 + [[package]] 98 122 name = "ascii-canvas" 99 123 version = "4.0.0" 100 124 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 104 128 ] 105 129 106 130 [[package]] 131 131 + name = "async-trait" 132 132 + version = "0.1.89" 133 133 + source = "registry+https://github.com/rust-lang/crates.io-index" 134 134 + checksum = "9035ad2d096bed7955a320ee7e2230574d28fd3c3a0f186cbea1ff3c7eed5dbb" 135 135 + dependencies = [ 136 136 + "proc-macro2", 137 137 + "quote", 138 138 + "syn", 139 139 + ] 140 140 + 141 141 + [[package]] 142 142 + name = "atomic-waker" 143 143 + version = "1.1.2" 144 144 + source = "registry+https://github.com/rust-lang/crates.io-index" 145 145 + checksum = "1505bd5d3d116872e7271a6d4e16d81d0c8570876c8de68093a09ac269d8aac0" 146 146 + 147 147 + [[package]] 148 148 + name = "atproto-client" 149 149 + version = "0.14.5" 150 150 + source = "registry+https://github.com/rust-lang/crates.io-index" 151 151 + checksum = "b0c1438d67d1fe2d06b5e5f8030c58cce991e074bab03b5e226a949507172f24" 152 152 + dependencies = [ 153 153 + "anyhow", 154 154 + "async-trait", 155 155 + "atproto-identity", 156 156 + "atproto-oauth", 157 157 + "atproto-record", 158 158 + "bytes", 159 159 + "reqwest", 160 160 + "reqwest-chain", 161 161 + "reqwest-middleware", 162 162 + "serde", 163 163 + "serde_json", 164 164 + "thiserror 2.0.18", 165 165 + "tokio", 166 166 + "tracing", 167 167 + "urlencoding", 168 168 + ] 169 169 + 170 170 + [[package]] 171 171 + name = "atproto-dasl" 172 172 + version = "0.14.5" 173 173 + source = "registry+https://github.com/rust-lang/crates.io-index" 174 174 + checksum = "a28d38577f468ab23e3351835f370cf34270caf290205a7e1520d352f5be4b28" 175 175 + dependencies = [ 176 176 + "blake3", 177 177 + "cid", 178 178 + "futures", 179 179 + "multihash", 180 180 + "serde", 181 181 + "serde_bytes", 182 182 + "sha2 0.11.0", 183 183 + "tempfile", 184 184 + "thiserror 2.0.18", 185 185 + "tokio", 186 186 + "tracing", 187 187 + "url", 188 188 + ] 189 189 + 190 190 + [[package]] 191 191 + name = "atproto-identity" 192 192 + version = "0.14.5" 193 193 + source = "registry+https://github.com/rust-lang/crates.io-index" 194 194 + checksum = "722940aeee9654eef58cdd8b70d62772357621a2587367191b1c5630742f8e77" 195 195 + dependencies = [ 196 196 + "anyhow", 197 197 + "async-trait", 198 198 + "atproto-dasl", 199 199 + "base64", 200 200 + "chrono", 201 201 + "data-encoding", 202 202 + "ecdsa", 203 203 + "ed25519-dalek", 204 204 + "elliptic-curve", 205 205 + "hickory-resolver", 206 206 + "idna", 207 207 + "k256", 208 208 + "lru", 209 209 + "multibase", 210 210 + "p256", 211 211 + "p384", 212 212 + "rand 0.10.1", 213 213 + "reqwest", 214 214 + "serde", 215 215 + "serde_json", 216 216 + "sha2 0.11.0", 217 217 + "thiserror 2.0.18", 218 218 + "tokio", 219 219 + "tracing", 220 220 + "url", 221 221 + ] 222 222 + 223 223 + [[package]] 224 224 + name = "atproto-oauth" 225 225 + version = "0.14.5" 226 226 + source = "registry+https://github.com/rust-lang/crates.io-index" 227 227 + checksum = "8f9b1e34b59d7d1f641dd03a2b05b5153a2a4eb2ef1b36d6d7fbbf80a4aa954b" 228 228 + dependencies = [ 229 229 + "anyhow", 230 230 + "async-trait", 231 231 + "atproto-identity", 232 232 + "base64", 233 233 + "chrono", 234 234 + "ecdsa", 235 235 + "elliptic-curve", 236 236 + "k256", 237 237 + "lru", 238 238 + "multibase", 239 239 + "p256", 240 240 + "p384", 241 241 + "rand 0.10.1", 242 242 + "reqwest", 243 243 + "reqwest-chain", 244 244 + "reqwest-middleware", 245 245 + "serde", 246 246 + "serde_json", 247 247 + "sha2 0.11.0", 248 248 + "thiserror 2.0.18", 249 249 + "tokio", 250 250 + "tracing", 251 251 + "ulid", 252 252 + ] 253 253 + 254 254 + [[package]] 255 255 + name = "atproto-record" 256 256 + version = "0.14.5" 257 257 + source = "registry+https://github.com/rust-lang/crates.io-index" 258 258 + checksum = "52a83494a80a9add1c3678e821f92153a4b5d139c0b6898bbf5eb97501cf2359" 259 259 + dependencies = [ 260 260 + "anyhow", 261 261 + "atproto-dasl", 262 262 + "atproto-identity", 263 263 + "base64", 264 264 + "chrono", 265 265 + "cid", 266 266 + "multihash", 267 267 + "rand 0.10.1", 268 268 + "serde", 269 269 + "serde_json", 270 270 + "sha2 0.11.0", 271 271 + "thiserror 2.0.18", 272 272 + ] 273 273 + 274 274 + [[package]] 275 275 + name = "autocfg" 276 276 + version = "1.5.1" 277 277 + source = "registry+https://github.com/rust-lang/crates.io-index" 278 278 + checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" 279 279 + 280 280 + [[package]] 107 281 name = "backtrace" 108 282 version = "0.3.76" 109 283 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 128 302 ] 129 303 130 304 [[package]] 305 305 + name = "base-x" 306 306 + version = "0.2.11" 307 307 + source = "registry+https://github.com/rust-lang/crates.io-index" 308 308 + checksum = "4cbbc9d0964165b47557570cce6c952866c2678457aca742aafc9fb771d30270" 309 309 + 310 310 + [[package]] 311 311 + name = "base16ct" 312 312 + version = "0.2.0" 313 313 + source = "registry+https://github.com/rust-lang/crates.io-index" 314 314 + checksum = "4c7f02d4ea65f2c1853089ffd8d2787bdbc63de2f0d29dedbcf8ccdfa0ccd4cf" 315 315 + 316 316 + [[package]] 317 317 + name = "base256emoji" 318 318 + version = "1.0.2" 319 319 + source = "registry+https://github.com/rust-lang/crates.io-index" 320 320 + checksum = "b5e9430d9a245a77c92176e649af6e275f20839a48389859d1661e9a128d077c" 321 321 + dependencies = [ 322 322 + "const-str", 323 323 + "match-lookup", 324 324 + ] 325 325 + 326 326 + [[package]] 131 327 name = "base64" 132 328 version = "0.22.1" 133 329 source = "registry+https://github.com/rust-lang/crates.io-index" 134 330 checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6" 331 331 + 332 332 + [[package]] 333 333 + name = "base64ct" 334 334 + version = "1.8.3" 335 335 + source = "registry+https://github.com/rust-lang/crates.io-index" 336 336 + checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" 135 337 136 338 [[package]] 137 339 name = "bincode" ··· 170 372 checksum = "a1d084b0137aaa901caf9f1e8b21daa6aa24d41cd806e111335541eff9683bd6" 171 373 172 374 [[package]] 375 375 + name = "blake3" 376 376 + version = "1.8.5" 377 377 + source = "registry+https://github.com/rust-lang/crates.io-index" 378 378 + checksum = "0aa83c34e62843d924f905e0f5c866eb1dd6545fc4d719e803d9ba6030371fce" 379 379 + dependencies = [ 380 380 + "arrayref", 381 381 + "arrayvec 0.7.6", 382 382 + "cc", 383 383 + "cfg-if", 384 384 + "constant_time_eq", 385 385 + "cpufeatures 0.3.0", 386 386 + ] 387 387 + 388 388 + [[package]] 173 389 name = "block-buffer" 174 390 version = "0.10.4" 175 391 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 179 395 ] 180 396 181 397 [[package]] 398 398 + name = "block-buffer" 399 399 + version = "0.12.0" 400 400 + source = "registry+https://github.com/rust-lang/crates.io-index" 401 401 + checksum = "cdd35008169921d80bc60d3d0ab416eecb028c4cd653352907921d95084790be" 402 402 + dependencies = [ 403 403 + "hybrid-array", 404 404 + ] 405 405 + 406 406 + [[package]] 182 407 name = "bon" 183 408 version = "3.9.1" 184 409 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 216 441 checksum = "c8efb64bd706a16a1bdde310ae86b351e4d21550d98d056f22f8a7f7a2183fec" 217 442 218 443 [[package]] 444 444 + name = "bytes" 445 445 + version = "1.11.1" 446 446 + source = "registry+https://github.com/rust-lang/crates.io-index" 447 447 + checksum = "1e748733b7cbc798e1434b6ac524f0c1ff2ab456fe201501e6497c8417a4fc33" 448 448 + 449 449 + [[package]] 219 450 name = "caseless" 220 451 version = "0.2.2" 221 452 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 247 478 checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" 248 479 249 480 [[package]] 481 481 + name = "chacha20" 482 482 + version = "0.10.0" 483 483 + source = "registry+https://github.com/rust-lang/crates.io-index" 484 484 + checksum = "6f8d983286843e49675a4b7a2d174efe136dc93a18d69130dd18198a6c167601" 485 485 + dependencies = [ 486 486 + "cfg-if", 487 487 + "cpufeatures 0.3.0", 488 488 + "rand_core 0.10.1", 489 489 + ] 490 490 + 491 491 + [[package]] 492 492 + name = "chrono" 493 493 + version = "0.4.44" 494 494 + source = "registry+https://github.com/rust-lang/crates.io-index" 495 495 + checksum = "c673075a2e0e5f4a1dde27ce9dee1ea4558c7ffe648f576438a20ca1d2acc4b0" 496 496 + dependencies = [ 497 497 + "num-traits", 498 498 + "serde", 499 499 + ] 500 500 + 501 501 + [[package]] 502 502 + name = "cid" 503 503 + version = "0.11.3" 504 504 + source = "registry+https://github.com/rust-lang/crates.io-index" 505 505 + checksum = "21a304f95f84d169a6f31c4d0a30d784643aaa0bbc9c1e449a2c23e963ec4971" 506 506 + dependencies = [ 507 507 + "multibase", 508 508 + "multihash", 509 509 + "unsigned-varint", 510 510 + ] 511 511 + 512 512 + [[package]] 250 513 name = "clap" 251 514 version = "4.6.1" 252 515 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 344 607 ] 345 608 346 609 [[package]] 610 610 + name = "const-oid" 611 611 + version = "0.9.6" 612 612 + source = "registry+https://github.com/rust-lang/crates.io-index" 613 613 + checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8" 614 614 + 615 615 + [[package]] 616 616 + name = "const-oid" 617 617 + version = "0.10.2" 618 618 + source = "registry+https://github.com/rust-lang/crates.io-index" 619 619 + checksum = "a6ef517f0926dd24a1582492c791b6a4818a4d94e789a334894aa15b0d12f55c" 620 620 + 621 621 + [[package]] 622 622 + name = "const-str" 623 623 + version = "0.4.3" 624 624 + source = "registry+https://github.com/rust-lang/crates.io-index" 625 625 + checksum = "2f421161cb492475f1661ddc9815a745a1c894592070661180fdec3d4872e9c3" 626 626 + 627 627 + [[package]] 628 628 + name = "constant_time_eq" 629 629 + version = "0.4.2" 630 630 + source = "registry+https://github.com/rust-lang/crates.io-index" 631 631 + checksum = "3d52eff69cd5e647efe296129160853a42795992097e8af39800e1060caeea9b" 632 632 + 633 633 + [[package]] 347 634 name = "convert_case" 348 635 version = "0.10.0" 349 636 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 362 649 ] 363 650 364 651 [[package]] 652 652 + name = "core-foundation" 653 653 + version = "0.9.4" 654 654 + source = "registry+https://github.com/rust-lang/crates.io-index" 655 655 + checksum = "91e195e091a93c46f7102ec7818a2aa394e1e1771c3ab4825963fa03e45afb8f" 656 656 + dependencies = [ 657 657 + "core-foundation-sys", 658 658 + "libc", 659 659 + ] 660 660 + 661 661 + [[package]] 662 662 + name = "core-foundation-sys" 663 663 + version = "0.8.7" 664 664 + source = "registry+https://github.com/rust-lang/crates.io-index" 665 665 + checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" 666 666 + 667 667 + [[package]] 365 668 name = "cpufeatures" 366 669 version = "0.2.17" 367 670 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 371 674 ] 372 675 373 676 [[package]] 677 677 + name = "cpufeatures" 678 678 + version = "0.3.0" 679 679 + source = "registry+https://github.com/rust-lang/crates.io-index" 680 680 + checksum = "8b2a41393f66f16b0823bb79094d54ac5fbd34ab292ddafb9a0456ac9f87d201" 681 681 + dependencies = [ 682 682 + "libc", 683 683 + ] 684 684 + 685 685 + [[package]] 374 686 name = "crc32fast" 375 687 version = "1.5.0" 376 688 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 378 690 dependencies = [ 379 691 "cfg-if", 380 692 ] 693 693 + 694 694 + [[package]] 695 695 + name = "critical-section" 696 696 + version = "1.2.0" 697 697 + source = "registry+https://github.com/rust-lang/crates.io-index" 698 698 + checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" 381 699 382 700 [[package]] 383 701 name = "crokey" ··· 486 804 checksum = "acdd7c62a3665c7f6830a51635d9ac9b23ed385797f70a83bb8bafe9c572ab2b" 487 805 dependencies = [ 488 806 "winapi", 807 807 + ] 808 808 + 809 809 + [[package]] 810 810 + name = "crypto-bigint" 811 811 + version = "0.5.5" 812 812 + source = "registry+https://github.com/rust-lang/crates.io-index" 813 813 + checksum = "0dc92fb57ca44df6db8059111ab3af99a63d5d0f8375d9972e319a379c6bab76" 814 814 + dependencies = [ 815 815 + "generic-array", 816 816 + "rand_core 0.6.4", 817 817 + "subtle", 818 818 + "zeroize", 489 819 ] 490 820 491 821 [[package]] ··· 499 829 ] 500 830 501 831 [[package]] 832 832 + name = "crypto-common" 833 833 + version = "0.2.2" 834 834 + source = "registry+https://github.com/rust-lang/crates.io-index" 835 835 + checksum = "ce6e4c961d6cd6c9a86db418387425e8bdeaf05b3c8bc1411e6dca4c252f1453" 836 836 + dependencies = [ 837 837 + "hybrid-array", 838 838 + ] 839 839 + 840 840 + [[package]] 841 841 + name = "curve25519-dalek" 842 842 + version = "4.1.3" 843 843 + source = "registry+https://github.com/rust-lang/crates.io-index" 844 844 + checksum = "97fb8b7c4503de7d6ae7b42ab72a5a59857b4c937ec27a3d4539dba95b5ab2be" 845 845 + dependencies = [ 846 846 + "cfg-if", 847 847 + "cpufeatures 0.2.17", 848 848 + "curve25519-dalek-derive", 849 849 + "digest 0.10.7", 850 850 + "fiat-crypto", 851 851 + "rustc_version", 852 852 + "subtle", 853 853 + "zeroize", 854 854 + ] 855 855 + 856 856 + [[package]] 857 857 + name = "curve25519-dalek-derive" 858 858 + version = "0.1.1" 859 859 + source = "registry+https://github.com/rust-lang/crates.io-index" 860 860 + checksum = "f46882e17999c6cc590af592290432be3bce0428cb0d5f8b6715e4dc7b383eb3" 861 861 + dependencies = [ 862 862 + "proc-macro2", 863 863 + "quote", 864 864 + "syn", 865 865 + ] 866 866 + 867 867 + [[package]] 502 868 name = "darling" 503 869 version = "0.23.0" 504 870 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 533 899 ] 534 900 535 901 [[package]] 902 902 + name = "data-encoding" 903 903 + version = "2.11.0" 904 904 + source = "registry+https://github.com/rust-lang/crates.io-index" 905 905 + checksum = "a4ae5f15dda3c708c0ade84bfee31ccab44a3da4f88015ed22f63732abe300c8" 906 906 + 907 907 + [[package]] 908 908 + name = "data-encoding-macro" 909 909 + version = "0.1.20" 910 910 + source = "registry+https://github.com/rust-lang/crates.io-index" 911 911 + checksum = "3259c913752a86488b501ed8680446a5ed2d5aeac6e596cb23ba3800768ea32c" 912 912 + dependencies = [ 913 913 + "data-encoding", 914 914 + "data-encoding-macro-internal", 915 915 + ] 916 916 + 917 917 + [[package]] 918 918 + name = "data-encoding-macro-internal" 919 919 + version = "0.1.18" 920 920 + source = "registry+https://github.com/rust-lang/crates.io-index" 921 921 + checksum = "ccc2776f0c61eca1ca32528f85548abd1a4be8fb53d1b21c013e4f18da1e7090" 922 922 + dependencies = [ 923 923 + "data-encoding", 924 924 + "syn", 925 925 + ] 926 926 + 927 927 + [[package]] 928 928 + name = "der" 929 929 + version = "0.7.10" 930 930 + source = "registry+https://github.com/rust-lang/crates.io-index" 931 931 + checksum = "e7c1832837b905bbfb5101e07cc24c8deddf52f93225eee6ead5f4d63d53ddcb" 932 932 + dependencies = [ 933 933 + "const-oid 0.9.6", 934 934 + "pem-rfc7468", 935 935 + "zeroize", 936 936 + ] 937 937 + 938 938 + [[package]] 536 939 name = "deranged" 537 940 version = "0.5.8" 538 941 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 575 978 source = "registry+https://github.com/rust-lang/crates.io-index" 576 979 checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" 577 980 dependencies = [ 578 578 - "block-buffer", 579 579 - "crypto-common", 981 981 + "block-buffer 0.10.4", 982 982 + "const-oid 0.9.6", 983 983 + "crypto-common 0.1.7", 984 984 + "subtle", 985 985 + ] 986 986 + 987 987 + [[package]] 988 988 + name = "digest" 989 989 + version = "0.11.3" 990 990 + source = "registry+https://github.com/rust-lang/crates.io-index" 991 991 + checksum = "f1dd6dbb5841937940781866fa1281a1ff7bd3bf827091440879f9994983d5c2" 992 992 + dependencies = [ 993 993 + "block-buffer 0.12.0", 994 994 + "const-oid 0.10.2", 995 995 + "crypto-common 0.2.2", 580 996 ] 581 997 582 998 [[package]] ··· 600 1016 ] 601 1017 602 1018 [[package]] 1019 1019 + name = "ecdsa" 1020 1020 + version = "0.16.9" 1021 1021 + source = "registry+https://github.com/rust-lang/crates.io-index" 1022 1022 + checksum = "ee27f32b5c5292967d2d4a9d7f1e0b0aed2c15daded5a60300e4abb9d8020bca" 1023 1023 + dependencies = [ 1024 1024 + "der", 1025 1025 + "digest 0.10.7", 1026 1026 + "elliptic-curve", 1027 1027 + "rfc6979", 1028 1028 + "serdect", 1029 1029 + "signature", 1030 1030 + "spki", 1031 1031 + ] 1032 1032 + 1033 1033 + [[package]] 1034 1034 + name = "ed25519" 1035 1035 + version = "2.2.3" 1036 1036 + source = "registry+https://github.com/rust-lang/crates.io-index" 1037 1037 + checksum = "115531babc129696a58c64a4fef0a8bf9e9698629fb97e9e40767d235cfbcd53" 1038 1038 + dependencies = [ 1039 1039 + "pkcs8", 1040 1040 + "signature", 1041 1041 + ] 1042 1042 + 1043 1043 + [[package]] 1044 1044 + name = "ed25519-dalek" 1045 1045 + version = "2.2.0" 1046 1046 + source = "registry+https://github.com/rust-lang/crates.io-index" 1047 1047 + checksum = "70e796c081cee67dc755e1a36a0a172b897fab85fc3f6bc48307991f64e4eca9" 1048 1048 + dependencies = [ 1049 1049 + "curve25519-dalek", 1050 1050 + "ed25519", 1051 1051 + "rand_core 0.6.4", 1052 1052 + "serde", 1053 1053 + "sha2 0.10.9", 1054 1054 + "subtle", 1055 1055 + "zeroize", 1056 1056 + ] 1057 1057 + 1058 1058 + [[package]] 603 1059 name = "either" 604 1060 version = "1.16.0" 605 1061 source = "registry+https://github.com/rust-lang/crates.io-index" 606 1062 checksum = "91622ff5e7162018101f2fea40d6ebf4a78bbe5a49736a2020649edf9693679e" 607 1063 608 1064 [[package]] 1065 1065 + name = "elliptic-curve" 1066 1066 + version = "0.13.8" 1067 1067 + source = "registry+https://github.com/rust-lang/crates.io-index" 1068 1068 + checksum = "b5e6043086bf7973472e0c7dff2142ea0b680d30e18d9cc40f267efbf222bd47" 1069 1069 + dependencies = [ 1070 1070 + "base16ct", 1071 1071 + "base64ct", 1072 1072 + "crypto-bigint", 1073 1073 + "digest 0.10.7", 1074 1074 + "ff", 1075 1075 + "generic-array", 1076 1076 + "group", 1077 1077 + "hkdf", 1078 1078 + "pem-rfc7468", 1079 1079 + "pkcs8", 1080 1080 + "rand_core 0.6.4", 1081 1081 + "sec1", 1082 1082 + "serde_json", 1083 1083 + "serdect", 1084 1084 + "subtle", 1085 1085 + "zeroize", 1086 1086 + ] 1087 1087 + 1088 1088 + [[package]] 609 1089 name = "emojis" 610 1090 version = "0.6.4" 611 1091 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 624 1104 ] 625 1105 626 1106 [[package]] 1107 1107 + name = "encoding_rs" 1108 1108 + version = "0.8.35" 1109 1109 + source = "registry+https://github.com/rust-lang/crates.io-index" 1110 1110 + checksum = "75030f3c4f45dafd7586dd6780965a8c7e8e285a5ecb86713e63a79c5b2766f3" 1111 1111 + dependencies = [ 1112 1112 + "cfg-if", 1113 1113 + ] 1114 1114 + 1115 1115 + [[package]] 627 1116 name = "endian-type" 628 1117 version = "0.1.2" 629 1118 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 636 1125 checksum = "b5320ae4c3782150d900b79807611a59a99fc9a1d61d686faafc24b93fc8d7ca" 637 1126 638 1127 [[package]] 1128 1128 + name = "enum-as-inner" 1129 1129 + version = "0.6.1" 1130 1130 + source = "registry+https://github.com/rust-lang/crates.io-index" 1131 1131 + checksum = "a1e6a265c649f3f5979b601d26f1d05ada116434c87741c9493cb56218f76cbc" 1132 1132 + dependencies = [ 1133 1133 + "heck 0.5.0", 1134 1134 + "proc-macro2", 1135 1135 + "quote", 1136 1136 + "syn", 1137 1137 + ] 1138 1138 + 1139 1139 + [[package]] 639 1140 name = "equivalent" 640 1141 version = "1.0.2" 641 1142 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 648 1149 checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" 649 1150 dependencies = [ 650 1151 "libc", 651 651 - "windows-sys 0.52.0", 1152 1152 + "windows-sys 0.61.2", 652 1153 ] 653 1154 654 1155 [[package]] ··· 667 1168 "regex-automata", 668 1169 "regex-syntax", 669 1170 ] 1171 1171 + 1172 1172 + [[package]] 1173 1173 + name = "fastrand" 1174 1174 + version = "2.4.1" 1175 1175 + source = "registry+https://github.com/rust-lang/crates.io-index" 1176 1176 + checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6" 670 1177 671 1178 [[package]] 672 1179 name = "fd-lock" ··· 676 1183 dependencies = [ 677 1184 "cfg-if", 678 1185 "rustix", 679 679 - "windows-sys 0.52.0", 1186 1186 + "windows-sys 0.59.0", 680 1187 ] 1188 1188 + 1189 1189 + [[package]] 1190 1190 + name = "ff" 1191 1191 + version = "0.13.1" 1192 1192 + source = "registry+https://github.com/rust-lang/crates.io-index" 1193 1193 + checksum = "c0b50bfb653653f9ca9095b427bed08ab8d75a137839d9ad64eb11810d5b6393" 1194 1194 + dependencies = [ 1195 1195 + "rand_core 0.6.4", 1196 1196 + "subtle", 1197 1197 + ] 1198 1198 + 1199 1199 + [[package]] 1200 1200 + name = "fiat-crypto" 1201 1201 + version = "0.2.9" 1202 1202 + source = "registry+https://github.com/rust-lang/crates.io-index" 1203 1203 + checksum = "28dea519a9695b9977216879a3ebfddf92f1c08c05d984f8996aecd6ecdc811d" 681 1204 682 1205 [[package]] 683 1206 name = "find-msvc-tools" ··· 830 1353 dependencies = [ 831 1354 "typenum", 832 1355 "version_check", 1356 1356 + "zeroize", 833 1357 ] 834 1358 835 1359 [[package]] ··· 839 1363 checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0" 840 1364 dependencies = [ 841 1365 "cfg-if", 1366 1366 + "js-sys", 842 1367 "libc", 843 1368 "wasi", 1369 1369 + "wasm-bindgen", 1370 1370 + ] 1371 1371 + 1372 1372 + [[package]] 1373 1373 + name = "getrandom" 1374 1374 + version = "0.3.4" 1375 1375 + source = "registry+https://github.com/rust-lang/crates.io-index" 1376 1376 + checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" 1377 1377 + dependencies = [ 1378 1378 + "cfg-if", 1379 1379 + "js-sys", 1380 1380 + "libc", 1381 1381 + "r-efi 5.3.0", 1382 1382 + "wasip2", 1383 1383 + "wasm-bindgen", 1384 1384 + ] 1385 1385 + 1386 1386 + [[package]] 1387 1387 + name = "getrandom" 1388 1388 + version = "0.4.2" 1389 1389 + source = "registry+https://github.com/rust-lang/crates.io-index" 1390 1390 + checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555" 1391 1391 + dependencies = [ 1392 1392 + "cfg-if", 1393 1393 + "libc", 1394 1394 + "r-efi 6.0.0", 1395 1395 + "rand_core 0.10.1", 1396 1396 + "wasip2", 1397 1397 + "wasip3", 844 1398 ] 845 1399 846 1400 [[package]] ··· 850 1404 checksum = "e629b9b98ef3dd8afe6ca2bd0f89306cec16d43d907889945bc5d6687f2f13c7" 851 1405 852 1406 [[package]] 1407 1407 + name = "group" 1408 1408 + version = "0.13.0" 1409 1409 + source = "registry+https://github.com/rust-lang/crates.io-index" 1410 1410 + checksum = "f0f9ef7462f7c099f518d754361858f86d8a07af53ba9af0fe635bbccb151a63" 1411 1411 + dependencies = [ 1412 1412 + "ff", 1413 1413 + "rand_core 0.6.4", 1414 1414 + "subtle", 1415 1415 + ] 1416 1416 + 1417 1417 + [[package]] 1418 1418 + name = "h2" 1419 1419 + version = "0.4.14" 1420 1420 + source = "registry+https://github.com/rust-lang/crates.io-index" 1421 1421 + checksum = "171fefbc92fe4a4de27e0698d6a5b392d6a0e333506bc49133760b3bcf948733" 1422 1422 + dependencies = [ 1423 1423 + "atomic-waker", 1424 1424 + "bytes", 1425 1425 + "fnv", 1426 1426 + "futures-core", 1427 1427 + "futures-sink", 1428 1428 + "http", 1429 1429 + "indexmap", 1430 1430 + "slab", 1431 1431 + "tokio", 1432 1432 + "tokio-util", 1433 1433 + "tracing", 1434 1434 + ] 1435 1435 + 1436 1436 + [[package]] 853 1437 name = "hashbrown" 854 1438 version = "0.15.5" 855 1439 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 864 1448 source = "registry+https://github.com/rust-lang/crates.io-index" 865 1449 checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100" 866 1450 dependencies = [ 1451 1451 + "allocator-api2", 1452 1452 + "equivalent", 867 1453 "foldhash 0.2.0", 868 1454 ] 869 1455 ··· 893 1479 version = "0.5.0" 894 1480 source = "registry+https://github.com/rust-lang/crates.io-index" 895 1481 checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" 1482 1482 + 1483 1483 + [[package]] 1484 1484 + name = "hickory-proto" 1485 1485 + version = "0.25.2" 1486 1486 + source = "registry+https://github.com/rust-lang/crates.io-index" 1487 1487 + checksum = "f8a6fe56c0038198998a6f217ca4e7ef3a5e51f46163bd6dd60b5c71ca6c6502" 1488 1488 + dependencies = [ 1489 1489 + "async-trait", 1490 1490 + "cfg-if", 1491 1491 + "data-encoding", 1492 1492 + "enum-as-inner", 1493 1493 + "futures-channel", 1494 1494 + "futures-io", 1495 1495 + "futures-util", 1496 1496 + "idna", 1497 1497 + "ipnet", 1498 1498 + "once_cell", 1499 1499 + "rand 0.9.4", 1500 1500 + "ring", 1501 1501 + "thiserror 2.0.18", 1502 1502 + "tinyvec", 1503 1503 + "tokio", 1504 1504 + "tracing", 1505 1505 + "url", 1506 1506 + ] 1507 1507 + 1508 1508 + [[package]] 1509 1509 + name = "hickory-resolver" 1510 1510 + version = "0.25.2" 1511 1511 + source = "registry+https://github.com/rust-lang/crates.io-index" 1512 1512 + checksum = "dc62a9a99b0bfb44d2ab95a7208ac952d31060efc16241c87eaf36406fecf87a" 1513 1513 + dependencies = [ 1514 1514 + "cfg-if", 1515 1515 + "futures-util", 1516 1516 + "hickory-proto", 1517 1517 + "ipconfig", 1518 1518 + "moka", 1519 1519 + "once_cell", 1520 1520 + "parking_lot", 1521 1521 + "rand 0.9.4", 1522 1522 + "resolv-conf", 1523 1523 + "smallvec", 1524 1524 + "thiserror 2.0.18", 1525 1525 + "tokio", 1526 1526 + "tracing", 1527 1527 + ] 1528 1528 + 1529 1529 + [[package]] 1530 1530 + name = "hkdf" 1531 1531 + version = "0.12.4" 1532 1532 + source = "registry+https://github.com/rust-lang/crates.io-index" 1533 1533 + checksum = "7b5f8eb2ad728638ea2c7d47a21db23b7b58a72ed6a38256b8a1849f15fbbdf7" 1534 1534 + dependencies = [ 1535 1535 + "hmac", 1536 1536 + ] 1537 1537 + 1538 1538 + [[package]] 1539 1539 + name = "hmac" 1540 1540 + version = "0.12.1" 1541 1541 + source = "registry+https://github.com/rust-lang/crates.io-index" 1542 1542 + checksum = "6c49c37c09c17a53d937dfbb742eb3a961d65a994e6bcdcf37e7399d0cc8ab5e" 1543 1543 + dependencies = [ 1544 1544 + "digest 0.10.7", 1545 1545 + ] 896 1546 897 1547 [[package]] 898 1548 name = "home" ··· 904 1554 ] 905 1555 906 1556 [[package]] 1557 1557 + name = "http" 1558 1558 + version = "1.4.1" 1559 1559 + source = "registry+https://github.com/rust-lang/crates.io-index" 1560 1560 + checksum = "8be7462df143984c4598a256ef469b251d7d7f9e271135073e78fc535414f3d0" 1561 1561 + dependencies = [ 1562 1562 + "bytes", 1563 1563 + "itoa", 1564 1564 + ] 1565 1565 + 1566 1566 + [[package]] 1567 1567 + name = "http-body" 1568 1568 + version = "1.0.1" 1569 1569 + source = "registry+https://github.com/rust-lang/crates.io-index" 1570 1570 + checksum = "1efedce1fb8e6913f23e0c92de8e62cd5b772a67e7b3946df930a62566c93184" 1571 1571 + dependencies = [ 1572 1572 + "bytes", 1573 1573 + "http", 1574 1574 + ] 1575 1575 + 1576 1576 + [[package]] 1577 1577 + name = "http-body-util" 1578 1578 + version = "0.1.3" 1579 1579 + source = "registry+https://github.com/rust-lang/crates.io-index" 1580 1580 + checksum = "b021d93e26becf5dc7e1b75b1bed1fd93124b374ceb73f43d4d4eafec896a64a" 1581 1581 + dependencies = [ 1582 1582 + "bytes", 1583 1583 + "futures-core", 1584 1584 + "http", 1585 1585 + "http-body", 1586 1586 + "pin-project-lite", 1587 1587 + ] 1588 1588 + 1589 1589 + [[package]] 1590 1590 + name = "httparse" 1591 1591 + version = "1.10.1" 1592 1592 + source = "registry+https://github.com/rust-lang/crates.io-index" 1593 1593 + checksum = "6dbf3de79e51f3d586ab4cb9d5c3e2c14aa28ed23d180cf89b4df0454a69cc87" 1594 1594 + 1595 1595 + [[package]] 1596 1596 + name = "hybrid-array" 1597 1597 + version = "0.4.12" 1598 1598 + source = "registry+https://github.com/rust-lang/crates.io-index" 1599 1599 + checksum = "9155a582abd142abc056962c29e3ce5ff2ad5469f4246b537ed42c5deba857da" 1600 1600 + dependencies = [ 1601 1601 + "typenum", 1602 1602 + ] 1603 1603 + 1604 1604 + [[package]] 1605 1605 + name = "hyper" 1606 1606 + version = "1.10.1" 1607 1607 + source = "registry+https://github.com/rust-lang/crates.io-index" 1608 1608 + checksum = "55281c53a1894c864990125767da440a4e630446785086f52523b20033b74498" 1609 1609 + dependencies = [ 1610 1610 + "atomic-waker", 1611 1611 + "bytes", 1612 1612 + "futures-channel", 1613 1613 + "futures-core", 1614 1614 + "h2", 1615 1615 + "http", 1616 1616 + "http-body", 1617 1617 + "httparse", 1618 1618 + "itoa", 1619 1619 + "pin-project-lite", 1620 1620 + "smallvec", 1621 1621 + "tokio", 1622 1622 + "want", 1623 1623 + ] 1624 1624 + 1625 1625 + [[package]] 1626 1626 + name = "hyper-rustls" 1627 1627 + version = "0.27.9" 1628 1628 + source = "registry+https://github.com/rust-lang/crates.io-index" 1629 1629 + checksum = "33ca68d021ef39cf6463ab54c1d0f5daf03377b70561305bb89a8f83aab66e0f" 1630 1630 + dependencies = [ 1631 1631 + "http", 1632 1632 + "hyper", 1633 1633 + "hyper-util", 1634 1634 + "rustls", 1635 1635 + "tokio", 1636 1636 + "tokio-rustls", 1637 1637 + "tower-service", 1638 1638 + "webpki-roots 1.0.7", 1639 1639 + ] 1640 1640 + 1641 1641 + [[package]] 1642 1642 + name = "hyper-util" 1643 1643 + version = "0.1.20" 1644 1644 + source = "registry+https://github.com/rust-lang/crates.io-index" 1645 1645 + checksum = "96547c2556ec9d12fb1578c4eaf448b04993e7fb79cbaad930a656880a6bdfa0" 1646 1646 + dependencies = [ 1647 1647 + "base64", 1648 1648 + "bytes", 1649 1649 + "futures-channel", 1650 1650 + "futures-util", 1651 1651 + "http", 1652 1652 + "http-body", 1653 1653 + "hyper", 1654 1654 + "ipnet", 1655 1655 + "libc", 1656 1656 + "percent-encoding", 1657 1657 + "pin-project-lite", 1658 1658 + "socket2", 1659 1659 + "system-configuration", 1660 1660 + "tokio", 1661 1661 + "tower-service", 1662 1662 + "tracing", 1663 1663 + "windows-registry", 1664 1664 + ] 1665 1665 + 1666 1666 + [[package]] 907 1667 name = "icu_collections" 908 1668 version = "2.2.0" 909 1669 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 986 1746 ] 987 1747 988 1748 [[package]] 1749 1749 + name = "id-arena" 1750 1750 + version = "2.3.0" 1751 1751 + source = "registry+https://github.com/rust-lang/crates.io-index" 1752 1752 + checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954" 1753 1753 + 1754 1754 + [[package]] 989 1755 name = "ident_case" 990 1756 version = "1.0.1" 991 1757 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1043 1809 ] 1044 1810 1045 1811 [[package]] 1812 1812 + name = "ipconfig" 1813 1813 + version = "0.3.4" 1814 1814 + source = "registry+https://github.com/rust-lang/crates.io-index" 1815 1815 + checksum = "4d40460c0ce33d6ce4b0630ad68ff63d6661961c48b6dba35e5a4d81cfb48222" 1816 1816 + dependencies = [ 1817 1817 + "socket2", 1818 1818 + "widestring", 1819 1819 + "windows-registry", 1820 1820 + "windows-result", 1821 1821 + "windows-sys 0.61.2", 1822 1822 + ] 1823 1823 + 1824 1824 + [[package]] 1825 1825 + name = "ipnet" 1826 1826 + version = "2.12.0" 1827 1827 + source = "registry+https://github.com/rust-lang/crates.io-index" 1828 1828 + checksum = "d98f6fed1fde3f8c21bc40a1abb88dd75e67924f9cffc3ef95607bad8017f8e2" 1829 1829 + 1830 1830 + [[package]] 1046 1831 name = "is_ci" 1047 1832 version = "1.2.0" 1048 1833 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1104 1889 ] 1105 1890 1106 1891 [[package]] 1892 1892 + name = "k256" 1893 1893 + version = "0.13.4" 1894 1894 + source = "registry+https://github.com/rust-lang/crates.io-index" 1895 1895 + checksum = "f6e3919bbaa2945715f0bb6d3934a173d1e9a59ac23767fbaaef277265a7411b" 1896 1896 + dependencies = [ 1897 1897 + "cfg-if", 1898 1898 + "ecdsa", 1899 1899 + "elliptic-curve", 1900 1900 + "once_cell", 1901 1901 + "sha2 0.10.9", 1902 1902 + "signature", 1903 1903 + ] 1904 1904 + 1905 1905 + [[package]] 1107 1906 name = "keccak" 1108 1907 version = "0.1.6" 1109 1908 source = "registry+https://github.com/rust-lang/crates.io-index" 1110 1909 checksum = "cb26cec98cce3a3d96cbb7bced3c4b16e3d13f27ec56dbd62cbc8f39cfb9d653" 1111 1910 dependencies = [ 1112 1112 - "cpufeatures", 1911 1911 + "cpufeatures 0.2.17", 1113 1912 ] 1114 1913 1115 1914 [[package]] ··· 1168 1967 ] 1169 1968 1170 1969 [[package]] 1970 1970 + name = "leb128fmt" 1971 1971 + version = "0.1.0" 1972 1972 + source = "registry+https://github.com/rust-lang/crates.io-index" 1973 1973 + checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" 1974 1974 + 1975 1975 + [[package]] 1171 1976 name = "libc" 1172 1977 version = "0.2.186" 1173 1978 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1251 2056 ] 1252 2057 1253 2058 [[package]] 2059 2059 + name = "lru" 2060 2060 + version = "0.16.4" 2061 2061 + source = "registry+https://github.com/rust-lang/crates.io-index" 2062 2062 + checksum = "7f66e8d5d03f609abc3a39e6f08e4164ebf1447a732906d39eb9b99b7919ef39" 2063 2063 + dependencies = [ 2064 2064 + "hashbrown 0.16.1", 2065 2065 + ] 2066 2066 + 2067 2067 + [[package]] 2068 2068 + name = "lru-slab" 2069 2069 + version = "0.1.2" 2070 2070 + source = "registry+https://github.com/rust-lang/crates.io-index" 2071 2071 + checksum = "112b39cec0b298b6c1999fee3e31427f74f676e4cb9879ed1a121b43661a4154" 2072 2072 + 2073 2073 + [[package]] 1254 2074 name = "malachite" 1255 2075 version = "0.9.1" 1256 2076 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1313 2133 ] 1314 2134 1315 2135 [[package]] 2136 2136 + name = "match-lookup" 2137 2137 + version = "0.1.2" 2138 2138 + source = "registry+https://github.com/rust-lang/crates.io-index" 2139 2139 + checksum = "757aee279b8bdbb9f9e676796fd459e4207a1f986e87886700abf589f5abf771" 2140 2140 + dependencies = [ 2141 2141 + "proc-macro2", 2142 2142 + "quote", 2143 2143 + "syn", 2144 2144 + ] 2145 2145 + 2146 2146 + [[package]] 1316 2147 name = "md-5" 1317 2148 version = "0.10.6" 1318 2149 source = "registry+https://github.com/rust-lang/crates.io-index" 1319 2150 checksum = "d89e7ee0cfbedfc4da3340218492196241d89eefb6dab27de5df917a6d2e78cf" 1320 2151 dependencies = [ 1321 2152 "cfg-if", 1322 1322 - "digest", 2153 2153 + "digest 0.10.7", 1323 2154 ] 1324 2155 1325 2156 [[package]] ··· 1359 2190 ] 1360 2191 1361 2192 [[package]] 2193 2193 + name = "mime" 2194 2194 + version = "0.3.17" 2195 2195 + source = "registry+https://github.com/rust-lang/crates.io-index" 2196 2196 + checksum = "6877bb514081ee2a7ff5ef9de3281f14a4dd4bceac4c09388074a6b5df8a139a" 2197 2197 + 2198 2198 + [[package]] 2199 2199 + name = "mime_guess" 2200 2200 + version = "2.0.5" 2201 2201 + source = "registry+https://github.com/rust-lang/crates.io-index" 2202 2202 + checksum = "f7c44f8e672c00fe5308fa235f821cb4198414e1c77935c1ab6948d3fd78550e" 2203 2203 + dependencies = [ 2204 2204 + "mime", 2205 2205 + "unicase", 2206 2206 + ] 2207 2207 + 2208 2208 + [[package]] 1362 2209 name = "minimad" 1363 2210 version = "0.14.0" 1364 2211 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1393 2240 name = "mlang_http" 1394 2241 version = "0.1.0" 1395 2242 dependencies = [ 2243 2243 + "atproto-client", 2244 2244 + "atproto-identity", 2245 2245 + "atproto-record", 1396 2246 "nickel-lang-core", 2247 2247 + "reqwest", 1397 2248 "serde_json", 2249 2249 + "tokio", 1398 2250 "ureq", 1399 2251 ] 1400 2252 1401 2253 [[package]] 2254 2254 + name = "moka" 2255 2255 + version = "0.12.15" 2256 2256 + source = "registry+https://github.com/rust-lang/crates.io-index" 2257 2257 + checksum = "957228ad12042ee839f93c8f257b62b4c0ab5eaae1d4fa60de53b27c9d7c5046" 2258 2258 + dependencies = [ 2259 2259 + "crossbeam-channel", 2260 2260 + "crossbeam-epoch", 2261 2261 + "crossbeam-utils", 2262 2262 + "equivalent", 2263 2263 + "parking_lot", 2264 2264 + "portable-atomic", 2265 2265 + "smallvec", 2266 2266 + "tagptr", 2267 2267 + "uuid", 2268 2268 + ] 2269 2269 + 2270 2270 + [[package]] 2271 2271 + name = "multibase" 2272 2272 + version = "0.9.2" 2273 2273 + source = "registry+https://github.com/rust-lang/crates.io-index" 2274 2274 + checksum = "8694bb4835f452b0e3bb06dbebb1d6fc5385b6ca1caf2e55fd165c042390ec77" 2275 2275 + dependencies = [ 2276 2276 + "base-x", 2277 2277 + "base256emoji", 2278 2278 + "data-encoding", 2279 2279 + "data-encoding-macro", 2280 2280 + ] 2281 2281 + 2282 2282 + [[package]] 2283 2283 + name = "multihash" 2284 2284 + version = "0.19.5" 2285 2285 + source = "registry+https://github.com/rust-lang/crates.io-index" 2286 2286 + checksum = "577c63b00ad74d57e8c9aa870b5fccebf2fd64a308a5aee9f1bb88e4aea19447" 2287 2287 + dependencies = [ 2288 2288 + "unsigned-varint", 2289 2289 + ] 2290 2290 + 2291 2291 + [[package]] 1402 2292 name = "new_debug_unreachable" 1403 2293 version = "1.0.6" 1404 2294 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1449 2339 "serde_json", 1450 2340 "serde_yaml", 1451 2341 "sha-1", 1452 1452 - "sha2", 2342 2342 + "sha2 0.10.9", 1453 2343 "simple-counter", 1454 2344 "smallvec", 1455 2345 "strip-ansi-escapes", ··· 1519 2409 checksum = "521739c6d2bac4aa25192232afe6841231376b2b26d4d9fae5ecf8ca5772e441" 1520 2410 1521 2411 [[package]] 2412 2412 + name = "num-traits" 2413 2413 + version = "0.2.19" 2414 2414 + source = "registry+https://github.com/rust-lang/crates.io-index" 2415 2415 + checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" 2416 2416 + dependencies = [ 2417 2417 + "autocfg", 2418 2418 + ] 2419 2419 + 2420 2420 + [[package]] 1522 2421 name = "object" 1523 2422 version = "0.37.3" 1524 2423 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1532 2431 version = "1.21.4" 1533 2432 source = "registry+https://github.com/rust-lang/crates.io-index" 1534 2433 checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" 2434 2434 + dependencies = [ 2435 2435 + "critical-section", 2436 2436 + "portable-atomic", 2437 2437 + ] 1535 2438 1536 2439 [[package]] 1537 2440 name = "once_cell_polyfill" ··· 1592 2495 checksum = "d211803b9b6b570f68772237e415a029d5a50c65d382910b879fb19d3271f94d" 1593 2496 1594 2497 [[package]] 2498 2498 + name = "p256" 2499 2499 + version = "0.13.2" 2500 2500 + source = "registry+https://github.com/rust-lang/crates.io-index" 2501 2501 + checksum = "c9863ad85fa8f4460f9c48cb909d38a0d689dba1f6f6988a5e3e0d31071bcd4b" 2502 2502 + dependencies = [ 2503 2503 + "ecdsa", 2504 2504 + "elliptic-curve", 2505 2505 + "primeorder", 2506 2506 + "serdect", 2507 2507 + "sha2 0.10.9", 2508 2508 + ] 2509 2509 + 2510 2510 + [[package]] 2511 2511 + name = "p384" 2512 2512 + version = "0.13.1" 2513 2513 + source = "registry+https://github.com/rust-lang/crates.io-index" 2514 2514 + checksum = "fe42f1670a52a47d448f14b6a5c61dd78fce51856e68edaa38f7ae3a46b8d6b6" 2515 2515 + dependencies = [ 2516 2516 + "ecdsa", 2517 2517 + "elliptic-curve", 2518 2518 + "primeorder", 2519 2519 + "serdect", 2520 2520 + "sha2 0.10.9", 2521 2521 + ] 2522 2522 + 2523 2523 + [[package]] 1595 2524 name = "parking_lot" 1596 2525 version = "0.12.5" 1597 2526 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1621 2550 checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" 1622 2551 1623 2552 [[package]] 2553 2553 + name = "pem-rfc7468" 2554 2554 + version = "0.7.0" 2555 2555 + source = "registry+https://github.com/rust-lang/crates.io-index" 2556 2556 + checksum = "88b39c9bfcfc231068454382784bb460aae594343fb030d46e9f50a645418412" 2557 2557 + dependencies = [ 2558 2558 + "base64ct", 2559 2559 + ] 2560 2560 + 2561 2561 + [[package]] 1624 2562 name = "percent-encoding" 1625 2563 version = "2.3.2" 1626 2564 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1667 2605 checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" 1668 2606 1669 2607 [[package]] 2608 2608 + name = "pkcs8" 2609 2609 + version = "0.10.2" 2610 2610 + source = "registry+https://github.com/rust-lang/crates.io-index" 2611 2611 + checksum = "f950b2377845cebe5cf8b5165cb3cc1a5e0fa5cfa3e1f7f55707d8fd82e0a7b7" 2612 2612 + dependencies = [ 2613 2613 + "der", 2614 2614 + "spki", 2615 2615 + ] 2616 2616 + 2617 2617 + [[package]] 1670 2618 name = "pkg-config" 1671 2619 version = "0.3.33" 1672 2620 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1686 2634 ] 1687 2635 1688 2636 [[package]] 2637 2637 + name = "portable-atomic" 2638 2638 + version = "1.13.1" 2639 2639 + source = "registry+https://github.com/rust-lang/crates.io-index" 2640 2640 + checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49" 2641 2641 + 2642 2642 + [[package]] 1689 2643 name = "potential_utf" 1690 2644 version = "0.1.5" 1691 2645 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1701 2655 checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" 1702 2656 1703 2657 [[package]] 2658 2658 + name = "ppv-lite86" 2659 2659 + version = "0.2.21" 2660 2660 + source = "registry+https://github.com/rust-lang/crates.io-index" 2661 2661 + checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" 2662 2662 + dependencies = [ 2663 2663 + "zerocopy", 2664 2664 + ] 2665 2665 + 2666 2666 + [[package]] 1704 2667 name = "precomputed-hash" 1705 2668 version = "0.1.1" 1706 2669 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1712 2675 source = "registry+https://github.com/rust-lang/crates.io-index" 1713 2676 checksum = "0d22152487193190344590e4f30e219cf3fe140d9e7a3fdb683d82aa2c5f4156" 1714 2677 dependencies = [ 1715 1715 - "arrayvec", 2678 2678 + "arrayvec 0.5.2", 1716 2679 "typed-arena", 1717 2680 "unicode-width 0.2.2", 1718 2681 ] ··· 1747 2710 ] 1748 2711 1749 2712 [[package]] 2713 2713 + name = "primeorder" 2714 2714 + version = "0.13.6" 2715 2715 + source = "registry+https://github.com/rust-lang/crates.io-index" 2716 2716 + checksum = "353e1ca18966c16d9deb1c69278edbc5f194139612772bd9537af60ac231e1e6" 2717 2717 + dependencies = [ 2718 2718 + "elliptic-curve", 2719 2719 + "serdect", 2720 2720 + ] 2721 2721 + 2722 2722 + [[package]] 1750 2723 name = "proc-macro2" 1751 2724 version = "1.0.106" 1752 2725 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1778 2751 ] 1779 2752 1780 2753 [[package]] 2754 2754 + name = "quinn" 2755 2755 + version = "0.11.9" 2756 2756 + source = "registry+https://github.com/rust-lang/crates.io-index" 2757 2757 + checksum = "b9e20a958963c291dc322d98411f541009df2ced7b5a4f2bd52337638cfccf20" 2758 2758 + dependencies = [ 2759 2759 + "bytes", 2760 2760 + "cfg_aliases", 2761 2761 + "pin-project-lite", 2762 2762 + "quinn-proto", 2763 2763 + "quinn-udp", 2764 2764 + "rustc-hash", 2765 2765 + "rustls", 2766 2766 + "socket2", 2767 2767 + "thiserror 2.0.18", 2768 2768 + "tokio", 2769 2769 + "tracing", 2770 2770 + "web-time", 2771 2771 + ] 2772 2772 + 2773 2773 + [[package]] 2774 2774 + name = "quinn-proto" 2775 2775 + version = "0.11.14" 2776 2776 + source = "registry+https://github.com/rust-lang/crates.io-index" 2777 2777 + checksum = "434b42fec591c96ef50e21e886936e66d3cc3f737104fdb9b737c40ffb94c098" 2778 2778 + dependencies = [ 2779 2779 + "bytes", 2780 2780 + "getrandom 0.3.4", 2781 2781 + "lru-slab", 2782 2782 + "rand 0.9.4", 2783 2783 + "ring", 2784 2784 + "rustc-hash", 2785 2785 + "rustls", 2786 2786 + "rustls-pki-types", 2787 2787 + "slab", 2788 2788 + "thiserror 2.0.18", 2789 2789 + "tinyvec", 2790 2790 + "tracing", 2791 2791 + "web-time", 2792 2792 + ] 2793 2793 + 2794 2794 + [[package]] 2795 2795 + name = "quinn-udp" 2796 2796 + version = "0.5.14" 2797 2797 + source = "registry+https://github.com/rust-lang/crates.io-index" 2798 2798 + checksum = "addec6a0dcad8a8d96a771f815f0eaf55f9d1805756410b39f5fa81332574cbd" 2799 2799 + dependencies = [ 2800 2800 + "cfg_aliases", 2801 2801 + "libc", 2802 2802 + "once_cell", 2803 2803 + "socket2", 2804 2804 + "tracing", 2805 2805 + "windows-sys 0.59.0", 2806 2806 + ] 2807 2807 + 2808 2808 + [[package]] 1781 2809 name = "quote" 1782 2810 version = "1.0.45" 1783 2811 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1785 2813 dependencies = [ 1786 2814 "proc-macro2", 1787 2815 ] 2816 2816 + 2817 2817 + [[package]] 2818 2818 + name = "r-efi" 2819 2819 + version = "5.3.0" 2820 2820 + source = "registry+https://github.com/rust-lang/crates.io-index" 2821 2821 + checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" 2822 2822 + 2823 2823 + [[package]] 2824 2824 + name = "r-efi" 2825 2825 + version = "6.0.0" 2826 2826 + source = "registry+https://github.com/rust-lang/crates.io-index" 2827 2827 + checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" 1788 2828 1789 2829 [[package]] 1790 2830 name = "radix_trie" ··· 1797 2837 ] 1798 2838 1799 2839 [[package]] 2840 2840 + name = "rand" 2841 2841 + version = "0.9.4" 2842 2842 + source = "registry+https://github.com/rust-lang/crates.io-index" 2843 2843 + checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" 2844 2844 + dependencies = [ 2845 2845 + "rand_chacha", 2846 2846 + "rand_core 0.9.5", 2847 2847 + ] 2848 2848 + 2849 2849 + [[package]] 2850 2850 + name = "rand" 2851 2851 + version = "0.10.1" 2852 2852 + source = "registry+https://github.com/rust-lang/crates.io-index" 2853 2853 + checksum = "d2e8e8bcc7961af1fdac401278c6a831614941f6164ee3bf4ce61b7edb162207" 2854 2854 + dependencies = [ 2855 2855 + "chacha20", 2856 2856 + "getrandom 0.4.2", 2857 2857 + "rand_core 0.10.1", 2858 2858 + ] 2859 2859 + 2860 2860 + [[package]] 2861 2861 + name = "rand_chacha" 2862 2862 + version = "0.9.0" 2863 2863 + source = "registry+https://github.com/rust-lang/crates.io-index" 2864 2864 + checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" 2865 2865 + dependencies = [ 2866 2866 + "ppv-lite86", 2867 2867 + "rand_core 0.9.5", 2868 2868 + ] 2869 2869 + 2870 2870 + [[package]] 2871 2871 + name = "rand_core" 2872 2872 + version = "0.6.4" 2873 2873 + source = "registry+https://github.com/rust-lang/crates.io-index" 2874 2874 + checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" 2875 2875 + dependencies = [ 2876 2876 + "getrandom 0.2.17", 2877 2877 + ] 2878 2878 + 2879 2879 + [[package]] 2880 2880 + name = "rand_core" 2881 2881 + version = "0.9.5" 2882 2882 + source = "registry+https://github.com/rust-lang/crates.io-index" 2883 2883 + checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" 2884 2884 + dependencies = [ 2885 2885 + "getrandom 0.3.4", 2886 2886 + ] 2887 2887 + 2888 2888 + [[package]] 2889 2889 + name = "rand_core" 2890 2890 + version = "0.10.1" 2891 2891 + source = "registry+https://github.com/rust-lang/crates.io-index" 2892 2892 + checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69" 2893 2893 + 2894 2894 + [[package]] 1800 2895 name = "rayon" 1801 2896 version = "1.12.0" 1802 2897 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1855 2950 checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a" 1856 2951 1857 2952 [[package]] 2953 2953 + name = "reqwest" 2954 2954 + version = "0.12.28" 2955 2955 + source = "registry+https://github.com/rust-lang/crates.io-index" 2956 2956 + checksum = "eddd3ca559203180a307f12d114c268abf583f59b03cb906fd0b3ff8646c1147" 2957 2957 + dependencies = [ 2958 2958 + "base64", 2959 2959 + "bytes", 2960 2960 + "encoding_rs", 2961 2961 + "futures-core", 2962 2962 + "futures-util", 2963 2963 + "h2", 2964 2964 + "http", 2965 2965 + "http-body", 2966 2966 + "http-body-util", 2967 2967 + "hyper", 2968 2968 + "hyper-rustls", 2969 2969 + "hyper-util", 2970 2970 + "js-sys", 2971 2971 + "log", 2972 2972 + "mime", 2973 2973 + "mime_guess", 2974 2974 + "percent-encoding", 2975 2975 + "pin-project-lite", 2976 2976 + "quinn", 2977 2977 + "rustls", 2978 2978 + "rustls-pki-types", 2979 2979 + "serde", 2980 2980 + "serde_json", 2981 2981 + "serde_urlencoded", 2982 2982 + "sync_wrapper", 2983 2983 + "tokio", 2984 2984 + "tokio-rustls", 2985 2985 + "tower", 2986 2986 + "tower-http", 2987 2987 + "tower-service", 2988 2988 + "url", 2989 2989 + "wasm-bindgen", 2990 2990 + "wasm-bindgen-futures", 2991 2991 + "web-sys", 2992 2992 + "webpki-roots 1.0.7", 2993 2993 + ] 2994 2994 + 2995 2995 + [[package]] 2996 2996 + name = "reqwest-chain" 2997 2997 + version = "1.0.0" 2998 2998 + source = "registry+https://github.com/rust-lang/crates.io-index" 2999 2999 + checksum = "da5c014fb79a8227db44a0433d748107750d2550b7fca55c59a3d7ee7d2ee2b2" 3000 3000 + dependencies = [ 3001 3001 + "anyhow", 3002 3002 + "async-trait", 3003 3003 + "http", 3004 3004 + "reqwest-middleware", 3005 3005 + ] 3006 3006 + 3007 3007 + [[package]] 3008 3008 + name = "reqwest-middleware" 3009 3009 + version = "0.4.2" 3010 3010 + source = "registry+https://github.com/rust-lang/crates.io-index" 3011 3011 + checksum = "57f17d28a6e6acfe1733fe24bcd30774d13bffa4b8a22535b4c8c98423088d4e" 3012 3012 + dependencies = [ 3013 3013 + "anyhow", 3014 3014 + "async-trait", 3015 3015 + "http", 3016 3016 + "reqwest", 3017 3017 + "serde", 3018 3018 + "thiserror 1.0.69", 3019 3019 + "tower-service", 3020 3020 + ] 3021 3021 + 3022 3022 + [[package]] 3023 3023 + name = "resolv-conf" 3024 3024 + version = "0.7.6" 3025 3025 + source = "registry+https://github.com/rust-lang/crates.io-index" 3026 3026 + checksum = "1e061d1b48cb8d38042de4ae0a7a6401009d6143dc80d2e2d6f31f0bdd6470c7" 3027 3027 + 3028 3028 + [[package]] 3029 3029 + name = "rfc6979" 3030 3030 + version = "0.4.0" 3031 3031 + source = "registry+https://github.com/rust-lang/crates.io-index" 3032 3032 + checksum = "f8dd2a808d456c4a54e300a23e9f5a67e122c3024119acbfd73e3bf664491cb2" 3033 3033 + dependencies = [ 3034 3034 + "hmac", 3035 3035 + "subtle", 3036 3036 + ] 3037 3037 + 3038 3038 + [[package]] 1858 3039 name = "ring" 1859 3040 version = "0.17.14" 1860 3041 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1862 3043 dependencies = [ 1863 3044 "cc", 1864 3045 "cfg-if", 1865 1865 - "getrandom", 3046 3046 + "getrandom 0.2.17", 1866 3047 "libc", 1867 3048 "untrusted", 1868 3049 "windows-sys 0.52.0", ··· 1875 3056 checksum = "b50b8869d9fc858ce7266cce0194bd74df58b9d0e3f6df3a9fc8eb470d95c09d" 1876 3057 1877 3058 [[package]] 3059 3059 + name = "rustc-hash" 3060 3060 + version = "2.1.2" 3061 3061 + source = "registry+https://github.com/rust-lang/crates.io-index" 3062 3062 + checksum = "94300abf3f1ae2e2b8ffb7b58043de3d399c73fa6f4b73826402a5c457614dbe" 3063 3063 + 3064 3064 + [[package]] 1878 3065 name = "rustc_version" 1879 3066 version = "0.4.1" 1880 3067 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 1893 3080 "errno", 1894 3081 "libc", 1895 3082 "linux-raw-sys", 1896 1896 - "windows-sys 0.52.0", 3083 3083 + "windows-sys 0.61.2", 1897 3084 ] 1898 3085 1899 3086 [[package]] ··· 1917 3104 source = "registry+https://github.com/rust-lang/crates.io-index" 1918 3105 checksum = "30a7197ae7eb376e574fe940d068c30fe0462554a3ddbe4eca7838e049c937a9" 1919 3106 dependencies = [ 3107 3107 + "web-time", 1920 3108 "zeroize", 1921 3109 ] 1922 3110 ··· 2011 3199 checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" 2012 3200 2013 3201 [[package]] 3202 3202 + name = "sec1" 3203 3203 + version = "0.7.3" 3204 3204 + source = "registry+https://github.com/rust-lang/crates.io-index" 3205 3205 + checksum = "d3e97a565f76233a6003f9f5c54be1d9c5bdfa3eccfb189469f11ec4901c47dc" 3206 3206 + dependencies = [ 3207 3207 + "base16ct", 3208 3208 + "der", 3209 3209 + "generic-array", 3210 3210 + "pkcs8", 3211 3211 + "serdect", 3212 3212 + "subtle", 3213 3213 + "zeroize", 3214 3214 + ] 3215 3215 + 3216 3216 + [[package]] 2014 3217 name = "semver" 2015 3218 version = "1.0.28" 2016 3219 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2024 3227 dependencies = [ 2025 3228 "serde_core", 2026 3229 "serde_derive", 3230 3230 + ] 3231 3231 + 3232 3232 + [[package]] 3233 3233 + name = "serde_bytes" 3234 3234 + version = "0.11.19" 3235 3235 + source = "registry+https://github.com/rust-lang/crates.io-index" 3236 3236 + checksum = "a5d440709e79d88e51ac01c4b72fc6cb7314017bb7da9eeff678aa94c10e3ea8" 3237 3237 + dependencies = [ 3238 3238 + "serde", 3239 3239 + "serde_core", 2027 3240 ] 2028 3241 2029 3242 [[package]] ··· 2070 3283 ] 2071 3284 2072 3285 [[package]] 3286 3286 + name = "serde_urlencoded" 3287 3287 + version = "0.7.1" 3288 3288 + source = "registry+https://github.com/rust-lang/crates.io-index" 3289 3289 + checksum = "d3491c14715ca2294c4d6a88f15e84739788c1d030eed8c110436aafdaa2f3fd" 3290 3290 + dependencies = [ 3291 3291 + "form_urlencoded", 3292 3292 + "itoa", 3293 3293 + "ryu", 3294 3294 + "serde", 3295 3295 + ] 3296 3296 + 3297 3297 + [[package]] 2073 3298 name = "serde_yaml" 2074 3299 version = "0.9.34+deprecated" 2075 3300 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2083 3308 ] 2084 3309 2085 3310 [[package]] 3311 3311 + name = "serdect" 3312 3312 + version = "0.2.0" 3313 3313 + source = "registry+https://github.com/rust-lang/crates.io-index" 3314 3314 + checksum = "a84f14a19e9a014bb9f4512488d9829a68e04ecabffb0f9904cd1ace94598177" 3315 3315 + dependencies = [ 3316 3316 + "base16ct", 3317 3317 + "serde", 3318 3318 + ] 3319 3319 + 3320 3320 + [[package]] 2086 3321 name = "sha-1" 2087 3322 version = "0.10.1" 2088 3323 source = "registry+https://github.com/rust-lang/crates.io-index" 2089 3324 checksum = "f5058ada175748e33390e40e872bd0fe59a19f265d0158daa551c5a88a76009c" 2090 3325 dependencies = [ 2091 3326 "cfg-if", 2092 2092 - "cpufeatures", 2093 2093 - "digest", 3327 3327 + "cpufeatures 0.2.17", 3328 3328 + "digest 0.10.7", 2094 3329 ] 2095 3330 2096 3331 [[package]] ··· 2100 3335 checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283" 2101 3336 dependencies = [ 2102 3337 "cfg-if", 2103 2103 - "cpufeatures", 2104 2104 - "digest", 3338 3338 + "cpufeatures 0.2.17", 3339 3339 + "digest 0.10.7", 3340 3340 + ] 3341 3341 + 3342 3342 + [[package]] 3343 3343 + name = "sha2" 3344 3344 + version = "0.11.0" 3345 3345 + source = "registry+https://github.com/rust-lang/crates.io-index" 3346 3346 + checksum = "446ba717509524cb3f22f17ecc096f10f4822d76ab5c0b9822c5f9c284e825f4" 3347 3347 + dependencies = [ 3348 3348 + "cfg-if", 3349 3349 + "cpufeatures 0.3.0", 3350 3350 + "digest 0.11.3", 2105 3351 ] 2106 3352 2107 3353 [[package]] ··· 2110 3356 source = "registry+https://github.com/rust-lang/crates.io-index" 2111 3357 checksum = "77fd7028345d415a4034cf8777cd4f8ab1851274233b45f84e3d955502d93874" 2112 3358 dependencies = [ 2113 2113 - "digest", 3359 3359 + "digest 0.10.7", 2114 3360 "keccak", 2115 3361 ] 2116 3362 ··· 2158 3404 ] 2159 3405 2160 3406 [[package]] 3407 3407 + name = "signature" 3408 3408 + version = "2.2.0" 3409 3409 + source = "registry+https://github.com/rust-lang/crates.io-index" 3410 3410 + checksum = "77549399552de45a898a580c1b41d445bf730df867cc44e6c0233bbc4b8329de" 3411 3411 + dependencies = [ 3412 3412 + "digest 0.10.7", 3413 3413 + "rand_core 0.6.4", 3414 3414 + ] 3415 3415 + 3416 3416 + [[package]] 2161 3417 name = "simd-adler32" 2162 3418 version = "0.3.9" 2163 3419 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2188 3444 checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" 2189 3445 2190 3446 [[package]] 3447 3447 + name = "socket2" 3448 3448 + version = "0.6.4" 3449 3449 + source = "registry+https://github.com/rust-lang/crates.io-index" 3450 3450 + checksum = "52d1cfed4120b4d927bf7c0f86d2087a4a7d6027c906d9f9d525a80573b9be51" 3451 3451 + dependencies = [ 3452 3452 + "libc", 3453 3453 + "windows-sys 0.61.2", 3454 3454 + ] 3455 3455 + 3456 3456 + [[package]] 3457 3457 + name = "spki" 3458 3458 + version = "0.7.3" 3459 3459 + source = "registry+https://github.com/rust-lang/crates.io-index" 3460 3460 + checksum = "d91ed6c858b01f942cd56b37a94b3e0a1798290327d1236e4d9cf4eaca44d29d" 3461 3461 + dependencies = [ 3462 3462 + "base64ct", 3463 3463 + "der", 3464 3464 + ] 3465 3465 + 3466 3466 + [[package]] 2191 3467 name = "stable_deref_trait" 2192 3468 version = "1.2.1" 2193 3469 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2277 3553 ] 2278 3554 2279 3555 [[package]] 3556 3556 + name = "sync_wrapper" 3557 3557 + version = "1.0.2" 3558 3558 + source = "registry+https://github.com/rust-lang/crates.io-index" 3559 3559 + checksum = "0bf256ce5efdfa370213c1dabab5935a12e49f2c58d15e9eac2870d3b4f27263" 3560 3560 + dependencies = [ 3561 3561 + "futures-core", 3562 3562 + ] 3563 3563 + 3564 3564 + [[package]] 2280 3565 name = "synstructure" 2281 3566 version = "0.13.2" 2282 3567 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2304 3589 "serde", 2305 3590 "serde_derive", 2306 3591 "serde_json", 2307 2307 - "thiserror", 3592 3592 + "thiserror 2.0.18", 2308 3593 "walkdir", 2309 3594 "yaml-rust", 2310 3595 ] 2311 3596 2312 3597 [[package]] 3598 3598 + name = "system-configuration" 3599 3599 + version = "0.7.0" 3600 3600 + source = "registry+https://github.com/rust-lang/crates.io-index" 3601 3601 + checksum = "a13f3d0daba03132c0aa9767f98351b3488edc2c100cda2d2ec2b04f3d8d3c8b" 3602 3602 + dependencies = [ 3603 3603 + "bitflags", 3604 3604 + "core-foundation", 3605 3605 + "system-configuration-sys", 3606 3606 + ] 3607 3607 + 3608 3608 + [[package]] 3609 3609 + name = "system-configuration-sys" 3610 3610 + version = "0.6.0" 3611 3611 + source = "registry+https://github.com/rust-lang/crates.io-index" 3612 3612 + checksum = "8e1d1b10ced5ca923a1fcb8d03e96b8d3268065d724548c0211415ff6ac6bac4" 3613 3613 + dependencies = [ 3614 3614 + "core-foundation-sys", 3615 3615 + "libc", 3616 3616 + ] 3617 3617 + 3618 3618 + [[package]] 3619 3619 + name = "tagptr" 3620 3620 + version = "0.2.0" 3621 3621 + source = "registry+https://github.com/rust-lang/crates.io-index" 3622 3622 + checksum = "7b2093cf4c8eb1e67749a6762251bc9cd836b6fc171623bd0a9d324d37af2417" 3623 3623 + 3624 3624 + [[package]] 3625 3625 + name = "tempfile" 3626 3626 + version = "3.27.0" 3627 3627 + source = "registry+https://github.com/rust-lang/crates.io-index" 3628 3628 + checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" 3629 3629 + dependencies = [ 3630 3630 + "fastrand", 3631 3631 + "getrandom 0.4.2", 3632 3632 + "once_cell", 3633 3633 + "rustix", 3634 3634 + "windows-sys 0.61.2", 3635 3635 + ] 3636 3636 + 3637 3637 + [[package]] 2313 3638 name = "term" 2314 3639 version = "1.2.1" 2315 3640 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2339 3664 "lazy-regex", 2340 3665 "minimad", 2341 3666 "serde", 2342 2342 - "thiserror", 3667 3667 + "thiserror 2.0.18", 2343 3668 "unicode-width 0.1.14", 2344 3669 ] 2345 3670 ··· 2365 3690 2366 3691 [[package]] 2367 3692 name = "thiserror" 3693 3693 + version = "1.0.69" 3694 3694 + source = "registry+https://github.com/rust-lang/crates.io-index" 3695 3695 + checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" 3696 3696 + dependencies = [ 3697 3697 + "thiserror-impl 1.0.69", 3698 3698 + ] 3699 3699 + 3700 3700 + [[package]] 3701 3701 + name = "thiserror" 2368 3702 version = "2.0.18" 2369 3703 source = "registry+https://github.com/rust-lang/crates.io-index" 2370 3704 checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4" 2371 3705 dependencies = [ 2372 2372 - "thiserror-impl", 3706 3706 + "thiserror-impl 2.0.18", 3707 3707 + ] 3708 3708 + 3709 3709 + [[package]] 3710 3710 + name = "thiserror-impl" 3711 3711 + version = "1.0.69" 3712 3712 + source = "registry+https://github.com/rust-lang/crates.io-index" 3713 3713 + checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" 3714 3714 + dependencies = [ 3715 3715 + "proc-macro2", 3716 3716 + "quote", 3717 3717 + "syn", 2373 3718 ] 2374 3719 2375 3720 [[package]] ··· 2445 3790 source = "registry+https://github.com/rust-lang/crates.io-index" 2446 3791 checksum = "8fc7f01b389ac15039e4dc9531aa973a135d7a4135281b12d7c1bc79fd57fffe" 2447 3792 dependencies = [ 3793 3793 + "bytes", 3794 3794 + "libc", 3795 3795 + "mio", 2448 3796 "pin-project-lite", 3797 3797 + "socket2", 2449 3798 "tokio-macros", 3799 3799 + "windows-sys 0.61.2", 2450 3800 ] 2451 3801 2452 3802 [[package]] ··· 2461 3811 ] 2462 3812 2463 3813 [[package]] 3814 3814 + name = "tokio-rustls" 3815 3815 + version = "0.26.4" 3816 3816 + source = "registry+https://github.com/rust-lang/crates.io-index" 3817 3817 + checksum = "1729aa945f29d91ba541258c8df89027d5792d85a8841fb65e8bf0f4ede4ef61" 3818 3818 + dependencies = [ 3819 3819 + "rustls", 3820 3820 + "tokio", 3821 3821 + ] 3822 3822 + 3823 3823 + [[package]] 3824 3824 + name = "tokio-util" 3825 3825 + version = "0.7.18" 3826 3826 + source = "registry+https://github.com/rust-lang/crates.io-index" 3827 3827 + checksum = "9ae9cec805b01e8fc3fd2fe289f89149a9b66dd16786abd8b19cfa7b48cb0098" 3828 3828 + dependencies = [ 3829 3829 + "bytes", 3830 3830 + "futures-core", 3831 3831 + "futures-sink", 3832 3832 + "pin-project-lite", 3833 3833 + "tokio", 3834 3834 + ] 3835 3835 + 3836 3836 + [[package]] 2464 3837 name = "toml" 2465 3838 version = "0.9.12+spec-1.1.0" 2466 3839 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2528 3901 "serde", 2529 3902 "serde_json", 2530 3903 "streaming-iterator", 2531 2531 - "thiserror", 3904 3904 + "thiserror 2.0.18", 2532 3905 "tokio", 2533 3906 "topiary-tree-sitter-facade", 2534 3907 "topiary-web-tree-sitter-sys", ··· 2569 3942 ] 2570 3943 2571 3944 [[package]] 3945 3945 + name = "tower" 3946 3946 + version = "0.5.3" 3947 3947 + source = "registry+https://github.com/rust-lang/crates.io-index" 3948 3948 + checksum = "ebe5ef63511595f1344e2d5cfa636d973292adc0eec1f0ad45fae9f0851ab1d4" 3949 3949 + dependencies = [ 3950 3950 + "futures-core", 3951 3951 + "futures-util", 3952 3952 + "pin-project-lite", 3953 3953 + "sync_wrapper", 3954 3954 + "tokio", 3955 3955 + "tower-layer", 3956 3956 + "tower-service", 3957 3957 + ] 3958 3958 + 3959 3959 + [[package]] 3960 3960 + name = "tower-http" 3961 3961 + version = "0.6.11" 3962 3962 + source = "registry+https://github.com/rust-lang/crates.io-index" 3963 3963 + checksum = "4cfcf7e2740e6fc6d4d688b4ef00650406bb94adf4731e43c096c3a19fe40840" 3964 3964 + dependencies = [ 3965 3965 + "bitflags", 3966 3966 + "bytes", 3967 3967 + "futures-util", 3968 3968 + "http", 3969 3969 + "http-body", 3970 3970 + "pin-project-lite", 3971 3971 + "tower", 3972 3972 + "tower-layer", 3973 3973 + "tower-service", 3974 3974 + "url", 3975 3975 + ] 3976 3976 + 3977 3977 + [[package]] 3978 3978 + name = "tower-layer" 3979 3979 + version = "0.3.3" 3980 3980 + source = "registry+https://github.com/rust-lang/crates.io-index" 3981 3981 + checksum = "121c2a6cda46980bb0fcd1647ffaf6cd3fc79a013de288782836f6df9c48780e" 3982 3982 + 3983 3983 + [[package]] 3984 3984 + name = "tower-service" 3985 3985 + version = "0.3.3" 3986 3986 + source = "registry+https://github.com/rust-lang/crates.io-index" 3987 3987 + checksum = "8df9b6e13f2d32c91b9bd719c00d1958837bc7dec474d94952798cc8e69eeec3" 3988 3988 + 3989 3989 + [[package]] 3990 3990 + name = "tracing" 3991 3991 + version = "0.1.44" 3992 3992 + source = "registry+https://github.com/rust-lang/crates.io-index" 3993 3993 + checksum = "63e71662fa4b2a2c3a26f570f037eb95bb1f85397f3cd8076caed2f026a6d100" 3994 3994 + dependencies = [ 3995 3995 + "pin-project-lite", 3996 3996 + "tracing-attributes", 3997 3997 + "tracing-core", 3998 3998 + ] 3999 3999 + 4000 4000 + [[package]] 4001 4001 + name = "tracing-attributes" 4002 4002 + version = "0.1.31" 4003 4003 + source = "registry+https://github.com/rust-lang/crates.io-index" 4004 4004 + checksum = "7490cfa5ec963746568740651ac6781f701c9c5ea257c58e057f3ba8cf69e8da" 4005 4005 + dependencies = [ 4006 4006 + "proc-macro2", 4007 4007 + "quote", 4008 4008 + "syn", 4009 4009 + ] 4010 4010 + 4011 4011 + [[package]] 4012 4012 + name = "tracing-core" 4013 4013 + version = "0.1.36" 4014 4014 + source = "registry+https://github.com/rust-lang/crates.io-index" 4015 4015 + checksum = "db97caf9d906fbde555dd62fa95ddba9eecfd14cb388e4f491a66d74cd5fb79a" 4016 4016 + dependencies = [ 4017 4017 + "once_cell", 4018 4018 + ] 4019 4019 + 4020 4020 + [[package]] 2572 4021 name = "tree-sitter" 2573 4022 version = "0.26.9" 2574 4023 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2600 4049 ] 2601 4050 2602 4051 [[package]] 4052 4052 + name = "try-lock" 4053 4053 + version = "0.2.5" 4054 4054 + source = "registry+https://github.com/rust-lang/crates.io-index" 4055 4055 + checksum = "e421abadd41a4225275504ea4d6566923418b7f05506fbc9c0fe86ba7396114b" 4056 4056 + 4057 4057 + [[package]] 2603 4058 name = "typed-arena" 2604 4059 version = "2.0.2" 2605 4060 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2612 4067 checksum = "b6f5e870be6c3b371b77fe0ee0bafb859fa4964b4404c27de1d380043c4dda20" 2613 4068 2614 4069 [[package]] 4070 4070 + name = "ulid" 4071 4071 + version = "1.2.1" 4072 4072 + source = "registry+https://github.com/rust-lang/crates.io-index" 4073 4073 + checksum = "470dbf6591da1b39d43c14523b2b469c86879a53e8b758c8e090a470fe7b1fbe" 4074 4074 + dependencies = [ 4075 4075 + "rand 0.9.4", 4076 4076 + "web-time", 4077 4077 + ] 4078 4078 + 4079 4079 + [[package]] 4080 4080 + name = "unicase" 4081 4081 + version = "2.9.0" 4082 4082 + source = "registry+https://github.com/rust-lang/crates.io-index" 4083 4083 + checksum = "dbc4bc3a9f746d862c45cb89d705aa10f187bb96c76001afab07a0d35ce60142" 4084 4084 + 4085 4085 + [[package]] 2615 4086 name = "unicode-ident" 2616 4087 version = "1.0.24" 2617 4088 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2667 4138 version = "0.2.11" 2668 4139 source = "registry+https://github.com/rust-lang/crates.io-index" 2669 4140 checksum = "673aac59facbab8a9007c7f6108d11f63b603f7cabff99fabf650fea5c32b861" 4141 4141 + 4142 4142 + [[package]] 4143 4143 + name = "unsigned-varint" 4144 4144 + version = "0.8.0" 4145 4145 + source = "registry+https://github.com/rust-lang/crates.io-index" 4146 4146 + checksum = "eb066959b24b5196ae73cb057f45598450d2c5f71460e98c49b738086eff9c06" 2670 4147 2671 4148 [[package]] 2672 4149 name = "untrusted" ··· 2703 4180 ] 2704 4181 2705 4182 [[package]] 4183 4183 + name = "urlencoding" 4184 4184 + version = "2.1.3" 4185 4185 + source = "registry+https://github.com/rust-lang/crates.io-index" 4186 4186 + checksum = "daf8dba3b7eb870caf1ddeed7bc9d2a049f3cfdfae7cb521b087cc33ae4c49da" 4187 4187 + 4188 4188 + [[package]] 2706 4189 name = "utf8_iter" 2707 4190 version = "1.0.4" 2708 4191 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2715 4198 checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" 2716 4199 2717 4200 [[package]] 4201 4201 + name = "uuid" 4202 4202 + version = "1.23.2" 4203 4203 + source = "registry+https://github.com/rust-lang/crates.io-index" 4204 4204 + checksum = "d258b83ceec21034727ecee8c382cfa6c3e133699b0742c64571814fb420c9f7" 4205 4205 + dependencies = [ 4206 4206 + "getrandom 0.4.2", 4207 4207 + "js-sys", 4208 4208 + "wasm-bindgen", 4209 4209 + ] 4210 4210 + 4211 4211 + [[package]] 2718 4212 name = "version_check" 2719 4213 version = "0.9.5" 2720 4214 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2740 4234 ] 2741 4235 2742 4236 [[package]] 4237 4237 + name = "want" 4238 4238 + version = "0.3.1" 4239 4239 + source = "registry+https://github.com/rust-lang/crates.io-index" 4240 4240 + checksum = "bfa7760aed19e106de2c7c0b581b509f2f25d3dacaf737cb82ac61bc6d760b0e" 4241 4241 + dependencies = [ 4242 4242 + "try-lock", 4243 4243 + ] 4244 4244 + 4245 4245 + [[package]] 2743 4246 name = "wasi" 2744 4247 version = "0.11.1+wasi-snapshot-preview1" 2745 4248 source = "registry+https://github.com/rust-lang/crates.io-index" 2746 4249 checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" 4250 4250 + 4251 4251 + [[package]] 4252 4252 + name = "wasip2" 4253 4253 + version = "1.0.3+wasi-0.2.9" 4254 4254 + source = "registry+https://github.com/rust-lang/crates.io-index" 4255 4255 + checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6" 4256 4256 + dependencies = [ 4257 4257 + "wit-bindgen 0.57.1", 4258 4258 + ] 4259 4259 + 4260 4260 + [[package]] 4261 4261 + name = "wasip3" 4262 4262 + version = "0.4.0+wasi-0.3.0-rc-2026-01-06" 4263 4263 + source = "registry+https://github.com/rust-lang/crates.io-index" 4264 4264 + checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5" 4265 4265 + dependencies = [ 4266 4266 + "wit-bindgen 0.51.0", 4267 4267 + ] 2747 4268 2748 4269 [[package]] 2749 4270 name = "wasm-bindgen" ··· 2817 4338 ] 2818 4339 2819 4340 [[package]] 4341 4341 + name = "wasm-encoder" 4342 4342 + version = "0.244.0" 4343 4343 + source = "registry+https://github.com/rust-lang/crates.io-index" 4344 4344 + checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319" 4345 4345 + dependencies = [ 4346 4346 + "leb128fmt", 4347 4347 + "wasmparser", 4348 4348 + ] 4349 4349 + 4350 4350 + [[package]] 4351 4351 + name = "wasm-metadata" 4352 4352 + version = "0.244.0" 4353 4353 + source = "registry+https://github.com/rust-lang/crates.io-index" 4354 4354 + checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909" 4355 4355 + dependencies = [ 4356 4356 + "anyhow", 4357 4357 + "indexmap", 4358 4358 + "wasm-encoder", 4359 4359 + "wasmparser", 4360 4360 + ] 4361 4361 + 4362 4362 + [[package]] 4363 4363 + name = "wasmparser" 4364 4364 + version = "0.244.0" 4365 4365 + source = "registry+https://github.com/rust-lang/crates.io-index" 4366 4366 + checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" 4367 4367 + dependencies = [ 4368 4368 + "bitflags", 4369 4369 + "hashbrown 0.15.5", 4370 4370 + "indexmap", 4371 4371 + "semver", 4372 4372 + ] 4373 4373 + 4374 4374 + [[package]] 2820 4375 name = "web-sys" 2821 4376 version = "0.3.77" 2822 4377 source = "registry+https://github.com/rust-lang/crates.io-index" 2823 4378 checksum = "33b6dd2ef9186f1f2072e409e99cd22a975331a6b3591b12c764e0e55c60d5d2" 4379 4379 + dependencies = [ 4380 4380 + "js-sys", 4381 4381 + "wasm-bindgen", 4382 4382 + ] 4383 4383 + 4384 4384 + [[package]] 4385 4385 + name = "web-time" 4386 4386 + version = "1.1.0" 4387 4387 + source = "registry+https://github.com/rust-lang/crates.io-index" 4388 4388 + checksum = "5a6580f308b1fad9207618087a65c04e7a10bc77e02c8e84e9b00dd4b12fa0bb" 2824 4389 dependencies = [ 2825 4390 "js-sys", 2826 4391 "wasm-bindgen", ··· 2855 4420 ] 2856 4421 2857 4422 [[package]] 4423 4423 + name = "widestring" 4424 4424 + version = "1.2.1" 4425 4425 + source = "registry+https://github.com/rust-lang/crates.io-index" 4426 4426 + checksum = "72069c3113ab32ab29e5584db3c6ec55d416895e60715417b5b883a357c3e471" 4427 4427 + 4428 4428 + [[package]] 2858 4429 name = "winapi" 2859 4430 version = "0.3.9" 2860 4431 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2876 4447 source = "registry+https://github.com/rust-lang/crates.io-index" 2877 4448 checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" 2878 4449 dependencies = [ 2879 2879 - "windows-sys 0.52.0", 4450 4450 + "windows-sys 0.61.2", 2880 4451 ] 2881 4452 2882 4453 [[package]] ··· 2892 4463 checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" 2893 4464 2894 4465 [[package]] 4466 4466 + name = "windows-registry" 4467 4467 + version = "0.6.1" 4468 4468 + source = "registry+https://github.com/rust-lang/crates.io-index" 4469 4469 + checksum = "02752bf7fbdcce7f2a27a742f798510f3e5ad88dbe84871e5168e2120c3d5720" 4470 4470 + dependencies = [ 4471 4471 + "windows-link", 4472 4472 + "windows-result", 4473 4473 + "windows-strings", 4474 4474 + ] 4475 4475 + 4476 4476 + [[package]] 4477 4477 + name = "windows-result" 4478 4478 + version = "0.4.1" 4479 4479 + source = "registry+https://github.com/rust-lang/crates.io-index" 4480 4480 + checksum = "7781fa89eaf60850ac3d2da7af8e5242a5ea78d1a11c49bf2910bb5a73853eb5" 4481 4481 + dependencies = [ 4482 4482 + "windows-link", 4483 4483 + ] 4484 4484 + 4485 4485 + [[package]] 4486 4486 + name = "windows-strings" 4487 4487 + version = "0.5.1" 4488 4488 + source = "registry+https://github.com/rust-lang/crates.io-index" 4489 4489 + checksum = "7837d08f69c77cf6b07689544538e017c1bfcf57e34b4c0ff58e6c2cd3b37091" 4490 4490 + dependencies = [ 4491 4491 + "windows-link", 4492 4492 + ] 4493 4493 + 4494 4494 + [[package]] 2895 4495 name = "windows-sys" 2896 4496 version = "0.52.0" 2897 4497 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 2998 4598 checksum = "0592e1c9d151f854e6fd382574c3a0855250e1d9b2f99d9281c6e6391af352f1" 2999 4599 3000 4600 [[package]] 4601 4601 + name = "wit-bindgen" 4602 4602 + version = "0.51.0" 4603 4603 + source = "registry+https://github.com/rust-lang/crates.io-index" 4604 4604 + checksum = "d7249219f66ced02969388cf2bb044a09756a083d0fab1e566056b04d9fbcaa5" 4605 4605 + dependencies = [ 4606 4606 + "wit-bindgen-rust-macro", 4607 4607 + ] 4608 4608 + 4609 4609 + [[package]] 4610 4610 + name = "wit-bindgen" 4611 4611 + version = "0.57.1" 4612 4612 + source = "registry+https://github.com/rust-lang/crates.io-index" 4613 4613 + checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" 4614 4614 + 4615 4615 + [[package]] 4616 4616 + name = "wit-bindgen-core" 4617 4617 + version = "0.51.0" 4618 4618 + source = "registry+https://github.com/rust-lang/crates.io-index" 4619 4619 + checksum = "ea61de684c3ea68cb082b7a88508a8b27fcc8b797d738bfc99a82facf1d752dc" 4620 4620 + dependencies = [ 4621 4621 + "anyhow", 4622 4622 + "heck 0.5.0", 4623 4623 + "wit-parser", 4624 4624 + ] 4625 4625 + 4626 4626 + [[package]] 4627 4627 + name = "wit-bindgen-rust" 4628 4628 + version = "0.51.0" 4629 4629 + source = "registry+https://github.com/rust-lang/crates.io-index" 4630 4630 + checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21" 4631 4631 + dependencies = [ 4632 4632 + "anyhow", 4633 4633 + "heck 0.5.0", 4634 4634 + "indexmap", 4635 4635 + "prettyplease", 4636 4636 + "syn", 4637 4637 + "wasm-metadata", 4638 4638 + "wit-bindgen-core", 4639 4639 + "wit-component", 4640 4640 + ] 4641 4641 + 4642 4642 + [[package]] 4643 4643 + name = "wit-bindgen-rust-macro" 4644 4644 + version = "0.51.0" 4645 4645 + source = "registry+https://github.com/rust-lang/crates.io-index" 4646 4646 + checksum = "0c0f9bfd77e6a48eccf51359e3ae77140a7f50b1e2ebfe62422d8afdaffab17a" 4647 4647 + dependencies = [ 4648 4648 + "anyhow", 4649 4649 + "prettyplease", 4650 4650 + "proc-macro2", 4651 4651 + "quote", 4652 4652 + "syn", 4653 4653 + "wit-bindgen-core", 4654 4654 + "wit-bindgen-rust", 4655 4655 + ] 4656 4656 + 4657 4657 + [[package]] 4658 4658 + name = "wit-component" 4659 4659 + version = "0.244.0" 4660 4660 + source = "registry+https://github.com/rust-lang/crates.io-index" 4661 4661 + checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" 4662 4662 + dependencies = [ 4663 4663 + "anyhow", 4664 4664 + "bitflags", 4665 4665 + "indexmap", 4666 4666 + "log", 4667 4667 + "serde", 4668 4668 + "serde_derive", 4669 4669 + "serde_json", 4670 4670 + "wasm-encoder", 4671 4671 + "wasm-metadata", 4672 4672 + "wasmparser", 4673 4673 + "wit-parser", 4674 4674 + ] 4675 4675 + 4676 4676 + [[package]] 4677 4677 + name = "wit-parser" 4678 4678 + version = "0.244.0" 4679 4679 + source = "registry+https://github.com/rust-lang/crates.io-index" 4680 4680 + checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" 4681 4681 + dependencies = [ 4682 4682 + "anyhow", 4683 4683 + "id-arena", 4684 4684 + "indexmap", 4685 4685 + "log", 4686 4686 + "semver", 4687 4687 + "serde", 4688 4688 + "serde_derive", 4689 4689 + "serde_json", 4690 4690 + "unicode-xid", 4691 4691 + "wasmparser", 4692 4692 + ] 4693 4693 + 4694 4694 + [[package]] 3001 4695 name = "writeable" 3002 4696 version = "0.6.3" 3003 4697 source = "registry+https://github.com/rust-lang/crates.io-index" ··· 3045 4739 "quote", 3046 4740 "syn", 3047 4741 "synstructure", 4742 4742 + ] 4743 4743 + 4744 4744 + [[package]] 4745 4745 + name = "zerocopy" 4746 4746 + version = "0.8.50" 4747 4747 + source = "registry+https://github.com/rust-lang/crates.io-index" 4748 4748 + checksum = "3b065d4f0e55f82fae73202e189638116a87c55ab6b8e6c2721e13dd9d854ad1" 4749 4749 + dependencies = [ 4750 4750 + "zerocopy-derive", 4751 4751 + ] 4752 4752 + 4753 4753 + [[package]] 4754 4754 + name = "zerocopy-derive" 4755 4755 + version = "0.8.50" 4756 4756 + source = "registry+https://github.com/rust-lang/crates.io-index" 4757 4757 + checksum = "0b631b19d36a892ab55420c92dbc83ccd79274f25be714855d3074aa71cab639" 4758 4758 + dependencies = [ 4759 4759 + "proc-macro2", 4760 4760 + "quote", 4761 4761 + "syn", 3048 4762 ] 3049 4763 3050 4764 [[package]]

+5

native/mlang_http/Cargo.toml

View file Reviewed

··· 7 7 crate-type = ["staticlib"] 8 8 9 9 [dependencies] 10 10 + atproto-client = "0.14" 11 11 + atproto-identity = "0.14" 12 12 + atproto-record = "0.14" 10 13 nickel-lang-core = "0.17" 14 14 + reqwest = { version = "0.12", default-features = false, features = ["json", "rustls-tls"] } 11 15 serde_json = "1" 16 16 + tokio = { version = "1", features = ["rt-multi-thread"] } 12 17 ureq = { version = "2.10", default-features = true }

+67 -7

native/mlang_http/src/lib.rs

View file Reviewed

··· 1 1 + use atproto_client::{HttpRecordResolver, RecordResolver}; 2 2 + use atproto_identity::resolve::{HickoryDnsResolver, InnerIdentityResolver, SharedIdentityResolver}; 3 3 + use atproto_record::aturi::ATURI; 1 4 use nickel_lang_core::deserialize; 2 5 use std::ffi::{CStr, CString}; 3 6 use std::io::Read; 4 7 use std::os::raw::c_char; 5 8 use std::ptr; 9 9 + use std::str::FromStr; 10 10 + use std::sync::Arc; 6 11 7 12 fn render_json_value(value: &serde_json::Value) -> Result<String, String> { 8 13 match value { ··· 13 18 Ok(i.to_string()) 14 19 } else if let Some(u) = n.as_u64() { 15 20 Ok(u.to_string()) 16 16 - } else if let Some(f) = n.as_f64() { 17 17 - if f.fract() == 0.0 { 18 18 - Ok(format!("{:.0}", f)) 19 19 - } else { 20 20 - Err(format!("non-integer Nickel number is not supported: {n}")) 21 21 - } 22 21 } else { 23 23 - Err(format!("non-integer Nickel number is not supported: {n}")) 22 22 + Ok(n.to_string()) 24 23 } 25 24 } 26 25 serde_json::Value::String(s) => serde_json::to_string(s) ··· 72 71 let value: serde_json::Value = 73 72 serde_json::from_str(source).map_err(|err| format!("{err}"))?; 74 73 render_json_value(&value) 74 74 + } 75 75 + 76 76 + fn aturi_to_data_string(source: &str) -> Result<String, String> { 77 77 + ATURI::from_str(source).map_err(|err| format!("{err}"))?; 78 78 + let runtime = tokio::runtime::Runtime::new() 79 79 + .map_err(|err| format!("failed to create Tokio runtime: {err}"))?; 80 80 + let value: serde_json::Value = runtime 81 81 + .block_on(async { 82 82 + let http_client = reqwest::Client::new(); 83 83 + let dns_resolver = Arc::new(HickoryDnsResolver::create_resolver(&[])); 84 84 + let identity_resolver = SharedIdentityResolver(Arc::new(InnerIdentityResolver { 85 85 + dns_resolver, 86 86 + http_client: http_client.clone(), 87 87 + plc_hostname: "plc.directory".to_owned(), 88 88 + })); 89 89 + let resolver = HttpRecordResolver::new(http_client, Arc::new(identity_resolver)); 90 90 + resolver.resolve(source).await 91 91 + }) 92 92 + .map_err(|err| format!("AT-URI lookup failed: {err}"))?; 93 93 + let body = 94 94 + serde_json::to_string(&value).map_err(|err| format!("failed to encode record: {err}"))?; 95 95 + json_to_data_string(&body) 75 96 } 76 97 77 98 fn alloc_c_string(s: String) -> *mut c_char { ··· 256 277 } 257 278 } 258 279 } 280 280 + 281 281 + #[no_mangle] 282 282 + pub extern "C" fn mlang_aturi_parse( 283 283 + source: *const c_char, 284 284 + out_body: *mut *mut c_char, 285 285 + out_error: *mut *mut c_char, 286 286 + ) -> i32 { 287 287 + if source.is_null() || out_body.is_null() || out_error.is_null() { 288 288 + return 0; 289 289 + } 290 290 + unsafe { 291 291 + *out_body = ptr::null_mut(); 292 292 + *out_error = ptr::null_mut(); 293 293 + } 294 294 + let source = unsafe { CStr::from_ptr(source) }; 295 295 + let source = match source.to_str() { 296 296 + Ok(source) => source, 297 297 + Err(err) => { 298 298 + unsafe { 299 299 + *out_error = alloc_c_string(format!("invalid AT-URI UTF-8: {err}")); 300 300 + } 301 301 + return 0; 302 302 + } 303 303 + }; 304 304 + match aturi_to_data_string(source) { 305 305 + Ok(rendered) => { 306 306 + unsafe { 307 307 + *out_body = alloc_c_string(rendered); 308 308 + } 309 309 + 1 310 310 + } 311 311 + Err(err) => { 312 312 + unsafe { 313 313 + *out_error = alloc_c_string(format!("AT-URI parse error: {err}")); 314 314 + } 315 315 + 0 316 316 + } 317 317 + } 318 318 + }

+9

native/mlang_http_ffi.c

View file Reviewed

··· 7 7 extern uint8_t mlang_nickel_eval(const char *source, char **out_body, char **out_error); 8 8 extern uint8_t mlang_nickel_eval_file(const char *path, char **out_body, char **out_error); 9 9 extern uint8_t mlang_json_eval(const char *source, char **out_body, char **out_error); 10 10 + extern uint8_t mlang_aturi_parse(const char *source, char **out_body, char **out_error); 10 11 extern void mlang_http_string_free(char *ptr); 11 12 extern lean_obj_res lean_mk_io_user_error(lean_obj_arg msg); 12 13 ··· 74 75 uint8_t ok = mlang_json_eval(lean_string_cstr(source), &body, &error); 75 76 return wrap_string_result(ok, body, error); 76 77 } 78 78 + 79 79 + LEAN_EXPORT lean_obj_res mlang_aturi_parse_string(b_lean_obj_arg source, lean_obj_arg world) { 80 80 + (void)world; 81 81 + char *body = NULL; 82 82 + char *error = NULL; 83 83 + uint8_t ok = mlang_aturi_parse(lean_string_cstr(source), &body, &error); 84 84 + return wrap_string_result(ok, body, error); 85 85 + }