Skip to content

Commit

Permalink
[ fix ] Fix the order of search, look for already derived before hinted
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed May 29, 2023
1 parent 13aa82b commit 2abfe8c
Showing 1 changed file with 15 additions and 17 deletions.
32 changes: 15 additions & 17 deletions src/Deriving/DepTyCheck/Gen/Checked.idr
Original file line number Diff line number Diff line change
Expand Up @@ -110,37 +110,35 @@ namespace ClojuringCanonicImpl
DerivatorCore => ClojuringContext m => Elaboration m => CanonicGen m where
callGen sig fuel values = do

--- check if no derivation is needed ---

-- look for external gens, and call it if exists
let Nothing = lookupLengthChecked sig !ask
| Just (name, Element extSig lenEq) => pure $ callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values

-- look for existing already derived (internal) gen, use it if exists
let Nothing = lookup sig !get
| Just internalGenName => pure $ callCanonic sig internalGenName fuel values

-- look for very external gens, i.e. those that can be reached with `%search`
canonicSigType <- try .| check (canonicSig sig)
.| fail "INTERNAL ERROR: canonic signature of \{show sig.targetType.name} is not a type"
Nothing <- search canonicSigType
| Just found => flip (foldl app) values <$> flip app fuel <$> quote found

-- get the name of internal gen, derive if necessary
internalGenName <- do

-- look for existing (already derived) internals, use it if exists
let Nothing = lookup sig !get
| Just name => pure name

-- nothing found, then derive! acquire the name
let name = nameForGen sig
--- nothing's found, then derive! ---

-- remember that we're responsible for this signature derivation
modify $ insert sig name
-- acquire the name
let internalGenName = nameForGen sig

-- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle
(genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig name
-- remember that we're responsible for this signature derivation
modify $ insert sig internalGenName

-- remember the derived stuff
tell ([genFunClaim], [genFunBody])
-- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle
(genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig internalGenName

-- return the name of the newly derived generator
pure name
-- remember the derived stuff
tell ([genFunClaim], [genFunBody])

-- call the internal gen
pure $ callCanonic sig internalGenName fuel values
Expand Down

0 comments on commit 2abfe8c

Please sign in to comment.